Next
Prev
Up
RightChopEqvChop
⊢
g
≡
g
1
⇒ ⊢
(
f ⌢ g
)
≡
(
f ⌢ g
1
)
RightChopEqvChop
Proof:
1
g
≡
g
1
Assump
2
g
⊃
g
1
1
,
Prop
3
f ⌢ g
⊃
f ⌢ g
1
2
,
RightChopImpChop
4
g
1
⊃
g
1
,
Prop
5
f ⌢ g
1
⊃
f ⌢ g
4
,
RightChopImpChop
6
f ⌢ g
≡
f ⌢ g
1
3
,
5
,
Prop
qed
Next
Prev
Up
2023-09-12
Contact
|
Home
|
ITL home
|
Course
|
Proofs
|
Algebra
|
FL
© 1996-2023