#### 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 :

 ⊢ (more ⊃T) ≡ more ⊃T BfMoreImpNLoneEqvMoreImpNLone

Proof:

 1 (more ⊃T) ≡¬¬(more ⊃T) def. of 2 ¬(more ⊃T) ≡ more ∧¬T 3 ¬(more ⊃T) ≡(more ∧¬T) 2,DfEqvDf 4 (more ∧¬T) ≡ more ∧¬T DfMoreAndNLoneEqvMoreAndNLone 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 BfMoreImpNLoneEqvMoreImpNLone 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 BfSkipImpAndNextImpAndSkipAndChop 3 (more ⊃f) ∧g ⊃(skip ∧ f) ⌢ g 1, 2,Prop

qed

 ⊢ (skip ∧ T) ≡ more ∧ T DfSkipAndNLoneEqvMoreAndNLone

Proof:

 1 ﬁnite ⊃(skip ∧ T) ≡ (more ∧ T) 2 (skip ∧ T) ≡(more ∧ T) 3 (skip ∧ T) ≡(skip ∧ T) 4 (more ∧ T) ≡ more ∧ T DfMoreAndNLoneEqvMoreAndNLone 5 (skip ∧ T) ≡ more ∧ T 2 −−4,Prop

qed

 ⊢ (skip ∧ T) ⊃(skip ⊃T) DfSkipAndNLoneImpBfSkipImpNLone

Proof:

 1 (skip ∧ T) ≡ more ∧ T DfSkipAndNLoneEqvMoreAndNLone 2 (skip ∧¬T) ≡ more ∧¬T DfSkipAndNLoneEqvMoreAndNLone 3 more ∧ T ⊃¬(more ∧ T) 4 (skip ∧ T) ⊃¬(skip ∧¬T) 1 −−3,Prop 5 skip ∧¬T ≡¬(skip ⊃T) 6 (skip ∧¬T) ≡¬(skip ⊃T) 5,DfEqvDf 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 DfSkipAndNLoneEqvMoreAndNLone 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 BfMoreImpAndNextImpAndSkipAndChop 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) NLoneAndSkipChopEqvNLoneAndNext 5 T until f ≡ f ∨(T ∧(T until f)) 3 −−4,Prop

qed

 ⊢ T until f ⊃f UntilImpDiamond

Proof:

 1 (skip ∧ T)⋆ ⌢ f ⊃f ChopImpDiamond 2 T until f ⊃f 1, def. of  until

qed

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