Next Prev Up
DfDiamondEqvDiamondDf

⊢ f ≡ f DfDiamondEqvDiamondDf

Proof:

1
(true ⌢ f) ⌢ true ≡true ⌢ (f ⌢ true)
ChopAssoc
2
( f) ⌢ true ≡ (f ⌢ true)
1, def. of 
3
f ≡ f
2, def. of 

qed

Next Prev Up

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