Empty-list returns on an active characteristic spine

An empty-list rule removes its active marker completely, so the final-list cancellation used for nonbase productions is unavailable. This file isolates the corresponding return problem and records the exact terminal displacement forced by equality of the two post-return forms.

theorem DPDA_to_LR.append_terminals_eq_cases {T : Type} [Fintype T] {N : Type} {p₁ p₂ : List (symbol T N)} {s₂ y : List T} (h : p₂ ++ List.map symbol.terminal s₂ = p₁ ++ List.map symbol.terminal y) : (∃ (z : List T), p₁ = p₂ ++ List.map symbol.terminal z ∧ s₂ = z ++ y) ∨ ∃ (z : List T), p₂ = p₁ ++ List.map symbol.terminal z ∧ y = z ++ s₂

If two prefixes become equal after terminal suffixes are appended, one prefix extends the other by a terminal word, and the same word is transferred between the suffixes.

theorem DPDA_to_LR.cancel_final_nonterminal {T : Type} [Fintype T] {N : Type} {p₁ p₂ : List (symbol T N)} {A₁ A₂ : N} {s₁ s₂ : List T} (h : p₂ ++ [symbol.nonterminal A₂] ++ List.map symbol.terminal s₂ = p₁ ++ [symbol.nonterminal A₁] ++ List.map symbol.terminal s₁) : p₂ = p₁ ∧ A₂ = A₁ ∧ s₂ = s₁

A displayed final nonterminal followed only by terminals is a unique right marker, even when arbitrary nonterminals occur in its prefix.

def DPDA_to_LR.EmptyListSpinesUnique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Prop

Spine-native form of the remaining empty-return uniqueness property.

Equations

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

theorem DPDA_to_LR.emptyListHandlesUnique_of_spines {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (h : EmptyListSpinesUnique M) : EmptyListHandlesUnique M

A spine-level empty-return theorem supplies the exact semantic property expected by the LR-core reduction.

The three possible incoming edges of an empty-list occurrence

inductive DPDA_to_LR.EmptyBaseEdge {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : List (symbol T (Nonterminal M)) → State M → List T → Prop

A normalized top spine edge whose child is list q [] q.

• read {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {suffix : List T} {source : State M} {a : T} {Z : StackSymbol M} {q : State M} (hparent : ActiveSpine M p (PDA_to_CFG.N.single source Z q) suffix) (htransition : (q, []) ∈ (emptyStackPDA M).transition_fun source a Z) (hrule : (PDA_to_CFG.N.single source Z q, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list q [] q)]) ∈ (characteristicGrammar M).rules) : EmptyBaseEdge M (p ++ [symbol.terminal a]) q suffix
• epsilon {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {suffix : List T} {source : State M} {Z : StackSymbol M} {q : State M} (hparent : ActiveSpine M p (PDA_to_CFG.N.single source Z q) suffix) (htransition : (q, []) ∈ (emptyStackPDA M).transition_fun' source Z) (hrule : (PDA_to_CFG.N.single source Z q, [symbol.nonterminal (PDA_to_CFG.N.list q [] q)]) ∈ (characteristicGrammar M).rules) : EmptyBaseEdge M p q suffix
• split {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {suffix : List T} {source : State M} {Z : StackSymbol M} {q : State M} (hparent : ActiveSpine M p (PDA_to_CFG.N.list source [Z] q) suffix) (hlength : ↑[Z].length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hrule : (PDA_to_CFG.N.list source [Z] q, [symbol.nonterminal (PDA_to_CFG.N.single source Z q), symbol.nonterminal (PDA_to_CFG.N.list q [] q)]) ∈ (characteristicGrammar M).rules) : EmptyBaseEdge M (p ++ [symbol.nonterminal (PDA_to_CFG.N.single source Z q)]) q suffix

inductive DPDA_to_LR.EmptyTransitionEdge {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : List (symbol T (Nonterminal M)) → State M → List T → Prop

An empty return generated by an actual PDA transition, rather than by the structural empty right child of a stack split.

• read {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {suffix : List T} {source : State M} {a : T} {Z : StackSymbol M} {q : State M} (hparent : ActiveSpine M p (PDA_to_CFG.N.single source Z q) suffix) (htransition : (q, []) ∈ (emptyStackPDA M).transition_fun source a Z) (hrule : (PDA_to_CFG.N.single source Z q, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list q [] q)]) ∈ (characteristicGrammar M).rules) : EmptyTransitionEdge M (p ++ [symbol.terminal a]) q suffix
• epsilon {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {suffix : List T} {source : State M} {Z : StackSymbol M} {q : State M} (hparent : ActiveSpine M p (PDA_to_CFG.N.single source Z q) suffix) (htransition : (q, []) ∈ (emptyStackPDA M).transition_fun' source Z) (hrule : (PDA_to_CFG.N.single source Z q, [symbol.nonterminal (PDA_to_CFG.N.list q [] q)]) ∈ (characteristicGrammar M).rules) : EmptyTransitionEdge M p q suffix

theorem DPDA_to_LR.EmptyTransitionEdge.baseEdge {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} (h : EmptyTransitionEdge M p q suffix) : EmptyBaseEdge M p q suffix

Forgetting the transition-only tag gives the corresponding normalized empty edge.

theorem DPDA_to_LR.EmptyBaseEdge.split_shape_of_not_transition {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} (h : EmptyBaseEdge M p q suffix) (hnot : ¬EmptyTransitionEdge M p q suffix) : ∃ (base : List (symbol T (Nonterminal M))) (source : State M) (Z : StackSymbol M), p = base ++ [symbol.nonterminal (PDA_to_CFG.N.single source Z q)]

A normalized empty edge which is not transition-generated has the exact visible-prefix shape of the right child of a split.

inductive DPDA_to_LR.SingleBaseEdge {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : List (symbol T (Nonterminal M)) → State M → StackSymbol M → State M → List T → Prop

The only possible incoming spine edge of a characteristic single nonterminal. Its parent is the corresponding nonempty list node, and the terminal word stored in the child's suffix is exactly the completed right sibling of that split.

• split {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {parentSuffix z : List T} {source middle target : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (hparent : ActiveSpine M p (PDA_to_CFG.N.list source (Z :: gamma) target) parentSuffix) (hlength : ↑(Z :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hrule : (PDA_to_CFG.N.list source (Z :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single source Z middle), symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)]) ∈ (characteristicGrammar M).rules) (hright : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)] (List.map symbol.terminal z)) : SingleBaseEdge M p source Z middle (z ++ parentSuffix)

theorem DPDA_to_LR.singleBaseEdge_of_activeSpine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {source target : State M} {Z : StackSymbol M} {suffix : List T} (h : ActiveSpine M p (PDA_to_CFG.N.single source Z target) suffix) : SingleBaseEdge M p source Z target suffix

Every reachable active single occurrence is the left child of one split edge.

theorem DPDA_to_LR.emptyBaseEdge_of_activeSpine {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} (h : ActiveSpine M p (PDA_to_CFG.N.list q [] q) suffix) : EmptyBaseEdge M p q suffix

Every active empty-list occurrence was introduced by exactly one of the three normalized edge forms above.

Operational factorization of an empty return

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

Completing the visible prefix of an empty-list edge exposes one complete net-pop segment. The segment starts just before the edge's parent, removes its displayed stack symbol, and ends at the empty-list state with the saved stack context restored.

Equations

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

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

Transition-generated empty returns have the stronger factorization in which the net-pop segment consists of exactly one PDA step.

Equations

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

theorem DPDA_to_LR.EmptyBaseEdge.returnRun {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 preWord : List T} (edge : EmptyBaseEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) : EmptyReturnRun M preWord suffix q

Every normalized empty edge has an exact useful net-pop run after any chosen terminal completion of its visible prefix.

theorem DPDA_to_LR.EmptyTransitionEdge.transitionRun {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 preWord : List T} (edge : EmptyTransitionEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) : EmptyTransitionRun M preWord suffix q

The one-step specialization of EmptyBaseEdge.returnRun for an actual read or epsilon transition edge.

theorem DPDA_to_LR.EmptyBaseEdge.prefixCompletion {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} (edge : EmptyBaseEdge M p q suffix) : ∃ (preWord : List T), (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)

Every visible prefix of an empty edge has a terminal completion. In the split case this explicitly completes the exposed left single; the retained split rule guarantees that this nonterminal is productive.

theorem DPDA_to_LR.EmptyBaseEdge.concrete {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 preWord : List T} (edge : EmptyBaseEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) : ConcreteEmptyEdge M p q suffix

A chosen terminal completion of the visible prefix upgrades a normalized empty edge to its exact-context concrete form.

theorem DPDA_to_LR.EmptyTransitionEdge.concrete {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 preWord : List T} (edge : EmptyTransitionEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal preWord)) : ConcreteEmptyTransitionEdge M p q suffix

A chosen completion similarly upgrades a transition-tagged empty edge.

theorem DPDA_to_LR.EmptyBaseEdge.exists_concrete {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} (edge : EmptyBaseEdge M p q suffix) : ConcreteEmptyEdge M p q suffix

Every syntax-facing empty edge has a concrete exact-context witness.

theorem DPDA_to_LR.EmptyTransitionEdge.exists_concrete {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} (edge : EmptyTransitionEdge M p q suffix) : ConcreteEmptyTransitionEdge M p q suffix

Every syntax-facing transition edge has a concrete transition witness.

theorem DPDA_to_LR.EmptyBaseEdge.exists_returnRun {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} (edge : EmptyBaseEdge M p q suffix) : ∃ (preWord : List T), EmptyReturnRun M preWord suffix q

An empty edge therefore always admits at least one concrete useful net-pop factorization.

The exact semantic return residual

def DPDA_to_LR.EmptyReturnEdgesUnique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Prop

Uniqueness of normalized empty-return edges. All grammar syntax has already been eliminated from this statement: its two witnesses are precisely the three possible incoming edges of an active list q [] q node.

This is the empty-handle counterpart of IntroducingEdgesUnique. The remaining proof is the useful-path/no-epsilon-cycle argument for the normalized DPDA; the adapters below contain the entire derivation-spine and rule-shape assembly.

Equations

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

theorem DPDA_to_LR.emptyReturnEdgesUnique_of_concretePairsClassified {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (h : ConcreteEmptyReturnPairsClassified M) : EmptyReturnEdgesUnique M

A concrete paired-return classifier supplies normalized empty-return edge uniqueness. The synchronization proof may be plugged in here once available.

theorem DPDA_to_LR.emptyListSpinesUnique_of_returnEdges {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (h : EmptyReturnEdgesUnique M) : EmptyListSpinesUnique M

Normalized empty-return edge uniqueness implies the spine-native property used by the grammar proof.

theorem DPDA_to_LR.emptyListHandlesUnique_of_returnEdges {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (h : EmptyReturnEdgesUnique M) : EmptyListHandlesUnique M

Normalized empty-return edge uniqueness supplies the exact base-rule obligation expected by the LR core.

theorem DPDA_to_LR.characteristicGrammar_coreIsLR1_of_edgeSemantics {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hedges : IntroducingEdgesUnique M) (hreturns : EmptyReturnEdgesUnique M) : (characteristicGrammar M).CoreIsLRk 1

The complete unaugmented LR(1) core, parameterized only by the two normalized operational uniqueness statements.

theorem DPDA_to_LR.characteristicGrammar_isLR1_of_edgeSemantics {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hedges : IntroducingEdgesUnique M) (hreturns : EmptyReturnEdgesUnique M) : (characteristicGrammar M).IsLRk 1

The complete augmented LR(1) result, with every grammar-syntactic case already discharged.