| ⊢ | f∗∧more ⊃ f∗ ; f | CSAndMoreImpCSChop |
Proof:
1 | ⊢ f∗∧more ≡ (f ∧more) ; f∗ | |
2 | ⊢ empty ∨more | |
3 | ⊢ f∗⊃empty ∨ (f∗∧more) | |
4 | ⊢ (f ∧more) ; f∗⊃ (f ∧more) ∨ ((f ∧more) ; (f∗∧more)) | |
5 | ⊢ f∗∧more ∧¬f ⊃ (f ∧more) ; (f∗∧more) | |
6 | ⊢ f∗≡empty ∨ (f ∧more) ; f∗ | |
7 | ⊢ f∗ ; f ≡ f ∨ ((f ∧more) ; f∗) ; f | |
8 | ⊢ ((f ∧more) ; f∗) ; f ≡ (f ∧more) ; (f∗ ; f) | |
9 | ⊢ (f∗∧more) ∧¬(f∗ ; f) ⊃ |
|
(f ∧more) ; (f∗∧more) ∧¬((f ∧more) ; (f∗ ; f)) | ||
10 | ⊢ f ∧more ⊃more | |
11 | ⊢ f∗∧more ⊃ f∗ ; f |
qed
The following lemma is used in the proof of CSAndMoreImpCSChop: