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-2-eq, and


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 :


Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023