Next: Implementing stratified abstraction in Up: Implementing case expression logic Previous: Implementing case expression logic

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
```

Randall Holmes
2000-11-03