| ⊢ f ⊃ more ⇒ ⊢ f⋆ ≡empty ∨ (f ⌢ f⋆) | ImpMoreChopStarEqvRule |
Proof:
1 | f ⊃ more | Assump |
2 | f ∧more ≡ f | |
3 | (f ∧more) ⌢ f⋆ ≡ f ⌢ f⋆ | |
4 | f⋆ ≡empty ∨ ((f ∧more) ⌢ f⋆) | |
5 | f⋆ ≡empty ∨ (f ⌢ f⋆) |
qed