| ⊢ | f ≡if w then f1 else f2 ⇒ ⊢ f ; g ≡if w then (f1 ; g) else (f2 ; g) | IfChopEqvRule |
Proof:
1 | ⊢ f ≡if w then f1 else f2 | given |
2 | ⊢ f ≡ (w ∧ f1) ∨ (¬w ∧ f2) | |
3 | ⊢ f ; g ≡ (w ∧ f1) ; g ∨ (¬w ∧ f2) ; g | |
4 | ⊢ (w ∧ f1) ; g ≡ w ∧ (f1 ; g) | |
5 | ⊢ (¬w ∧ f2) ; g ≡¬w ∧ (f2 ; g) | |
6 | ⊢ f ; g ≡ (w ∧ f1 ; g) ∨ (¬w ∧ f2 ; g) | |
7 | ⊢ f ; g ≡if w then f1 ; g else f2 ; g |
qed