1 ~p(a) Premise 2 r(g(a)) Premise 3 AX:(p(g(X)) => p(X)) Premise 4 AY:(r(g(g(Y))) <=> r(g(Y))) Premise 5 p(a) Assumption 6 r(g(a)) Reiteration 2 7 p(a) => r(g(a)) Implication Introduction 5 6 8 p(c) => r(g(c)) Assumption 9 p(g(c)) Assumption 10 p(g(c)) => p(c) Universal Elimination 3 11 p(c) Implication Elimination 10 9 12 r(g(c)) Implication Elimination 8 11 13 r(g(g(c))) <=> r(g(c)) Universal Elimination 4 14 r(g(c)) => r(g(g(c))) Biconditional Elimination 13 15 r(g(g(c))) Implication Elimination 14 12 16 p(g(c)) => r(g(g(c))) Implication Introduction 9 15 17 (p(c) => r(g(c))) => (p(g(c)) => r(g(g(c)))) Implication Introduction 8 16 18 AX:((p(X) => r(g(X))) => (p(g(X)) => r(g(g(X))))) Universal Introduction 17 19 AX:(p(X) => r(g(X))) Induction 7 18 1 ~p(a) Premise 2 r(g(a)) Premise 3 AX:(p(g(X)) => p(X)) Premise 4 AY:(r(g(g(Y))) => r(g(Y))) Premise 5 ~p(c) Assumption 6 p(g(c)) => p(c) Universal Elimination 3 7 p(g(c)) Assumption 8 ~p(c) Reiteration 5 9 p(g(c)) => ~p(c) Implication Introduction 7 8 10 ~p(g(c)) Negation Introduction 6 9 11 ~p(c) => ~p(g(c)) Implication Introduction 5 10 12 AX:(~p(X) => ~p(g(X))) Universal Introduction 11 13 AX:~p(X) Induction 1 12 14 p(c) Assumption 15 ~r(g(c)) Assumption 16 p(c) Reiteration 14 17 ~r(g(c)) => p(c) Implication Introduction 15 16 18 ~r(g(c)) Assumption 19 ~p(c) Universal Elimination 13 20 ~r(g(c)) => ~p(c) Implication Introduction 18 19 21 ~~r(g(c)) Negation Introduction 17 20 22 r(g(c)) Negation Elimination 21 23 p(c) => r(g(c)) Implication Introduction 14 22 24 AX:(p(X) => r(g(X))) Universal Introduction 23 1 EX:q(X) => EX:p(X) Premise 2 EX:~r(X) Premise 3 AX:(~q(X) => r(X)) Premise 4 ~r(c) Assumption 5 ~q(c) Assumption 6 ~r(c) Reiteration 4 7 ~q(c) => ~r(c) Implication Introduction 5 6 8 ~q(c) Assumption 9 ~q(c) => r(c) Universal Elimination 3 10 r(c) Implication Elimination 9 8 11 ~q(c) => r(c) Implication Introduction 8 10 12 ~~q(c) Negation Introduction 11 7 13 q(c) Negation Elimination 12 14 EX:q(X) Existential Introduction 13 15 ~r(c) => EX:q(X) Implication Introduction 4 14 16 AX:(~r(X) => EX:q(X)) Universal Introduction 15 17 EX:q(X) Existential Elimination 2 16 18 EX:p(X) Implication Elimination 1 17 1 EX:EY:(p(X) | p(Y)) Premise 2 EY:(p(c) | p(Y)) Assumption 3 p(c) | p(d) Assumption 4 p(c) Assumption 5 p(a) | p(c) Or Introduction 4 6 EY:(p(a) | p(Y)) Existential Introduction 5 7 p(c) => EY:(p(a) | p(Y)) Implication Introduction 4 6 8 p(d) Assumption 9 p(a) | p(d) Or Introduction 8 10 EY:(p(a) | p(Y)) Existential Introduction 9 11 p(d) => EY:(p(a) | p(Y)) Implication Introduction 8 10 12 EY:(p(a) | p(Y)) Or Elimination 3 7 11 13 p(c) | p(d) => EY:(p(a) | p(Y)) Implication Introduction 3 12 14 AY:(p(c) | p(Y) => EY:(p(a) | p(Y))) Universal Introduction 13 15 EY:(p(a) | p(Y)) Existential Elimination 2 14 16 EY:(p(c) | p(Y)) => EY:(p(a) | p(Y)) Implication Introduction 2 15 17 AX:(EY:(p(X) | p(Y)) => EY:(p(a) | p(Y))) Universal Introduction 16 18 EY:(p(a) | p(Y)) Existential Elimination 1 17 19 AX:EY:(p(X) | p(Y)) Universal Introduction 18 1 ~q Premise 2 ~p => (~q => ~r) Premise 3 s | r Premise 4 s => t Premise 5 p => t Premise 6 r Assumption 7 ~p Assumption 8 ~q => ~r Implication Elimination 2 7 9 ~r Implication Elimination 8 1 10 ~p => ~r Implication Introduction 7 9 11 ~p Assumption 12 r Reiteration 6 13 ~p => r Implication Introduction 11 12 14 ~~p Negation Introduction 13 10 15 p Negation Elimination 14 16 t Implication Elimination 5 15 17 r => t Implication Introduction 6 16 18 t Or Elimination 3 4 17 1 AX:s(X) | AX:r(X) Premise 2 AX:s(X) => t(c) Premise 3 AX:(r(X) => t(X)) Premise 4 AX:r(X) Assumption 5 r(c) Universal Elimination 4 6 r(c) => t(c) Universal Elimination 3 7 t(c) Implication Elimination 6 5 8 AX:r(X) => t(c) Implication Introduction 4 7 9 t(c) Or Elimination 1 2 8 10 EX:t(X) Existential Introduction 9 1 AX:AY:(p(X) => q(Y)) Premise 2 EX:p(X) Assumption 3 AY:(p(c) => q(Y)) Universal Elimination 1 4 p(c) => q([d]) Universal Elimination 3 5 p(c) Assumption 6 q([d]) Implication Elimination 4 5 7 AY:q(Y) Universal Introduction 6 8 p(c) => AY:q(Y) Implication Introduction 5 7 9 AX:(p(X) => AY:q(Y)) Universal Introduction 8 10 AY:q(Y) Existential Elimination 2 9 11 EX:p(X) => AY:q(Y) Implication Introduction 2 10 1 AX:(zero(X) => pos(t(X)) | neg(t(X))) Premise 2 AX:(pos(X) => zero(t(X))) Premise 3 AX:(neg(X) => zero(t(X))) Premise 4 zero([c]) Assumption 5 zero([c]) => pos(t([c])) | neg(t([c])) Universal Elimination 1 6 pos(t([c])) | neg(t([c])) Implication Elimination 5 4 7 pos(t([c])) => zero(t(t([c]))) Universal Elimination 2 8 neg(t([c])) => zero(t(t([c]))) Universal Elimination 3 9 zero(t(t([c]))) Or Elimination 6 7 8 10 zero([c]) => zero(t(t([c]))) Implication Introduction 4 9 11 AX:(zero(X) => zero(t(t(X)))) Universal Introduction 10 1 p(a,b) Premise 2 p(b,c) Premise 3 p(c,a) Premise 4 EY:p(a,Y) Existential Introduction 1 5 EY:p(b,Y) Existential Introduction 2 6 EY:p(c,Y) Existential Introduction 3 7 AX:EY:p(X,Y) Domain Closure 4 5 6 1 p(a) Premise 2 AX:(p(X) => q(X) | r(X)) Premise 3 AX:(q(X) => p(s(X))) Premise 4 AX:(r(X) => p(s(X))) Premise 5 p(c) Assumption 6 p(c) => q(c) | r(c) Universal Elimination 2 7 q(c) | r(c) Implication Elimination 6 5 8 q(c) => p(s(c)) Universal Elimination 3 9 r(c) => p(s(c)) Universal Elimination 4 10 p(s(c)) Or Elimination 7 8 9 11 p(c) => p(s(c)) Implication Introduction 5 10 12 AX:(p(X) => p(s(X))) Universal Introduction 11 13 AX:p(X) Induction 1 12 1 p(a) Premise 2 AX:(p(f(X)) <=> p(g(X))) Premise 3 AX:(p(X) => p(f(X)) | p(g(X))) Premise 4 p(f(c)) <=> p(g(c)) Universal Elimination 2 5 p(f(c)) => p(g(c)) Biconditional Elimination 4 6 p(g(c)) => p(f(c)) Biconditional Elimination 4 7 p(c) => p(f(c)) | p(g(c)) Universal Elimination 3 8 p(c) Assumption 9 p(f(c)) | p(g(c)) Implication Elimination 7 8 10 p(f(c)) Assumption 11 p(f(c)) => p(f(c)) Implication Introduction 10 10 12 p(f(c)) Or Elimination 9 11 6 13 p(c) => p(f(c)) Implication Introduction 8 12 14 AX:(p(X) => p(f(X))) Universal Introduction 13 15 p(c) Assumption 16 p(f(c)) | p(g(c)) Implication Elimination 7 15 17 p(g(c)) Assumption 18 p(g(c)) => p(g(c)) Implication Introduction 17 17 19 p(g(c)) Or Elimination 16 5 18 20 p(c) => p(g(c)) Implication Introduction 15 19 21 AX:(p(X) => p(g(X))) Universal Introduction 20 22 AX:p(X) Induction 1 14 21 1 p(a) Premise 2 AX:AY:(p(X) & p(Y) => r(X,Y)) Premise 3 AX:AY:(r(X,Y) => p(h(Y,X))) Premise 4 p(c) & p(d) Assumption 5 p(c) And Elimination 4 6 p(d) And Elimination 4 7 p(d) & p(c) And Introduction 6 5 8 AY:(p(d) & p(Y) => r(d,Y)) Universal Elimination 2 9 p(d) & p(c) => r(d,c) Universal Elimination 8 10 r(d,c) Implication Elimination 9 7 11 AY:(r(d,Y) => p(h(Y,d))) Universal Elimination 3 12 r(d,c) => p(h(c,d)) Universal Elimination 11 13 p(h(c,d)) Implication Elimination 12 10 14 p(c) & p(d) => p(h(c,d)) Implication Introduction 4 13 15 AY:(p(c) & p(Y) => p(h(c,Y))) Universal Introduction 14 16 AX:AY:(p(X) & p(Y) => p(h(X,Y))) Universal Introduction 15 17 AX:p(X) Induction 1 16 1 s & t | ~s & ~t Premise 2 s & t Assumption 3 s Assumption 4 t And Elimination 2 5 s => t Implication Introduction 3 4 6 s & t => (s => t) Implication Introduction 2 5 7 ~s & ~t Assumption 8 s Assumption 9 ~t Assumption 10 s Reiteration 8 11 ~t => s Implication Introduction 9 10 12 ~t Assumption 13 ~s And Elimination 7 14 ~t => ~s Implication Introduction 12 13 15 ~~t Negation Introduction 11 14 16 t Negation Elimination 15 17 s => t Implication Introduction 8 16 18 ~s & ~t => (s => t) Implication Introduction 7 17 19 s => t Or Elimination 1 6 18 1 AX:AY:AZ:(r(X,Y) & r(Y,Z) => r(X,Z)) Premise 2 AX:~r(X,X) Premise 3 r(c,d) Assumption 4 r(d,c) Assumption 5 AY:AZ:(r(c,Y) & r(Y,Z) => r(c,Z)) Universal Elimination 1 6 AZ:(r(c,d) & r(d,Z) => r(c,Z)) Universal Elimination 5 7 r(c,d) & r(d,c) => r(c,c) Universal Elimination 6 8 r(c,d) & r(d,c) And Introduction 3 4 9 r(c,c) Implication Elimination 7 8 10 r(d,c) => r(c,c) Implication Introduction 4 9 11 r(d,c) Assumption 12 ~r(c,c) Universal Elimination 2 13 r(d,c) => ~r(c,c) Implication Introduction 11 12 14 ~r(d,c) Negation Introduction 10 13 15 r(c,d) => ~r(d,c) Implication Introduction 3 14 16 AY:(r(c,Y) => ~r(Y,c)) Universal Introduction 15 17 AX:AY:(r(X,Y) => ~r(Y,X)) Universal Introduction 16 1 AX:(p(X) => ~EY:q(Y)) Premise 2 EX:p(X) => AX:q(X) Premise 3 EX:p(X) Assumption 4 AX:q(X) Implication Elimination 2 3 5 q(c) Universal Elimination 4 6 EY:q(Y) Existential Introduction 5 7 EX:p(X) => EY:q(Y) Implication Introduction 3 6 8 EX:p(X) Assumption 9 ~EY:q(Y) Existential Elimination 8 1 10 EX:p(X) => ~EY:q(Y) Implication Introduction 8 9 11 ~EX:p(X) Negation Introduction 7 10 1 ~p(a) Premise 2 q(b) Premise 3 p(a) Assumption 4 ~q(a) Assumption 5 p(a) Reiteration 3 6 ~q(a) => p(a) Implication Introduction 4 5 7 ~q(a) Assumption 8 ~p(a) Reiteration 1 9 ~q(a) => ~p(a) Implication Introduction 7 8 10 ~~q(a) Negation Introduction 6 9 11 q(a) Negation Elimination 10 12 p(a) => q(a) Implication Introduction 3 11 13 p(b) Assumption 14 q(b) Reiteration 2 15 p(b) => q(b) Implication Introduction 13 14 16 AX:(p(X) => q(X)) Domain Closure 12 15 1 p(a) Premise 2 AX:(p(X) & p(s(X)) | ~p(X) & ~p(s(X))) Premise 3 p(c) & p(s(c)) | ~p(c) & ~p(s(c)) Universal Elimination 2 4 p(c) Assumption 5 p(c) & p(s(c)) Assumption 6 p(s(c)) And Elimination 5 7 p(c) & p(s(c)) => p(s(c)) Implication Introduction 5 6 8 ~p(c) & ~p(s(c)) Assumption 9 ~p(c) And Elimination 8 10 ~p(s(c)) Assumption 11 p(c) Reiteration 4 12 ~p(s(c)) => p(c) Implication Introduction 10 11 13 ~p(s(c)) Assumption 14 ~p(c) Reiteration 9 15 ~p(s(c)) => ~p(c) Implication Introduction 13 14 16 ~~p(s(c)) Negation Introduction 12 15 17 p(s(c)) Negation Elimination 16 18 ~p(c) & ~p(s(c)) => p(s(c)) Implication Introduction 8 17 19 p(s(c)) Or Elimination 3 7 18 20 p(c) => p(s(c)) Implication Introduction 4 19 21 AX:(p(X) => p(s(X))) Universal Introduction 20 22 AX:p(X) Induction 1 21 1 p(a) Premise 2 AX:(p(X) => p(f(X))) Premise 3 AX:(p(f(f(X))) => p(g(X))) Premise 4 p(c) Assumption 5 p(c) => p(f(c)) Universal Elimination 2 6 p(f(c)) Implication Elimination 5 4 7 p(f(c)) => p(f(f(c))) Universal Elimination 2 8 p(f(f(c))) Implication Elimination 7 6 9 p(f(f(c))) => p(g(c)) Universal Elimination 3 10 p(g(c)) Implication Elimination 9 8 11 p(c) => p(g(c)) Implication Introduction 4 10 12 AX:(p(X) => p(g(X))) Universal Introduction 11 13 AX:p(X) Induction 1 2 12 1 p(a) Premise 2 AX:(p(X) => q(X)) Premise 3 AX:AY:(p(X) & q(Y) => p(h(X,Y))) Premise 4 p(c) & p(d) Assumption 5 p(c) And Elimination 4 6 p(d) And Elimination 4 7 p(d) => q(d) Universal Elimination 2 8 q(d) Implication Elimination 7 6 9 p(c) & q(d) And Introduction 5 8 10 AY:(p(c) & q(Y) => p(h(c,Y))) Universal Elimination 3 11 p(c) & q(d) => p(h(c,d)) Universal Elimination 10 12 p(h(c,d)) Implication Elimination 11 9 13 p(c) & p(d) => p(h(c,d)) Implication Introduction 4 12 14 AY:(p(c) & p(Y) => p(h(c,Y))) Universal Introduction 13 15 AX:AY:(p(X) & p(Y) => p(h(X,Y))) Universal Introduction 14 16 AX:p(X) Induction 1 15 1 ~p | ~q Premise 2 ~p Assumption 3 p & q Assumption 4 p And Elimination 3 5 p & q => p Implication Introduction 3 4 6 p & q Assumption 7 ~p Reiteration 2 8 p & q => ~p Implication Introduction 6 7 9 ~(p & q) Negation Introduction 5 8 10 ~p => ~(p & q) Implication Introduction 2 9 11 ~q Assumption 12 p & q Assumption 13 q And Elimination 12 14 p & q => q Implication Introduction 12 13 15 p & q Assumption 16 ~q Reiteration 11 17 p & q => ~q Implication Introduction 15 16 18 ~(p & q) Negation Introduction 14 17 19 ~q => ~(p & q) Implication Introduction 11 18 20 ~(p & q) Or Elimination 1 10 19 1 AX:AY:(~p(X,Y) => p(Y,X)) Premise 2 ~p(c,c) Assumption 3 ~p(c,c) => ~p(c,c) Implication Introduction 2 2 4 AY:(~p(c,Y) => p(Y,c)) Universal Elimination 1 5 ~p(c,c) => p(c,c) Universal Elimination 4 6 ~~p(c,c) Negation Introduction 5 3 7 p(c,c) Negation Elimination 6 8 AX:p(X,X) Universal Introduction 7 1 AX:(p(X) => q(X)) Premise 2 EX:~q(X) Premise 3 ~q(c) Assumption 4 p(c) Assumption 5 ~q(c) Reiteration 3 6 p(c) => ~q(c) Implication Introduction 4 5 7 p(c) => q(c) Universal Elimination 1 8 ~p(c) Negation Introduction 7 6 9 EX:~p(X) Existential Introduction 8 10 ~q(c) => EX:~p(X) Implication Introduction 3 9 11 AX:(~q(X) => EX:~p(X)) Universal Introduction 10 12 EX:~p(X) Existential Elimination 2 11 1 AX:(p(X) | q(X)) Premise 2 AX:(p(X) => q(s(X))) Premise 3 AX:(q(X) => p(s(X))) Premise 4 p(c) | q(c) Universal Elimination 1 5 p(c) Assumption 6 p(c) => q(s(c)) Universal Elimination 2 7 q(s(c)) Implication Elimination 6 5 8 q(c) | q(s(c)) Or Introduction 7 9 p(c) => q(c) | q(s(c)) Implication Introduction 5 8 10 q(c) Assumption 11 q(c) | q(s(c)) Or Introduction 10 12 q(c) => q(c) | q(s(c)) Implication Introduction 10 11 13 q(c) | q(s(c)) Or Elimination 4 9 12 14 AX:(q(X) | q(s(X))) Universal Introduction 13 1 p(a) Premise 2 AX:(p(X) => p(s(X)) | q(s(X))) Premise 3 AX:(q(X) => p(s(X)) | q(s(X))) Premise 4 p(a) | q(a) Or Introduction 1 5 p(c) | q(c) Assumption 6 p(c) => p(s(c)) | q(s(c)) Universal Elimination 2 7 q(c) => p(s(c)) | q(s(c)) Universal Elimination 3 8 p(s(c)) | q(s(c)) Or Elimination 5 6 7 9 p(c) | q(c) => p(s(c)) | q(s(c)) Implication Introduction 5 8 10 AX:(p(X) | q(X) => p(s(X)) | q(s(X))) Universal Introduction 9 11 AX:(p(X) | q(X)) Induction 4 10 1 p(a) Premise 2 q(a) Premise 3 AX:(p(X) | q(X) => p(f(X))) Premise 4 AX:(p(X) | q(X) => q(g(X))) Premise 5 p(a) | q(a) Or Introduction 1 6 p(c) | q(c) Assumption 7 p(c) | q(c) => p(f(c)) Universal Elimination 3 8 p(f(c)) Implication Elimination 7 6 9 p(f(c)) | q(f(c)) Or Introduction 8 10 p(c) | q(c) => p(f(c)) | q(f(c)) Implication Introduction 6 9 11 AX:(p(X) | q(X) => p(f(X)) | q(f(X))) Universal Introduction 10 12 p(c) | q(c) Assumption 13 p(c) | q(c) => q(g(c)) Universal Elimination 4 14 q(g(c)) Implication Elimination 13 12 15 p(g(c)) | q(g(c)) Or Introduction 14 16 p(c) | q(c) => p(g(c)) | q(g(c)) Implication Introduction 12 15 17 AX:(p(X) | q(X) => p(g(X)) | q(g(X))) Universal Introduction 16 18 AX:(p(X) | q(X)) Induction 5 11 17 1 p(a) & p(b) Premise 2 AX:AY:(p(X) => (p(Y) => p(h(X,Y)))) Premise 3 p(a) And Elimination 1 4 p(b) And Elimination 1 5 p(c) & p(d) Assumption 6 p(c) And Elimination 5 7 p(d) And Elimination 5 8 AY:(p(c) => (p(Y) => p(h(c,Y)))) Universal Elimination 2 9 p(c) => (p(d) => p(h(c,d))) Universal Elimination 8 10 p(d) => p(h(c,d)) Implication Elimination 9 6 11 p(h(c,d)) Implication Elimination 10 7 12 p(c) & p(d) => p(h(c,d)) Implication Introduction 5 11 13 AY:(p(c) & p(Y) => p(h(c,Y))) Universal Introduction 12 14 AX:AY:(p(X) & p(Y) => p(h(X,Y))) Universal Introduction 13 15 AX:p(X) Induction 3 4 14 1 f(0)=0 Premise 2 AX:f(X+1)=f(X)+2 Premise 3 0=2*0 Equation 4 f(0)=2*0 Equality Elimination 3 1 5 f(c)=2*c Assumption 6 f(c+1)=f(c)+2 Universal Elimination 2 7 f(c+1)=2*c+2 Equality Elimination 5 6 8 2*(c+1)=2*c+2 Equation 9 f(c+1)=2*(c+1) Equality Elimination 8 7 10 f(c)=2*c => f(c+1)=2*(c+1) Implication Introduction 5 9 11 AX:(f(X)=2*X => f(X+1)=2*(X+1)) Universal Introduction 10 12 AX:f(X)=2*X Rational Induction 1 ~p | q Premise 2 p Assumption 3 q Assumption 4 q => q Implication Introduction 3 3 5 ~p Assumption 6 ~q Assumption 7 p Reiteration 2 8 ~q => p Implication Introduction 6 7 9 ~q Assumption 10 ~p Reiteration 5 11 ~q => ~p Implication Introduction 9 10 12 ~~q Negation Introduction 8 11 13 q Negation Elimination 12 14 ~p => q Implication Introduction 5 13 15 q Or Elimination 1 14 4 16 p => q Implication Introduction 2 15 1 AX:AY:(p(X,Y) => p(Y,X)) Premise 2 AX:AY:AZ:(p(X,Y) & p(Y,Z) => p(X,Z)) Premise 3 AX:~p(X,X) Premise 4 p(c,d) Assumption 5 AY:(p(c,Y) => p(Y,c)) Universal Elimination 1 6 p(c,d) => p(d,c) Universal Elimination 5 7 p(d,c) Implication Elimination 6 4 8 p(c,d) & p(d,c) And Introduction 4 7 9 AY:AZ:(p(c,Y) & p(Y,Z) => p(c,Z)) Universal Elimination 2 10 AZ:(p(c,d) & p(d,Z) => p(c,Z)) Universal Elimination 9 11 p(c,d) & p(d,c) => p(c,c) Universal Elimination 10 12 p(c,c) Implication Elimination 11 8 13 p(c,d) => p(c,c) Implication Introduction 4 12 14 p(c,d) Assumption 15 ~p(c,c) Universal Elimination 3 16 p(c,d) => ~p(c,c) Implication Introduction 14 15 17 ~p(c,d) Negation Introduction 13 16 18 AY:~p(c,Y) Universal Introduction 17 19 AX:AY:~p(X,Y) Universal Introduction 18 1 EX:(p(X) | q(X)) Premise 2 AX:(p(X) => r(X)) Premise 3 AX:(q(X) => r(X)) Premise 4 p(c) | q(c) Assumption 5 p(c) => r(c) Universal Elimination 2 6 q(c) => r(c) Universal Elimination 3 7 r(c) Or Elimination 4 5 6 8 EX:r(X) Existential Introduction 7 9 p(c) | q(c) => EX:r(X) Implication Introduction 4 8 10 AX:(p(X) | q(X) => EX:r(X)) Universal Introduction 9 11 EX:r(X) Existential Elimination 1 10 1 AX:X+0=X Premise 2 AX:AY:X+s(Y)=s(X+Y) Premise 3 even(0) Premise 4 AX:(even(X) => odd(s(X))) Premise 5 AX:(odd(X) => even(s(X))) Premise 6 AY:s(0)+s(Y)=s(s(0)+Y) Universal Elimination 2 7 s(0)+s(0)=s(s(0)+0) Universal Elimination 6 8 s(0)+0=s(0) Universal Elimination 1 9 s(0)+s(0)=s(s(0)) Equality Elimination 8 7 10 even(0) => odd(s(0)) Universal Elimination 4 11 odd(s(0)) Implication Elimination 10 3 12 odd(s(0)) => even(s(s(0))) Universal Elimination 5 13 even(s(s(0))) Implication Elimination 12 11 14 even(s(0)+s(0)) Equality Elimination 9 13 1 AX:r(X,X) Premise 2 AX:r(X,s(X)) Premise 3 AX:AY:AZ:(r(X,Y) & r(Y,Z) => r(X,Z)) Premise 4 r(0,0) Universal Elimination 1 5 r(0,c) Assumption 6 r(c,s(c)) Universal Elimination 2 7 AY:AZ:(r(0,Y) & r(Y,Z) => r(0,Z)) Universal Elimination 3 8 AZ:(r(0,c) & r(c,Z) => r(0,Z)) Universal Elimination 7 9 r(0,c) & r(c,s(c)) => r(0,s(c)) Universal Elimination 8 10 r(0,c) & r(c,s(c)) And Introduction 5 6 11 r(0,s(c)) Implication Elimination 9 10 12 r(0,c) => r(0,s(c)) Implication Introduction 5 11 13 AX:(r(0,X) => r(0,s(X))) Universal Introduction 12 14 AX:r(0,X) Induction 4 13 1 p(a) Premise 2 AX:(p(X) => p(f(f(X)))) Premise 3 AX:(p(f(X)) => p(g(X))) Premise 4 AX:(p(g(X)) => p(X)) Premise 5 p(c) Assumption 6 p(c) => p(f(f(c))) Universal Elimination 2 7 p(f(f(c))) Implication Elimination 6 5 8 p(f(f(c))) => p(g(f(c))) Universal Elimination 3 9 p(g(f(c))) Implication Elimination 8 7 10 p(g(f(c))) => p(f(c)) Universal Elimination 4 11 p(f(c)) Implication Elimination 10 9 12 p(c) => p(f(c)) Implication Introduction 5 11 13 AX:(p(X) => p(f(X))) Universal Introduction 12 14 p(c) Assumption 15 p(f(c)) Implication Elimination 12 14 16 p(f(c)) => p(g(c)) Universal Elimination 3 17 p(g(c)) Implication Elimination 16 15 18 p(c) => p(g(c)) Implication Introduction 14 17 19 AX:(p(X) => p(g(X))) Universal Introduction 18 20 AX:p(X) Induction 1 13 19 1 f(0,0)=0 Premise 2 f(1,0)=1 Premise 3 AX:AY:AZ:f(f(X,Y),Z)=f(X,f(Y,Z)) Premise 4 f(c,0)=c & f(d,0)=d Assumption 5 f(c,0)=c And Elimination 4 6 f(d,0)=d And Elimination 4 7 AY:AZ:f(f(c,Y),Z)=f(c,f(Y,Z)) Universal Elimination 3 8 AZ:f(f(c,d),Z)=f(c,f(d,Z)) Universal Elimination 7 9 f(f(c,d),0)=f(c,f(d,0)) Universal Elimination 8 10 f(f(c,d),0)=f(c,d) Equality Elimination 6 9 11 f(c,0)=c & f(d,0)=d => f(f(c,d),0)=f(c,d) Implication Introduction 4 10 12 AY:(f(c,0)=c & f(Y,0)=Y => f(f(c,Y),0)=f(c,Y)) Universal Introduction 11 13 AX:AY:(f(X,0)=X & f(Y,0)=Y => f(f(X,Y),0)=f(X,Y)) Universal Introduction 12 14 AX:f(X,0)=X Induction 1 2 13 1 f(0)=0 Premise 2 AX:f(X+1)=f(X)+(2*X+1) Premise 3 0=0*0 Equation 4 f(0)=0*0 Equality Elimination 3 1 5 f(c)=c*c Assumption 6 f(c+1)=f(c)+(2*c+1) Universal Elimination 2 7 f(c+1)=c*c+(2*c+1) Equality Elimination 5 6 8 (c+1)*(c+1)=c*c+(2*c+1) Equation 9 f(c+1)=(c+1)*(c+1) Equality Elimination 8 7 10 f(c)=c*c => f(c+1)=(c+1)*(c+1) Implication Introduction 5 9 11 AX:(f(X)=X*X => f(X+1)=(X+1)*(X+1)) Universal Introduction 10 12 AX:f(X)=X*X Rational Induction 1 p => q Premise 2 q => r Assumption 3 p Assumption 4 q Implication Elimination 1 3 5 r Implication Elimination 2 4 6 p => r Implication Introduction 3 5 7 (q => r) => (p => r) Implication Introduction 2 6 1 q => r Premise 2 p => q Assumption 3 p Assumption 4 q Implication Elimination 2 3 5 r Implication Elimination 1 4 6 p => r Implication Introduction 3 5 7 (p => q) => (p => r) Implication Introduction 2 6 1 p => (q => r) Premise 2 q Assumption 3 p Assumption 4 q => r Implication Elimination 1 3 5 r Implication Elimination 4 2 6 p => r Implication Introduction 3 5 7 q => (p => r) Implication Introduction 2 6 1 p => (q => r) Premise 2 p => q Premise 3 p Assumption 4 q => r Implication Elimination 1 3 5 q Implication Elimination 2 3 6 r Implication Elimination 4 5 7 p => r Implication Introduction 3 6 1 p => q Premise 2 p => ~q Premise 3 ~p Negation Introduction 1 2 c 1 p Premise 2 q Premise 3 p & q => r Premise 4 p & q And Introduction 1 2 5 r Implication Elimination 3 4 1 p & q Premise 2 p And Elimination 1 3 q And Elimination 1 4 q | r Or Introduction 3 1 p => q Premise 2 q <=> r Premise 3 q => r Biconditional Elimination 2 4 r => q Biconditional Elimination 2 5 p Assumption 6 q Implication Elimination 1 5 7 r Implication Elimination 3 6 8 p => r Implication Introduction 5 7 1 p => q Premise 2 m => p | q Premise 3 m Assumption 4 p | q Implication Elimination 2 3 5 q Assumption 6 q => q Implication Introduction 5 5 7 q Or Elimination 4 1 6 8 m => q Implication Introduction 3 7 1 p => q => r Premise 2 p => q Assumption 3 p Assumption 4 q Implication Elimination 2 3 5 q => r Implication Elimination 1 3 6 r Implication Elimination 5 4 7 p => r Implication Introduction 3 6 8 (p => q) => p => r Implication Introduction 2 7 1 p Assumption 2 q Assumption 3 p Reiteration 1 4 q => p Implication Introduction 2 3 5 p => q => p Implication Introduction 1 4 1 p => q => r Assumption 2 p => q Assumption 3 p Assumption 4 q => r Implication Elimination 1 3 5 q Implication Elimination 2 3 6 r Implication Elimination 4 5 7 p => r Implication Introduction 3 6 8 (p => q) => p => r Implication Introduction 2 7 9 (p => q => r) => (p => q) => p => r Implication Introduction 1 8 1 ~p => q Assumption 2 ~p => ~q Assumption 3 ~~p Negation Introduction 1 2 4 p Negation Elimination 3 5 (~p => ~q) => p Implication Introduction 2 4 6 (~p => q) => (~p => ~q) => p Implication Introduction 1 5 1 p Premise 2 ~p Assumption 3 p Reiteration 4 ~p => p Implication Introduction 2 3 5 ~p Assumption 6 ~p => ~p Implication Introduction 5 5 7 ~~p Negation Introduction 4 6 1 p => q Premise 2 ~q Assumption 3 p Assumption 4 ~q Reiteration 2 5 p => ~q Implication Introduction 3 4 6 ~p Negation Introduction 1 5 7 ~q => ~p Implication Introduction 2 6 1 p => q Premise 2 ~(~p | q) Assumption 3 p Assumption 4 q Implication Elimination 1 3 5 ~p | q Or Introduction 4 6 p => ~p | q Implication Introduction 3 5 7 p Assumption 8 ~(~p | q) Reiteration 2 9 p => ~(~p | q) Implication Introduction 7 8 10 ~p Negation Introduction 6 9 11 ~(~p | q) => ~p Implication Introduction 2 10 12 ~(~p | q) Assumption 13 ~p Assumption 14 ~p | q Or Introduction 13 15 ~p => ~p | q Implication Introduction 13 14 16 ~p Assumption 17 ~(~p | q) Reiteration 12 18 ~p => ~(~p | q) Implication Introduction 16 17 19 ~~p Negation Introduction 15 18 20 ~(~p | q) => ~~p Implication Introduction 12 19 21 ~~(~p | q) Negation Introduction 11 20 22 ~p | q Negation Elimination 21 1 (p => q) => p Assumption 2 ~p Assumption 3 p Assumption 4 ~q Assumption 5 p Reiteration 3 6 ~q => p Implication Introduction 4 5 7 ~q Assumption 8 ~p Reiteration 2 9 ~q => ~p Implication Introduction 7 8 10 ~~q Negation Introduction 6 9 11 q Negation Elimination 10 12 p => q Implication Introduction 3 11 13 ~p => p => q Implication Introduction 12 14 ~p Assumption 15 p => q Assumption 16 ~p Reiteration 14 17 (p => q) => ~p Implication Introduction 15 16 18 ~(p => q) Negation Introduction 1 17 19 ~p => ~(p => q) Implication Introduction 14 18 20 ~~p Negation Introduction 13 19 21 p Negation Elimination 20 22 ((p => q) => p) => p Implication Introduction 1 21 1 ~(p | q) Premise 2 p Assumption 3 p | q Or Introduction 2 4 p => p | q Implication Introduction 2 3 5 p Assumption 6 ~(p | q) Reiteration 1 7 p => ~(p | q) Implication Introduction 5 6 8 ~p Negation Introduction 4 7 9 q Assumption 10 p | q Or Introduction 9 11 q => p | q Implication Introduction 9 10 12 q Assumption 13 ~(p | q) Reiteration 1 14 q => ~(p | q) Implication Introduction 12 13 15 ~q Negation Introduction 11 14 16 ~p & ~q And Introduction 8 15 1 ~(p | ~p) Assumption 2 p Assumption 3 p | ~p Or Introduction 2 4 p => p | ~p Implication Introduction 2 3 5 p Assumption 6 ~(p | ~p) Reiteration 1 7 p => ~(p | ~p) Implication Introduction 5 6 8 ~p Negation Introduction 4 7 9 ~(p | ~p) => ~p Implication Introduction 1 8 10 ~(p | ~p) Assumption 11 ~p Assumption 12 p | ~p Or Introduction 11 13 ~p => p | ~p Implication Introduction 11 12 14 ~p Assumption 15 ~(p | ~p) Reiteration 10 16 ~p => ~(p | ~p) Implication Introduction 14 15 17 ~~p Negation Introduction 13 16 18 ~(p | ~p) => ~~p Implication Introduction 10 17 19 ~~(p | ~p) Negation Introduction 9 18 20 p | ~p Negation Elimination 19 1 AX:(p(X) & q(X)) Premise 2 p(c) & q(c) Universal Elimination 1 3 p(c) And Elimination 2 4 q(c) And Elimination 2 5 AX:p(X) Universal Introduction 3 6 AX:q(X) Universal Introduction 4 7 AX:p(X) & AX:q(X) And Introduction 5 6 1 AX:(p(X) => q(X)) Premise 2 AX:p(X) Assumption 3 p(c) Universal Elimination 2 4 p(c) => q(c) Universal Elimination 1 5 q(c) Implication Elimination 4 3 6 AX:q(X) Universal Introduction 5 7 AX:p(X) => AX:q(X) Implication Introduction 2 6 1 AX:(p(X) => q(X)) Premise 2 AX:(q(X) => r(X)) Premise 3 p(c) Assumption 4 p(c) => q(c) Universal Elimination 1 5 q(c) Implication Elimination 4 3 6 q(c) => r(c) Universal Elimination 2 7 r(c) Implication Elimination 6 5 8 p(c) => r(c) Implication Introduction 3 7 9 AX:(p(X) => r(X)) Universal Introduction 8 1 AX:AY:p(X,Y) Premise 2 AY:p(c,Y) Universal Elimination 1 3 p(c,d) Universal Elimination 2 4 AX:p(X,d) Universal Introduction 3 5 AY:AX:p(X,Y) Universal Introduction 4 1 AX:AY:p(X,Y) Premise 2 AY:p(c,Y) Universal Elimination 1 3 p(c,d) Universal Elimination 2 4 AY:p(Y,d) Universal Introduction 3 5 AX:AY:p(Y,X) Universal Introduction 4 1 EY:AX:p(X,Y) Premise 2 AX:p(X,d) Assumption 3 p(c,d) Universal Elimination 2 4 EY:p(c,Y) Existential Introduction 3 5 AX:p(X,d) => EY:p(c,Y) Implication Introduction 2 4 6 AY:(AX:p(X,Y) => EY:p(c,Y)) Universal Introduction 5 7 EY:p(c,Y) Existential Elimination 1 6 8 AX:EY:p(X,Y) Universal Introduction 7 1 EX:~p(X) Premise 2 ~p(c) Assumption 3 AX:p(X) Assumption 4 ~p(c) Reiteration 2 5 AX:p(X) => ~p(c) Implication Introduction 3 4 6 AX:p(X) Assumption 7 p(c) Universal Elimination 6 8 AX:p(X) => p(c) Implication Introduction 6 7 9 ~AX:p(X) Negation Introduction 8 5 10 ~p(c) => ~AX:p(X) Implication Introduction 2 9 11 AX:(~p(X) => ~AX:p(X)) Universal Introduction 10 12 ~AX:p(X) Existential Elimination 1 11 1 AX:~p(X) Premise 2 EX:p(X) Assumption 3 AX:~p(X) Reiteration 1 4 EX:p(X) => AX:~p(X) Implication Introduction 2 3 5 EX:p(X) Assumption 6 p(c) Assumption 7 AX:~p(X) Assumption 8 p(c) Reiteration 6 9 AX:~p(X) => p(c) Implication Introduction 7 8 10 AX:~p(X) Assumption 11 ~p(c) Universal Elimination 10 12 AX:~p(X) => ~p(c) Implication Introduction 10 11 13 ~AX:~p(X) Negation Introduction 9 12 14 p(c) => ~AX:~p(X) Implication Introduction 6 13 15 AX:(p(X) => ~AX:~p(X)) Universal Introduction 14 16 ~AX:~p(X) Existential Elimination 5 15 17 EX:p(X) => ~AX:~p(X) Implication Introduction 5 16 18 ~EX:p(X) Negation Introduction 4 17 1 ~EX:p(X) Premise 2 p(c) Assumption 3 EX:p(X) Existential Introduction 2 4 p(c) => EX:p(X) Implication Introduction 2 3 5 p(c) Assumption 6 ~EX:p(X) Reiteration 1 7 p(c) => ~EX:p(X) Implication Introduction 5 6 8 ~p(c) Negation Introduction 4 7 9 AX:~p(X) Universal Introduction 9 1 ~AX:p(X) Premise 2 ~EX:~p(X) Assumption 3 ~p(c) Assumption 4 EX:~p(X) Existential Introduction 3 5 ~p(c) => EX:~p(X) Implication Introduction 3 4 6 ~p(c) Assumption 7 ~EX:~p(X) Reiteration 2 8 ~p(c) => ~EX:~p(X) Implication Introduction 6 7 9 ~~p(c) Negation Introduction 5 8 10 p(c) Negation Elimination 9 11 AX:p(X) Universal Introduction 10 12 ~EX:~p(X) => AX:p(X) Implication Introduction 2 11 13 ~EX:~p(X) Assumption 14 ~AX:p(X) Reiteration 1 15 ~EX:~p(X) => ~AX:p(X) Implication Introduction 13 14 16 ~~EX:~p(X) Negation Introduction 12 15 17 EX:~p(X) Negation Elimination 16 1 AZ:(p(Z) => ~p(f(Z))) Premise 2 AZ:(~p(Z) => p(f(Z))) Premise 3 p(c) Assumption 4 p(c) => ~p(f(c)) Universal Elimination 1 5 ~p(f(c)) Implication Elimination 4 3 6 ~p(f(c)) => p(f(f(c))) Universal Elimination 2 7 p(f(f(c))) Implication Elimination 6 5 8 p(c) => p(f(f(c))) Implication Introduction 3 7 9 AZ:(p(Z) => p(f(f(Z)))) Universal Introduction 8 1 AZ:(p(Z) <=> q(f(Z))) Premise 2 AZ:(p(Z) <=> r(g(Z))) Premise 3 p(c) <=> q(f(c)) Universal Elimination 1 4 q(f(c)) => p(c) Biconditional Elimination 3 5 p(c) <=> r(g(c)) Universal Elimination 2 6 p(c) => r(g(c)) Biconditional Elimination 5 7 q(f(c)) Assumption 8 p(c) Implication Elimination 4 7 9 r(g(c)) Implication Elimination 6 8 10 q(f(c)) => r(g(c)) Implication Introduction 7 9 11 AZ:(q(f(Z)) => r(g(Z))) Universal Introduction 10 1 q(a) Premise 2 q(b) Premise 3 p(a) Assumption 4 q(a) Reiteration 1 5 p(a) => q(a) Implication Introduction 3 4 6 p(b) Assumption 7 q(b) Reiteration 2 8 p(b) => q(b) Implication Introduction 6 7 9 AX:(p(X) => q(X)) Domain Closure 5 8 1 r(a) Premise 2 AX:(p(X) => r(s(X))) Premise 3 AX:(q(X) => r(s(X))) Premise 4 AX:(r(X) => p(X) | q(X)) Premise 5 r(c) Assumption 6 p(c) => r(s(c)) Universal Elimination 2 7 q(c) => r(s(c)) Universal Elimination 3 8 r(c) => p(c) | q(c) Universal Elimination 4 9 p(c) | q(c) Implication Elimination 8 5 10 r(s(c)) Or Elimination 9 6 7 11 r(c) => r(s(c)) Implication Introduction 5 10 12 AX:(r(X) => r(s(X))) Universal Introduction 11 13 AX:r(X) Induction 1 12 1 p(a) Premise 2 AX:(p(X) => p(f(X))) Premise 3 AX:(p(f(X)) => p(g(X))) Premise 4 p(c) Assumption 5 p(c) => p(f(c)) Universal Elimination 2 6 p(f(c)) Implication Elimination 5 4 7 p(f(c)) => p(g(c)) Universal Elimination 3 8 p(g(c)) Implication Elimination 7 6 9 p(c) => p(g(c)) Implication Introduction 4 8 10 AX:(p(X) => p(g(X))) Universal Introduction 9 11 AX:p(X) Induction 1 2 10 1 p(a) Premise 2 AX:AY:(p(X) | p(Y) => p(h(X,Y))) Premise 3 p(c) & p(d) Assumption 4 p(c) And Elimination 3 5 p(c) | p(d) Or Introduction 4 6 AY:(p(c) | p(Y) => p(h(c,Y))) Universal Elimination 2 7 p(c) | p(d) => p(h(c,d)) Universal Elimination 6 8 p(h(c,d)) Implication Elimination 7 5 9 p(c) & p(d) => p(h(c,d)) Implication Introduction 3 8 10 AY:(p(c) & p(Y) => p(h(c,Y))) Universal Introduction 9 11 AX:AY:(p(X) & p(Y) => p(h(X,Y))) Universal Introduction 10 12 AX:p(X) Induction 1 11 1 p(a) Premise 2 AX:(p(X) => q(f(X))) Premise 3 AX:(q(X) => p(f(X))) Premise 4 p(a) | q(a) Or Introduction 1 5 p(c) | q(c) Assumption 6 p(c) Assumption 7 p(c) => q(f(c)) Universal Elimination 2 8 q(f(c)) Implication Elimination 7 6 9 p(f(c)) | q(f(c)) Or Introduction 8 10 p(c) => p(f(c)) | q(f(c)) Implication Introduction 6 9 11 q(c) Assumption 12 q(c) => p(f(c)) Universal Elimination 3 13 p(f(c)) Implication Elimination 12 11 14 p(f(c)) | q(f(c)) Or Introduction 13 15 q(c) => p(f(c)) | q(f(c)) Implication Introduction 11 14 16 p(f(c)) | q(f(c)) Or Elimination 5 10 15 17 p(c) | q(c) => p(f(c)) | q(f(c)) Implication Introduction 5 16 18 AX:(p(X) | q(X) => p(f(X)) | q(f(X))) Universal Introduction 17 19 AX:(p(X) | q(X)) Induction 4 18 1 p(a) Premise 2 p(s(a)) Premise 3 AX:(p(X) => p(s(s(X)))) Premise 4 p(a) & p(s(a)) And Introduction 1 2 5 p(c) & p(s(c)) Assumption 6 p(c) And Elimination 5 7 p(s(c)) And Elimination 5 8 p(c) => p(s(s(c))) Universal Elimination 3 9 p(s(s(c))) Implication Elimination 8 6 10 p(s(c)) & p(s(s(c))) And Introduction 7 9 11 p(c) & p(s(c)) => p(s(c)) & p(s(s(c))) Implication Introduction 5 10 12 AX:(p(X) & p(s(X)) => p(s(X)) & p(s(s(X)))) Universal Introduction 11 13 AX:(p(X) & p(s(X))) Induction 4 12 14 p(c) & p(s(c)) Universal Elimination 13 15 p(c) And Elimination 14 16 AX:p(X) Universal Introduction 15 1 AX:X=X Premise 2 AX:AY:(X=Y => Y=X) Premise 3 AX:AY:AZ:(X=Y & Y=Z => X=Z) Premise 4 a=b Premise 5 b=c Premise 6 AY:AZ:(a=Y & Y=Z => a=Z) Universal Elimination: 3 7 AZ:(a=b & b=Z => a=Z) Universal Elimination: 6 8 a=b & b=c => a=c Universal Elimination: 7 9 a=b & b=c And Introduction: 4, 5 10 a=c Implication Elimination: 8, 9 1 AX:X=X Premise 2 AX:AY:(X=Y => Y=X) Premise 3 AX:AY:AZ:(X=Y & Y=Z => X=Z) Premise 4 AX:AY:(p(X) & X=Y => p(Y)) Premise 5 a=b Premise 6 p(a) Premise 7 AY:(p(a) & a=Y => p(Y)) Universal Elimination: 4 8 p(a) & a=b => p(b) Universal Elimination: 7 9 p(a) & a=b And Introduction: 6, 5 10 p(b) Implication Elimination: 8, 9 1 AY:f(Y,0)=Y Premise 2 AX:AY:AZ:f(X,f(Y,Z))=f(f(X,Y),Z) Premise 3 f(0,0)=0 Universal Elimination 1 4 f(0,c)=c & f(0,d)=d Assumption 5 f(0,c)=c And Elimination 4 6 AY:AZ:f(0,f(Y,Z))=f(f(0,Y),Z) Universal Elimination 2 7 AZ:f(0,f(c,Z))=f(f(0,c),Z) Universal Elimination 6 8 f(0,f(c,d))=f(f(0,c),d) Universal Elimination 7 9 f(0,f(c,d))=f(c,d) Equality Elimination 8 5 10 f(0,c)=c & f(0,d)=d => f(0,f(c,d))=f(c,d) Implication Introduction 4 9 11 AY:(f(0,c)=c & f(0,Y)=Y => f(0,f(c,Y))=f(c,Y)) Universal Introduction 10 12 AX:AY:(f(0,X)=X & f(0,Y)=Y => f(0,f(X,Y))=f(X,Y)) Universal Introduction 11 13 AY:f(0,Y)=Y Induction 3 12 1 rev(a)=a Premise 2 rev(b)=b Premise 3 AX:AY:rev(cons(X,Y))=cons(rev(Y),rev(X)) Premise 4 rev(rev(a))=a Equality Elimination 1 1 5 rev(rev(b))=b Equality Elimination 2 2 6 rev(rev(c))=c & rev(rev(d))=d Assumption 7 rev(rev(cons(c,d)))=rev(rev(cons(c,d))) Equality Introduction 8 AY:rev(cons(c,Y))=cons(rev(Y),rev(c)) Universal Elimination 3 9 rev(cons(c,d))=cons(rev(d),rev(c)) Universal Elimination 8 10 rev(rev(cons(c,d)))=rev(cons(rev(d),rev(c))) Equality Elimination 7 9 11 AY:rev(cons(rev(d),Y))=cons(rev(Y),rev(rev(d))) Universal Elimination 3 12 rev(cons(rev(d),rev(c)))=cons(rev(rev(c)),rev(rev(d))) Universal Elimination 11 13 rev(rev(cons(c,d)))=cons(rev(rev(c)),rev(rev(d))) Equality Elimination 12 10 14 rev(rev(c))=c And Elimination 6 15 rev(rev(d))=d And Elimination 6 16 rev(rev(cons(c,d)))=cons(c,rev(rev(d))) Equality Elimination 13 14 17 rev(rev(cons(c,d)))=cons(c,d) Equality Elimination 16 15 18 rev(rev(c))=c & rev(rev(d))=d => rev(rev(cons(c,d)))=cons(c,d) Implication Introduction 6 17 19 AY:(rev(rev(c))=c & rev(rev(Y))=Y => rev(rev(cons(c,Y)))=cons(c,Y)) Universal Introduction 18 20 AX:AY:(rev(rev(X))=X & rev(rev(Y))=Y => rev(rev(cons(X,Y)))=cons(X,Y)) Universal Introduction 19 21 AX:rev(rev(X))=X Induction 4 5 20 1 f(0)=0 Premise 2 AZ:f(Z+1)=f(Z)+((Z+1)+(Z+1)) Premise 3 0*(0+1)=0 Rational Equation 4 f(0)=0*(0+1) QE: 1, 3 5 f(c)=c*(c+1) Assumption 6 f(c+1)=f(c)+((c+1)+(c+1)) Universal Elimination 2 7 f(c+1)=c*(c+1)+((c+1)+(c+1)) Equality Elimination 6 5 8 c*(c+1)+((c+1)+(c+1))=(c+1)*((c+1)+1) Rational Equation 9 f(c+1)=(c+1)*((c+1)+1) Equality Elimination 7 8 10 f(c)=c*(c+1) => f(c+1)=(c+1)*((c+1)+1) Implication Introduction 5 9 11 AZ:(f(Z)=Z*(Z+1) => f(Z+1)=(Z+1)*((Z+1)+1)) Universal Introduction 10 12 AZ:f(Z)=Z*(Z+1) Rational Induction 4 11 1 EY:AX:p(X,Y) Premise 2 AX:p(X,d) Assumption 3 p(c,d) Universal Elimination 2 4 EY:p(c,Y) Existential Introduction 3 5 AX:p(X,d) => EY:p(c,Y) Implication Introduction 2 4 6 AY:(AX:p(X,Y) => EY:p(c,Y)) Universal Introduction 5 7 EY:p(c,Y) Existential Elimination 1 6 8 AX:EY:p(X,Y) Universal Introduction 7 1 ~p => r Premise 2 ~(p | r) Assumption 3 p Assumption 4 p | r Or Introduction 3 5 p => p | r Implication Introduction 3 4 6 p Assumption 7 ~(p | r) Reiteration 2 8 p => ~(p | r) Implication Introduction 6 7 9 ~p Negation Introduction 5 8 10 r Implication Elimination 1 9 11 p | r Or Introduction 10 12 ~(p | r) => p | r Implication Introduction 2 11 13 ~(p | r) Assumption 14 ~(p | r) => ~(p | r) Implication Introduction 13 13 15 ~~(p | r) Negation Introduction 12 14 16 p | r Negation Elimination 15 1 EY:p(Y) Premise 2 p(d) Assumption 3 p(c) | p(d) Or Introduction 2 4 EY:(p(c) | p(Y)) Existential Introduction 3 5 p(d) => EY:(p(c) | p(Y)) Implication Introduction 2 4 6 AY:(p(Y) => EY:(p(c) | p(Y))) Universal Introduction 5 7 EY:(p(c) | p(Y)) Existential Elimination 1 6 8 AX:EY:(p(X) | p(Y)) Universal Introduction 7 1 EX:EY:(p(X) | p(Y)) Premise 2 EY:(p(c) | p(Y)) Assumption 3 p(c) | p(d) Assumption 4 p(c) Assumption 5 EY:p(Y) Existential Introduction 4 6 p(c) => EY:p(Y) Implication Introduction 4 5 7 p(d) Assumption 8 EY:p(Y) Existential Introduction 7 9 p(d) => EY:p(Y) Implication Introduction 7 8 10 EY:p(Y) Or Elimination 3 6 9 11 p(c) | p(d) => EY:p(Y) Implication Introduction 3 10 12 AY:(p(c) | p(Y) => EY:p(Y)) Universal Introduction 11 13 EY:p(Y) Existential Elimination 2 12 14 EY:(p(c) | p(Y)) => EY:p(Y) Implication Introduction 2 13 15 AX:(EY:(p(X) | p(Y)) => EY:p(Y)) Universal Introduction 14 16 EY:p(Y) Existential Elimination 1 15 1 AX:(p(X) => q(f(X))) Premise 2 AX:(q(X) => p(f(X))) Premise 3 p(a) | q(a) Premise 4 p(c) | q(c) Assumption 5 p(c) Assumption 6 p(c) => q(f(c)) Universal Elimination 1 7 q(f(c)) Implication Elimination 6 5 8 p(f(c)) | q(f(c)) Or Introduction 7 9 p(c) => p(f(c)) | q(f(c)) Implication Introduction 5 8 10 q(c) Assumption 11 q(c) => p(f(c)) Universal Elimination 2 12 p(f(c)) Implication Elimination 11 10 13 p(f(c)) | q(f(c)) Or Introduction 12 14 q(c) => p(f(c)) | q(f(c)) Implication Introduction 10 13 15 p(f(c)) | q(f(c)) Or Elimination 4 9 14 16 p(c) | q(c) => p(f(c)) | q(f(c)) Implication Introduction 4 15 17 AX:(p(X) | q(X) => p(f(X)) | q(f(X))) Universal Introduction 16 18 AX:(p(X) | q(X)) Induction 3 17 1 p(a) Premise 2 p(s(a)) Premise 3 AX:(p(X) => p(s(s(X)))) Premise 4 p(a) & p(s(a)) And Introduction 1 2 5 p(c) & p(s(c)) Assumption 6 p(c) And Elimination 5 7 p(s(c)) And Elimination 5 8 p(c) => p(s(s(c))) Universal Elimination 3 9 p(s(s(c))) Implication Elimination 8 6 10 p(s(c)) & p(s(s(c))) And Introduction 7 9 11 p(c) & p(s(c)) => p(s(c)) & p(s(s(c))) Implication Introduction 5 10 12 AX:(p(X) & p(s(X)) => p(s(X)) & p(s(s(X)))) Universal Introduction 11 13 AX:(p(X) & p(s(X))) Induction 4 12 14 p(c) & p(s(c)) Universal Elimination 13 15 p(c) And Elimination 14 16 AX:p(X) Universal Introduction 15 1 EX:q(X) => EX:p(X) Premise 2 EX:~r(X) Premise 3 AX:(~q(X) => r(X)) Premise 4 ~r(c) Assumption 5 ~q(c) => r(c) Universal Elimination 3 6 ~q(c) Assumption 7 ~r(c) Reiteration 4 8 ~q(c) => ~r(c) Implication Introduction 6 7 9 ~~q(c) Negation Introduction 5 8 10 q(c) Negation Elimination 9 11 EX:q(X) Existential Introduction 10 12 ~r(c) => EX:q(X) Implication Introduction 4 11 13 AX:(~r(X) => EX:q(X)) Universal Introduction 12 14 EX:q(X) Existential Elimination 2 13 15 EX:p(X) Implication Elimination 1 14 1 EX:(p(X) | q(X)) Premise 2 p(a) | q(a) Assumption 3 p(a) Assumption 4 EX:p(X) Existential Introduction 3 5 EX:p(X) | EX:q(X) Or Introduction 4 6 p(a) => EX:p(X) | EX:q(X) Implication Introduction 3 5 7 q(a) Assumption 8 EX:q(X) Existential Introduction 7 9 EX:p(X) | EX:q(X) Or Introduction 8 10 q(a) => EX:p(X) | EX:q(X) Implication Introduction 7 9 11 EX:p(X) | EX:q(X) Or Elimination 2 6 10 12 p(a) | q(a) => EX:p(X) | EX:q(X) Implication Introduction 2 11 13 AX:(p(X) | q(X) => EX:p(X) | EX:q(X)) Universal Introduction 12 14 EX:p(X) | EX:q(X) Existential Elimination 1 13 1 EX:p(X) | EX:q(X) Premise 2 AX:(p(X) => q(X)) Premise 3 EX:p(X) Assumption 4 p(c) Assumption 5 p(c) => q(c) Universal Elimination 2 6 q(c) Implication Elimination 5 4 7 EX:q(X) Existential Introduction 6 8 p(c) => EX:q(X) Implication Introduction 4 7 9 AX:(p(X) => EX:q(X)) Universal Introduction 8 10 EX:q(X) Existential Elimination 3 9 11 EX:p(X) => EX:q(X) Implication Introduction 3 10 12 EX:q(X) Assumption 13 EX:q(X) => EX:q(X) Implication Introduction 12 12 14 EX:q(X) Or Elimination 1 11 13 1 AX:(p(X) | q) Premise 2 ~(AX:p(X) | q) Assumption 3 q Assumption 4 AX:p(X) | q Or Introduction 3 5 q => AX:p(X) | q Implication Introduction 3 4 6 q Assumption 7 ~(AX:p(X) | q) Reiteration 2 8 q => ~(AX:p(X) | q) Implication Introduction 6 7 9 ~q Negation Introduction 5 8 10 ~(AX:p(X) | q) => ~q Implication Introduction 2 9 11 ~(AX:p(X) | q) Assumption 12 AX:p(X) Assumption 13 AX:p(X) | q Or Introduction 12 14 AX:p(X) => AX:p(X) | q Implication Introduction 12 13 15 AX:p(X) Assumption 16 ~(AX:p(X) | q) Reiteration 11 17 AX:p(X) => ~(AX:p(X) | q) Implication Introduction 15 16 18 ~AX:p(X) Negation Introduction 14 17 19 ~q Assumption 20 ~AX:p(X) Reiteration 18 21 ~q => ~AX:p(X) Implication Introduction 19 20 22 ~q Assumption 23 p(c) | q Universal Elimination 1 24 p(c) Assumption 25 p(c) => p(c) Implication Introduction 24 24 26 q Assumption 27 ~p(c) Assumption 28 q Reiteration 26 29 ~p(c) => q Implication Introduction 27 28 30 ~p(c) Assumption 31 ~q Reiteration 22 32 ~p(c) => ~q Implication Introduction 30 31 33 ~~p(c) Negation Introduction 29 32 34 p(c) Negation Elimination 33 35 q => p(c) Implication Introduction 26 34 36 p(c) Or Elimination 23 25 35 37 AX:p(X) Universal Introduction 36 38 ~q => AX:p(X) Implication Introduction 22 37 39 ~~q Negation Introduction 38 21 40 q Negation Elimination 39 41 ~(AX:p(X) | q) => q Implication Introduction 11 40 42 ~~(AX:p(X) | q) Negation Introduction 41 10 43 AX:p(X) | q Negation Elimination 42 1 AX:X+0=X Premise 2 AX:AY:X+Y=Y+X Premise 3 AX:AY:s(X)+Y=s(X+Y) Premise 4 even(0) Premise 5 AX:(even(X) => odd(s(X))) Premise 6 AX:(odd(X) => even(s(X))) Premise 7 0+0=0 Universal Elimination 1 8 even(0+0) Equality Elimination 7 4 9 even(c+c) Assumption 10 AY:s(c)+Y=s(c+Y) Universal Elimination 3 11 s(c)+s(c)=s(c+s(c)) Universal Elimination 10 12 AY:c+Y=Y+c Universal Elimination 2 13 c+s(c)=s(c)+c Universal Elimination 12 14 AY:s(c)+Y=s(c+Y) Universal Elimination 3 15 s(c)+c=s(c+c) Universal Elimination 14 16 c+s(c)=s(c+c) Equality Elimination 15 13 17 s(c)+s(c)=s(s(c+c)) Equality Elimination 16 11 18 even(c+c) => odd(s(c+c)) Universal Elimination 5 19 odd(s(c+c)) Implication Elimination 18 9 20 odd(s(c+c)) => even(s(s(c+c))) Universal Elimination 6 21 even(s(s(c+c))) Implication Elimination 20 19 22 even(s(c)+s(c)) Equality Elimination 17 21 23 even(c+c) => even(s(c)+s(c)) Implication Introduction 9 22 24 AZ:(even(Z+Z) => even(s(Z)+s(Z))) Universal Introduction 23 25 AZ:even(Z+Z) Induction 8 24 1 AX:f(X,0)=X Premise 2 AX:AY:f(X,s(Y))=s(f(X,Y)) Premise 3 f(0,0)=0 Universal Elimination 1 4 f(0,c)=c Assumption 5 AY:f(0,s(Y))=s(f(0,Y)) Universal Elimination 2 6 f(0,s(c))=s(f(0,c)) Universal Elimination 5 7 f(0,s(c))=s(c) Equality Elimination 4 6 8 f(0,c)=c => f(0,s(c))=s(c) Implication Introduction 4 7 9 AX:(f(0,X)=X => f(0,s(X))=s(X)) Universal Introduction 8 10 AX:f(0,X)=X Induction 3 9 1 AX:X+0=X Premise 2 AX:AY:AZ:X+(Y+Z)=(X+Y)+Z Premise 3 0+0=0 Universal Elimination 1 4 0+c=c & 0+d=d Assumption 5 0+c=c And Elimination 4 6 0+(c+d)=0+(c+d) Equality Introduction 7 AY:AZ:0+(Y+Z)=(0+Y)+Z Universal Elimination 2 8 AZ:0+(c+Z)=(0+c)+Z Universal Elimination 7 9 0+(c+d)=(0+c)+d Universal Elimination 8 10 0+(c+d)=c+d Equality Elimination 5 9 11 0+c=c & 0+d=d => 0+(c+d)=c+d Implication Introduction 4 10 12 AY:(0+c=c & 0+Y=Y => 0+(c+Y)=c+Y) Universal Introduction 11 13 AX:AY:(0+X=X & 0+Y=Y => 0+(X+Y)=X+Y) Universal Introduction 12 14 AY:0+Y=Y Induction 3 13 1 f(0)=0 Premise 2 AZ:f(Z+1)=f(Z)+(Z+1) Premise 3 f(0)+f(0)=f(0)+f(0) Equality Introduction 4 f(0)+f(0)=0+0 Equality Elimination 1 3 5 0+0=0 Equation 6 f(0)+f(0)=0 Equality Elimination 5 4 7 f(c)+f(c)=c*(c+1) Assumption 8 f(c+1)=f(c)+(c+1) Universal Elimination 2 9 f(c+1)+f(c+1)=f(c+1)+f(c+1) Equality Introduction 10 f(c+1)+f(c+1)=(f(c)+(c+1))+(f(c)+(c+1)) Equality Elimination 8 9 11 (f(c)+(c+1))+(f(c)+(c+1))=(f(c)+f(c))+((c+1)+(c+1)) Equation 12 f(c+1)+f(c+1)=(f(c)+f(c))+((c+1)+(c+1)) Equality Elimination 11 10 13 f(c+1)+f(c+1)=c*(c+1)+((c+1)+(c+1)) Equality Elimination 7 12 14 c*(c+1)+((c+1)+(c+1))=(c+1)*((c+1)+1) Equation 15 f(c+1)+f(c+1)=(c+1)*((c+1)+1) Equality Elimination 14 13 16 f(c)+f(c)=c*(c+1) => f(c+1)+f(c+1)=(c+1)*((c+1)+1) Implication Introduction 7 15 17 AX:(f(X)+f(X)=X*(X+1) => f(X+1)+f(X+1)=(X+1)*((X+1)+1)) Universal Introduction 16 18 AX:f(X)+f(X)=X*(X+1) Rational Induction 1 h(1)=1 Premise 2 AZ:h(Z+1)=h(Z)+6*Z Premise 3 0+1=1 Rational Equation 4 h(0+1)=1 Equality Elimination 3 1 5 3*0*(0+1)+1=1 Rational Equation 6 h(0+1)=3*0*(0+1)+1 Equality Elimination 5 4 7 h(c+1)=3*c*(c+1)+1 Assumption 8 h((c+1)+1)=h(c+1)+6*(c+1) Universal Elimination 2 9 h((c+1)+1)=(3*c*(c+1)+1)+6*(c+1) Equality Elimination 7 8 10 (3*c*(c+1)+1)+6*(c+1)=3*(c+1)*((c+1)+1)+1 Rational Equation 11 h((c+1)+1)=3*(c+1)*((c+1)+1)+1 Equality Elimination 10 9 12 h(c+1)=3*c*(c+1)+1 => h((c+1)+1)=3*(c+1)*((c+1)+1)+1 Implication Introduction 7 11 13 AZ:(h(Z+1)=3*Z*(Z+1)+1 => h((Z+1)+1)=3*(Z+1)*((Z+1)+1)+1) Universal Introduction 12 14 AZ:h(Z+1)=3*Z*(Z+1)+1 Rational Induction 6 13 1 f(1)=1 Premise 2 AX:f(X+1)=f(X)+(2*X+1) Premise 3 1=1*1 Equation 4 f(1)=1*1 Equality Elimination 3 1 5 f(c)=c*c Assumption 6 f(c+1)=f(c)+(2*c+1) Universal Elimination 2 7 f(c+1)=c*c+(2*c+1) Equality Elimination 5 6 8 (c+1)*(c+1)=c*c+(2*c+1) Equation 9 f(c+1)=(c+1)*(c+1) Equality Elimination 8 7 10 f(c)=c*c => f(c+1)=(c+1)*(c+1) Implication Introduction 5 9 11 AX:(f(X)=X*X => f(X+1)=(X+1)*(X+1)) Universal Introduction 10 12 AX:f(X)=X*X Rational Induction 1 ~p(a) Premise 2 AX:(p(g(X)) => p(X)) Premise 3 ~p(c) Assumption 4 p(g(c)) => p(c) Universal Elimination 2 5 p(g(c)) Assumption 6 ~p(c) Reiteration 3 7 p(g(c)) => ~p(c) Implication Introduction 5 6 8 ~p(g(c)) Negation Introduction 4 7 9 ~p(c) => ~p(g(c)) Implication Introduction 3 8 10 AX:(~p(X) => ~p(g(X))) Universal Introduction 9 11 AX:~p(X) Induction 1 10 1 p Premise 2 q Assumption 3 p Reiteration 1 4 q => p Implication Introduction 2 3 1 p => (q => r) Premise 2 p => q Assumption 3 p Assumption 4 q Implication Elimination 2 3 5 q => r Implication Elimination 1 3 6 r Implication Elimination 5 4 7 p => r Implication Introduction 3 6 8 (p => q) => (p => r) Implication Introduction 2 7 1 p => ~p Premise 2 p Assumption 3 p => p Implication Introduction 2 2 4 ~p Negation Introduction 3 1 1 ~q => ~p Premise 2 p Assumption 3 ~q Assumption 4 p Reiteration 2 5 ~q => p Implication Introduction 3 4 6 ~~q Negation Introduction 5 1 7 q Negation Elimination 6 8 p => q Implication Introduction 2 7 1 p Premise 2 ~p Premise 3 ~q Assumption 4 p Reiteration 1 5 ~q => p Implication Introduction 3 4 6 ~q Assumption 7 ~p Reiteration 2 8 ~q => ~p Implication Introduction 6 7 9 ~~q Negation Introduction 5 8 10 q Negation Elimination 9 1 AY:EZ:loves(Y,Z) Premise 2 AX:AY:(EZ:loves(Y,Z) => loves(X,Y)) Premise 3 AY:(EZ:loves(Y,Z) => loves(c,Y)) Universal Elimination 2 4 EZ:loves(d,Z) => loves(c,d) Universal Elimination 3 5 EZ:loves(d,Z) Universal Elimination 1 6 loves(c,d) Implication Elimination 4 5 7 AY:loves(c,Y) Universal Introduction 6 8 AX:AY:loves(X,Y) Universal Introduction 7 1 AX:AY:(p(X,Y) => q(X)) Premise 2 AY:(p(c,Y) => q(c)) Universal Elimination 1 3 EY:p(c,Y) Assumption 4 p(c,d) Assumption 5 p(c,d) => q(c) Universal Elimination 2 6 q(c) Implication Elimination 5 4 7 p(c,d) => q(c) Implication Introduction 4 6 8 AY:(p(c,Y) => q(c)) Universal Introduction 7 9 q(c) Existential Elimination 3 8 10 EY:p(c,Y) => q(c) Implication Introduction 3 9 11 AX:(EY:p(X,Y) => q(X)) Universal Introduction 10 1 AX:(EY:p(X,Y) => q(X)) Premise 2 EY:p(c,Y) => q(c) Universal Elimination 1 3 p(c,[d]) Assumption 4 EY:p(c,Y) Existential Introduction 3 5 q(c) Implication Elimination 2 4 6 p(c,[d]) => q(c) Implication Introduction 3 5 7 AY:(p(c,Y) => q(c)) Universal Introduction 6 8 AX:AY:(p(X,Y) => q(X)) Universal Introduction 7 1 AY:plus(0,Y,Y) Premise 2 AX:AY:AZ:(plus(X,Y,Z) => plus(s(X),Y,s(Z))) Premise 3 AX:AY:AZ:AW:(plus(X,Y,Z) & ~same(Z,W) => ~plus(X,Y,W)) Premise 4 plus(0,0,0) Universal Elimination 1 5 AY:AZ:(plus(c,Y,Z) => plus(s(c),Y,s(Z))) Universal Elimination 2 6 AZ:(plus(c,0,Z) => plus(s(c),0,s(Z))) Universal Elimination 5 7 plus(c,0,c) => plus(s(c),0,s(c)) Universal Elimination 6 8 AX:(plus(X,0,X) => plus(s(X),0,s(X))) Universal Introduction 7 9 AX:plus(X,0,X) Induction 4 8 1 purebred(rex) Premise 2 AX:(purebred(X) => purebred(f(X)) & purebred(g(X))) Premise 3 purebred(c) => purebred(f(c)) & purebred(g(c)) Universal Elimination 2 4 purebred(c) Assumption 5 purebred(f(c)) & purebred(g(c)) Implication Elimination 3 4 6 purebred(f(c)) And Elimination 5 7 purebred(c) => purebred(f(c)) Implication Introduction 4 6 8 AX:(purebred(X) => purebred(f(X))) Universal Introduction 7 9 purebred(c) Assumption 10 purebred(f(c)) & purebred(g(c)) Implication Elimination 3 9 11 purebred(g(c)) And Elimination 10 12 purebred(c) => purebred(g(c)) Implication Introduction 9 11 13 AX:(purebred(X) => purebred(g(X))) Universal Introduction 12 14 AX:purebred(X) Induction 1 8 13 1 AX:f(X,0)=X Premise 2 AX:AY:f(X,s(Y))=s(f(X,Y)) Premise 3 f(0,0)=0 Universal Elimination 1 4 f(0,c)=c Assumption 5 AY:f(0,s(Y))=s(f(0,Y)) Universal Elimination 2 6 f(0,s(c))=s(f(0,c)) Universal Elimination 5 7 f(0,s(c))=s(c) Equality Elimination 4 6 8 f(0,c)=c => f(0,s(c))=s(c) Implication Introduction 4 7 9 AX:(f(0,X)=X => f(0,s(X))=s(X)) Universal Introduction 8 10 AX:f(0,X)=X Induction 3 9 1 f(0)=0 Premise 2 AZ:f(Z+1)=f(Z)+((Z+1)+(Z+1)) Premise 3 0*(0+1)=0 Equation 4 f(0)=0*(0+1) Equality Elimination 3 1 5 f(c)=c*(c+1) Assumption 6 f(c+1)=f(c)+((c+1)+(c+1)) Universal Elimination 2 7 f(c+1)=c*(c+1)+((c+1)+(c+1)) Equality Elimination 5 6 8 c*(c+1)+((c+1)+(c+1))=(c+1)*((c+1)+1) Equation 9 f(c+1)=(c+1)*((c+1)+1) Equality Elimination 8 7 10 f(c)=c*(c+1) => f(c+1)=(c+1)*((c+1)+1) Implication Introduction 5 9 11 AZ:(f(Z)=Z*(Z+1) => f(Z+1)=(Z+1)*((Z+1)+1)) Universal Introduction 10 12 AZ:f(Z)=Z*(Z+1) Rational Induction 1 g(0)=0 Premise 2 AZ:g(Z+1)=g(Z)+(2*Z+1) Premise 3 0=0*0 Rational Equation 4 g(0)=0*0 Equality Elimination 3 1 5 g(z)=z*z Assumption 6 g(z+1)=g(z)+(2*z+1) Universal Elimination 2 7 g(z+1)=z*z+(2*z+1) Equality Elimination 5 6 8 z*z+(2*z+1)=(z+1)*(z+1) Rational Equation 9 g(z+1)=(z+1)*(z+1) Equality Elimination 8 7 10 g(z)=z*z => g(z+1)=(z+1)*(z+1) Implication Introduction 5 9 11 AZ:(g(Z)=Z*Z => g(Z+1)=(Z+1)*(Z+1)) Universal Introduction 10 12 AZ:g(Z)=Z*Z Rational Induction 4 11 1 h(1)=1 Premise 2 AZ:h(Z+1)=h(Z)+6*Z Premise 3 0+1=1 Rational Equation 4 h(0+1)=1 Equality Elimination 3 1 5 3*0*(0+1)+1=1 Rational Equation 6 h(0+1)=3*0*(0+1)+1 Equality Elimination 5 4 7 h(c+1)=3*c*(c+1)+1 Assumption 8 h((c+1)+1)=h(c+1)+6*(c+1) Universal Elimination 2 9 h((c+1)+1)=(3*c*(c+1)+1)+6*(c+1) Equality Elimination 7 8 10 (3*c*(c+1)+1)+6*(c+1)=3*(c+1)*((c+1)+1)+1 Rational Equation 11 h((c+1)+1)=3*(c+1)*((c+1)+1)+1 Equality Elimination 10 9 12 h(c+1)=3*c*(c+1)+1 => h((c+1)+1)=3*(c+1)*((c+1)+1)+1 Implication Introduction 7 11 13 AZ:(h(Z+1)=3*Z*(Z+1)+1 => h((Z+1)+1)=3*(Z+1)*((Z+1)+1)+1) Universal Introduction 12 14 AZ:h(Z+1)=3*Z*(Z+1)+1 Rational Induction 6 13 1 p => q Premise 2 ~q Premise 3 p Assumption 4 ~q Reiteration 2 5 p => ~q Implication Introduction 3 4 6 ~p Negation Introduction 1 5 1 p => q Premise 2 q => r Premise 3 p Assumption 4 q Implication Elimination 1 3 5 r Implication Elimination 2 4 6 p => r Implication Introduction 3 5 1 AX:(p(X) & q(X)) Premise 2 p(c) & q(c) Universal Elimination 1 3 p(c) And Elimination 2 4 q(c) And Elimination 2 5 AX:p(X) Universal Introduction 3 6 AX:q(X) Universal Introduction 4 7 AX:p(X) & AX:q(X) And Introduction 5 6 1 AX:(p(X) => q(X)) Premise 2 AX:p(X) Assumption 3 p(c) Universal Elimination 2 4 p(c) => q(c) Universal Elimination 1 5 q(c) Implication Elimination 4 3 6 AX:q(X) Universal Introduction 5 7 AX:p(X) => AX:q(X) Implication Introduction 2 6 1 AX:AY:p(X,Y) Premise 2 AY:p(c,Y) Universal Elimination 1 3 p(c,d) Universal Elimination 2 4 AX:p(X,d) Universal Introduction 3 5 AY:AX:p(X,Y) Universal Introduction 4