| ⊢ (w ∧ f) ⌢ g ≡ w ∧ (f ⌢ g) | StateAndChop |
Proof:
1 | (w ∧ f) ⌢ g ⊃ w | |
2 | (w ∧ f) ⌢ g ⊃ (w ⌢ g) ∧ (f ⌢ g) | |
3 | (w ∧ f) ⌢ g ⊃ w ∧ (f ⌢ g) | |
4 | w ∧ (f ⌢ g) ⊃ (w ∧ f) ⌢ g | |
5 | w ∧ (f ⌢ g) ≡ (w ∧ f) ⌢ g |
qed
Below is a useful corollary of StateAndChop used in decomposing the left side of chop: