ITL
© 1996-2018







8.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

qed

Proof for :

1
w w
2
w w
3
w w

qed

w w BfState

Proof:

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

qed

w f w StateChop

Proof:

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

qed

(w f) g w StateChopExportA

Proof:

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

qed

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

w (f g) (w f) g StateAndChopImport

Proof:

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

qed

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

(w f) g w (f g) StateAndChop

Proof:

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

qed

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

(w empty) f w f StateAndEmptyChop

Proof:

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

qed

The following is a simple corollary of StateAndEmptyChop:

(empty w) f w f EmptyAndStateChop

Proof:

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

qed

(w f) w f StateAndDf

Proof:

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

qed

w f ⇒ ⊢ w f StateImpBfGen

Proof:

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 

qed

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

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

Proof:

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

qed







2018-10-21
Contact | Home | ITL home | Course | Proofs | Algebra | FL