| ⊢ | f ≡ (while w do g) ; h ⇒ f ≡if w then g ; f else h | WhileChopEqvIfRule |
Proof:
1 | ⊢ f ≡ (while w do g) ; h | given |
2 | ⊢ (while w do g) ; h ≡if w then g ; (while w do g) ; h else h | |
3 | ⊢ g ; f ≡ g ; (while w do g) ; h | |
4 | ⊢ f ≡if w then g ; f else h |
qed