AndChopImpChopAndChop

(f f1) ⌢ g (f ⌢ g) (f1 ⌢ g) AndChopImpChopAndChop

Proof:

1
(f f1) ⌢ g f ⌢ g
2
(f f1) ⌢ g f1 ⌢ g
3
(f f1) ⌢ g (f ⌢ g) (f1 ⌢ g)
1, 2,Prop

qed

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