Add Function

Introduction
------------

Here we construct the add function starting from Peano's Axioms such that, for all x, y in n:

  add(x,1)=next(x)

  add(x,next(y))=next(add(x,y))

where n = {1, 2, 3...} and next() is the usual successor function defined on n.

We also show that add is unique.


Peano's Axioms 
--------------

A1: Let n be a set

1	Set(n)
	Axiom

A2: Let 1 be an element of n

2	1 ε n
	Axiom

A3: Let next be a function mapping n to itself

3	ALL(a):[a ε n => next(a) ε n]
	Axiom

A4: 1 has no pre-image under next

4	ALL(a):[a ε n => ~next(a)=1]
	Axiom

A5: next is injective

5	ALL(a):ALL(b):[a ε n & b ε n & next(a)=next(b) => a=b]
	Axiom

A6: The Principle of Mathematical Induction

Here, we will use PMI directly to prove various propositions about the natural numbers. We will not
make use of the DC Proof Induction Shortcut.

6	ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => next(b) ε a]
	=> ALL(b):[b ε n => b ε a]]
	Axiom


Proof
-----

Begin by constructing the set n3 of ordered triples of natural numbers.

Applying the Cartesian Product Axiom...

7	ALL(a1):ALL(a2):ALL(a3):[Set(a1) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) ε b <=> c1 ε a1 & c2 ε a2 & c3 ε a3]]]
	Cart Prod

8	ALL(a2):ALL(a3):[Set(n) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) ε b <=> c1 ε n & c2 ε a2 & c3 ε a3]]]
	U Spec, 7

9	ALL(a3):[Set(n) & Set(n) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) ε b <=> c1 ε n & c2 ε n & c3 ε a3]]]
	U Spec, 8

10	Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) ε b <=> c1 ε n & c2 ε n & c3 ε n]]
	U Spec, 9

11	Set(n) & Set(n)
	Join, 1, 1

12	Set(n) & Set(n) & Set(n)
	Join, 11, 1

13	EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) ε b <=> c1 ε n & c2 ε n & c3 ε n]]
	Detach, 10, 12

14	Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) ε n3 <=> c1 ε n & c2 ε n & c3 ε n]
	E Spec, 13


Define: n3
----------

n3 is a set of ordered triples

15	Set''(n3)
	Split, 14

n3 is the set of all ordered triples of natural numbers

16	ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) ε n3 <=> c1 ε n & c2 ε n & c3 ε n]
	Split, 14


Apply Power Set Axiom to construct pn3, the power set of n3

17	ALL(a):[Set''(a) => EXIST(b):[Set(b)
	& ALL(c):[c ε b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε a]]]]
	Power Set

18	Set''(n3) => EXIST(b):[Set(b)
	& ALL(c):[c ε b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε n3]]]
	U Spec, 17

19	EXIST(b):[Set(b)
	& ALL(c):[c ε b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε n3]]]
	Detach, 18, 15

20	Set(pn3)
	& ALL(c):[c ε pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε n3]]
	E Spec, 19


Define: pn3
-----------

pn3 is a set

21	Set(pn3)
	Split, 20

pn3 is the power set of n3, i.e. the set of all subsets of n3

22	ALL(c):[c ε pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε c => (d1,d2,d3) ε n3]]
	Split, 20


Apply Subset Axiom to construct s

23	EXIST(sub):[Set(sub) & ALL(a):[a ε sub <=> a ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε a]
	& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε a => (b,next(c),next(d)) ε a]]]]]
	Subset, 21

24	Set(s) & ALL(a):[a ε s <=> a ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε a]
	& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε a => (b,next(c),next(d)) ε a]]]]
	E Spec, 23


Define: s
---------

s is a set

25	Set(s)
	Split, 24

Every element of s is a set of ordered triples of natural numbers

26	ALL(a):[a ε s <=> a ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε a]
	& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε a => (b,next(c),next(d)) ε a]]]]
	Split, 24


Apply Subset Axiom to construct add

27	EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) ε sub
	<=> (a,b,c) ε n3 & ALL(d):[d ε s => (a,b,c) ε d]]]
	Subset, 15

28	Set''(add) & ALL(a):ALL(b):ALL(c):[(a,b,c) ε add
	<=> (a,b,c) ε n3 & ALL(d):[d ε s => (a,b,c) ε d]]
	E Spec, 27


Define: add
-----------

add is a set of ordered triples

29	Set''(add)
	Split, 28

add is the intersection of all sets in s

30	ALL(a):ALL(b):ALL(c):[(a,b,c) ε add
	<=> (a,b,c) ε n3 & ALL(d):[d ε s => (a,b,c) ε d]]
	Split, 28


Apply the Function Axiom to determine sufficient conditions for functionality of add

31	ALL(f):ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) ε f => c1 ε a1 & c2 ε a2 & d ε b]
	& ALL(c1):ALL(c2):[c1 ε a1 & c2 ε a2 => EXIST(d):[d ε b & (c1,c2,d) ε f]]
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) ε f & (c1,c2,d2) ε f => d1=d2]
	=> ALL(c1):ALL(c2):ALL(d):[d=f(c1,c2) <=> (c1,c2,d) ε f]]
	Function

32	ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) ε add => c1 ε a1 & c2 ε a2 & d ε b]
	& ALL(c1):ALL(c2):[c1 ε a1 & c2 ε a2 => EXIST(d):[d ε b & (c1,c2,d) ε add]]
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) ε add & (c1,c2,d2) ε add => d1=d2]
	=> ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) ε add]]
	U Spec, 31

33	ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) ε add => c1 ε n & c2 ε a2 & d ε b]
	& ALL(c1):ALL(c2):[c1 ε n & c2 ε a2 => EXIST(d):[d ε b & (c1,c2,d) ε add]]
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) ε add & (c1,c2,d2) ε add => d1=d2]
	=> ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) ε add]]
	U Spec, 32

34	ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) ε add => c1 ε n & c2 ε n & d ε b]
	& ALL(c1):ALL(c2):[c1 ε n & c2 ε n => EXIST(d):[d ε b & (c1,c2,d) ε add]]
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) ε add & (c1,c2,d2) ε add => d1=d2]
	=> ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) ε add]]
	U Spec, 33

Sufficient: For functionality of add

35	ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) ε add => c1 ε n & c2 ε n & d ε n]
	& ALL(c1):ALL(c2):[c1 ε n & c2 ε n => EXIST(d):[d ε n & (c1,c2,d) ε add]]
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) ε add & (c1,c2,d2) ε add => d1=d2]
	=> ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) ε add]
	U Spec, 34

	
	Prove: ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) ε add => c1 ε n & c2 ε n & d ε n]
	
	Suppose...

	36	(x,y,z) ε add
		Premise

	Apply definition of add

	37	ALL(b):ALL(c):[(x,b,c) ε add
		<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
		U Spec, 30

	38	ALL(c):[(x,y,c) ε add
		<=> (x,y,c) ε n3 & ALL(d):[d ε s => (x,y,c) ε d]]
		U Spec, 37

	39	(x,y,z) ε add
		<=> (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
		U Spec, 38

	40	[(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]]
		& [(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add]
		Iff-And, 39

	41	(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
		Split, 40

	42	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add
		Split, 40

	43	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
		Detach, 41, 36

	44	(x,y,z) ε n3
		Split, 43

	45	ALL(d):[d ε s => (x,y,z) ε d]
		Split, 43

	Apply definition of n3

	46	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
		U Spec, 16

	47	ALL(c3):[(x,y,c3) ε n3 <=> x ε n & y ε n & c3 ε n]
		U Spec, 46

	48	(x,y,z) ε n3 <=> x ε n & y ε n & z ε n
		U Spec, 47

	49	[(x,y,z) ε n3 => x ε n & y ε n & z ε n]
		& [x ε n & y ε n & z ε n => (x,y,z) ε n3]
		Iff-And, 48

	50	(x,y,z) ε n3 => x ε n & y ε n & z ε n
		Split, 49

	51	x ε n & y ε n & z ε n => (x,y,z) ε n3
		Split, 49

	52	x ε n & y ε n & z ε n
		Detach, 50, 44

Functionality of add, Part 1

As Required:

53	ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) ε add => c1 ε n & c2 ε n & d ε n]
	Conclusion, 36

	Prove: ALL(a):[a ε n => ALL(b):[b ε n => EXIST(c):[c ε n & (a,b,c) ε add]]]
	
	Suppose...

	54	x ε n
		Premise

	Apply the Subset Axiom to construct the set p, which is to be used in conjunction with the 
	PMI (A6 above).

	55	EXIST(sub):[Set(sub) & ALL(b):[b ε sub <=> b ε n & EXIST(c):[c ε n & (x,b,c) ε add]]]
		Subset, 1

	56	Set(p) & ALL(b):[b ε p <=> b ε n & EXIST(c):[c ε n & (x,b,c) ε add]]
		E Spec, 55

	
	Define: p

	57	Set(p)
		Split, 56

	58	ALL(b):[b ε p <=> b ε n & EXIST(c):[c ε n & (x,b,c) ε add]]
		Split, 56

	Apply PMI

	59	Set(p) & 1 ε p & ALL(b):[b ε n & b ε p => next(b) ε p]
		=> ALL(b):[b ε n => b ε p]
		U Spec, 6

	Apply definition of p

	60	1 ε p <=> 1 ε n & EXIST(c):[c ε n & (x,1,c) ε add]
		U Spec, 58

	61	[1 ε p => 1 ε n & EXIST(c):[c ε n & (x,1,c) ε add]]
		& [1 ε n & EXIST(c):[c ε n & (x,1,c) ε add] => 1 ε p]
		Iff-And, 60

	62	1 ε p => 1 ε n & EXIST(c):[c ε n & (x,1,c) ε add]
		Split, 61

	Sufficient: For 1 ε p

	63	1 ε n & EXIST(c):[c ε n & (x,1,c) ε add] => 1 ε p
		Split, 61

	Apply definition of add

	64	ALL(b):ALL(c):[(x,b,c) ε add
		<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
		U Spec, 30

	65	ALL(c):[(x,1,c) ε add
		<=> (x,1,c) ε n3 & ALL(d):[d ε s => (x,1,c) ε d]]
		U Spec, 64

	66	(x,1,next(x)) ε add
		<=> (x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d]
		U Spec, 65

	67	[(x,1,next(x)) ε add => (x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d]]
		& [(x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d] => (x,1,next(x)) ε add]
		Iff-And, 66

	68	(x,1,next(x)) ε add => (x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d]
		Split, 67

	Sufficient: For (x,1,next(x)) ε add

	69	(x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d] => (x,1,next(x)) ε add
		Split, 67

	70	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
		U Spec, 16

	71	ALL(c3):[(x,1,c3) ε n3 <=> x ε n & 1 ε n & c3 ε n]
		U Spec, 70

	72	(x,1,next(x)) ε n3 <=> x ε n & 1 ε n & next(x) ε n
		U Spec, 71

	73	[(x,1,next(x)) ε n3 => x ε n & 1 ε n & next(x) ε n]
		& [x ε n & 1 ε n & next(x) ε n => (x,1,next(x)) ε n3]
		Iff-And, 72

	74	(x,1,next(x)) ε n3 => x ε n & 1 ε n & next(x) ε n
		Split, 73

	Sufficient: For (x,1,next(x)) ε n3

	75	x ε n & 1 ε n & next(x) ε n => (x,1,next(x)) ε n3
		Split, 73

	Apply axiom

	76	x ε n => next(x) ε n
		U Spec, 3

	77	next(x) ε n
		Detach, 76, 54

	78	x ε n & 1 ε n
		Join, 54, 2

	79	x ε n & 1 ε n & next(x) ε n
		Join, 78, 77

	80	(x,1,next(x)) ε n3
		Detach, 75, 79

		Prove: ALL(d):[d ε s => (x,1,next(x)) ε d]
		
		Suppose...

		81	t ε s
			Premise

		Apply definition of s

		82	t ε s <=> t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
			U Spec, 26

		83	[t ε s => t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]]
			& [t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]] => t ε s]
			Iff-And, 82

		84	t ε s => t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
			Split, 83

		85	t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]] => t ε s
			Split, 83

		86	t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
			Detach, 84, 81

		87	t ε pn3
			Split, 86

		88	ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]
			Split, 86

		89	ALL(b):[b ε n => (b,1,next(b)) ε t]
			Split, 88

		90	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]
			Split, 88

		91	x ε n => (x,1,next(x)) ε t
			U Spec, 89

		92	(x,1,next(x)) ε t
			Detach, 91, 54

	As Required:

	93	ALL(d):[d ε s => (x,1,next(x)) ε d]
		Conclusion, 81

	94	(x,1,next(x)) ε n3
		& ALL(d):[d ε s => (x,1,next(x)) ε d]
		Join, 80, 93

	95	(x,1,next(x)) ε add
		Detach, 69, 94

	96	next(x) ε n & (x,1,next(x)) ε add
		Join, 77, 95

	97	EXIST(c):[c ε n & (x,1,c) ε add]
		E Gen, 96

	98	1 ε n & EXIST(c):[c ε n & (x,1,c) ε add]
		Join, 2, 97

	99	1 ε p
		Detach, 63, 98

		
		Prove: ALL(b):[b ε n & b ε p => next(b) ε p]
		
		Suppose...

		100	y ε n & y ε p
			Premise

		101	y ε n
			Split, 100

		102	y ε p
			Split, 100

		Apply definition of p

		103	y ε p <=> y ε n & EXIST(c):[c ε n & (x,y,c) ε add]
			U Spec, 58

		104	[y ε p => y ε n & EXIST(c):[c ε n & (x,y,c) ε add]]
			& [y ε n & EXIST(c):[c ε n & (x,y,c) ε add] => y ε p]
			Iff-And, 103

		105	y ε p => y ε n & EXIST(c):[c ε n & (x,y,c) ε add]
			Split, 104

		106	y ε n & EXIST(c):[c ε n & (x,y,c) ε add] => y ε p
			Split, 104

		107	y ε n & EXIST(c):[c ε n & (x,y,c) ε add]
			Detach, 105, 102

		108	y ε n
			Split, 107

		109	EXIST(c):[c ε n & (x,y,c) ε add]
			Split, 107

		110	z ε n & (x,y,z) ε add
			E Spec, 109

		Define: z

		111	z ε n
			Split, 110

		112	(x,y,z) ε add
			Split, 110

		Apply definition of p

		113	next(y) ε p <=> next(y) ε n & EXIST(c):[c ε n & (x,next(y),c) ε add]
			U Spec, 58

		114	[next(y) ε p => next(y) ε n & EXIST(c):[c ε n & (x,next(y),c) ε add]]
			& [next(y) ε n & EXIST(c):[c ε n & (x,next(y),c) ε add] => next(y) ε p]
			Iff-And, 113

		115	next(y) ε p => next(y) ε n & EXIST(c):[c ε n & (x,next(y),c) ε add]
			Split, 114

		Sufficient: For next(y) ε p

		116	next(y) ε n & EXIST(c):[c ε n & (x,next(y),c) ε add] => next(y) ε p
			Split, 114

		Apply axiom

		117	y ε n => next(y) ε n
			U Spec, 3

		118	next(y) ε n
			Detach, 117, 101

		Apply definition of add

		119	ALL(b):ALL(c):[(x,b,c) ε add
			<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
			U Spec, 30

		120	ALL(c):[(x,next(y),c) ε add
			<=> (x,next(y),c) ε n3 & ALL(d):[d ε s => (x,next(y),c) ε d]]
			U Spec, 119

		121	(x,next(y),next(z)) ε add
			<=> (x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d]
			U Spec, 120

		122	[(x,next(y),next(z)) ε add => (x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d]]
			& [(x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d] => (x,next(y),next(z)) ε add]
			Iff-And, 121

		123	(x,next(y),next(z)) ε add => (x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d]
			Split, 122

		Sufficient: For (x,next(y),next(z)) ε add

		124	(x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d] => (x,next(y),next(z)) ε add
			Split, 122

		Apply definition of n3

		125	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
			U Spec, 16

		126	ALL(c3):[(x,next(y),c3) ε n3 <=> x ε n & next(y) ε n & c3 ε n]
			U Spec, 125

		127	(x,next(y),next(z)) ε n3 <=> x ε n & next(y) ε n & next(z) ε n
			U Spec, 126

		128	[(x,next(y),next(z)) ε n3 => x ε n & next(y) ε n & next(z) ε n]
			& [x ε n & next(y) ε n & next(z) ε n => (x,next(y),next(z)) ε n3]
			Iff-And, 127

		129	(x,next(y),next(z)) ε n3 => x ε n & next(y) ε n & next(z) ε n
			Split, 128

		Sufficient: For (x,next(y),next(z)) ε n3

		130	x ε n & next(y) ε n & next(z) ε n => (x,next(y),next(z)) ε n3
			Split, 128

		Apply axiom

		131	z ε n => next(z) ε n
			U Spec, 3

		132	next(z) ε n
			Detach, 131, 111

		133	x ε n & next(y) ε n
			Join, 54, 118

		134	x ε n & next(y) ε n & next(z) ε n
			Join, 133, 132

		135	(x,next(y),next(z)) ε n3
			Detach, 130, 134

			
			Prove: ALL(d):[d ε s => (x,next(y),next(z)) ε d]
			
			Suppose...

			136	t ε s
				Premise

			Apply definition of s

			137	t ε s <=> t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
				U Spec, 26

			138	[t ε s => t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]]
				& [t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]] => t ε s]
				Iff-And, 137

			139	t ε s => t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
				Split, 138

			140	t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]] => t ε s
				Split, 138

			141	t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
				Detach, 139, 136

			142	t ε pn3
				Split, 141

			143	ALL(b):[b ε n => (b,1,next(b)) ε t]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]
				Split, 141

			144	ALL(b):[b ε n => (b,1,next(b)) ε t]
				Split, 143

			145	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]
				Split, 143

			146	ALL(c):ALL(d):[x ε n & c ε n & d ε n => [(x,c,d) ε t => (x,next(c),next(d)) ε t]]
				U Spec, 145

			147	ALL(d):[x ε n & y ε n & d ε n => [(x,y,d) ε t => (x,next(y),next(d)) ε t]]
				U Spec, 146

			148	x ε n & y ε n & z ε n => [(x,y,z) ε t => (x,next(y),next(z)) ε t]
				U Spec, 147

			149	x ε n & y ε n
				Join, 54, 101

			150	x ε n & y ε n & z ε n
				Join, 149, 111

			151	(x,y,z) ε t => (x,next(y),next(z)) ε t
				Detach, 148, 150

			Apply definition of add

			152	ALL(b):ALL(c):[(x,b,c) ε add
				<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
				U Spec, 30

			153	ALL(c):[(x,y,c) ε add
				<=> (x,y,c) ε n3 & ALL(d):[d ε s => (x,y,c) ε d]]
				U Spec, 152

			154	(x,y,z) ε add
				<=> (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
				U Spec, 153

			155	[(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]]
				& [(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add]
				Iff-And, 154

			156	(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
				Split, 155

			157	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add
				Split, 155

			158	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
				Detach, 156, 112

			159	(x,y,z) ε n3
				Split, 158

			160	ALL(d):[d ε s => (x,y,z) ε d]
				Split, 158

			161	t ε s => (x,y,z) ε t
				U Spec, 160

			162	(x,y,z) ε t
				Detach, 161, 136

			163	(x,next(y),next(z)) ε t
				Detach, 151, 162

		As Required:

		164	ALL(d):[d ε s => (x,next(y),next(z)) ε d]
			Conclusion, 136

		165	(x,next(y),next(z)) ε n3
			& ALL(d):[d ε s => (x,next(y),next(z)) ε d]
			Join, 135, 164

		166	(x,next(y),next(z)) ε add
			Detach, 124, 165

		167	next(z) ε n & (x,next(y),next(z)) ε add
			Join, 132, 166

		168	EXIST(c):[c ε n & (x,next(y),c) ε add]
			E Gen, 167

		169	next(y) ε n
			& EXIST(c):[c ε n & (x,next(y),c) ε add]
			Join, 118, 168

		170	next(y) ε p
			Detach, 116, 169

	As Required:

	171	ALL(b):[b ε n & b ε p => next(b) ε p]
		Conclusion, 100

	172	Set(p) & 1 ε p
		Join, 57, 99

	173	Set(p) & 1 ε p
		& ALL(b):[b ε n & b ε p => next(b) ε p]
		Join, 172, 171

	174	ALL(b):[b ε n => b ε p]
		Detach, 59, 173

		Prove: ALL(b):[b ε n => EXIST(c):[c ε n & (x,b,c) ε add]]
		
		Suppose...

		175	y ε n
			Premise

		176	y ε n => y ε p
			U Spec, 174

		177	y ε p
			Detach, 176, 175

		Apply definition of p

		178	y ε p <=> y ε n & EXIST(c):[c ε n & (x,y,c) ε add]
			U Spec, 58

		179	[y ε p => y ε n & EXIST(c):[c ε n & (x,y,c) ε add]]
			& [y ε n & EXIST(c):[c ε n & (x,y,c) ε add] => y ε p]
			Iff-And, 178

		180	y ε p => y ε n & EXIST(c):[c ε n & (x,y,c) ε add]
			Split, 179

		181	y ε n & EXIST(c):[c ε n & (x,y,c) ε add] => y ε p
			Split, 179

		182	y ε n & EXIST(c):[c ε n & (x,y,c) ε add]
			Detach, 180, 177

		183	y ε n
			Split, 182

		184	EXIST(c):[c ε n & (x,y,c) ε add]
			Split, 182

	As Required:

	185	ALL(b):[b ε n => EXIST(c):[c ε n & (x,b,c) ε add]]
		Conclusion, 175

As Required:

186	ALL(a):[a ε n
	=> ALL(b):[b ε n => EXIST(c):[c ε n & (a,b,c) ε add]]]
	Conclusion, 54

	Prove: ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & (a,b,c) ε add]]
	
	Suppose...

	187	x ε n & y ε n
		Premise

	188	x ε n
		Split, 187

	189	y ε n
		Split, 187

	Apply previous result

	190	x ε n
		=> ALL(b):[b ε n => EXIST(c):[c ε n & (x,b,c) ε add]]
		U Spec, 186

	191	ALL(b):[b ε n => EXIST(c):[c ε n & (x,b,c) ε add]]
		Detach, 190, 188

	192	y ε n => EXIST(c):[c ε n & (x,y,c) ε add]
		U Spec, 191

	193	EXIST(c):[c ε n & (x,y,c) ε add]
		Detach, 192, 189

Functionality of add, Part 2

As Required:

194	ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & (a,b,c) ε add]]
	Conclusion, 187

Apply the Subset Axiom to construct the set p, which is to be used in conjunction 
with PMI (A6 above).

195	EXIST(sub):[Set(sub) & ALL(b):[b ε sub <=> b ε n & ALL(a):ALL(c1):ALL(c2):[(a,b,c1) ε add & (a,b,c2) ε add => c1=c2]]]
	Subset, 1

196	Set(p) & ALL(b):[b ε p <=> b ε n & ALL(a):ALL(c1):ALL(c2):[(a,b,c1) ε add & (a,b,c2) ε add => c1=c2]]
	E Spec, 195

Define: p

197	Set(p)
	Split, 196

198	ALL(b):[b ε p <=> b ε n & ALL(a):ALL(c1):ALL(c2):[(a,b,c1) ε add & (a,b,c2) ε add => c1=c2]]
	Split, 196

Sufficient: For Functionalilty of add, Part 3

Apply PMI axiom

199	Set(p) & 1 ε p & ALL(b):[b ε n & b ε p => next(b) ε p]
	=> ALL(b):[b ε n => b ε p]
	U Spec, 6

200	1 ε p <=> 1 ε n & ALL(a):ALL(c1):ALL(c2):[(a,1,c1) ε add & (a,1,c2) ε add => c1=c2]
	U Spec, 198

201	[1 ε p => 1 ε n & ALL(a):ALL(c1):ALL(c2):[(a,1,c1) ε add & (a,1,c2) ε add => c1=c2]]
	& [1 ε n & ALL(a):ALL(c1):ALL(c2):[(a,1,c1) ε add & (a,1,c2) ε add => c1=c2] => 1 ε p]
	Iff-And, 200

202	1 ε p => 1 ε n & ALL(a):ALL(c1):ALL(c2):[(a,1,c1) ε add & (a,1,c2) ε add => c1=c2]
	Split, 201

Sufficient: For 1 ε p

203	1 ε n & ALL(a):ALL(c1):ALL(c2):[(a,1,c1) ε add & (a,1,c2) ε add => c1=c2] => 1 ε p
	Split, 201

	
	Prove: ALL(a):ALL(b):~[(a,1,b) ε add & ~b=next(a)]
	
	Suppose to the contrary...

	204	(x,1,y) ε add & ~y=next(x)
		Premise

	205	(x,1,y) ε add
		Split, 204

	206	~y=next(x)
		Split, 204

	Apply definition of add

	207	ALL(b):ALL(c):[(x,b,c) ε add
		<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
		U Spec, 30

	208	ALL(c):[(x,1,c) ε add
		<=> (x,1,c) ε n3 & ALL(d):[d ε s => (x,1,c) ε d]]
		U Spec, 207

	209	(x,1,y) ε add
		<=> (x,1,y) ε n3 & ALL(d):[d ε s => (x,1,y) ε d]
		U Spec, 208

	210	[(x,1,y) ε add => (x,1,y) ε n3 & ALL(d):[d ε s => (x,1,y) ε d]]
		& [(x,1,y) ε n3 & ALL(d):[d ε s => (x,1,y) ε d] => (x,1,y) ε add]
		Iff-And, 209

	211	(x,1,y) ε add => (x,1,y) ε n3 & ALL(d):[d ε s => (x,1,y) ε d]
		Split, 210

	212	(x,1,y) ε n3 & ALL(d):[d ε s => (x,1,y) ε d] => (x,1,y) ε add
		Split, 210

	213	(x,1,y) ε n3 & ALL(d):[d ε s => (x,1,y) ε d]
		Detach, 211, 205

	214	(x,1,y) ε n3
		Split, 213

	215	ALL(d):[d ε s => (x,1,y) ε d]
		Split, 213

	Apply definition of n3

	216	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
		U Spec, 16

	217	ALL(c3):[(x,1,c3) ε n3 <=> x ε n & 1 ε n & c3 ε n]
		U Spec, 216

	218	(x,1,y) ε n3 <=> x ε n & 1 ε n & y ε n
		U Spec, 217

	219	[(x,1,y) ε n3 => x ε n & 1 ε n & y ε n]
		& [x ε n & 1 ε n & y ε n => (x,1,y) ε n3]
		Iff-And, 218

	220	(x,1,y) ε n3 => x ε n & 1 ε n & y ε n
		Split, 219

	221	x ε n & 1 ε n & y ε n => (x,1,y) ε n3
		Split, 219

	222	x ε n & 1 ε n & y ε n
		Detach, 220, 214

	223	x ε n
		Split, 222

	224	1 ε n
		Split, 222

	225	y ε n
		Split, 222

	226	~EXIST(d):~[d ε s => (x,1,y) ε d]
		Quant, 215

	227	~EXIST(d):~~[d ε s & ~(x,1,y) ε d]
		Imply-And, 226

	Obtain contradiction of the following by constructing add' 
	such that add' ε s & ~(x,1,y) ε add'

	228	~EXIST(d):[d ε s & ~(x,1,y) ε d]
		Rem DNeg, 227

	Apply Subset Axiom

	229	EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) ε sub
		<=> (a,b,c) ε add & ~[a=x & b=1 & c=y]]]
		Subset, 29

	230	Set''(add') & ALL(a):ALL(b):ALL(c):[(a,b,c) ε add'
		<=> (a,b,c) ε add & ~[a=x & b=1 & c=y]]
		E Spec, 229

	
	Define: add'

	231	Set''(add')
		Split, 230

	232	ALL(a):ALL(b):ALL(c):[(a,b,c) ε add'
		<=> (a,b,c) ε add & ~[a=x & b=1 & c=y]]
		Split, 230

	Apply definition of s

	233	add' ε s <=> add' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add']
		& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add' => (b,next(c),next(d)) ε add']]]
		U Spec, 26

	234	[add' ε s => add' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add']
		& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add' => (b,next(c),next(d)) ε add']]]]
		& [add' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add']
		& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add' => (b,next(c),next(d)) ε add']]] => add' ε s]
		Iff-And, 233

	235	add' ε s => add' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add']
		& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add' => (b,next(c),next(d)) ε add']]]
		Split, 234

	Sufficient: For add' ε s

	236	add' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add']
		& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add' => (b,next(c),next(d)) ε add']]] => add' ε s
		Split, 234

	Apply definition f pn3

	237	add' ε pn3 <=> Set''(add') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add' => (d1,d2,d3) ε n3]
		U Spec, 22

	238	[add' ε pn3 => Set''(add') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add' => (d1,d2,d3) ε n3]]
		& [Set''(add') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add' => (d1,d2,d3) ε n3] => add' ε pn3]
		Iff-And, 237

	239	add' ε pn3 => Set''(add') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add' => (d1,d2,d3) ε n3]
		Split, 238

	Sufficient: For add' ε pn3

	240	Set''(add') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add' => (d1,d2,d3) ε n3] => add' ε pn3
		Split, 238

		Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add' => (d1,d2,d3) ε n3]
		
		Suppose...

		241	(t,u,v) ε add'
			Premise

		Apply definition of add'

		242	ALL(b):ALL(c):[(t,b,c) ε add'
			<=> (t,b,c) ε add & ~[t=x & b=1 & c=y]]
			U Spec, 232

		243	ALL(c):[(t,u,c) ε add'
			<=> (t,u,c) ε add & ~[t=x & u=1 & c=y]]
			U Spec, 242

		244	(t,u,v) ε add'
			<=> (t,u,v) ε add & ~[t=x & u=1 & v=y]
			U Spec, 243

		245	[(t,u,v) ε add' => (t,u,v) ε add & ~[t=x & u=1 & v=y]]
			& [(t,u,v) ε add & ~[t=x & u=1 & v=y] => (t,u,v) ε add']
			Iff-And, 244

		246	(t,u,v) ε add' => (t,u,v) ε add & ~[t=x & u=1 & v=y]
			Split, 245

		247	(t,u,v) ε add & ~[t=x & u=1 & v=y] => (t,u,v) ε add'
			Split, 245

		248	(t,u,v) ε add & ~[t=x & u=1 & v=y]
			Detach, 246, 241

		249	(t,u,v) ε add
			Split, 248

		250	~[t=x & u=1 & v=y]
			Split, 248

		Apply definition of add

		251	ALL(b):ALL(c):[(t,b,c) ε add
			<=> (t,b,c) ε n3 & ALL(d):[d ε s => (t,b,c) ε d]]
			U Spec, 30

		252	ALL(c):[(t,u,c) ε add
			<=> (t,u,c) ε n3 & ALL(d):[d ε s => (t,u,c) ε d]]
			U Spec, 251

		253	(t,u,v) ε add
			<=> (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
			U Spec, 252

		254	[(t,u,v) ε add => (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]]
			& [(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d] => (t,u,v) ε add]
			Iff-And, 253

		255	(t,u,v) ε add => (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
			Split, 254

		256	(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d] => (t,u,v) ε add
			Split, 254

		257	(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
			Detach, 255, 249

		258	(t,u,v) ε n3
			Split, 257

	As Required:

	259	ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add' => (d1,d2,d3) ε n3]
		Conclusion, 241

	260	Set''(add')
		& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add' => (d1,d2,d3) ε n3]
		Join, 231, 259

	261	add' ε pn3
		Detach, 240, 260

		Prove: ALL(b):[b ε n => (b,1,next(b)) ε add']
		
		Suppose...

		262	t ε n
			Premise

		Apply definition of add'

		263	ALL(b):ALL(c):[(t,b,c) ε add'
			<=> (t,b,c) ε add & ~[t=x & b=1 & c=y]]
			U Spec, 232

		264	ALL(c):[(t,1,c) ε add'
			<=> (t,1,c) ε add & ~[t=x & 1=1 & c=y]]
			U Spec, 263

		265	(t,1,next(t)) ε add'
			<=> (t,1,next(t)) ε add & ~[t=x & 1=1 & next(t)=y]
			U Spec, 264

		266	[(t,1,next(t)) ε add' => (t,1,next(t)) ε add & ~[t=x & 1=1 & next(t)=y]]
			& [(t,1,next(t)) ε add & ~[t=x & 1=1 & next(t)=y] => (t,1,next(t)) ε add']
			Iff-And, 265

		267	(t,1,next(t)) ε add' => (t,1,next(t)) ε add & ~[t=x & 1=1 & next(t)=y]
			Split, 266

		Sufficient: For (t,1,next(t)) ε add'
		
		(Suppose to the contrary: t=x & 1=1 & next(t)=y. Would contradict line 206.)

		268	(t,1,next(t)) ε add & ~[t=x & 1=1 & next(t)=y] => (t,1,next(t)) ε add'
			Split, 266

		Apply definition of add

		269	ALL(b):ALL(c):[(t,b,c) ε add
			<=> (t,b,c) ε n3 & ALL(d):[d ε s => (t,b,c) ε d]]
			U Spec, 30

		270	ALL(c):[(t,1,c) ε add
			<=> (t,1,c) ε n3 & ALL(d):[d ε s => (t,1,c) ε d]]
			U Spec, 269

		271	(t,1,next(t)) ε add
			<=> (t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d]
			U Spec, 270

		272	[(t,1,next(t)) ε add => (t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d]]
			& [(t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d] => (t,1,next(t)) ε add]
			Iff-And, 271

		273	(t,1,next(t)) ε add => (t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d]
			Split, 272

		Sufficient: For (t,1,next(t)) ε add

		274	(t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d] => (t,1,next(t)) ε add
			Split, 272

		275	ALL(c2):ALL(c3):[(t,c2,c3) ε n3 <=> t ε n & c2 ε n & c3 ε n]
			U Spec, 16

		276	ALL(c3):[(t,1,c3) ε n3 <=> t ε n & 1 ε n & c3 ε n]
			U Spec, 275

		277	(t,1,next(t)) ε n3 <=> t ε n & 1 ε n & next(t) ε n
			U Spec, 276

		278	[(t,1,next(t)) ε n3 => t ε n & 1 ε n & next(t) ε n]
			& [t ε n & 1 ε n & next(t) ε n => (t,1,next(t)) ε n3]
			Iff-And, 277

		279	(t,1,next(t)) ε n3 => t ε n & 1 ε n & next(t) ε n
			Split, 278

		280	t ε n & 1 ε n & next(t) ε n => (t,1,next(t)) ε n3
			Split, 278

		281	t ε n => next(t) ε n
			U Spec, 3

		282	next(t) ε n
			Detach, 281, 262

		283	t ε n & 1 ε n
			Join, 262, 2

		284	t ε n & 1 ε n & next(t) ε n
			Join, 283, 282

		285	(t,1,next(t)) ε n3
			Detach, 280, 284

			Prove: ALL(d):[d ε s => (t,1,next(t)) ε d]
			
			Suppose...

			286	w ε s
				Premise

			Apply definition of s

			287	w ε s <=> w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]
				U Spec, 26

			288	[w ε s => w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]]
				& [w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]] => w ε s]
				Iff-And, 287

			289	w ε s => w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]
				Split, 288

			290	w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]] => w ε s
				Split, 288

			291	w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]
				Detach, 289, 286

			292	w ε pn3
				Split, 291

			293	ALL(b):[b ε n => (b,1,next(b)) ε w]
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]
				Split, 291

			294	ALL(b):[b ε n => (b,1,next(b)) ε w]
				Split, 293

			295	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]
				Split, 293

			296	t ε n => (t,1,next(t)) ε w
				U Spec, 294

			297	(t,1,next(t)) ε w
				Detach, 296, 262

		As Required:

		298	ALL(d):[d ε s => (t,1,next(t)) ε d]
			Conclusion, 286

		299	(t,1,next(t)) ε n3
			& ALL(d):[d ε s => (t,1,next(t)) ε d]
			Join, 285, 298

		300	(t,1,next(t)) ε add
			Detach, 274, 299

			Prove: ~[t=x & 1=1 & next(t)=y]
			
			Suppose to the contrary...

			301	t=x & 1=1 & next(t)=y
				Premise

			302	t=x
				Split, 301

			303	1=1
				Split, 301

			304	next(t)=y
				Split, 301

			305	next(x)=y
				Substitute, 302, 304

			306	y=next(x)
				Sym, 305

			307	y=next(x) & ~y=next(x)
				Join, 306, 206

		As Required:

		308	~[t=x & 1=1 & next(t)=y]
			Conclusion, 301

		309	(t,1,next(t)) ε add & ~[t=x & 1=1 & next(t)=y]
			Join, 300, 308

		310	(t,1,next(t)) ε add'
			Detach, 268, 309

	As Required:

	311	ALL(b):[b ε n => (b,1,next(b)) ε add']
		Conclusion, 262

		Prove: 
		ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n
		=> [(b,c,d) ε add' => (b,next(c),next(d)) ε add']]
		
		Suppose...

		312	t ε n & u ε n & v ε n
			Premise

		313	t ε n
			Split, 312

		314	u ε n
			Split, 312

		315	v ε n
			Split, 312

			Prove: (t,u,v) ε add' => (t,next(u),next(v)) ε add'
			
			Suppose...

			316	(t,u,v) ε add'
				Premise

			Apply definition of add'

			317	ALL(b):ALL(c):[(t,b,c) ε add'
				<=> (t,b,c) ε add & ~[t=x & b=1 & c=y]]
				U Spec, 232

			318	ALL(c):[(t,u,c) ε add'
				<=> (t,u,c) ε add & ~[t=x & u=1 & c=y]]
				U Spec, 317

			319	(t,u,v) ε add'
				<=> (t,u,v) ε add & ~[t=x & u=1 & v=y]
				U Spec, 318

			320	[(t,u,v) ε add' => (t,u,v) ε add & ~[t=x & u=1 & v=y]]
				& [(t,u,v) ε add & ~[t=x & u=1 & v=y] => (t,u,v) ε add']
				Iff-And, 319

			321	(t,u,v) ε add' => (t,u,v) ε add & ~[t=x & u=1 & v=y]
				Split, 320

			322	(t,u,v) ε add & ~[t=x & u=1 & v=y] => (t,u,v) ε add'
				Split, 320

			323	(t,u,v) ε add & ~[t=x & u=1 & v=y]
				Detach, 321, 316

			324	(t,u,v) ε add
				Split, 323

			325	~[t=x & u=1 & v=y]
				Split, 323

			326	ALL(b):ALL(c):[(t,b,c) ε add'
				<=> (t,b,c) ε add & ~[t=x & b=1 & c=y]]
				U Spec, 232

			327	ALL(c):[(t,next(u),c) ε add'
				<=> (t,next(u),c) ε add & ~[t=x & next(u)=1 & c=y]]
				U Spec, 326

			328	(t,next(u),next(v)) ε add'
				<=> (t,next(u),next(v)) ε add & ~[t=x & next(u)=1 & next(v)=y]
				U Spec, 327

			329	[(t,next(u),next(v)) ε add' => (t,next(u),next(v)) ε add & ~[t=x & next(u)=1 & next(v)=y]]
				& [(t,next(u),next(v)) ε add & ~[t=x & next(u)=1 & next(v)=y] => (t,next(u),next(v)) ε add']
				Iff-And, 328

			330	(t,next(u),next(v)) ε add' => (t,next(u),next(v)) ε add & ~[t=x & next(u)=1 & next(v)=y]
				Split, 329

			Sufficient: For (t,next(u),next(v)) ε add'

			331	(t,next(u),next(v)) ε add & ~[t=x & next(u)=1 & next(v)=y] => (t,next(u),next(v)) ε add'
				Split, 329

			332	ALL(b):ALL(c):[(t,b,c) ε add
				<=> (t,b,c) ε n3 & ALL(d):[d ε s => (t,b,c) ε d]]
				U Spec, 30

			333	ALL(c):[(t,next(u),c) ε add
				<=> (t,next(u),c) ε n3 & ALL(d):[d ε s => (t,next(u),c) ε d]]
				U Spec, 332

			334	(t,next(u),next(v)) ε add
				<=> (t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d]
				U Spec, 333

			335	[(t,next(u),next(v)) ε add => (t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d]]
				& [(t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d] => (t,next(u),next(v)) ε add]
				Iff-And, 334

			336	(t,next(u),next(v)) ε add => (t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d]
				Split, 335

			Sufficient: For (t,next(u),next(v)) ε add

			337	(t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d] => (t,next(u),next(v)) ε add
				Split, 335

			Apply definition of n3

			338	ALL(c2):ALL(c3):[(t,c2,c3) ε n3 <=> t ε n & c2 ε n & c3 ε n]
				U Spec, 16

			339	ALL(c3):[(t,next(u),c3) ε n3 <=> t ε n & next(u) ε n & c3 ε n]
				U Spec, 338

			340	(t,next(u),next(v)) ε n3 <=> t ε n & next(u) ε n & next(v) ε n
				U Spec, 339

			341	[(t,next(u),next(v)) ε n3 => t ε n & next(u) ε n & next(v) ε n]
				& [t ε n & next(u) ε n & next(v) ε n => (t,next(u),next(v)) ε n3]
				Iff-And, 340

			342	(t,next(u),next(v)) ε n3 => t ε n & next(u) ε n & next(v) ε n
				Split, 341

			343	t ε n & next(u) ε n & next(v) ε n => (t,next(u),next(v)) ε n3
				Split, 341

			344	u ε n => next(u) ε n
				U Spec, 3

			345	next(u) ε n
				Detach, 344, 314

			346	v ε n => next(v) ε n
				U Spec, 3

			347	next(v) ε n
				Detach, 346, 315

			348	t ε n & next(u) ε n
				Join, 313, 345

			349	t ε n & next(u) ε n & next(v) ε n
				Join, 348, 347

			350	(t,next(u),next(v)) ε n3
				Detach, 343, 349

				Prove: ALL(d):[d ε s => (t,next(u),next(v)) ε d]
				
				Suppose...

				351	w ε s
					Premise

				Apply definition of s

				352	w ε s <=> w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
					& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]
					U Spec, 26

				353	[w ε s => w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
					& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]]
					& [w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
					& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]] => w ε s]
					Iff-And, 352

				354	w ε s => w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
					& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]
					Split, 353

				355	w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
					& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]] => w ε s
					Split, 353

				356	w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
					& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]
					Detach, 354, 351

				357	w ε pn3
					Split, 356

				358	ALL(b):[b ε n => (b,1,next(b)) ε w]
					& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]
					Split, 356

				359	ALL(b):[b ε n => (b,1,next(b)) ε w]
					Split, 358

				360	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]
					Split, 358

				361	ALL(c):ALL(d):[t ε n & c ε n & d ε n => [(t,c,d) ε w => (t,next(c),next(d)) ε w]]
					U Spec, 360

				362	ALL(d):[t ε n & u ε n & d ε n => [(t,u,d) ε w => (t,next(u),next(d)) ε w]]
					U Spec, 361

				363	t ε n & u ε n & v ε n => [(t,u,v) ε w => (t,next(u),next(v)) ε w]
					U Spec, 362

				364	(t,u,v) ε w => (t,next(u),next(v)) ε w
					Detach, 363, 312

				Apply definition of add

				365	ALL(b):ALL(c):[(t,b,c) ε add
					<=> (t,b,c) ε n3 & ALL(d):[d ε s => (t,b,c) ε d]]
					U Spec, 30

				366	ALL(c):[(t,u,c) ε add
					<=> (t,u,c) ε n3 & ALL(d):[d ε s => (t,u,c) ε d]]
					U Spec, 365

				367	(t,u,v) ε add
					<=> (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
					U Spec, 366

				368	[(t,u,v) ε add => (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]]
					& [(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d] => (t,u,v) ε add]
					Iff-And, 367

				369	(t,u,v) ε add => (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
					Split, 368

				370	(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d] => (t,u,v) ε add
					Split, 368

				371	(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
					Detach, 369, 324

				372	(t,u,v) ε n3
					Split, 371

				373	ALL(d):[d ε s => (t,u,v) ε d]
					Split, 371

				374	w ε s => (t,u,v) ε w
					U Spec, 373

				375	(t,u,v) ε w
					Detach, 374, 351

				376	(t,next(u),next(v)) ε w
					Detach, 364, 375

			As Required:

			377	ALL(d):[d ε s => (t,next(u),next(v)) ε d]
				Conclusion, 351

			378	(t,next(u),next(v)) ε n3
				& ALL(d):[d ε s => (t,next(u),next(v)) ε d]
				Join, 350, 377

			379	(t,next(u),next(v)) ε add
				Detach, 337, 378

				Prove: ~[t=x & next(u)=1 & next(v)=y]
				
				Suppose to contrary...

				380	t=x & next(u)=1 & next(v)=y
					Premise

				381	t=x
					Split, 380

				382	next(u)=1
					Split, 380

				383	next(v)=y
					Split, 380

				384	u ε n => ~next(u)=1
					U Spec, 4

				385	~next(u)=1
					Detach, 384, 314

				386	next(u)=1 & ~next(u)=1
					Join, 382, 385

			As Required:

			387	~[t=x & next(u)=1 & next(v)=y]
				Conclusion, 380

			388	(t,next(u),next(v)) ε add
				& ~[t=x & next(u)=1 & next(v)=y]
				Join, 379, 387

			389	(t,next(u),next(v)) ε add'
				Detach, 331, 388

		As Required:

		390	(t,u,v) ε add' => (t,next(u),next(v)) ε add'
			Conclusion, 316

	As Required:

	391	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n
		=> [(b,c,d) ε add' => (b,next(c),next(d)) ε add']]
		Conclusion, 312

	392	ALL(b):[b ε n => (b,1,next(b)) ε add']
		& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n
		=> [(b,c,d) ε add' => (b,next(c),next(d)) ε add']]
		Join, 311, 391

	393	add' ε pn3
		& [ALL(b):[b ε n => (b,1,next(b)) ε add']
		& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n
		=> [(b,c,d) ε add' => (b,next(c),next(d)) ε add']]]
		Join, 261, 392

	394	add' ε s
		Detach, 236, 393

	Apply definition of add'

	395	ALL(b):ALL(c):[(x,b,c) ε add'
		<=> (x,b,c) ε add & ~[x=x & b=1 & c=y]]
		U Spec, 232

	396	ALL(c):[(x,1,c) ε add'
		<=> (x,1,c) ε add & ~[x=x & 1=1 & c=y]]
		U Spec, 395

	397	(x,1,y) ε add'
		<=> (x,1,y) ε add & ~[x=x & 1=1 & y=y]
		U Spec, 396

	398	[(x,1,y) ε add' => (x,1,y) ε add & ~[x=x & 1=1 & y=y]]
		& [(x,1,y) ε add & ~[x=x & 1=1 & y=y] => (x,1,y) ε add']
		Iff-And, 397

	399	(x,1,y) ε add' => (x,1,y) ε add & ~[x=x & 1=1 & y=y]
		Split, 398

	400	(x,1,y) ε add & ~[x=x & 1=1 & y=y] => (x,1,y) ε add'
		Split, 398

	Sufficient: For ~(x,1,y) ε add'

	401	~[(x,1,y) ε add & ~[x=x & 1=1 & y=y]] => ~(x,1,y) ε add'
		Contra, 399

	402	~~[~(x,1,y) ε add | ~~[x=x & 1=1 & y=y]] => ~(x,1,y) ε add'
		DeMorgan, 401

	403	~(x,1,y) ε add | ~~[x=x & 1=1 & y=y] => ~(x,1,y) ε add'
		Rem DNeg, 402

	Sufficient: For ~(x,1,y) ε add'

	404	~(x,1,y) ε add | x=x & 1=1 & y=y => ~(x,1,y) ε add'
		Rem DNeg, 403

	405	x=x
		Reflex

	406	1=1
		Reflex

	407	y=y
		Reflex

	408	x=x & 1=1
		Join, 405, 406

	409	x=x & 1=1 & y=y
		Join, 408, 407

	410	~(x,1,y) ε add | x=x & 1=1 & y=y
		Arb Or, 409

	411	~(x,1,y) ε add'
		Detach, 404, 410

	412	add' ε s & ~(x,1,y) ε add'
		Join, 394, 411

	413	EXIST(d):[d ε s & ~(x,1,y) ε d]
		E Gen, 412

	414	EXIST(d):[d ε s & ~(x,1,y) ε d]
		& ~EXIST(d):[d ε s & ~(x,1,y) ε d]
		Join, 413, 228

As Required:

415	ALL(a):ALL(b):~[(a,1,b) ε add & ~b=next(a)]
	Conclusion, 204

416	ALL(a):ALL(b):~~[(a,1,b) ε add => ~~b=next(a)]
	Imply-And, 415

417	ALL(a):ALL(b):[(a,1,b) ε add => ~~b=next(a)]
	Rem DNeg, 416

418	ALL(a):ALL(b):[(a,1,b) ε add => b=next(a)]
	Rem DNeg, 417

	
	Prove: ALL(a):ALL(c1):ALL(c2):[(a,1,c1) ε add & (a,1,c2) ε add => c1=c2]
	
	Suppose...

	419	(x,1,y) ε add & (x,1,y') ε add
		Premise

	420	(x,1,y) ε add
		Split, 419

	421	(x,1,y') ε add
		Split, 419

	Apply previous result

	422	ALL(b):[(x,1,b) ε add => b=next(x)]
		U Spec, 418

	423	(x,1,y) ε add => y=next(x)
		U Spec, 422

	424	y=next(x)
		Detach, 423, 420

	425	(x,1,y') ε add => y'=next(x)
		U Spec, 422

	426	y'=next(x)
		Detach, 425, 421

	427	y=y'
		Substitute, 426, 424

As Required:

428	ALL(a):ALL(c1):ALL(c2):[(a,1,c1) ε add & (a,1,c2) ε add => c1=c2]
	Conclusion, 419

429	1 ε n
	& ALL(a):ALL(c1):ALL(c2):[(a,1,c1) ε add & (a,1,c2) ε add => c1=c2]
	Join, 2, 428

Base step
---------

As Required:

430	1 ε p
	Detach, 203, 429

	Inductive Step
	--------------
	
	Prove: ALL(b):[b ε n & b ε p => next(b) ε p]
	
	Suppose...

	431	y ε n & y ε p
		Premise

	432	y ε n
		Split, 431

	433	y ε p
		Split, 431

	Appy definition of p

	434	y ε p <=> y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]
		U Spec, 198

	435	[y ε p => y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]]
		& [y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2] => y ε p]
		Iff-And, 434

	436	y ε p => y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]
		Split, 435

	437	y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2] => y ε p
		Split, 435

	438	y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]
		Detach, 436, 433

	439	y ε n
		Split, 438

	440	ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]
		Split, 438

	441	[y ε p => y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]]
		& [y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2] => y ε p]
		Iff-And, 434

	442	y ε p => y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]
		Split, 441

	443	y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2] => y ε p
		Split, 441

	444	y ε n & ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]
		Detach, 442, 433

	445	y ε n
		Split, 444

	Since y ε p...

	446	ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]
		Split, 444

	Apply definition of p

	447	next(y) ε p <=> next(y) ε n & ALL(a):ALL(c1):ALL(c2):[(a,next(y),c1) ε add & (a,next(y),c2) ε add => c1=c2]
		U Spec, 198

	448	[next(y) ε p => next(y) ε n & ALL(a):ALL(c1):ALL(c2):[(a,next(y),c1) ε add & (a,next(y),c2) ε add => c1=c2]]
		& [next(y) ε n & ALL(a):ALL(c1):ALL(c2):[(a,next(y),c1) ε add & (a,next(y),c2) ε add => c1=c2] => next(y) ε p]
		Iff-And, 447

	449	next(y) ε p => next(y) ε n & ALL(a):ALL(c1):ALL(c2):[(a,next(y),c1) ε add & (a,next(y),c2) ε add => c1=c2]
		Split, 448

	Sufficient: For next(y) ε p

	450	next(y) ε n & ALL(a):ALL(c1):ALL(c2):[(a,next(y),c1) ε add & (a,next(y),c2) ε add => c1=c2] => next(y) ε p
		Split, 448

	451	y ε n => next(y) ε n
		U Spec, 3

	452	next(y) ε n
		Detach, 451, 432

		Prove: ALL(a):[a ε n => EXIST(c'):ALL(c):[(a,next(y),c) ε add => c=next(c')]]
		
		Suppose...

		453	x ε n
			Premise

		454	ALL(c1):ALL(c2):[(x,y,c1) ε add & (x,y,c2) ε add => c1=c2]
			U Spec, 446

		455	ALL(b):[x ε n & b ε n => EXIST(c):[c ε n & (x,b,c) ε add]]
			U Spec, 194

		456	x ε n & y ε n => EXIST(c):[c ε n & (x,y,c) ε add]
			U Spec, 455

		457	x ε n & y ε n
			Join, 453, 432

		458	EXIST(c):[c ε n & (x,y,c) ε add]
			Detach, 456, 457

		459	z ε n & (x,y,z) ε add
			E Spec, 458

		Define: z

		460	z ε n
			Split, 459

		461	(x,y,z) ε add
			Split, 459

		Apply definition of add

		462	ALL(b):ALL(c):[(x,b,c) ε add
			<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
			U Spec, 30

		463	ALL(c):[(x,y,c) ε add
			<=> (x,y,c) ε n3 & ALL(d):[d ε s => (x,y,c) ε d]]
			U Spec, 462

		464	(x,y,z) ε add
			<=> (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
			U Spec, 463

		465	[(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]]
			& [(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add]
			Iff-And, 464

		466	(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
			Split, 465

		467	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add
			Split, 465

		468	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
			Detach, 466, 461

		469	(x,y,z) ε n3
			Split, 468

		470	ALL(d):[d ε s => (x,y,z) ε d]
			Split, 468

			Prove: ALL(c):~[(x,next(y),c) ε add & ~c=next(z)]
			
			Suppose to the contrary...

			471	(x,next(y),z') ε add & ~z'=next(z)
				Premise

			472	(x,next(y),z') ε add
				Split, 471

			473	~z'=next(z)
				Split, 471

			Apply definition of add

			474	ALL(b):ALL(c):[(x,b,c) ε add
				<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
				U Spec, 30

			475	ALL(c):[(x,next(y),c) ε add
				<=> (x,next(y),c) ε n3 & ALL(d):[d ε s => (x,next(y),c) ε d]]
				U Spec, 474

			476	(x,next(y),z') ε add
				<=> (x,next(y),z') ε n3 & ALL(d):[d ε s => (x,next(y),z') ε d]
				U Spec, 475

			477	[(x,next(y),z') ε add => (x,next(y),z') ε n3 & ALL(d):[d ε s => (x,next(y),z') ε d]]
				& [(x,next(y),z') ε n3 & ALL(d):[d ε s => (x,next(y),z') ε d] => (x,next(y),z') ε add]
				Iff-And, 476

			478	(x,next(y),z') ε add => (x,next(y),z') ε n3 & ALL(d):[d ε s => (x,next(y),z') ε d]
				Split, 477

			479	(x,next(y),z') ε n3 & ALL(d):[d ε s => (x,next(y),z') ε d] => (x,next(y),z') ε add
				Split, 477

			480	(x,next(y),z') ε n3 & ALL(d):[d ε s => (x,next(y),z') ε d]
				Detach, 478, 472

			481	(x,next(y),z') ε n3
				Split, 480

			482	ALL(d):[d ε s => (x,next(y),z') ε d]
				Split, 480

			Apply definiton of n3

			483	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
				U Spec, 16

			484	ALL(c3):[(x,next(y),c3) ε n3 <=> x ε n & next(y) ε n & c3 ε n]
				U Spec, 483

			485	(x,next(y),z') ε n3 <=> x ε n & next(y) ε n & z' ε n
				U Spec, 484

			486	[(x,next(y),z') ε n3 => x ε n & next(y) ε n & z' ε n]
				& [x ε n & next(y) ε n & z' ε n => (x,next(y),z') ε n3]
				Iff-And, 485

			487	(x,next(y),z') ε n3 => x ε n & next(y) ε n & z' ε n
				Split, 486

			488	x ε n & next(y) ε n & z' ε n => (x,next(y),z') ε n3
				Split, 486

			489	x ε n & next(y) ε n & z' ε n
				Detach, 487, 481

			490	x ε n
				Split, 489

			491	next(y) ε n
				Split, 489

			492	z' ε n
				Split, 489

			493	~EXIST(d):~[d ε s => (x,next(y),z') ε d]
				Quant, 482

			494	~EXIST(d):~~[d ε s & ~(x,next(y),z') ε d]
				Imply-And, 493

			Obtain contradiction of the following by constructing add'' 
			such that add'' ε s & ~(x,next(y),z') ε add''

			495	~EXIST(d):[d ε s & ~(x,next(y),z') ε d]
				Rem DNeg, 494

			Apply Subset Axiom

			496	EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) ε sub
				<=> (a,b,c) ε add & ~[a=x & b=next(y) & c=z']]]
				Subset, 29

			497	Set''(add'') & ALL(a):ALL(b):ALL(c):[(a,b,c) ε add''
				<=> (a,b,c) ε add & ~[a=x & b=next(y) & c=z']]
				E Spec, 496

			Define: add''

			498	Set''(add'')
				Split, 497

			499	ALL(a):ALL(b):ALL(c):[(a,b,c) ε add''
				<=> (a,b,c) ε add & ~[a=x & b=next(y) & c=z']]
				Split, 497

			Apply definition of s

			500	add'' ε s <=> add'' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add'']
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add'' => (b,next(c),next(d)) ε add'']]]
				U Spec, 26

			501	[add'' ε s => add'' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add'']
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add'' => (b,next(c),next(d)) ε add'']]]]
				& [add'' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add'']
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add'' => (b,next(c),next(d)) ε add'']]] => add'' ε s]
				Iff-And, 500

			502	add'' ε s => add'' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add'']
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add'' => (b,next(c),next(d)) ε add'']]]
				Split, 501

			Sufficient: For add'' ε s

			503	add'' ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε add'']
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε add'' => (b,next(c),next(d)) ε add'']]] => add'' ε s
				Split, 501

			Apply definition of pn3

			504	add'' ε pn3 <=> Set''(add'') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add'' => (d1,d2,d3) ε n3]
				U Spec, 22

			505	[add'' ε pn3 => Set''(add'') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add'' => (d1,d2,d3) ε n3]]
				& [Set''(add'') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add'' => (d1,d2,d3) ε n3] => add'' ε pn3]
				Iff-And, 504

			506	add'' ε pn3 => Set''(add'') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add'' => (d1,d2,d3) ε n3]
				Split, 505

			Sufficient: For add'' ε pn3

			507	Set''(add'') & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add'' => (d1,d2,d3) ε n3] => add'' ε pn3
				Split, 505

				Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add'' => (d1,d2,d3) ε n3]
				
				Suppose...

				508	(t,u,v) ε add''
					Premise

				Apply definition of add''

				509	ALL(b):ALL(c):[(t,b,c) ε add''
					<=> (t,b,c) ε add & ~[t=x & b=next(y) & c=z']]
					U Spec, 499

				510	ALL(c):[(t,u,c) ε add''
					<=> (t,u,c) ε add & ~[t=x & u=next(y) & c=z']]
					U Spec, 509

				511	(t,u,v) ε add''
					<=> (t,u,v) ε add & ~[t=x & u=next(y) & v=z']
					U Spec, 510

				512	[(t,u,v) ε add'' => (t,u,v) ε add & ~[t=x & u=next(y) & v=z']]
					& [(t,u,v) ε add & ~[t=x & u=next(y) & v=z'] => (t,u,v) ε add'']
					Iff-And, 511

				513	(t,u,v) ε add'' => (t,u,v) ε add & ~[t=x & u=next(y) & v=z']
					Split, 512

				514	(t,u,v) ε add & ~[t=x & u=next(y) & v=z'] => (t,u,v) ε add''
					Split, 512

				515	(t,u,v) ε add & ~[t=x & u=next(y) & v=z']
					Detach, 513, 508

				516	(t,u,v) ε add
					Split, 515

				517	~[t=x & u=next(y) & v=z']
					Split, 515

				Apply definition of add

				518	ALL(b):ALL(c):[(t,b,c) ε add
					<=> (t,b,c) ε n3 & ALL(d):[d ε s => (t,b,c) ε d]]
					U Spec, 30

				519	ALL(c):[(t,u,c) ε add
					<=> (t,u,c) ε n3 & ALL(d):[d ε s => (t,u,c) ε d]]
					U Spec, 518

				520	(t,u,v) ε add
					<=> (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
					U Spec, 519

				521	[(t,u,v) ε add => (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]]
					& [(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d] => (t,u,v) ε add]
					Iff-And, 520

				522	(t,u,v) ε add => (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
					Split, 521

				523	(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d] => (t,u,v) ε add
					Split, 521

				524	(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
					Detach, 522, 516

				525	(t,u,v) ε n3
					Split, 524

			As Required:

			526	ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add'' => (d1,d2,d3) ε n3]
				Conclusion, 508

			527	Set''(add'')
				& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) ε add'' => (d1,d2,d3) ε n3]
				Join, 498, 526

			528	add'' ε pn3
				Detach, 507, 527

				Prove: ALL(b):[b ε n => (b,1,next(b)) ε add'']
				
				Suppose...

				529	t ε n
					Premise

				Apply definition of add''

				530	ALL(b):ALL(c):[(t,b,c) ε add''
					<=> (t,b,c) ε add & ~[t=x & b=next(y) & c=z']]
					U Spec, 499

				531	ALL(c):[(t,1,c) ε add''
					<=> (t,1,c) ε add & ~[t=x & 1=next(y) & c=z']]
					U Spec, 530

				532	(t,1,next(t)) ε add''
					<=> (t,1,next(t)) ε add & ~[t=x & 1=next(y) & next(t)=z']
					U Spec, 531

				533	[(t,1,next(t)) ε add'' => (t,1,next(t)) ε add & ~[t=x & 1=next(y) & next(t)=z']]
					& [(t,1,next(t)) ε add & ~[t=x & 1=next(y) & next(t)=z'] => (t,1,next(t)) ε add'']
					Iff-And, 532

				534	(t,1,next(t)) ε add'' => (t,1,next(t)) ε add & ~[t=x & 1=next(y) & next(t)=z']
					Split, 533

				535	(t,1,next(t)) ε add & ~[t=x & 1=next(y) & next(t)=z'] => (t,1,next(t)) ε add''
					Split, 533

				536	(t,1,next(t)) ε add & ~[~[~t=x | ~1=next(y)] & next(t)=z'] => (t,1,next(t)) ε add''
					DeMorgan, 535

				537	(t,1,next(t)) ε add & ~~[~~[~t=x | ~1=next(y)] | ~next(t)=z'] => (t,1,next(t)) ε add''
					DeMorgan, 536

				538	(t,1,next(t)) ε add & [~~[~t=x | ~1=next(y)] | ~next(t)=z'] => (t,1,next(t)) ε add''
					Rem DNeg, 537

				Sufficient: For (t,1,next(t)) ε add''

				539	(t,1,next(t)) ε add & [~t=x | ~1=next(y) | ~next(t)=z'] => (t,1,next(t)) ε add''
					Rem DNeg, 538

				Apply definition of add

				540	ALL(b):ALL(c):[(t,b,c) ε add
					<=> (t,b,c) ε n3 & ALL(d):[d ε s => (t,b,c) ε d]]
					U Spec, 30

				541	ALL(c):[(t,1,c) ε add
					<=> (t,1,c) ε n3 & ALL(d):[d ε s => (t,1,c) ε d]]
					U Spec, 540

				542	(t,1,next(t)) ε add
					<=> (t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d]
					U Spec, 541

				543	[(t,1,next(t)) ε add => (t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d]]
					& [(t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d] => (t,1,next(t)) ε add]
					Iff-And, 542

				544	(t,1,next(t)) ε add => (t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d]
					Split, 543

				Sufficient: (t,1,next(t)) ε add

				545	(t,1,next(t)) ε n3 & ALL(d):[d ε s => (t,1,next(t)) ε d] => (t,1,next(t)) ε add
					Split, 543

				Apply definition of n3

				546	ALL(c2):ALL(c3):[(t,c2,c3) ε n3 <=> t ε n & c2 ε n & c3 ε n]
					U Spec, 16

				547	ALL(c3):[(t,1,c3) ε n3 <=> t ε n & 1 ε n & c3 ε n]
					U Spec, 546

				548	(t,1,next(t)) ε n3 <=> t ε n & 1 ε n & next(t) ε n
					U Spec, 547

				549	[(t,1,next(t)) ε n3 => t ε n & 1 ε n & next(t) ε n]
					& [t ε n & 1 ε n & next(t) ε n => (t,1,next(t)) ε n3]
					Iff-And, 548

				550	(t,1,next(t)) ε n3 => t ε n & 1 ε n & next(t) ε n
					Split, 549

				Sufficient: (t,1,next(t)) ε n3

				551	t ε n & 1 ε n & next(t) ε n => (t,1,next(t)) ε n3
					Split, 549

				Apply Axiom

				552	t ε n => next(t) ε n
					U Spec, 3

				553	next(t) ε n
					Detach, 552, 529

				554	t ε n & 1 ε n
					Join, 529, 2

				555	t ε n & 1 ε n & next(t) ε n
					Join, 554, 553

				556	(t,1,next(t)) ε n3
					Detach, 551, 555

					Prove: ALL(d):[d ε s => (t,1,next(t)) ε d]
					
					Suppose...

					557	u ε s
						Premise

					Apply definition of s

					558	u ε s <=> u ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε u]
						& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε u => (b,next(c),next(d)) ε u]]]
						U Spec, 26

					559	[u ε s => u ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε u]
						& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε u => (b,next(c),next(d)) ε u]]]]
						& [u ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε u]
						& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε u => (b,next(c),next(d)) ε u]]] => u ε s]
						Iff-And, 558

					560	u ε s => u ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε u]
						& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε u => (b,next(c),next(d)) ε u]]]
						Split, 559

					561	u ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε u]
						& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε u => (b,next(c),next(d)) ε u]]] => u ε s
						Split, 559

					562	u ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε u]
						& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε u => (b,next(c),next(d)) ε u]]]
						Detach, 560, 557

					563	u ε pn3
						Split, 562

					564	ALL(b):[b ε n => (b,1,next(b)) ε u]
						& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε u => (b,next(c),next(d)) ε u]]
						Split, 562

					565	ALL(b):[b ε n => (b,1,next(b)) ε u]
						Split, 564

					566	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε u => (b,next(c),next(d)) ε u]]
						Split, 564

					567	t ε n => (t,1,next(t)) ε u
						U Spec, 565

					568	(t,1,next(t)) ε u
						Detach, 567, 529

				As Required:

				569	ALL(d):[d ε s => (t,1,next(t)) ε d]
					Conclusion, 557

				570	(t,1,next(t)) ε n3
					& ALL(d):[d ε s => (t,1,next(t)) ε d]
					Join, 556, 569

				571	(t,1,next(t)) ε add
					Detach, 545, 570

				572	y ε n => ~next(y)=1
					U Spec, 4

				573	~next(y)=1
					Detach, 572, 432

				574	~1=next(y)
					Sym, 573

				575	~t=x | ~1=next(y)
					Arb Or, 574

				576	~t=x | ~1=next(y) | ~next(t)=z'
					Arb Or, 575

				577	(t,1,next(t)) ε add
					& [~t=x | ~1=next(y) | ~next(t)=z']
					Join, 571, 576

				578	(t,1,next(t)) ε add''
					Detach, 539, 577

			As Required:

			579	ALL(b):[b ε n => (b,1,next(b)) ε add'']
				Conclusion, 529

				Prove: 
				ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n
				=> [(b,c,d) ε add'' => (b,next(c),next(d)) ε add'']]
				
				Suppose...

				580	t ε n & u ε n & v ε n
					Premise

				581	t ε n
					Split, 580

				582	u ε n
					Split, 580

				583	v ε n
					Split, 580

					Prove: (t,u,v) ε add'' => (t,next(u),next(v)) ε add''
					
					Suppose...

					584	(t,u,v) ε add''
						Premise

					Apply definition of add''

					585	ALL(b):ALL(c):[(t,b,c) ε add''
						<=> (t,b,c) ε add & ~[t=x & b=next(y) & c=z']]
						U Spec, 499

					586	ALL(c):[(t,u,c) ε add''
						<=> (t,u,c) ε add & ~[t=x & u=next(y) & c=z']]
						U Spec, 585

					587	(t,u,v) ε add''
						<=> (t,u,v) ε add & ~[t=x & u=next(y) & v=z']
						U Spec, 586

					588	[(t,u,v) ε add'' => (t,u,v) ε add & ~[t=x & u=next(y) & v=z']]
						& [(t,u,v) ε add & ~[t=x & u=next(y) & v=z'] => (t,u,v) ε add'']
						Iff-And, 587

					589	(t,u,v) ε add'' => (t,u,v) ε add & ~[t=x & u=next(y) & v=z']
						Split, 588

					590	(t,u,v) ε add & ~[t=x & u=next(y) & v=z'] => (t,u,v) ε add''
						Split, 588

					591	(t,u,v) ε add & ~[t=x & u=next(y) & v=z']
						Detach, 589, 584

					592	(t,u,v) ε add
						Split, 591

					593	~[t=x & u=next(y) & v=z']
						Split, 591

					Apply definition of add''

					594	ALL(b):ALL(c):[(t,b,c) ε add''
						<=> (t,b,c) ε add & ~[t=x & b=next(y) & c=z']]
						U Spec, 499

					595	ALL(c):[(t,next(u),c) ε add''
						<=> (t,next(u),c) ε add & ~[t=x & next(u)=next(y) & c=z']]
						U Spec, 594

					596	(t,next(u),next(v)) ε add''
						<=> (t,next(u),next(v)) ε add & ~[t=x & next(u)=next(y) & next(v)=z']
						U Spec, 595

					597	[(t,next(u),next(v)) ε add'' => (t,next(u),next(v)) ε add & ~[t=x & next(u)=next(y) & next(v)=z']]
						& [(t,next(u),next(v)) ε add & ~[t=x & next(u)=next(y) & next(v)=z'] => (t,next(u),next(v)) ε add'']
						Iff-And, 596

					598	(t,next(u),next(v)) ε add'' => (t,next(u),next(v)) ε add & ~[t=x & next(u)=next(y) & next(v)=z']
						Split, 597

					Sufficient: (t,next(u),next(v)) ε add''

					599	(t,next(u),next(v)) ε add & ~[t=x & next(u)=next(y) & next(v)=z'] => (t,next(u),next(v)) ε add''
						Split, 597

					Apply definition of add

					600	ALL(b):ALL(c):[(t,b,c) ε add
						<=> (t,b,c) ε n3 & ALL(d):[d ε s => (t,b,c) ε d]]
						U Spec, 30

					601	ALL(c):[(t,next(u),c) ε add
						<=> (t,next(u),c) ε n3 & ALL(d):[d ε s => (t,next(u),c) ε d]]
						U Spec, 600

					602	(t,next(u),next(v)) ε add
						<=> (t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d]
						U Spec, 601

					603	[(t,next(u),next(v)) ε add => (t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d]]
						& [(t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d] => (t,next(u),next(v)) ε add]
						Iff-And, 602

					604	(t,next(u),next(v)) ε add => (t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d]
						Split, 603

					Sufficient: (t,next(u),next(v)) ε add

					605	(t,next(u),next(v)) ε n3 & ALL(d):[d ε s => (t,next(u),next(v)) ε d] => (t,next(u),next(v)) ε add
						Split, 603

					Apply definition of n3

					606	ALL(c2):ALL(c3):[(t,c2,c3) ε n3 <=> t ε n & c2 ε n & c3 ε n]
						U Spec, 16

					607	ALL(c3):[(t,next(u),c3) ε n3 <=> t ε n & next(u) ε n & c3 ε n]
						U Spec, 606

					608	(t,next(u),next(v)) ε n3 <=> t ε n & next(u) ε n & next(v) ε n
						U Spec, 607

					609	[(t,next(u),next(v)) ε n3 => t ε n & next(u) ε n & next(v) ε n]
						& [t ε n & next(u) ε n & next(v) ε n => (t,next(u),next(v)) ε n3]
						Iff-And, 608

					610	(t,next(u),next(v)) ε n3 => t ε n & next(u) ε n & next(v) ε n
						Split, 609

					611	t ε n & next(u) ε n & next(v) ε n => (t,next(u),next(v)) ε n3
						Split, 609

					612	u ε n => next(u) ε n
						U Spec, 3

					613	next(u) ε n
						Detach, 612, 582

					614	v ε n => next(v) ε n
						U Spec, 3

					615	next(v) ε n
						Detach, 614, 583

					616	t ε n & next(u) ε n
						Join, 581, 613

					617	t ε n & next(u) ε n & next(v) ε n
						Join, 616, 615

					618	(t,next(u),next(v)) ε n3
						Detach, 611, 617

						Prove: ALL(d):[d ε s => (t,next(u),next(v)) ε d]
						
						Suppose...

						619	w ε s
							Premise

						Apply definition of s

						620	w ε s <=> w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
							& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]
							U Spec, 26

						621	[w ε s => w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
							& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]]
							& [w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
							& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]] => w ε s]
							Iff-And, 620

						622	w ε s => w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
							& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]
							Split, 621

						623	w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
							& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]] => w ε s
							Split, 621

						624	w ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε w]
							& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]]
							Detach, 622, 619

						625	w ε pn3
							Split, 624

						626	ALL(b):[b ε n => (b,1,next(b)) ε w]
							& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]
							Split, 624

						627	ALL(b):[b ε n => (b,1,next(b)) ε w]
							Split, 626

						628	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε w => (b,next(c),next(d)) ε w]]
							Split, 626

						629	ALL(c):ALL(d):[t ε n & c ε n & d ε n => [(t,c,d) ε w => (t,next(c),next(d)) ε w]]
							U Spec, 628

						630	ALL(d):[t ε n & u ε n & d ε n => [(t,u,d) ε w => (t,next(u),next(d)) ε w]]
							U Spec, 629

						631	t ε n & u ε n & v ε n => [(t,u,v) ε w => (t,next(u),next(v)) ε w]
							U Spec, 630

						632	(t,u,v) ε w => (t,next(u),next(v)) ε w
							Detach, 631, 580

						Apply definition of add

						633	ALL(b):ALL(c):[(t,b,c) ε add
							<=> (t,b,c) ε n3 & ALL(d):[d ε s => (t,b,c) ε d]]
							U Spec, 30

						634	ALL(c):[(t,u,c) ε add
							<=> (t,u,c) ε n3 & ALL(d):[d ε s => (t,u,c) ε d]]
							U Spec, 633

						635	(t,u,v) ε add
							<=> (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
							U Spec, 634

						636	[(t,u,v) ε add => (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]]
							& [(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d] => (t,u,v) ε add]
							Iff-And, 635

						637	(t,u,v) ε add => (t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
							Split, 636

						638	(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d] => (t,u,v) ε add
							Split, 636

						639	(t,u,v) ε n3 & ALL(d):[d ε s => (t,u,v) ε d]
							Detach, 637, 592

						640	(t,u,v) ε n3
							Split, 639

						641	ALL(d):[d ε s => (t,u,v) ε d]
							Split, 639

						642	w ε s => (t,u,v) ε w
							U Spec, 641

						643	(t,u,v) ε w
							Detach, 642, 619

						644	(t,next(u),next(v)) ε w
							Detach, 632, 643

					As Required:

					645	ALL(d):[d ε s => (t,next(u),next(v)) ε d]
						Conclusion, 619

					646	(t,next(u),next(v)) ε n3
						& ALL(d):[d ε s => (t,next(u),next(v)) ε d]
						Join, 618, 645

					647	(t,next(u),next(v)) ε add
						Detach, 605, 646

						Prove: ~[t=x & next(u)=next(y) & next(v)=z']
						
						Suppose to the contrary...

						648	t=x & next(u)=next(y) & next(v)=z'
							Premise

						649	t=x
							Split, 648

						650	next(u)=next(y)
							Split, 648

						651	next(v)=z'
							Split, 648

						652	ALL(b):[u ε n & b ε n & next(u)=next(b) => u=b]
							U Spec, 5

						653	u ε n & y ε n & next(u)=next(y) => u=y
							U Spec, 652

						654	u ε n & y ε n
							Join, 582, 432

						655	u ε n & y ε n & next(u)=next(y)
							Join, 654, 650

						656	u=y
							Detach, 653, 655

						657	(x,u,v) ε add
							Substitute, 649, 592

						658	(x,y,v) ε add
							Substitute, 656, 657

						659	ALL(c1):ALL(c2):[(x,y,c1) ε add & (x,y,c2) ε add => c1=c2]
							U Spec, 446

						660	ALL(c2):[(x,y,z) ε add & (x,y,c2) ε add => z=c2]
							U Spec, 659

						661	(x,y,z) ε add & (x,y,v) ε add => z=v
							U Spec, 660

						662	(x,y,z) ε add & (x,y,v) ε add
							Join, 461, 658

						663	z=v
							Detach, 661, 662

						664	next(z)=z'
							Substitute, 663, 651

						665	z'=next(z)
							Sym, 664

						666	z'=next(z) & ~z'=next(z)
							Join, 665, 473

					As Required:

					667	~[t=x & next(u)=next(y) & next(v)=z']
						Conclusion, 648

					668	(t,next(u),next(v)) ε add
						& ~[t=x & next(u)=next(y) & next(v)=z']
						Join, 647, 667

					669	(t,next(u),next(v)) ε add''
						Detach, 599, 668

				As Required:

				670	(t,u,v) ε add'' => (t,next(u),next(v)) ε add''
					Conclusion, 584

			As Required:

			671	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n
				=> [(b,c,d) ε add'' => (b,next(c),next(d)) ε add'']]
				Conclusion, 580

			672	ALL(b):[b ε n => (b,1,next(b)) ε add'']
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n
				=> [(b,c,d) ε add'' => (b,next(c),next(d)) ε add'']]
				Join, 579, 671

			673	add'' ε pn3
				& [ALL(b):[b ε n => (b,1,next(b)) ε add'']
				& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n
				=> [(b,c,d) ε add'' => (b,next(c),next(d)) ε add'']]]
				Join, 528, 672

			674	add'' ε s
				Detach, 503, 673

			Apply definition of add''

			675	ALL(b):ALL(c):[(x,b,c) ε add''
				<=> (x,b,c) ε add & ~[x=x & b=next(y) & c=z']]
				U Spec, 499

			676	ALL(c):[(x,next(y),c) ε add''
				<=> (x,next(y),c) ε add & ~[x=x & next(y)=next(y) & c=z']]
				U Spec, 675

			677	(x,next(y),z') ε add''
				<=> (x,next(y),z') ε add & ~[x=x & next(y)=next(y) & z'=z']
				U Spec, 676

			678	[(x,next(y),z') ε add'' => (x,next(y),z') ε add & ~[x=x & next(y)=next(y) & z'=z']]
				& [(x,next(y),z') ε add & ~[x=x & next(y)=next(y) & z'=z'] => (x,next(y),z') ε add'']
				Iff-And, 677

			679	(x,next(y),z') ε add'' => (x,next(y),z') ε add & ~[x=x & next(y)=next(y) & z'=z']
				Split, 678

			680	(x,next(y),z') ε add & ~[x=x & next(y)=next(y) & z'=z'] => (x,next(y),z') ε add''
				Split, 678

			681	~[(x,next(y),z') ε add & ~[x=x & next(y)=next(y) & z'=z']] => ~(x,next(y),z') ε add''
				Contra, 679

			682	~~[~(x,next(y),z') ε add | ~~[x=x & next(y)=next(y) & z'=z']] => ~(x,next(y),z') ε add''
				DeMorgan, 681

			683	~(x,next(y),z') ε add | ~~[x=x & next(y)=next(y) & z'=z'] => ~(x,next(y),z') ε add''
				Rem DNeg, 682

			Sufficient: ~(x,next(y),z') ε add''

			684	~(x,next(y),z') ε add | x=x & next(y)=next(y) & z'=z' => ~(x,next(y),z') ε add''
				Rem DNeg, 683

			685	x=x
				Reflex

			686	next(y)=next(y)
				Reflex

			687	z'=z'
				Reflex

			688	x=x & next(y)=next(y)
				Join, 685, 686

			689	x=x & next(y)=next(y) & z'=z'
				Join, 688, 687

			690	~(x,next(y),z') ε add | x=x & next(y)=next(y) & z'=z'
				Arb Or, 689

			691	~(x,next(y),z') ε add''
				Detach, 684, 690

			692	add'' ε s & ~(x,next(y),z') ε add''
				Join, 674, 691

			693	EXIST(d):[d ε s & ~(x,next(y),z') ε d]
				E Gen, 692

			694	EXIST(d):[d ε s & ~(x,next(y),z') ε d]
				& ~EXIST(d):[d ε s & ~(x,next(y),z') ε d]
				Join, 693, 495

		As Required:

		695	ALL(c):~[(x,next(y),c) ε add & ~c=next(z)]
			Conclusion, 471

		696	ALL(c):~~[(x,next(y),c) ε add => ~~c=next(z)]
			Imply-And, 695

		697	ALL(c):[(x,next(y),c) ε add => ~~c=next(z)]
			Rem DNeg, 696

		698	ALL(c):[(x,next(y),c) ε add => c=next(z)]
			Rem DNeg, 697

	As Required:

	699	ALL(a):[a ε n
		=> EXIST(c'):ALL(c):[(a,next(y),c) ε add => c=next(c')]]
		Conclusion, 453

		Prove: ALL(a):ALL(c1):ALL(c2):[(a,next(y),c1) ε add & (a,next(y),c2) ε add => c1=c2]
		
		Suppose...

		700	(x,next(y),z) ε add & (x,next(y),z') ε add
			Premise

		701	(x,next(y),z) ε add
			Split, 700

		702	(x,next(y),z') ε add
			Split, 700

		Apply definition of add

		703	ALL(b):ALL(c):[(x,b,c) ε add
			<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
			U Spec, 30

		704	ALL(c):[(x,next(y),c) ε add
			<=> (x,next(y),c) ε n3 & ALL(d):[d ε s => (x,next(y),c) ε d]]
			U Spec, 703

		705	(x,next(y),z) ε add
			<=> (x,next(y),z) ε n3 & ALL(d):[d ε s => (x,next(y),z) ε d]
			U Spec, 704

		706	[(x,next(y),z) ε add => (x,next(y),z) ε n3 & ALL(d):[d ε s => (x,next(y),z) ε d]]
			& [(x,next(y),z) ε n3 & ALL(d):[d ε s => (x,next(y),z) ε d] => (x,next(y),z) ε add]
			Iff-And, 705

		707	(x,next(y),z) ε add => (x,next(y),z) ε n3 & ALL(d):[d ε s => (x,next(y),z) ε d]
			Split, 706

		708	(x,next(y),z) ε n3 & ALL(d):[d ε s => (x,next(y),z) ε d] => (x,next(y),z) ε add
			Split, 706

		709	(x,next(y),z) ε n3 & ALL(d):[d ε s => (x,next(y),z) ε d]
			Detach, 707, 701

		710	(x,next(y),z) ε n3
			Split, 709

		711	ALL(d):[d ε s => (x,next(y),z) ε d]
			Split, 709

		Apply definition of n3

		712	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
			U Spec, 16

		713	ALL(c3):[(x,next(y),c3) ε n3 <=> x ε n & next(y) ε n & c3 ε n]
			U Spec, 712

		714	(x,next(y),z) ε n3 <=> x ε n & next(y) ε n & z ε n
			U Spec, 713

		715	[(x,next(y),z) ε n3 => x ε n & next(y) ε n & z ε n]
			& [x ε n & next(y) ε n & z ε n => (x,next(y),z) ε n3]
			Iff-And, 714

		716	(x,next(y),z) ε n3 => x ε n & next(y) ε n & z ε n
			Split, 715

		717	x ε n & next(y) ε n & z ε n => (x,next(y),z) ε n3
			Split, 715

		718	x ε n & next(y) ε n & z ε n
			Detach, 716, 710

		719	x ε n
			Split, 718

		720	next(y) ε n
			Split, 718

		721	z ε n
			Split, 718

		Apply previous result

		722	x ε n
			=> EXIST(c'):ALL(c):[(x,next(y),c) ε add => c=next(c')]
			U Spec, 699

		723	EXIST(c'):ALL(c):[(x,next(y),c) ε add => c=next(c')]
			Detach, 722, 719

		724	ALL(c):[(x,next(y),c) ε add => c=next(z'')]
			E Spec, 723

		725	(x,next(y),z) ε add => z=next(z'')
			U Spec, 724

		726	z=next(z'')
			Detach, 725, 701

		727	(x,next(y),z') ε add => z'=next(z'')
			U Spec, 724

		728	z'=next(z'')
			Detach, 727, 702

		729	z=z'
			Substitute, 728, 726

	As Required:

	730	ALL(a):ALL(c1):ALL(c2):[(a,next(y),c1) ε add & (a,next(y),c2) ε add => c1=c2]
		Conclusion, 700

	731	next(y) ε n
		& ALL(a):ALL(c1):ALL(c2):[(a,next(y),c1) ε add & (a,next(y),c2) ε add => c1=c2]
		Join, 452, 730

	732	next(y) ε p
		Detach, 450, 731

Inductive Step
--------------

As Required:

733	ALL(b):[b ε n & b ε p => next(b) ε p]
	Conclusion, 431

734	Set(p) & 1 ε p
	Join, 197, 430

735	Set(p) & 1 ε p
	& ALL(b):[b ε n & b ε p => next(b) ε p]
	Join, 734, 733

By induction...

736	ALL(b):[b ε n => b ε p]
	Detach, 199, 735

	Prove: ALL(b):[b ε n => ALL(a):ALL(c1):ALL(c2):[(a,b,c1) ε add & (a,b,c2) ε add => c1=c2]]
	
	Suppose...

	737	x ε n
		Premise

	738	x ε n => x ε p
		U Spec, 736

	739	x ε p
		Detach, 738, 737

	Apply definition of p

	740	x ε p <=> x ε n & ALL(a):ALL(c1):ALL(c2):[(a,x,c1) ε add & (a,x,c2) ε add => c1=c2]
		U Spec, 198

	741	[x ε p => x ε n & ALL(a):ALL(c1):ALL(c2):[(a,x,c1) ε add & (a,x,c2) ε add => c1=c2]]
		& [x ε n & ALL(a):ALL(c1):ALL(c2):[(a,x,c1) ε add & (a,x,c2) ε add => c1=c2] => x ε p]
		Iff-And, 740

	742	x ε p => x ε n & ALL(a):ALL(c1):ALL(c2):[(a,x,c1) ε add & (a,x,c2) ε add => c1=c2]
		Split, 741

	743	x ε n & ALL(a):ALL(c1):ALL(c2):[(a,x,c1) ε add & (a,x,c2) ε add => c1=c2] => x ε p
		Split, 741

	744	x ε n & ALL(a):ALL(c1):ALL(c2):[(a,x,c1) ε add & (a,x,c2) ε add => c1=c2]
		Detach, 742, 739

	745	x ε n
		Split, 744

	746	ALL(a):ALL(c1):ALL(c2):[(a,x,c1) ε add & (a,x,c2) ε add => c1=c2]
		Split, 744

As Required:

747	ALL(b):[b ε n
	=> ALL(a):ALL(c1):ALL(c2):[(a,b,c1) ε add & (a,b,c2) ε add => c1=c2]]
	Conclusion, 737

	Prove: ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) ε add & (c1,c2,d2) ε add => d1=d2]
	
	Suppose...

	748	(x,y,z) ε add & (x,y,z') ε add
		Premise

	749	(x,y,z) ε add
		Split, 748

	750	(x,y,z') ε add
		Split, 748

	Apply previous result

	751	y ε n
		=> ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]
		U Spec, 747

	Apply definition of add

	752	ALL(b):ALL(c):[(x,b,c) ε add
		<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
		U Spec, 30

	753	ALL(c):[(x,y,c) ε add
		<=> (x,y,c) ε n3 & ALL(d):[d ε s => (x,y,c) ε d]]
		U Spec, 752

	754	(x,y,z) ε add
		<=> (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
		U Spec, 753

	755	[(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]]
		& [(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add]
		Iff-And, 754

	756	(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
		Split, 755

	757	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add
		Split, 755

	758	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
		Detach, 756, 749

	759	(x,y,z) ε n3
		Split, 758

	760	ALL(d):[d ε s => (x,y,z) ε d]
		Split, 758

	Apply definition of n3

	761	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
		U Spec, 16

	762	ALL(c3):[(x,y,c3) ε n3 <=> x ε n & y ε n & c3 ε n]
		U Spec, 761

	763	(x,y,z) ε n3 <=> x ε n & y ε n & z ε n
		U Spec, 762

	764	[(x,y,z) ε n3 => x ε n & y ε n & z ε n]
		& [x ε n & y ε n & z ε n => (x,y,z) ε n3]
		Iff-And, 763

	765	(x,y,z) ε n3 => x ε n & y ε n & z ε n
		Split, 764

	766	x ε n & y ε n & z ε n => (x,y,z) ε n3
		Split, 764

	767	x ε n & y ε n & z ε n
		Detach, 765, 759

	768	x ε n
		Split, 767

	769	y ε n
		Split, 767

	770	z ε n
		Split, 767

	From previous result...

	771	ALL(a):ALL(c1):ALL(c2):[(a,y,c1) ε add & (a,y,c2) ε add => c1=c2]
		Detach, 751, 769

	772	ALL(c1):ALL(c2):[(x,y,c1) ε add & (x,y,c2) ε add => c1=c2]
		U Spec, 771

	773	ALL(c2):[(x,y,z) ε add & (x,y,c2) ε add => z=c2]
		U Spec, 772

	774	(x,y,z) ε add & (x,y,z') ε add => z=z'
		U Spec, 773

	775	z=z'
		Detach, 774, 748

Functionality of add, Part 3

As Required:

776	ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) ε add & (c1,c2,d2) ε add => d1=d2]
	Conclusion, 748

777	ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) ε add => c1 ε n & c2 ε n & d ε n]
	& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & (a,b,c) ε add]]
	Join, 53, 194

778	ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) ε add => c1 ε n & c2 ε n & d ε n]
	& ALL(a):ALL(b):[a ε n & b ε n => EXIST(c):[c ε n & (a,b,c) ε add]]
	& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) ε add & (c1,c2,d2) ε add => d1=d2]
	Join, 777, 776

As Required: add is a function

779	ALL(c1):ALL(c2):ALL(d):[d=add(c1,c2) <=> (c1,c2,d) ε add]
	Detach, 35, 778

	Prove: ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]
	
	Suppose...

	780	x ε n & y ε n
		Premise

	Apply functionality of add, part 2

	781	ALL(b):[x ε n & b ε n => EXIST(c):[c ε n & (x,b,c) ε add]]
		U Spec, 194

	782	x ε n & y ε n => EXIST(c):[c ε n & (x,y,c) ε add]
		U Spec, 781

	783	EXIST(c):[c ε n & (x,y,c) ε add]
		Detach, 782, 780

	784	z ε n & (x,y,z) ε add
		E Spec, 783

	785	z ε n
		Split, 784

	786	(x,y,z) ε add
		Split, 784

	Apply functionality of add

	787	ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) ε add]
		U Spec, 779

	788	ALL(d):[d=add(x,y) <=> (x,y,d) ε add]
		U Spec, 787

	789	z=add(x,y) <=> (x,y,z) ε add
		U Spec, 788

	790	[z=add(x,y) => (x,y,z) ε add]
		& [(x,y,z) ε add => z=add(x,y)]
		Iff-And, 789

	791	z=add(x,y) => (x,y,z) ε add
		Split, 790

	792	(x,y,z) ε add => z=add(x,y)
		Split, 790

	793	z=add(x,y)
		Detach, 792, 786

	794	add(x,y) ε n
		Substitute, 793, 785

As Required:

795	ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]
	Conclusion, 780

	Prove: ALL(a):[a ε n => add(a,1)=next(a)]
	
	Suppose...

	796	x ε n
		Premise

	Apply definition of add

	797	ALL(b):ALL(c):[(x,b,c) ε add
		<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
		U Spec, 30

	798	ALL(c):[(x,1,c) ε add
		<=> (x,1,c) ε n3 & ALL(d):[d ε s => (x,1,c) ε d]]
		U Spec, 797

	799	(x,1,next(x)) ε add
		<=> (x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d]
		U Spec, 798

	800	[(x,1,next(x)) ε add => (x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d]]
		& [(x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d] => (x,1,next(x)) ε add]
		Iff-And, 799

	801	(x,1,next(x)) ε add => (x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d]
		Split, 800

	Sufficient: (x,1,next(x)) ε add

	802	(x,1,next(x)) ε n3 & ALL(d):[d ε s => (x,1,next(x)) ε d] => (x,1,next(x)) ε add
		Split, 800

	Apply definition of n3

	803	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
		U Spec, 16

	804	ALL(c3):[(x,1,c3) ε n3 <=> x ε n & 1 ε n & c3 ε n]
		U Spec, 803

	805	(x,1,next(x)) ε n3 <=> x ε n & 1 ε n & next(x) ε n
		U Spec, 804

	806	[(x,1,next(x)) ε n3 => x ε n & 1 ε n & next(x) ε n]
		& [x ε n & 1 ε n & next(x) ε n => (x,1,next(x)) ε n3]
		Iff-And, 805

	807	(x,1,next(x)) ε n3 => x ε n & 1 ε n & next(x) ε n
		Split, 806

	Sufficient: (x,1,next(x)) ε n3

	808	x ε n & 1 ε n & next(x) ε n => (x,1,next(x)) ε n3
		Split, 806

	809	x ε n => next(x) ε n
		U Spec, 3

	810	next(x) ε n
		Detach, 809, 796

	811	x ε n & 1 ε n
		Join, 796, 2

	812	x ε n & 1 ε n & next(x) ε n
		Join, 811, 810

	813	(x,1,next(x)) ε n3
		Detach, 808, 812

		Prove: ALL(d):[d ε s => (x,1,next(x)) ε d]
		
		Suppose...

		814	t ε s
			Premise

		Apply definition of s

		815	t ε s <=> t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
			U Spec, 26

		816	[t ε s => t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]]
			& [t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]] => t ε s]
			Iff-And, 815

		817	t ε s => t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
			Split, 816

		818	t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]] => t ε s
			Split, 816

		819	t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
			Detach, 817, 814

		820	t ε pn3
			Split, 819

		821	ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]
			Split, 819

		822	ALL(b):[b ε n => (b,1,next(b)) ε t]
			Split, 821

		823	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]
			Split, 821

		824	x ε n => (x,1,next(x)) ε t
			U Spec, 822

		825	(x,1,next(x)) ε t
			Detach, 824, 796

	As Required:

	826	ALL(d):[d ε s => (x,1,next(x)) ε d]
		Conclusion, 814

	827	(x,1,next(x)) ε n3
		& ALL(d):[d ε s => (x,1,next(x)) ε d]
		Join, 813, 826

	828	(x,1,next(x)) ε add
		Detach, 802, 827

	Apply functionality of add

	829	ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) ε add]
		U Spec, 779

	830	ALL(d):[d=add(x,1) <=> (x,1,d) ε add]
		U Spec, 829

	831	next(x)=add(x,1) <=> (x,1,next(x)) ε add
		U Spec, 830

	832	[next(x)=add(x,1) => (x,1,next(x)) ε add]
		& [(x,1,next(x)) ε add => next(x)=add(x,1)]
		Iff-And, 831

	833	next(x)=add(x,1) => (x,1,next(x)) ε add
		Split, 832

	834	(x,1,next(x)) ε add => next(x)=add(x,1)
		Split, 832

	835	next(x)=add(x,1)
		Detach, 834, 828

	836	add(x,1)=next(x)
		Sym, 835

As Required:

837	ALL(a):[a ε n => add(a,1)=next(a)]
	Conclusion, 796

	Prove: ALL(a):ALL(b):[a ε n & b ε n => add(a,next(b))=next(add(a,b))]
	
	Suppose...

	838	x ε n & y ε n
		Premise

	839	x ε n
		Split, 838

	840	y ε n
		Split, 838

	841	ALL(b):[x ε n & b ε n => EXIST(c):[c ε n & (x,b,c) ε add]]
		U Spec, 194

	842	x ε n & y ε n => EXIST(c):[c ε n & (x,y,c) ε add]
		U Spec, 841

	843	EXIST(c):[c ε n & (x,y,c) ε add]
		Detach, 842, 838

	844	z ε n & (x,y,z) ε add
		E Spec, 843

	845	z ε n
		Split, 844

	846	(x,y,z) ε add
		Split, 844

	847	y ε n => next(y) ε n
		U Spec, 3

	848	next(y) ε n
		Detach, 847, 840

	849	z ε n => next(z) ε n
		U Spec, 3

	850	next(z) ε n
		Detach, 849, 845

	851	ALL(b):ALL(c):[(x,b,c) ε add
		<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
		U Spec, 30

	852	ALL(c):[(x,next(y),c) ε add
		<=> (x,next(y),c) ε n3 & ALL(d):[d ε s => (x,next(y),c) ε d]]
		U Spec, 851

	853	(x,next(y),next(z)) ε add
		<=> (x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d]
		U Spec, 852

	854	[(x,next(y),next(z)) ε add => (x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d]]
		& [(x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d] => (x,next(y),next(z)) ε add]
		Iff-And, 853

	855	(x,next(y),next(z)) ε add => (x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d]
		Split, 854

	Sufficient: (x,next(y),next(z)) ε add

	856	(x,next(y),next(z)) ε n3 & ALL(d):[d ε s => (x,next(y),next(z)) ε d] => (x,next(y),next(z)) ε add
		Split, 854

	857	ALL(c2):ALL(c3):[(x,c2,c3) ε n3 <=> x ε n & c2 ε n & c3 ε n]
		U Spec, 16

	858	ALL(c3):[(x,next(y),c3) ε n3 <=> x ε n & next(y) ε n & c3 ε n]
		U Spec, 857

	859	(x,next(y),next(z)) ε n3 <=> x ε n & next(y) ε n & next(z) ε n
		U Spec, 858

	860	[(x,next(y),next(z)) ε n3 => x ε n & next(y) ε n & next(z) ε n]
		& [x ε n & next(y) ε n & next(z) ε n => (x,next(y),next(z)) ε n3]
		Iff-And, 859

	861	(x,next(y),next(z)) ε n3 => x ε n & next(y) ε n & next(z) ε n
		Split, 860

	862	x ε n & next(y) ε n & next(z) ε n => (x,next(y),next(z)) ε n3
		Split, 860

	863	x ε n & next(y) ε n
		Join, 839, 848

	864	x ε n & next(y) ε n & next(z) ε n
		Join, 863, 850

	865	(x,next(y),next(z)) ε n3
		Detach, 862, 864

		Prove: ALL(d):[d ε s => (x,next(y),next(z)) ε d]
		
		Suppose...

		866	t ε s
			Premise

		867	t ε s <=> t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
			U Spec, 26

		868	[t ε s => t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]]
			& [t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]] => t ε s]
			Iff-And, 867

		869	t ε s => t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
			Split, 868

		870	t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]] => t ε s
			Split, 868

		871	t ε pn3 & [ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]]
			Detach, 869, 866

		872	t ε pn3
			Split, 871

		873	ALL(b):[b ε n => (b,1,next(b)) ε t]
			& ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]
			Split, 871

		874	ALL(b):[b ε n => (b,1,next(b)) ε t]
			Split, 873

		875	ALL(b):ALL(c):ALL(d):[b ε n & c ε n & d ε n => [(b,c,d) ε t => (b,next(c),next(d)) ε t]]
			Split, 873

		876	ALL(c):ALL(d):[x ε n & c ε n & d ε n => [(x,c,d) ε t => (x,next(c),next(d)) ε t]]
			U Spec, 875

		877	ALL(d):[x ε n & y ε n & d ε n => [(x,y,d) ε t => (x,next(y),next(d)) ε t]]
			U Spec, 876

		878	x ε n & y ε n & z ε n => [(x,y,z) ε t => (x,next(y),next(z)) ε t]
			U Spec, 877

		879	x ε n & y ε n & z ε n
			Join, 838, 845

		880	(x,y,z) ε t => (x,next(y),next(z)) ε t
			Detach, 878, 879

		881	ALL(b):ALL(c):[(x,b,c) ε add
			<=> (x,b,c) ε n3 & ALL(d):[d ε s => (x,b,c) ε d]]
			U Spec, 30

		882	ALL(c):[(x,y,c) ε add
			<=> (x,y,c) ε n3 & ALL(d):[d ε s => (x,y,c) ε d]]
			U Spec, 881

		883	(x,y,z) ε add
			<=> (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
			U Spec, 882

		884	[(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]]
			& [(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add]
			Iff-And, 883

		885	(x,y,z) ε add => (x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
			Split, 884

		886	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d] => (x,y,z) ε add
			Split, 884

		887	(x,y,z) ε n3 & ALL(d):[d ε s => (x,y,z) ε d]
			Detach, 885, 846

		888	(x,y,z) ε n3
			Split, 887

		889	ALL(d):[d ε s => (x,y,z) ε d]
			Split, 887

		890	t ε s => (x,y,z) ε t
			U Spec, 889

		891	(x,y,z) ε t
			Detach, 890, 866

		892	(x,next(y),next(z)) ε t
			Detach, 880, 891

	As Required:

	893	ALL(d):[d ε s => (x,next(y),next(z)) ε d]
		Conclusion, 866

	894	(x,next(y),next(z)) ε n3
		& ALL(d):[d ε s => (x,next(y),next(z)) ε d]
		Join, 865, 893

	895	(x,next(y),next(z)) ε add
		Detach, 856, 894

	Apply functionality of add

	896	ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) ε add]
		U Spec, 779

	897	ALL(d):[d=add(x,next(y)) <=> (x,next(y),d) ε add]
		U Spec, 896

	898	next(z)=add(x,next(y)) <=> (x,next(y),next(z)) ε add
		U Spec, 897

	899	[next(z)=add(x,next(y)) => (x,next(y),next(z)) ε add]
		& [(x,next(y),next(z)) ε add => next(z)=add(x,next(y))]
		Iff-And, 898

	900	next(z)=add(x,next(y)) => (x,next(y),next(z)) ε add
		Split, 899

	901	(x,next(y),next(z)) ε add => next(z)=add(x,next(y))
		Split, 899

	902	next(z)=add(x,next(y))
		Detach, 901, 895

	Apply functionality of add

	903	ALL(c2):ALL(d):[d=add(x,c2) <=> (x,c2,d) ε add]
		U Spec, 779

	904	ALL(d):[d=add(x,y) <=> (x,y,d) ε add]
		U Spec, 903

	905	z=add(x,y) <=> (x,y,z) ε add
		U Spec, 904

	906	[z=add(x,y) => (x,y,z) ε add]
		& [(x,y,z) ε add => z=add(x,y)]
		Iff-And, 905

	907	z=add(x,y) => (x,y,z) ε add
		Split, 906

	908	(x,y,z) ε add => z=add(x,y)
		Split, 906

	909	z=add(x,y)
		Detach, 908, 846

	910	next(add(x,y))=add(x,next(y))
		Substitute, 909, 902

	911	add(x,next(y))=next(add(x,y))
		Sym, 910

As Required:

912	ALL(a):ALL(b):[a ε n & b ε n => add(a,next(b))=next(add(a,b))]
	Conclusion, 838

913	ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]
	& ALL(a):[a ε n => add(a,1)=next(a)]
	Join, 795, 837

As Required:

914	ALL(a):ALL(b):[a ε n & b ε n => add(a,b) ε n]
	& ALL(a):[a ε n => add(a,1)=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => add(a,next(b))=next(add(a,b))]
	Join, 913, 912

Prove: The add function is unique

Suppose we have add' such that...

915	ALL(a):ALL(b):[a ε n & b ε n => add'(a,b) ε n]
	& ALL(a):[a ε n => add'(a,1)=next(a)]
	& ALL(a):ALL(b):[a ε n & b ε n => add'(a,next(b))=next(add'(a,b))]
	Premise

916	ALL(a):ALL(b):[a ε n & b ε n => add'(a,b) ε n]
	Split, 915

917	ALL(a):[a ε n => add'(a,1)=next(a)]
	Split, 915

918	ALL(a):ALL(b):[a ε n & b ε n => add'(a,next(b))=next(add'(a,b))]
	Split, 915

	Prove: ALL(a):[a ε n => ALL(b):[b ε n => add(a,b)=add'(a,b)]]
	
	Suppose...

	919	x ε n
		Premise

	Apply the Subset Axiom to construct the set q, which is to be used in conjunction 
	with PMI (A6 above).

	920	EXIST(sub):[Set(sub) & ALL(b):[b ε sub <=> b ε n & add(x,b)=add'(x,b)]]
		Subset, 1

	921	Set(q) & ALL(b):[b ε q <=> b ε n & add(x,b)=add'(x,b)]
		E Spec, 920

	Define: q

	922	Set(q)
		Split, 921

	923	ALL(b):[b ε q <=> b ε n & add(x,b)=add'(x,b)]
		Split, 921

	Apply PMI

	924	Set(q) & 1 ε q & ALL(b):[b ε n & b ε q => next(b) ε q]
		=> ALL(b):[b ε n => b ε q]
		U Spec, 6

	Apply definition of q

	925	1 ε q <=> 1 ε n & add(x,1)=add'(x,1)
		U Spec, 923

	926	[1 ε q => 1 ε n & add(x,1)=add'(x,1)]
		& [1 ε n & add(x,1)=add'(x,1) => 1 ε q]
		Iff-And, 925

	927	1 ε q => 1 ε n & add(x,1)=add'(x,1)
		Split, 926

	Sufficient: 1 ε q

	928	1 ε n & add(x,1)=add'(x,1) => 1 ε q
		Split, 926

	Apply definition of add

	929	x ε n => add(x,1)=next(x)
		U Spec, 837

	930	add(x,1)=next(x)
		Detach, 929, 919

	Apply definition of add'

	931	x ε n => add'(x,1)=next(x)
		U Spec, 917

	932	add'(x,1)=next(x)
		Detach, 931, 919

	933	add(x,1)=add'(x,1)
		Substitute, 932, 930

	934	1 ε n & add(x,1)=add'(x,1)
		Join, 2, 933

	Base Step
	---------
	
	As Required:

	935	1 ε q
		Detach, 928, 934

		Prove: ALL(b):[b ε n & b ε q => next(b) ε q]
		
		Suppose...

		936	y ε n & y ε q
			Premise

		937	y ε n
			Split, 936

		938	y ε q
			Split, 936

		Apply definition of q

		939	y ε q <=> y ε n & add(x,y)=add'(x,y)
			U Spec, 923

		940	[y ε q => y ε n & add(x,y)=add'(x,y)]
			& [y ε n & add(x,y)=add'(x,y) => y ε q]
			Iff-And, 939

		941	y ε q => y ε n & add(x,y)=add'(x,y)
			Split, 940

		942	y ε n & add(x,y)=add'(x,y) => y ε q
			Split, 940

		943	y ε n & add(x,y)=add'(x,y)
			Detach, 941, 938

		944	y ε n
			Split, 943

		945	add(x,y)=add'(x,y)
			Split, 943

		Apply definition of q

		946	next(y) ε q <=> next(y) ε n & add(x,next(y))=add'(x,next(y))
			U Spec, 923

		947	[next(y) ε q => next(y) ε n & add(x,next(y))=add'(x,next(y))]
			& [next(y) ε n & add(x,next(y))=add'(x,next(y)) => next(y) ε q]
			Iff-And, 946

		948	next(y) ε q => next(y) ε n & add(x,next(y))=add'(x,next(y))
			Split, 947

		Sufficient: next(y) ε q

		949	next(y) ε n & add(x,next(y))=add'(x,next(y)) => next(y) ε q
			Split, 947

		950	y ε n => next(y) ε n
			U Spec, 3

		951	next(y) ε n
			Detach, 950, 937

		Apply previous result

		952	ALL(b):[x ε n & b ε n => add(x,next(b))=next(add(x,b))]
			U Spec, 912

		953	x ε n & y ε n => add(x,next(y))=next(add(x,y))
			U Spec, 952

		954	x ε n & y ε n
			Join, 919, 937

		955	add(x,next(y))=next(add(x,y))
			Detach, 953, 954

		Apply previous result

		956	ALL(b):[x ε n & b ε n => add'(x,next(b))=next(add'(x,b))]
			U Spec, 918

		957	x ε n & y ε n => add'(x,next(y))=next(add'(x,y))
			U Spec, 956

		958	add'(x,next(y))=next(add'(x,y))
			Detach, 957, 954

		959	add'(x,next(y))=next(add(x,y))
			Substitute, 945, 958

		960	add(x,next(y))=add'(x,next(y))
			Substitute, 959, 955

		961	next(y) ε n & add(x,next(y))=add'(x,next(y))
			Join, 951, 960

		962	next(y) ε q
			Detach, 949, 961

	Inductive Step
	--------------
	
	As Required:

	963	ALL(b):[b ε n & b ε q => next(b) ε q]
		Conclusion, 936

	964	Set(q) & 1 ε q
		Join, 922, 935

	965	Set(q) & 1 ε q
		& ALL(b):[b ε n & b ε q => next(b) ε q]
		Join, 964, 963

	By induction...

	966	ALL(b):[b ε n => b ε q]
		Detach, 924, 965

		Prove: ALL(b):[b ε n => add(x,b)=add'(x,b)]
		
		Suppose...

		967	y ε n
			Premise

		968	y ε n => y ε q
			U Spec, 966

		969	y ε q
			Detach, 968, 967

		Apply definition of q

		970	y ε q <=> y ε n & add(x,y)=add'(x,y)
			U Spec, 923

		971	[y ε q => y ε n & add(x,y)=add'(x,y)]
			& [y ε n & add(x,y)=add'(x,y) => y ε q]
			Iff-And, 970

		972	y ε q => y ε n & add(x,y)=add'(x,y)
			Split, 971

		973	y ε n & add(x,y)=add'(x,y) => y ε q
			Split, 971

		974	y ε n & add(x,y)=add'(x,y)
			Detach, 972, 969

		975	y ε n
			Split, 974

		976	add(x,y)=add'(x,y)
			Split, 974

	977	ALL(b):[b ε n => add(x,b)=add'(x,b)]
		Conclusion, 967

As Required:

978	ALL(a):[a ε n => ALL(b):[b ε n => add(a,b)=add'(a,b)]]
	Conclusion, 919

	Prove: ALL(a):ALL(b):[a ε n & b ε n => add(a,b)=add'(a,b)]
	
	Suppose...

	979	x ε n & y ε n
		Premise

	980	x ε n
		Split, 979

	981	y ε n
		Split, 979

	Apply previous result

	982	x ε n => ALL(b):[b ε n => add(x,b)=add'(x,b)]
		U Spec, 978

	983	ALL(b):[b ε n => add(x,b)=add'(x,b)]
		Detach, 982, 980

	984	y ε n => add(x,y)=add'(x,y)
		U Spec, 983

	985	add(x,y)=add'(x,y)
		Detach, 984, 981

As Required:

add and add' are identical

986	ALL(a):ALL(b):[a ε n & b ε n => add(a,b)=add'(a,b)]
	Conclusion, 979

	
	Introducing the infix '+' operator, suppose...

	987	ALL(a):ALL(b):[a ε n & b ε n => a+b=add(a,b)]
		Premise

		Prove: ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
		
		Suppose...

		988	x ε n & y ε n
			Premise

		989	ALL(b):[x ε n & b ε n => add(x,b) ε n]
			U Spec, 795

		990	x ε n & y ε n => add(x,y) ε n
			U Spec, 989

		991	add(x,y) ε n
			Detach, 990, 988

		992	ALL(b):[x ε n & b ε n => x+b=add(x,b)]
			U Spec, 987

		993	x ε n & y ε n => x+y=add(x,y)
			U Spec, 992

		994	x+y=add(x,y)
			Detach, 993, 988

		995	x+y ε n
			Substitute, 994, 991

	As Required:

	996	ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
		Conclusion, 988

		Prove: ALL(a):[a ε n => a+1=next(a)]
		
		Suppose...

		997	x ε n
			Premise

		998	x ε n => add(x,1)=next(x)
			U Spec, 837

		999	add(x,1)=next(x)
			Detach, 998, 997

		1000	ALL(b):[x ε n & b ε n => x+b=add(x,b)]
			U Spec, 987

		1001	x ε n & 1 ε n => x+1=add(x,1)
			U Spec, 1000

		1002	x ε n & 1 ε n
			Join, 997, 2

		1003	x+1=add(x,1)
			Detach, 1001, 1002

		1004	x+1=next(x)
			Substitute, 1003, 999

	As Required:

	1005	ALL(a):[a ε n => a+1=next(a)]
		Conclusion, 997

		Prove: ALL(a):[a ε n => ~a+1=1]
		
		Suppose...

		1006	x ε n
			Premise

		1007	x ε n => ~next(x)=1
			U Spec, 4

		1008	~next(x)=1
			Detach, 1007, 1006

		1009	x ε n => x+1=next(x)
			U Spec, 1005

		1010	x+1=next(x)
			Detach, 1009, 1006

		1011	~x+1=1
			Substitute, 1010, 1008

	As Required:

	1012	ALL(a):[a ε n => ~a+1=1]
		Conclusion, 1006

		Prove: ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
		
		Suppose...

		1013	x ε n & y ε n & x+1=y+1
			Premise

		1014	x ε n
			Split, 1013

		1015	y ε n
			Split, 1013

		1016	x+1=y+1
			Split, 1013

		1017	ALL(b):[x ε n & b ε n & next(x)=next(b) => x=b]
			U Spec, 5

		1018	x ε n & y ε n & next(x)=next(y) => x=y
			U Spec, 1017

		1019	x ε n => x+1=next(x)
			U Spec, 1005

		1020	x+1=next(x)
			Detach, 1019, 1014

		1021	x ε n & y ε n & x+1=next(y) => x=y
			Substitute, 1020, 1018

		1022	y ε n => y+1=next(y)
			U Spec, 1005

		1023	y+1=next(y)
			Detach, 1022, 1015

		1024	x ε n & y ε n & x+1=y+1 => x=y
			Substitute, 1023, 1021

		1025	x=y
			Detach, 1024, 1013

	As Required:

	1026	ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
		Conclusion, 1013

		Prove: ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
		
		Suppose...

		1027	x ε n & y ε n
			Premise

		1028	x ε n
			Split, 1027

		1029	y ε n
			Split, 1027

		1030	ALL(b):[x ε n & b ε n => add(x,next(b))=next(add(x,b))]
			U Spec, 912

		1031	x ε n & y ε n => add(x,next(y))=next(add(x,y))
			U Spec, 1030

		1032	add(x,next(y))=next(add(x,y))
			Detach, 1031, 1027

		1033	y ε n => y+1=next(y)
			U Spec, 1005

		1034	y+1=next(y)
			Detach, 1033, 1029

		1035	add(x,y+1)=next(add(x,y))
			Substitute, 1034, 1032

		1036	ALL(b):[x ε n & b ε n => x+b=add(x,b)]
			U Spec, 987

		1037	x ε n & y+1 ε n => x+(y+1)=add(x,y+1)
			U Spec, 1036

		1038	ALL(b):[y ε n & b ε n => y+b ε n]
			U Spec, 996

		1039	y ε n & 1 ε n => y+1 ε n
			U Spec, 1038

		1040	y ε n & 1 ε n
			Join, 1029, 2

		1041	y+1 ε n
			Detach, 1039, 1040

		1042	x ε n & y+1 ε n
			Join, 1028, 1041

		1043	x+(y+1)=add(x,y+1)
			Detach, 1037, 1042

		1044	x+(y+1)=next(add(x,y))
			Substitute, 1043, 1035

		1045	ALL(b):[x ε n & b ε n => x+b=add(x,b)]
			U Spec, 987

		1046	x ε n & y ε n => x+y=add(x,y)
			U Spec, 1045

		1047	x+y=add(x,y)
			Detach, 1046, 1027

		1048	x+(y+1)=next(x+y)
			Substitute, 1047, 1044

		1049	x+y ε n => x+y+1=next(x+y)
			U Spec, 1005

		1050	ALL(b):[x ε n & b ε n => x+b ε n]
			U Spec, 996

		1051	x ε n & y ε n => x+y ε n
			U Spec, 1050

		1052	x+y ε n
			Detach, 1051, 1027

		1053	x+y+1=next(x+y)
			Detach, 1049, 1052

		1054	x+(y+1)=x+y+1
			Substitute, 1053, 1048

	As Required:

	1055	ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
		Conclusion, 1027

		Prove: ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a]
		
		Suppose...

		1056	Set(x) & 1 ε x & ALL(b):[b ε n & b ε x => b+1 ε x]
			Premise

		1057	Set(x)
			Split, 1056

		1058	1 ε x
			Split, 1056

		1059	ALL(b):[b ε n & b ε x => b+1 ε x]
			Split, 1056

		1060	Set(x) & 1 ε x & ALL(b):[b ε n & b ε x => next(b) ε x]
			=> ALL(b):[b ε n => b ε x]
			U Spec, 6

			Prove: ALL(b):[b ε n & b ε x => next(b) ε x]
			
			Suppose...

			1061	t ε n & t ε x
				Premise

			1062	t ε n
				Split, 1061

			1063	t ε x
				Split, 1061

			1064	t ε n & t ε x => t+1 ε x
				U Spec, 1059

			1065	t+1 ε x
				Detach, 1064, 1061

			1066	t ε n => t+1=next(t)
				U Spec, 1005

			1067	t+1=next(t)
				Detach, 1066, 1062

			1068	next(t) ε x
				Substitute, 1067, 1065

		1069	ALL(b):[b ε n & b ε x => next(b) ε x]
			Conclusion, 1061

		1070	Set(x) & 1 ε x
			Join, 1057, 1058

		1071	Set(x) & 1 ε x
			& ALL(b):[b ε n & b ε x => next(b) ε x]
			Join, 1070, 1069

		1072	ALL(b):[b ε n => b ε x]
			Detach, 1060, 1071

	As Required:

	1073	ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a]
		=> ALL(b):[b ε n => b ε a]]
		Conclusion, 1056

	1074	Set(n) & 1 ε n
		Join, 1, 2

	1075	Set(n) & 1 ε n
		& ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
		Join, 1074, 996

	1076	Set(n) & 1 ε n
		& ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
		& ALL(a):[a ε n => ~a+1=1]
		Join, 1075, 1012

	1077	Set(n) & 1 ε n
		& ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
		& ALL(a):[a ε n => ~a+1=1]
		& ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
		Join, 1076, 1026

	1078	Set(n) & 1 ε n
		& ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
		& ALL(a):[a ε n => ~a+1=1]
		& ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
		& ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
		Join, 1077, 1055

	1079	Set(n) & 1 ε n
		& ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
		& ALL(a):[a ε n => ~a+1=1]
		& ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
		& ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
		& ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a]
		=> ALL(b):[b ε n => b ε a]]
		Join, 1078, 1073

Introducing infix '+' operator  (DC Proof Number Axioms)

As Required:

1080	ALL(a):ALL(b):[a ε n & b ε n => a+b=add(a,b)]
	=> Set(n) & 1 ε n
	& ALL(a):ALL(b):[a ε n & b ε n => a+b ε n]
	& ALL(a):[a ε n => ~a+1=1]
	& ALL(a):ALL(b):[a ε n & b ε n & a+1=b+1 => a=b]
	& ALL(a):ALL(b):[a ε n & b ε n => a+(b+1)=a+b+1]
	& ALL(a):[Set(a) & 1 ε a & ALL(b):[b ε n & b ε a => b+1 ε a]
	=> ALL(b):[b ε n => b ε a]]
	Conclusion, 987

This proof written with the aid of DC Proof 2.0