| ⊢ | f∗≡empty ∨ (f ∧more) ; f∗ | CSEqv |
Proof:
1 | ⊢ f+ ≡ f ∨ (f ∧more) ; f+ | |
2 | ⊢ empty ≡¬more | |
3 | ⊢ empty ∨ f+ ≡empty ∨ (f ∧more) ∨ (f ∧more) ; f+ | |
4 | ⊢ (f ∧more) ; empty ≡ f ∧more | |
5 | ⊢ (f ∧more) ; (empty ∨ f+) ≡ |
|
(f ∧more) ; empty ∨ (f ∧more) ; f+ | ||
6 | ⊢ empty ∨ f+ ≡empty ∨ ((f ∧more) ; (empty ∨ f+)) | |
7 | ⊢ f∗≡empty ∨ (f ∧more) ; f∗ | 6, def. of ∗ |
qed