Proof: (a+b)+c+ = [by AP2] ((a+b)+c)+ = [by hypothesis] (a+(b+c))+ = [by AP2] a+(b+c)+ = [by AP2] a+(b+c+) |
Proof: :(a+b)+c+ = [by AP2] ((a+b)+c)+ = [by hypothesis] :(a+(b+c))+ = [by AP2] a+(b+c)+ = [by AP2] :a+(b+c+) |
Hypothesis: a++b = (a+b)+ Base: a++0 = [by AP1] a+ = [by AP1] (a+0)+ |
:Hypothesis: a++b = (a+b)+ :Base: a++0 = [by AP1] a+ = [by AP1] (a+0)+ |
a++b+ = [by AP2] (a++b)+ = [by hypothesis] (a+b)++ = [by AP2] (a+b+)+. |
:a++b+ = [by AP2] (a++b)+ = [by hypothesis] (a+b)++ = [by AP2] (a+b+)+. |
a+b+ = [by AP2] (a+b)+ = [by hypothesis] (b+a)+ = [by previous proof] b++a. |
:a+b+ = [by AP2] (a+b)+ = [by hypothesis] :(b+a)+ = [by previous proof] b++a. |
The operation of addition, commonly written as infix operator +, is a function of N x N -> N
a + b = c
a and b are called the addend, while c is being called sum.
By convention, a+ is referred as the successor of a as defined in the Peano postulates.
The first is referred as AP1, the second as AP2.
FIXME: missing
By the principle of mathematical induction:
Hypothesis: (a+b)+c = a+(b+c)
Base: (a+b)+0 = a+(b+0)
Proof: (a+b)+0 = [by AP1] a+b = [by AP1] a+(b+0).
Induction step: (a+b)+c+ = a+(b+c+)
Proof:
The principle of mathematical induction has to be employed twice:
Proof that: a++b+ = (a+b+)+
Hypothesis: a+b = b+a
Base: a+0=0+a
By [AP1].
Proof that: a+b+=b++a
FIXME: enhance visibility by nicer formatting