(* August 19, 1997 (after general overhaul) *)

script "logic_tools";
script "tableau2";
script "algebra2";

(* induction proofs on even and odd numbers *)


(* a proof partially set up by Holmes, mostly by Michael Parvin,
with guidance *)

(*

EVENODD:

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

true

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

*)

initializecounter();
s "forall@[(even@?1)|odd@?1]";
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();
(* we are now looking at a disjunction whose left term is true *)
left();
rri "DINSTANTIATE"; ex();
left();
assign "?x_4" "0";ri "EVAL"; ex();
ri "RIGHT@PLUSCOMP"; ex();
ri "REFLEX"; ex();
up();
ri "ALTORDEF"; ex();
ri "LEFT@REFLEX"; ex();
up();
ri "ALTORDEF"; ex();
ri "LEFT@REFLEX"; ex();
up();
ri "RL@EVAL"; ex();
ri "AND"; ex();
ri "LEFT@REFLEX"; ex();
rri "BOOLDEF"; ex();
rri "FORALLBOOL"; ex();
right();right();
ri "RL@EVAL";ex();
rri "3pt78";ex();
left();
rri "FORALL_IMP_FORSOME_EQ";ex();
right();right();
ri "IMPTOCOND";ex();
right();left();
ri "RIGHT@PLUSTYPE2";ex();
ri "SAMESUCC";ex();
ri "RIGHT@RIGHT@ $PLUSTYPE2";ex();
up();right();left();right();
ri "DINSTANTIATEF1 @ ?2";ex();
left();
ri "EVAL"; ex();
ri "EQUATION"; ex();
ri "1|-|1"; ex();
up();
ri "ALTORDEF"; ex();
ri "LEFT@REFLEX"; ex();
up();
ri "DSYM";ex();
ri "ALTORDEF"; ex();
ri "LEFT@REFLEX"; ex();
up();up();
rri "CASEINTRO"; ex();
up();
ri "AT"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
up();
ri "AND"; ex();
ri "LEFT@REFLEX"; ex();
rri "BOOLDEF"; ex();
ri "RIGHT@ $FORALL_IMP_FORSOME_EQ";ex();
rri "FORALLBOOL"; ex();
right();right();left();
ri "RIGHT@(LEFT@ONENAT)**(RIGHT@PLUSTYPE2)**PLUSTYPE2";ex();
ri "SAMESUCC"; ex();
ri "RIGHT@RIGHT@($PLUSTYPE2)**(RIGHT@ $PLUSTYPE2)**LEFT@ $ONENAT";ex();
ri "RIGHT@(RIGHT@($PLUSASSOC)**PLUSCOMM)** $PLUSASSOC"; ex();
up();
ri "IMPTOCOND";ex();
right();right();left();left();
ri "DINSTANTIATEF1 @ 1 + Nat: ?2";ex();
left();
ri "EVAL"; ex();
ri "EVERYWHERE@ONENAT"; ex();
ri "RIGHT@RL@ $PLUSTYPE2"; ex();
ri "EVERYWHERE@ $ONENAT"; ex();
ri "EQUATION"; ex();
ri "1|-|1"; ex();
up();
ri "ALTORDEF"; ex();
ri "LEFT@REFLEX"; ex();
up();
ri "ALTORDEF"; ex();
ri "LEFT@REFLEX"; ex();
up();up();
rri "CASEINTRO"; ex();
up();
ri "AT"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
prove "EVENODD";


(* the full-strength theorem *)

(*

PARITY:

forall 
@ [(forsome @ [(Nat : ?1) = (Nat : ?2) + Nat : ?2]) 
   =/= forsome 
   @ [(Nat : ?1) = (Nat : ?2) + (Nat : ?2) + 1]] = 

true

["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CHOICE","CONVIF","EQBOOL","EQUATION","FNDIST","FORSOMEDIST2","IF","IFF","IGNOREFIRST","INDUCTION","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","SUCCNOTZERO","SYM","TYPES","XOR","forall","forsome"]


*)

(* a tool *)

initializecounter();
s "forall@[ (forsome@[(Nat:?1)=(Nat:?2)+Nat:?2]) =/= forsome@[(Nat:?1)=(Nat:?2)+(Nat:?2)+1]]";
ri "INDUCT_TAC"; ex();
left();
left();
ri "DINSTANTIATEF1@0"; ex();
left();
ri "EVAL"; ex();
ri "EVERYWHERE@ $ZERONAT"; ex();
ri "(RIGHT@PLUSID**REALNUMERAL2)**REFLEX"; ex();
up();
ri "DSYM**DZER"; ex();
up();right();
right();right();
ri "(RIGHT@(GETPLUS@1)**RIGHT@PLUSTYPE2)**SUCCNOTZERO"; ex();
up();up();
ri "forsome**RIGHT@FORALLDROP**AF"; ex();
ri "NRULE2**DUBNEG2**AF";ex();
up();
ri "TAB_XOR"; ex();
up();right();
right();right();
ri "LEFT@XALTDEF"; ex();
rri "3pt78"; ex();
left();
rri "3pt65"; ex();
ri "IMPTOCOND"; ex();
right();
ri "TAB_NOT_2"; ex();
right();right();
rri "FORALL_IMP_FORSOME_EQ"; ex();
right();right();
ri "IMPTOCOND"; ex();
right();right();left();
right();right();right();
ri "(RIGHT@(GETPLUS@1)**RIGHT@PLUSTYPE2)** $SAMESUCC"; ex();
ri "RIGHT@ $PLUSTYPE2"; ex();
up();up();
ri "forsomecase**1|-|1";ex();
up();left();
ri "DINSTANTIATEF1@1+Nat:?2"; ex();
left();
ri "EVAL"; ex();
right();
ri "(EVERYWHERE@ONENAT)**EVERYWHERE@ $PLUSTYPE2"; ex();
ri "GETPLUS@Nat:1"; ex();
right();
ri "GETPLUS@Nat:1";ex();
ri "PLUSCOMM**PLUSASSOC"; ex();
up();
ri "(LEFT@ $BUILTIN)**RIGHT@EVERYWHERE@PLUSTYPE2"; ex();
up();
rri "SAMESUCC"; ex();
right();
ri "($PLUSTYPE2)** RIGHT@ $PLUSTYPE2"; ex();
ri "EVERYWHERE@ $ONENAT"; ex();
up();
ri "EQUATION**1|-|2"; ex();
up();
ri "TAB_OR"; ex();
up();
ri "TAB_XOR"; ex();
up();up();up();
ri "(EVERYWHERE@ $CASEINTRO)**AT"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
up();up();
rri "CASEINTRO"; ex();
up(); ri "AT"; ex();
up();right();
rri "3pt65"; ex();
rri "FORALL_IMP_FORSOME_EQ"; ex();
right();right();
ri "IMPTOCOND"; ex();
right();right();left();
ri "IMPTOCOND"; ex();
right();
ri "TAB_NOT_2"; ex();
right();right();
right();
ri "DINSTANTIATEF1@?2"; ex();
left();
ri "EVAL"; ex();
ri "RIGHT@GETPLUS@1"; ex();
ri "RIGHT@RIGHT@PLUSTYPE2"; ex();
rri "SAMESUCC"; ex();
ri "RIGHT@ $PLUSTYPE2"; ex();
ri "EQUATION**1|-|1"; ex();
up();
ri "TAB_OR"; ex();
up();up();up();

right();right();left();
right();right();
ri "PCASEINTRO@(0=Nat:?3)|forsome@[(Nat:?3)=1+Nat:?4]";ex();
ri "TAB_OR_2"; ex();
right();left();
ri "EQSYMM"; ex();
ri "LEFT@(RL@ $0|-|3)**PLUSID**REALNUMERAL2"; ex();
ri "SUCCNOTZERO"; ex();
up();right();
ri "LEFT@CHOICE_TAC";ex();
ri "BIND@ !!![(Nat : ?3) = 1 + Nat : ?4]";ex(); (* suppress the complex name
	of the witness *)
left();right();
right();left();
ri "RIGHT@RL@0|-|4"; ex();
right();
ri "PLUSASSOC**RIGHT@GETPLUS@1"; ex();
ri "RIGHT@(LEFT@TYPENUMERAL)**(RIGHT@PLUSTYPE2)**PLUSTYPE2"; ex();
up();
rri "SAMESUCC"; ex();
ri "RIGHT@($PLUSTYPE2)**RIGHT@ $PLUSTYPE2"; ex();
ri "EQUATION"; ex();
right();left();
rri "(2|-|2)@false"; ex();
left();
ri "DINSTANTIATEF1@?4"; ex();
ri "LEFT@EVAL"; ex();
ri "LEFT@RIGHT@(GETPLUS@1)**LEFT@ONENAT"; ex();
ri "(LEFT@EQUATION**1|-|5)**TAB_OR"; ex();
up();ex();
up();up();
rri "CASEINTRO"; ex();
up();up();up();up();
ri "EVAL"; ex();
ri "LEFT@ (BIND@ !!![(Nat : ?3) = 1 + Nat : ?4])** $CHOICE"; ex();
up();up();
rri "TAB_OR_2"; ex();
ri "LEFT@9pt16a@?3,ZEROORSUCC"; ex();  (* it has its uses! *)
up();up();
ri "FORSOMEDROP**AF"; ex();
up();
ri "TAB_XOR"; ex();
upto "[?P@?1]"; right();

ri "EVERYWHERE@ $CASEINTRO"; ex();
ri "EVERYWHERE@AT"; ex();
ri "EVERYWHERE@ $CASEINTRO"; ex();
ri "AT"; ex();

up();up();
ri "FORALLDROP**AT"; ex();
up(); ri "TAB_AND"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
up(); ri "TAB_AND"; ex();
p "PARITY";

quit();