| ⊢ | while w do f ≡if w then f ; (while w do f) else empty | WhileEqvIf |
Proof:
1 | ⊢ while w do f ≡ (w ∧ f)∗∧fin ¬w | def. of while |
2 | ⊢ (w ∧ f)∗≡empty ∨ ((w ∧ f) ; (w ∧ f)∗) | |
3 | ⊢ empty ∧fin ¬w ≡¬w ∧empty | |
4 | ⊢ (w ∧ f) ; (w ∧ f)∗≡ w ∧ f ; (w ∧ f)∗ | |
5 | ⊢ (f ; (w ∧ f)∗) ∧fin ¬w ≡ f ; ((w ∧ f)∗∧fin ¬w) | |
6 | ⊢ f ; ((w ∧ f)∗∧fin ¬w) ≡ f ; while w do f | def. of while |
7 | ⊢ while w do f | |
≡ (¬w ∧empty) ∨ (w ∧ (f ; while w do f)) |
||
8 | ⊢ while w do f ≡if w then f ; (while w do f) else empty |
qed