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∨ 1≤i≤n(wi ∧ w′i) for some natural number n ≥ 1 and n pairs of state formulas wi and w′i:
| ⊢ more ∧ T ≡∨ 1≤i≤n(wi ∧ w′i) | DfMoreAndNLoneEqvMoreAndNLone-1-eq |
Now by Theorem DfStateAndNextEqv any conjunction w ∧ w′ is deducibly equivalent to (w ∧ w′). Therefore the disjunction in DfMoreAndNLoneEqvMoreAndNLone-1-eq can be re-expressed as ∨ 1≤i≤n (wi ∧ w′i):
| ⊢ ∨ 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 (∨ 1≤i≤n(wi ∧ w′i)):
| ⊢ ∨ 1≤i≤n (wi ∧ w′i) ≡ (∨ 1≤i≤n(wi ∧ w′i)) | DfMoreAndNLoneEqvMoreAndNLone-3-eq |
The chain of the three equivalences
DfMoreAndNLoneEqvMoreAndNLone-1-eq,
DfMoreAndNLoneEqvMoreAndNLone-2-eq, and
DfMoreAndNLoneEqvMoreAndNLone-3-eq
yields the following:
| ⊢ more ∧ T ≡ (∨ 1≤i≤n(wi ∧ w′i)) |
We then apply Derived Rule DfEqvDf to the first 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 :