Next Prev Up
FinImpYieldsFin

⊢ fin w ⊃ f fin w FinImpYieldsFin

Proof:

1
⊢ f ; fin ¬w ⊃fin ¬w
ChopFinImpFin
2
⊢ fin ¬w ≡¬fin w
PTL
3
⊢ f ; fin ¬w ≡ f ; ¬fin w
2,RightChopEqvChop
4
⊢ f ; ¬fin w ⊃¬fin w
1, 2, 3,Prop
5
⊢ fin w ⊃¬(f ; ¬fin w)
4,Prop
6
⊢ fin w ⊃ f fin w
5, def. of 

qed

Next Prev Up

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