| ⊢ | ¬w ∧ f ⊃empty | WhileIntro | |
| ⊢ w ∧ f ⊃ (g ∧more) ; f | |||
| ⇒ ⊢ f ⊃while w do g |
Proof:
1 | ⊢ ¬w ∧ f ⊃empty | given |
2 | ⊢ w ∧ f ⊃ (g ∧more) ; f | given |
3 | ⊢ while w do g ≡ |
|
(¬w ∧empty) ∨ (w ∧ (g ∧more) ; while w do g) | ||
4 | ⊢ f ∧¬while w do g ⊃ |
|
(g ∧more) ; f ∧¬((g ∧more) ; while w do g) | ||
5 | ⊢ g ∧more ⊃more | |
6 | ⊢ f ⊃while w do g |
qed