Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. P: . P[SKIP] (c1,c2:. P[c1] P[c2] P[c1; c2]) (v:Atom. e:Exp. P[v := e]) (b:exp. c1,c2:. P[c1] P[c2] P[IF b THEN c1 ELSE c2 ]) (b:exp. c:. P[c] P[WHILE b DO c OD]) {c:. P[c]}

Applied Tactic: Unfolds ``so_apply guard`` 0 THEN UnivCD THEN Auto
Generated subgoals:

1. P c