The residual case of epsilon/split synchronization

This file separates the easy paired-read contradiction from the genuinely interval-sensitive paired-split case. In particular, the useful endpoint form below avoids rebuilding a list completion merely to exclude a nonempty zero-visible return to the same physical list cut.

theorem DPDA_to_LR.epsilonBearing_sameListCutTail_false_of_useful {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 future : 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) (huseful : PDA.Reaches { state := q, input := future, stack := gamma ++ currentContext } { state := final, input := [], stack := [] }) : False

A useful epsilon-bearing tail cannot return to the same physical list head. This is the direct-usefulness variant of epsilonBearing_sameListCutTail_false: the caller may already have the combined child-completion/continuation path.

theorem DPDA_to_LR.epsilonBearing_pairedRead_false {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {base : List (symbol T (Nonterminal M))} {beforeWord suffix₁ suffix₂ currentSuffix future : List T} {context₁ context₂ currentContext : List (StackSymbol M)} {q₁ target₁ next₁ q₂ target₂ next₂ final : State M} {a : T} {Z₁ Z₂ : StackSymbol M} {gamma₁ gamma₂ : List (StackSymbol 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₁) (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₂) (tail : ZeroVisibleTail M (base ++ [symbol.terminal a]) (beforeWord ++ [a]) (PDA_to_CFG.N.list next₁ gamma₁ target₁) suffix₁ context₁ (PDA_to_CFG.N.list next₂ gamma₂ target₂) currentSuffix currentContext) (bearing : EpsilonBearingZeroVisibleTail M (base ++ [symbol.terminal a]) (beforeWord ++ [a]) (PDA_to_CFG.N.list next₁ gamma₁ target₁) suffix₁ context₁ (PDA_to_CFG.N.list next₂ gamma₂ target₂) currentSuffix currentContext) (useful : PDA.Reaches { state := next₂, input := future, stack := gamma₂ ++ currentContext } { state := final, input := [], stack := [] }) : False

The paired-read constructor of an epsilon/split tail is impossible. Both read anchors have the same deterministic output cut, so the bearing tail is a nonempty useful return to that same physical list head.

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

The counted operational content left by the paired-split constructor. The first two intervals are the two completed single source top next returns. The last retained run is the genuinely nonempty epsilon-bearing tail from the first return endpoint to the epsilon child cut.

Equations

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

theorem DPDA_to_LR.EpsilonSplitTailData.splitRightIntervalResidual {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} (data : EpsilonSplitTailData M childPrefix next target gamma epsilonSuffix splitSuffix) : ∃ (completedWord : List T) (childWord : List T), SplitRightEpsilonIntervalResidual M completedWord next target gamma childWord epsilonSuffix splitSuffix

Every epsilon/split tail reduces to the counted paired-split residual. The root constructor is excluded by the right list index, while the read constructor is discharged by epsilonBearing_pairedRead_false.