| ⊢ f ⊃ more ⇒ ⊢ f⋆ ⌢ g ≡ g ∨ (f ⌢ (f⋆ ⌢ g)) | ImpMoreChopStarChopEqvRule |
Proof:
1 | f ⊃ more | Assump |
2 | f⋆ ≡empty ∨ (f ⌢ f⋆) | |
3 | f⋆ ⌢ g ≡ (empty ∨ (f ⌢ f⋆)) ⌢ g | |
4 | (empty ∨ (f ⌢ f⋆)) ⌢ g ≡ (empty ⌢ g) ∨ ((f ⌢ f⋆) ⌢ g) | |
5 | empty ⌢ g ≡ g | |
6 | (f ⌢ f⋆) ⌢ g ≡ f ⌢ (f⋆ ⌢ g) | |
7 | f⋆ ⌢ g ≡ g ∨ (f ⌢ (f⋆ ⌢ g)) |
qed