The concrete overlap behind an epsilon/split conflict

An epsilon introduction and a split-right introduction of the same list child have the same completed visible prefix. Decomposing the epsilon parent at its last visible event therefore produces a paired visible anchor; the tail on that side is genuinely epsilon-bearing, while the other anchor is the displayed split-right child itself. This file packages that exact configuration together with a common completion of the list child.

inductive DPDA_to_LR.EpsilonSplitTailData {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (childPrefix : List (symbol T (Nonterminal M))) (next target : State M) (gamma : List (StackSymbol M)) (epsilonSuffix splitSuffix : List T) : Prop

All ancestry and productivity data present in an active epsilon/split conflict after choosing one common completion of the shared list child.

• mk {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {childPrefix : List (symbol T (Nonterminal M))} {next target : State M} {gamma : List (StackSymbol M)} {epsilonSuffix splitSuffix : List T} (preWord : List T) (epsilonContext splitContext : List (StackSymbol M)) (base : List (symbol T (Nonterminal M))) (beforeWord leftWord : List T) (splitSource : State M) (splitTop : StackSymbol M) (splitParent : ConcreteOperationalSpine M base (PDA_to_CFG.N.list splitSource (splitTop :: gamma) target) splitSuffix beforeWord splitContext) (splitLength : ↑(splitTop :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (splitRule : (PDA_to_CFG.N.list splitSource (splitTop :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single splitSource splitTop next), symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (splitLeft : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single splitSource splitTop next)] (List.map symbol.terminal leftWord)) (childPrefixEq : childPrefix = base ++ [symbol.nonterminal (PDA_to_CFG.N.single splitSource splitTop next)]) (preWordEq : preWord = beforeWord ++ leftWord) (anchor : Nonterminal M) (anchorSuffix : List T) (anchorContext : List (StackSymbol M)) (anchorWitness : VisibleSpineAnchor M childPrefix anchor anchorSuffix preWord anchorContext) (tail : ZeroVisibleTail M childPrefix preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.list next gamma target) epsilonSuffix epsilonContext) (bearing : EpsilonBearingZeroVisibleTail M childPrefix preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.list next gamma target) epsilonSuffix epsilonContext) (splitAnchor : VisibleSpineAnchor M childPrefix (PDA_to_CFG.N.list next gamma target) splitSuffix preWord splitContext) (paired : PairedVisibleAnchors M childPrefix preWord anchor anchorSuffix anchorContext (PDA_to_CFG.N.list next gamma target) splitSuffix splitContext) (childWord : List T) (childCompletion : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)] (List.map symbol.terminal childWord)) (epsilonFinal splitFinal : State M) (epsilonUseful : PDA.Reaches { state := next, input := childWord ++ epsilonSuffix, stack := gamma ++ epsilonContext } { state := epsilonFinal, input := [], stack := [] }) (splitUseful : PDA.Reaches { state := next, input := childWord ++ splitSuffix, stack := gamma ++ splitContext } { state := splitFinal, input := [], stack := [] }) (suffixLookahead : List.take 1 epsilonSuffix = List.take 1 splitSuffix) (futureLookahead : List.take 1 (childWord ++ epsilonSuffix) = List.take 1 (childWord ++ splitSuffix)) : EpsilonSplitTailData M childPrefix next target gamma epsilonSuffix splitSuffix

theorem DPDA_to_LR.activeEpsilonSplit_tailData {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix base : List (symbol T (Nonterminal M))} {epsilonSuffix splitSuffix : List T} {epsilonSource next target splitSource : State M} {epsilonTop splitTop : StackSymbol M} {gamma : List (StackSymbol M)} (epsilonParent : ActiveSpine M childPrefix (PDA_to_CFG.N.single epsilonSource epsilonTop target) epsilonSuffix) (epsilonTransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' epsilonSource epsilonTop) (epsilonRule : (PDA_to_CFG.N.single epsilonSource epsilonTop target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (splitParent : ActiveSpine M base (PDA_to_CFG.N.list splitSource (splitTop :: gamma) target) splitSuffix) (splitLength : ↑(splitTop :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (splitRule : (PDA_to_CFG.N.list splitSource (splitTop :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single splitSource splitTop next), symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (hprefix : childPrefix = base ++ [symbol.nonterminal (PDA_to_CFG.N.single splitSource splitTop next)]) (hlook : List.take 1 epsilonSuffix = List.take 1 splitSuffix) : EpsilonSplitTailData M childPrefix next target gamma epsilonSuffix splitSuffix

Construct the exact paired-anchor/epsilon-tail configuration from the two active introductions. The theorem deliberately keeps the paired anchor abstract; inversion of data.paired exposes the two split-right return intervals and their hidden contexts without losing the tail.

inductive DPDA_to_LR.EpsilonSplitReturnData {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (next target : State M) (gamma : List (StackSymbol M)) (epsilonSuffix splitSuffix : List T) : Prop

The only possible paired-anchor branch of an epsilon/split conflict is split-right/split-right. This proposition is the fully specialized branch, with no dependent equalities or irrelevant read case left to invert.

• mk {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {next target : State M} {gamma : List (StackSymbol M)} {epsilonSuffix splitSuffix : List T} (preWord childWord : List T) (epsilonContext splitContext : List (StackSymbol M)) (base : List (symbol T (Nonterminal M))) (anchorSuffix : List T) (anchorContext : List (StackSymbol M)) (beforeWord₁ leftWord₁ beforeWord₂ leftWord₂ : List T) (source target₁ : State M) (top : StackSymbol M) (gamma₁ : List (StackSymbol M)) (parent₁ : ConcreteOperationalSpine M base (PDA_to_CFG.N.list source (top :: gamma₁) target₁) anchorSuffix beforeWord₁ anchorContext) (length₁ : ↑(top :: gamma₁).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (rule₁ : (PDA_to_CFG.N.list source (top :: gamma₁) target₁, [symbol.nonterminal (PDA_to_CFG.N.single source top next), symbol.nonterminal (PDA_to_CFG.N.list next gamma₁ target₁)]) ∈ (characteristicGrammar M).rules) (left₁ : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top next)] (List.map symbol.terminal leftWord₁)) (parent₂ : ConcreteOperationalSpine M base (PDA_to_CFG.N.list source (top :: gamma) target) splitSuffix beforeWord₂ splitContext) (length₂ : ↑(top :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (rule₂ : (PDA_to_CFG.N.list source (top :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single source top next), symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) (left₂ : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top next)] (List.map symbol.terminal leftWord₂)) (word₁ : preWord = beforeWord₁ ++ leftWord₁) (word₂ : preWord = beforeWord₂ ++ leftWord₂) (tail : ZeroVisibleTail M (base ++ [symbol.nonterminal (PDA_to_CFG.N.single source top next)]) preWord (PDA_to_CFG.N.list next gamma₁ target₁) anchorSuffix anchorContext (PDA_to_CFG.N.list next gamma target) epsilonSuffix epsilonContext) (bearing : EpsilonBearingZeroVisibleTail M (base ++ [symbol.nonterminal (PDA_to_CFG.N.single source top next)]) preWord (PDA_to_CFG.N.list next gamma₁ target₁) anchorSuffix anchorContext (PDA_to_CFG.N.list next gamma target) epsilonSuffix epsilonContext) (childCompletion : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)] (List.map symbol.terminal childWord)) (epsilonFinal splitFinal : State M) (epsilonUseful : PDA.Reaches { state := next, input := childWord ++ epsilonSuffix, stack := gamma ++ epsilonContext } { state := epsilonFinal, input := [], stack := [] }) (splitUseful : PDA.Reaches { state := next, input := childWord ++ splitSuffix, stack := gamma ++ splitContext } { state := splitFinal, input := [], stack := [] }) (suffixLookahead : List.take 1 epsilonSuffix = List.take 1 splitSuffix) (futureLookahead : List.take 1 (childWord ++ epsilonSuffix) = List.take 1 (childWord ++ splitSuffix)) : EpsilonSplitReturnData M next target gamma epsilonSuffix splitSuffix

theorem DPDA_to_LR.EpsilonSplitTailData.returnData {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {next target : State M} {gamma : List (StackSymbol M)} {epsilonSuffix splitSuffix : List T} (h : EpsilonSplitTailData M childPrefix next target gamma epsilonSuffix splitSuffix) : EpsilonSplitReturnData M next target gamma epsilonSuffix splitSuffix

Eliminate the impossible read/read paired-anchor branch and expose the two concrete split-right return intervals.

theorem DPDA_to_LR.epsilonSplitTail_false_of_gamma_eq {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base : List (symbol T (Nonterminal M))} {preWord : List T} {next target target₁ source : State M} {top : StackSymbol M} {gamma gamma₁ : List (StackSymbol M)} {beforeWord leftWord anchorSuffix epsilonSuffix : List T} {anchorContext epsilonContext : List (StackSymbol M)} (parent₁ : ConcreteOperationalSpine M base (PDA_to_CFG.N.list source (top :: gamma₁) target₁) anchorSuffix beforeWord anchorContext) (length₁ : ↑(top :: gamma₁).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (rule₁ : (PDA_to_CFG.N.list source (top :: gamma₁) target₁, [symbol.nonterminal (PDA_to_CFG.N.single source top next), symbol.nonterminal (PDA_to_CFG.N.list next gamma₁ target₁)]) ∈ (characteristicGrammar M).rules) (left₁ : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.single source top next)] (List.map symbol.terminal leftWord)) (hword : preWord = beforeWord ++ leftWord) (tail : ZeroVisibleTail M (base ++ [symbol.nonterminal (PDA_to_CFG.N.single source top next)]) preWord (PDA_to_CFG.N.list next gamma₁ target₁) anchorSuffix anchorContext (PDA_to_CFG.N.list next gamma target) epsilonSuffix epsilonContext) (bearing : EpsilonBearingZeroVisibleTail M (base ++ [symbol.nonterminal (PDA_to_CFG.N.single source top next)]) preWord (PDA_to_CFG.N.list next gamma₁ target₁) anchorSuffix anchorContext (PDA_to_CFG.N.list next gamma target) epsilonSuffix epsilonContext) (hgamma : gamma₁ = gamma) {childWord : List T} (childCompletion : (characteristicGrammar M).DerivesRightmost [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)] (List.map symbol.terminal childWord)) : False

If the anchor-side right-list stack already agrees with the exact child stack, the epsilon-bearing tail is immediately a forbidden useful return to the same list cut. Thus every genuine residual split branch must have different right-list stack texts.