Next Up
DfDfEqvDf

⊢ f ≡ f DfDfEqvDf

Proof:

1
(f ⌢ true) ⌢ true ≡ f ⌢ (true ⌢ true)
ChopAssoc
2
true ≡true
DfState
3
(true ⌢ true) ≡true
2, def. of 
4
f ⌢ (true ⌢ true) ≡ f ⌢ true
3,LeftChopEqvChop
5
(f ⌢ true) ⌢ true ≡ f ⌢ true
1, 4,EqvChain
6
f ≡ f
5, def. of 

qed

Next Up

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