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