| ⊢ | f ∧fin w ≡ f ; (w ∧empty) | AndFinEqvChopStateAndEmpty |
Proof for ⊃ :
1 | ⊢ f ; empty ≡ f | |
2 | ⊢ empty ⊃ (w ∧empty) ∨ (¬w ∧empty) | |
3 | ⊢ f ; empty ⊃ f ; (w ∧empty) ∨ f ; (¬w ∧empty) | |
4 | ⊢ f ; (¬w ∧empty) ⊃ (¬w ∧empty) | |
5 | ⊢ (¬w ∧empty) ⊃¬fin w | |
6 | ⊢ f ⊃ f ; (w ∧empty) ∨¬fin w | |
7 | ⊢ f ∧fin w ⊃ f ; (w ∧empty) |
qed
Proof for ⊂:
1 | ⊢ f ; (w ∧empty) ⊃ f ; empty | |
2 | ⊢ f ; empty ≡ f | |
3 | ⊢ f ; (w ∧empty) ⊃ (w ∧empty) | |
4 | ⊢ (w ∧empty) ⊃fin w | |
5 | ⊢ f ; (w ∧empty) ⊃ f ∧fin w |
qed
The following is a lemma used in the proof of theorem FinChopEqvDiamond.