| ⊢ | (while w do f) ; g ≡if w then f ; (while w do f) ; g else g | WhileChopEqvIf |
Proof:
1 | ⊢ while w do f ≡if w then f ; (while w do f) else empty | |
2 | ⊢ (while w do f) ; g ≡ |
|
if w then (f ; while w do f) ; g else empty ; g | ||
3 | ⊢ (f ; while w do f) ; g ≡ f ; (while w do f) ; g | |
4 | ⊢ empty ; g ≡ g | |
5 | ⊢ (while w do f) ; g ≡if w then f ; (while w do f) ; g else g |
qed