Synchronizing concrete empty returns

Empty-list occurrences forget the stack symbol removed by their introducing edge. The concrete edge types below retain that edge together with the exact outer stack context supplied by ConcreteOperationalSpine. They are kept independent of EmptyReturns so that the latter can adapt its syntax-facing edge types without creating an import cycle.

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

The two impossible operational outcomes of a genuinely distinct pair of useful empty returns. This definition is syntax-independent and can be shared by both the concrete synchronization proof and its grammar adapter.

Equations

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

theorem DPDA_to_LR.noUsefulReturnObstruction {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : ¬UsefulReturnObstruction M

Useful cycles and nonempty stack self-embeddings are excluded by the normalized FS→ES kernels.

inductive DPDA_to_LR.ConcreteEmptyEdge {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 concrete normalized edge introducing an active list q [] q node. The chosen terminal completion and exact physical context are existential in the constructors and therefore do not burden the syntax-facing indices.

• read {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {suffix preWord : List T} {context : List (StackSymbol M)} {source : State M} {a : T} {Z : StackSymbol M} {q : State M} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.single source Z q) suffix preWord context) (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) : ConcreteEmptyEdge 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 preWord : List T} {context : List (StackSymbol M)} {source : State M} {Z : StackSymbol M} {q : State M} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.single source Z q) suffix preWord context) (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) : ConcreteEmptyEdge 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 preWord leftWord : List T} {context : List (StackSymbol M)} {source : State M} {Z : StackSymbol M} {q : State M} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.list source [Z] q) suffix preWord context) (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) (hleft : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source Z q)] (List.map symbol.terminal leftWord)) : ConcreteEmptyEdge M (p ++ [symbol.nonterminal (PDA_to_CFG.N.single source Z q)]) q suffix

inductive DPDA_to_LR.ConcreteEmptyTransitionEdge {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

The transition-generated concrete empty edges, excluding structural split-right introductions.

• read {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {suffix preWord : List T} {context : List (StackSymbol M)} {source : State M} {a : T} {Z : StackSymbol M} {q : State M} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.single source Z q) suffix preWord context) (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) : ConcreteEmptyTransitionEdge 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 preWord : List T} {context : List (StackSymbol M)} {source : State M} {Z : StackSymbol M} {q : State M} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.single source Z q) suffix preWord context) (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) : ConcreteEmptyTransitionEdge M p q suffix

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

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

theorem DPDA_to_LR.ConcreteEmptyEdge.transitionEdge_of_strictTerminalExtension {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p base : List (symbol T (Nonterminal M))} {q : State M} {suffix z : List T} (edge : ConcreteEmptyEdge M p q suffix) (hp : p = base ++ List.map symbol.terminal z) (hz : z ≠ []) : ConcreteEmptyTransitionEdge M p q suffix

An empty edge at a prefix which strictly extends another prefix by terminals cannot be a structural split-right edge: such an edge ends in a nonterminal marker. It is therefore transition-generated.

theorem DPDA_to_LR.ConcreteEmptyEdge.exists_childSpine {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 : ConcreteEmptyEdge M p q suffix) : ∃ (preWord : List T) (context : List (StackSymbol M)), ConcreteOperationalSpine M p (PDA_to_CFG.N.list q [] q) suffix preWord context

The child of a concrete empty edge is itself a concrete normalized spine, with the same exact outer context carried by the introducing parent.

theorem DPDA_to_LR.ConcreteEmptyEdge.exists_cut {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 : ConcreteEmptyEdge M p q suffix) : ∃ (preWord : List T) (context : List (StackSymbol M)) (final : State M), PDA.Reaches { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := q, input := [], stack := context } ∧ PDA.Reaches { state := q, input := suffix, stack := context } { state := final, input := [], stack := [] }

Exact accepting cut carried by a concrete empty edge.

theorem DPDA_to_LR.ConcreteEmptyEdge.exists_zeroVisibleDecomposition {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 : ConcreteEmptyEdge M p q suffix) : ∃ (preWord : List T) (context : List (StackSymbol M)) (anchor : Nonterminal M) (anchorSuffix : List T) (anchorContext : List (StackSymbol M)), VisibleSpineAnchor M p anchor anchorSuffix preWord anchorContext ∧ ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.list q [] q) suffix context

Every concrete empty edge inherits the last-visible-event decomposition of its exact child spine.

theorem DPDA_to_LR.ConcreteEmptyEdge.exists_childSpineAtCompletion {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} (h : ConcreteEmptyEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal completion)) : ∃ (context : List (StackSymbol M)), ConcreteOperationalSpine M p (PDA_to_CFG.N.list q [] q) suffix completion context

Re-complete the visible prefix of a concrete empty edge by an arbitrary terminal word. The ancestry retained by the edge is independent of the particular productive completion originally used to make it concrete.

theorem DPDA_to_LR.ConcreteEmptyTransitionEdge.exists_childSpineAtCompletion {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} (h : ConcreteEmptyTransitionEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal completion)) : ∃ (context : List (StackSymbol M)), ConcreteOperationalSpine M p (PDA_to_CFG.N.list q [] q) suffix completion context

Re-completing a transition-tagged edge is just the corresponding operation on its underlying concrete empty edge.

theorem DPDA_to_LR.ConcreteEmptyEdge.exists_zeroVisibleDecompositionAtCompletion {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} (h : ConcreteEmptyEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal completion)) : ∃ (context : List (StackSymbol M)) (anchor : Nonterminal M) (anchorSuffix : List T) (anchorContext : List (StackSymbol M)), VisibleSpineAnchor M p anchor anchorSuffix completion anchorContext ∧ ZeroVisibleTail M p completion anchor anchorSuffix anchorContext (PDA_to_CFG.N.list q [] q) suffix context

Last-visible-event decomposition after a deliberately chosen completion of the shared visible prefix. This is the form needed to compare two empty returns whose original concrete witnesses used unrelated completions.

theorem DPDA_to_LR.ZeroVisibleTail.fromEmptyList_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord : List T} {q target : State M} {anchorSuffix : List T} {anchorContext : List (StackSymbol M)} {current : Nonterminal M} {currentSuffix : List T} {currentContext : List (StackSymbol M)} (h : ZeroVisibleTail M p preWord (PDA_to_CFG.N.list q [] target) anchorSuffix anchorContext current currentSuffix currentContext) : current = PDA_to_CFG.N.list q [] target ∧ currentSuffix = anchorSuffix ∧ currentContext = anchorContext

An empty-stack list nonterminal has no zero-visible child. Every zero-visible constructor expects either a single, a nonempty list stack, or the start marker, so a tail beginning at list q [] target is literal reflexivity.

theorem DPDA_to_LR.ConcreteEmptyEdge.exists_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} (h : ConcreteEmptyEdge M p q suffix) : ∃ (completion : List T), (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal completion)

Every concrete empty edge has at least one productive completion of its visible prefix.

Terminal displacement of two empty-return prefixes

theorem DPDA_to_LR.concreteEmptyReturn_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₂

Equality after appending terminal suffixes exposes the precise terminal displacement between the two visible prefixes. Keeping this lemma in the concrete synchronization layer lets the hard semantic proof choose aligned terminal completions before returning to the syntax-facing adapter.

Net-pop runs at a chosen completion

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

Operational factorization of a concrete empty return after deliberately choosing a terminal completion of its visible prefix.

Equations

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

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

One-step specialization for a transition-generated concrete empty return.

Equations

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

theorem DPDA_to_LR.ConcreteEmptyTransitionRun.returnRun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {completion suffix : List T} {q : State M} (h : ConcreteEmptyTransitionRun M completion suffix q) : ConcreteEmptyReturnRun M completion suffix q

Forgetting the one-step tag gives the ordinary concrete return run.

theorem DPDA_to_LR.ConcreteEmptyEdge.directAnchor_or_epsilonBearingAtCompletion {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 : ConcreteEmptyEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal completion)) : (∃ (context : List (StackSymbol M)), VisibleSpineAnchor M p (PDA_to_CFG.N.list q [] q) suffix completion context) ∨ ∃ (context : List (StackSymbol M)) (anchor : Nonterminal M) (anchorSuffix : List T) (anchorContext : List (StackSymbol M)), VisibleSpineAnchor M p anchor anchorSuffix completion anchorContext ∧ ZeroVisibleTail M p completion anchor anchorSuffix anchorContext (PDA_to_CFG.N.list q [] q) suffix context ∧ EpsilonBearingZeroVisibleTail M p completion anchor anchorSuffix anchorContext (PDA_to_CFG.N.list q [] q) suffix context

At any chosen completion an empty edge is either itself the last visible anchor (read or split-right), or its child is reached through a genuinely epsilon-bearing zero-visible tail.

theorem DPDA_to_LR.directEmptyReturnAnchors_state_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {completion : List T} {q₁ q₂ : State M} {s₁ s₂ : List T} {context₁ context₂ : List (StackSymbol M)} (h₁ : VisibleSpineAnchor M p (PDA_to_CFG.N.list q₁ [] q₁) s₁ completion context₁) (h₂ : VisibleSpineAnchor M p (PDA_to_CFG.N.list q₂ [] q₂) s₂ completion context₂) : q₁ = q₂

Two empty returns which are both their own last visible anchors have the same return state. Read anchors use deterministic output synchronization; split-right anchors already share their displayed middle state.

theorem DPDA_to_LR.concreteReadEmptyReturn_alignedSpine_shape {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base : List (symbol T (Nonterminal M))} {suffixRead suffixOther beforeWord : List T} {readContext otherContext : List (StackSymbol M)} {source q : State M} {a : T} {Z : StackSymbol M} {A : Nonterminal M} (parent : ConcreteOperationalSpine M base (PDA_to_CFG.N.single source Z q) suffixRead beforeWord readContext) (htransition : (q, []) ∈ (emptyStackPDA M).transition_fun source a Z) (other : ConcreteOperationalSpine M (base ++ [symbol.terminal a]) A suffixOther (beforeWord ++ [a]) otherContext) : ∃ (target : State M), A = PDA_to_CFG.N.list q [] target

Any concrete spine aligned with a read/pop empty return is itself an empty-stack list cut in the same state. Deterministic read output fixes the aligned visible anchor, and an empty-list anchor has no proper zero-visible descendant.

theorem DPDA_to_LR.concreteReadEmptyReturn_samePrefix_state_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base : List (symbol T (Nonterminal M))} {suffix₁ suffix₂ beforeWord : List T} {context : List (StackSymbol M)} {source q₁ q₂ : State M} {a : T} {Z : StackSymbol M} (parent : ConcreteOperationalSpine M base (PDA_to_CFG.N.single source Z q₁) suffix₁ beforeWord context) (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) (edge₂ : ConcreteEmptyEdge M (base ++ [symbol.terminal a]) q₂ suffix₂) : q₁ = q₂

A read/pop empty return is synchronized with every other empty return at the same retained prefix. Aligning the other edge at the read completion either gives another direct empty-list anchor, or makes its last visible anchor a read with the same deterministic output. In the latter case that anchor already has empty stack text, so its zero-visible tail is reflexive.

theorem DPDA_to_LR.concreteEmptyReturn_read_samePrefix_state_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base : List (symbol T (Nonterminal M))} {suffix₁ suffix₂ beforeWord : List T} {context : List (StackSymbol M)} {source q₁ q₂ : State M} {a : T} {Z : StackSymbol M} (edge₁ : ConcreteEmptyEdge M (base ++ [symbol.terminal a]) q₁ suffix₁) (parent : ConcreteOperationalSpine M base (PDA_to_CFG.N.single source Z q₂) suffix₂ beforeWord context) (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) : q₁ = q₂

Symmetric orientation of concreteReadEmptyReturn_samePrefix_state_eq, for a read/pop return displayed on the right.

theorem DPDA_to_LR.ConcreteOperationalSpine.lastRead_of_terminalSuffix {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {z : List T} {a : T} {A : Nonterminal M} {suffix completion : List T} {context : List (StackSymbol M)} (h : ConcreteOperationalSpine M (p ++ List.map symbol.terminal z ++ [symbol.terminal a]) A suffix completion context) : ∃ (parentSuffix : List T) (beforeWord : List T) (parentContext : List (StackSymbol M)) (source : State M) (target : State M) (next : State M) (Z : StackSymbol M) (gamma : List (StackSymbol M)), ConcreteOperationalSpine M (p ++ List.map symbol.terminal z) (PDA_to_CFG.N.single source Z target) parentSuffix beforeWord parentContext ∧ (next, gamma) ∈ (emptyStackPDA M).transition_fun source a Z ∧ (PDA_to_CFG.N.single source Z target, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules ∧ completion = beforeWord ++ [a] ∧ ZeroVisibleTail M (p ++ List.map symbol.terminal z ++ [symbol.terminal a]) completion (PDA_to_CFG.N.list next gamma target) parentSuffix parentContext A suffix context

A concrete spine whose visible prefix ends in a terminal has a retained last read edge. The theorem exposes that edge together with the entire zero-visible tail from its list child to the original endpoint; this is the ancestry-preserving form needed by displaced empty-return comparisons.

theorem DPDA_to_LR.ConcreteOperationalSpine.firstRead_of_terminalBlock {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {a : T} {z : List T} {A : Nonterminal M} {suffix completion : List T} {context : List (StackSymbol M)} (h : ConcreteOperationalSpine M (p ++ List.map symbol.terminal (a :: z)) A suffix completion context) : ∃ (parentSuffix : List T) (beforeWord : List T) (parentContext : List (StackSymbol M)) (source : State M) (target : State M) (next : State M) (Z : StackSymbol M) (gamma : List (StackSymbol M)), ConcreteOperationalSpine M p (PDA_to_CFG.N.single source Z target) parentSuffix beforeWord parentContext ∧ (next, gamma) ∈ (emptyStackPDA M).transition_fun source a Z ∧ (PDA_to_CFG.N.single source Z target, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules

Walking backward through a nonempty terminal extension exposes the read parent of its first terminal. The proof peels last-read anchors from the right, preserving the concrete retained ancestry at every step.

theorem DPDA_to_LR.concreteReadEmptyReturn_no_strictTerminalExtension {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base : List (symbol T (Nonterminal M))} {suffixRead beforeWord : List T} {readContext : List (StackSymbol M)} {source q : State M} {a b : T} {Z : StackSymbol M} {z : List T} {A : Nonterminal M} {suffixOther completionOther : List T} {otherContext : List (StackSymbol M)} (parent : ConcreteOperationalSpine M base (PDA_to_CFG.N.single source Z q) suffixRead beforeWord readContext) (htransition : (q, []) ∈ (emptyStackPDA M).transition_fun source a Z) (other : ConcreteOperationalSpine M (base ++ [symbol.terminal a] ++ List.map symbol.terminal (b :: z)) A suffixOther completionOther otherContext) : False

Once a read transition has popped its displayed symbol, no active concrete spine can occur at a strict terminal extension of that empty-return prefix. Walking the extension back to its first read produces a single node at the old prefix, while deterministic alignment with the pop says that every node there is an empty-list cut.

theorem DPDA_to_LR.ConcreteEmptyEdge.returnRunAtCompletion {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 : ConcreteEmptyEdge M p q suffix) (hp : (characteristicGrammar M).DerivesRightmost p (List.map symbol.terminal completion)) : ConcreteEmptyReturnRun M completion suffix q

Every concrete empty edge has a net-pop run at every chosen terminal completion of its visible prefix.

theorem DPDA_to_LR.ConcreteEmptyTransitionEdge.transitionRunAtCompletion {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)) : ConcreteEmptyTransitionRun M completion suffix q

A transition-tagged concrete edge has a one-step net-pop run at every chosen terminal completion.

Oriented cuts for a nonempty terminal displacement

theorem DPDA_to_LR.concreteEmptyReturn_forward_displacement {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p₁ p₂ : List (symbol T (Nonterminal M))} {q₁ q₂ : State M} {s₁ s₂ z : List T} (edge₁ : ConcreteEmptyEdge M p₁ q₁ s₁) (edge₂ : ConcreteEmptyEdge M p₂ q₂ s₂) (hp₂ : p₂ = p₁ ++ List.map symbol.terminal z) (hz : z ≠ []) (hlook : List.take 1 s₁ = List.take 1 (z ++ s₂)) : ∃ (completion : List T) (context₁ : List (StackSymbol M)) (context₂ : List (StackSymbol M)) (final₁ : State M) (final₂ : State M), PDA.Reaches { state := (emptyStackPDA M).initial_state, input := completion, stack := [(emptyStackPDA M).start_symbol] } { state := q₁, input := [], stack := context₁ } ∧ PDA.Reaches { state := (emptyStackPDA M).initial_state, input := completion ++ z, stack := [(emptyStackPDA M).start_symbol] } { state := q₂, input := [], stack := context₂ } ∧ PDA.Reaches { state := q₁, input := s₁, stack := context₁ } { state := final₁, input := [], stack := [] } ∧ PDA.Reaches { state := q₂, input := s₂, stack := context₂ } { state := final₂, input := [], stack := [] } ∧ PDA.Reaches { state := q₁, input := z, stack := context₁ } { state := q₂, input := [], stack := context₂ }

If the second visible prefix extends the first by a nonempty terminal block, the first empty-return cut processes exactly that block to the second cut. The witnesses retain both useful continuations for the subsequent net-pop crossing argument.

theorem DPDA_to_LR.concreteEmptyReturn_backward_displacement {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p₁ p₂ : List (symbol T (Nonterminal M))} {q₁ q₂ : State M} {s₁ s₂ y z : List T} (edge₁ : ConcreteEmptyEdge M p₁ q₁ s₁) (edge₂ : ConcreteEmptyEdge M p₂ q₂ s₂) (hp₁ : p₁ = p₂ ++ List.map symbol.terminal z) (hs₂ : s₂ = z ++ y) (hz : z ≠ []) : ∃ (completion : List T) (context₁ : List (StackSymbol M)) (context₂ : List (StackSymbol M)) (final₁ : State M) (final₂ : State M), PDA.Reaches { state := (emptyStackPDA M).initial_state, input := completion ++ z, stack := [(emptyStackPDA M).start_symbol] } { state := q₁, input := [], stack := context₁ } ∧ PDA.Reaches { state := (emptyStackPDA M).initial_state, input := completion, stack := [(emptyStackPDA M).start_symbol] } { state := q₂, input := [], stack := context₂ } ∧ PDA.Reaches { state := q₁, input := s₁, stack := context₁ } { state := final₁, input := [], stack := [] } ∧ PDA.Reaches { state := q₂, input := s₂, stack := context₂ } { state := final₂, input := [], stack := [] } ∧ PDA.Reaches { state := q₂, input := z, stack := context₂ } { state := q₁, input := [], stack := context₁ }

If the first visible prefix extends the second by a nonempty terminal block, the same comparison is oriented from the second return cut to the first. Here the transferred suffix equation itself supplies the common first symbol because the displacement is nonempty.

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

Concrete version of the syntax-facing paired empty-return classifier. The proof below will turn every genuinely distinct pair into one of the two public operational obstructions.

Equations

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

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

The genuinely semantic residual, with the transition witness used as the left edge rather than carried redundantly beside another proof with the same indices.

Equations

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

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

Symmetric semantic residual in which the transition witness is the right edge. The LR lookahead equation is directional, so this is not merely the preceding proposition with its arguments swapped.

Equations

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

theorem DPDA_to_LR.concreteEmptyReturnPairsClassified_of_transitionSides {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hleft : ConcreteLeftTransitionReturnPairsClassified M) (hright : ConcreteRightTransitionReturnPairsClassified M) : ConcreteEmptyReturnPairsClassified M

The two directional transition-vs-return lemmas are exactly sufficient for the concrete paired classifier; the redundant concrete edge on the transition-tagged side is intentionally discarded.