Next Prev Up
CSEqvCS

⊢ f ≡ g ⇒ ⊢ f∗≡ g∗ CSEqvCS

Proof:

1
⊢ f ≡ g
given
2
⊢ f+ ≡ g+
1,ChopPlusEqvChopPlus
3
⊢ empty ∨ f+ ≡empty ∨ g+
2,Prop
4
⊢ f∗≡ g∗
3, def. of ∗

qed

Next Prev Up

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023