| ⊢ | w ∧ f∗≡ w ∧ ( w ∧ f)∗ | BoxStateAndCSEqvCS |
Proof for ⊃ :
1 | ⊢ w ⊃ w | |
2 | ⊢ f∗∧more ≡ (f ∧more) ; f∗ | |
3 | ⊢ w ∧ ((f ∧more) ; f∗) ≡ ( w ∧ f ∧more) ; ( w ∧ f∗) | |
4 | ⊢ w ∧ f ∧more ⊃ ( w ∧ f) ∧more | |
5 | ⊢ ( w ∧ f ∧more) ; ( w ∧ f∗) ⊃ |
|
(( w ∧ f) ∧more) ; ( w ∧ f∗) | ||
6 | ⊢ ( w ∧ f∗) ∧more ⊃ (( w ∧ f) ∧more) ; ( w ∧ f∗) | |
7 | ⊢ w ∧ f∗⊃ ( w ∧ f)∗ | |
8 | ⊢ w ∧ f∗⊃ w ∧ ( w ∧ f)∗ |
qed
Proof for ⊂:
1 | ⊢ ( w ∧ f)∗⊃ ( w)∗ | |
2 | ⊢ w ∧ ( w)∗≡ w | |
3 | ⊢ ( w ∧ f)∗⊃ f∗ | |
4 | ⊢ w ∧ ( w ∧ f)∗⊃ w ∧ f∗ |
qed
See also the lemma BoxStateAndChopEqvChop for chop.