Recall that NL^{1} 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 NL^{1} 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}(w_{i} ∧ w′_{i}) for some natural number n ≥ 1 and n pairs of state formulas w_{i} and
w′_{i}:

⊢ more ∧ T ≡∨
_{1≤i≤n}(w_{i} ∧ 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} (w_{i} ∧ w′_{i}):

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

⊢ ∨
_{1≤i≤n} (w_{i} ∧ w′_{i}) ≡ (∨
_{1≤i≤n}(w_{i} ∧ 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}(w_{i} ∧ w′_{i})) |

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

⊢ (more ∧ T) ≡ (∨
_{1≤i≤n}(w_{i} ∧ 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
NL^{1} formula T :

BfMoreImpNLoneEqvMoreImpNLone

MoreAndNLoneImpBfMoreImpNLone

BfSkipImpAndNextImpAndSkipAndChop

BfMoreImpImpBfSkipImp

BfMoreImpAndNextImpAndSkipAndChop

DfSkipAndNLoneEqvMoreAndNLone

DfSkipAndNLoneImpBfSkipImpNLone

NLoneAndSkipChopEqvNLoneAndNext

UntilEqv

UntilImpDiamond

MoreAndNLoneImpBfMoreImpNLone

BfSkipImpAndNextImpAndSkipAndChop

BfMoreImpImpBfSkipImp

BfMoreImpAndNextImpAndSkipAndChop

DfSkipAndNLoneEqvMoreAndNLone

DfSkipAndNLoneImpBfSkipImpNLone

NLoneAndSkipChopEqvNLoneAndNext

UntilEqv

UntilImpDiamond