AndChopAndCommute

(f g) ; (f1 g1) (g f) ; (g1 f1) AndChopAndCommute

Proof:

1
(f g) ; (f1 g1) (g f) ; (f1 g1)
2
(g f) ; (f1 g1) (g f) ; (g1 f1)
3
(f g) ; (f1 g1) (g f) ; (g1 f1)
1, 2,EqvChain

qed

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