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