Next Prev Up
DfEqvDf

⊢ f ≡ g ⇒ ⊢ f ≡ g DfEqvDf

Proof:

1
f ≡ g
Assump
2
f ⌢ true ≡ g ⌢ true
1,LeftChopEqvChop
3
f ≡ g
2, def. of 

qed

Next Prev Up

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024