CSChopEqvOrChopPlusChop

⊢

f^∗ ; g ≡ g ∨ f⁺ ; g

Proof:

1	⊢ f^∗≡empty ∨ f⁺	def. of ^∗
2	⊢ f^∗ ; g ≡ g ∨ f⁺ ; g	1,EmptyOrChopEqvRule

qed

2023-09-12