Prove: The ADD function function for natural numbers uniquely determined by:

ALL(a):ALL(b):[an & bn => add(a,b)n]
& ALL(a):[an => add(a,1)=next(a)]
& ALL(a):ALL(b):[an & bn => add1(a,next(b))=next(add1(a,b))]

Peano's Axioms

1	Set(n)
	& 1n
	& ALL(a):[an => next(a)n]
	& ALL(a):[an => ~next(a)=1]
	& ALL(a):ALL(b):[an & bn & next(a)=next(b) => a=b]
	& ALL(a):[Set(a) & 1a & ALL(b):[bn & ba => next(b)a]
	=> ALL(b):[bn => ba]]
	Premise

	
	Prove: ALL(a):ALL(b):[an & bn => add1(a,b)n]
	       & ALL(a):[an => add1(a,1)=next(a)]
	       & ALL(a):ALL(b):[an & bn => add1(a,next(b))=next(add1(a,b))]
	       & [ALL(a):ALL(b):[an & bn => add2(a,b)n]
	       & ALL(a):[an => add2(a,1)=next(a)]
	       & ALL(a):ALL(b):[an & bn => add2(a,next(b))=next(add2(a,b))]]
	
	       => ALL(b):[bn => ALL(a):[an => add1(a,b)=add2(a,b)]]
	
	Suppose we have two functions, add1 and add2, such that...

	2	ALL(a):ALL(b):[an & bn => add1(a,b)n]
		& ALL(a):[an => add1(a,1)=next(a)]
		& ALL(a):ALL(b):[an & bn => add1(a,next(b))=next(add1(a,b))]
		& [ALL(a):ALL(b):[an & bn => add2(a,b)n]
		& ALL(a):[an => add2(a,1)=next(a)]
		& ALL(a):ALL(b):[an & bn => add2(a,next(b))=next(add2(a,b))]]
		Premise

	3	ALL(a):ALL(b):[an & bn => add1(a,b)n]
		Split, 2

	4	ALL(a):[an => add1(a,1)=next(a)]
		Split, 2

	5	ALL(a):ALL(b):[an & bn => add1(a,next(b))=next(add1(a,b))]
		Split, 2

	6	ALL(a):ALL(b):[an & bn => add2(a,b)n]
		& ALL(a):[an => add2(a,1)=next(a)]
		& ALL(a):ALL(b):[an & bn => add2(a,next(b))=next(add2(a,b))]
		Split, 2

	7	ALL(a):ALL(b):[an & bn => add2(a,b)n]
		Split, 6

	8	ALL(a):[an => add2(a,1)=next(a)]
		Split, 6

	9	ALL(a):ALL(b):[an & bn => add2(a,next(b))=next(add2(a,b))]
		Split, 6

	10	pn => add1(p,1)=next(p)
		U Spec, 4

	11	pn => add2(p,1)=next(p)
		U Spec, 8

		12	pn
			Premise

		13	add2(p,1)=next(p)
			Detach, 11, 12

		14	add1(p,1)=next(p)
			Detach, 10, 12

		15	add1(p,1)=add2(p,1)
			Substitute, 13, 14

	16	pn => add1(p,1)=add2(p,1)
		Conclusion, 12

	17	ALL(b):[qn & bn => add1(q,next(b))=next(add1(q,b))]
		U Spec, 5

	18	qn & rn => add1(q,next(r))=next(add1(q,r))
		U Spec, 17

	19	ALL(b):[qn & bn => add2(q,next(b))=next(add2(q,b))]
		U Spec, 9

	20	qn & rn => add2(q,next(r))=next(add2(q,r))
		U Spec, 19

		21	qn & rn
			Premise

		22	add2(q,next(r))=next(add2(q,r))
			Detach, 20, 21

		23	add1(q,next(r))=next(add1(q,r))
			Detach, 18, 21

			24	add1(q,r)=add2(q,r)
				Premise

			25	add1(q,next(r))=next(add2(q,r))
				Substitute, 24, 23

			26	add1(q,next(r))=add2(q,next(r))
				Substitute, 22, 25

		27	add1(q,r)=add2(q,r)
			=> add1(q,next(r))=add2(q,next(r))
			Conclusion, 24

	28	qn & rn
		=> [add1(q,r)=add2(q,r)
		=> add1(q,next(r))=add2(q,next(r))]
		Conclusion, 21

	29	ALL(a):[an => add1(a,1)=add2(a,1)]
		& ALL(b):[bn & ALL(a):[an => add1(a,b)=add2(a,b)] => ALL(a):[an => add1(a,next(b))=add2(a,next(b))]]
		=> ALL(b):[bn => ALL(a):[an => add1(a,b)=add2(a,b)]]
		Induction

	30	ALL(a):[an => add1(a,1)=add2(a,1)]
		U Gen, 16

		31	rn
			Premise

			32	ALL(a):[an => add1(a,r)=add2(a,r)]
				Premise

			33	qn => add1(q,r)=add2(q,r)
				U Spec, 32

				34	qn
					Premise

				35	qn & rn
					Join, 34, 31

				36	add1(q,r)=add2(q,r)
					Detach, 33, 34

				37	add1(q,r)=add2(q,r)
					=> add1(q,next(r))=add2(q,next(r))
					Detach, 28, 35

				38	add1(q,next(r))=add2(q,next(r))
					Detach, 37, 36

			39	qn => add1(q,next(r))=add2(q,next(r))
				Conclusion, 34

			40	ALL(a):[an => add1(a,next(r))=add2(a,next(r))]
				U Gen, 39

		41	ALL(a):[an => add1(a,r)=add2(a,r)]
			=> ALL(a):[an => add1(a,next(r))=add2(a,next(r))]
			Conclusion, 32

		42	rn
			& [ALL(a):[an => add1(a,r)=add2(a,r)]
			=> ALL(a):[an => add1(a,next(r))=add2(a,next(r))]]
			Join, 31, 41

	43	rn
		=> rn
		& [ALL(a):[an => add1(a,r)=add2(a,r)]
		=> ALL(a):[an => add1(a,next(r))=add2(a,next(r))]]
		Conclusion, 31

		44	rn & ALL(a):[an => add1(a,r)=add2(a,r)]
			Premise

		45	rn
			Split, 44

		46	ALL(a):[an => add1(a,r)=add2(a,r)]
			Split, 44

		47	rn
			& [ALL(a):[an => add1(a,r)=add2(a,r)]
			=> ALL(a):[an => add1(a,next(r))=add2(a,next(r))]]
			Detach, 43, 45

		48	rn
			Split, 47

		49	ALL(a):[an => add1(a,r)=add2(a,r)]
			=> ALL(a):[an => add1(a,next(r))=add2(a,next(r))]
			Split, 47

		50	ALL(a):[an => add1(a,next(r))=add2(a,next(r))]
			Detach, 49, 46

	51	rn & ALL(a):[an => add1(a,r)=add2(a,r)]
		=> ALL(a):[an => add1(a,next(r))=add2(a,next(r))]
		Conclusion, 44

	52	ALL(b):[bn & ALL(a):[an => add1(a,b)=add2(a,b)]
		=> ALL(a):[an => add1(a,next(b))=add2(a,next(b))]]
		U Gen, 51

	53	ALL(a):[an => add1(a,1)=add2(a,1)]
		& ALL(b):[bn & ALL(a):[an => add1(a,b)=add2(a,b)]
		=> ALL(a):[an => add1(a,next(b))=add2(a,next(b))]]
		Join, 30, 52

	54	ALL(b):[bn => ALL(a):[an => add1(a,b)=add2(a,b)]]
		Detach, 29, 53

As Required:

55	ALL(a):ALL(b):[an & bn => add1(a,b)n]
	& ALL(a):[an => add1(a,1)=next(a)]
	& ALL(a):ALL(b):[an & bn => add1(a,next(b))=next(add1(a,b))]
	& [ALL(a):ALL(b):[an & bn => add2(a,b)n]
	& ALL(a):[an => add2(a,1)=next(a)]
	& ALL(a):ALL(b):[an & bn => add2(a,next(b))=next(add2(a,b))]]
	=> ALL(b):[bn => ALL(a):[an => add1(a,b)=add2(a,b)]]
	Conclusion, 2

Generalizing...

56	ALL(add2):[ALL(a):ALL(b):[an & bn => add1(a,b)n]
	& ALL(a):[an => add1(a,1)=next(a)]
	& ALL(a):ALL(b):[an & bn => add1(a,next(b))=next(add1(a,b))]
	& [ALL(a):ALL(b):[an & bn => add2(a,b)n]
	& ALL(a):[an => add2(a,1)=next(a)]
	& ALL(a):ALL(b):[an & bn => add2(a,next(b))=next(add2(a,b))]]
	=> ALL(b):[bn => ALL(a):[an => add1(a,b)=add2(a,b)]]]
	U Gen, 55

As Required:

57	ALL(add1):ALL(add2):[ALL(a):ALL(b):[an & bn => add1(a,b)n]
	& ALL(a):[an => add1(a,1)=next(a)]
	& ALL(a):ALL(b):[an & bn => add1(a,next(b))=next(add1(a,b))]
	& [ALL(a):ALL(b):[an & bn => add2(a,b)n]
	& ALL(a):[an => add2(a,1)=next(a)]
	& ALL(a):ALL(b):[an & bn => add2(a,next(b))=next(add2(a,b))]]
	=> ALL(b):[bn => ALL(a):[an => add1(a,b)=add2(a,b)]]]
	U Gen, 56