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

script "logicdefs2"; (* basic logic definitions, tautology checker
and Gries chapter 3 *)

(* this file includes a selection of logical tools: Parvin tactics for
conversion of "implication" theorems from one form to another,
Alves-Foss theorems about case expressions, and basic results about
quantifiers proved "by hand" *)

(* Parvin's tactics for converting between different forms of
"implication" theorems *)

(*
"?p -> ?q" = "true"
"?p & ?q" = "?p"
"?p | ?q" = "?q";
*)

(* if ?thm is "?p->?q"="true" then "?p&?q"="|-?p" *)

(*

CONVIMPAND @ ?thm:

?p & ?q = 

CID => ?p & ?thm => ?p -> ?q

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

*)

s "?p & ?q";
rri "3pt44a"; ex();
right();
rri "IF";ex();
ri "?thm";
up();
ri "CID";
p "CONVIMPAND@?thm";

(* if ?thm is "?p->?q"="true" then "?p|?q"="|-?q" *)

(*

CONVIMPOR @ ?thm:

?p | ?q = 

DID => ?q | FDEF <= ~?thm => ?p -> ?q

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

*)

s "?p | ?q";
ri "DSYM"; ex();
rri "3pt44b"; ex();
right();
ri "ANDBOOL";ex();
rri "DUBNEG"; ex();
right();
rri "DEMa";ex();
rri "IF"; ex();
rri "CONTP";ex();
ri "?thm";
up();
rri "FDEF";
up();
ri "DID";
p "CONVIMPOR@?thm";

(* if ?thm is "?p&?q"="|-?p" then "?p->?q"="true" *)

(*

CONVANDIMP @ ?thm:

?p -> ?q = 

BID => BRULE2 => (?thm => ?p & ?q) == ?p

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

*)

s "?p -> ?q";
ri "IDEF3"; ex();
left();
ri "?thm";
up();
ri "BRULE2";
ri "BID";
p "CONVANDIMP@?thm";

(* if ?thm is "?p&?q"="|-?p" then "?p|?q"="|-?q" *)

(*

CONVANDOR @ ?thm:

?p | ?q = 

DID => ?q | FDEF 
<= ~(CONVANDIMP @ ?thm) => ?p -> ?q

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

*)

s "?p | ?q";
ri "DSYM";ex();
rri "3pt44b"; ex();
right();
ri "CSYM"; ex();
ri "ANDBOOL"; ex();
rri "DUBNEG"; ex();
right();
rri "DEMa"; ex();
ri "(RIGHT@DUBNEG2)**DRULE3"; ex();
rri "IF"; ex();
ri "CONVANDIMP@?thm";
up();
rri "FDEF";
up();
ri "DID";
p "CONVANDOR@?thm";

(* if ?thm is "?p|?q"="|-?q" then "?p->?q"="true" *)

(*

CONVORIMP @ ?thm:

?p -> ?q = 

BID => BRULE2 => (?thm => ?p | ?q) == ?q

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

*)

s "?p -> ?q";
ri "IDEF"; ex();
left();
ri "?thm";
up();
ri "BRULE2";
ri "BID";
p "CONVORIMP@?thm";

(* if ?thm is "?p|?q"="|-?q" then "?p&?q"="|-?p" *)

(*

CONVORAND @ ?thm:

?p & ?q = 

BID2 => (RIGHT @ BID) => BASSOC => BRULE3 
=> (?p == ?q) == ?thm => ?p | ?q

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

*)

s "?p & ?q";
rri "GR2"; ex();
right();
ri "?thm";
up();
ri "BRULE3";
ri "BASSOC";
ri "RIGHT@BID";
ri "BID2";
p "CONVORAND@?thm";

(* Alves-Foss case expression results *)

(* ************************************
- ASRTCOND:
===========
?a || ?b , ?c = 

( |-?a) || ?b , ?c

["BCONV","BDIS","BID","BID2","BSYM","EQT","FDEF","NTYPE","ODDCHOICE","SYM","TWOASSERTS"]
*************************************** *)

start "(?a || ?b, ?c)";
ri "ODDCHOICE"; ex();
left(); ri "EQSYMM"; ex();
rri "EQT"; ex(); right(); rri "AT"; ex();
up(); rri "BCONV"; ri "BID2"; ex();
p "ASRTCOND";

(* ***************************************
- BEQSUBS:
========== 
(?a == ?b) -> ?a = 
 
(?a == ?b) -> ?b
 
["ASRTEQ","BASSOC","BCONV","BDIS","BID","BID2","BSYM","BTYPE","CONTYPE","CTYPE","DDIS","DIDEM","DSYM","DTYPE","DXM","FDEF","GR","IDEF","IMPTYPE","LZ","NTYPE","TWOASSERTS","XORDEF","XORTYPE"]

*************************************** *)
start "(?a == ?b) -> ?a";

ri "MKASRT@?a"; ex();
right(); ri "BIND@ |-?a"; ex();
top(); left(); ri "GCLEAN"; ri "BCONV"; ex();
up(); ri "3pt84b"; ex();
right(); ri "EVAL"; ex();
top(); left(); rri "BCONV"; ex();
top(); ri "GCLEAN"; ex();
p "BEQSUBS"; 

(* *************************************** 
- CONDCASESL1:
=============
(?a || ?b , ?c) == (?a & ?b) | ( ~?a) & ?c = 

true

["ASRTEQ","BASSOC","BCONV","BDIS","BID","BID2","BSYM","BTYPE","CONTYPE","CTYPE","DASSOC","DDIS","DIDEM","DSYM","DTYPE","DXM","EQT","FDEF","GR","IMPTYPE","LZ","NTYPE","ODDCHOICE","SYM","TWOASSERTS","XORDEF","XORTYPE"]
*************************************** *)

start "(?a || ?b,?c) == (?a & ?b) | ((~?a) & ?c)";

(* ** Introduce ?a | ~?a ** *)
ri "BTYPE"; rri "CID"; ex();
right(); ri "DXMF @ ?a"; ex();
ri "DTYPE"; ex();

(* ** Change to ?a = true or ?a = false ** *)
right(); left(); rri "BID2"; ex();
up(); right(); rri "3pt15a"; ex();
rri "BID2"; ex();
ri "3pt11"; ex();
right(); rri "FDEF"; ex();

(* ** Distribute this as an option ** *)
top();ri "GCLEAN"; ri "CDISD"; ex();

(* ** Now get left side ready for LZ ** *)

top(); left(); ri "CSYM"; ri "CDISD"; ex();
right();right();right();left();rri"NRULE2";ex();
up();up();left();ri "MKASRT@?a"; ex();
up(); up(); left(); ri"ASRTCOND"; ex();
up(); ri "BIND@ |-?a"; ex();

(* ** Apply LZ ** *)
up(); left(); ri "BCONV"; ex();
up(); ri "LZ"; ex();
right(); ri "EVAL"; ex();

(* ** Simplify out the conditions ** *)


left(); left(); ri "AT"; ex();
up(); ri "EVAL"; ex();
up(); right(); left(); left(); ri "AT"; ex();
up(); ri "CSYM"; ri "CID"; ex();
up(); right(); left(); rri "REMA"; ex();
right(); rri "FDEF"; ex();
up(); ri "AF"; ex();
up(); ri "CSYM"; ri "CZER"; ex();
up(); ri "GCLEAN"; ri "DID"; ex();
up(); ri "GCLEAN"; ri "BID"; ri "GCLEAN"; ex();
up(); ri "CID"; ex();
rri"ASRTEQ"; rri" BCONV"; ex();
ri "BID2"; ex();

(* ** Now get right side ready for LZ ** *)
top(); right(); ri "CSYM"; ri "CDISD"; ex();
right();right();right();left();
rri"NRULE2";ex();
up();up();left();ri "MKASRT@?a"; ex();
up(); up(); left(); ri"ASRTCOND"; ex();
up(); ri "BIND@ |-?a"; ex();

(* ** Apply LZ ** *)
up(); left(); ri "BCONV"; ex();
up(); ri "LZ"; ex();
right(); ri "EVAL"; ex();

(* ** Simplify out the conditions ** *)
left(); left(); ri "AF"; ex();
up(); ri "EVAL"; ex();
up(); right(); left(); left(); ri "AF"; ex();
up(); ri "CSYM"; ri "CZER"; ex();
up(); right(); left(); rri "REMA"; ex();

right(); ri "NEGF"; ex();
up(); ri "AT"; ex();
up(); ri "CSYM"; ri "CID"; ex();
up(); ri "GCLEAN"; ri"DSYM"; ri "DID"; ex();
up(); ri "GCLEAN"; ri "BID"; ri "GCLEAN"; ex();
up(); ri "CID"; ex();
rri"ASRTEQ"; rri" BCONV"; ex();
ri "3pt15a"; ex();
up(); ri "GCLEAN"; ri "DXM"; ex();
prove "CONDCASESL1";


(* *** Set up theorem for distruction of information *** *)
ae "CONDCASESL1"; wb(); p "CONDCASESL1F@?a,?b,?c";

(* ***************************************
- CONDCASES:  create an equation from a == b = true to a = b
============
 
(?a & ?b) | ( ~?a) & ?c =

  |-?a || ?b , ?c 

["ASRTEQ","BASSOC","BCONV","BDIS","BID","BID2","BSYM","BTYPE","CONTYPE","CTYPE","DASSOC","DDIS","DIDEM","DSYM","DTYPE","DXM","EQT","FDEF","GR","IDEF","IMPTYPE","LZ","NTYPE","ODDCHOICE","SYM","TWOASSERTS","XORDEF","XORTYPE"]
*************************************** *) 

start "(?a & ?b) | (~?a) & ?c";

ri "DTYPE"; ex();
rri "ILID"; ex();
left(); ri "CONDCASESL1F@?a,?b,?c"; ri "BSYM"; ex();
top(); right(); ri "GCLEAN"; ex();
top(); ri "BEQSUBS"; ex();
top(); left(); ri "BSYM"; ri "CONDCASESL1"; ex();
top(); ri "ILID"; ex();
p "CONDCASES";

(* ***************************************
- IMPTOCOND:
============
?a -> ?b = 
 
 |-?a || ?b , true
 
["ASRTEQ","BASSOC","BCONV","BDIS","BID","BID2","BSYM","BTYPE","CONTYPE","CTYPE","DASSOC","DDIS","DIDEM","DSYM","DTYPE","DXM","EQT","FDEF","GR","IDEF","IMPTYPE","LZ","NTYPE","ODDCHOICE","SYM","TWOASSERTS","XORDEF","XORTYPE"]
*************************************** *)
start "(?a -> ?b)";

(* ** Introduce ?a | ~?a and distribute  ** *)
ri "IMPTYPE"; ex();
rri "CID"; ex();
right(); ri "DXMF@?a"; ex();
top(); ri "CDISD"; ex();

(* ** Work left side ** *)
top(); ri "GCLEAN"; ex();
left(); ri "CSYM"; ri "3pt66"; ex();

(* ** Work right side ** *)
top(); right(); ri "CSYM"; ex();
right(); ri "IDEF2"; ex();
up(); ri "3pt43a"; ex();
rri "CID"; ex();

(* Now get into form for CONDCASES *)
top(); ri "GCLEAN"; ex();
ri "CONDCASES"; ex();
p "IMPTOCOND";

(* an application of CONDCASES *)
(* an algorithm which converts case expressions to propositional logic 
notation *)

(* still slow! *)

(* I think that Parvin has developed better algorithms of this kind
which will become publicly available *)

(*

CONDCASES2:

?a || (|-?b) , |-?c = 

(?a & ?b) | (~?a) & ?c

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

*)

s "?a||(|-?b), (|-?c)";
right();left();
ri "BIND@?b";
up();right();
ri "BIND@?c";
top();
rri "FNDIST";
ri "EVAL";
rri "CONDCASES";ex();
prove "CONDCASES2";

s "?a||?b,?c";
right();left(); ri "?b= |-?b"; ri "ALLASSERTS";
up();right(); ri "?c= |-?c"; ri "ALLASSERTS";
prove "CASEPREP";

s "(?a & ~?b) | (~?a) & ?b";
ri "PROVETAUT2@ ~?a==?b"; ex();
prove "XORALTDEF";

s "?a||(|-?b),(|-?c)";
ri "CONDCASES2"; ex();
ri "RL@CRULE1**CRULE2**CID**CZER";
ri "DRULE1**DRULE2";
rri "BALTDEF"; ri "XORALTDEF";
ri "DID**DZER";
ri "DSYM";
ri "DID";
ari "DZER";
ari "DSYM";
prove "CONDSIMP";

(* this is the main procedure *)

start "?a||?b,?c";
ri "EVERYWHERE@CASEPREP**CONDSIMP";
ri "EVERYWHERE@ $IDEF2";
ri "EVERYWHERE@ $XOR";
prove "TESTSIMP";

(* basic results about quantifiers *)

(*

INSTANTIATE:

(?P @ ?x) & forall @ [?P @ ?1] = 

forall @ [?P @ ?1]

["AND","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","NONTRIV","REFLEX","forall"]

*)

initializecounter();
s "(?P@?x)&forall@[?P@?1]";
ri "CASEINTRO"; ex();
assign "?y_1" "forall@[?P@?1]";
ri "LEFT@forall"; ex();
right(); left(); left();
ri "BIND@?x"; ex();
 ri "(LEFT@0|-|1)**EVAL"; ex();
up();
ri "AND"; ex();
ri "LEFT@REFLEX"; ex();
rri "BOOLDEF"; ex(); rri "FORALLBOOL"; ex();
up();right();right();
ri "forall"; ex(); ri "EQUATION"; ex();
ri "1|-|1"; ex();
up();
ri "AND"; ex(); ri "RIGHT@LEFT@NONTRIV"; ex(); rri "CASEINTRO"; ex(); 
rri "1|-|1"; ex();
assign "?x_18" "true";
rri "EQUATION"; ex(); 
left();right();
ri "BIND@?1"; ex();
up();up();
rri "forall"; ex();
top(); rri "CASEINTRO"; ex();
p "INSTANTIATE";

(* dual basic theorem about existential quantifier *)

(*

DINSTANTIATE:

(?P @ ?x) | forsome @ [?P @ ?1] = 

forsome @ ?P

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

*)

s "(?P@?x)|forsome@[?P@?1]";
ri "OR"; ex();
right();left();
ri "BIND@?x"; ex();
up();right(); right();
ri "forsome"; ex();
up();
ri "DUBNEG"; rri "FORALLBOOL"; ex();
up();
ri "INSTANTIATE"; ex();
top(); rri "forsome"; ex();
p "DINSTANTIATE";

ae "DINSTANTIATE";wb();p "DINSTANTIATEF1@?x";

(* proof of distributivity of universal quantification over
conjunction *)

(*

FORALLDIST:

forall @ [(?P @ ?1) & ?Q @ ?1] = 

(forall @ [?P @ ?1]) & forall @ [?Q @ ?1]

["AND","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","NONTRIV","ODDCHOICE","REFLEX","TYPES","forall"]

*)

initializecounter();
s "forall @ [(?P @ ?1) & ?Q @ ?1]";
ri "CASEINTRO"; ex();
assign "?y_1" "(forall@[?P@?1])& forall@[?Q@?1]";
ri "(LEFT@AND)**UNPACK";ex();
ri "($ODDCHOICE)**LEFT@forall"; ex();
right();left();
right();left();
right();left();left();
ri "(BIND@?1)**(LEFT@0|-|1)**EVAL";ex();
top();right();left();right();right();right();left();left();
ri "(BIND@?1)**(LEFT@0|-|1)**EVAL";ex();
top();right();right();
ri "forall"; ex();
ri "EQUATION"; ex();
right();left();
rri "1|-|1"; ex();
assign "?x_19" "false";
left();left();left();
ri "CASEINTRO"; ex(); (* notice dependency of new variable on ?1 *)
assign "[?y_20@?1]" "[(?P@?1)&(?Q@?1)]";
ri "LEFT@AND"; ex();ri "UNPACK"; ex();
right();left(); ri "RIGHT@LEFT@ $0|-|3"; ex();
 up();up();rri "ANDUNPACK"; ex();
left();ri "BIND@?1";ex(); ri "LEFT@0|-|2"; ex(); ri "EVAL"; ex();
up(); ex(); up();up(); ri "REFLEX"; up(); ex();
up();up();rri "CASEINTRO"; ex();
top();right();left();
ri "($ODDCHOICE)**LEFT@forall";ex();
right();left();right();right();right();
ri "(BIND@?1)**(LEFT@0|-|2)**EVAL";ex();
up();ri "AND"; ex(); 
ri "(EVERYWHERE@REFLEX)**(LEFT@REFLEX)"; ex(); 
up();up(); ri "forall**REFLEX"; ex();
up();right();
ri "forall"; ex();
ri "EQUATION"; ex();
right();left();
rri "1|-|2"; ex();
assign "?x_56" "false";
left();left();left();
ri "CASEINTRO"; ex();
assign "[?y_57@?1]" "[true & ?Q@?1]";
ri "ANDUNPACK"; ex();
right();left();right();left();
rri "0|-|5"; ex(); 
up();up();up();up();
rri "ANDUNPACK"; ex();
left();
ri "(BIND@?1)**(LEFT@0|-|3)**EVAL"; ex();
up();ex();
up();up();ri "REFLEX";up();ex();
up();up(); rri "CASEINTRO"; ex();
top();
ri "EVERYWHERE@ $EQUATION"; ex();
ri "LEFT@EQBOOL**BOOLDEF"; ex();
ri "RIGHT@LEFT@EQBOOL**BOOLDEF"; ex();
rri "AND"; ex();
ri "RL@ $forall"; ex();
assign "?P" "[?P@?1]";assign "?Q" "[?Q@?1]";
prove "FORALLDIST";

(* commutativity of quantifiers -- this comes in different versions
depending on stratification! *)

(* development of this proof demonstrated to me that using theorems
which introduce new variables where stratification is involved is not
desirable; that's why the parameterized PCASEINTRO was proved above *)

initializecounter();
s "forall@[forall@[?P@?1,?2]]";
ri "PCASEINTRO@forall@[forall@[?P@?2,?1]]";ex();
left();right();right();
ri "($FORALLBOOL2)**forall"; ex();
up();up();
ri "forall"; ex();
up();
right();left();
right();right();
rri "FORALLBOOL2"; ex();
right();right();
ri "BIND@?1"; ex();
ri "PCASEINTRO@[bool : ?P @ ?3 , ?2]=[true]";ex();
right();left();
ri "(LEFT@0|-|2)**EVAL";ex();
up();up();
left();
ri "BIND@?2"; ex();
ri "(LEFT@0|-|1)**EVAL"; ex();
up();ex();
up();up();ri "forall**REFLEX"; ex();
up();up();ri "forall**REFLEX"; ex();
up();right();
right();right();
ri "($FORALLBOOL2)**forall"; ex();
up();up();
ri "forall"; ex();
ri "EQUATION"; ex();
right();left();
rri "1|-|1"; ex();
assign "?x_25" "false";
left();left();left();left();left();
ri "BIND@?1"; ex();
ri "PCASEINTRO@[bool : ?P @ ?2 , ?3]=[true]";ex();
right();left();
ri "(LEFT@0|-|3)**EVAL"; ex();
up();up();
left();
ri "BIND@?2"; ex();
ri "(LEFT@0|-|2)**EVAL";ex();
up();ex();
up();up();ri "REFLEX";ex();
up();up();ri "REFLEX";ex();
up();ex();
up();up();rri "CASEINTRO"; ex();
top(); rri "EQUATION"; ex();
rri "forall"; ex();
right();right();
rri "forall"; ex();
ri "FORALLBOOL2"; ex();
p "FORALLSWITCH";


(* FORALLDROP:

forall @ [?x] = 

 |-?x

["ASSERT","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","REFLEX","forall"]  *)

start "forall@[?x]";
ri "PCASEINTRO@(true=?x)"; ex();
right();left();  (* first case *)
ri "forall"; ex();
left();left();
rri "0|-|1"; ex();
up();up();
ri "REFLEX"; ex();
up();right();  (* second case *)
rri "FORALLBOOL2"; ex();
right();right();
ri "BOOLDEF"; ri "EQUATION"; ri "1|-|1"; ex();
up();up();
ri "forall"; ri "EQUATION"; ex();
right();left();
ri "(BIND@?x)**(LEFT@ $0|-|2)**EVAL"; ex();
up();up();
rri "CASEINTRO"; ex();
top();
rri "EQUATION"; rri "BOOLDEF"; ri "ASSERT2"; ex();
p "FORALLDROP";

(*

FORSOMEDROP:

forsome @ [?x] = 

 |-?x

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

*)

s "forsome@[?x]";
ri "forsome"; ex();
right();
ri "FORALLDROP"; ex();
ri "NRULE1"; ex();
top();
ri "DUBNEG2"; ex();
p "FORSOMEDROP";

(* another case of quantifier switching *)

(* this is a nasty proof, very sensitive to stratification considerations *)

(* FORALLSWITCH2:

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

forall @ [forall @ [bool : (?P @ ?2) @ ?1]]

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

s "forall@[forall@[(?P@?1)@?2]]";
ri "PCASEINTRO@forall@[forall@[bool:(?P@?2)@?1]]";
ri "LEFT@forall";ex();
right();left();  (* the positive case *)
right();right();  rri "FORALLBOOL2"; ex();
right();right();  rri "TYPES"; ex();
right();
ri "BIND@?1"; ex();
left();
ri "PCASEINTRO@[bool : (?P @ ?3) @ ?2]=[true]"; ex();
right();left();
ri "0|-|2"; ex();
up();up();
left();
ri "EQBOOL"; ex();
right();
ri "BIND@?2"; ex();
left();left();
rri "forall"; ex();
up();
ri "0|-|1"; ex();
up();
ri "EVAL"; ex();
up();
rri "TRUEBOOL"; ex();
up(); ex();
up();
ri "EVAL"; ex();
up();
rri "TRUEBOOL"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
up();right();  (* enter the negative case *)
ri "forall"; ex();
ri "EQUATION"; ex();
right();left();  (* enter the contradictory case *)
initializecounter();
rri "1|-|1"; ex();
assign "?x_1" "false";
left();left();right();right();right();right();
ri "BIND@?1"; ex();
left();
ri "PCASEINTRO@[(?P @ ?2) @ ?3]=[true]";ex();
right();left();
ri "0|-|3"; ex();
up();up();
left();rri "forall2"; ex();
ri "BIND@?2"; ex();
ri "LEFT@0|-|2"; ex();
ri "EVAL"; ex();
up();up();ex();
ri "EVAL"; ex();
up(); rri "TRUEBOOL"; ex();
up();up();ri "FORALLDROP**AT"; ex();
up();up();up();ri "LEFT@REFLEX"; ex();
up();up();rri "CASEINTRO";ex();
up();up();ri "LEFT@ $forall";ex();
ri "ODDCHOICE** ($EQUATION)**($BOOLDEF)**($FORALLBOOL)"; ex();
p "FORALLSWITCH2";


(* NOTFORALL:

 ~forall @ [?P @ ?1] = 

(forall @ [ ~?P @ ?1]) |  ~forall @ [?P @ ?1]

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

s "~forall@[?P@?1]";
ri "PCASEINTRO@forall@[~?P@?1]"; ex();
ri "LEFT@forall"; ex();
right();left();  (* go to the case of interest *)
right();
rri "FORALLBOOL2"; ex();
right();right();
rri "DUBNEG"; ex();
right();
ri "BIND@?1"; ri "LEFT@ 0|-|1"; ri "EVAL"; ex();
up();
rri "FDEF"; ex();
up();up();
ri "FORALLDROP"; ex();
ri "AF"; ex();
up();
ri "NEGF"; ex();
top();
right();right();
ri "MAKE_CASE"; ex();
top();
rri "OR_EXP"; ex();
ri "ODDCHOICE ** ($EQUATION) ** ($BOOLDEF) ** ($ORBOOL)"; ex();
ri "LEFT@ $forall"; ex();
p "NOTFORALL";


(* FORALLNOT:

forall @ [ ~?P @ ?1] = 

(forall @ [ ~?P @ ?1]) &  ~forall @ [?P @ ?1]

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

s "forall @ [ ~?P @ ?1]";
ri "FORALLBOOL"; ex();
ri "ASSERT2"; ex();
ri "3pt43aF@ ~forall@[?P@?1]"; ex();
right();
rri "NOTFORALL"; ex();
p "FORALLNOT";

(* FORALLOR:

forall @ [(?P @ ?1) | ?Q @ ?1] = 

(forall @ [?P @ ?1]) | forall 
@ [(?P @ ?1) | ?Q @ ?1]

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

s "forall@[(?P@?1)|?Q@?1]";
ri "PCASEINTRO@forall@[?P@?1]"; ex();
ri "LEFT@forall"; ex();
right();left();  (* proceed to the interesting case *)
right();right();left();
ri "(BIND@?1)**(LEFT@0|-|1)**EVAL"; ex();
up();
ri "DSYM"; ex();
ri "DZER"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
top();
right();right();
ri "MAKE_CASE"; ex();
top();
right();right();
ri "MAKE_CASE"; ex();
top();
rri "OR_EXP"; ex();
ri "ODDCHOICE ** ($EQUATION) ** ($BOOLDEF) ** ($ORBOOL)"; ex();
ri "LEFT@ $forall";ex();
assign "?P" "[?P@?1]";
p "FORALLOR";

(* FORALLORDIST:

forall @ [?P | ?Q @ ?1] = 

?P | forall @ [?Q @ ?1]

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

s "forall@[?P|?Q@?1]";
ri "PCASEINTRO@(true=?P)"; ex();
right();left();  (* first case *)
right();right();left();
rri "0|-|1"; ex();
up();
ri "DSYM**DZER"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
up();right();  (* enter the other case *)
right();right();
rri "DRULE2"; ex();
left();
rri "ASSERT2"; ri "BOOLDEF"; ri "EQUATION"; ri "1|-|1"; ex();
up();
ri "DSYM**DID"; ex();
rri "ASSERT2";ex();
up();up();
ri "FORALLBOOL2"; ex();
top();
right();right();
ri "MAKE_CASE"; ex();
top();
right();right();
ri "MAKE_CASE"; ex();
top();
rri "OR_EXP"; ex();
ri "ODDCHOICE ** ($EQUATION) ** ($BOOLDEF) ** ($ORBOOL)"; ex();
left();
rri "BOOLDEF"; ex();
ri "ASSERT2"; ex();
up();
ri "DRULE2"; ex();
p "FORALLORDIST";

initializecounter();
s "forsome@[(?P@?1)&?Q]";
ri "forsome"; ex();
right();right();right();
rri "DEMa"; ex();
ri "DSYM";ex();
up();up();
ri "FORALLORDIST"; ex();
right();
ri "FORALLBOOL"; ex();
rri "DUBNEG"; ex();
ri "RIGHT@ $forsome2"; ex();
top();
rri "DEMb"; ex();
ri "(RL@DUBNEG**ASSERT2)**GCLEAN"; ex();
ri "CSYM";ex();
prove "FORSOMEDIST2"; 

(* popular Alves-Foss quantification theorems *)

(*

FORALL_NOTFORSOME:

~forsome @ ?P = 

forall @ [~?P @ ?1]

*)

s "~forsome @?P";
right();ri"forsome";ex();
top();ri "DUBNEG";ex();
rri "FORALLBOOL"; ex();
p "FORALL_NOTFORSOME";

(*

FORSOME_NOTFORALL:

~forall @ ?P = 

forsome @ [~?P @ ?1]

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

*)

s "~forall @?P";
right(); ri "forall";  rri "forall2"; ex();
rri"FORALLBOOL2";ex();
right();right();
rri "DUBNEG";ex();
top();
rri "forsome";
ex();
p "FORSOME_NOTFORALL";


s "forall @ [(?P@?1)->?Q]";
right();right();ri "IF";ex();
ri "OR"; ex();
top();
rri"FORALL_NOTFORSOME";ex();
right();right();right();left();
ri "DUBNEG";ex();
up();right();
ri "NOTBOOL";ex();
up();
ri"ANDSCIN";ex();
up();up();
ri"FORSOMEDIST2";ex();
up();
rri"DEMa";ex();
right();
ri"DUBNEG";ex();
up();
left();
ri "NOTBOOL";ex();
up();
ri"ORSCIN";ex();
rri"IF";ex();
p "FORALL_IMP_FORSOME_EQ";

quit();