| ⊢ while w do f ≡ (¬w ∧empty) ∨ (w ∧ (f ∧more) ; while w do f) | WhileEqvEmptyOrChopWhile |
Proof:
1 | ⊢ (w ∧ f)∗≡empty ∨ ((w ∧ f) ∧more) ; (w ∧ f)∗ | |
2 | ⊢ (w ∧ f) ∧more ≡ w ∧ (f ∧more) | |
3 | ⊢ ((w ∧ f) ∧more) ; (w ∧ f)∗≡ (w ∧ f ∧more) ; (w ∧ f)∗ | |
4 | ⊢ (w ∧ f)∗≡empty ∨ (w ∧ f ∧more) ; (w ∧ f)∗ | |
5 | ⊢ (w ∧ f)∗∧fin ¬w ≡ |
|
(empty ∧fin ¬w) ∨ ((w ∧ f ∧more) ; (w ∧ f)∗∧fin ¬w) | ||
6 | ⊢ empty ∧fin ¬w ≡¬w ∧empty | |
7 | ⊢ (w ∧ f ∧more) ; (w ∧ f)∗≡ w ∧ (f ∧more) ; (w ∧ f)∗ | |
8 | ⊢ (f ∧more) ; (w ∧ f)∗∧fin ¬w ≡ |
|
(f ∧more) ; ((w ∧ f)∗∧fin ¬w) | ||
9 | ⊢ (w ∧ f)∗∧fin ¬w ≡ |
|
(¬w ∧empty) ∨ (w ∧ (f ∧more) ; ((w ∧ f)∗∧fin ¬w)) | ||
10 | ⊢ while w do f ≡ |
|
(¬w ∧empty) ∨ (w ∧ (f ∧more) ; while w do f) | 9, def. of while |
qed