ITL
© 1996-2018







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
2
true
3
true
1, 2,MP
4
⊢ ¬¬true
3, def. of 
5
⊢ ¬true false
6
¬true false
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

qed

Proof for :

1
w w

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
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
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
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
2
(w ¬(f ; ¬g)) ≡¬((w f) ; ¬g)
1,Prop

qed

w f (w f) StateAndDi

Proof:

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

qed

f f DiNext

Proof:

1
( f) ; true (f ; true)
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
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
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 fin w1 ⇒ ⊢ w (f w1) StateImpYields

Proof:

1
w f fin w1
given
2
w (f fin w1)
1,Prop
3
w (f fin w1)
4
(f fin w1) f w1
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
2
⊢ ¬¬g ¬(f ; ¬g)
1,Prop
3
g f g
2, def. of ,

qed

f true f BoxEqvTrueYields

Proof:

1
true ; ¬f ¬f
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
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)
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
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)
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
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
3
f skip f
1, 2,Prop

qed

more skip ; true MoreEqvSkipChopTrue

Proof:

1
skip ; true true
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
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)
4
more ; f
3, def. of 

qed

Proof of :

1
f true ; f
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
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
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
3
¬f ¬f
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
2
(f g) f g
1, def. of 

qed

(f g) f DiAndA

Proof:

1
(f g) ; true f ; true
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
4
more more
3, def. of more

qed

Proof of :

1
more more

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
3
empty ; true
1, 2,Prop
4
empty
3, def. of 

qed







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