ITL
© 1996-2018







17.3 Some Properties of Chop, and with State Formulas


w w DfState


Proof for

1
¬w ¬w
2
¬w ¬¬¬w
1, def. of 
3
¬¬w w
2,Prop
4
w ¬¬w
5
w ¬¬w
6
w w

Proof for

1
w w
2
w w
3
w w


w w BfState


1
¬w ≡¬w
2
¬¬w w
1,Prop
3
w w
2, def. of 


w f w StateChop


1
w f w
2
w w
3
w f w
1, 2,Prop


(w f) g w StateChopExportA


1
w f w
2
(w f) g w g
3
w g w
4
(w f) g w
2, 3,ImpChain

The following lets us move a state formula into the left side of chop:


w (f g) (w f) g StateAndChopImport


1
w w
2
w (f g) w (f g)
1,Prop
3
w (f g) (w f) g
4
w (f g) (w f) g
2, 3,ImpChain

We can easily combine this with theorem StateChopExportA to deduce the equivalence below:


(w f) g w (f g) StateAndChop


1
(w f) g w
2
(w f) g (w g) (f g)
3
(w f) g w (f g)
1, 2,Prop
4
w (f g) (w f) g
5
w (f g) (w f) g
3, 4,Prop

Below is a useful corollary of StateAndChop used in decomposing the left side of chop:


(w empty) f w f StateAndEmptyChop


1
(w empty) f w (empty f)
2
empty f f
3
(w empty) f w f
1, 2,Prop

The following is a simple corollary of StateAndEmptyChop:


(empty w) f w f EmptyAndStateChop


1
(empty w) f (w empty) f
2
(w empty) f w f
3
(empty w) f w f
1, 2,EqvChain


(w f) w f StateAndDf


1
(w f) true w (f true)
2
(w f) w f
1, def. of 


w f ⇒ ⊢ w f StateImpBfGen


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

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


f g ¬(f g1) f (g ¬g1) ChopAndNotChopImp


1
g (g ¬g1) g1
2
f g f (g ¬g1) f g1
3
f g ¬(f g1) f (g ¬g1)
2,Prop







2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL