| ⊢ | f∗∧more ∧¬f ⊃ (f ∧more) ; (f∗∧more) | CSMoreNotImpChopCSAndMore |
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∗∧more ∧¬f ⊃ (f ∧more) ; (f∗∧more) | |
6 | ⊢ f∗∧more ∧¬f ⊃ (f ∧more) ; (f∗∧more) |
qed