Next Prev Up
StateImpBfGen

⊢ w ⊃ f ⇒ ⊢ w ⊃ f StateImpBfGen

Proof:

1
w ⊃ f
Assump
2
¬f ⊃ ¬w
1,Prop
3
¬f ⊃ ¬w
2,DfImpDf
4
¬w ≡¬w
DfState
5
¬f ⊃ ¬w
3, 4,Prop
6
w ⊃ ¬¬f
5,Prop
7
w ⊃ f
6, def. of 

qed

The following theorem can be used to do induction over time with chop:

Next Prev Up

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