| ⊢ | f∗ ; f∗⊃ f∗ | CSChopCSImpCS |
Proof:
1 | ⊢ f∗≡empty ∨ (f ∧more) ; f∗ | |
2 | ⊢ f∗ ; f∗≡ f∗∨ ((f ∧more) ; f∗) ; f∗ | |
3 | ⊢ f∗ ; f∗∧¬(f∗) ⊃ ((f ∧more) ; f∗) ; f∗∧¬((f ∧more) ; f∗) | |
4 | ⊢ ((f ∧more) ; f∗) ; f∗≡ (f ∧more) ; f∗ ; f∗ | |
5 | ⊢ f∗ ; f∗∧¬(f∗) ⊃ (f ∧more) ; f∗ ; f∗∧¬((f ∧more) ; f∗) | |
6 | ⊢ f ∧more ⊃more | |
7 | ⊢ f∗ ; f∗⊃ f∗ |
qed