Replace x and y in theorem 1 with x' and x, respectively.

Have you defined the string a - b? If not, you cannot use that type of algebra, as the symbol "-" has not been defined, nor have you defined the concept of additive inverse (the set of natural numbers has no additive inverses), so it is not apparent that the concept of addition has a unique inverse operation per addend.