Prev Up

#### 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 ≡∨ 1≤i≤n(wi ∧ w′i) 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):

 ⊢ ∨ 1≤i≤n(wi ∧ w′i) ≡∨ 1≤i≤n (wi ∧ w′i) 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)):

 ⊢ ∨ 1≤i≤n (wi ∧ w′i) ≡ (∨ 1≤i≤n(wi ∧ w′i)) DfMoreAndNLoneEqvMoreAndNLone-3-eq

The chain of the three equivalences

yields the following:

 ⊢ more ∧ T ≡ (∨ 1≤i≤n(wi ∧ w′i))

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

 ⊢ (more ∧ T) ≡ (∨ 1≤i≤n(wi ∧ w′i))

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 :

 Prev Up

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