Examples of reasoning about case expressions

- s "(?a=?b)||((?c=?b)||(?a+?b),?x),?y";
- right();left();right();left();left();    (* navigate 
                                           to term ?a *)

(?a = ?b) || ((?c = ?b) || ({?a} + ?b) , ?x) , ?y  
?a                                     (* the display *)

- lookhyps();     (* view locally relevant hypotheses *)

(* hypotheses displayed *)

1 (positive):  
?a  =  
?b

2 (positive):  
?c  =  
?b

(* end of hypothesis display *)

- ri "0|-|1"; ex();

(?a = ?b) || ((?c = ?b) || ({?b} + ?b) , ?x) , ?y  
?b                                    (* the display *)

- rri "0|-|2"; ex();         (* apply second hypothesis 
                             in converse sense *)

(?a = ?b) || ((?c = ?b) || ({?c} + ?b) , ?x) , ?y  
?c                                    (* the display *)

- rri "1|-|1"; ex();   (* introduce new case expression 
                               with first hypothesis *)

(?a = ?b) || ((?c = ?b) || ({(?a = ?b) || ?c , ?x_3} 
      + ?b) , ?x) , ?y                (* the display *)

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

- ri "1|-|1"; ex();

(?a = ?b) || ((?c = ?b) || ({?c} + ?b) , ?x) , ?y  
?c                                    (* the display *)

- up(); up(); right();

(?a = ?b) || ((?c = ?b) || (?c + ?b) , {?x}) , ?y  
?x                                    (* the display *)

- lookhyps();
(* hypotheses displayed *)

1 (positive):                (* note change of sense of 
                                   second hypothesis *)
?a  =  
?b

2 (negative):  
?c  =  
?b

(* end of hypothesis display *)

- rri "(2|-|2)@0"; ex();          (* introduce new case 
                       expression stipulating the value
                             to go in the new branch *)

(?a = ?b) || ((?c = ?b) || (?c + ?b) , {(?c = ?b) 
      || 0 , ?x}) , ?y

(?c = ?b) || 0 , ?x

(* sample definitions of propositional connectives *)

- defineinfix "NOT" "~?x" "?x||false,true";

NOT:  
~ ?x  =  
?x || false , true
NOT , 0

- defineinfix "AND" "?x&?y" 
                        "?x||(?y||true,false),false";

AND:  
?x & ?y  =  
?x || (?y || true , false) , false
AND , 0