Synchronizing characteristic spines

Two independent operational run summaries do not determine an active characteristic spine: in particular, successive drain pops can have the same visible cut and the same transition output. The synchronization theorem must therefore retain the syntactic spine ancestry. This file first records the common-child completion facts used by that ancestry-sensitive argument.

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

A list-introducing edge together with its normalized concrete ancestry and the chosen terminal completion of the child's visible prefix. Unlike ListTransitionRun, this relation retains the actual final grammar edge, so successive drain pops cannot be confused with one another.

• 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)} {q target next : State M} {a : T} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.single q Z target) suffix preWord context) (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) : ConcreteListIntroduction M (p ++ [symbol.terminal a]) next gamma target suffix (preWord ++ [a]) context (PDA_to_CFG.N.single q Z target) (PDA_to_CFG.N.single q Z target, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next gamma target)])
• 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)} {q target next : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.single q Z target) suffix preWord context) (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) : ConcreteListIntroduction M p next gamma target suffix preWord context (PDA_to_CFG.N.single q Z target) (PDA_to_CFG.N.single q Z target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)])
• splitRight {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)} {q middle target : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (parent : ConcreteOperationalSpine M p (PDA_to_CFG.N.list q (Z :: gamma) target) suffix preWord context) (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)) : ConcreteListIntroduction M (p ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z middle)]) middle gamma target suffix (preWord ++ leftWord) context (PDA_to_CFG.N.list q (Z :: gamma) target) (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)])
• start {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {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) : ConcreteListIntroduction M [] (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target [] [] [] PDA_to_CFG.N.start (PDA_to_CFG.N.start, [symbol.nonterminal (PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target)])

theorem DPDA_to_LR.ConcreteListIntroduction.childSpine {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {next target : State M} {gamma : List (StackSymbol M)} {suffix preWord : List T} {context : List (StackSymbol M)} {parent : Nonterminal M} {rule : Nonterminal M × List (symbol T (Nonterminal M))} (h : ConcreteListIntroduction M p next gamma target suffix preWord context parent rule) : ConcreteOperationalSpine M p (PDA_to_CFG.N.list next gamma target) suffix preWord context

The concrete introduction contains the normalized concrete spine of its child.

theorem DPDA_to_LR.ConcreteListIntroduction.gammaLength {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {next target : State M} {gamma : List (StackSymbol M)} {suffix preWord : List T} {context : List (StackSymbol M)} {parent : Nonterminal M} {rule : Nonterminal M × List (symbol T (Nonterminal M))} (h : ConcreteListIntroduction M p next gamma target suffix preWord context parent rule) : ↑gamma.length ≤ PDA_to_CFG.max_push (emptyStackPDA M)

Every replacement stack carried by a concrete list introduction satisfies the characteristic grammar's uniform push bound.

theorem DPDA_to_LR.ListIntroduction.prefixCompletion {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {child : Nonterminal M} {childSuffix : List T} {parentPrefix : List (symbol T (Nonterminal M))} {parent : Nonterminal M} {rule : Nonterminal M × List (symbol T (Nonterminal M))} (h : ListIntroduction M childPrefix child childSuffix parentPrefix parent rule) : ∃ (preWord : List T), (characteristicGrammar M).DerivesRightmost childPrefix (List.map symbol.terminal preWord)

Every visible prefix of a list-introducing edge has a terminal completion. For a split edge, productivity of the exposed left single supplies the additional completed segment.

theorem DPDA_to_LR.concreteListIntroduction_of_listIntroduction {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {child : Nonterminal M} {childSuffix : List T} {parentPrefix : List (symbol T (Nonterminal M))} {parent : Nonterminal M} {rule : Nonterminal M × List (symbol T (Nonterminal M))} {preWord : List T} (h : ListIntroduction M childPrefix child childSuffix parentPrefix parent rule) (hp : (characteristicGrammar M).DerivesRightmost childPrefix (List.map symbol.terminal preWord)) : ∃ (next : State M) (target : State M) (gamma : List (StackSymbol M)) (context : List (StackSymbol M)), child = PDA_to_CFG.N.list next gamma target ∧ ConcreteListIntroduction M childPrefix next gamma target childSuffix preWord context parent rule

Normalize a list-introducing active edge after choosing a terminal completion of its child prefix. The returned witness retains both the exact last edge and the concrete ancestry leading to its parent.

theorem DPDA_to_LR.retainedChild_completion {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {r : Nonterminal M × List (symbol T (Nonterminal M))} {A : Nonterminal M} (hr : r ∈ (characteristicGrammar M).rules) (hA : symbol.nonterminal A ∈ r.2) : ∃ (w : List T), (characteristicGrammar M).DerivesRightmost [symbol.nonterminal A] (List.map symbol.terminal w)

A nonterminal occurring in a retained characteristic rule has a terminal rightmost completion.

theorem DPDA_to_LR.ConcreteListIntroduction.childCompletion {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {next target : State M} {gamma : List (StackSymbol M)} {suffix preWord : List T} {context : List (StackSymbol M)} {parent : Nonterminal M} {rule : Nonterminal M × List (symbol T (Nonterminal M))} (h : ConcreteListIntroduction M p next gamma target suffix preWord context parent rule) : ∃ (w : List T), (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)] (List.map symbol.terminal w)

The list child selected by a concrete introduction has a terminal completion, independently of the surrounding active suffix.

theorem DPDA_to_LR.ConcreteListIntroduction.childContinuation {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {next target : State M} {gamma : List (StackSymbol M)} {suffix preWord : List T} {context : List (StackSymbol M)} {parent : Nonterminal M} {rule : Nonterminal M × List (symbol T (Nonterminal M))} (h : ConcreteListIntroduction M p next gamma target suffix preWord context parent rule) : ∃ (final : State M), PDA.Reaches { state := target, input := suffix, stack := context } { state := final, input := [], stack := [] }

The focused continuation of a concrete introduction starts at its list target with exactly the saved suffix and outer context.

theorem DPDA_to_LR.completedList_reaches_with_context {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q target : State M} {gamma context : List (StackSymbol M)} {w : List T} (hgamma : ↑gamma.length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hcomplete : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list q gamma target)] (List.map symbol.terminal w)) : PDA.Reaches { state := q, input := w, stack := gamma ++ context } { state := target, input := [], stack := context }

A terminal completion of a characteristic list child realizes its encoded net-pop computation under every saved outer stack context.

theorem DPDA_to_LR.completedList_useful_with_context {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q target final : State M} {gamma context : List (StackSymbol M)} {w suffix : List T} (hgamma : ↑gamma.length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hcomplete : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list q gamma target)] (List.map symbol.terminal w)) (hcontinuation : PDA.Reaches { state := target, input := suffix, stack := context } { state := final, input := [], stack := [] }) : PDA.Reaches { state := q, input := w ++ suffix, stack := gamma ++ context } { state := final, input := [], stack := [] }

Completing a list child and then following its focused continuation gives an accepting continuation from the child's concrete stack cut.

Concrete anchor comparison

theorem DPDA_to_LR.PairedVisibleAnchors.leftAnchor {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord : List T} {A₁ A₂ : Nonterminal M} {suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} (h : PairedVisibleAnchors M p preWord A₁ suffix₁ context₁ A₂ suffix₂ context₂) : VisibleSpineAnchor M p A₁ suffix₁ preWord context₁

Recover the left visible anchor retained by a paired-anchor witness.

theorem DPDA_to_LR.PairedVisibleAnchors.rightAnchor {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord : List T} {A₁ A₂ : Nonterminal M} {suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} (h : PairedVisibleAnchors M p preWord A₁ suffix₁ context₁ A₂ suffix₂ context₂) : VisibleSpineAnchor M p A₂ suffix₂ preWord context₂

Recover the right visible anchor retained by a paired-anchor witness.

theorem DPDA_to_LR.PairedVisibleAnchors.simulationCutsComparable {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₁ q₂ : Q × Bool} {target₁ target₂ : State M} {gamma₁ gamma₂ context₁ context₂ : List (StackSymbol M)} {suffix₁ suffix₂ : List T} (h : PairedVisibleAnchors M p preWord (PDA_to_CFG.N.list (Sum.inl q₁) gamma₁ target₁) suffix₁ context₁ (PDA_to_CFG.N.list (Sum.inl q₂) gamma₂ target₂) suffix₂ context₂) : PDA.Reaches { state := Sum.inl q₁, input := [], stack := gamma₁ ++ context₁ } { state := Sum.inl q₂, input := [], stack := gamma₂ ++ context₂ } ∨ PDA.Reaches { state := Sum.inl q₂, input := [], stack := gamma₂ ++ context₂ } { state := Sum.inl q₁, input := [], stack := gamma₁ ++ context₁ }

Paired visible anchors whose endpoint states both remain in the simulation component lie on one ordered normalized computation. This is the comparison needed for split-right/split-right anchors; read anchors admit the stronger literal equality proved below.

theorem DPDA_to_LR.emptyStack_read_output_unique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q next₁ next₂ : State M} {a : T} {Z : StackSymbol M} {gamma₁ gamma₂ : List (StackSymbol M)} (h₁ : (next₁, gamma₁) ∈ (emptyStackPDA M).transition_fun q a Z) (h₂ : (next₂, gamma₂) ∈ (emptyStackPDA M).transition_fun q a Z) : (next₁, gamma₁) = (next₂, gamma₂)

Read transitions of the normalized empty-stack machine have a unique output. The FS→ES wrapper introduces nondeterminism only through an epsilon edge into the drain, never between two reading edges.

theorem DPDA_to_LR.concreteRead_anchor_data_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {q₁ q₂ target₁ target₂ next₁ next₂ : State M} {a : T} {Z₁ Z₂ : StackSymbol M} {gamma₁ gamma₂ : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M p (PDA_to_CFG.N.single q₁ Z₁ target₁) suffix₁ preWord context₁) (parent₂ : ConcreteOperationalSpine M p (PDA_to_CFG.N.single q₂ Z₂ target₂) suffix₂ preWord context₂) (read₁ : (next₁, gamma₁) ∈ (emptyStackPDA M).transition_fun q₁ a Z₁) (read₂ : (next₂, gamma₂) ∈ (emptyStackPDA M).transition_fun q₂ a Z₂) : next₁ = next₂ ∧ gamma₁ = gamma₂ ∧ context₁ = context₂

Aligned concrete read anchors agree componentwise on their output cut, including the hidden outer context.

theorem DPDA_to_LR.emptyStack_step_target_ne_boot {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c d : (emptyStackPDA M).conf} (h : PDA.Reaches₁ c d) : d.state ≠ Sum.inr 0

No transition of the FS→ES machine enters its distinguished boot state.

theorem DPDA_to_LR.emptyStack_global_boot_cut_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w input : List T} {stack : List (StackSymbol M)} (h : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inr 0, input := input, stack := stack }) : { state := Sum.inr 0, input := input, stack := stack } = { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] }

A globally reachable boot-state configuration is literally the initial configuration; no nonempty computation can return to boot.

theorem DPDA_to_LR.PairedVisibleAnchors.cutsComparable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord : List T} {A₁ A₂ : Nonterminal M} {suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} (h : PairedVisibleAnchors M p preWord A₁ suffix₁ context₁ A₂ suffix₂ context₂) : PDA.Reaches { state := spineCutState M A₁, input := [], stack := spineCutStack M A₁ context₁ } { state := spineCutState M A₂, input := [], stack := spineCutStack M A₂ context₂ } ∨ PDA.Reaches { state := spineCutState M A₂, input := [], stack := spineCutStack M A₂ context₂ } { state := spineCutState M A₁, input := [], stack := spineCutStack M A₁ context₁ }

All paired visible-anchor cuts are comparable. Read anchors are equal, split anchors use the deterministic simulation or drain phase, and the boot case reduces to the literal initial configuration.

Removing the untouched outer context of a zero-visible tail

theorem DPDA_to_LR.ZeroVisibleTail.reachesCutWithoutAnchorContext {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} {preWord : List T} {anchor current : Nonterminal M} {anchorSuffix currentSuffix : List T} {anchorContext currentContext : List (StackSymbol M)} (h : ZeroVisibleTail M p preWord anchor anchorSuffix anchorContext current currentSuffix currentContext) : ∃ (added : List (StackSymbol M)), currentContext = added ++ anchorContext ∧ PDA.Reaches { state := spineCutState M anchor, input := [], stack := spineCutStack M anchor [] } { state := spineCutState M current, input := [], stack := spineCutStack M current added }

A zero-visible tail has a context-free operational realization. The returned added block is exactly what the tail inserted immediately above the anchor's untouched outer context.

theorem DPDA_to_LR.epsilonBearing_sameListCutTail_false {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 anchorTarget currentTarget final : State M} {gamma : List (StackSymbol M)} {anchorSuffix currentSuffix completion : List T} {anchorContext currentContext : List (StackSymbol M)} (htail : ZeroVisibleTail M p preWord (PDA_to_CFG.N.list q gamma anchorTarget) anchorSuffix anchorContext (PDA_to_CFG.N.list q gamma currentTarget) currentSuffix currentContext) (hbearing : EpsilonBearingZeroVisibleTail M p preWord (PDA_to_CFG.N.list q gamma anchorTarget) anchorSuffix anchorContext (PDA_to_CFG.N.list q gamma currentTarget) currentSuffix currentContext) (hgamma : ↑gamma.length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hcomplete : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list q gamma currentTarget)] (List.map symbol.terminal completion)) (hcontinuation : PDA.Reaches { state := currentTarget, input := currentSuffix, stack := currentContext } { state := final, input := [], stack := [] }) : False

A zero-visible tail cannot return nontrivially to the same list nonterminal on a productive spine. With no inserted context it is a useful cycle; with a nonempty inserted block it is useful stack growth.

Paired read/epsilon synchronization

theorem DPDA_to_LR.visibleReadAnchor_aligned_data_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base p₂ : List (symbol T (Nonterminal M))} {beforeWord preWord₂ : List T} {a : T} {suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {q₁ target₁ next₁ : State M} {Z₁ : StackSymbol M} {gamma₁ : List (StackSymbol M)} {A₂ : Nonterminal M} (parent₁ : ConcreteOperationalSpine M base (PDA_to_CFG.N.single q₁ Z₁ target₁) suffix₁ beforeWord context₁) (transition₁ : (next₁, gamma₁) ∈ (emptyStackPDA M).transition_fun q₁ a Z₁) (h₂ : VisibleSpineAnchor M p₂ A₂ suffix₂ preWord₂ context₂) (hp : base ++ [symbol.terminal a] = p₂) (hw : beforeWord ++ [a] = preWord₂) : ∃ (target₂ : State M), A₂ = PDA_to_CFG.N.list next₁ gamma₁ target₂ ∧ context₂ = context₁

Any visible anchor aligned with a concrete read anchor is another read anchor with the same physical output data.

theorem DPDA_to_LR.concreteRead_epsilon_false {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base childPrefix : List (symbol T (Nonterminal M))} {beforeWord preWord : List T} {a : T} {suffixRead suffixEpsilon : List T} {readContext epsilonContext : List (StackSymbol M)} {qRead qEpsilon next target : State M} {ZRead ZEpsilon : StackSymbol M} {gamma : List (StackSymbol M)} (readParent : ConcreteOperationalSpine M base (PDA_to_CFG.N.single qRead ZRead target) suffixRead beforeWord readContext) (readTransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun qRead a ZRead) (epsilonParent : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single qEpsilon ZEpsilon target) suffixEpsilon preWord epsilonContext) (epsilonTransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' qEpsilon ZEpsilon) (epsilonRule : (PDA_to_CFG.N.single qEpsilon ZEpsilon target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (hprefix : base ++ [symbol.terminal a] = childPrefix) (hword : beforeWord ++ [a] = preWord) : False

A concrete read edge and a concrete epsilon edge cannot introduce the same active list child. Aligning their last visible read anchors makes the epsilon side a productive nonempty return to the same physical list cut.

theorem DPDA_to_LR.activeRead_epsilon_false {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base childPrefix : List (symbol T (Nonterminal M))} {a : T} {suffixRead suffixEpsilon : List T} {qRead qEpsilon next target : State M} {ZRead ZEpsilon : StackSymbol M} {gamma : List (StackSymbol M)} (readParent : ActiveSpine M base (PDA_to_CFG.N.single qRead ZRead target) suffixRead) (readTransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun qRead a ZRead) (readRule : (PDA_to_CFG.N.single qRead ZRead target, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (epsilonParent : ActiveSpine M childPrefix (PDA_to_CFG.N.single qEpsilon ZEpsilon target) suffixEpsilon) (epsilonTransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' qEpsilon ZEpsilon) (epsilonRule : (PDA_to_CFG.N.single qEpsilon ZEpsilon target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (hprefix : base ++ [symbol.terminal a] = childPrefix) : False

Active-spine form of concreteRead_epsilon_false, obtaining the common visible-prefix completion and exact hidden contexts internally.