#### 2.2 Further properties of Diamond-i and Box-i

 ⊢ f ⊃f ImpDi

Proof:

 1 ⊢ f ; empty ≡ f 2 ⊢ empty ⊃ true 3 ⊢ f ; empty ⊃ f ; true 4 ⊢ f ⊃ f ; true 1, 3,Prop 5 ⊢ f ⊃f 4, def. of

qed

 ⊢ ¬ false NotDiFalse

Proof:

 1 ⊢ true ⊃ true StateImpBi 2 ⊢ true 3 ⊢ true 1, 2,MP 4 ⊢ ¬¬true 3, def. of 5 ⊢ ¬true ≡ false 6 ⊢ ¬true ≡ false 5,DiEqvDi 7 ⊢ ¬ false 4, 6,Prop

qed

 ⊢ w ≡ w DiState

Proof for :

 1 ⊢ ¬w ⊃¬w 2 ⊢ ¬w ⊃¬¬¬w 1, def. of 3 ⊢ (¬w ⊃¬¬¬w) ⊃ ( ¬¬w ⊃w) 4 ⊢ ¬¬w ⊃ w 2, 3,MP 5 ⊢ w ⊃¬¬w 6 ⊢ w ⊃¬¬w 7 ⊢ w ⊃ w 4, 6,ImpChain

qed

Proof for :

 1 w ⊃w ImpDi

qed

Here are two important corollaries of DiState that are easy to prove:

 ⊢ w ; f ⊃ w. StateChop

 ⊢ (w ∧ f) ; g ⊃ w StateChopExportA

The following lets us move a state formula into the left side of a 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 BiAndChopImport 4 ⊢ w ∧ (f ; g) ⊃ (w ∧ f) ; g 2, 3,ImpChain

qed

With this proved, we can easily combine it with theorem StateChopExportA to deduce the following equivalence:

 ⊢ (w ∧ f) ; g ≡ w ∧ (f ; g) StateAndChop

A useful corollary 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

 ⊢ (w ∧f) ; g ≡ w ∧(f ; g) StateAndNextChop

Proof:

 1 ⊢ (w ∧f) ; g ≡ w ∧ ( f) ; g StateAndChop 2 ⊢ ( f) ; g ≡(f ; g) 3 ⊢ (w ∧f) ; g ≡ w ∧(f ; g) 1, 2,Prop

qed

 ⊢ ((w ∧ f) ; g) ≡w ∧(f ; g) NextStateAndChop

Proof:

 1 ⊢ (w ∧ f) ; g ≡ w ∧ f ; g 2 ⊢ ((w ∧ f) ; g) ≡(w ∧ f ; g) 3 ⊢ (w ∧ f ; g) ≡w ∧(f ; g) 4 ⊢ ((w ∧ f) ; g) ≡w ∧(f ; g) 2, 3,EqvChain

qed

 ⊢ (w ⊃(f g)) ≡ (w ∧ f) g StateYieldsEqv

Proof:

 1 ⊢ w ∧ f ; (¬g) ≡ (w ∧ f) ; ¬g StateAndChop 2 ⊢ (w ⊃¬(f ; ¬g)) ≡¬((w ∧ f) ; ¬g) 1,Prop

qed

 ⊢ w ∧f ≡(w ∧ f) StateAndDi

Proof:

 1 ⊢ w ∧ f ; true ≡ (w ∧ f) ; true StateAndChop 2 ⊢ w ∧f ≡(w ∧ f) 1, def. of

qed

 ⊢ f ≡f DiNext

Proof:

 1 ⊢ ( f) ; true ≡(f ; true) NextChop 2 ⊢ f ≡f 1, def. of

qed

 ⊢ w ≡w DiNextState

Proof of :

 1 ⊢ w ≡w 2 ⊢ w ≡ w 3 ⊢ w ≡w 4 ⊢ w ≡w 1, 3, 4,EqvChain

qed

 ⊢ w ⊃f ⇒ ⊢ w ⊃f StateImpBiGen

Proof:

 1 ⊢ w ⊃ f given 2 ⊢ ¬f ⊃¬w 1,Prop 3 ⊢ ¬f ⊃¬w 2,DiImpDi 4 ⊢ ¬w ≡¬w 5 ⊢ ¬f ⊃¬w 3, 4,Prop 6 ⊢ w ⊃¬¬f 5,Prop 7 ⊢ w ⊃f 6, def. of

qed

Let us now consider the following valuable theorem:

 ⊢ 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

Here is a related theorem for the yields operator:

 ⊢ f ; g ∧ f g1 ⊃ f ; (g ∧ g1) ChopAndYieldsImp

This shows how yields adds information to the right of a suitable chop formula.

Proof:

 1 ⊢ g ⊃ (g ∧ g1) ∨¬g1 2 ⊢ f ; g ⊃ f ; (g ∧ g1) ∨ f ; ¬g1 3 ⊢ f ; g ∧¬(f ; ¬g1) ⊃ f ; (g ∧ g1) 2,Prop 4 ⊢ f ; g ∧ f g1 ⊃ f ; (g ∧ g1) 3, def. of

qed

Here is a corollary:

 ⊢ f ; g ∧ f (g ⊃g1) ⊃ f ; g1 ChopAndYieldsMP

Proof:

 1 ⊢ f ; g ∧ f (g ⊃g1) ⊃ f ; (g ∧ (g ⊃g1)) 2 ⊢ g ∧ (g ⊃g1) ⊃ g1 3 ⊢ f ; (g ∧ (g ⊃g1)) ⊃ f ; g1 4 ⊢ f ; g ∧ f (g ⊃g1) ⊃ f ; g1 1, 3,ImpChain

qed

 ⊢ (f ∨ f1) g ≡ (f g) ∧ (f1 g) OrYieldsImp

Proof:

 1 ⊢ (f ∨ f1) ; ¬g ≡ f ; ¬g ∨ f1 ; ¬g OrChopEqv 2 ⊢ ¬((f ∨ f) ; ¬g) ≡¬(f ; ¬g) ∧¬(f1 ; ¬g) 1,Prop 3 ⊢ (f ∨ f1) g ≡ (f g) ∧ (f1 g) 2, def. of

qed

 ⊢ f ⊃f1 ⇒ ⊢ (f1 g) ⊃(f g) LeftYieldsImpYields

Proof:

 1 ⊢ f ⊃ f1 given 2 ⊢ f ; ¬g ⊃ f1 ; ¬g 3 ⊢ ¬(f1 ; ¬g) ⊃¬(f ; ¬g) 2,Prop 4 ⊢ f1 g ⊃ f g 3, def. of

qed

 ⊢ f ≡ f1 ⇒ ⊢ (f g) ≡ (f1 g) LeftYieldsEqvYields

Proof:

 1 ⊢ f ≡ f1 given 2 ⊢ f ; ¬g ≡ f1 ; ¬g 3 ⊢ ¬(f ; ¬g) ≡¬(f1 ; ¬g) 2,Prop 4 ⊢ f g ≡ f1 g 3, def. of

qed

 ⊢ w ∧ f ⊃ ﬁn w1 ⇒ ⊢ w ⊃(f w1) StateImpYields

Proof:

 1 ⊢ w ∧ f ⊃ ﬁn w1 given 2 ⊢ w ⊃ (f ⊃ ﬁn w1) 1,Prop 3 ⊢ w ⊃(f ⊃ ﬁn w1) 4 ⊢ (f ⊃ ﬁn w1) ≡ f w1 BiImpFinEqvYieldsState 5 ⊢ w ⊃(f w1) 3, 4,EqvChain

qed

 ⊢ w ∧ f ⊃f1 ⇒ ⊢ w ∧ (f1 g) ⊃(f g) StateAndYieldsImpYields

Proof:

 1 ⊢ w ∧ f ⊃ f1 given 2 ⊢ w ∧ (f ; ¬g) ⊃ f1 ; ¬g 3 ⊢ w ∧¬(f1 ; ¬g) ⊃¬(f ; ¬g) 2,Prop 4 ⊢ w ∧ (f1 g) ⊃ (f g) 3, def. of

qed

 ⊢ f g ⊃ (f ∧ f1) g AndYieldsA

Proof:

 1 ⊢ f ∧ f1 ⊃ f 2 ⊢ f g ⊃ (f ∧ f1) g

qed

 ⊢ f1 g ⊃ (f ∧ f1) g AndYieldsB

Proof:

 1 ⊢ f ∧ f1 ⊃ f1 2 ⊢ f1 g ⊃ (f ∧ f1) g

qed

 ⊢ g ⊃g1 ⇒ ⊢ (f g) ⊃(f g1) RightYieldsImpYields

Proof:

 1 ⊢ g ⊃ g1 given 2 ⊢ ¬g1 ⊃¬g 1,Prop 3 ⊢ f ; ¬g1 ⊃ f ; ¬g 4 ⊢ ¬(f ; ¬g) ⊃¬(f ; ¬g1) 3,Prop 5 ⊢ (f g) ⊃(f g1) 3, def. of

qed

 ⊢ g ≡ g1 ⇒ ⊢ (f g) ≡ (f g1) RightYieldsEqvYields

Proof:

 1 ⊢ g ≡ g1 given 2 ⊢ ¬g ≡¬g1 1,Prop 3 ⊢ f ; ¬g ≡ f ; ¬g1 4 ⊢ ¬(f ; ¬g) ≡¬(f ; ¬g1) 3,Prop 5 ⊢ f g ≡ f g1 4, def. of

qed

 ⊢ g ⊃ f g BoxImpYields

Proof:

 1 ⊢ f ; ¬g ⊃¬g ChopImpDiamond 2 ⊢ ¬¬g ⊃¬(f ; ¬g) 1,Prop 3 ⊢ g ⊃ f g 2, def. of ,

qed

 ⊢ f ≡ true f BoxEqvTrueYields

Proof:

 1 ⊢ true ; ¬f ≡¬f TrueChopEqvDiamond 2 ⊢ ¬(true ; ¬f) ≡¬¬f 1,Prop 3 ⊢ f ≡¬¬f 4 ⊢ f ≡¬(true ; ¬f) 2, 3,Prop 5 ⊢ f ≡ true f 4, def. of

qed

 ⊢ g ⇒ ⊢ f g YieldsGen

Proof:

 1 ⊢ g given 2 ⊢ g 3 ⊢ g ⊃ f g BoxImpYields 4 ⊢ f g 2, 3,MP

qed

 ⊢ (f g) ∧ (f g1) ≡ f (g ∧ g1) YieldsAndYieldsEqvYieldsAnd

Proof:

 1 ⊢ f ; (¬g ∨¬g1) ≡ (f ; ¬g) ∨ (f ; ¬g1) 2 ⊢ (f ; ¬g) ∨ (f ; ¬g1) ≡ f ; (¬g ∨¬g1) 1,Prop 3 ⊢ ¬g ∨¬g1 ≡¬(g ∧ g1) 4 ⊢ f ; (¬g ∨¬g1) ≡ f ; ¬(g ∧ g1) 5 ⊢ (f ; ¬g) ∨ (f ; ¬g1) ≡ f ; ¬(g ∧ g1) 2, 4,ImpChain 6 ⊢ ¬(f ; ¬g) ∧¬(f ; ¬g1) ≡¬(f ; ¬(g ∧ g1)) 5,Prop 7 ⊢ (f g) ∧ (f g1) ≡ f (g ∧ g1) 6, def. of

qed

 ⊢ (f g) ∧ (f1 g1) ⊃ (f ∧ f1) (g ∧ g1) YieldsAndYieldsImpAndYieldsAnd

Proof:

 1 ⊢ f g ⊃ (f ∧ f1) g 2 ⊢ f1 g1 ⊃ (f ∧ f1) g1 3 ⊢ (f ∧ f1) g ∧ (f ∧ f1) g1 ≡ (f ∧ f1) (g ∧ g1) YieldsAndYieldsEqvYieldsAnd 4 ⊢ (f g) ∧ (f1 g1) ⊃ (f ∧ f1) (g ∧ g1) 1, 2, 3,Prop

qed

 ⊢ f (g h) ≡ (f ; g) h YieldsYieldsEqvChopYields

Proof:

 1 ⊢ (f ; g) ; ¬h ≡ f ; (g ; ¬h) 2 ⊢ f ; (g ; ¬h) ≡ (f ; g) ; ¬h 1,Prop 3 ⊢ g ; ¬h ≡¬¬(g ; ¬h) 4 ⊢ f ; (g ; ¬h) ≡ f ; ¬¬(g ; ¬h) 5 ⊢ f ; ¬¬(g ; ¬h) ≡ (f ; g) ; ¬h 2, 4,Prop 6 ⊢ f ; ¬(g h) ≡ (f ; g) ; ¬h 5, def. of 7 ⊢ ¬(f ; ¬(g h)) ≡¬((f ; g) ; ¬h) 6,Prop 8 ⊢ f (g h) ≡ (f ; g) h 7, def. of

qed

 ⊢ empty f ≡ f EmptyYields

Proof:

 1 ⊢ empty ; ¬f ≡¬f EmptyChop 2 ⊢ ¬(empty ; ¬f) ≡ f 1,Prop 3 ⊢ empty f ≡ f 2, def. of

qed

 ⊢ ( f) g ≡(f g) NextYields

Proof:

 1 ⊢ ( f) ; ¬g ≡(f ; ¬g) NextChop 2 ⊢ ¬(( f) ; ¬g) ≡¬(f ; ¬g) 1,Prop 3 ⊢ ( f) g ≡¬(f ; ¬g) 2, def. of 4 ⊢ ¬(f ; ¬g) ≡¬(f ; ¬g) 5 ⊢ ( f) g ≡¬(f ; ¬g) 3, 4,Prop 6 ⊢ ( f) g ≡(f g) 5, def. of

qed

 ⊢ skip ; f ≡f SkipChopEqvNext

Proof:

 1 ⊢ ( empty) ; f ≡(empty ; f) 2 ⊢ empty ; f ≡ f 3 ⊢ (empty ; f) ≡f 4 ⊢ ( empty) ; f ≡f 1, 3,Prop 5 ⊢ skip ; f ≡f 4, def. of skip

qed

 ⊢ skip f ≡f SkipYieldsEqvWeakNext

Proof:

 1 ⊢ skip ; ¬f ≡¬f SkipChopEqvNext 2 ⊢ ¬(skip ; ¬f) ≡¬¬f 1,Prop 3 ⊢ ¬¬f ≡f 4 ⊢ ¬(skip ; ¬f) ≡f 2, 3,EqvChain 5 ⊢ skip f ≡f 4, def. of

qed

 ⊢ f ⊃ skip f NextImpSkipYields

Proof:

 1 ⊢ f ⊃f 2 ⊢ skip f ≡f SkipYieldsEqvWeakNext 3 ⊢ f ⊃ skip f 1, 2,Prop

qed

 ⊢ more ≡ skip ; true MoreEqvSkipChopTrue

Proof:

 1 ⊢ skip ; true ≡ true SkipChopEqvNext 2 ⊢ true ≡ skip ; true 1,Prop 3 ⊢ more ≡ skip ; true def. of more

qed

 ⊢ more ; f ⊃ more MoreChopImpMore

Proof:

 1 ⊢ ( true) ; f ≡(true ; f) 2 ⊢ (true ; f) ⊃ more 3 ⊢ ( true ; f) ⊃ more 1, 2,Prop 4 ⊢ more ; f ⊃ more 3, def. of more

qed

 ⊢ f ; more ⊃ more ChopMoreImpMore

Proof:

 1 ⊢ f ; more ⊃ more ChopImpDiamond 2 ⊢ more ⊃ more 3 ⊢ f ; more ⊃ more 1, 2,ImpChain

qed

 ⊢ more ; f ≡f MoreChopEqvNextDiamond

Proof of :

 1 ⊢ more ; f ≡ ( true) ; f def. of more 2 ⊢ ( true) ; f ≡(true ; f) 3 ⊢ more ; f ≡(true ; f) 1, 2,EqvChain 4 ⊢ more ; f ≡ 3, def. of

qed

Proof of :

 1 ⊢ f ⊃ true ; f DiamondImpTrueChop 2 ⊢ f ⊃(true ; f) 3 ⊢ ( true) ; f ≡(true ; f) 4 ⊢ more ; f ≡(true ; f) 3, def. of 5 ⊢ f ⊃ more ; f 2, 3, 4,Prop

qed

The following are is an easy corollary:

 ⊢ more f ≡f WeakNextBoxImpMoreYields

 ⊢ ¬f ≡ f more NotEqvYieldsMore

Proof:

 1 ⊢ f ; empty ≡ f 2 ⊢ ¬(f ; empty) ≡¬f 1,Prop 3 ⊢ empty ≡¬more def. of empty 4 ⊢ f ; empty ≡ f ; ¬more 5 ⊢ ¬(f ; empty) ≡¬(f ; ¬more) 4,Prop 6 ⊢ ¬f ≡¬(f ; ¬more) 2, 5,EqvChain 7 ⊢ ¬f ≡ f more 6, def. of

qed

 ⊢ f ⊃more ⇒ ⊢ f ; g ⊃more LeftChopImpMoreRule

Proof:

 1 ⊢ f ⊃ more given 2 ⊢ f ; g ⊃ more ; g 3 ⊢ more ; g ⊃ more 4 ⊢ f ; g ⊃ more 2, 3,ImpChain

qed

 ⊢ g ⊃more ⇒ ⊢ f ; g ⊃more RightChopImpMoreRule

Proof:

 1 ⊢ g ⊃ more given 2 ⊢ f ; g ⊃ f ; more 3 ⊢ f ; more ⊃ more 4 ⊢ f ; g ⊃ more 2, 3,ImpChain

qed

 ⊢ ¬f ≡¬f NotDiEqvBiNot

Proof:

 1 ⊢ f ≡¬¬f 2 ⊢ f ≡¬¬f 1,DiEqvDi 3 ⊢ ¬f ≡¬¬¬f 2,Prop 4 ⊢ ¬f ≡¬f 3, def. of

qed

 ⊢ f ; g ⊃f ChopImpDi

Proof:

 1 ⊢ g ⊃ true 2 ⊢ f ; g ⊃ f ; true 3 ⊢ f ; g ⊃f 2, def. of

qed

 ⊢ true ≡ true ; true TrueEqvTrueChopTrue

Proof:

 1 ⊢ true ; true ⊃ true 2 ⊢ true ⊃ true 3 ⊢ true ⊃ true ; true 2, def. of 4 ⊢ true ≡ true ; true 1, 3,Prop

qed

 ⊢ f ≡f DiEqvDiDi

Proof:

 1 ⊢ true ≡ true ; true TrueEqvTrueChopTrue 2 ⊢ f ; true ≡ f ; (true ; true) 3 ⊢ (f ; true) ; true ≡ f ; (true ; true) 4 ⊢ f ; true ≡ (f ; true) ; true 2, 3,Prop 5 ⊢ f ≡f 4, def. of

qed

 ⊢ f ≡f BiEqvBiBi

Proof:

 1 ⊢ ¬f ≡¬f 2 ⊢ ¬f ≡¬f DiNotEqvNotBi 3 ⊢ ¬f ≡¬f 2,DiEqvDi 4 ⊢ ¬f ≡¬f 1, 3,EqvChain 5 ⊢ ¬¬f ≡¬¬f 4,Prop 6 ⊢ f ≡f 5, def. of

qed

 ⊢ (f ∨ g) ≡f ∨g DiOrEqv

Proof:

 1 ⊢ (f ∨ g) ; true ≡ f ; true ∨ g ; true OrChopEqv 2 ⊢ (f ∨ g) ≡f ∨g 1, def. of

qed

 ⊢ (f ∧ g) ⊃f DiAndA

Proof:

 1 ⊢ (f ∧ g) ; true ⊃ f ; true AndChopA 2 ⊢ (f ∧ g) ⊃f 1, def. of

qed

 ⊢ (f ∧ g) ⊃g DiAndB

 ⊢ (f ∧ g) ⊃f ∧g DiAndImpAnd

Proof:

 1 ⊢ (f ∧ g) ⊃f 2 ⊢ (f ∧ g) ⊃g 3 ⊢ (f ∧ g) ⊃f ∧g 1, 2,Prop

qed

 ⊢ skip ≡ more DiSkipEqvMore

Proof:

 1 ⊢ skip ; true ≡ true 2 ⊢ true ≡ more 3 ⊢ skip ; true ≡ more 1, 2,Prop 4 ⊢ skip ≡ more 3, def. of

qed

 ⊢ more ≡ more DiMoreEqvMore

Proof for :

 1 ⊢ ( skip) ≡ true 2 ⊢ skip ⊃ more 3 ⊢ skip ⊃ more 1, 2,ImpChain 4 ⊢ more ⊃ more 3, def. of more

qed

Proof of :

 1 ⊢ more ⊃ more ImpDi

qed

 ⊢ f ≡ if w then g else h ⇒ ⊢f ≡ if w then g else h DiIfEqvRule

Proof:

 1 ⊢ f ≡ if w then g else h given 2 ⊢ f ; true ≡ if w then (g ; true) else (h ; true) 3 ⊢ f ≡ if w then g else h 2, def. of

qed

 ⊢ empty DiEmpty

Proof:

 1 ⊢ true 2 ⊢ empty ; true ≡ true EmptyChop 3 ⊢ empty ; true 1, 2,Prop 4 ⊢ empty 3, def. of

qed

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