Synchronizing two epsilon introductions

Two epsilon rules which introduce the same characteristic list child have the same productive future. This file isolates the counted synchronization argument from the remaining structural ancestry argument: equal global positions force the two source heads to be literally equal, even though the terminal suffixes following the child may differ.

theorem DPDA_to_LR.LeftmostEpsilonTrace.expandListContext_toSingle {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q source : State M} {Z : StackSymbol M} {displayed context finalContext : List (StackSymbol M)} (trace : LeftmostEpsilonTrace M (LeftmostEpsilonPosition.list q displayed context) (LeftmostEpsilonPosition.single source Z finalContext)) : LeftmostEpsilonTrace M (LeftmostEpsilonPosition.list q (displayed ++ context) []) (LeftmostEpsilonPosition.single source Z finalContext)

A leftmost structural trace from a list position to a single position may move the entire hidden context into the displayed list at its source. The trace cannot be reflexive, and its first event is necessarily split; after that event both source decompositions reach the identical single position.

theorem DPDA_to_LR.leftmostEpsilonTrace_converging_heads_eq_of_list_cut_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {anchorState₁ anchorState₂ q₁ q₂ next final₁ final₂ : State M} {Z₁ Z₂ : StackSymbol M} {displayed₁ displayed₂ anchorContext₁ anchorContext₂ gamma context₁ context₂ : List (StackSymbol M)} {suffix₁ suffix₂ whole₁ whole₂ : List T} (trace₁ : LeftmostEpsilonTrace M (LeftmostEpsilonPosition.list anchorState₁ displayed₁ anchorContext₁) (LeftmostEpsilonPosition.single q₁ Z₁ context₁)) (trace₂ : LeftmostEpsilonTrace M (LeftmostEpsilonPosition.list anchorState₂ displayed₂ anchorContext₂) (LeftmostEpsilonPosition.single q₂ Z₂ context₂)) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (hstate : anchorState₁ = anchorState₂) (hstack : displayed₁ ++ anchorContext₁ = displayed₂ ++ anchorContext₂) (global₁ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₁, stack := [(emptyStackPDA M).start_symbol] } (LeftmostEpsilonPosition.conf M suffix₁ (LeftmostEpsilonPosition.list anchorState₁ displayed₁ anchorContext₁))) (global₂ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := whole₂, stack := [(emptyStackPDA M).start_symbol] } (LeftmostEpsilonPosition.conf M suffix₂ (LeftmostEpsilonPosition.list anchorState₂ displayed₂ anchorContext₂))) (useful₁ : PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₁ (LeftmostEpsilonPosition.list next gamma context₁)) { state := final₁, input := [], stack := [] }) (useful₂ : PDA.Reaches (LeftmostEpsilonPosition.conf M suffix₂ (LeftmostEpsilonPosition.list next gamma context₂)) { state := final₂, input := [], stack := [] }) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂

Converging epsilon exits also synchronize when their two structural traces start from different displayed/hidden decompositions of the same physical list cut. Expanding both source contexts into their displayed lists gives a literal common LeftmostEpsilonPosition, after which the general converging-trace theorem applies.

theorem DPDA_to_LR.ZeroVisibleTail.fromSingle_exists_retainedFrameRun {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} {Z : StackSymbol 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.single q Z target) anchorSuffix anchorContext current currentSuffix currentContext) : ∃ (n : ℕ), (emptyStackPDA M).RetainedFrameRun anchorContext n { state := q, input := [], stack := Z :: anchorContext } { state := spineCutState M current, input := [], stack := spineCutStack M current currentContext }

A zero-visible tail starting at a single node retains the complete hidden context of that node. This is the non-anchor variant needed when one epsilon parent is assumed to be a structural descendant of the other.

theorem DPDA_to_LR.concreteEpsilonEpsilon_heads_eq_of_equal_steps {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {preWord suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {q₁ q₂ next target : State M} {Z₁ Z₂ : StackSymbol M} {gamma : List (StackSymbol M)} {steps : ℕ} (parent₁ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ preWord context₁) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (rule₁ : (PDA_to_CFG.N.single q₁ Z₁ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (parent₂ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ preWord context₂) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (rule₂ : (PDA_to_CFG.N.single q₂ Z₂ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (run₁ : PDA.ReachesIn steps { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := q₁, input := [], stack := Z₁ :: context₁ }) (run₂ : PDA.ReachesIn steps { state := (emptyStackPDA M).initial_state, input := preWord, stack := [(emptyStackPDA M).start_symbol] } { state := q₂, input := [], stack := Z₂ :: context₂ }) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂

Equal-length globally rooted realizations of two concrete epsilon introductions of the same list child have the same source state and exposed stack symbol.

The common completion of the child supplies usefulness on both sides. The one-symbol hypothesis is needed only when that completion is empty.

theorem DPDA_to_LR.concreteEpsilonEpsilon_heads_eq_of_zeroVisibleTail {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {preWord suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {q₁ q₂ next target : State M} {Z₁ Z₂ : StackSymbol M} {gamma : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ preWord context₁) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (rule₁ : (PDA_to_CFG.N.single q₁ Z₁ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (parent₂ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ preWord context₂) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (rule₂ : (PDA_to_CFG.N.single q₂ Z₂ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (tail : ZeroVisibleTail M childPrefix preWord (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ context₁ (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ context₂) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂

If the second epsilon parent is a zero-visible structural descendant of the first, the two exposed heads are equal. A genuinely nonempty descendant tail retains the first hidden context. Its first PDA step synchronizes with the direct epsilon edge to the common child; the remaining retained segment therefore repeats that child cut, either exactly or with a nonempty inserted stack block. Both alternatives contradict usefulness.

theorem DPDA_to_LR.concreteEpsilonEpsilon_heads_eq_of_zeroVisibleComparable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {preWord suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {q₁ q₂ next target : State M} {Z₁ Z₂ : StackSymbol M} {gamma : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ preWord context₁) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (rule₁ : (PDA_to_CFG.N.single q₁ Z₁ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (parent₂ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ preWord context₂) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (rule₂ : (PDA_to_CFG.N.single q₂ Z₂ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (comparable : ZeroVisibleTail M childPrefix preWord (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ context₁ (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ context₂ ∨ ZeroVisibleTail M childPrefix preWord (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ context₂ (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ context₁) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂

Symmetric interface: structural zero-visible comparability of the two parent occurrences is sufficient for epsilon/epsilon head uniqueness.

theorem DPDA_to_LR.concreteEpsilonEpsilon_heads_eq_of_anchor_position_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {preWord suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {q₁ q₂ next target : State M} {Z₁ Z₂ : StackSymbol M} {gamma : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ preWord context₁) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (rule₁ : (PDA_to_CFG.N.single q₁ Z₁ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (parent₂ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ preWord context₂) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (rule₂ : (PDA_to_CFG.N.single q₂ Z₂ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) {anchor₁ anchor₂ : Nonterminal M} {anchorSuffix₁ anchorSuffix₂ : List T} {anchorContext₁ anchorContext₂ : List (StackSymbol M)} (leftAnchor : VisibleSpineAnchor M childPrefix anchor₁ anchorSuffix₁ preWord anchorContext₁) (rightAnchor : VisibleSpineAnchor M childPrefix anchor₂ anchorSuffix₂ preWord anchorContext₂) (leftTail : ZeroVisibleTail M childPrefix preWord anchor₁ anchorSuffix₁ anchorContext₁ (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ context₁) (rightTail : ZeroVisibleTail M childPrefix preWord anchor₂ anchorSuffix₂ anchorContext₂ (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ context₂) (hposition : leftmostEpsilonPositionOf M anchor₁ anchorContext₁ = leftmostEpsilonPositionOf M anchor₂ anchorContext₂) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂

Two concrete epsilon introductions whose last-visible anchors denote the same physical position have equal source heads. The anchors may retain different grammar target indices: LeftmostEpsilonPosition deliberately forgets those indices and synchronizes the productive zero-visible traces at the operational cut.

theorem DPDA_to_LR.concreteEpsilonEpsilon_heads_eq_of_list_anchor_cut_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {preWord suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {q₁ q₂ next target : State M} {Z₁ Z₂ : StackSymbol M} {gamma : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ preWord context₁) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (rule₁ : (PDA_to_CFG.N.single q₁ Z₁ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (parent₂ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ preWord context₂) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (rule₂ : (PDA_to_CFG.N.single q₂ Z₂ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) {anchorState₁ anchorState₂ anchorTarget₁ anchorTarget₂ : State M} {displayed₁ displayed₂ : List (StackSymbol M)} {anchorSuffix₁ anchorSuffix₂ : List T} {anchorContext₁ anchorContext₂ : List (StackSymbol M)} (leftAnchor : VisibleSpineAnchor M childPrefix (PDA_to_CFG.N.list anchorState₁ displayed₁ anchorTarget₁) anchorSuffix₁ preWord anchorContext₁) (rightAnchor : VisibleSpineAnchor M childPrefix (PDA_to_CFG.N.list anchorState₂ displayed₂ anchorTarget₂) anchorSuffix₂ preWord anchorContext₂) (leftTail : ZeroVisibleTail M childPrefix preWord (PDA_to_CFG.N.list anchorState₁ displayed₁ anchorTarget₁) anchorSuffix₁ anchorContext₁ (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ context₁) (rightTail : ZeroVisibleTail M childPrefix preWord (PDA_to_CFG.N.list anchorState₂ displayed₂ anchorTarget₂) anchorSuffix₂ anchorContext₂ (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ context₂) (hstate : anchorState₁ = anchorState₂) (hstack : displayed₁ ++ anchorContext₁ = displayed₂ ++ anchorContext₂) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂

Two concrete epsilon introductions also synchronize when their selected last-visible anchors are list nodes with the same physical PDA cut. The displayed lists and hidden contexts need not agree separately: equality of their concatenations is exactly the information supplied by equality of two split-return endpoint configurations.

def DPDA_to_LR.PairedSplitEpsilonEpsilonHeadsData {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (childPrefix : List (symbol T (Nonterminal M))) (q₁ q₂ next target : State M) (Z₁ Z₂ : StackSymbol M) (gamma : List (StackSymbol M)) (suffix₁ suffix₂ : List T) : Prop

The last structural residual for two epsilon introductions of one list child. Both concrete parents and their zero-visible ancestries are retained. The paired anchors have unequal physical positions; paired root and read anchors therefore cannot inhabit this datum, so its paired witness is necessarily a splitRight/splitRight pair.

Keeping the position inequality, rather than flattening the split constructor into a large tuple, preserves the two original structural spines for the interval argument which consumes this residual.

Equations

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

theorem DPDA_to_LR.concreteEpsilonEpsilon_heads_eq_or_pairedSplit {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {preWord suffix₁ suffix₂ : List T} {context₁ context₂ : List (StackSymbol M)} {q₁ q₂ next target : State M} {Z₁ Z₂ : StackSymbol M} {gamma : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁ preWord context₁) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (rule₁ : (PDA_to_CFG.N.single q₁ Z₁ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (parent₂ : ConcreteOperationalSpine M childPrefix (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂ preWord context₂) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (rule₂ : (PDA_to_CFG.N.single q₂ Z₂ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂ ∨ PairedSplitEpsilonEpsilonHeadsData M childPrefix q₁ q₂ next target Z₁ Z₂ gamma suffix₁ suffix₂

Concrete epsilon introductions either synchronize at their paired last-visible anchor, or expose the exact unequal-position paired-split residual. Root and read pairs have equal physical anchor positions, so the right disjunct can only survive the splitRight constructor of PairedVisibleAnchors.

theorem DPDA_to_LR.activeEpsilonEpsilon_heads_eq_or_pairedSplit {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {suffix₁ suffix₂ : List T} {q₁ q₂ next target : State M} {Z₁ Z₂ : StackSymbol M} {gamma : List (StackSymbol M)} (parent₁ : ActiveSpine M childPrefix (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (rule₁ : (PDA_to_CFG.N.single q₁ Z₁ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (parent₂ : ActiveSpine M childPrefix (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (rule₂ : (PDA_to_CFG.N.single q₂ Z₂ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂ ∨ PairedSplitEpsilonEpsilonHeadsData M childPrefix q₁ q₂ next target Z₁ Z₂ gamma suffix₁ suffix₂

Active-spine interface for the same classifier. A single completion of the shared child prefix is chosen first, so both returned concrete parent spines live over the same completed word.

def DPDA_to_LR.UnequalCountEpsilonEpsilonHeadsData {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (childPrefix : List (symbol T (Nonterminal M))) (q₁ q₂ next target : State M) (Z₁ Z₂ : StackSymbol M) (gamma : List (StackSymbol M)) (suffix₁ suffix₂ : List T) : Prop

The exact unequal-position residual for two epsilon introductions. It retains the normalized parent spines and their globally counted source cuts; no interval or hidden context has been compressed away.

Equations

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

theorem DPDA_to_LR.activeEpsilonEpsilon_heads_eq_or_unequal_counts {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {suffix₁ suffix₂ : List T} {q₁ q₂ next target : State M} {Z₁ Z₂ : StackSymbol M} {gamma : List (StackSymbol M)} (parent₁ : ActiveSpine M childPrefix (PDA_to_CFG.N.single q₁ Z₁ target) suffix₁) (transition₁ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₁ Z₁) (rule₁ : (PDA_to_CFG.N.single q₁ Z₁ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (parent₂ : ActiveSpine M childPrefix (PDA_to_CFG.N.single q₂ Z₂ target) suffix₂) (transition₂ : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q₂ Z₂) (rule₂ : (PDA_to_CFG.N.single q₂ Z₂ target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (hlook : List.take 1 suffix₁ = List.take 1 suffix₂) : q₁ = q₂ ∧ Z₁ = Z₂ ∨ UnequalCountEpsilonEpsilonHeadsData M childPrefix q₁ q₂ next target Z₁ Z₂ gamma suffix₁ suffix₂

Active epsilon introductions either already have equal source heads, or expose the exact unequal-count structural datum needed by the frontier-trace comparison argument.

theorem DPDA_to_LR.UnequalCountEpsilonEpsilonHeadsData.strict_extension {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {suffix₁ suffix₂ : List T} {q₁ q₂ next target : State M} {Z₁ Z₂ : StackSymbol M} {gamma : List (StackSymbol M)} (data : UnequalCountEpsilonEpsilonHeadsData M childPrefix q₁ q₂ next target Z₁ Z₂ gamma suffix₁ suffix₂) : ∃ (childWord : List T) (context₁ : List (StackSymbol M)) (context₂ : List (StackSymbol M)) (final₁ : State M) (final₂ : State M), PDA.Reaches { state := next, input := childWord ++ suffix₁, stack := gamma ++ context₁ } { state := final₁, input := [], stack := [] } ∧ PDA.Reaches { state := next, input := childWord ++ suffix₂, stack := gamma ++ context₂ } { state := final₂, input := [], stack := [] } ∧ ((∃ (k : ℕ), 0 < k ∧ PDA.ReachesIn k { state := q₁, input := childWord ++ suffix₁, stack := Z₁ :: context₁ } { state := q₂, input := childWord ++ suffix₁, stack := Z₂ :: context₂ }) ∨ ∃ (k : ℕ), 0 < k ∧ PDA.ReachesIn k { state := q₂, input := childWord ++ suffix₂, stack := Z₂ :: context₂ } { state := q₁, input := childWord ++ suffix₂, stack := Z₁ :: context₁ })

Operational orientation of the unequal-count residual. Besides the positive epsilon-only segment between the two parent cuts, the conclusion retains a common completion of the shared child and both useful child endpoints. These are the exact ingredients needed to rule out a purported structural extension by the useful-cycle and stack-growth kernels.