LEMMA 1

*******

Here we construct an exponentiation function exp using an arbitrary value x0 for exp(0,0).

ALL(x0):[x0 e n

=> EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x0

& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]

This formal, machine-verified proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

AXIOMS USED

***********

Function Axiom (2 variables)

1 ALL(f):ALL(a1):ALL(a2):ALL(b):[Set''(f) & Set(a1) & Set(a2) & Set(b)

=> [ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e f => c1 e a1 & c2 e a2 & d e b]

& ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e f]]

& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e f & (c1,c2,d2) e f => d1=d2]

=> ALL(c1):ALL(c2):ALL(d):[c1 e a1 & c2 e a2 & d e b => [d=f(c1,c2) <=> (c1,c2,d) e f]]]]

Axiom

2 Set(n)

Axiom

3 0 e n

Axiom

4 ALL(a):ALL(b):[a e n & b e n => [a+1=b+1 => a=b]]

Axiom

5 ALL(a):[a e n => ~a+1=0]

Axiom

6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [0 e a & ALL(b):[b e a => b+1 e a]

=> ALL(b):[b e n => b e a]]]

Axiom

7 1 e n

Axiom

8 2 e n

Axiom

9 ALL(a):ALL(b):[a e n & b e n => a+b e n]

Axiom

10 ALL(a):ALL(b):[a e n & b e n => a*b e n]

Axiom

PROOF

*****

Suppose...

11 x0 e n

Premise

Apply Cartesian Product Axiom

12 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) e b <=> c1 e a1 & c2 e a2 & c3 e a3]]]

Cart Prod

13 ALL(a2):ALL(a3):[Set(n) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e a2 & c3 e a3]]]

U Spec, 12

14 ALL(a3):[Set(n) & Set(n) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e a3]]]

U Spec, 13

15 Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]

U Spec, 14

16 Set(n) & Set(n)

Join, 2, 2

17 Set(n) & Set(n) & Set(n)

Join, 16, 2

18 EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]

Detach, 15, 17

19 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

E Spec, 18

Define: n3

***********

20 Set''(n3)

Split, 19

21 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

Split, 19

Apply Subset Axiom

22 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

<=> (a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (a,b,c) e d]]]]

Subset, 20

23 Set''(exp) & ALL(a):ALL(b):ALL(c):[(a,b,c) e exp

<=> (a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (a,b,c) e d]]]

E Spec, 22

Define: exp (a subset of n3)

***********

24 Set''(exp)

Split, 23

25 ALL(a):ALL(b):ALL(c):[(a,b,c) e exp

<=> (a,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (a,b,c) e d]]]

Split, 23

Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e exp => a e n & b e n & c e n & (a,b,c) e n3]

Suppose...

26 (x,y,z) e exp

Premise

27 ALL(b):ALL(c):[(x,b,c) e exp

<=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,b,c) e d]]]

U Spec, 25

28 ALL(c):[(x,y,c) e exp

<=> (x,y,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,c) e d]]]

U Spec, 27

29 (x,y,z) e exp

<=> (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]

U Spec, 28

30 [(x,y,z) e exp => (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]]

& [(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]] => (x,y,z) e exp]

Iff-And, 29

31 (x,y,z) e exp => (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]

Split, 30

32 (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]] => (x,y,z) e exp

Split, 30

33 (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]

Detach, 31, 26

34 (x,y,z) e n3

Split, 33

35 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]

Split, 33

36 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

U Spec, 21

37 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

U Spec, 36

38 (x,y,z) e n3 <=> x e n & y e n & z e n

U Spec, 37

39 [(x,y,z) e n3 => x e n & y e n & z e n]

& [x e n & y e n & z e n => (x,y,z) e n3]

Iff-And, 38

40 (x,y,z) e n3 => x e n & y e n & z e n

Split, 39

41 x e n & y e n & z e n => (x,y,z) e n3

Split, 39

42 x e n & y e n & z e n

Detach, 40, 34

43 x e n & y e n & z e n & (x,y,z) e n3

Join, 42, 34

As Required:

44 ALL(a):ALL(b):ALL(c):[(a,b,c) e exp => a e n & b e n & c e n & (a,b,c) e n3]

4 Conclusion, 26

Prove: (0,0,x0) e exp

Apply definition of exp

45 ALL(b):ALL(c):[(0,b,c) e exp

<=> (0,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,b,c) e d]]]

U Spec, 25

46 ALL(c):[(0,0,c) e exp

<=> (0,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,c) e d]]]

U Spec, 45

47 (0,0,x0) e exp

<=> (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,x0) e d]]

U Spec, 46

48 [(0,0,x0) e exp => (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,x0) e d]]]

& [(0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,x0) e d]] => (0,0,x0) e exp]

Iff-And, 47

49 (0,0,x0) e exp => (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,x0) e d]]

Split, 48

Sufficient: For (0,0,x0) e exp

50 (0,0,x0) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,x0) e d]] => (0,0,x0) e exp

Split, 48

51 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]

U Spec, 21

52 ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]

U Spec, 51

53 (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n

U Spec, 52

54 [(0,0,x0) e n3 => 0 e n & 0 e n & x0 e n]

& [0 e n & 0 e n & x0 e n => (0,0,x0) e n3]

Iff-And, 53

55 (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n

Split, 54

56 0 e n & 0 e n & x0 e n => (0,0,x0) e n3

Split, 54

57 0 e n & 0 e n

Join, 3, 3

58 0 e n & 0 e n & x0 e n

Join, 57, 11

59 (0,0,x0) e n3

Detach, 56, 58

60 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

Premise

61 (0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

Premise

62 (0,0,x0) e d

Split, 61

63 (0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,x0) e d

4 Conclusion, 61

64 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,x0) e d]]

4 Conclusion, 60

65 (0,0,x0) e n3

& ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,x0) e d]]

Join, 59, 64

As Required:

66 (0,0,x0) e exp

Detach, 50, 65

Prove: ALL(a):[a e n => [~a=0 => (a,0,1) e exp]]

Suppose...

67 x e n

Premise

Prove: ~x=0 => (x,0,1) e exp

Suppose...

68 ~x=0

Premise

69 ALL(b):ALL(c):[(x,b,c) e exp

<=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,b,c) e d]]]

U Spec, 25

70 ALL(c):[(x,0,c) e exp

<=> (x,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,0,c) e d]]]

U Spec, 69

71 (x,0,1) e exp

<=> (x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,0,1) e d]]

U Spec, 70

72 [(x,0,1) e exp => (x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,0,1) e d]]]

& [(x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,0,1) e d]] => (x,0,1) e exp]

Iff-And, 71

73 (x,0,1) e exp => (x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,0,1) e d]]

Split, 72

Sufficient: For (x,0,1) e exp

74 (x,0,1) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,0,1) e d]] => (x,0,1) e exp

Split, 72

75 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

U Spec, 21

76 ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]

U Spec, 75

77 (x,0,1) e n3 <=> x e n & 0 e n & 1 e n

U Spec, 76

78 [(x,0,1) e n3 => x e n & 0 e n & 1 e n]

& [x e n & 0 e n & 1 e n => (x,0,1) e n3]

Iff-And, 77

79 (x,0,1) e n3 => x e n & 0 e n & 1 e n

Split, 78

80 x e n & 0 e n & 1 e n => (x,0,1) e n3

Split, 78

81 x e n & 0 e n

Join, 67, 3

82 x e n & 0 e n & 1 e n

Join, 81, 7

83 (x,0,1) e n3

Detach, 80, 82

84 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

Premise

Suppose...

85 (0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

Premise

86 (0,0,x0) e d

Split, 85

87 ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

Split, 85

88 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

Split, 85

89 x e n => [~x=0 => (x,0,1) e d]

U Spec, 87

90 ~x=0 => (x,0,1) e d

Detach, 89, 67

91 (x,0,1) e d

Detach, 90, 68

92 (0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,0,1) e d

4 Conclusion, 85

93 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,0,1) e d]]

4 Conclusion, 84

94 (x,0,1) e n3

& ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,0,1) e d]]

Join, 83, 93

95 (x,0,1) e exp

Detach, 74, 94

As Required:

96 ~x=0 => (x,0,1) e exp

4 Conclusion, 68

As Required:

97 ALL(a):[a e n => [~a=0 => (a,0,1) e exp]]

4 Conclusion, 67

Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e exp => (a,b+1,c*a) e exp]

Suppose...

98 (x,y,z) e exp

Premise

99 ALL(b):ALL(c):[(x,b,c) e exp

<=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,b,c) e d]]]

U Spec, 25

100 ALL(c):[(x,y,c) e exp

<=> (x,y,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,c) e d]]]

U Spec, 99

101 (x,y,z) e exp

<=> (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]

U Spec, 100

102 [(x,y,z) e exp => (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]]

& [(x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]] => (x,y,z) e exp]

Iff-And, 101

103 (x,y,z) e exp => (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]

Split, 102

104 (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]] => (x,y,z) e exp

Split, 102

105 (x,y,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]

Detach, 103, 98

106 (x,y,z) e n3

Split, 105

107 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]]

Split, 105

108 ALL(b):ALL(c):[(x,b,c) e exp

<=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,b,c) e d]]]

U Spec, 25

109 ALL(c):[(x,y+1,c) e exp

<=> (x,y+1,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,c) e d]]]

U Spec, 108

110 (x,y+1,z*x) e exp

<=> (x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z*x) e d]]

U Spec, 109

111 [(x,y+1,z*x) e exp => (x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z*x) e d]]]

& [(x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z*x) e d]] => (x,y+1,z*x) e exp]

Iff-And, 110

112 (x,y+1,z*x) e exp => (x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z*x) e d]]

Split, 111

Sufficient: For (x,y+1,z*x) e exp

113 (x,y+1,z*x) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z*x) e d]] => (x,y+1,z*x) e exp

Split, 111

114 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

U Spec, 21

115 ALL(c3):[(x,y+1,c3) e n3 <=> x e n & y+1 e n & c3 e n]

U Spec, 114

116 (x,y+1,z*x) e n3 <=> x e n & y+1 e n & z*x e n

U Spec, 115

117 [(x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n]

& [x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3]

Iff-And, 116

118 (x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n

Split, 117

119 x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3

Split, 117

120 ALL(b):[y e n & b e n => y+b e n]

U Spec, 9

121 y e n & 1 e n => y+1 e n

U Spec, 120

122 ALL(b):ALL(c):[(x,b,c) e exp => x e n & b e n & c e n & (x,b,c) e n3]

U Spec, 44

123 ALL(c):[(x,y,c) e exp => x e n & y e n & c e n & (x,y,c) e n3]

U Spec, 122

124 (x,y,z) e exp => x e n & y e n & z e n & (x,y,z) e n3

U Spec, 123

125 x e n & y e n & z e n & (x,y,z) e n3

Detach, 124, 98

126 x e n

Split, 125

127 y e n

Split, 125

128 z e n

Split, 125

129 (x,y,z) e n3

Split, 125

130 y e n & 1 e n

Join, 127, 7

131 y+1 e n

Detach, 121, 130

132 ALL(b):[z e n & b e n => z*b e n]

U Spec, 10

133 z e n & x e n => z*x e n

U Spec, 132

134 z e n & x e n

Join, 128, 126

135 z*x e n

Detach, 133, 134

136 x e n & y+1 e n

Join, 126, 131

137 x e n & y+1 e n & z*x e n

Join, 136, 135

138 (x,y+1,z*x) e n3

Detach, 119, 137

Prove: ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z*x) e d]]

Suppose...

139 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

Premise

Suppose...

140 (0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

Premise

141 (0,0,x0) e d

Split, 140

142 ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

Split, 140

143 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

Split, 140

144 ALL(f):ALL(g):[(x,f,g) e d => (x,f+1,g*x) e d]

U Spec, 143

145 ALL(g):[(x,y,g) e d => (x,y+1,g*x) e d]

U Spec, 144

146 (x,y,z) e d => (x,y+1,z*x) e d

U Spec, 145

147 Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d]

U Spec, 107

148 (0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y,z) e d

Detach, 147, 139

149 (x,y,z) e d

Detach, 148, 140

150 (x,y+1,z*x) e d

Detach, 146, 149

151 (0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z*x) e d

4 Conclusion, 140

152 ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z*x) e d]]

4 Conclusion, 139

153 (x,y+1,z*x) e n3

& ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z*x) e d]]

Join, 138, 152

154 (x,y+1,z*x) e exp

Detach, 113, 153

As Required:

155 ALL(a):ALL(b):ALL(c):[(a,b,c) e exp => (a,b+1,c*a) e exp]

4 Conclusion, 98

Apply Function Axiom (2 varibles, as given)

156 ALL(a1):ALL(a2):ALL(b):[Set''(exp) & Set(a1) & Set(a2) & Set(b)

=> [ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e exp => c1 e a1 & c2 e a2 & d e b]

& ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e exp]]

& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e exp & (c1,c2,d2) e exp => d1=d2]

=> ALL(c1):ALL(c2):ALL(d):[c1 e a1 & c2 e a2 & d e b => [d=exp(c1,c2) <=> (c1,c2,d) e exp]]]]

U Spec, 1

157 ALL(a2):ALL(b):[Set''(exp) & Set(n) & Set(a2) & Set(b)

=> [ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e exp => c1 e n & c2 e a2 & d e b]

& ALL(c1):ALL(c2):[c1 e n & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e exp]]

& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e exp & (c1,c2,d2) e exp => d1=d2]

=> ALL(c1):ALL(c2):ALL(d):[c1 e n & c2 e a2 & d e b => [d=exp(c1,c2) <=> (c1,c2,d) e exp]]]]

U Spec, 156

158 ALL(b):[Set''(exp) & Set(n) & Set(n) & Set(b)

=> [ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e exp => c1 e n & c2 e n & d e b]

& ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(d):[d e b & (c1,c2,d) e exp]]

& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e exp & (c1,c2,d2) e exp => d1=d2]

=> ALL(c1):ALL(c2):ALL(d):[c1 e n & c2 e n & d e b => [d=exp(c1,c2) <=> (c1,c2,d) e exp]]]]

U Spec, 157

159 Set''(exp) & Set(n) & Set(n) & Set(n)

=> [ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e exp => c1 e n & c2 e n & d e n]

& ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(d):[d e n & (c1,c2,d) e exp]]

& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e exp & (c1,c2,d2) e exp => d1=d2]

=> ALL(c1):ALL(c2):ALL(d):[c1 e n & c2 e n & d e n => [d=exp(c1,c2) <=> (c1,c2,d) e exp]]]

U Spec, 158

160 Set''(exp) & Set(n)

Join, 24, 2

161 Set''(exp) & Set(n) & Set(n)

Join, 160, 2

162 Set''(exp) & Set(n) & Set(n) & Set(n)

Join, 161, 2

Sufficient: For functionality of exp

163 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e exp => c1 e n & c2 e n & d e n]

& ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(d):[d e n & (c1,c2,d) e exp]]

& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e exp & (c1,c2,d2) e exp => d1=d2]

=> ALL(c1):ALL(c2):ALL(d):[c1 e n & c2 e n & d e n => [d=exp(c1,c2) <=> (c1,c2,d) e exp]]

Detach, 159, 162

Prove: ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e exp => c1 e n & c2 e n & d e n]

Suppose...

164 (x,y,z) e exp

Premise

165 ALL(b):ALL(c):[(x,b,c) e exp => x e n & b e n & c e n & (x,b,c) e n3]

U Spec, 44

166 ALL(c):[(x,y,c) e exp => x e n & y e n & c e n & (x,y,c) e n3]

U Spec, 165

167 (x,y,z) e exp => x e n & y e n & z e n & (x,y,z) e n3

U Spec, 166

168 x e n & y e n & z e n & (x,y,z) e n3

Detach, 167, 164

169 x e n

Split, 168

170 y e n

Split, 168

171 z e n

Split, 168

172 (x,y,z) e n3

Split, 168

173 x e n & y e n

Join, 169, 170

174 x e n & y e n & z e n

Join, 173, 171

Functionality - Part 1

175 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e exp => c1 e n & c2 e n & d e n]

4 Conclusion, 164

Prove: ALL(a):[a e n

=> [~a=0

=> ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e exp]]]] (by induction)

Apply Subset Axiom

176 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (0,b,c) e exp]]]

Subset, 2

177 Set(p) & ALL(b):[b e p <=> b e n & EXIST(c):[c e n & (0,b,c) e exp]]

E Spec, 176

Define: p

178 Set(p)

Split, 177

179 ALL(b):[b e p <=> b e n & EXIST(c):[c e n & (0,b,c) e exp]]

Split, 177

Apply Induction Axiom (given)

180 Set(p) & ALL(b):[b e p => b e n]

=> [0 e p & ALL(b):[b e p => b+1 e p]

=> ALL(b):[b e n => b e p]]

U Spec, 6

181 x e p

Premise

182 x e p <=> x e n & EXIST(c):[c e n & (0,x,c) e exp]

U Spec, 179

183 [x e p => x e n & EXIST(c):[c e n & (0,x,c) e exp]]

& [x e n & EXIST(c):[c e n & (0,x,c) e exp] => x e p]

Iff-And, 182

184 x e p => x e n & EXIST(c):[c e n & (0,x,c) e exp]

Split, 183

185 x e n & EXIST(c):[c e n & (0,x,c) e exp] => x e p

Split, 183

186 x e n & EXIST(c):[c e n & (0,x,c) e exp]

Detach, 184, 181

187 x e n

Split, 186

188 ALL(b):[b e p => b e n]

4 Conclusion, 181

189 Set(p) & ALL(b):[b e p => b e n]

Join, 178, 188

Sufficient: For ALL(b):[b e n => b e p]

190 0 e p & ALL(b):[b e p => b+1 e p]

=> ALL(b):[b e n => b e p]

Detach, 180, 189

Base case

*********

Prove: 0 e p

191 0 e p <=> 0 e n & EXIST(c):[c e n & (0,0,c) e exp]

U Spec, 179

192 [0 e p => 0 e n & EXIST(c):[c e n & (0,0,c) e exp]]

& [0 e n & EXIST(c):[c e n & (0,0,c) e exp] => 0 e p]

Iff-And, 191

193 0 e p => 0 e n & EXIST(c):[c e n & (0,0,c) e exp]

Split, 192

Sufficient:

194 0 e n & EXIST(c):[c e n & (0,0,c) e exp] => 0 e p

Split, 192

195 x0 e n & (0,0,x0) e exp

Join, 11, 66

196 EXIST(c):[c e n & (0,0,c) e exp]

E Gen, 195

197 0 e n & EXIST(c):[c e n & (0,0,c) e exp]

Join, 3, 196

As Required:

198 0 e p

Detach, 194, 197

Inductive Step

**************

Suppose...

199 x e p

Premise

200 x e p <=> x e n & EXIST(c):[c e n & (0,x,c) e exp]

U Spec, 179

201 [x e p => x e n & EXIST(c):[c e n & (0,x,c) e exp]]

& [x e n & EXIST(c):[c e n & (0,x,c) e exp] => x e p]

Iff-And, 200

202 x e p => x e n & EXIST(c):[c e n & (0,x,c) e exp]

Split, 201

203 x e n & EXIST(c):[c e n & (0,x,c) e exp] => x e p

Split, 201

204 x e n & EXIST(c):[c e n & (0,x,c) e exp]

Detach, 202, 199

205 x e n

Split, 204

206 EXIST(c):[c e n & (0,x,c) e exp]

Split, 204

207 y e n & (0,x,y) e exp

E Spec, 206

208 y e n

Split, 207

209 (0,x,y) e exp

Split, 207

210 x+1 e p <=> x+1 e n & EXIST(c):[c e n & (0,x+1,c) e exp]

U Spec, 179

211 [x+1 e p => x+1 e n & EXIST(c):[c e n & (0,x+1,c) e exp]]

& [x+1 e n & EXIST(c):[c e n & (0,x+1,c) e exp] => x+1 e p]

Iff-And, 210

212 x+1 e p => x+1 e n & EXIST(c):[c e n & (0,x+1,c) e exp]

Split, 211

Sufficient:

213 x+1 e n & EXIST(c):[c e n & (0,x+1,c) e exp] => x+1 e p

Split, 211

214 ALL(b):[x e n & b e n => x+b e n]

U Spec, 9

215 x e n & 1 e n => x+1 e n

U Spec, 214

216 x e n & 1 e n

Join, 205, 7

217 x+1 e n

Detach, 215, 216

218 ALL(b):ALL(c):[(0,b,c) e exp => (0,b+1,c*0) e exp]

U Spec, 155

219 ALL(c):[(0,x,c) e exp => (0,x+1,c*0) e exp]

U Spec, 218

220 (0,x,y) e exp => (0,x+1,y*0) e exp

U Spec, 219

221 (0,x+1,y*0) e exp

Detach, 220, 209

222 ALL(b):[y e n & b e n => y*b e n]

U Spec, 10

223 y e n & 0 e n => y*0 e n

U Spec, 222

224 y e n & 0 e n

Join, 208, 3

225 y*0 e n

Detach, 223, 224

226 y*0 e n & (0,x+1,y*0) e exp

Join, 225, 221

227 EXIST(c):[c e n & (0,x+1,c) e exp]

E Gen, 226

228 x+1 e n & EXIST(c):[c e n & (0,x+1,c) e exp]

Join, 217, 227

229 x+1 e p

Detach, 213, 228

As Required:

230 ALL(b):[b e p => b+1 e p]

4 Conclusion, 199

231 0 e p & ALL(b):[b e p => b+1 e p]

Join, 198, 230

As Required:

232 ALL(b):[b e n => b e p]

Detach, 190, 231

Prove: ALL(b):[b e n => EXIST(c):[c e n & (0,b,c) e exp]]

Suppose...

233 x e n

Premise

234 x e n => x e p

U Spec, 232

235 x e p

Detach, 234, 233

236 x e p <=> x e n & EXIST(c):[c e n & (0,x,c) e exp]

U Spec, 179

237 [x e p => x e n & EXIST(c):[c e n & (0,x,c) e exp]]

& [x e n & EXIST(c):[c e n & (0,x,c) e exp] => x e p]

Iff-And, 236

238 x e p => x e n & EXIST(c):[c e n & (0,x,c) e exp]

Split, 237

239 x e n & EXIST(c):[c e n & (0,x,c) e exp] => x e p

Split, 237

240 x e n & EXIST(c):[c e n & (0,x,c) e exp]

Detach, 238, 235

241 x e n

Split, 240

242 EXIST(c):[c e n & (0,x,c) e exp]

Split, 240

As Required:

243 ALL(b):[b e n => EXIST(c):[c e n & (0,b,c) e exp]]

4 Conclusion, 233

Prove: ALL(a):[a e n

=> [~a=0

=> ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e exp]]]]

Suppose...

244 x e n

Premise

Prove: ~x=0

=> ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e exp]]

Suppose...

245 ~x=0

Premise

246 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (x,b,c) e exp]]]

Subset, 2

247 Set(p2) & ALL(b):[b e p2 <=> b e n & EXIST(c):[c e n & (x,b,c) e exp]]

E Spec, 246

Define: p2

248 Set(p2)

Split, 247

249 ALL(b):[b e p2 <=> b e n & EXIST(c):[c e n & (x,b,c) e exp]]

Split, 247

250 Set(p2) & ALL(b):[b e p2 => b e n]

=> [0 e p2 & ALL(b):[b e p2 => b+1 e p2]

=> ALL(b):[b e n => b e p2]]

U Spec, 6

251 y e p2

Premise

252 y e p2 <=> y e n & EXIST(c):[c e n & (x,y,c) e exp]

U Spec, 249

253 [y e p2 => y e n & EXIST(c):[c e n & (x,y,c) e exp]]

& [y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p2]

Iff-And, 252

254 y e p2 => y e n & EXIST(c):[c e n & (x,y,c) e exp]

Split, 253

255 y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p2

Split, 253

256 y e n & EXIST(c):[c e n & (x,y,c) e exp]

Detach, 254, 251

257 y e n

Split, 256

258 ALL(b):[b e p2 => b e n]

4 Conclusion, 251

259 Set(p2) & ALL(b):[b e p2 => b e n]

Join, 248, 258

Sufficient:

260 0 e p2 & ALL(b):[b e p2 => b+1 e p2]

=> ALL(b):[b e n => b e p2]

Detach, 250, 259

261 0 e p2 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e exp]

U Spec, 249

262 [0 e p2 => 0 e n & EXIST(c):[c e n & (x,0,c) e exp]]

& [0 e n & EXIST(c):[c e n & (x,0,c) e exp] => 0 e p2]

Iff-And, 261

263 0 e p2 => 0 e n & EXIST(c):[c e n & (x,0,c) e exp]

Split, 262

Sufficient:

264 0 e n & EXIST(c):[c e n & (x,0,c) e exp] => 0 e p2

Split, 262

265 x e n => [~x=0 => (x,0,1) e exp]

U Spec, 97

266 ~x=0 => (x,0,1) e exp

Detach, 265, 244

267 (x,0,1) e exp

Detach, 266, 245

268 1 e n & (x,0,1) e exp

Join, 7, 267

269 EXIST(c):[c e n & (x,0,c) e exp]

E Gen, 268

270 0 e n & EXIST(c):[c e n & (x,0,c) e exp]

Join, 3, 269

271 0 e p2

Detach, 264, 270

Suppose...

272 y e p2

Premise

273 y e p2 <=> y e n & EXIST(c):[c e n & (x,y,c) e exp]

U Spec, 249

274 [y e p2 => y e n & EXIST(c):[c e n & (x,y,c) e exp]]

& [y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p2]

Iff-And, 273

275 y e p2 => y e n & EXIST(c):[c e n & (x,y,c) e exp]

Split, 274

276 y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p2

Split, 274

277 y e n & EXIST(c):[c e n & (x,y,c) e exp]

Detach, 275, 272

278 y e n

Split, 277

279 EXIST(c):[c e n & (x,y,c) e exp]

Split, 277

280 z e n & (x,y,z) e exp

E Spec, 279

281 z e n

Split, 280

282 (x,y,z) e exp

Split, 280

283 y+1 e p2 <=> y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]

U Spec, 249

284 [y+1 e p2 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]]

& [y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp] => y+1 e p2]

Iff-And, 283

285 y+1 e p2 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]

Split, 284

Sufficient:

286 y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp] => y+1 e p2

Split, 284

287 ALL(b):[y e n & b e n => y+b e n]

U Spec, 9

288 y e n & 1 e n => y+1 e n

U Spec, 287

289 y e n & 1 e n

Join, 278, 7

290 y+1 e n

Detach, 288, 289

291 ALL(b):ALL(c):[(x,b,c) e exp => (x,b+1,c*x) e exp]

U Spec, 155

292 ALL(c):[(x,y,c) e exp => (x,y+1,c*x) e exp]

U Spec, 291

293 (x,y,z) e exp => (x,y+1,z*x) e exp

U Spec, 292

294 (x,y+1,z*x) e exp

Detach, 293, 282

295 ALL(b):[z e n & b e n => z*b e n]

U Spec, 10

296 z e n & x e n => z*x e n

U Spec, 295

297 z e n & x e n

Join, 281, 244

298 z*x e n

Detach, 296, 297

299 z*x e n & (x,y+1,z*x) e exp

Join, 298, 294

300 EXIST(c):[c e n & (x,y+1,c) e exp]

E Gen, 299

301 y+1 e n & EXIST(c):[c e n & (x,y+1,c) e exp]

Join, 290, 300

302 y+1 e p2

Detach, 286, 301

As Required:

303 ALL(b):[b e p2 => b+1 e p2]

4 Conclusion, 272

304 0 e p2 & ALL(b):[b e p2 => b+1 e p2]

Join, 271, 303

As Required:

305 ALL(b):[b e n => b e p2]

Detach, 260, 304

306 y e n

Premise

307 y e n => y e p2

U Spec, 305

308 y e p2

Detach, 307, 306

309 y e p2 <=> y e n & EXIST(c):[c e n & (x,y,c) e exp]

U Spec, 249

310 [y e p2 => y e n & EXIST(c):[c e n & (x,y,c) e exp]]

& [y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p2]

Iff-And, 309

311 y e p2 => y e n & EXIST(c):[c e n & (x,y,c) e exp]

Split, 310

312 y e n & EXIST(c):[c e n & (x,y,c) e exp] => y e p2

Split, 310

313 y e n & EXIST(c):[c e n & (x,y,c) e exp]

Detach, 311, 308

314 y e n

Split, 313

315 EXIST(c):[c e n & (x,y,c) e exp]

Split, 313

As Required:

316 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e exp]]

4 Conclusion, 306

As Required:

317 ~x=0

=> ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e exp]]

4 Conclusion, 245

As Required:

318 ALL(a):[a e n

=> [~a=0

=> ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e exp]]]]

4 Conclusion, 244

319 x e n & y e n

Premise

320 x e n

Split, 319

321 y e n

Split, 319

Two cases:

322 x=0 | ~x=0

Or Not

323 x=0

Premise

324 y e n => EXIST(c):[c e n & (0,y,c) e exp]

U Spec, 243

325 EXIST(c):[c e n & (0,y,c) e exp]

Detach, 324, 321

326 EXIST(c):[c e n & (x,y,c) e exp]

Substitute, 323, 325

327 x=0 => EXIST(c):[c e n & (x,y,c) e exp]

4 Conclusion, 323

328 ~x=0

Premise

329 x e n

=> [~x=0

=> ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e exp]]]

U Spec, 318

330 ~x=0

=> ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e exp]]

Detach, 329, 320

331 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e exp]]

Detach, 330, 328

332 y e n => EXIST(c):[c e n & (x,y,c) e exp]

U Spec, 331

333 EXIST(c):[c e n & (x,y,c) e exp]

Detach, 332, 321

334 ~x=0 => EXIST(c):[c e n & (x,y,c) e exp]

4 Conclusion, 328

335 [x=0 => EXIST(c):[c e n & (x,y,c) e exp]]

& [~x=0 => EXIST(c):[c e n & (x,y,c) e exp]]

Join, 327, 334

336 EXIST(c):[c e n & (x,y,c) e exp]

Cases, 322, 335

Functionality - Part 2

337 ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e exp]]

4 Conclusion, 319

338 z e n

Premise

Suppose...

339 ~[(0,0,z) e exp => z=x0]

Premise

340 ~~[(0,0,z) e exp & ~z=x0]

Imply-And, 339

341 (0,0,z) e exp & ~z=x0

Rem DNeg, 340

342 (0,0,z) e exp

Split, 341

343 ~z=x0

Split, 341

344 ALL(b):ALL(c):[(0,b,c) e exp

<=> (0,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,b,c) e d]]]

U Spec, 25

345 ALL(c):[(0,0,c) e exp

<=> (0,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,c) e d]]]

U Spec, 344

346 (0,0,z) e exp

<=> (0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,z) e d]]

U Spec, 345

347 [(0,0,z) e exp => (0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,z) e d]]]

& [(0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,z) e d]] => (0,0,z) e exp]

Iff-And, 346

348 (0,0,z) e exp => (0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,z) e d]]

Split, 347

349 (0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,z) e d]] => (0,0,z) e exp

Split, 347

350 ~[(0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (0,0,z) e d]]] => ~(0,0,z) e exp

Contra, 348

351 ~[(0,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> ~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d]]] => ~(0,0,z) e exp

Imply-And, 350

352 ~~[~(0,0,z) e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> ~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d]]] => ~(0,0,z) e exp

DeMorgan, 351

353 ~(0,0,z) e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> ~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d]] => ~(0,0,z) e exp

Rem DNeg, 352

354 ~(0,0,z) e n3 | ~~EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> ~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d]] => ~(0,0,z) e exp

Quant, 353

355 ~(0,0,z) e n3 | EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> ~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d]] => ~(0,0,z) e exp

Rem DNeg, 354

356 ~(0,0,z) e n3 | EXIST(d):~~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & ~~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d]] => ~(0,0,z) e exp

Imply-And, 355

357 ~(0,0,z) e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & ~~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d]] => ~(0,0,z) e exp

Rem DNeg, 356

Sufficient: For ~(0,0,z) e exp (to obtain a contradiction using d=q, as defined below)

See line 157 of InfinitelyManyPowFunctions.htm

358 ~(0,0,z) e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d]] => ~(0,0,z) e exp

Rem DNeg, 357

359 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

<=> (a,b,c) e exp & ~[a=0 & b=0 & c=z]]]

Subset, 24

360 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q

<=> (a,b,c) e exp & ~[a=0 & b=0 & c=z]]

E Spec, 359

Define: q (q = exp - (0,0,z))

361 Set''(q)

Split, 360

362 ALL(a):ALL(b):ALL(c):[(a,b,c) e q

<=> (a,b,c) e exp & ~[a=0 & b=0 & c=z]]

Split, 360

Suppose...

363 (t,u,v) e q

Premise

364 ALL(b):ALL(c):[(t,b,c) e q

<=> (t,b,c) e exp & ~[t=0 & b=0 & c=z]]

U Spec, 362

365 ALL(c):[(t,u,c) e q

<=> (t,u,c) e exp & ~[t=0 & u=0 & c=z]]

U Spec, 364

366 (t,u,v) e q

<=> (t,u,v) e exp & ~[t=0 & u=0 & v=z]

U Spec, 365

367 [(t,u,v) e q => (t,u,v) e exp & ~[t=0 & u=0 & v=z]]

& [(t,u,v) e exp & ~[t=0 & u=0 & v=z] => (t,u,v) e q]

Iff-And, 366

368 (t,u,v) e q => (t,u,v) e exp & ~[t=0 & u=0 & v=z]

Split, 367

369 (t,u,v) e exp & ~[t=0 & u=0 & v=z] => (t,u,v) e q

Split, 367

370 (t,u,v) e exp & ~[t=0 & u=0 & v=z]

Detach, 368, 363

371 (t,u,v) e exp

Split, 370

372 ~[t=0 & u=0 & v=z]

Split, 370

373 ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n & (t,b,c) e n3]

U Spec, 44

374 ALL(c):[(t,u,c) e exp => t e n & u e n & c e n & (t,u,c) e n3]

U Spec, 373

375 (t,u,v) e exp => t e n & u e n & v e n & (t,u,v) e n3

U Spec, 374

376 t e n & u e n & v e n & (t,u,v) e n3

Detach, 375, 371

377 t e n

Split, 376

378 u e n

Split, 376

379 v e n

Split, 376

380 (t,u,v) e n3

Split, 376

381 t e n & u e n

Join, 377, 378

382 t e n & u e n & v e n

Join, 381, 379

As Required:

383 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]

4 Conclusion, 363

384 ALL(b):ALL(c):[(0,b,c) e q

<=> (0,b,c) e exp & ~[0=0 & b=0 & c=z]]

U Spec, 362

385 ALL(c):[(0,0,c) e q

<=> (0,0,c) e exp & ~[0=0 & 0=0 & c=z]]

U Spec, 384

386 (0,0,x0) e q

<=> (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]

U Spec, 385

387 [(0,0,x0) e q => (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]]

& [(0,0,x0) e exp & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q]

Iff-And, 386

388 (0,0,x0) e q => (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]

Split, 387

Sufficient:

389 (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q

Split, 387

390 0=0 & 0=0 & x0=z

Premise

391 0=0

Split, 390

392 0=0

Split, 390

393 x0=z

Split, 390

394 z=x0

Sym, 393

395 z=x0 & ~z=x0

Join, 394, 343

396 ~[0=0 & 0=0 & x0=z]

4 Conclusion, 390

397 (0,0,x0) e exp & ~[0=0 & 0=0 & x0=z]

Join, 66, 396

As Required:

398 (0,0,x0) e q

Detach, 389, 397

399 t e n

Premise

400 ~t=0

Premise

401 ALL(b):ALL(c):[(t,b,c) e q

<=> (t,b,c) e exp & ~[t=0 & b=0 & c=z]]

U Spec, 362

402 ALL(c):[(t,0,c) e q

<=> (t,0,c) e exp & ~[t=0 & 0=0 & c=z]]

U Spec, 401

403 (t,0,1) e q

<=> (t,0,1) e exp & ~[t=0 & 0=0 & 1=z]

U Spec, 402

404 [(t,0,1) e q => (t,0,1) e exp & ~[t=0 & 0=0 & 1=z]]

& [(t,0,1) e exp & ~[t=0 & 0=0 & 1=z] => (t,0,1) e q]

Iff-And, 403

405 (t,0,1) e q => (t,0,1) e exp & ~[t=0 & 0=0 & 1=z]

Split, 404

Sufficient:

406 (t,0,1) e exp & ~[t=0 & 0=0 & 1=z] => (t,0,1) e q

Split, 404

407 t e n => [~t=0 => (t,0,1) e exp]

U Spec, 97

408 ~t=0 => (t,0,1) e exp

Detach, 407, 399

409 (t,0,1) e exp

Detach, 408, 400

410 t=0 & 0=0 & 1=z

Premise

411 t=0

Split, 410

412 0=0

Split, 410

413 1=z

Split, 410

414 t=0 & ~t=0

Join, 411, 400

415 ~[t=0 & 0=0 & 1=z]

4 Conclusion, 410

416 (t,0,1) e exp & ~[t=0 & 0=0 & 1=z]

Join, 409, 415

417 (t,0,1) e q

Detach, 406, 416

418 ~t=0 => (t,0,1) e q

4 Conclusion, 400

As Required:

419 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

4 Conclusion, 399

420 (t,u,v) e q

Premise

421 ALL(b):ALL(c):[(t,b,c) e q

<=> (t,b,c) e exp & ~[t=0 & b=0 & c=z]]

U Spec, 362

422 ALL(c):[(t,u,c) e q

<=> (t,u,c) e exp & ~[t=0 & u=0 & c=z]]

U Spec, 421

423 (t,u,v) e q

<=> (t,u,v) e exp & ~[t=0 & u=0 & v=z]

U Spec, 422

424 [(t,u,v) e q => (t,u,v) e exp & ~[t=0 & u=0 & v=z]]

& [(t,u,v) e exp & ~[t=0 & u=0 & v=z] => (t,u,v) e q]

Iff-And, 423

425 (t,u,v) e q => (t,u,v) e exp & ~[t=0 & u=0 & v=z]

Split, 424

426 (t,u,v) e exp & ~[t=0 & u=0 & v=z] => (t,u,v) e q

Split, 424

427 (t,u,v) e exp & ~[t=0 & u=0 & v=z]

Detach, 425, 420

428 (t,u,v) e exp

Split, 427

429 ~[t=0 & u=0 & v=z]

Split, 427

430 ALL(b):ALL(c):[(t,b,c) e q

<=> (t,b,c) e exp & ~[t=0 & b=0 & c=z]]

U Spec, 362

431 ALL(c):[(t,u+1,c) e q

<=> (t,u+1,c) e exp & ~[t=0 & u+1=0 & c=z]]

U Spec, 430

432 (t,u+1,v*t) e q

<=> (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]

U Spec, 431

433 [(t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]]

& [(t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q]

Iff-And, 432

434 (t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]

Split, 433

Sufficient:

435 (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q

Split, 433

436 ALL(b):ALL(c):[(t,b,c) e exp => (t,b+1,c*t) e exp]

U Spec, 155

437 ALL(c):[(t,u,c) e exp => (t,u+1,c*t) e exp]

U Spec, 436

438 (t,u,v) e exp => (t,u+1,v*t) e exp

U Spec, 437

439 (t,u+1,v*t) e exp

Detach, 438, 428

440 t=0 & u+1=0 & v*t=z

Premise

441 t=0

Split, 440

442 u+1=0

Split, 440

443 v*t=z

Split, 440

444 u e n => ~u+1=0

U Spec, 5

445 ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n & (t,b,c) e n3]

U Spec, 44

446 ALL(c):[(t,u,c) e exp => t e n & u e n & c e n & (t,u,c) e n3]

U Spec, 445

447 (t,u,v) e exp => t e n & u e n & v e n & (t,u,v) e n3

U Spec, 446

448 t e n & u e n & v e n & (t,u,v) e n3

Detach, 447, 428

449 t e n

Split, 448

450 u e n

Split, 448

451 v e n

Split, 448

452 (t,u,v) e n3

Split, 448

453 ~u+1=0

Detach, 444, 450

454 u+1=0 & ~u+1=0

Join, 442, 453

455 ~[t=0 & u+1=0 & v*t=z]

4 Conclusion, 440

456 (t,u+1,v*t) e exp & ~[t=0 & u+1=0 & v*t=z]

Join, 439, 455

457 (t,u+1,v*t) e q

Detach, 435, 456

As Required:

458 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

4 Conclusion, 420

459 ALL(b):ALL(c):[(0,b,c) e q

<=> (0,b,c) e exp & ~[0=0 & b=0 & c=z]]

U Spec, 362

460 ALL(c):[(0,0,c) e q

<=> (0,0,c) e exp & ~[0=0 & 0=0 & c=z]]

U Spec, 459

461 (0,0,z) e q

<=> (0,0,z) e exp & ~[0=0 & 0=0 & z=z]

U Spec, 460

462 [(0,0,z) e q => (0,0,z) e exp & ~[0=0 & 0=0 & z=z]]

& [(0,0,z) e exp & ~[0=0 & 0=0 & z=z] => (0,0,z) e q]

Iff-And, 461

463 (0,0,z) e q => (0,0,z) e exp & ~[0=0 & 0=0 & z=z]

Split, 462

464 (0,0,z) e exp & ~[0=0 & 0=0 & z=z] => (0,0,z) e q

Split, 462

465 ~[(0,0,z) e exp & ~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q

Contra, 463

466 ~~[~(0,0,z) e exp | ~~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q

DeMorgan, 465

467 ~(0,0,z) e exp | ~~[0=0 & 0=0 & z=z] => ~(0,0,z) e q

Rem DNeg, 466

468 ~(0,0,z) e exp | 0=0 & 0=0 & z=z => ~(0,0,z) e q

Rem DNeg, 467

469 0=0

Reflex

470 z=z

Reflex

471 0=0 & 0=0

Join, 469, 469

472 0=0 & 0=0 & z=z

Join, 471, 470

473 ~(0,0,z) e exp | 0=0 & 0=0 & z=z

Arb Or, 472

As Required:

474 ~(0,0,z) e q

Detach, 468, 473

475 Set''(q)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]

Join, 361, 383

476 (0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

Join, 398, 419

477 (0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

Join, 476, 458

478 (0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

& ~(0,0,z) e q

Join, 477, 474

479 Set''(q)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]

& [(0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

& ~(0,0,z) e q]

Join, 475, 478

480 EXIST(d):[Set''(d)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

& [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

& ~(0,0,z) e d]]

E Gen, 479

481 ~(0,0,z) e n3 | EXIST(d):[Set''(d)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

& [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

& ~(0,0,z) e d]]

Arb Or, 480

482 ~(0,0,z) e exp

Detach, 358, 481

483 (0,0,z) e exp & ~(0,0,z) e exp

Join, 342, 482

As Required:

484 ~~[(0,0,z) e exp => z=x0]

4 Conclusion, 339

485 (0,0,z) e exp => z=x0

Rem DNeg, 484

As Required:

486 ALL(a):[a e n => [(0,0,a) e exp => a=x0]]

4 Conclusion, 338

Suppose...

487 t e n

Premise

488 ~t=0

Premise

Suppose to the contrary...

489 ~[(t,0,z) e exp => z=1]

Premise

490 ~~[(t,0,z) e exp & ~z=1]

Imply-And, 489

491 (t,0,z) e exp & ~z=1

Rem DNeg, 490

492 (t,0,z) e exp

Split, 491

493 ~z=1

Split, 491

494 ALL(b):ALL(c):[(t,b,c) e exp

<=> (t,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,b,c) e d]]]

U Spec, 25

495 ALL(c):[(t,0,c) e exp

<=> (t,0,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,c) e d]]]

U Spec, 494

496 (t,0,z) e exp

<=> (t,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]]

U Spec, 495

497 [(t,0,z) e exp => (t,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]]]

& [(t,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]] => (t,0,z) e exp]

Iff-And, 496

498 (t,0,z) e exp => (t,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]]

Split, 497

499 (t,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]] => (t,0,z) e exp

Split, 497

500 ~[(t,0,z) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]]] => ~(t,0,z) e exp

Contra, 498

501 ~~[~(t,0,z) e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]]] => ~(t,0,z) e exp

DeMorgan, 500

502 ~(t,0,z) e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]] => ~(t,0,z) e exp

Rem DNeg, 501

503 ~(t,0,z) e n3 | ~~EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]] => ~(t,0,z) e exp

Quant, 502

504 ~(t,0,z) e n3 | EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]] => ~(t,0,z) e exp

Rem DNeg, 503

505 ~(t,0,z) e n3 | EXIST(d):~~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & ~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]] => ~(t,0,z) e exp

Imply-And, 504

506 ~(t,0,z) e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & ~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (t,0,z) e d]] => ~(t,0,z) e exp

Rem DNeg, 505

507 ~(t,0,z) e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & ~~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(t,0,z) e d]] => ~(t,0,z) e exp

Imply-And, 506

Sufficient: For ~(t,0,z) e exp (to obtain a contradiction)

508 ~(t,0,z) e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(t,0,z) e d]] => ~(t,0,z) e exp

Rem DNeg, 507

509 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

<=> (a,b,c) e exp & ~[a=t & b=0 & c=z]]]

Subset, 24

510 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q

<=> (a,b,c) e exp & ~[a=t & b=0 & c=z]]

E Spec, 509

Define: q (exp - {t,0,z})

511 Set''(q)

Split, 510

512 ALL(a):ALL(b):ALL(c):[(a,b,c) e q

<=> (a,b,c) e exp & ~[a=t & b=0 & c=z]]

Split, 510

Suppose...

513 (u,v,w) e q

Premise

514 ALL(b):ALL(c):[(u,b,c) e q

<=> (u,b,c) e exp & ~[u=t & b=0 & c=z]]

U Spec, 512

515 ALL(c):[(u,v,c) e q

<=> (u,v,c) e exp & ~[u=t & v=0 & c=z]]

U Spec, 514

516 (u,v,w) e q

<=> (u,v,w) e exp & ~[u=t & v=0 & w=z]

U Spec, 515

517 [(u,v,w) e q => (u,v,w) e exp & ~[u=t & v=0 & w=z]]

& [(u,v,w) e exp & ~[u=t & v=0 & w=z] => (u,v,w) e q]

Iff-And, 516

518 (u,v,w) e q => (u,v,w) e exp & ~[u=t & v=0 & w=z]

Split, 517

519 (u,v,w) e exp & ~[u=t & v=0 & w=z] => (u,v,w) e q

Split, 517

520 (u,v,w) e exp & ~[u=t & v=0 & w=z]

Detach, 518, 513

521 (u,v,w) e exp

Split, 520

522 ~[u=t & v=0 & w=z]

Split, 520

523 ALL(b):ALL(c):[(u,b,c) e exp => u e n & b e n & c e n & (u,b,c) e n3]

U Spec, 44

524 ALL(c):[(u,v,c) e exp => u e n & v e n & c e n & (u,v,c) e n3]

U Spec, 523

525 (u,v,w) e exp => u e n & v e n & w e n & (u,v,w) e n3

U Spec, 524

526 u e n & v e n & w e n & (u,v,w) e n3

Detach, 525, 521

527 u e n

Split, 526

528 v e n

Split, 526

529 w e n

Split, 526

530 (u,v,w) e n3

Split, 526

531 u e n & v e n

Join, 527, 528

532 u e n & v e n & w e n

Join, 531, 529

As Required:

533 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]

4 Conclusion, 513

534 ALL(b):ALL(c):[(0,b,c) e q

<=> (0,b,c) e exp & ~[0=t & b=0 & c=z]]

U Spec, 512

535 ALL(c):[(0,0,c) e q

<=> (0,0,c) e exp & ~[0=t & 0=0 & c=z]]

U Spec, 534

536 (0,0,x0) e q

<=> (0,0,x0) e exp & ~[0=t & 0=0 & x0=z]

U Spec, 535

537 [(0,0,x0) e q => (0,0,x0) e exp & ~[0=t & 0=0 & x0=z]]

& [(0,0,x0) e exp & ~[0=t & 0=0 & x0=z] => (0,0,x0) e q]

Iff-And, 536

538 (0,0,x0) e q => (0,0,x0) e exp & ~[0=t & 0=0 & x0=z]

Split, 537

Sufficient:

539 (0,0,x0) e exp & ~[0=t & 0=0 & x0=z] => (0,0,x0) e q

Split, 537

540 0=t & 0=0 & x0=z

Premise

541 0=t

Split, 540

542 0=0

Split, 540

543 x0=z

Split, 540

544 t=0

Substitute, 541, 542

545 t=0 & ~t=0

Join, 544, 488

546 ~[0=t & 0=0 & x0=z]

4 Conclusion, 540

547 (0,0,x0) e exp & ~[0=t & 0=0 & x0=z]

Join, 66, 546

As Required:

548 (0,0,x0) e q

Detach, 539, 547

549 u e n

Premise

550 ~u=0

Premise

551 ALL(b):ALL(c):[(u,b,c) e q

<=> (u,b,c) e exp & ~[u=t & b=0 & c=z]]

U Spec, 512

552 ALL(c):[(u,0,c) e q

<=> (u,0,c) e exp & ~[u=t & 0=0 & c=z]]

U Spec, 551

553 (u,0,1) e q

<=> (u,0,1) e exp & ~[u=t & 0=0 & 1=z]

U Spec, 552

554 [(u,0,1) e q => (u,0,1) e exp & ~[u=t & 0=0 & 1=z]]

& [(u,0,1) e exp & ~[u=t & 0=0 & 1=z] => (u,0,1) e q]

Iff-And, 553

555 (u,0,1) e q => (u,0,1) e exp & ~[u=t & 0=0 & 1=z]

Split, 554

Sufficient:

556 (u,0,1) e exp & ~[u=t & 0=0 & 1=z] => (u,0,1) e q

Split, 554

557 u e n => [~u=0 => (u,0,1) e exp]

U Spec, 97

558 ~u=0 => (u,0,1) e exp

Detach, 557, 549

559 (u,0,1) e exp

Detach, 558, 550

560 u=t & 0=0 & 1=z

Premise

561 u=t

Split, 560

562 0=0

Split, 560

563 1=z

Split, 560

564 z=1

Sym, 563

565 z=1 & ~z=1

Join, 564, 493

566 ~[u=t & 0=0 & 1=z]

4 Conclusion, 560

567 (u,0,1) e exp & ~[u=t & 0=0 & 1=z]

Join, 559, 566

568 (u,0,1) e q

Detach, 556, 567

569 ~u=0 => (u,0,1) e q

4 Conclusion, 550

As Required:

570 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

4 Conclusion, 549

571 (u,v,w) e q

Premise

572 ALL(b):ALL(c):[(u,b,c) e q

<=> (u,b,c) e exp & ~[u=t & b=0 & c=z]]

U Spec, 512

573 ALL(c):[(u,v,c) e q

<=> (u,v,c) e exp & ~[u=t & v=0 & c=z]]

U Spec, 572

574 (u,v,w) e q

<=> (u,v,w) e exp & ~[u=t & v=0 & w=z]

U Spec, 573

575 [(u,v,w) e q => (u,v,w) e exp & ~[u=t & v=0 & w=z]]

& [(u,v,w) e exp & ~[u=t & v=0 & w=z] => (u,v,w) e q]

Iff-And, 574

576 (u,v,w) e q => (u,v,w) e exp & ~[u=t & v=0 & w=z]

Split, 575

577 (u,v,w) e exp & ~[u=t & v=0 & w=z] => (u,v,w) e q

Split, 575

578 (u,v,w) e exp & ~[u=t & v=0 & w=z]

Detach, 576, 571

579 (u,v,w) e exp

Split, 578

580 ~[u=t & v=0 & w=z]

Split, 578

581 ALL(b):ALL(c):[(u,b,c) e q

<=> (u,b,c) e exp & ~[u=t & b=0 & c=z]]

U Spec, 512

582 ALL(c):[(u,v+1,c) e q

<=> (u,v+1,c) e exp & ~[u=t & v+1=0 & c=z]]

U Spec, 581

583 (u,v+1,w*u) e q

<=> (u,v+1,w*u) e exp & ~[u=t & v+1=0 & w*u=z]

U Spec, 582

584 [(u,v+1,w*u) e q => (u,v+1,w*u) e exp & ~[u=t & v+1=0 & w*u=z]]

& [(u,v+1,w*u) e exp & ~[u=t & v+1=0 & w*u=z] => (u,v+1,w*u) e q]

Iff-And, 583

585 (u,v+1,w*u) e q => (u,v+1,w*u) e exp & ~[u=t & v+1=0 & w*u=z]

Split, 584

Sufficient:

586 (u,v+1,w*u) e exp & ~[u=t & v+1=0 & w*u=z] => (u,v+1,w*u) e q

Split, 584

587 ALL(b):ALL(c):[(u,b,c) e exp => (u,b+1,c*u) e exp]

U Spec, 155

588 ALL(c):[(u,v,c) e exp => (u,v+1,c*u) e exp]

U Spec, 587

589 (u,v,w) e exp => (u,v+1,w*u) e exp

U Spec, 588

590 (u,v+1,w*u) e exp

Detach, 589, 579

591 u=t & v+1=0 & w*u=z

Premise

592 u=t

Split, 591

593 v+1=0

Split, 591

594 w*u=z

Split, 591

595 v e n => ~v+1=0

U Spec, 5

596 ALL(b):ALL(c):[(u,b,c) e exp => u e n & b e n & c e n & (u,b,c) e n3]

U Spec, 44

597 ALL(c):[(u,v,c) e exp => u e n & v e n & c e n & (u,v,c) e n3]

U Spec, 596

598 (u,v,w) e exp => u e n & v e n & w e n & (u,v,w) e n3

U Spec, 597

599 u e n & v e n & w e n & (u,v,w) e n3

Detach, 598, 579

600 u e n

Split, 599

601 v e n

Split, 599

602 w e n

Split, 599

603 (u,v,w) e n3

Split, 599

604 ~v+1=0

Detach, 595, 601

605 v+1=0 & ~v+1=0

Join, 593, 604

606 ~[u=t & v+1=0 & w*u=z]

4 Conclusion, 591

607 (u,v+1,w*u) e exp & ~[u=t & v+1=0 & w*u=z]

Join, 590, 606

608 (u,v+1,w*u) e q

Detach, 586, 607

As Required:

609 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

4 Conclusion, 571

610 ALL(b):ALL(c):[(t,b,c) e q

<=> (t,b,c) e exp & ~[t=t & b=0 & c=z]]

U Spec, 512

611 ALL(c):[(t,0,c) e q

<=> (t,0,c) e exp & ~[t=t & 0=0 & c=z]]

U Spec, 610

612 (t,0,z) e q

<=> (t,0,z) e exp & ~[t=t & 0=0 & z=z]

U Spec, 611

613 [(t,0,z) e q => (t,0,z) e exp & ~[t=t & 0=0 & z=z]]

& [(t,0,z) e exp & ~[t=t & 0=0 & z=z] => (t,0,z) e q]

Iff-And, 612

614 (t,0,z) e q => (t,0,z) e exp & ~[t=t & 0=0 & z=z]

Split, 613

615 (t,0,z) e exp & ~[t=t & 0=0 & z=z] => (t,0,z) e q

Split, 613

616 ~[(t,0,z) e exp & ~[t=t & 0=0 & z=z]] => ~(t,0,z) e q

Contra, 614

617 ~~[~(t,0,z) e exp | ~~[t=t & 0=0 & z=z]] => ~(t,0,z) e q

DeMorgan, 616

618 ~(t,0,z) e exp | ~~[t=t & 0=0 & z=z] => ~(t,0,z) e q

Rem DNeg, 617

619 ~(t,0,z) e exp | t=t & 0=0 & z=z => ~(t,0,z) e q

Rem DNeg, 618

620 t=t

Reflex

621 0=0

Reflex

622 z=z

Reflex

623 t=t & 0=0

Join, 620, 621

624 t=t & 0=0 & z=z

Join, 623, 622

625 ~(t,0,z) e exp | t=t & 0=0 & z=z

Arb Or, 624

As Required:

626 ~(t,0,z) e q

Detach, 619, 625

627 Set''(q)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]

Join, 511, 533

628 (0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

Join, 548, 570

629 (0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

Join, 628, 609

630 (0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

& ~(t,0,z) e q

Join, 629, 626

631 Set''(q)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]

& [(0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

& ~(t,0,z) e q]

Join, 627, 630

632 EXIST(d):[Set''(d)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

& [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

& ~(t,0,z) e d]]

E Gen, 631

633 ~(t,0,z) e n3 | EXIST(d):[Set''(d)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

& [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

& ~(t,0,z) e d]]

Arb Or, 632

634 ~(t,0,z) e exp

Detach, 508, 633

635 (t,0,z) e exp & ~(t,0,z) e exp

Join, 492, 634

636 ~EXIST(c):~[(t,0,c) e exp => c=1]

4 Conclusion, 489

637 ~~ALL(c):~~[(t,0,c) e exp => c=1]

Quant, 636

638 ALL(c):~~[(t,0,c) e exp => c=1]

Rem DNeg, 637

639 ALL(c):[(t,0,c) e exp => c=1]

Rem DNeg, 638

640 ~t=0 => ALL(c):[(t,0,c) e exp => c=1]

4 Conclusion, 488

As Required:

641 ALL(a):[a e n => [~a=0 => ALL(c):[(a,0,c) e exp => c=1]]]

4 Conclusion, 487

Supose...

642 x e n

Premise

643 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ALL(c):ALL(d):[(x,b,c) e exp & (x,b,d) e exp => c=d]]]

Subset, 2

644 Set(p3) & ALL(b):[b e p3 <=> b e n & ALL(c):ALL(d):[(x,b,c) e exp & (x,b,d) e exp => c=d]]

E Spec, 643

Define: p3

645 Set(p3)

Split, 644

646 ALL(b):[b e p3 <=> b e n & ALL(c):ALL(d):[(x,b,c) e exp & (x,b,d) e exp => c=d]]

Split, 644

647 Set(p3) & ALL(b):[b e p3 => b e n]

=> [0 e p3 & ALL(b):[b e p3 => b+1 e p3]

=> ALL(b):[b e n => b e p3]]

U Spec, 6

648 y e p3

Premise

649 y e p3 <=> y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

U Spec, 646

650 [y e p3 => y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]]

& [y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d] => y e p3]

Iff-And, 649

651 y e p3 => y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

Split, 650

652 y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d] => y e p3

Split, 650

653 y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

Detach, 651, 648

654 y e n

Split, 653

655 ALL(b):[b e p3 => b e n]

4 Conclusion, 648

656 Set(p3) & ALL(b):[b e p3 => b e n]

Join, 645, 655

Sufficient:

657 0 e p3 & ALL(b):[b e p3 => b+1 e p3]

=> ALL(b):[b e n => b e p3]

Detach, 647, 656

658 0 e p3 <=> 0 e n & ALL(c):ALL(d):[(x,0,c) e exp & (x,0,d) e exp => c=d]

U Spec, 646

659 [0 e p3 => 0 e n & ALL(c):ALL(d):[(x,0,c) e exp & (x,0,d) e exp => c=d]]

& [0 e n & ALL(c):ALL(d):[(x,0,c) e exp & (x,0,d) e exp => c=d] => 0 e p3]

Iff-And, 658

660 0 e p3 => 0 e n & ALL(c):ALL(d):[(x,0,c) e exp & (x,0,d) e exp => c=d]

Split, 659

Sufficient:

661 0 e n & ALL(c):ALL(d):[(x,0,c) e exp & (x,0,d) e exp => c=d] => 0 e p3

Split, 659

662 x=0 | ~x=0

Or Not

663 (x,0,z1) e exp & (x,0,z2) e exp

Premise

664 (x,0,z1) e exp

Split, 663

665 (x,0,z2) e exp

Split, 663

666 ALL(b):ALL(c):[(x,b,c) e exp => x e n & b e n & c e n & (x,b,c) e n3]

U Spec, 44

667 ALL(c):[(x,0,c) e exp => x e n & 0 e n & c e n & (x,0,c) e n3]

U Spec, 666

668 (x,0,z1) e exp => x e n & 0 e n & z1 e n & (x,0,z1) e n3

U Spec, 667

669 x e n & 0 e n & z1 e n & (x,0,z1) e n3

Detach, 668, 664

670 x e n

Split, 669

671 0 e n

Split, 669

672 z1 e n

Split, 669

673 (x,0,z1) e n3

Split, 669

674 (x,0,z2) e exp => x e n & 0 e n & z2 e n & (x,0,z2) e n3

U Spec, 667

675 x e n & 0 e n & z2 e n & (x,0,z2) e n3

Detach, 674, 665

676 x e n

Split, 675

677 0 e n

Split, 675

678 z2 e n

Split, 675

679 (x,0,z2) e n3

Split, 675

680 x=0

Premise

681 z1 e n => [(0,0,z1) e exp => z1=x0]

U Spec, 486

682 (0,0,z1) e exp => z1=x0

Detach, 681, 672

683 (0,0,z1) e exp

Substitute, 680, 664

684 z1=x0

Detach, 682, 683

685 z2 e n => [(0,0,z2) e exp => z2=x0]

U Spec, 486

686 (0,0,z2) e exp => z2=x0

Detach, 685, 678

687 (0,0,z2) e exp

Substitute, 680, 665

688 z2=x0

Detach, 686, 687

689 z1=z2

Substitute, 688, 684

690 x=0 => z1=z2

4 Conclusion, 680

691 ~x=0

Premise

692 x e n => [~x=0 => ALL(c):[(x,0,c) e exp => c=1]]

U Spec, 641

693 ~x=0 => ALL(c):[(x,0,c) e exp => c=1]

Detach, 692, 642

694 ALL(c):[(x,0,c) e exp => c=1]

Detach, 693, 691

695 (x,0,z1) e exp => z1=1

U Spec, 694

696 z1=1

Detach, 695, 664

697 (x,0,z2) e exp => z2=1

U Spec, 694

698 z2=1

Detach, 697, 665

699 z1=z2

Substitute, 698, 696

700 ~x=0 => z1=z2

4 Conclusion, 691

701 [x=0 => z1=z2] & [~x=0 => z1=z2]

Join, 690, 700

702 z1=z2

Cases, 662, 701

703 ALL(c):ALL(d):[(x,0,c) e exp & (x,0,d) e exp => c=d]

4 Conclusion, 663

704 0 e n

& ALL(c):ALL(d):[(x,0,c) e exp & (x,0,d) e exp => c=d]

Join, 3, 703

As Required:

705 0 e p3

Detach, 661, 704

Suppose...

706 y e p3

Premise

707 y e p3 <=> y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

U Spec, 646

708 [y e p3 => y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]]

& [y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d] => y e p3]

Iff-And, 707

709 y e p3 => y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

Split, 708

710 y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d] => y e p3

Split, 708

711 y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

Detach, 709, 706

712 y e n

Split, 711

713 ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

Split, 711

714 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e exp]]

U Spec, 337

715 x e n & y e n => EXIST(c):[c e n & (x,y,c) e exp]

U Spec, 714

716 x e n & y e n

Join, 642, 712

717 EXIST(c):[c e n & (x,y,c) e exp]

Detach, 715, 716

718 z1 e n & (x,y,z1) e exp

E Spec, 717

719 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e exp]]

U Spec, 337

720 x e n & y e n => EXIST(c):[c e n & (x,y,c) e exp]

U Spec, 719

721 x e n & y e n

Join, 642, 712

722 EXIST(c):[c e n & (x,y,c) e exp]

Detach, 720, 721

723 z e n & (x,y,z) e exp

E Spec, 722

724 z e n

Split, 723

725 (x,y,z) e exp

Split, 723

726 ALL(d):[(x,y,z) e exp & (x,y,d) e exp => z=d]

U Spec, 713

Suppose...

727 z' e n

Premise

728 (x,y,z) e exp & (x,y,z') e exp => z=z'

U Spec, 726

729 (x,y,z') e exp

Premise

730 (x,y,z) e exp & (x,y,z') e exp

Join, 725, 729

731 z=z'

Detach, 728, 730

732 (x,y,z') e exp => z=z'

4 Conclusion, 729

733 ALL(c):[c e n => [(x,y,c) e exp => z=c]]

4 Conclusion, 727

Suppose...

734 z' e n

Premise

Suppose to the contrary...

735 ~[(x,y+1,z') e exp => z'=z*x]

Premise

736 ~~[(x,y+1,z') e exp & ~z'=z*x]

Imply-And, 735

737 (x,y+1,z') e exp & ~z'=z*x

Rem DNeg, 736

738 (x,y+1,z') e exp

Split, 737

739 ~z'=z*x

Split, 737

740 ALL(b):ALL(c):[(x,b,c) e exp

<=> (x,b,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,b,c) e d]]]

U Spec, 25

741 ALL(c):[(x,y+1,c) e exp

<=> (x,y+1,c) e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,c) e d]]]

U Spec, 740

742 (x,y+1,z') e exp

<=> (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]]

U Spec, 741

743 [(x,y+1,z') e exp => (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]]]

& [(x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]] => (x,y+1,z') e exp]

Iff-And, 742

744 (x,y+1,z') e exp => (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]]

Split, 743

745 (x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]] => (x,y+1,z') e exp

Split, 743

746 ~[(x,y+1,z') e n3 & ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]]] => ~(x,y+1,z') e exp

Contra, 744

747 ~~[~(x,y+1,z') e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]]] => ~(x,y+1,z') e exp

DeMorgan, 746

748 ~(x,y+1,z') e n3 | ~ALL(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]] => ~(x,y+1,z') e exp

Rem DNeg, 747

749 ~(x,y+1,z') e n3 | ~~EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]] => ~(x,y+1,z') e exp

Quant, 748

750 ~(x,y+1,z') e n3 | EXIST(d):~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

=> [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]] => ~(x,y+1,z') e exp

Rem DNeg, 749

751 ~(x,y+1,z') e n3 | EXIST(d):~~[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & ~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]] => ~(x,y+1,z') e exp

Imply-And, 750

752 ~(x,y+1,z') e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & ~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

=> (x,y+1,z') e d]] => ~(x,y+1,z') e exp

Rem DNeg, 751

753 ~(x,y+1,z') e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & ~~[(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d]] => ~(x,y+1,z') e exp

Imply-And, 752

Sufficient: ~(x,y+1,z') e exp

754 ~(x,y+1,z') e n3 | EXIST(d):[Set''(d) & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n] & [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d]] => ~(x,y+1,z') e exp

Rem DNeg, 753

755 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

<=> (a,b,c) e exp & ~[a=x & b=y+1 & c=z']]]

Subset, 24

756 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q

<=> (a,b,c) e exp & ~[a=x & b=y+1 & c=z']]

E Spec, 755

Define: q

757 Set''(q)

Split, 756

758 ALL(a):ALL(b):ALL(c):[(a,b,c) e q

<=> (a,b,c) e exp & ~[a=x & b=y+1 & c=z']]

Split, 756

759 (t,u,v) e q

Premise

760 ALL(b):ALL(c):[(t,b,c) e q

<=> (t,b,c) e exp & ~[t=x & b=y+1 & c=z']]

U Spec, 758

761 ALL(c):[(t,u,c) e q

<=> (t,u,c) e exp & ~[t=x & u=y+1 & c=z']]

U Spec, 760

762 (t,u,v) e q

<=> (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

U Spec, 761

763 [(t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']]

& [(t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]

Iff-And, 762

764 (t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

Split, 763

765 (t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q

Split, 763

766 (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

Detach, 764, 759

767 (t,u,v) e exp

Split, 766

768 ~[t=x & u=y+1 & v=z']

Split, 766

769 ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n & (t,b,c) e n3]

U Spec, 44

770 ALL(c):[(t,u,c) e exp => t e n & u e n & c e n & (t,u,c) e n3]

U Spec, 769

771 (t,u,v) e exp => t e n & u e n & v e n & (t,u,v) e n3

U Spec, 770

772 t e n & u e n & v e n & (t,u,v) e n3

Detach, 771, 767

773 t e n

Split, 772

774 u e n

Split, 772

775 v e n

Split, 772

776 (t,u,v) e n3

Split, 772

777 t e n & u e n

Join, 773, 774

778 t e n & u e n & v e n

Join, 777, 775

As Required:

779 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]

4 Conclusion, 759

780 ALL(b):ALL(c):[(0,b,c) e q

<=> (0,b,c) e exp & ~[0=x & b=y+1 & c=z']]

U Spec, 758

781 ALL(c):[(0,0,c) e q

<=> (0,0,c) e exp & ~[0=x & 0=y+1 & c=z']]

U Spec, 780

782 (0,0,x0) e q

<=> (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']

U Spec, 781

783 [(0,0,x0) e q => (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']]

& [(0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q]

Iff-And, 782

784 (0,0,x0) e q => (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']

Split, 783

785 (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q

Split, 783

Suppose to the contrary...

786 0=x & 0=y+1 & x0=z'

Premise

787 0=x

Split, 786

788 0=y+1

Split, 786

789 x0=z'

Split, 786

790 y e n => ~y+1=0

U Spec, 5

791 ~y+1=0

Detach, 790, 712

792 ~0=y+1

Sym, 791

793 0=y+1 & ~0=y+1

Join, 788, 792

794 ~[0=x & 0=y+1 & x0=z']

4 Conclusion, 786

795 (0,0,x0) e exp & ~[0=x & 0=y+1 & x0=z']

Join, 66, 794

As Required:

796 (0,0,x0) e q

Detach, 785, 795

Suppose...

797 t e n

Premise

Suppose...

798 ~t=0

Premise

799 ALL(b):ALL(c):[(t,b,c) e q

<=> (t,b,c) e exp & ~[t=x & b=y+1 & c=z']]

U Spec, 758

800 ALL(c):[(t,0,c) e q

<=> (t,0,c) e exp & ~[t=x & 0=y+1 & c=z']]

U Spec, 799

801 (t,0,1) e q

<=> (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']

U Spec, 800

802 [(t,0,1) e q => (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']]

& [(t,0,1) e exp & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q]

Iff-And, 801

803 (t,0,1) e q => (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']

Split, 802

Sufficient:

804 (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q

Split, 802

805 t e n => [~t=0 => (t,0,1) e exp]

U Spec, 97

806 ~t=0 => (t,0,1) e exp

Detach, 805, 797

807 (t,0,1) e exp

Detach, 806, 798

808 t=x & 0=y+1 & 1=z'

Premise

809 t=x

Split, 808

810 0=y+1

Split, 808

811 1=z'

Split, 808

812 y e n => ~y+1=0

U Spec, 5

813 ~y+1=0

Detach, 812, 712

814 ~0=y+1

Sym, 813

815 0=y+1 & ~0=y+1

Join, 810, 814

816 ~[t=x & 0=y+1 & 1=z']

4 Conclusion, 808

817 (t,0,1) e exp & ~[t=x & 0=y+1 & 1=z']

Join, 807, 816

818 (t,0,1) e q

Detach, 804, 817

819 ~t=0 => (t,0,1) e q

4 Conclusion, 798

As Required:

820 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

4 Conclusion, 797

Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

Suppose...

821 (t,u,v) e q

Premise

822 ALL(b):ALL(c):[(t,b,c) e q

<=> (t,b,c) e exp & ~[t=x & b=y+1 & c=z']]

U Spec, 758

823 ALL(c):[(t,u,c) e q

<=> (t,u,c) e exp & ~[t=x & u=y+1 & c=z']]

U Spec, 822

824 (t,u,v) e q

<=> (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

U Spec, 823

825 [(t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']]

& [(t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]

Iff-And, 824

826 (t,u,v) e q => (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

Split, 825

827 (t,u,v) e exp & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q

Split, 825

828 (t,u,v) e exp & ~[t=x & u=y+1 & v=z']

Detach, 826, 821

829 (t,u,v) e exp

Split, 828

830 ~[t=x & u=y+1 & v=z']

Split, 828

831 ALL(b):ALL(c):[(t,b,c) e exp => t e n & b e n & c e n & (t,b,c) e n3]

U Spec, 44

832 ALL(c):[(t,u,c) e exp => t e n & u e n & c e n & (t,u,c) e n3]

U Spec, 831

833 (t,u,v) e exp => t e n & u e n & v e n & (t,u,v) e n3

U Spec, 832

834 t e n & u e n & v e n & (t,u,v) e n3

Detach, 833, 829

835 t e n

Split, 834

836 u e n

Split, 834

837 v e n

Split, 834

838 (t,u,v) e n3

Split, 834

839 ALL(b):ALL(c):[(t,b,c) e q

<=> (t,b,c) e exp & ~[t=x & b=y+1 & c=z']]

U Spec, 758

840 ALL(c):[(t,u+1,c) e q

<=> (t,u+1,c) e exp & ~[t=x & u+1=y+1 & c=z']]

U Spec, 839

841 (t,u+1,v*t) e q

<=> (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']

U Spec, 840

842 [(t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']]

& [(t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q]

Iff-And, 841

843 (t,u+1,v*t) e q => (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']

Split, 842

Sufficient:

844 (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q

Split, 842

845 ALL(b):ALL(c):[(t,b,c) e exp => (t,b+1,c*t) e exp]

U Spec, 155

846 ALL(c):[(t,u,c) e exp => (t,u+1,c*t) e exp]

U Spec, 845

847 (t,u,v) e exp => (t,u+1,v*t) e exp

U Spec, 846

848 (t,u+1,v*t) e exp

Detach, 847, 829

849 t=x & u+1=y+1 & v*t=z'

Premise

850 t=x

Split, 849

851 u+1=y+1

Split, 849

852 v*t=z'

Split, 849

853 v*x=z'

Substitute, 850, 852

854 ALL(b):[u e n & b e n => [u+1=b+1 => u=b]]

U Spec, 4

855 u e n & y e n => [u+1=y+1 => u=y]

U Spec, 854

856 u e n & y e n

Join, 836, 712

857 u+1=y+1 => u=y

Detach, 855, 856

858 u=y

Detach, 857, 851

859 (x,u,v) e exp

Substitute, 850, 829

860 (x,y,v) e exp

Substitute, 858, 859

861 v e n => [(x,y,v) e exp => z=v]

U Spec, 733

862 (x,y,v) e exp => z=v

Detach, 861, 837

863 z=v

Detach, 862, 860

864 z*x=z'

Substitute, 863, 853

865 z'=z*x

Sym, 864

866 z'=z*x & ~z'=z*x

Join, 865, 739

867 ~[t=x & u+1=y+1 & v*t=z']

4 Conclusion, 849

868 (t,u+1,v*t) e exp & ~[t=x & u+1=y+1 & v*t=z']

Join, 848, 867

869 (t,u+1,v*t) e q

Detach, 844, 868

As Required:

870 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

4 Conclusion, 821

871 ALL(b):ALL(c):[(x,b,c) e q

<=> (x,b,c) e exp & ~[x=x & b=y+1 & c=z']]

U Spec, 758

872 ALL(c):[(x,y+1,c) e q

<=> (x,y+1,c) e exp & ~[x=x & y+1=y+1 & c=z']]

U Spec, 871

873 (x,y+1,z') e q

<=> (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']

U Spec, 872

874 [(x,y+1,z') e q => (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']]

& [(x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q]

Iff-And, 873

875 (x,y+1,z') e q => (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']

Split, 874

876 (x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q

Split, 874

877 ~[(x,y+1,z') e exp & ~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q

Contra, 875

878 ~~[~(x,y+1,z') e exp | ~~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q

DeMorgan, 877

879 ~(x,y+1,z') e exp | ~~[x=x & y+1=y+1 & z'=z'] => ~(x,y+1,z') e q

Rem DNeg, 878

880 ~(x,y+1,z') e exp | x=x & y+1=y+1 & z'=z' => ~(x,y+1,z') e q

Rem DNeg, 879

881 x=x

Reflex

882 y+1=y+1

Reflex

883 z'=z'

Reflex

884 x=x & y+1=y+1

Join, 881, 882

885 x=x & y+1=y+1 & z'=z'

Join, 884, 883

886 ~(x,y+1,z') e exp | x=x & y+1=y+1 & z'=z'

Arb Or, 885

As Required:

887 ~(x,y+1,z') e q

Detach, 880, 886

888 Set''(q)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]

Join, 757, 779

889 (0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

Join, 796, 820

890 (0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

Join, 889, 870

891 (0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

& ~(x,y+1,z') e q

Join, 890, 887

892 Set''(q)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => e e n & f e n & g e n]

& [(0,0,x0) e q

& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

& ~(x,y+1,z') e q]

Join, 888, 891

893 EXIST(d):[Set''(d)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

& [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

& ~(x,y+1,z') e d]]

E Gen, 892

894 ~(x,y+1,z') e n3 | EXIST(d):[Set''(d)

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => e e n & f e n & g e n]

& [(0,0,x0) e d

& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

& ~(x,y+1,z') e d]]

Arb Or, 893

895 ~(x,y+1,z') e exp

Detach, 754, 894

896 (x,y+1,z') e exp & ~(x,y+1,z') e exp

Join, 738, 895

897 ~~[(x,y+1,z') e exp => z'=z*x]

4 Conclusion, 735

898 (x,y+1,z') e exp => z'=z*x

Rem DNeg, 897

899 ALL(d):[d e n => [(x,y+1,d) e exp => d=z*x]]

4 Conclusion, 734

900 y+1 e p3 <=> y+1 e n & ALL(c):ALL(d):[(x,y+1,c) e exp & (x,y+1,d) e exp => c=d]

U Spec, 646

901 [y+1 e p3 => y+1 e n & ALL(c):ALL(d):[(x,y+1,c) e exp & (x,y+1,d) e exp => c=d]]

& [y+1 e n & ALL(c):ALL(d):[(x,y+1,c) e exp & (x,y+1,d) e exp => c=d] => y+1 e p3]

Iff-And, 900

902 y+1 e p3 => y+1 e n & ALL(c):ALL(d):[(x,y+1,c) e exp & (x,y+1,d) e exp => c=d]

Split, 901

Sufficient: y+1 e p3

903 y+1 e n & ALL(c):ALL(d):[(x,y+1,c) e exp & (x,y+1,d) e exp => c=d] => y+1 e p3

Split, 901

904 ALL(b):[y e n & b e n => y+b e n]

U Spec, 9

905 y e n & 1 e n => y+1 e n

U Spec, 904

906 y e n & 1 e n

Join, 712, 7

907 y+1 e n

Detach, 905, 906

908 (x,y+1,z') e exp & (x,y+1,z'') e exp

Premise

909 (x,y+1,z') e exp

Split, 908

910 (x,y+1,z'') e exp

Split, 908

911 ALL(b):ALL(c):[(x,b,c) e exp => x e n & b e n & c e n & (x,b,c) e n3]

U Spec, 44

912 ALL(c):[(x,y+1,c) e exp => x e n & y+1 e n & c e n & (x,y+1,c) e n3]

U Spec, 911

913 (x,y+1,z') e exp => x e n & y+1 e n & z' e n & (x,y+1,z') e n3

U Spec, 912

914 x e n & y+1 e n & z' e n & (x,y+1,z') e n3

Detach, 913, 909

915 x e n

Split, 914

916 y+1 e n

Split, 914

917 z' e n

Split, 914

918 (x,y+1,z') e n3

Split, 914

919 z' e n => [(x,y+1,z') e exp => z'=z*x]

U Spec, 899

920 (x,y+1,z') e exp => z'=z*x

Detach, 919, 917

921 z'=z*x

Detach, 920, 909

922 (x,y+1,z'') e exp => x e n & y+1 e n & z'' e n & (x,y+1,z'') e n3

U Spec, 912

923 x e n & y+1 e n & z'' e n & (x,y+1,z'') e n3

Detach, 922, 910

924 x e n

Split, 923

925 y+1 e n

Split, 923

926 z'' e n

Split, 923

927 (x,y+1,z'') e n3

Split, 923

928 z'' e n => [(x,y+1,z'') e exp => z''=z*x]

U Spec, 899

929 (x,y+1,z'') e exp => z''=z*x

Detach, 928, 926

930 z''=z*x

Detach, 929, 910

931 z'=z''

Substitute, 930, 921

932 ALL(c):ALL(d):[(x,y+1,c) e exp & (x,y+1,d) e exp => c=d]

4 Conclusion, 908

933 y+1 e n

& ALL(c):ALL(d):[(x,y+1,c) e exp & (x,y+1,d) e exp => c=d]

Join, 907, 932

934 y+1 e p3

Detach, 903, 933

935 ALL(b):[b e p3 => b+1 e p3]

4 Conclusion, 706

936 0 e p3 & ALL(b):[b e p3 => b+1 e p3]

Join, 705, 935

937 ALL(b):[b e n => b e p3]

Detach, 657, 936

938 y e n

Premise

939 y e n => y e p3

U Spec, 937

940 y e p3

Detach, 939, 938

941 y e p3 <=> y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

U Spec, 646

942 [y e p3 => y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]]

& [y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d] => y e p3]

Iff-And, 941

943 y e p3 => y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

Split, 942

944 y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d] => y e p3

Split, 942

945 y e n & ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

Detach, 943, 940

946 y e n

Split, 945

947 ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

Split, 945

948 ALL(b):[b e n

=> ALL(c):ALL(d):[(x,b,c) e exp & (x,b,d) e exp => c=d]]

4 Conclusion, 938

949 ALL(a):[a e n

=> ALL(b):[b e n

=> ALL(c):ALL(d):[(a,b,c) e exp & (a,b,d) e exp => c=d]]]

4 Conclusion, 642

950 (x,y,z1) e exp & (x,y,z2) e exp

Premise

951 (x,y,z1) e exp

Split, 950

952 (x,y,z2) e exp

Split, 950

953 ALL(b):ALL(c):[(x,b,c) e exp => x e n & b e n & c e n & (x,b,c) e n3]

U Spec, 44

954 ALL(c):[(x,y,c) e exp => x e n & y e n & c e n & (x,y,c) e n3]

U Spec, 953

955 (x,y,z1) e exp => x e n & y e n & z1 e n & (x,y,z1) e n3

U Spec, 954

956 x e n & y e n & z1 e n & (x,y,z1) e n3

Detach, 955, 951

957 x e n

Split, 956

958 y e n

Split, 956

959 z1 e n

Split, 956

960 (x,y,z1) e n3

Split, 956

961 (x,y,z2) e exp => x e n & y e n & z2 e n & (x,y,z2) e n3

U Spec, 954

962 x e n & y e n & z2 e n & (x,y,z2) e n3

Detach, 961, 952

963 x e n

Split, 962

964 y e n

Split, 962

965 z2 e n

Split, 962

966 (x,y,z2) e n3

Split, 962

967 x e n

=> ALL(b):[b e n

=> ALL(c):ALL(d):[(x,b,c) e exp & (x,b,d) e exp => c=d]]

U Spec, 949

968 ALL(b):[b e n

=> ALL(c):ALL(d):[(x,b,c) e exp & (x,b,d) e exp => c=d]]

Detach, 967, 963

969 y e n

=> ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

U Spec, 968

970 ALL(c):ALL(d):[(x,y,c) e exp & (x,y,d) e exp => c=d]

Detach, 969, 964

971 ALL(d):[(x,y,z1) e exp & (x,y,d) e exp => z1=d]

U Spec, 970

972 (x,y,z1) e exp & (x,y,z2) e exp => z1=z2

U Spec, 971

973 z1=z2

Detach, 972, 950

Functionality - Part 3

974 ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e exp & (c1,c2,d2) e exp => d1=d2]

4 Conclusion, 950

975 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e exp => c1 e n & c2 e n & d e n]

& ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e exp]]

Join, 175, 337

976 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e exp => c1 e n & c2 e n & d e n]

& ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e exp]]

& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e exp & (c1,c2,d2) e exp => d1=d2]

Join, 975, 974

exp is a function!

As Required:

977 ALL(c1):ALL(c2):ALL(d):[c1 e n & c2 e n & d e n => [d=exp(c1,c2) <=> (c1,c2,d) e exp]]

Detach, 163, 976

978 t e n & u e n

Premise

979 ALL(b):[t e n & b e n => EXIST(c):[c e n & (t,b,c) e exp]]

U Spec, 337

980 t e n & u e n => EXIST(c):[c e n & (t,u,c) e exp]

U Spec, 979

981 EXIST(c):[c e n & (t,u,c) e exp]

Detach, 980, 978

982 v e n & (t,u,v) e exp

E Spec, 981

983 v e n

Split, 982

984 (t,u,v) e exp

Split, 982

985 ALL(c2):ALL(d):[t e n & c2 e n & d e n => [d=exp(t,c2) <=> (t,c2,d) e exp]]

U Spec, 977

986 ALL(d):[t e n & u e n & d e n => [d=exp(t,u) <=> (t,u,d) e exp]]

U Spec, 985

987 t e n & u e n & v e n => [v=exp(t,u) <=> (t,u,v) e exp]

U Spec, 986

988 t e n & u e n & v e n

Join, 978, 983

989 v=exp(t,u) <=> (t,u,v) e exp

Detach, 987, 988

990 [v=exp(t,u) => (t,u,v) e exp]

& [(t,u,v) e exp => v=exp(t,u)]

Iff-And, 989

991 v=exp(t,u) => (t,u,v) e exp

Split, 990

992 (t,u,v) e exp => v=exp(t,u)

Split, 990

993 v=exp(t,u)

Detach, 992, 984

994 exp(t,u) e n

Substitute, 993, 983

As Required:

995 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

4 Conclusion, 978

996 ALL(c2):ALL(d):[0 e n & c2 e n & d e n => [d=exp(0,c2) <=> (0,c2,d) e exp]]

U Spec, 977

997 ALL(d):[0 e n & 0 e n & d e n => [d=exp(0,0) <=> (0,0,d) e exp]]

U Spec, 996

998 0 e n & 0 e n & x0 e n => [x0=exp(0,0) <=> (0,0,x0) e exp]

U Spec, 997

999 0 e n & 0 e n

Join, 3, 3

1000 0 e n & 0 e n & x0 e n

Join, 999, 11

1001 x0=exp(0,0) <=> (0,0,x0) e exp

Detach, 998, 1000

1002 [x0=exp(0,0) => (0,0,x0) e exp]

& [(0,0,x0) e exp => x0=exp(0,0)]

Iff-And, 1001

1003 x0=exp(0,0) => (0,0,x0) e exp

Split, 1002

1004 (0,0,x0) e exp => x0=exp(0,0)

Split, 1002

1005 x0=exp(0,0)

Detach, 1004, 66

As Required:

1006 exp(0,0)=x0

Sym, 1005

1007 t e n

Premise

1008 ~t=0

Premise

1009 t e n => [~t=0 => (t,0,1) e exp]

U Spec, 97

1010 ~t=0 => (t,0,1) e exp

Detach, 1009, 1007

1011 (t,0,1) e exp

Detach, 1010, 1008

1012 ALL(c2):ALL(d):[t e n & c2 e n & d e n => [d=exp(t,c2) <=> (t,c2,d) e exp]]

U Spec, 977

1013 ALL(d):[t e n & 0 e n & d e n => [d=exp(t,0) <=> (t,0,d) e exp]]

U Spec, 1012

1014 t e n & 0 e n & 1 e n => [1=exp(t,0) <=> (t,0,1) e exp]

U Spec, 1013

1015 t e n & 0 e n

Join, 1007, 3

1016 t e n & 0 e n & 1 e n

Join, 1015, 7

1017 1=exp(t,0) <=> (t,0,1) e exp

Detach, 1014, 1016

1018 [1=exp(t,0) => (t,0,1) e exp]

& [(t,0,1) e exp => 1=exp(t,0)]

Iff-And, 1017

1019 1=exp(t,0) => (t,0,1) e exp

Split, 1018

1020 (t,0,1) e exp => 1=exp(t,0)

Split, 1018

1021 1=exp(t,0)

Detach, 1020, 1011

1022 exp(t,0)=1

Sym, 1021

1023 ~t=0 => exp(t,0)=1

4 Conclusion, 1008

As Required:

1024 ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

4 Conclusion, 1007

1025 t e n & u e n

Premise

1026 t e n

Split, 1025

1027 u e n

Split, 1025

1028 ALL(b):[t e n & b e n => EXIST(c):[c e n & (t,b,c) e exp]]

U Spec, 337

1029 t e n & u e n => EXIST(c):[c e n & (t,u,c) e exp]

U Spec, 1028

1030 EXIST(c):[c e n & (t,u,c) e exp]

Detach, 1029, 1025

1031 v e n & (t,u,v) e exp

E Spec, 1030

1032 v e n

Split, 1031

1033 (t,u,v) e exp

Split, 1031

1034 ALL(c2):ALL(d):[t e n & c2 e n & d e n => [d=exp(t,c2) <=> (t,c2,d) e exp]]

U Spec, 977

1035 ALL(d):[t e n & u e n & d e n => [d=exp(t,u) <=> (t,u,d) e exp]]

U Spec, 1034

1036 t e n & u e n & v e n => [v=exp(t,u) <=> (t,u,v) e exp]

U Spec, 1035

1037 t e n & u e n & v e n

Join, 1025, 1032

1038 v=exp(t,u) <=> (t,u,v) e exp

Detach, 1036, 1037

1039 [v=exp(t,u) => (t,u,v) e exp]

& [(t,u,v) e exp => v=exp(t,u)]

Iff-And, 1038

1040 v=exp(t,u) => (t,u,v) e exp

Split, 1039

1041 (t,u,v) e exp => v=exp(t,u)

Split, 1039

1042 v=exp(t,u)

Detach, 1041, 1033

1043 ALL(b):ALL(c):[(t,b,c) e exp => (t,b+1,c*t) e exp]

U Spec, 155

1044 ALL(c):[(t,u,c) e exp => (t,u+1,c*t) e exp]

U Spec, 1043

1045 (t,u,v) e exp => (t,u+1,v*t) e exp

U Spec, 1044

1046 (t,u+1,v*t) e exp

Detach, 1045, 1033

1047 ALL(c2):ALL(d):[t e n & c2 e n & d e n => [d=exp(t,c2) <=> (t,c2,d) e exp]]

U Spec, 977

1048 ALL(d):[t e n & u+1 e n & d e n => [d=exp(t,u+1) <=> (t,u+1,d) e exp]]

U Spec, 1047

1049 t e n & u+1 e n & v*t e n => [v*t=exp(t,u+1) <=> (t,u+1,v*t) e exp]

U Spec, 1048

1050 ALL(b):[u e n & b e n => u+b e n]

U Spec, 9

1051 u e n & 1 e n => u+1 e n

U Spec, 1050

1052 u e n & 1 e n

Join, 1027, 7

1053 u+1 e n

Detach, 1051, 1052

1054 ALL(b):[v e n & b e n => v*b e n]

U Spec, 10

1055 v e n & t e n => v*t e n

U Spec, 1054

1056 v e n & t e n

Join, 1032, 1026

1057 v*t e n

Detach, 1055, 1056

1058 t e n & u+1 e n

Join, 1026, 1053

1059 t e n & u+1 e n & v*t e n

Join, 1058, 1057

1060 v*t=exp(t,u+1) <=> (t,u+1,v*t) e exp

Detach, 1049, 1059

1061 [v*t=exp(t,u+1) => (t,u+1,v*t) e exp]

& [(t,u+1,v*t) e exp => v*t=exp(t,u+1)]

Iff-And, 1060

1062 v*t=exp(t,u+1) => (t,u+1,v*t) e exp

Split, 1061

1063 (t,u+1,v*t) e exp => v*t=exp(t,u+1)

Split, 1061

1064 v*t=exp(t,u+1)

Detach, 1063, 1046

1065 exp(t,u)*t=exp(t,u+1)

Substitute, 1042, 1064

1066 exp(t,u+1)=exp(t,u)*t

Sym, 1065

1067 ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

4 Conclusion, 1025

1068 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x0

Join, 995, 1006

1069 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x0

& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

Join, 1068, 1024

1070 ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x0

& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

Join, 1069, 1067

As Required:

1071 ALL(x0):[x0 e n

=> EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x0

& ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]

4 Conclusion, 11