(* August 19, 1997 (as part of general overhaul) *)

script "logicdefs2";

(* this "package" implements a complete style of reasoning for
predicate logic (tableau proofs) *)

(* The strategy is to use the TAB_??? commands to expand logical
assertions into cases (at the moment, I only provide TAB_??? commands
for a subset of the connectives, but this is easily corrected);
the TAB_ALL and TAB_SOME commands require parameters, which represent
counterexamples or witnesses, respectively.  Use the TAB_ALL_2 and
TAB_SOME_2 commands when it is necessary to reuse a statement
(when it is already the defining proposition of a case expression);
actually, it is the _2 commands which will usually be used! *)

(*

TAB_NOT:

 ~?p = 

?p || false , true

["NOT","ODDCHOICE"]

*)

s "~?p";
ri "NOT"; ex();
rri "ODDCHOICE"; ex();
p "TAB_NOT";

(*

TAB_NOT_2:

( ~?p) || ?a , ?b = 

?p || ?b , ?a

["CASEINTRO","NOT","ODDCHOICE"]

*)

s "(~?p)||?a,?b";
ri "LEFT@TAB_NOT"; ex();
ri "UNPACK"; ex();
p "TAB_NOT_2";

(*

TAB_AND:

?p & ?q = 

?p || (?q || true , false) , false

["AND","EQUATION","ODDCHOICE"]

*)

s "?p&?q";
ri "AND"; ex();
rri "ODDCHOICE"; ex();
right();left();
ri "EQUATION** $ODDCHOICE"; ex();
p "TAB_AND";

(*

TAB_AND_2:

(?p & ?q) || ?a , ?b = 

?p || (?q || ?a , ?b) , ?b

["AND","CASEINTRO","EQUATION","ODDCHOICE"]


*)

s "(?p&?q)||?a,?b";
ri "(LEFT@TAB_AND)**UNPACK"; ex();
ri "EVERYWHERE@UNPACK"; ex();
p "TAB_AND_2";


(*

TAB_OR:

?p | ?q = 

?p || true , ?q || true , false

["AND","CASEINTRO","EQUATION","NONTRIV","NOT","ODDCHOICE","OR","REFLEX"]

*)

s "?p|?q"; 
ri "ALTORDEF"; ex();
rri "ODDCHOICE"; ex();
right();right();
ri "EQUATION** $ODDCHOICE"; ex();
p "TAB_OR";

(*
TAB_OR_2:

(?p | ?q) || ?a , ?b = 

?p || ?a , ?q || ?a , ?b

["AND","CASEINTRO","EQUATION","NONTRIV","NOT","ODDCHOICE","OR","REFLEX"]


*)

s "(?p|?q)||?a,?b";
ri "(LEFT@TAB_OR)**UNPACK"; ex();
ri "EVERYWHERE@UNPACK"; ex();
p "TAB_OR_2";


(*

TAB_IF:

?p -> ?q = 

?p || (?q || true , false) , true

["AND","CASEINTRO","EQUATION","IF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX"]

*)

s "?p->?q";
ri "IF"; ex();
ri "TAB_OR"; ex();
left();
ri "TAB_NOT"; ex();
up();
ri "UNPACK"; ex();
p "TAB_IF";

(*
TAB_IF_2:

(?p -> ?q) || ?a , ?b = 

?p || (?q || ?a , ?b) , ?a

["AND","CASEINTRO","EQUATION","IF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX"]


*)

s "(?p->?q)||?a,?b";
ri "(LEFT@TAB_IF)**UNPACK"; ex();
ri "EVERYWHERE@UNPACK"; ex();
p "TAB_IF_2";

(*

TAB_IFF:

?x == ?y = 

?x || (?y || true , false) , ?y || false , true

*)

s "?x==?y";
ri "NEWTAUT"; ex();
p "TAB_IFF";

(*

TAB_IFF_2:

(?x == ?y) || ?a , ?b = 

?x || (?y || ?a , ?b) , ?y || ?b , ?a

["AND","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","XOR"]

*)

s "(?x==?y)||?a,?b";
ri "LEFT@TAB_IFF";
ri "UNPACK";
ri "EVERYWHERE@UNPACK"; ex();
p "TAB_IFF_2";

(*
TAB_XOR:

?x =/= ?y = 

?x || (?y || false , true) , ?y || true , false

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION","FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"]

*)

s "?x=/=?y";
tri "(~?x)==?y";
ri "NEWTAUT"; ex();
p "TAB_XOR";

(*

TAB_XOR_2:

(?x =/= ?y) || ?a , ?b = 

?x || (?y || ?b , ?a) , ?y || ?a , ?b

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION","FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR"]


*)

s "(?x=/=?y)||?a,?b";
ri "LEFT@TAB_XOR";
ri "UNPACK";
ri "EVERYWHERE@UNPACK"; ex();
p "TAB_XOR_2";

(*

TAB_ALL @ ?x:

forall @ [?P @ ?1] = 

(forall @ [?P @ ?1]) 
|| ((EVAL => ?P @ ?x) || true , false) , false

["CASEINTRO","EQUATION","forall"]

*)




initializecounter();
s "forall@[?P@?1]";
ri "forall**EQUATION"; ex();
right();left();
ri "PCASEINTRO@?P@?x"; ex();
right();right();
rri "1|-|2"; ex();
assign "?x_5" "false";
left();
ri "(BIND@?x)**(LEFT@0|-|1)**EVAL"; ex();
up();ex();
top();
ri "LEFT@ $forall2";ex();
top();right();left();left();
ri "EVAL";
prove "TAB_ALL@?x";


(*

TAB_SOME @ ?x:

forsome @ [?P @ ?1] = 

(forsome @ [?P @ ?1]) || true , (EVAL => ?P @ ?x) 
|| true , false

["CASEINTRO","EQBOOL","EQUATION","FNDIST","NONTRIV","NOT","ODDCHOICE","REFLEX","forall","forsome"]



*)



s "forsome@[?P@?1]";
ri "forsome"; ex();
right();
ri "TAB_ALL@?x"; ex();
drls "TAB_NOT";
ri "TAB_NOT"; up(); ri "UNPACK"; ex();
top();
ri "TAB_NOT"; ex();
ri "UNPACK"; ex();
ri "EVERYWHERE@UNPACK"; ex();
rri "NOT_EXP"; ex();
left();
rri "forsome2"; ex();
top();
right();right();left();
ri "EVAL";
prove "TAB_SOME@?x";


(*

TAB_ALL_2 @ ?x:

(forall @ [?P @ ?1]) || ?a , ?b = 

(forall @ [?P @ ?1]) 
|| ((EVAL => ?P @ ?x) || ?a , ?b) , ?b

["CASEINTRO","EQUATION","forall"]


*)


s "(forall@[?P@?1])||?a,?b";
ri "LEFT@TAB_ALL@?x"; ex();
ri "EVERYWHERE@UNPACK"; ex();
ri "EVERYWHERE@UNPACK"; ex();
right();left();left();
ri "EVAL";
prove "TAB_ALL_2@?x";

(*

TAB_SOME_2 @ ?x:

(forsome @ [?P @ ?1]) || ?a , ?b = 

(forsome @ [?P @ ?1]) || ?a , (EVAL => ?P @ ?x) 
|| ?a , ?b

["CASEINTRO","EQBOOL","EQUATION","FNDIST","NONTRIV","NOT","ODDCHOICE","REFLEX","forall","forsome"]


*)

s "(forsome@[?P@?1])||?a,?b";
ri "LEFT@TAB_SOME@?x"; ex();
ri "EVERYWHERE@UNPACK"; ex();
ri "EVERYWHERE@UNPACK"; ex();
right();right();left();
ri "EVAL";
prove "TAB_SOME_2@?x";

(* an example *)


initializecounter();
s "(forall@[?P@?1])->forsome@[?P@?1]";
ri "TAB_IF"; ex();
ri "TAB_ALL_2@?x"; ex();
dlls "TAB_SOME_2";
ri "TAB_SOME_2@?x"; ex();
downtoleft "false";
rri "1|-|2"; ex(); ri "1|-|4"; ex();
assign "?x_4" "true";
top();
ri "EVERYWHERE@ $CASEINTRO"; ex();  

(* notice the extreme effectiveness of this command!!! *)

(* a propositional example *)


initializecounter();
s "(?x&?y&?z)->?y";
ri "TAB_IF"; ex();
ri "TAB_AND_2"; ex();
right(); left();
ri "TAB_AND_2"; ex();
downtoleft "false";

(*

- lookhyps();
1 (positive):

?x


2 (positive):

?y


3 (positive):

?z


4 (negative):

?y

*)

rri "1|-|2"; ex(); ri "1|-|4"; ex();
assign "?x_4" "true";
top();
ri "EVERYWHERE@ $CASEINTRO"; ex();

(* we now introduce the tactics which were missing in the premature release:
these implement reasoning with "new" witnesses or counterexamples.  They
involve abstraction, and the setup is more complicated!  I don't think
that it will be at all transparent what is going on here *)

(* this theorem sets up a context with a "new" witness for 
reasoning under an existential hypothesis *)

(* the ugly part is that one needs to know which context to move to
after this setup (the leftmost ?a of the pair ?a,?a, the context in which
one has the hypothesis ?P @ ?1) ); the strategy is to convert this
expression to "true", return to the top, and apply the theorem
TAB_SOME_NEW_2 given below *)

(* the movement problems are soluble:

as in the example, use downtoright "?x,?x"; left(); (after
TAB_SOME_NEW_1; right(); after TAB_ALL_NEW_1) to get to the right
subexpression; use uptols "TAB_SOME_NEW_2" to get back up to the place
where TAB_SOME_NEW_2 can be applied (for example). *)

(*

TAB_SOME_NEW_1:

(forsome @ [?P @ ?1]) || ?a , ?b = 

(forsome @ [?P @ ?1]) 
|| (([?a] = [(EVAL => ?P @ ?1) || ?a , ?a]) || ?a 
   , true) , ?b

["CASEINTRO","REFLEX"]

*)

initializecounter();
s "(forsome@[?P@?1])||?a,?b";
right();left();
ri "PCASEINTRO@[?a]=[?a]"; ex();
right();right();
rri "1|-|2"; ex();
ri "LEFT@REFLEX"; ex();
assign "?x_2" "true";
up();up();left();right();right();
ri "PCASEINTRO@?P@?1"; ex();
left();
ri "EVAL"; 
p "TAB_SOME_NEW_1";

(* this is the setup for the theorem which is used to "finish up"
reasoning about "new" witnesses *)

(*

TAB_SOME_NEW_2:

(forsome @ [?P @ ?1]) 
|| (([?a] = [(?P @ ?1) || true , ?a]) || ?a , true) 
, ?b = 

(forsome @ [?P @ ?1]) || true , ?b

["CASEINTRO","EQBOOL","EQUATION","FNDIST","NONTRIV","NOT","ODDCHOICE","REFLEX","forall","forsome"]


*)

initializecounter();
s "(forsome@[?P@?1])||(([?a]=[(?P@?1)||true,?a])||?a,true),?b";
ri "LEFT@forsome"; ex();
ri "TAB_NOT_2"; ex();
ri "LEFT@forall"; ex();
right();right();
right();left();
ri "PCASEINTRO@?a=true"; ex();
right();left();
ri "0|-|3"; ex();
up();right();
rri "1|-|1"; ex();
left();left();left();
ri "NOT"; ex();
right();left();
rri "NONTRIV"; ex();
left();
rri "REFLEX"; ex();
assign "?a_10" "[?a]";
ri "RL@BIND@?1";ex();
right();left();
ri "0|-|2"; ex();
up();up();
ri "RL@EVAL"; ex();
right();left();
rri "0|-|4"; ex();
up();ex();
up();
ri "EQUATION"; ex();
ri "1|-|3"; ex();
up();
ri "REFLEX"; ex();
up();up();
rri "CASEINTRO"; ex();
up();up();up();
ri "LEFT@REFLEX"; ex();
assign "?x_7" "true";
top();
ri "EVERYWHERE@ $CASEINTRO"; ex();
ri "LEFT@ $forall";ex();
rri "NOT_EXP"; ex();
ri "LEFT@ $forsome2"; ex();
prove "TAB_SOME_NEW_2";

(* setup for the universal quantifier: introducing a "new"
counterexample when a universal statement is assumed to be false *)

(* the strategy is to move into the rightmost of the pair ?b,?b which
is created, the context in which the hypothesis ?P@?1 is available in
the _negative_ sense, convert that to "true", then return to the top
of the expression and apply TAB_ALL_NEW_2 below *)

(*

TAB_ALL_NEW_1:

(forall @ [?P @ ?1]) || ?a , ?b = 

(forall @ [?P @ ?1]) || ?a 
, ([?b] = [(EVAL => ?P @ ?1) || ?b , ?b]) || ?b 
, true

["BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","NONTRIV","NOT","ODDCHOICE","REFLEX","forall","forsome"]

*)

s "(forall@[?P@?1])||?a,?b";
left();
rri "FORALLBOOL2"; ex();
right();right();
rri "DUBNEG"; ex();
top();
rri "NOT_EXP"; ex();
ri "LEFT@ $forsome"; ex();
ri "TAB_SOME_NEW_1"; ex();
ri "LEFT@forsome"; ex();
ri "NOT_EXP"; ex();
left();right();right();
ri "DUBNEG"; ex();
up();up();
ri "FORALLBOOL2"; ex();
top();
dlls "NOT_EXP";
ri "NOT_EXP"; ex();
left();
ri "EVAL";
p "TAB_ALL_NEW_1";

(* theorem for finishing up reasoning using a "new" counterexample *)

(*

TAB_ALL_NEW_2:

(forall @ [?P @ ?1]) || ?a 
, ([?b] = [(?P @ ?1) || ?b , true]) || ?b , true = 

(forall @ [?P @ ?1]) || ?a , true

["BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","NONTRIV","NOT","ODDCHOICE","REFLEX","forall","forsome"]


*)

s "(forall @ [?P @ ?1]) || ?a , ([?b] = [(?P @ ?1) || ?b , true]) || ?b , true";
left();
rri "FORALLBOOL2"; ex();
right();right();
rri "DUBNEG"; ex();
top();
rri "NOT_EXP"; ex();
ri "LEFT@ $forsome"; ex();
right();left();left();right();right();
rri "NOT_EXP"; ex();
top();
ri "TAB_SOME_NEW_2"; ex();

ri "LEFT@forsome"; ex();
ri "NOT_EXP"; ex();
left();right();right();
ri "DUBNEG"; ex();
up();up();
ri "FORALLBOOL2"; ex();

p "TAB_ALL_NEW_2";

(* a tactic for cleanup (automatic application of the NEW_2 tactics and
of $CASEINTRO) seems both necessary and possible *)


(* example *)

(* a narrative description of what happens in the following proof would be
useful!!! (now provided) *)

(*

ALT_QUANT_IMP:

(forsome @ [forall @ [?P @ ?1 , ?2]]) -> forall 
@ [forsome @ [?P @ ?2 , ?1]] = 

true

["AND","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","IF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","forall","forsome"]


*)

initializecounter();
s "(forsome@[forall@[?P@?1,?2]]) -> (forall@[forsome@[?P@?2,?1]])";
ri "TAB_IF"; ex();  (* expand the implication into cases *)
ri "TAB_SOME_NEW_1"; ex();  (* set up "new" witness for existential *)
downtoright "?x,?x"; left();  (* go to environment with "new" witness ?1 *)
ri "TAB_ALL_NEW_1"; ex();  (* set up "new" counterexample ?2 for universal *)
downtoright "?x,?x"; right();  (* go to environment with "new" 
	counterexample *)
rri "1|-|2"; ex();  (* use hypothesis 2 (view with lookhyps) *)
assign "?x_4" "[true]";
ri "TAB_ALL_2@?2"; ex(); (* instantiate hypothesis 2 with the counterexample *)
downtoleft "false";
rri "1|-|4"; ex();  (* use hypothesis 4 (view with lookhyps) *)
assign "?x_6" "[true]";
ri "TAB_SOME_2@?1"; ex(); (* use witness ?1 as counterexample to hyp 4 *)
downtoright "false";  (* here we can see a contradiction (use lookhyps) *)
ri "($1|-|6)**1|-|8"; ex();  (* clinch the deal *)
assign "?x_10" "[true]";
up();up();  (* continue going up as long as all cases are true *)
up();up();
up();up();
up();up();
up();up();
ri "EVERYWHERE@ $CASEINTRO"; ex();  (* collapse true cases together *)
uptols "TAB_ALL_NEW_2"; (* go up to the place where the universal statement
     can be proved *)
ri "TAB_ALL_NEW_2"; ex();  (* prove it *)
up();up();
ri "EVERYWHERE@ $CASEINTRO"; ex();  (* collapse true cases together *)
uptols "TAB_SOME_NEW_2";  (* go up to the place where the existential statement
     can be proved *)
ri "TAB_SOME_NEW_2";ex();  (* prove it *)
rri "CASEINTRO"; ex();  (* collapse true cases together *)
p "ALT_QUANT_IMP";

(* an alternate approach to quantification involves the use of choice to
build explicit witnesses *)

declaretypedinfix 0 1 "!!!";
declareprefix "!!!" "defaultprefix";

axiom "CHOICE" "forsome@[?P@?1]" "?P@ !!![?P@?1]";

(* this really is the axiom of choice! *)

definetypedinfix "COUNTER1" 0 1 "***?P" "!!![~?P@?1]";
s "***[?P@?1]";ri "COUNTER1";ex();p "COUNTER";

(* deferred from typestuff.mk2:  the official definition of the subtype
constructor *)

declareinfix "|/";

axiom "SUBTYPE" "(?t |/ ?P):?x" "(?P@?t:?x)||(?t:?x),?t: !!![?P@?t:?1]";

(* theorem for introduction of counterexamples *)

(*

CEX:

forall @ [?P @ ?1] = 

bool : ?P @  ***[?P @ ?1]

["BOOLDEF","CASEINTRO","CHOICE","COUNTER1","EQBOOL","EQUATION","FNDIST","NONTRIV","NOT","REFLEX","forall","forsome"]


*)

s "forall@[?P@?1]";
ri "($FORALLBOOL2)** RIGHT@VALUE@[$DUBNEG]"; ex();
ri "FORALLBOOL** $DUBNEG"; ex();
ri "RIGHT@ $forsome2"; ex();
ri "RIGHT@CHOICE"; ex();
ri "RIGHT@RIGHT@ $COUNTER"; ex();
ri "RIGHT@EVAL"; ex();
ri "DUBNEG"; ex();
p "CEX";

s "forsome@[?P@?1]";
ri "CHOICE"; ex();
ri "EVAL";
p "CHOICE_TAC";

s "forall@[?P@?1]";
ri "CEX"; ex();
right(); ri "EVAL";
p "CEX_TAC";


(* an omission rectified; simple case introduction for quantifiers *)

(*

forsomecase:

forsome @ [?P @ ?1] = 

(forsome @ [?P @ ?1]) || true , false

["BOOLDEF","EQBOOL","EQUATION","FNDIST","NONTRIV","NOT","ODDCHOICE","REFLEX","forsome"]

*)

s "forsome@[?P@?1]";
ri "FORSOMEBOOL**BOOLDEF**EQUATION** $ODDCHOICE"; ex();
p "forsomecase";

(*

forallcase:

forall @ [?P @ ?1] = 

(forall @ [?P @ ?1]) || true , false

["BOOLDEF","EQBOOL","EQUATION","ODDCHOICE","forall"]

*)

s "forall@[?P@?1]";
ri "FORALLBOOL**BOOLDEF**EQUATION** $ODDCHOICE"; ex();
prove "forallcase";

(*

ANY_INSTANCE:

(?P @ ?x) -> ?P @  !!![?P @ ?1] = 

true

["AND","CASEINTRO","CHOICE","EQBOOL","EQUATION","FNDIST","IF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","forall","forsome"]

*)

initializecounter();
s "(?P@?x)->?P@ !!![?P@?1]";
ri "TAB_IF"; ex();
downtoleft "false";
rri "1|-|2"; ex();
ri "LEFT@ $CHOICE"; ex();
ri "LEFT@forsome"; ex();
ri "TAB_NOT_2"; ex();
ri "LEFT@forall"; ex();
downtoleft "false";
rri "1|-|1"; ex();
rri "TAB_NOT_2"; ex();
left();
ri "BIND@?x"; ex();
ri "(LEFT@0|-|3)**EVAL"; ex();
up();ex();
assign "?x_2" "true";
assign "?x_11" "true";
top();
ri "EVERYWHERE@ $CASEINTRO"; ex();
p "ANY_INSTANCE";

(* tableau proof tactics using choice *)

(*

TAB_WITNESS:

(forsome @ [?P @ ?1]) || ?a , ?b = 

(forsome @ [?P @ ?1]) 
|| ((CHOICE_TAC => forsome @ [?P @ ?1]) || ?a , ?b) 
, ?b

["CHOICE"]

*)

initializecounter();
s "(forsome@[?P@?1])||?a,?b"; 
right();left();
rri "1|-|1"; ex();
assign "?x_1" "?b";
left();
ri "CHOICE_TAC";
p "TAB_WITNESS";

(*

TAB_CEX:

(forall @ [?P @ ?1]) || ?a , ?b = 

(forall @ [?P @ ?1]) || ?a , ODDCHOICE 
<= (BOOLDEF => CEX_TAC => forall @ [?P @ ?1]) 
|| ?a , ?b

["BOOLDEF","CASEINTRO","CHOICE","COUNTER1","EQBOOL","EQUATION","FNDIST","NONTRIV","NOT","ODDCHOICE","REFLEX","forall","forsome"]

*)

initializecounter();
s "(forall@[?P@?1])||?a,?b"; 
right();right();
rri "1|-|1"; ex();
assign "?x_1" "?a";
left();
ri "CEX_TAC";ri "BOOLDEF";up();rri "ODDCHOICE";
prove "TAB_CEX";

(* another stab at alternating quantifiers *)

(*

ALT_QUANT_AGAIN:

(forsome @ [forall @ [?P @ ?1 , ?2]]) -> forall 
@ [forsome @ [?P @ ?2 , ?1]] = 

true

["AND","BOOLDEF","CASEINTRO","CHOICE","COUNTER1","EQBOOL","EQUATION","FNDIST","IF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","forall","forsome"]

*)

initializecounter();
s "(forsome@[forall@[?P@?1,?2]]) -> (forall@[forsome@[?P@?2,?1]])";
ri "TAB_IF"; ex();
ri "TAB_WITNESS"; ex();
downtoleft "false";
upto "?x||?y,?z";
ri "TAB_CEX"; ex();
 downtoleft "false";
rri "1|-|2"; ex();
ri "TAB_ALL_2@ ***[forsome @ [?P@?2,?1]]";ex();
downtoleft "false";
rri "1|-|4"; ex();
ri "TAB_SOME_2@ !!![forall @ [?P @ ?1,?2]]";ex();
downtoleft "false";
ri "($1|-|6)**1|-|8"; ex();
assign "?x_8" "true";
assign "?x_10" "true";
assign "?x_14" "true";
top();
ri "EVERYWHERE@ $CASEINTRO"; ex();
p "ALT_QUANT_AGAIN";

(* this style is much better; no need for special cleanup for the 
TAB_WITNESS and TAB_CEX tactics!!!  There is a syntactical cost:  the
witnesses have long names with bound variables in them.  It might
be a good idea to introduce definitions in long proofs, though this
would require a little work after the proof was done to get rid of the
definition deps *)


(* Alex's example *)

(*

COMMUTE_LEVEL_QUANT:

(forall @ [forall @ [?P @ ?1 , ?2]]) == forall 
@ [forall @ [?P @ ?2 , ?1]] = 

true

["AND","BOOLDEF","CASEINTRO","CHOICE","CONVIF","COUNTER1","EQBOOL","EQUATION","FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","XOR","forall","forsome"]

*)

s "(forall@[forall@[?P@?1,?2]]) == forall@[forall@[?P@?2,?1]]";
ri "TAB_IFF"; ex();
downtoleft "false";
rri "(2|-|2)@true"; ex();
ri "TAB_CEX"; ex();
right();right();
ri "TAB_CEX"; ex();
downtoright "false";
rri "(2|-|1)@true"; ex();
ri "TAB_ALL_2@ ***[?P @ ?1 ,  ***[forall @ [?P @ ?3 , ?2]]]";ex();
right();left();
ri "TAB_ALL_2@ ***[forall @ [?P @ ?2 , ?1]]"; ex(); 
downtoright "false";
ri "($(2|-|8)@true)**1|-|5"; ex();
top();
ri "EVERYWHERE@ $CASEINTRO"; ex();
downtoright "false"; (* the second part used cut and paste a lot *)
rri "(2|-|1)@true"; ex();
ri "TAB_CEX"; ex();
right();right();
ri "TAB_CEX"; ex();
downtoright "false";
rri "(2|-|2)@true"; ex();
ri "TAB_ALL_2@ ***[?P @ ( ***[forall @ [?P @ ?2 , ?3]]) , ?1] "; ex();
right();left();
ri "TAB_ALL_2@ ***[forall @ [?P @ ?1 , ?2]] "; ex(); 
downtoright "false";
ri "($(2|-|8)@true)**1|-|5"; ex();
top();
ri "EVERYWHERE@ $CASEINTRO"; ex();
p "COMMUTE_LEVEL_QUANT";

(* a handy result *)

(*

EQ_TRANS:

((?x = ?y) & ?y = ?z) -> ?x = ?z = 

true

["AND","CASEINTRO","EQUATION","IF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX"]

*)

s "((?x=?y)&(?y=?z))->?x=?z";
ri "TAB_IF"; ex();
ri "TAB_AND_2"; ex();
right();left();
ri "EVERYWHERE@LEFT@EVERYWHERE@0|-|1"; ex();
right();left();
ri "1|-|2"; ex();
top();
ri "EVERYWHERE@ $CASEINTRO"; ex();
prove "EQ_TRANS";

quit();