(* theorems on the concepts "even" and "odd" proved by Minglong Wu *)

(* posted June 24, 1998 *)

(* Some lemmas are needed *)

(*
        IDIS5:
        -----
        (?p & ?q) -> ?r & ?s =

        ((?p -> ?r) & ?p -> ?s) | (?q -> ?r) & ?q -> ?s
*)

s "(?p&?q)->(?r&?s)";
ri "IDIS2";ex();
ri "EVERYWHERE@IDIS3";ex();
p "IDIS5";


(*

EQ_IMP_LEQ:

((Nat : ?m) = Nat : ?n) -> (Nat : ?m) =< Nat : ?n =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","LESS_EQ_REAL","NONTRIV","NOT","ODDCHOICE","OR","PLUSCOMP","PLUSTYPE","REFLEX","TYPES","XOR"]
*)

s "((Nat:?m)=Nat:?n)->(Nat:?m)=<Nat:?n";
ri "RIGHT@LESS_OR_EQ";ex();
ri "IDIS4";ex();
ri "RIGHT@IREF";ex();
ri "DZER";ex();

p "EQ_IMP_LEQ";

(*

LESS_ONE_EQ_0:

(Nat : ?x) < 1 =

(Nat : ?x) = 0

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","DIST","EQUATION","EVALEQ","IF","IFF","INDUCTION","LESS1","LESSTYPE","MINUSTYPE","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","POSTIMES","POSTYPE","REAL_LESS_DEF","REFLEX","TIMESCOMM","TIMESID","TIMESTYPE","TRICHOTOMY","TYPES","XOR","forall","forsome"]
*)

s "(Nat:?x)<1";
ri "RIGHT@ONENAT"; ex();
ri "LESSBOOL";ex();
ri "ASSERT2** $CID";ex();
right();initializecounter();
rri "LESS_LEMMA1";ex();
assign "?x_1" "?x";
assign "?y_1" "0";
ri "EVERYWHERE@ $ZERONAT";ex();
ri "EVERYWHERE@ONENAT**COMMPLUSID** $REALNAT";ex();
up();ri "3pt66";ex();
right();right();ri "RIGHT@ZERONAT";ex();
ri "LESSBOOL** $DUBNEG";ex();
right();ri "RIGHT@RIGHT@ $ZERONAT";ex();
ri "NOT_LESS_0";ex();
up();rri "FDEF";ex();
up();ri "DID";ex();
up();ri "CRULE3";ex();
ri "CSYM";ex();
ri "TAB_AND";ex();
right();left();left();left();ri "0|-|1";ex();
up();ri "RIGHT@ $ONENAT";ex();
rri "ALT_POS_DEF";ex(); (* Web Page "realorder.mk2 *)
ri "POS_ONE";ex(); (* Web Page "realorder.mk2 *)
up();ex();
up();up();rri "EQUATION";ex();

p "LESS_ONE_EQ_0";


(*

LEQ_LESS_MONO:

(((Nat : ?m) =< Nat : ?p) & (Nat : ?n) < Nat : ?q)
-> ((Nat : ?m) + Nat : ?n) < (Nat : ?p) + Nat : ?q =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","
INDUCTION","LESS1","LESSCOMP","LESSTYPE","LESS_EQ_REAL","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","TYPES","XOR","forall","forsome"]
*)

s
"(((Nat:?m)=<Nat:?p)&(Nat:?n)<Nat:?q)->((Nat:?m)+Nat:?n)<(Nat:?p)+Nat:?q";
left();ri "(LEFT@LEQ_MONO_ADD_EQF@?n)";ex();
right();initializecounter();
ri "LESS_MONO_ADD_EQ";ex();
assign "?p_1" "?p";
ri "LEFT@PLUSCOMM";ex();
ri "RIGHT@PLUSCOMM";ex();
top();ri "EVERYWHERE@PLUSTYPE2";ex();
ri "LEQ_LESS_TRANS";ex();

p "LEQ_LESS_MONO";


(*

SAME_ADD_NOT_1:

((Nat : ?x) + Nat : ?x) = 1 =

false

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","DIST","EQUATION","EVALEQ","IF","IFF","INDUCTION","LESS1","LESSCOMP","LESSTYPE","LESS_EQ_REAL","MINUSCOMP","MINUSTYPE","NATMINUSCOMP","NAT_SUB","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","POSTIMES","POSTYPE","REAL_LESS_DEF","REFLEX","SAMESUCC","SUCCNOTZERO","TIMESCOMM","TIMESID","TIMESTYPE","TRICHOTOMY","TYPES","XOR","forall","forsome"]
*)

s "((Nat:?x)+Nat:?x)=1";
ri "PCASEINTRO@(Nat:?x)<1";ex();
left();ri "LESS_ONE_EQ_0";ex();
up();right();left();left();ri "RL@0|-|1";ex();
ri "PLUSID** $REALZERO";ex();
up();ri "ZERONOTONE";ex();
top();left();rri "LESS_ONE_EQ_0";ex();
top();right();right();ri "EQUATION";ex();
right();left();initializecounter();
rri "REFLEX";ex();
assign "?a_1" "(Nat:?x).-.1";ex();
ri "EVERYWHERE@NATMINUSSCIN";ex();
ri "EVERYWHERE@TYPES";ex();
ri "EVERYWHERE@ $NATMINUSSCIN";ex();
ri "EVERYWHERE@NATMINUSTYPE";ex();
ri "RL@REALNAT";ex();initializecounter();
rri "ADD_CANCEL";ex();
assign "?z_1" "Nat:?x";ex();
right();right();rri "NATMINUSTYPE";ex();
ri "NAT_SUB";ex();
left();ri "RIGHT@ $ONENAT";ex();
up();ri "ODDCHOICE";ex();
top();ri "ODDCHOICE";ex();
right();right();right();left();right();right();
ri "1|-|1";ex();
ri "REALSUBNATTYPE";ex();
left();ri "RIGHT@ $ONENAT";ex();
up();ri "ODDCHOICE**1|-|1";ex();
ri "BREAKMINUS";ex();
up();rri "PLUSASSOC";ex();
ri "LEFT@0|-|2";ex();
rri "BREAKMINUS";ex();
ri "RIGHT@ $ONENAT";ex();
ri "SUB_REFL";ex();
up();ri "ADD_BOTH_0";ex();
left();ri "EQUATION";ex();
ri "LEFT@ $LESS_ONE_EQ_0";ex();
ri "ODDCHOICE**1|-|1";ex();
up();ri "CSYM**CZER";ex();
top();ri "EVERYWHERE@ $CASEINTRO";ex();

p "SAME_ADD_NOT_1";


(*

DUB_ADD_NOT_SUC:

((Nat : ?m) + Nat : ?m) = 1 + (Nat : ?n) + Nat
: ?n =

false

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","LESS1","LESSCOMP","LESSTYPE","LESS_EQ_REAL","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","TYPES","XOR","forall","forsome"]
*)

s "((Nat:?m)+Nat:?m)=1+(Nat:?n)+Nat:?n";
ri "PCASEINTRO@((Nat:?m)=<Nat:?n)";ex();
ri "ODDCHOICE";ex();
right();left();ri "ASRTEQ";ex();
rri "CID";ex();
left();ri "EVERYWHERE@PLUSTYPE2";ex();
up();right();initializecounter();
rri "SUC_EQ_LESS";ex();
assign "?x_1" "(Nat:?n)+Nat:?n";
assign "?y_1" "(Nat:?m)+Nat:?m";
ri "LEFT@EQSYMM";ex();
up();ri "3pt66";ex();
rri "CRULE3";ex();
right();rri "CID";ex();
right();rri "AT";ex();
rri "CID";ex();
right();rri "AT";ex();
rri "CID";ex();
up();rri "CASSOC";ex();
right();initializecounter();
rri "LEQ_LEQ_MONO";ex();
assign "?m_1" "?m";
assign "?p_1" "?n";
assign "?n_1" "?m";
assign "?q_1" "?n";
up();left();ri "RL@0|-|1";ex();
up();ri "3pt66";ex();
up();ri "CSYM";ex();
ri "CASSOC";ex();
right();left();ri "EVERYWHERE@PLUSTYPE2";ex();
up();left();rri "NOT_LESS";ex();
up();ri "CSYM";ex();
ri "CCON";ex();
up();ri "CZER";ex();
up();ri "CZER";ex();

top();rri "ODDCHOICE";ex();
rri "NOT_EXP";ex();
left();ri "NOT_LEQ";ex();
up();ri "ODDCHOICE";ex();
right();left();ri "ASRTEQ";ex();
rri "CID";ex();
right();rri "AT";ex();
rri "CID";ex();
right();rri "AT";ex();
rri "CID";ex();
up();rri "CASSOC";ex();
left();ri "LEFT@0|-|1";ex();
right();initializecounter();
rri "LESS_OR";ex();
assign "?m_1" "?n";
assign "?n_1" "?m";
up();ri "3pt66";ex();
up();right();initializecounter();
rri "LEQ_LESS_MONO";ex();
assign "?m_1" "1+Nat:?n";
assign "?p_1" "?m";
assign "?n_1" "?n";
assign "?q_1" "?m";
up();left();ri "CSYM";ex();
left();ri "EVERYWHERE@ONENAT**PLUSTYPE2";ex();
up();up();right();ri "EVERYWHERE@ONENAT";ex();
up();ri "3pt66";ex();
up();ri "CSYM";ex();
ri "CASSOC";ex();
right();rri "CRULE3";ex();
right();rri "CID";ex();
right();initializecounter();
rri "EQ_IMP_LEQ";ex();

assign "?m_1" "(Nat:?m)+Nat:?m";
assign "?n_1" "1+(Nat:?n)+Nat:?n";
left();ri "LEFT@ $PLUSTYPE2";ex();
right();right();rri "PLUSASSOC";ex();
left();ri "EVERYWHERE@ONENAT**PLUSTYPE2";ex();
up();up();rri "PLUSTYPE2";ex();
left();rri "PLUSTYPE2";ex();
ri "LEFT@ $ONENAT";ex();
up();ri "PLUSASSOC";ex();
up();up();up();ri "3pt66";ex();
up();ri "CSYM";ex();
ri "CASSOC";ex();
right();right();left();ri "PLUSTYPE2";ex();
right();left();rri "PLUSTYPE2";ex();
up();ri "PLUSASSOC";ex();
ri "EVERYWHERE@ $ONENAT";ex();
up();up();ri "RIGHT@PLUSTYPE2";ex();
up();ri "LEFT@ $NOT_LESS";ex();
ri "CSYM";ex();
ri "CCON";ex();
up();up();ri "EVERYWHERE@CZER";ex();
top();rri "CASEINTRO";ex();

p "DUB_ADD_NOT_SUC";

(*

NOT_FORSOME_EVEN_ODD:

~ forsome @ [(even @ ?1) & odd @ ?1] = 

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","LESS1","LESSCOMP","LESSTYPE","LESS_EQ_REAL","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","SUCCNOTZERO","TYPES","XOR","even","forall","forsome","odd"]
*)


initializecounter();
s "~forsome@[(even@?1)&odd@?1]";
ri "FORALL_NOTFORSOME";ex();
right();right();right();left();ri "even"; ex();
up(); right();
ri "odd"; ex();
top();right();right();ri "BIND@Nat:?1"; ex();
top();ri "INDUCTION"; ex();
left(); ri "EVAL"; ex();
right();right();right();right();right();ri "RIGHT@PLUSTYPE2";ex();
up();ri "SUCCNOTZERO";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();ri "CZER";ex();
up();ri "NEGF";ex();
up();right();right();right();ri "EVERYWHERE@EVAL";ex();
rri "CONTP";ex();

ri "IDIS5";ex();
left();left();rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();
ri "RIGHT@PLUSTYPE2";ex();
ri "SAMESUCC";ex();
left();ri "0|-|1";ex();  (*  (1+Nat:?1) = (Nat:?2)+Nat:?2  *)
up();ri "RIGHT@RIGHT@ $PLUSTYPE2";ex();
ri "DUB_ADD_NOT_SUC";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();up();rri "NOT_EXP";ex();
ri "ASSERT_UNEXP";ex();
ri "NRULE1";ex();
up();ri "REMA";ex();
ri "NRULE2";ex();
up();up();rri "FORALL_NOTFORSOME";ex();
up();ri "RIGHT@CONTP";ex();
ri "3pt67";ex();
ri "NRULE1";ex();
up();right();left();left();right();right();ri
"RIGHT@RIGHT@PLUSTYPE2";ex();

rri "SAMESUCC";ex();
ri "RIGHT@ $PLUSTYPE2";ex();
up();up();up();ri "IREF";ex();
up();ri "CSYM**CID";ex();
right();left();right();right();ri "RIGHT@RIGHT@PLUSTYPE2";ex();
rri "SAMESUCC";ex();
ri "RIGHT@ $PLUSTYPE2";ex();
up();up();up();rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();left();
ri "0|-|1";ex(); (*  (Nat:?1) = (Nat:?2)+Nat:?2  *)
up();ri "DUB_ADD_NOT_SUC";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();up();rri "NOT_EXP";ex();
ri "ASSERT_UNEXP";ex();
ri "NRULE1";ex();
up();ri "NRULE1";ex();
up();up();rri "FORALL_NOTFORSOME";ex();
up();ri "NRULE1";ex();
up();ri "DSYM** $IDEF2";ex();

rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();right();left();
ri "RIGHT@0|-|1";ex();  (*  (Nat:?1) = (Nat:?2)+Nat:?2  *)
up();ri "EQSYMM**DUB_ADD_NOT_SUC";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();ri "NEGF";ex();
up();up();rri "CASEINTRO";ex();
up();ri "AT";ex();
up();up();ri "FORALLDROP**AT";ex();
up();up();ri "FORALLDROP**AT";ex();
up();ri "CID**AT";ex();

p "NOT_FORSOME_EVEN_ODD";

(*

(*

NOT_FORSOME_EVEN_ODD:

~ forsome @ [(even @ ?1) & odd @ ?1] = 

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","LESS1","LESSCOMP","LESSTYPE","LESS_EQ_REAL","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","SUCCNOTZERO","TYPES","XOR","even","forall","forsome","odd"]
*)


initializecounter();
s "~forsome@[(even@?1)&odd@?1]";
ri "FORALL_NOTFORSOME";ex();
right();right();right();left();ri "even"; ex();
up(); right();
ri "odd"; ex();
top();right();right();ri "BIND@Nat:?1"; ex();
top();ri "INDUCTION"; ex();
left(); ri "EVAL"; ex();
right();right();right();right();right();ri "RIGHT@PLUSTYPE2";ex();
up();ri "SUCCNOTZERO";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();ri "CZER";ex();
up();ri "NEGF";ex();
up();right();right();right();ri "EVERYWHERE@EVAL";ex();
rri "CONTP";ex();

ri "IDIS5";ex();
left();left();rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();
ri "RIGHT@PLUSTYPE2";ex();
ri "SAMESUCC";ex();
left();ri "0|-|1";ex();  (*  (1+Nat:?1) = (Nat:?2)+Nat:?2  *)
up();ri "RIGHT@RIGHT@ $PLUSTYPE2";ex();
ri "DUB_ADD_NOT_SUC";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();up();rri "NOT_EXP";ex();
ri "ASSERT_UNEXP";ex();
ri "NRULE1";ex();
up();ri "REMA";ex();
ri "NRULE2";ex();
up();up();rri "FORALL_NOTFORSOME";ex();
up();ri "RIGHT@CONTP";ex();
ri "3pt67";ex();
ri "NRULE1";ex();
up();right();left();left();right();right();ri
"RIGHT@RIGHT@PLUSTYPE2";ex();

rri "SAMESUCC";ex();
ri "RIGHT@ $PLUSTYPE2";ex();
up();up();up();ri "IREF";ex();
up();ri "CSYM**CID";ex();
right();left();right();right();ri "RIGHT@RIGHT@PLUSTYPE2";ex();
rri "SAMESUCC";ex();
ri "RIGHT@ $PLUSTYPE2";ex();
up();up();up();rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();left();
ri "0|-|1";ex(); (*  (Nat:?1) = (Nat:?2)+Nat:?2  *)
up();ri "DUB_ADD_NOT_SUC";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();up();rri "NOT_EXP";ex();
ri "ASSERT_UNEXP";ex();
ri "NRULE1";ex();
up();ri "NRULE1";ex();
up();up();rri "FORALL_NOTFORSOME";ex();
up();ri "NRULE1";ex();
up();ri "DSYM** $IDEF2";ex();

rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();right();left();
ri "RIGHT@0|-|1";ex();  (*  (Nat:?1) = (Nat:?2)+Nat:?2  *)
up();ri "EQSYMM**DUB_ADD_NOT_SUC";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();ri "NEGF";ex();
up();up();rri "CASEINTRO";ex();
up();ri "AT";ex();
up();up();ri "FORALLDROP**AT";ex();
up();up();ri "FORALLDROP**AT";ex();
up();ri "CID**AT";ex();

p "NOT_FORSOME_EVEN_ODD";

*)

(* Now I use theorem "NOT_FORSOME_EVEN_ODD" to give a short proof of 
   theorem "PARITY"
*)

initializecounter();
s "forall@[ (forsome@[(Nat:?1)=(Nat:?2)+Nat:?2]) =/= forsome@[(Nat:?1)=1+(Nat:?2)+Nat:?2]]";
right();right();ri "EVERYWHERE@ $even";ex();
ri "EVERYWHERE@ $odd";ex();
ri "XALTDEF";ex();
ri "DDISC";ex();
ri "LEFT@DSYM**3pt44b";ex();
ri "RIGHT@DSYM**DDISC";ex();
right();ri "EVERYWHERE@DSYM**DXM**CID**DRULE1";ex();
ri "DEMa";ex();
top();ri "FORALLDIST";ex();
ri "LEFT@EVENODD";ex();
ri "RIGHT@ $FORALL_NOTFORSOME";ex();
ri "RIGHT@NOT_FORSOME_EVEN_ODD";ex();
ri "CID**AT";ex();

p "PARITY_2";

(*

EVEN_AND_ODD:

~ forall @ [(even @ ?1) & odd @ ?1] =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","LESS1","LESSCOMP","LESSTYPE","LESS_EQ_REAL","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","SUCCNOTZERO","TYPES","XOR","even","forall","forsome","odd"]
*)

initializecounter();
s "~forall@[(even@?1)&odd@?1]";
rri "3pt74";ex();
ri "RIGHT@FDEF";ex();
ri "RIGHT@RIGHT@ $NOT_FORSOME_EVEN_ODD";ex();
ri "IMPTOCOND";ex();
right();ri "LEFT@forall";ex();
right();left();right();right();ri "RIGHT@0|-|1";ex();
ri "FORSOMEDROP**AT";ex();
up();up();ri "DUBNEG** $TRUEBOOL";ex();
up();up();rri "CASEINTRO";ex();
up();ri "AT";ex();

p "EVEN_AND_ODD";


(*
ADD_DUB_EVEN:

even @ (Nat : ?m) + Nat : ?m =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","NONTRIV","NOT","ODDCHOICE","OR","PLUSTYPE","PLUSTYPE2","REFLEX","TYPES","XOR","even","forall","forsome"]
*)

s "even@(Nat:?m)+Nat:?m";
ri "even";ex();
ri "DINSTANTIATEF1@?m";ex();
left();ri "EVAL";ex();
ri "LEFT@ $PLUSTYPE2";ex();
ri "REFLEX";ex();
up();ri"DSYM**DZER";ex();
 
p "ADD_DUB_EVEN";

(*

DUB_ADD_EVEN:

forall @ [even @ (Nat : ?1) + Nat : ?1] =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSTYPE","PLUSTYPE
*)

(* easy way: use "ADD_DUB_EVEN", here I haven't used it *)

s "forall@[even@((Nat:?1)+Nat:?1)]";
right();right();ri "even";ex();
top();ri "INDUCT_TAC";ex();
left();ri "DINSTANTIATEF1@0";ex();
ri "LEFT@EVAL";ex();
left();left();ri "EVERYWHERE@ZERONAT** $PLUSTYPE2";ex();
up();ri "REFLEX";ex();
up();ri "DSYM**DZER";ex();
up();right();right();right();
rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();right();
ri "DINSTANTIATEF1@((Nat:?2)+1)";ex();
left();ri"EVAL";ex();
left();right();ri "EVERYWHERE@ONENAT";ex();
ri "RL@PLUSTYPE2";ex();
up();rri "PLUSTYPE2";ex();
ri "LEFT@ $PLUSTYPE2";ex();
ri "PLUSASSOC";ex();
ri "LEFT@ $ONENAT";ex();
ri "RIGHT@PLUSTYPE2";ex();

up();right();right();ri "EVERYWHERE@ONENAT** $PLUSTYPE2";ex();
ri "RIGHT@ $ONENAT";ex();
up();rri "PLUSASSOC";ex();
ri "PLUSCOMM";ex();
ri "RIGHT@PLUSTYPE2";ex();
up();rri "SAMESUCC";ex();
left();rri "PLUSTYPE2";ex();
right();rri "PLUSTYPE2";ex();
ri "LEFT@ $ONENAT";ex();
up();ri "PLUSCOMM**PLUSASSOC";ex();
ri "RIGHT@PLUSTYPE2";ex();
up();right();ri "EVERYWHERE@ $PLUSTYPE2";ex();
left();ri "EVERYWHERE@ONENAT** $PLUSTYPE2";ex();
ri "EVERYWHERE@PLUSCOMM** $ONENAT";ex();
up();ri "PLUSASSOC";ex();
ri "RIGHT@PLUSTYPE2";ex();
up();rri "SAMESUCC";ex();
ri "RIGHT@ $PLUSTYPE2";ex();
up();up();ri "IDIS4";ex();
ri "LEFT@IREF";ex();
ri "DSYM**DZER";ex();
top();ri "EVERYWHERE@FORALLDROP**AT";ex();
ri "EVERYWHERE@FORALLDROP**AT";ex();
ri "CID**AT";ex();

p "DUB_ADD_EVEN";


(*

ZERO_EVEN:

even @ 0 =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","NONTRIV","NOT","ODDCHOICE","OR","PLUSCOMP","PLUSID","PLUSTYPE","REFLEX","TYPES","XOR","even","forall","forsome"]
*)

s "even@0";
ri "even";ex();
ri "DINSTANTIATEF1@0";ex();
left();ri "EVAL";ex();
right();ri "LEFT@ $ZERONAT";ex();
ri "PLUSID** $REALNAT";ex();
up();ri "REFLEX";ex();
up();ri "DSYM**DZER";ex();

p "ZERO_EVEN";


(*

ONE_ODD:

odd @ 1 =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","NONTRIV","NOT","ODDCHOICE","OR","PLUSCOMM","PLUSCOMP","PLUSID","PLUSTYPE","REFLEX","TYPES","XOR","forall","forsome","odd"]
*)

s "odd@1";
ri "odd";ex();
ri "DINSTANTIATEF1@0";ex();
left();ri "EVAL";ex();
right();right();ri "EVERYWHERE@ $ZERONAT";ex();
ri "PLUSID** $REALZERO";ex();
up();ri "COMMPLUSID";ex();
ri "(RIGHT@ONENAT)** $REALNAT";ex();
up();ri "REFLEX";ex();
up();ri "DSYM**DZER";ex();

p "ONE_ODD";


(*

FORALL_IMP_EVEN_ODD:

(forall @ [(even @ ?1) | odd @ ?1]) -> (even @ ?x)
| odd @ ?x =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR","forall"]
*)

s "(forall@[(even@?1)|odd@?1])->(even@?x)|odd@?x";
left();initializecounter();
rri "INSTANTIATE";ex();
assign "?x_1" "?x";
ri "LEFT@EVAL";ex();
up();ri "IDIS2";ex();
ri "LEFT@IREF";ex();
ri "DSYM**DZER";ex();

p "FORALL_IMP_EVEN_ODD";

(* note : generally "(?P@?x)->forall@[?P@?1]" is not necessary true *)
(*
EVEN_ODD_IMP_FORALL:

((even @ ?x) | odd @ ?x) -> forall
@ [(even @ ?1) | odd @ ?1] =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","TYPES","XOR","even","forall","forsome","odd"]
*)

s "((even@?x)|odd@?x)->(forall@[(even@?1)|odd@?1])";
ri "RIGHT@EVENODD";ex();
ri "IRZER";ex();

p "EVEN_ODD_IMP_FORALL";


(*

EVEN_ODD_IMP_FORSOME:

((even @ ?x) | odd @ ?x) -> forsome
@ [(even @ ?1) | odd @ ?1] =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR","forall","forsome"]
*)

s "((even@?x)|odd@?x)->(forsome@[(even@?1)|odd@?1])";
right();ri "DINSTANTIATEF1@?x";ex();
ri "LEFT@EVAL";ex();
up();ri "IDIS4";ex();
ri "LEFT@IREF";ex();
ri "DSYM**DZER";ex();

p "EVEN_ODD_IMP_FORSOME";


(*

FORALL_EVEN_ODD_EQ:

((even @ ?x) | odd @ ?x) == forall
@ [(even @ ?1) | odd @ ?1] =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","TYPES","XOR","even","forall","forsome","odd"]
*)

s "((even@?x)|odd@?x)==forall@[(even@?1)|odd@?1]";
rri "3pt80";ex();
ri "LEFT@EVEN_ODD_IMP_FORALL";ex();
ri "RIGHT@FORALL_IMP_EVEN_ODD";ex();
ri "CID";ex();
ri "AT";ex();

p "FORALL_EVEN_ODD_EQ";


(*

EVEN_ODD:

(even @ ?x) | odd @ ?x =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","TYPES","XOR","even","forall","forsome","odd"]
*)

s "(even@?x)|odd@?x";
rri "DRULE1";ex();
rri "BID2";ex();
right();initializecounter();
rri "EVENODD";ex();
up();ri "FORALL_EVEN_ODD_EQ";ex();

p "EVEN_ODD";


(*

EVEN_IMP_NOT_ODD:

(even @ Nat : ?x) -> ~ odd @ Nat : ?x =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","LESS1","LESSCOMP","LESSTYPE","LESS_EQ_REAL","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","TYPES","XOR","even","forall","forsome","odd"]
*)

s "(even@Nat:?x)-> ~odd@Nat:?x";
ri "EVERYWHERE@even**odd";ex();
rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();right();ri "LEFT@0|-|1";ex();
ri "DUB_ADD_NOT_SUC";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();ri "NEGF";ex();
up();up();rri "CASEINTRO";ex();
up();ri "AT";ex();
up();up();ri "FORALLDROP**AT";ex();

p "EVEN_IMP_NOT_ODD";


(*

ODD_IMP_NOT_EVEN:

(odd @ Nat : ?x) -> ~ even @ Nat : ?x =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","LESS1","LESSCOMP","LESSTYPE","LESS_EQ_REAL","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","TYPES","XOR","even","forall","forsome","odd"]
*)

s "(odd@Nat:?x)-> ~even@Nat:?x";
ri "EVERYWHERE@even**odd";ex();
rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();right();ri "LEFT@0|-|1";ex();
ri "EQSYMM**DUB_ADD_NOT_SUC";ex();
up();up();ri "FORSOMEDROP**AF";ex();
up();ri "NEGF";ex();
up();up();rri "CASEINTRO";ex();
up();ri "AT";ex();
up();up();ri "FORALLDROP**AT";ex();

p "ODD_IMP_NOT_EVEN";


(*

NOT_ODD_IMP_EVEN:

(~ odd @ Nat : ?x) -> even @ Nat : ?x =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","TYPES","XOR","even","forall","forsome","odd"]
*)

s "(~odd@Nat:?x)->even@Nat:?x";
ri "IDEF2";ex();
ri "LEFT@DUBNEG**ASSERT2";ex();
ri "DRULE2";ex();
ri "DSYM**EVEN_ODD";ex();

p "NOT_ODD_IMP_EVEN";


(*

EVEN_EQ_NOT_ODD:

even @ Nat : ?x =

~ odd @ Nat : ?x

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","INDUCTION","LESS1","LESSCOMP","LESSTYPE","LESS_EQ_REAL","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","TYPES","XOR","even","forall","forsome","odd"]
*)

s "even@Nat:?x";
ri "even";ex();
ri "FORSOMEBOOL";ex();
right();rri "even";ex();
up();ri "ASSERT2";ex();
rri "CID";ex();
right();initializecounter();
rri "EVEN_IMP_NOT_ODD";ex();
assign "?x_1" "?x";
up();ri "3pt66";ex();
ri "CSYM";ex();
initializecounter();
rri "3pt66";ex();
ri "RIGHT@NOT_ODD_IMP_EVEN";ex();
ri "CID**NRULE1";ex();

p "EVEN_EQ_NOT_ODD";

(*

EVEN_ADD_EVEN:

((even @ Nat : ?x) & even @ Nat : ?y) -> even
@ (Nat : ?x) + Nat : ?y =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSTYPE","PLUSTYPE2","REFLEX","TYPES","XOR","even","forall","forsome"]
*)

s "((even@Nat:?x)&even@Nat:?y)->(even@(Nat:?x)+Nat:?y)";
ri "EVERYWHERE@even";ex();
rri "3pt65";ex();
ri "EVERYWHERE@ $FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();ri "LEFT@ $PLUSTYPE2";ex();
left();ri "EVERYWHERE@ $TYPES";ex();
ri "LEFT@0|-|1";ex(); (* (Nat : Nat : ?x) = (Nat : ?1) + Nat : ?1 *)
ri "RIGHT@0|-|2";ex(); (* (Nat : Nat : ?y) = (Nat : ?2) + Nat : ?2 *)
up();up();up();ri "DINSTANTIATEF1@((Nat:?1)+Nat:?2)";ex();
left();ri "EVAL";ex();
ri "EVERYWHERE@ $PLUSTYPE2";ex();
right();rri "PLUSASSOC";ex();
ri "LEFT@PLUSCOMM** $PLUSASSOC";ex();
ri "PLUSASSOC";ex();
up();ri "REFLEX";ex();
up();ri "DSYM**DZER";ex();
up();up();rri "CASEINTRO";ex();
up();ri "AT";ex();
up();up();ri "FORALLDROP**AT";ex();
up();up();rri "CASEINTRO";ex();
up();ri "AT";ex();
up();up();ri "FORALLDROP**AT";ex();

p "EVEN_ADD_EVEN";


(*

ODD_ADD_EVEN:

((odd @ Nat : ?x) & odd @ Nat : ?y) -> even
@ (Nat : ?x) + Nat : ?y =

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQUATION","IF","IFF","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSTYPE","PLUSTYPE2","REFLEX","TYPES","XOR","even","forall","forsome","odd"]
*)

s "((odd@Nat:?x)&odd@Nat:?y)->(even@(Nat:?x)+Nat:?y)";
ri "EVERYWHERE@even**odd";ex();
rri "3pt65";ex();
ri "EVERYWHERE@ $FORALL_IMP_FORSOME_EQ";ex();
right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();ri "IMPTOCOND";ex();
right();right();left();right();right();ri "LEFT@ $PLUSTYPE2";ex();
left();ri "EVERYWHERE@ $TYPES";ex();
ri "LEFT@0|-|1";ex();  (* (Nat : Nat : ?x) = 1 + (Nat : ?1) + Nat : ?1 *)
ri "RIGHT@0|-|2";ex(); (* (Nat : Nat : ?y) = 1 + (Nat : ?2) + Nat : ?2 *)
up();up();up();ri "DINSTANTIATEF1@(1+(Nat:?1)+Nat:?2)";ex();
left();ri "EVAL";ex();
right();left();right();ri "EVERYWHERE@PLUSTYPE2";ex();
ri "LEFT@ONENAT";ex();
up();rri "PLUSTYPE2";ex();
ri "EVERYWHERE@ $PLUSTYPE2";ex();
ri "LEFT@ $ONENAT";ex();
rri "PLUSASSOC";ex();
up();right();right();ri "EVERYWHERE@PLUSTYPE2";ex();
ri "LEFT@ONENAT";ex();
up();rri "PLUSTYPE2";ex();
ri "EVERYWHERE@ $PLUSTYPE2";ex();
ri "LEFT@ $ONENAT";ex();
up();ri "PLUSASSOC";ex();
right();ri "PLUSCOMM";ex();
left();rri "PLUSASSOC";ex();
ri "LEFT@PLUSCOMM";ex();
ri "PLUSASSOC";ex();
up();ri "PLUSASSOC";ex();
up();rri "PLUSASSOC";ex();
ri "RIGHT@PLUSASSOC";ex();
ri "LEFT@PLUSASSOC";ex();
up();ri "REFLEX";ex();
up();ri "DSYM**DZER";ex();
up();up();rri "CASEINTRO";ex();
up();ri "AT";ex();
up();up();ri "FORALLDROP**AT";ex();
up();up();rri "CASEINTRO";ex();
up();ri "AT";ex();
up();up();ri "FORALLDROP**AT";ex();

p "ODD_ADD_EVEN";

quit();