Counted traces of pending characteristic frontiers

A concrete characteristic spine records which grammar symbols have become visible, but ordinary reachability forgets when that happened. This module keeps the two views together. A trace starts with one fixed input word and records, at every spine position, the already completed part and the still unconsumed part of that word.

The visible constructors have their literal operational cost. A read consumes one terminal and appends that terminal to the pending frontier. A splitRight executes the selected positive retained-frame completion of its left single, and appends the single marker only at the return endpoint. start, epsilon, and splitLeft do not change the pending frontier.

The final section packages structural extension of a trace. If such an extension has the same pending frontier at both ends, its read and split-right cases are impossible; the extension is therefore a counted zero-visible tail. This is the ancestry statement needed before comparing independently selected return intervals.

structure DPDA_to_LR.PendingFrontierPosition {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Type

All indices attached to one point of a pending-frontier execution.

• frontier : List (symbol T (Nonterminal M))
• node : Nonterminal M
• suffix : List T
• consumed : List T
• context : List (StackSymbol M)
• remaining : List T

theorem DPDA_to_LR.PendingFrontierPosition.ext {Q T S : Type} {inst✝ : Fintype Q} {inst✝¹ : Fintype T} {inst✝² : Fintype S} {M : DPDA Q T S} {x y : PendingFrontierPosition M} (frontier : x.frontier = y.frontier) (node : x.node = y.node) (suffix : x.suffix = y.suffix) (consumed : x.consumed = y.consumed) (context : x.context = y.context) (remaining : x.remaining = y.remaining) : x = y

theorem DPDA_to_LR.PendingFrontierPosition.ext_iff {Q T S : Type} {inst✝ : Fintype Q} {inst✝¹ : Fintype T} {inst✝² : Fintype S} {M : DPDA Q T S} {x y : PendingFrontierPosition M} : x = y ↔ x.frontier = y.frontier ∧ x.node = y.node ∧ x.suffix = y.suffix ∧ x.consumed = y.consumed ∧ x.context = y.context ∧ x.remaining = y.remaining

def DPDA_to_LR.PendingFrontierPosition.cut {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (position : PendingFrontierPosition M) : (emptyStackPDA M).conf

The physical PDA configuration represented by a frontier position.

Equations

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

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

A normalized spine annotated by an exact counted computation on one fixed whole input word. The word consumed by a completed single is stored on the splitRight constructor, together with its positive retained run.

• root {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {word : List T} : PendingFrontierTrace M word { frontier := [], node := PDA_to_CFG.N.start, suffix := [], consumed := [], context := [], remaining := word } 0
• start {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {word : List T} {target : State M} (hrule : (PDA_to_CFG.N.start, [symbol.nonterminal (PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target)]) ∈ (characteristicGrammar M).rules) : PendingFrontierTrace M word { frontier := [], node := PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target, 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) : PendingFrontierTrace 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)
• epsilon {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} {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 := remaining } steps) (htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q Z) (hrule : (PDA_to_CFG.N.single q Z target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) : PendingFrontierTrace M word { frontier := p, node := PDA_to_CFG.N.list next gamma target, suffix := suffix, consumed := consumed, context := context, remaining := remaining } (steps + 1)
• splitLeft {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 z remaining : List T} {context : List (StackSymbol M)} {steps : ℕ} {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 := 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) (hright : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)] (List.map symbol.terminal z)) : PendingFrontierTrace M word { frontier := p, node := PDA_to_CFG.N.single q Z middle, suffix := z ++ suffix, consumed := consumed, context := gamma ++ context, remaining := remaining } steps
• 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 }) : PendingFrontierTrace 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.PendingFrontierTrace.word_eq {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) : word = position.consumed ++ position.remaining

The completion word is always the consumed prefix followed by the input still present at the represented cut.

theorem DPDA_to_LR.PendingFrontierTrace.concreteOperationalSpine {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) : ConcreteOperationalSpine M position.frontier position.node position.suffix position.consumed position.context

Forgetting counts and the unconsumed completion suffix recovers the underlying normalized concrete spine.

theorem DPDA_to_LR.PendingFrontierTrace.reachesIn {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) : PDA.ReachesIn steps { state := (emptyStackPDA M).initial_state, input := word, stack := [(emptyStackPDA M).start_symbol] } (PendingFrontierPosition.cut M position)

Exact counted operational meaning of an annotated trace.

theorem DPDA_to_LR.ConcreteOperationalSpine.exists_pendingFrontierTrace {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {A : Nonterminal M} {suffix consumed remaining : List T} {context : List (StackSymbol M)} (h : ConcreteOperationalSpine M p A suffix consumed context) : ∃ (steps : ℕ), PendingFrontierTrace M (consumed ++ remaining) { frontier := p, node := A, suffix := suffix, consumed := consumed, context := context, remaining := remaining } steps

Every normalized concrete spine admits a counted annotation after an arbitrary still-unconsumed suffix is appended to its chosen completion.

Structural extension and zero-visible ancestry

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

A suffix of an annotated execution. Its step count is relative to the starting position.

• refl {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} : PendingFrontierExtension M startPosition startPosition 0
• start {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} {p : List (symbol T (Nonterminal M))} {consumed remaining : List T} {steps : ℕ} (previous : PendingFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.start, suffix := [], consumed := consumed, context := [], remaining := remaining } steps) {target : State M} (hrule : (PDA_to_CFG.N.start, [symbol.nonterminal (PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target)]) ∈ (characteristicGrammar M).rules) : PendingFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target, suffix := [], consumed := consumed, context := [], remaining := remaining } steps
• read {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} {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 : PendingFrontierExtension M startPosition { 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) : PendingFrontierExtension M startPosition { 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)
• epsilon {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} {p : List (symbol T (Nonterminal M))} {suffix consumed remaining : List T} {context : List (StackSymbol M)} {steps : ℕ} {q target next : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (previous : PendingFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.single q Z target, suffix := suffix, consumed := consumed, context := context, remaining := remaining } steps) (htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q Z) (hrule : (PDA_to_CFG.N.single q Z target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) : PendingFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.list next gamma target, suffix := suffix, consumed := consumed, context := context, remaining := remaining } (steps + 1)
• splitLeft {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} {p : List (symbol T (Nonterminal M))} {suffix consumed z remaining : List T} {context : List (StackSymbol M)} {steps : ℕ} {q middle target : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (previous : PendingFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.list q (Z :: gamma) target, suffix := suffix, consumed := consumed, context := context, remaining := 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) (hright : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)] (List.map symbol.terminal z)) : PendingFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.single q Z middle, suffix := z ++ suffix, consumed := consumed, context := gamma ++ context, remaining := remaining } steps
• splitRight {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} {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 : PendingFrontierExtension M startPosition { 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 }) : PendingFrontierExtension M startPosition { 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.PendingFrontierExtension.reachesIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {startPosition endPosition : PendingFrontierPosition M} {steps : ℕ} (h : PendingFrontierExtension M startPosition endPosition steps) : PDA.ReachesIn steps (PendingFrontierPosition.cut M startPosition) (PendingFrontierPosition.cut M endPosition)

The counted subrun represented by a structural frontier extension.

theorem DPDA_to_LR.PendingFrontierTrace.extend {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {word : List T} {startPosition endPosition : PendingFrontierPosition M} {startSteps extraSteps : ℕ} (htrace : PendingFrontierTrace M word startPosition startSteps) (hextension : PendingFrontierExtension M startPosition endPosition extraSteps) : PendingFrontierTrace M word endPosition (startSteps + extraSteps)

Extending an annotated trace by a structural suffix preserves the fixed whole input word and adds the suffix's exact step count.

theorem DPDA_to_LR.PendingFrontierExtension.prefix_eq_append {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {startPosition endPosition : PendingFrontierPosition M} {steps : ℕ} (h : PendingFrontierExtension M startPosition endPosition steps) : ∃ (added : List (symbol T (Nonterminal M))), endPosition.frontier = startPosition.frontier ++ added

The end frontier of an extension is the start frontier followed by the visible events occurring in that extension.

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

A counted structural suffix containing only start, epsilon, and split-left events.

• refl {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} : ZeroVisibleFrontierExtension M startPosition startPosition 0
• start {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} {p : List (symbol T (Nonterminal M))} {consumed remaining : List T} {steps : ℕ} (previous : ZeroVisibleFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.start, suffix := [], consumed := consumed, context := [], remaining := remaining } steps) {target : State M} (hrule : (PDA_to_CFG.N.start, [symbol.nonterminal (PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target)]) ∈ (characteristicGrammar M).rules) : ZeroVisibleFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target, suffix := [], consumed := consumed, context := [], remaining := remaining } steps
• epsilon {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} {p : List (symbol T (Nonterminal M))} {suffix consumed remaining : List T} {context : List (StackSymbol M)} {steps : ℕ} {q target next : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (previous : ZeroVisibleFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.single q Z target, suffix := suffix, consumed := consumed, context := context, remaining := remaining } steps) (htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q Z) (hrule : (PDA_to_CFG.N.single q Z target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) : ZeroVisibleFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.list next gamma target, suffix := suffix, consumed := consumed, context := context, remaining := remaining } (steps + 1)
• splitLeft {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {startPosition : PendingFrontierPosition M} {p : List (symbol T (Nonterminal M))} {suffix consumed z remaining : List T} {context : List (StackSymbol M)} {steps : ℕ} {q middle target : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (previous : ZeroVisibleFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.list q (Z :: gamma) target, suffix := suffix, consumed := consumed, context := context, remaining := 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) (hright : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)] (List.map symbol.terminal z)) : ZeroVisibleFrontierExtension M startPosition { frontier := p, node := PDA_to_CFG.N.single q Z middle, suffix := z ++ suffix, consumed := consumed, context := gamma ++ context, remaining := remaining } steps

theorem DPDA_to_LR.PendingFrontierExtension.zeroVisible_of_prefix_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {startPosition endPosition : PendingFrontierPosition M} {steps : ℕ} (h : PendingFrontierExtension M startPosition endPosition steps) (hprefix : endPosition.frontier = startPosition.frontier) : ZeroVisibleFrontierExtension M startPosition endPosition steps

Equal pending frontiers force a structural extension to contain no read or completed-single event, even when that single completes on epsilon.

theorem DPDA_to_LR.ZeroVisibleFrontierExtension.zeroVisibleTail {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {startPosition endPosition : PendingFrontierPosition M} {steps : ℕ} (h : ZeroVisibleFrontierExtension M startPosition endPosition steps) : ZeroVisibleTail M startPosition.frontier startPosition.consumed startPosition.node startPosition.suffix startPosition.context endPosition.node endPosition.suffix endPosition.context

A counted zero-visible frontier suffix is the existing structural ZeroVisibleTail after forgetting its count and remaining input.

theorem DPDA_to_LR.ZeroVisibleFrontierExtension.reachesIn {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {startPosition endPosition : PendingFrontierPosition M} {steps : ℕ} (h : ZeroVisibleFrontierExtension M startPosition endPosition steps) : PDA.ReachesIn steps (PendingFrontierPosition.cut M startPosition) (PendingFrontierPosition.cut M endPosition)

Zero-visible frontier suffixes retain their remaining input and have the exact counted operational meaning advertised by their index.

theorem DPDA_to_LR.ZeroVisibleFrontierExtension.remaining_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {startPosition endPosition : PendingFrontierPosition M} {steps : ℕ} (h : ZeroVisibleFrontierExtension M startPosition endPosition steps) : endPosition.remaining = startPosition.remaining

Zero-visible suffixes preserve the unconsumed part of the fixed word.

theorem DPDA_to_LR.ZeroVisibleFrontierExtension.consumed_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {startPosition endPosition : PendingFrontierPosition M} {steps : ℕ} (h : ZeroVisibleFrontierExtension M startPosition endPosition steps) : endPosition.consumed = startPosition.consumed

Zero-visible suffixes preserve the completed part of the fixed word.

theorem DPDA_to_LR.PendingFrontierTrace.extend_same_frontier {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {word : List T} {startPosition endPosition : PendingFrontierPosition M} {startSteps extraSteps : ℕ} (htrace : PendingFrontierTrace M word startPosition startSteps) (hextension : PendingFrontierExtension M startPosition endPosition extraSteps) (hfrontier : endPosition.frontier = startPosition.frontier) : PendingFrontierTrace M word endPosition (startSteps + extraSteps) ∧ endPosition.remaining = startPosition.remaining ∧ endPosition.consumed = startPosition.consumed ∧ ZeroVisibleTail M startPosition.frontier startPosition.consumed startPosition.node startPosition.suffix startPosition.context endPosition.node endPosition.suffix endPosition.context ∧ PDA.ReachesIn extraSteps (PendingFrontierPosition.cut M startPosition) (PendingFrontierPosition.cut M endPosition)

Packaged ancestry consequence for two points of one annotated execution. The endpoint trace has the summed count, and equality of visible frontiers forces the entire extra counted segment to be zero-visible.