(*
____________________________________________________________________
NOT_UNEXP:
?p || false , true =
~?p
["NOT","ODDCHOICE"]
____________________________________________________________________
*)

(* a needed theorem *)

ae "TAB_NOT";wb();p "NOT_UNEXP";

(*
____________________________________________________________________
RID_STUBBORN:

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

((?x & ?y) | (~?x) & ?z) || ?a , ?b
____________________________________________________________________
*)

(*
convers stubborn case statements into propositional logic statements
*)

s "?x||(?y||?a,?b),?z||?a,?b";
ri "($UNPACK)**ASRTCOND**LEFT@ $CONDCASES";ex();
p "RID_STUBBORN";

(*
____________________________________________________________________
CONT_APPLY @ ?thm:

?x =

((CONT_APPLY @ ?thm) *> ?thm) => ?x
____________________________________________________________________
*)

(*
continue applying ?thm as long as ?thm applies
*)

dpt "CONT_APPLY";
s "?x";
ri "(CONT_APPLY@?thm)*>?thm";
p "CONT_APPLY@?thm";

(*
____________________________________________________________________
ALL_APPLY_CASE @ ?thm:

?p || ?a , ?b =

?thm => ?p || ((ALL_APPLY_CASE @ ?thm) => ?a)
, (ALL_APPLY_CASE @ ?thm) => ?b
____________________________________________________________________
*)

(*
similar to EVERYWHERE, but specialized to apply only to cases and
nested cases for speed in the tautological routines 
*)

dpt "ALL_APPLY_CASE";
s "?p||?a,?b";
right();left();
ri "ALL_APPLY_CASE@?thm";
up();right();
ri "ALL_APPLY_CASE@?thm";
top();
ri "?thm";
p "ALL_APPLY_CASE@?thm";

s "?a||?b,?c";
right();left(); ri "?thm";
up();right(); ri "?thm";
p "RIGHTRL@?thm";

(*
____________________________________________________________________
ALL_APPLY_CASE_TD @ ?thm:

?p || ?a , ?b =

(RIGHT @ RL @ ALL_APPLY_CASE_TD @ ?thm) => ?thm
=> ?p || ?a , ?b
____________________________________________________________________
*)

(*
similar to TOPDOWN, but specialized to apply only to cases and
nested cases for speed in the tautological routines 
*)

dpt "ALL_APPLY_CASE_TD";
s "?p||?a,?b";
ri "?thm";
ri "RIGHTRL@ALL_APPLY_CASE_TD@?thm";
p "ALL_APPLY_CASE_TD@?thm";

(*
____________________________________________________________________
EVAL_CASES:

?p || ?a , ?b =

CASEINTRO <= ?p
|| (EVAL_CASES
   => (ALL_APPLY_CASE_TD @ CONT_APPLY @ 1 |-| 1)
   => ?a)
, EVAL_CASES
=> (ALL_APPLY_CASE_TD @ CONT_APPLY @ 1 |-| 1)
=> ?b
____________________________________________________________________
*)

(*
uses case assumptions to simplify a nested case statement in
which an value assumed to be true or false in that case is used
as a selector in an internal case statement
*)

dpt "EVAL_CASES";
s "?p||?a,?b";
right();left();
ri "ALL_APPLY_CASE_TD@CONT_APPLY@1|-|1";
ri "EVAL_CASES";
up();right();
ri "ALL_APPLY_CASE_TD@CONT_APPLY@1|-|1";
ri "EVAL_CASES";
top();
rri "CASEINTRO";
p "EVAL_CASES";

(*
____________________________________________________________________
DOLOOP @ ?thm:

?x . ?y =

(DOLOOP @ ?thm) =>> STOPLOOP => ?y . ?thm => ?y
____________________________________________________________________
*)

(*
looping procedure for applying ?thm and checking to see if anything
has been changed.
*)

dpt "DOLOOP";
s "?x.?y";
ri "IGNOREFIRST";ex();
ri "STARTLOOP";ex();
right();
ri "?thm";
up();
ri "STOPLOOP";
ari "DOLOOP@?thm";
p "DOLOOP@?thm";

(*
____________________________________________________________________
CASECOND:

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

|-?a || ?b , ?c
____________________________________________________________________
*)

(*CASECOND*)
s "|-?a||?b,?c";
ri "BIND@?a||?b,?c";ex();
ri "FNDIST";ex();
ri "EVERYWHERE@EVAL";ex();
wb();
p "CASECOND";

(*
____________________________________________________________________
CASE_BOOL:

?x || ?y , ?z =

ASSERT => CASECOND => ?x
|| (ASSERT2 => MAKE_BOOL => ?y) , ASSERT2
=> MAKE_BOOL => ?z
____________________________________________________________________
*)

(*
attempts to give a case statement a boolean label
*)

dpt "MAKE_BOOL";
s"?x||?y,?z";
right();left();
ri "MAKE_BOOL";
ri "ASSERT2";
up();right();
ri "MAKE_BOOL";
ri "ASSERT2";
top();
ri "CASECOND";
ri "ASSERT";
p "CASE_BOOL";

(*
____________________________________________________________________
MAKE_BOOL:

?p =

TYPES => ((?p = |-?p) ** ASSERT) =>> CASE_BOOL
=>> (?p = bool : ?p) => ?p
____________________________________________________________________
*)

(*
attempts to give a general expression a boolean label
*)

s "?p";
ri "(?p= bool:?p)";
ari "CASE_BOOL";
ari "(?p= |-?p)**ASSERT";
ri "TYPES";
p "MAKE_BOOL";

(*
____________________________________________________________________
CASE_MAKE:

?x =

ODDCHOICE <= EQUATION => BOOLDEF => MAKE_BOOL
=> ?x
____________________________________________________________________
*)

(*
attempts to convert a general expression into a case statement
*)

s "?x";
ri "MAKE_BOOL";
ri "BOOLDEF";
ri "EQUATION";
rri "ODDCHOICE";
p "CASE_MAKE";

(*
____________________________________________________________________
EXPAND_ALL:

?p || ?a , ?b =

UNPACK =>> CN_EXP =>> XOR_EXP =>> IFF_EXP
=>> IF_EXP =>> OR_EXP =>> AND_EXP =>> NOT_EXP
=> ?p || (EXPAND_ALL => ?a) , EXPAND_ALL => ?b
____________________________________________________________________
*)

(*
expands a case statement w/ a complicated selector into nested case
statements w/ simpler selectors
*)

dpt "EXPAND_ALL";
s "?p||?a,?b";
right();left();
ri "EXPAND_ALL";
up();right();
ri "EXPAND_ALL";
top();
ri "NOT_EXP";
ari "AND_EXP";
ari "OR_EXP";
ari "IF_EXP";
ari "IFF_EXP";
ari "XOR_EXP";
ari "CN_EXP";
ari "UNPACK";
p "EXPAND_ALL";

(*
____________________________________________________________________
STEP_ONE:

?p || ?a , ?b =

EVAL_CASES => EXPAND_ALL => ?p || ?a , ?b
____________________________________________________________________
*)

(*
attempts to simplify a case statement by partially simplifying
its selector and the selectors of nested cases and by using
the case assumptions in each section, it attempts to remove
redundant case expressions
*)

s "?p||?a,?b";
ri "EXPAND_ALL";
ri "EVAL_CASES";
p "STEP_ONE";

(*
____________________________________________________________________
TAUTNEW:

?x =

(DOLOOP @ STEP_ONE) => STARTLOOP => CASE_MAKE
=> ?x
____________________________________________________________________
*)

(*
simplify a boolean expression but leave it in case statement form
*)

s "?x";
ri "CASE_MAKE";
ri "STARTLOOP";
ri "DOLOOP@STEP_ONE";
p "TAUTNEW";

(*
____________________________________________________________________
COLLAPSE_ALL:

?p || ?a , ?b =

RID_STUBBORN =>> AND_EXP <<= OR_EXP <<= CN_EXP
<<= IF_EXP <<= XOR_EXP <<= IFF_EXP <= ?p
|| (COLLAPSE_ALL => ?a) , COLLAPSE_ALL => ?b
____________________________________________________________________
*)

(*
removes some of the levels of nesting by converting nested cases
in to a case statement w/ a more complex selector
*)

dpt"COLLAPSE_ALL";
s "?p||?a,?b";
right();left();
ri "COLLAPSE_ALL";
up();right();
ri "COLLAPSE_ALL";
top();
rri "IFF_EXP";
arri "XOR_EXP";
arri "IF_EXP";
arri "CN_EXP";
arri "OR_EXP";
arri "AND_EXP";
ari "RID_STUBBORN";
p "COLLAPSE_ALL";

(*
____________________________________________________________________
TAUTCOLLAPSE:

?p || ?a , ?b =

GCLEAN
=> (ALL_APPLY_CASE @ NOT_UNEXP ** ASSERT_UNEXP)
=> (DOLOOP @ COLLAPSE_ALL) => (?p || ?a , ?b) . ?p
|| ?a , ?b
____________________________________________________________________
*)

(*
takes the case expression form of a boolean expression and converts
it back to its propositional form
*)

s "?p||?a,?b";
ri "STARTLOOP";ex();
ri "DOLOOP@COLLAPSE_ALL";
ri "ALL_APPLY_CASE @ NOT_UNEXP**ASSERT_UNEXP";
ri "GCLEAN";
p "TAUTCOLLAPSE";

(*
____________________________________________________________________
COLLAPSE:

?x =

TAUTCOLLAPSE => TAUTNEW => ?x
____________________________________________________________________
*)

(*
simplify a boolean expression
*)

s "?x";
ri "TAUTNEW";
ri "TAUTCOLLAPSE";
p "COLLAPSE";

(*
____________________________________________________________________
SIMPLIFY_CASE:

?p || ?a , ?b =

EVAL_CASES => (DOLOOP @ EXPAND_ALL)
=> (?p || ?a , ?b) . ?p || ?a , ?b
____________________________________________________________________
*)

(*
expands a case statement out as far as it can and then gets rid
of unnecessary cases.
*)

s "?p||?a,?b";
ri "STARTLOOP";ex();
ri "DOLOOP@EXPAND_ALL";
ri "EVAL_CASES";
p "SIMPLIFY_CASE";

(*
____________________________________________________________________
THIRD_TAUT:

?x =

SIMPLIFY_CASE => CASE_MAKE => ?x
____________________________________________________________________
*)

(*
similar to TAUTNEW, but taking a slightly different approach
*)

s "?x";
ri "CASE_MAKE";
ri "SIMPLIFY_CASE";
p "THIRD_TAUT";

(*
____________________________________________________________________
SECOND_COLLAPSE:

?x =

TAUTCOLLAPSE => THIRD_TAUT => ?x
____________________________________________________________________
*)

(*
similar to COLLAPSE, but instead of using TAUTNEW, it uses
THIRD_TAUT
*)

s "?x";
ri "THIRD_TAUT";
ri "TAUTCOLLAPSE";
p "SECOND_COLLAPSE";

quit();