ITL
© 1996-2018







8.9 Some Properties of Skip, Next And Until

Recall that NL1 formulas are exactly those PTL formulas in which the only temporal operators are unnested s (e.g., P ¬P but not P ¬P ). The next theorem holds for any NL1 formula T :

(more T) more T DfMoreAndNLoneEqvMoreAndNLone

Proof 1 We use Axiom VPTL to re-express more T as a logically equivalent disjunction 1in(wi wi) for some natural number n 1 and n pairs of state formulas wi and wi:

more T 1in(wi wi) DfMoreAndNLoneEqvMoreAndNLone-1-eq

Now by Theorem DfStateAndNextEqv any conjunction w wis deducibly equivalent to (w w). Therefore the disjunction in DfMoreAndNLoneEqvMoreAndNLone-1-eq can be re-expressed as 1in (wi wi):

1in(wi wi) 1in (wi wi) DfMoreAndNLoneEqvMoreAndNLone-2-eq

Then by n 1 applications of Theorem DfOrEqv and some simple propositional reasoning, the righthand operand of this equivalence is itself is deducibly equivalent to ( 1in(wi wi)):

1in (wi wi) ( 1in(wi wi)) DfMoreAndNLoneEqvMoreAndNLone-3-eq

The chain of the three equivalences

DfMoreAndNLoneEqvMoreAndNLone-1-eq,

DfMoreAndNLoneEqvMoreAndNLone-2-eq, and

DfMoreAndNLoneEqvMoreAndNLone-3-eq

yields the following:

more T ( 1in(wi wi))

We then apply Derived Rule DfEqvDf to the first equivalence DfMoreAndNLoneEqvMoreAndNLone-1-eq:

(more T) ( 1in(wi wi))

The last two equivalences with simple propositional reasoning yield our goal DfMoreAndNLoneEqvMoreAndNLone.

Here is a corollary of the previous PITL Theorem DfMoreAndNLoneEqvMoreAndNLone for any NL1 formula T :

(more T) more T BfMoreImpNLoneEqvMoreImpNLone

Proof:

1
(more T) ≡¬¬(more T)
def. of 
2
¬(more T) more ¬T
3
¬(more T) (more ¬T)
4
(more ¬T) more ¬T
5
¬(more T) more ¬T
3, 4,EqvChain
6
(more T) ≡¬(more ¬T)
1, 5,Prop
7
¬(more ¬T) more T
8
(more T) more T
6, 7,EqvChain

qed

more T (more T) MoreAndNLoneImpBfMoreImpNLone

Proof:

1
(more T) more T
2
more T (more T)
1,Prop

qed

(skip f) g (skip f) g BfSkipImpAndNextImpAndSkipAndChop

Proof:

1
(skip f) (skip g) ((skip f) skip) g
2
(skip f) skip skip f
3
((skip f) skip) g (skip f) g
4
(skip f) (skip g) (skip f) g
1, 3,Prop
5
(skip f) g (skip f) g
4, def. of 

qed

(more f) (skip f) BfMoreImpImpBfSkipImp

Proof:

1
more skip
2
(more f) (skip f)
1,Prop
3
(more f) (skip f)

qed

(more f) g (skip f) g BfMoreImpAndNextImpAndSkipAndChop

Proof:

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

qed

(skip T) more T DfSkipAndNLoneEqvMoreAndNLone

Proof:

1
finite (skip T) (more T)
2
(skip T) (more T)
3
(skip T) (skip T)
4
(more T) more T
5
(skip T) more T
2 −−4,Prop

qed

(skip T) (skip T) DfSkipAndNLoneImpBfSkipImpNLone

Proof:

1
(skip T) more T
2
(skip ¬T) more ¬T
3
more T ¬(more T)
4
(skip T) ¬(skip ¬T)
1 −−3,Prop
5
skip ¬T ≡¬(skip T)
6
(skip ¬T) ¬(skip T)
7
¬(skip ¬T) ≡¬¬(skip T)
6,Prop
8
(skip T) ¬¬(skip T)
4, 7,Prop
9
(skip T) (skip T)
8, def. of 

qed

(skip T) f T f NLoneAndSkipChopEqvNLoneAndNext

Proof for :

1
(skip T) f (skip T)
2
(skip T) more T
3
(skip T) f T
1, 2,Prop
4
(skip T) f skip f
5
(skip T) f f
4, def. of 
6
(skip T) f T f
3, 5,Prop

qed

Proof for :

1
f more
2
more T (more T)
3
T f (more T)
1, 2,Prop
4
(more T) f (skip T) f
5
T f (skip T) f
3, 4,Prop

qed

T until f f (T (T until f)) UntilEqv

Proof:

1
skip T more
2
(skip T) f f ((skip T) ((skip T) f))
3
T until f f ((skip T) (T until f))
2, def. of  until
4
(skip T) (T until f) T (T until f)
5
T until f f (T (T until f))
3 −−4,Prop

qed

T until f f UntilImpDiamond

Proof:

1
(skip T) f f
2
T until f f
1, def. of  until

qed







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