Same-prefix transition-generated empty returns

This module isolates the part of concrete empty-return synchronization which is already forced by a transition-generated edge. Reading edges synchronize with every other edge using the existing concrete read theorem. Consequently only an epsilon-generated left edge paired with an epsilon or structural split edge remains.

The counted factorization below strengthens the transition side to an exact one-step retained return. This makes the remaining boundary-order question explicit rather than hiding it behind ordinary reachability.

def DPDA_to_LR.ConcreteEpsilonEmptyEdge {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (p : List (symbol T (Nonterminal M))) (q : State M) (suffix : List T) : Prop

Constructor-exact view of an epsilon-generated concrete empty edge.

Equations

• One or more equations did not get rendered due to their size.

def DPDA_to_LR.ConcreteSplitEmptyEdge {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (p : List (symbol T (Nonterminal M))) (q : State M) (suffix : List T) : Prop

Constructor-exact view of a structural split concrete empty edge.

Equations

• One or more equations did not get rendered due to their size.

def DPDA_to_LR.SamePrefixEpsilonReturnResidual {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (p : List (symbol T (Nonterminal M))) (q₁ q₂ : State M) (suffix₁ suffix₂ : List T) : Prop

Exact residual after dispatching all same-prefix cases involving a read edge.

Equations

• One or more equations did not get rendered due to their size.

theorem DPDA_to_LR.concreteTransitionEmptyReturn_samePrefix_state_eq_or_residual {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {q₁ q₂ : State M} {suffix₁ suffix₂ : List T} (edge₁ : ConcreteEmptyTransitionEdge M p q₁ suffix₁) (edge₂ : ConcreteEmptyEdge M p q₂ suffix₂) : q₁ = q₂ ∨ SamePrefixEpsilonReturnResidual M p q₁ q₂ suffix₁ suffix₂

At a common visible prefix, a transition-generated empty edge either has the same return state as the other edge, or the pair is exactly one of the two epsilon residuals.

def DPDA_to_LR.CountedConcreteEmptyTransitionInterval {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (completion suffix : List T) (q : State M) : Prop

Counted form of a transition-generated return. Unlike the general CountedConcreteEmptyReturnInterval, the retained return has exactly one PDA step.

Equations

• One or more equations did not get rendered due to their size.

theorem DPDA_to_LR.ConcreteEmptyTransitionEdge.countedIntervalAtCompletion {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {q : State M} {suffix completion : List T} (edge : ConcreteEmptyTransitionEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal completion)) : CountedConcreteEmptyTransitionInterval M completion suffix q

Exact one-step counted interval supplied by a transition-tagged edge at any selected completion of its prefix.

theorem DPDA_to_LR.samePrefixTransitionReturn_exists_countedIntervals {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {q₁ q₂ : State M} {suffix₁ suffix₂ completion : List T} (edge₁ : ConcreteEmptyTransitionEdge M p q₁ suffix₁) (edge₂ : ConcreteEmptyEdge M p q₂ suffix₂) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal completion)) : CountedConcreteEmptyTransitionInterval M completion suffix₁ q₁ ∧ CountedConcreteEmptyReturnInterval M completion suffix₂ q₂

Both exact counted intervals are available at one common completion of a same-prefix pair. This is the input expected by the retained-return nesting theorems; the remaining issue is to relate their boundary counts.