Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

n:. True {f := 1; i := 0; WHILE NOT i == n DO i := i + 1; f := i * f OD} [f] = (n)!

Applied Tactic: D 0 THENM Cut m.[f] = 1 [i] = 0 THENA Auto
Generated subgoals:

1. True {f := 1; i := 0} [f] = 1 [i] = 0

2. [f] = 1 [i] = 0 {WHILE NOT i == n DO i := i + 1; f := i * f OD} [f] = (n)!