Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

c:. m,m':Atom . <c;m> m'

Applied Tactic: Unfold `nat_evolves` 0 THEN Auto
Generated subgoals:

1. case cmm'.1 of SKIP nat_evolves_skip(cmm') c1;c2 nat_evolves_seq(ev;cmm';c1;c2) i := e nat_evolves_assig(cmm';i;e) IF (b1) c3 ELSE c4 nat_evolves_if(ev;cmm';b1;c3;c4) WHILE (b2) c5 nat_evolves_while(ev;cmm';b2;c5)

2. Mono{i}(ev,cmm'.case cmm'.1 of SKIP nat_evolves_skip(cmm') c1;c2 nat_evolves_seq(ev;cmm';c1;c2) i := e nat_evolves_assig(cmm';i;e) IF (b1) c3 ELSE c4 nat_evolves_if(ev;cmm';b1;c3;c4) WHILE (b2) c5 nat_evolves_while(ev;cmm';b2;c5) on (Atom ) (Atom ))