ITL
© 1996-2018







4 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 


¬ 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


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

Proof for :

1
w w

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

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


(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


((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


(w (f g)) (w f) g StateYieldsEqv


Proof:

1
w f ; (¬g) (w f) ; ¬g
2
(w ¬(f ; ¬g)) ≡¬((w f) ; ¬g)
1,Prop


w f (w f) StateAndDi


Proof:

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


f f DiNext


Proof:

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


w w DiNextState


Proof of :

1
w w
2
w w
3
w w
4
w w
1, 3, 4,EqvChain


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 

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

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 

Here is a corollary:


f ; g f (g g1) f ; g1 ChopAndYieldsMP


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


(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 


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 


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 


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


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 


f g (f f1) g AndYieldsA


Proof:

1
f f1 f
2
f g (f f1) g


f1 g (f f1) g AndYieldsB


Proof:

1
f f1 f1
2
f1 g (f f1) g


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 


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 


g f g BoxImpYields


Proof:

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


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 


g ⇒ ⊢ f g YieldsGen


Proof:

1
g
given
2
g
3
g f g
4
f g
2, 3,MP


(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 


(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


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 


empty f f EmptyYields


Proof:

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


( 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 


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


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 


f skip f NextImpSkipYields


Proof:

1
f f
2
skip f f
3
f skip f
1, 2,Prop


more skip ; true MoreEqvSkipChopTrue


Proof:

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


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


f ; more more ChopMoreImpMore


Proof:

1
f ; more more
2
more more
3
f ; more more
1, 2,ImpChain


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 

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

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 


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


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


¬f ¬f NotDiEqvBiNot


Proof:

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


f ; g f ChopImpDi


Proof:

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


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


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 


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 


(f g) f g DiOrEqv


Proof:

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


(f g) f DiAndA



(f g) g DiAndB


Proof of theorem DiAndA:

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


(f g) f g DiAndImpAnd


Proof:

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


skip more DiSkipEqvMore


Proof:

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


more more DiMoreEqvMore


Proof for :

1
( skip) true
2
skip more
3
skip more
4
more more
3, def. of more

Proof of :

1
more more


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 


empty DiEmpty


Proof:

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







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