(* Mar. 3, 1998 *)

(* sample application of UNEVAL added May 14, 1998 *)

(* more applications added May 17 *)

(* more quantifier theorems; calls the old total logic file *)

(* script with all earlier logic *)

script "gries9";

ae "ONEPOINT"; p "8pt14U";
ae "RIGHT"; p "R@?thm";
ae "LEFT"; p "L@?thm";

(*
******************************************************************
theorems below this point were proved by me (Michael Parvin)
******************************************************************
*)

(*
******************************************************************
8pt14E:

forsomer @ [?1 = ?e] , [?P @ ?1] =

 |-EVAL => ?P @ ?e

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsomer"]
******************************************************************
*)
s "forsomer@[?1=?e],[?P@?1]";
ri "forsomer2**(R@8pt14U)**NRULE2**DUBNEG2"; ex();
right();
ri "EVAL";
p "8pt14E";


(*
******************************************************************
UNIV_RANGE_2:

forsomer @ [true] , [?p @ ?1] =

forsome @ [?p @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsome",
"forsomer"]
******************************************************************
*)
s "forsomer@[true],[?P@?1]";
ri "forsomer2**(R@UNIV_RANGE_1)** $forsome2";ex();
p "UNIV_RANGE_2";

(* other theorems to introduce or strip bool: lables from ranged quantifiers *)


(*
******************************************************************
FORALLRBOOL2:

forallr @ [?R @ ?1] , [?P @ ?1] =

forallr @ [bool : ?R @ ?1] , [?P @ ?1]

["ASSERT","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","IF",
"NONTRIV","NOT","OR","PI1","PI2","REFLEX","TYPES","forallr"]
******************************************************************
*)
s "forallr@[?R@?1],[?P@?1]";
ri "forallr2**(R@VALUE@[($IRULE2)**L@ASSERT])** $forallr2";ex();
p "FORALLRBOOL2";


(*
******************************************************************
FORALLRBOOL3:

forallr @ [?R @ ?1] , [?P @ ?1] =

forallr @ [?R @ ?1] , [bool : ?P @ ?1]

["ASSERT","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","IF",
"NONTRIV","NOT","OR","PI1","PI2","REFLEX","TYPES","forallr"]
******************************************************************
*)
s "forallr@[?R@?1],[?P@?1]";
ri "forallr2**(R@VALUE@[($IRULE3)**R@ASSERT])** $forallr2";ex();
p "FORALLRBOOL3";


(*
******************************************************************
FORSOMERBOOL2:

forsomer @ [?R @ ?1] , [?P @ ?1] =

forsomer @ [bool : ?R @ ?1] , [?P @ ?1]

["ASSERT","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","IF",
"NONTRIV","NOT","OR","PI1","PI2","REFLEX","TYPES","forallr",
"forsomer"]
******************************************************************
*)
s "forsomer@[?R@?1],[?P@?1]";
ri "forsomer2**(R@FORALLRBOOL2)** $forsomer2"; ex();
p "FORSOMERBOOL2";


(*
******************************************************************
FORSOMERBOOL3:

forsomer @ [?R @ ?1] , [?P @ ?1] =

forsomer @ [?R @ ?1] , [bool : ?P @ ?1]

["BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","NONTRIV","NOT",
"PI1","PI2","REFLEX","forsomer"]
******************************************************************
*)
s "forsomer@[?R@?1],[?P@?1]";
ri "forsomer2**(R@R@R@VALUE@[$NOTBOOLDROP])** $forsomer2"; ex();
p "FORSOMERBOOL3";


(*
******************************************************************
8pt13U:

forallr @ [false] , [?P @ ?1] =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "forallr@[false],[?P@?1]";
ri "forallr2**(R@VALUE@[3pt75])**FORALLDROP**AT";ex();
p "8pt13U";


(*
******************************************************************
8pt13E:

forsomer @ [false] , [?P @ ?1] =

false

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsomer"]
******************************************************************
*)
s "forsomer@[false],[?P@?1]";
ri "forsomer2**(R@8pt13U)** $FDEF"; ex();
p "8pt13E";


(*
******************************************************************
8pt15U:

(forallr @ [?R @ ?1] , [?P @ ?1]) & forallr
@ [?R @ ?1] , [?Q @ ?1] =

forallr @ [?R @ ?1] , [(?P @ ?1) & ?Q @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "(forallr@[?R@?1],[?P@?1])&forallr@[?R@?1],[?Q@?1]";
ri "(RL@forallr2)** $FORALLDIST"; ex();
ri "(R@VALUE@[(RL@IF)**($DDISC)** $IF])** $forallr2";ex();
p "8pt15U";


(*
******************************************************************
8pt15E:

(forsomer @ [?R @ ?1] , [?P @ ?1]) | forsomer
@ [?R @ ?1] , [?Q @ ?1] =

forsomer @ [?R @ ?1] , [(?P @ ?1) | ?Q @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsomer"]
******************************************************************
*)
s "(forsomer@[?R@?1],[?P@?1])|forsomer@[?R@?1],[?Q@?1]";
ri "(RL@forsomer2)**DEMa**R@8pt15U**R@R@VALUE@[DEMb]"; ex();
rri "forsomer2"; ex();
p "8pt15E";


(*
******************************************************************
8pt16U:

forallr @ [(?R @ ?1) | ?S @ ?1] , [?P @ ?1] =

(forallr @ [?R @ ?1] , [?P @ ?1]) & forallr
@ [?S @ ?1] , [?P @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "forallr@[(?R@?1)|?S@?1],[?P@?1]";
ri "forallr2**(R@VALUE@[$3pt78])**FORALLDIST**RL@ $forallr2"; ex();
p "8pt16U";


(*
******************************************************************
8pt16E:

forsomer @ [(?R @ ?1) | ?S @ ?1] , [?P @ ?1] =

(forsomer @ [?R @ ?1] , [?P @ ?1]) | forsomer
@ [?S @ ?1] , [?P @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsomer"]
******************************************************************
*)
s "forsomer@[(?R@?1)|?S@?1],[?P@?1]";
ri "forsomer2**(R@8pt16U)**($DEMa)**RL@ $forsomer2"; ex();
p "8pt16E";


(*
******************************************************************
8pt19U:

forallr @ [?R @ ?1]
, [forallr @ [?Q @ ?2] , [?P @ ?1 , ?2]] =

forallr @ [?Q @ ?1]
, [forallr @ [?R @ ?2] , [?P @ ?2 , ?1]]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "forallr@[?R@?1],[forallr@[?Q@?2],[?P@?1,?2]]";
ri "forallr2"; ex();
right();right();
ri "(R@forallr2)**IDEF2** $FORALLORDIST"; ex();
right();right();
ri "(R@IDEF2)**($DASSOC)**(L@DSYM)**PAIRBIND@?1,?2"; ex();
top();
ri "FORALLSWITCH"; ex();
right();right();right();right();
ri "EVAL**(L@RL@R@R@PI1**PI2)**DASSOC**R@ $IDEF2";ex();
up();up();
ri "FORALLORDIST**(R@ $forallr2)** $IDEF2"; ex();
top();
rri "forallr2"; ex();
p "8pt19U";


(*
******************************************************************
8pt19E:

forsomer @ [?R @ ?1]
, [forsomer @ [?Q @ ?2] , [?P @ ?1 , ?2]] =

forsomer @ [?Q @ ?1]
, [forsomer @ [?R @ ?2] , [?P @ ?2 , ?1]]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsomer"]
******************************************************************
*)
s "forsomer@[?R@?1],[forsomer@[?Q@?2],[?P@?1,?2]]";
ri "(R@R@VALUE@[forsomer2])**forsomer2"; ex();
right();right();right();right();
ri "DUBNEG**($FORALLRBOOL)**R@R@VALUE@[BIND@?1,?2]";ex();
top();right();
ri "8pt19U";ex();
right();right();
ri "VALUE@[(R@R@VALUE@[EVAL])**FORALLRBOOL** $DUBNEG]"; ex();
ri "VALUE@[R@ $forsomer2]";ex();
top();
rri "forsomer2";ex();
p "8pt19E";


(*
******************************************************************
9pt3a:

forallr @ [?R @ ?1] , [?P @ ?1] =

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

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forallr"]
******************************************************************
*)
s "forallr@[?R@?1],[?P@?1]";
ri "forallr2**R@VALUE@[IDEF2]"; ex();
p "9pt3a";


(*
******************************************************************
9pt3b:

forallr @ [?R @ ?1] , [?P @ ?1] =

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

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forallr"]
******************************************************************
*)
s "forallr@[?R@?1],[?P@?1]";
ri "forallr2**R@VALUE@[IDEF3]"; ex();
p "9pt3b";


(*
******************************************************************
9pt3c:

forallr @ [?R @ ?1] , [?P @ ?1] =

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

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forallr"]
******************************************************************
*)
s "forallr@[?R@?1],[?P@?1]";
ri "forallr2**R@VALUE@[IDEF]"; ex();
p "9pt3c";


(*
******************************************************************
9pt4a:

forallr @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] =

forallr @ [?Q @ ?1] , [(?R @ ?1) -> ?P @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forallr"]
******************************************************************
*)
s "forallr@[(?Q@?1)&?R@?1],[?P@?1]";
ri "forallr2**(R@VALUE@[$3pt65])** $forallr2"; ex();
p "9pt4a";


(*
******************************************************************
9pt4b:

forallr @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] =

forallr @ [?Q @ ?1] , [( ~?R @ ?1) | ?P @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forallr"]
******************************************************************
*)
s "forallr@[(?Q@?1)&?R@?1],[?P@?1]";
ri "9pt4a**R@R@VALUE@[IDEF2]";ex();
p "9pt4b";


(*
******************************************************************
9pt4c:

forallr @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] =

forallr @ [?Q @ ?1]
, [((?R @ ?1) & ?P @ ?1) == ?R @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forallr"]
******************************************************************
*)
s "forallr@[(?Q@?1)&?R@?1],[?P@?1]";
ri "9pt4a**R@R@VALUE@[IDEF3]";ex();
p "9pt4c";


(*
******************************************************************
9pt4d:

forallr @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] =

forallr @ [?Q @ ?1]
, [((?R @ ?1) | ?P @ ?1) == ?P @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forallr"]
******************************************************************
*)
s "forallr@[(?Q@?1)&?R@?1],[?P@?1]";
ri "9pt4a**R@R@VALUE@[IDEF]";ex();
p "9pt4d";


(*
******************************************************************
9pt5:

?P | forallr @ [?R @ ?1] , [?Q @ ?1] =

forallr @ [?R @ ?1] , [?P | ?Q @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "?P|forallr@[?R@?1],[?Q@?1]";
ri "(R@forallr2)** $FORALLORDIST"; ex();
right();right();
ri "(R@IDEF2)**($DASSOC)**(L@DSYM)**DASSOC** $IDEF2";ex();
top();
rri "forallr2"; ex();
p "9pt5";


(*
******************************************************************
9pt6:

forallr @ [?R @ ?1] , [?P] =

?P | forall @ [ ~?R @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "forallr@[?R@?1],[?P]";
ri "9pt3a**(R@VALUE@[DSYM])**FORALLORDIST"; ex();
p "9pt6";


(*
******************************************************************
9pt7:

( ~forall @ [ ~?R @ ?1])
-> (forallr @ [?R @ ?1] , [?P & ?Q @ ?1]) == ?P
& forallr @ [?R @ ?1] , [?Q @ ?1] =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "(~forall@[~?R@?1])->(forallr@[?R@?1],[?P&?Q@?1])==?P&forallr@[?R@?1],[?Q@?1]";
ri "(R@L@($8pt15U)**L@9pt6)**3pt62";ex();
left();
ri "($CASSOC)**L@(R@DSYM**L@FORALLBOOL** $DUBNEG)**3pt44a"; ex();
ri "CASSOC";ex();
up();
ri "($3pt62)**(R@BID)**IRZER"; ex();
p "9pt7";


(*
******************************************************************
9pt8:

forallr @ [?R @ ?1] , [true] =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "forallr@[?R@?1],[true]";
ri "forallr2**(R@VALUE@[IRZER])**FORALLDROP**AT"; ex();
p "9pt8";


(*
******************************************************************
9pt10:

(forallr @ [(?Q @ ?1) | ?R @ ?1] , [?P @ ?1])
-> forallr @ [?Q @ ?1] , [?P @ ?1] =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "(forallr@[(?Q@?1)|?R@?1],[?P@?1])->forallr@[?Q@?1],[(?P@?1)]";
ri "(L@8pt16U)**3pt76b";ex();
p "9pt10";


(*
******************************************************************
9pt11:

(forallr @ [?R @ ?1] , [(?P @ ?1) & ?Q @ ?1])
-> forallr @ [?R @ ?1] , [?P @ ?1] =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr"]
******************************************************************
*)
s "(forallr@[?R@?1],[(?P@?1)&?Q@?1])->forallr@[?R@?1],[(?P@?1)]";
ri "(L@ $8pt15U)**3pt76b";ex();
p "9pt11";



(*
******************************************************************
9pt18a:

 ~forsomer @ [?R @ ?1] , [ ~?P @ ?1] =

forallr @ [?R @ ?1] , [?P @ ?1]

["ASSERT","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","IF",
"NONTRIV","NOT","OR","PI1","PI2","REFLEX","TYPES","forall",
"forallr","forsomer"]
******************************************************************
*)
s "~forsomer@[?R@?1],[~?P@?1]";
ri "(R@forsomer2)**DUBNEG** $FORALLRBOOL"; ex();
ri "(R@R@VALUE@[DUBNEG])** $FORALLRBOOL3"; ex();
p "9pt18a";


(*
******************************************************************
9pt18b:

 ~forsomer @ [?R @ ?1] , [?P @ ?1] =

forallr @ [?R @ ?1] , [ ~?P @ ?1]

["BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","IF","NONTRIV",
"NOT","OR","P
I1","PI2","REFLEX","forall","forallr","forsomer"]
******************************************************************
*)
s "~forsomer@[?R@?1],[?P@?1]";
ri "(R@forsomer2)**DUBNEG** $FORALLRBOOL"; ex();
p "9pt18b";


(*
******************************************************************
9pt18c:

forsomer @ [?R @ ?1] , [ ~?P @ ?1] =

 ~forallr @ [?R @ ?1] , [?P @ ?1]

["ASSERT","BOOLDEF","CASEINTRO","EQBOOL","EQUATION","FNDIST","IF",
"NONTRIV","NOT","OR","PI1","PI2","REFLEX","TYPES","forallr",
"forsomer"]
******************************************************************
*)
s "forsomer@[?R@?1],[~?P@?1]";
ri "forsomer2**(R@R@R@VALUE@[DUBNEG])**R@ $FORALLRBOOL3"; ex();
p "9pt18c";


(*
******************************************************************
9pt20:

forsomer @ [(?Q @ ?1) & ?R @ ?1] , [?P @ ?1] =

forsomer @ [?Q @ ?1] , [(?R @ ?1) & ?P @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forallr","forsome","forsomer"]
******************************************************************
*)
s "forsomer@[(?Q@?1)&?R@?1],[?P@?1]";
ri "forsomer3**(R@VALUE@[CASSOC])** $forsomer3"; ex();
p "9pt20";


(*
******************************************************************
9pt21:

forsomer @ [?R @ ?1] , [?P & ?Q @ ?1] =

?P & forsomer @ [?R @ ?1] , [?Q @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsomer"]
******************************************************************
*)
s "forsomer@[?R@?1],[?P&?Q@?1]";
ri "forsomer2**R@(R@R@VALUE@[$DEMa])** $9pt5"; ex();
ri "($DEMb)**(L@DUBNEG2)**CRULE2**R@ $forsomer2"; ex();
p "9pt21";


(*
******************************************************************
9pt22:

forsomer @ [?R @ ?1] , [?P] =

?P & forsome @ [?R @ ?1]

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsome",
"forsomer"]
******************************************************************
*)
s "forsomer@[?R@?1],[?P]";
ri "forsomer3**FORSOMEDIST2**CSYM"; ex();
p "9pt22";


(*
******************************************************************
9pt23:

(forsome @ [?R @ ?1])
-> (forsomer @ [?R @ ?1] , [?P | ?Q @ ?1]) == ?P
| forsomer @ [?R @ ?1] , [?Q @ ?1] =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsome",
"forsomer"]
******************************************************************
*)
s "(forsome@[?R@?1])->(forsomer@[?R@?1],[?P|?Q@?1])==?P|forsomer@[?R@?1],[?Q@?1]";
ri "L@forsome2"; ex();
ri "R@(L@forsomer2)**(R@R@forsomer2)**L@R@R@R@VALUE@[$DEMb]"; ex();
ri "(R@3pt11**R@($DEMb)**R@DUBNEG** $FORALLRBOOL)**9pt7";ex();
p "9pt23";


(*
******************************************************************
9pt24:

forsomer @ [?R @ ?1] , [false] =

false

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsomer"]
******************************************************************
*)
s "forsomer@[?R@?1],[false]";
ri "forsomer2**(R@R@R@VALUE@[NEGF])**(R@9pt8)** $FDEF"; ex();
p "9pt24";


(*
******************************************************************
9pt25:

(forsomer @ [?R @ ?1] , [?P @ ?1]) -> forsomer
@ [(?Q @ ?1) | ?R @ ?1] , [?P @ ?1] =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsomer"]
******************************************************************
*)
s "(forsomer@[?R@?1],[?P@?1])->forsomer@[(?Q@?1)|?R@?1],[?P@?1]";
ri "(RL@forsomer2)**($CONTP)**L@R@L@VALUE@[DSYM]"; ex();
ri "(RL@RIGHT@RIGHT@VALUE@[BIND@?1])**9pt10";ex();
p "9pt25";


(*
******************************************************************
9pt26:

(forsomer @ [?R @ ?1] , [?P @ ?1]) -> forsomer
@ [?R @ ?1] , [(?P @ ?1) | ?Q @ ?1] =

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION",
"FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR",
"PI1","PI2","REFLEX","TYPES","XOR","forall","forallr","forsome",
"forsomer"]
******************************************************************
*)
s "(forsomer@[?R@?1],[?P@?1])->forsomer@[?R@?1],[(?P@?1)|?Q@?1]";
ri "RL@forsomer3**(R@VALUE@[CSYM])** $forsomer3"; ex();
ri "(R@R@L@VALUE@[DSYM])**9pt25"; ex();
p "9pt26";

(* application of the new built-in tactic UNEVAL *)

s "(forall@?t)||?x,?y";
ri "LEFT@forall";
ri "RIGHT@LEFT@EVERYWHERE2@UNEVAL@?t";
ri "PIVOT";
ri "RIGHT@LEFT@EVERYWHERE2@EVAL";
ri "LEFT@ $forall";
p "UNIV_TAC";

s "(forall@[(?P@?1)=?Q@?1])";
ri "forall"; ri "EQUATION"; ex();
ri "PCASEINTRO@[?P@?1]=[?Q@?1]"; ex();
right(); left(); ri "EVERYWHERE2@UNEVAL@[?P@?1]"; ex();
ri "EVERYWHERE2@0|-|1"; ex();
ri "EVERYWHERE2@EVAL**REFLEX"; ex();
up(); right(); right(); left(); rri "(2|-|1)@false"; ex(); 
left(); left(); left(); ri "PCASEINTRO@(?P@?1)=?Q@?1"; ri "PIVOT"; ex();
left(); ri "BIND@?1"; ri "LEFT@0|-|2"; ri "EVAL"; up();ex();
up();up(); ri "REFLEX"; up(); ex();
uptors "CASEINTRO"; rri "CASEINTRO"; ex();
top(); rri "EQUATION"; ex();
p "UNIV_EQ";

s "(forall@[(?P@?1)=?Q@?1])||?t,?u";
ri "LEFT@UNIV_EQ"; ex();
right(); left(); ri "EVERYWHERE@UNEVAL@[?P@?1]"; ri "EVERYWHERE@0|-|1";
	ri "EVERYWHERE@EVAL";
top(); ri "LEFT@ $UNIV_EQ";
p "UNIV_EQ_TAC";

quit();