© 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 4,DfImpDf 6 w ⊃w 3, 5,ImpChain

qed

Proof for :

 1 w ⊃w 2 w ⊃w 3 w ⊃w 1, 2,ImpChain

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 ChopImpDf 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 BfAndChopImport 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) AndChopImpChopAndChop 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) StateAndChop 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 StateAndEmptyChop 3 (empty ∧ w) ⌢ f ≡ w ∧ f 1, 2,EqvChain

qed

 ⊢ (w ∧ f) ≡ w ∧f StateAndDf

Proof:

 1 (w ∧ f) ⌢ true ≡ w ∧ (f ⌢ true) StateAndChop 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 2,DfImpDf 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