| ⊢ | halt w ; f ≡if w then f else (halt w ; f) | HaltChopEqv |
Proof:
1 | ⊢ halt w ≡if w then empty else halt w | |
2 | ⊢ halt w ; f ≡if w then empty ; f else ( halt w) ; f | |
3 | ⊢ empty ; f ≡ f | |
4 | ⊢ ( halt w) ; f ≡ (halt w ; f) | |
5 | ⊢ halt w ; f ≡if w then f else (halt w ; f) | |
qed