Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
b:
exp.
c:
. WHILE b DO c OD
Applied Tactic:
Unfolds ``while com`` 0 THEN UnivCD THENM MemTypeCD THEN Auto
Generated subgoals:
None
b:
exp. c:
. WHILE b DO c OD 