Rigidity of productive pending frontiers

A pending frontier records the visible events of a characteristic-spine execution. This file proves that two productive counted executions which have reached the same pending frontier have consumed the same prefix of their fixed input word. The productive continuations may use different appended input tails; equality of their first symbols is enough.

The proof factors each counted trace after its last visible event. It then recurses on the shorter common frontier. Reading anchors synchronize by determinism. At paired split-right anchors, the recursive synchronization of the parent positions gives one common retained frame, and prefix-freeness of productive retained returns forces the two selected completion words to be equal.

inductive DPDA_to_LR.PendingFrontierVisibleAnchor {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (word : List T) : PendingFrontierPosition M → ℕ → Prop

The root or the child of the last visible event of a counted pending frontier trace.

• root {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {word : List T} : PendingFrontierVisibleAnchor M word { frontier := [], node := PDA_to_CFG.N.start, suffix := [], consumed := [], context := [], remaining := word } 0
• read {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {word : List T} {p : List (symbol T (Nonterminal M))} {suffix consumed remaining : List T} {context : List (StackSymbol M)} {steps : ℕ} {q target next : State M} {a : T} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (previous : PendingFrontierTrace M word { frontier := p, node := PDA_to_CFG.N.single q Z target, suffix := suffix, consumed := consumed, context := context, remaining := a :: remaining } steps) (htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun q a Z) (hrule : (PDA_to_CFG.N.single q Z target, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) : PendingFrontierVisibleAnchor M word { frontier := p ++ [symbol.terminal a], node := PDA_to_CFG.N.list next gamma target, suffix := suffix, consumed := consumed ++ [a], context := context, remaining := remaining } (steps + 1)
• splitRight {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {word : List T} {p : List (symbol T (Nonterminal M))} {suffix consumed leftWord remaining : List T} {context : List (StackSymbol M)} {steps returnSteps : ℕ} {q middle target : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (previous : PendingFrontierTrace M word { frontier := p, node := PDA_to_CFG.N.list q (Z :: gamma) target, suffix := suffix, consumed := consumed, context := context, remaining := leftWord ++ remaining } steps) (hlength : ↑(Z :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hrule : (PDA_to_CFG.N.list q (Z :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single q Z middle), symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)]) ∈ (characteristicGrammar M).rules) (hleft : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single q Z middle)] (List.map symbol.terminal leftWord)) (hpositive : 0 < returnSteps) (hreturn : (emptyStackPDA M).RetainedFrameRun (gamma ++ context) returnSteps { state := q, input := leftWord, stack := Z :: (gamma ++ context) } { state := middle, input := [], stack := gamma ++ context }) : PendingFrontierVisibleAnchor M word { frontier := p ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z middle)], node := PDA_to_CFG.N.list middle gamma target, suffix := suffix, consumed := consumed ++ leftWord, context := context, remaining := remaining } (steps + returnSteps)

theorem DPDA_to_LR.PendingFrontierVisibleAnchor.trace {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {word : List T} {position : PendingFrontierPosition M} {steps : ℕ} (h : PendingFrontierVisibleAnchor M word position steps) : PendingFrontierTrace M word position steps

A counted visible anchor is itself a complete counted pending-frontier trace.

theorem DPDA_to_LR.PendingFrontierVisibleAnchor.visibleSpineAnchor {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {word : List T} {position : PendingFrontierPosition M} {steps : ℕ} (h : PendingFrontierVisibleAnchor M word position steps) : VisibleSpineAnchor M position.frontier position.node position.suffix position.consumed position.context

Forgetting the count and remaining input gives the corresponding ordinary last-visible spine anchor.

theorem DPDA_to_LR.PendingFrontierTrace.exists_visibleAnchor_decomposition {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {word : List T} {position : PendingFrontierPosition M} {steps : ℕ} (h : PendingFrontierTrace M word position steps) : ∃ (anchorPosition : PendingFrontierPosition M) (anchorSteps : ℕ) (tailSteps : ℕ), PendingFrontierVisibleAnchor M word anchorPosition anchorSteps ∧ ZeroVisibleFrontierExtension M anchorPosition position tailSteps

Every counted pending-frontier trace factors as its last visible anchor followed by a counted zero-visible suffix.

theorem DPDA_to_LR.productivePendingFrontierVisibleAnchor_rigid {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {word future₁ future₂ : List T} {position₁ position₂ : PendingFrontierPosition M} {steps₁ steps₂ : ℕ} {final₁ final₂ : State M} (anchor₁ : PendingFrontierVisibleAnchor M word position₁ steps₁) (anchor₂ : PendingFrontierVisibleAnchor M word position₂ steps₂) (hfrontier : position₁.frontier = position₂.frontier) (useful₁ : PDA.Reaches ((PendingFrontierPosition.cut M position₁).appendInput future₁) { state := final₁, input := [], stack := [] }) (useful₂ : PDA.Reaches ((PendingFrontierPosition.cut M position₂).appendInput future₂) { state := final₂, input := [], stack := [] }) (hlook : List.take 1 future₁ = List.take 1 future₂) : position₁.consumed = position₂.consumed ∧ leftmostEpsilonPositionOf M position₁.node position₁.context = leftmostEpsilonPositionOf M position₂.node position₂.context

Two productive counted last-visible anchors with the same pending frontier have consumed the same prefix and have the same exact structural anchor position.

theorem DPDA_to_LR.productivePendingFrontier_same_frontier_consumed_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {word future₁ future₂ : List T} {position₁ position₂ : PendingFrontierPosition M} {steps₁ steps₂ : ℕ} {final₁ final₂ : State M} (trace₁ : PendingFrontierTrace M word position₁ steps₁) (trace₂ : PendingFrontierTrace M word position₂ steps₂) (hfrontier : position₁.frontier = position₂.frontier) (useful₁ : PDA.Reaches ((PendingFrontierPosition.cut M position₁).appendInput future₁) { state := final₁, input := [], stack := [] }) (useful₂ : PDA.Reaches ((PendingFrontierPosition.cut M position₂).appendInput future₂) { state := final₂, input := [], stack := [] }) (hlook : List.take 1 future₁ = List.take 1 future₂) : position₁.consumed = position₂.consumed

Productive counted pending-frontier traces reaching the same visible frontier have consumed the same prefix of their common fixed input word. The productive continuations may append different tails, provided their one-symbol lookahead agrees.