| ⊢ | f ≡ g∗ ; h ⇒ ⊢ f ≡ (g ; f) ∨ h | CSChopEqvChopOrRule |
Proof:
1 | ⊢ f ≡ g∗ ; h | given |
2 | ⊢ g∗≡empty ∨ (g ; g∗) | |
3 | ⊢ g∗ ; h ≡ h ∨ ((g ; g∗) ; h) | |
4 | ⊢ (g ; g∗) ; h ≡ g ; (g∗ ; h) | ChopAssoc |
5 | ⊢ g ; f ≡ g ; (g∗ ; h) | |
6 | ⊢ f ≡ (g ; f) ∨ h |
qed