Level: Lib Thy Top:
Hypotheses:None
Conclusion:
T:
'. skip_case:T. seq_case:
T. assig_case:Atom Exp T. if_case:
exp
T.
while_case:exp T. c:.
case c
of SKIP skip_case
c1;c2 seq_case[c1;c2]
v := e assig_case[v;e]
IF (b1) c3 ELSE c4 if_case[b1;c3;c4]
WHILE (b2) c5 while_case[b2;c5]
T
Applied Tactic: Unfolds ``so_apply com_cases`` 0 THEN UnivCD THENA Auto
Generated subgoals:1. case c
of inl(sk) => skip_case
| inr(nsk) => case nsk
of inl(se) => let <c1,c2> = se in seq_case c1 c2
| inr(nse) => case nse
of inl(as) => let <v,e> = as in assig_case v e
| inr(nas) => case nas
of inl(i) => let <b1,c3c4> = i
in
let <c3,c4> = c3c4 in if_case b1 c3 c4
| inr(wh) => let <b2,c5> = wh in while_case b2 c5 T