History of Addition in N

	Revision 5 . . November 17, 2001 9:57 pm by The Anome
	Revision 4 . . November 17, 2001 12:12 pm by AxelBoldt [simplify proofs: start with zero, don't use associativity for commutativity proof]
	Revision 3 . . (edit) November 13, 2001 2:08 am by Clemens Fruhwirth [spelling]

---

Difference (from prior major revision) (no other diffs)

Changed: 43,45c43,46

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+)

Changed: 51,52c52,53

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)+

Changed: 56,57c57

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+)+.

Changed: 65,66c65,66

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.