| ⊢ | f+ ≡ f ∨ (f ; f+) | ChopPlusEqvOrChopChopPlus |
Proof for ⊃ :
1 | ⊢ f+ ≡ f ∨ (f ∧more) ; f+ | |
2 | ⊢ (f ∧more) ; f+ ⊃ f ; f+ | |
3 | ⊢ f+ ⊃ f ∨ f ; f+ |
qed
Proof for ⊂:
1 | ⊢ f ⊃ 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 | ⊢ f ∨ (f ; f+) ⊃ f+ |
qed