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