Comparing FS→ES cuts at displaced input positions

Visible characteristic prefixes may differ by a terminal block. Lifting the earlier global prefix path by that unconsumed block puts both operational cuts under one global input. This module packages the resulting comparisons, including the phase split needed when one endpoint has already entered the FS→ES drain.

theorem DPDA_to_LR.emptyStack_global_simulation_cuts_comparable_any_input {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w input₁ input₂ : List T} {q₁ q₂ : Q × Bool} {stack₁ stack₂ : List (Option S)} (h₁ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inl q₁, input := input₁, stack := stack₁ }) (h₂ : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inl q₂, input := input₂, stack := stack₂ }) : PDA.Reaches { state := Sum.inl q₁, input := input₁, stack := stack₁ } { state := Sum.inl q₂, input := input₂, stack := stack₂ } ∨ PDA.Reaches { state := Sum.inl q₂, input := input₂, stack := stack₂ } { state := Sum.inl q₁, input := input₁, stack := stack₁ }

Globally reachable simulation cuts are comparable even when they have consumed different amounts of the common input.

theorem DPDA_to_LR.emptyStack_global_simulation_drain_useful_any_input {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w simInput drainInput : List T} {q : Q × Bool} {simStack drainStack : List (Option S)} {final₁ final₂ : EState M} (hsimGlobal : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inl q, input := simInput, stack := simStack }) (hdrainGlobal : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := Sum.inr 1, input := drainInput, stack := drainStack }) (hsimUseful : PDA.Reaches { state := Sum.inl q, input := simInput, stack := simStack } { state := final₁, input := [], stack := [] }) (hdrainUseful : PDA.Reaches { state := Sum.inr 1, input := drainInput, stack := drainStack } { state := final₂, input := [], stack := [] }) : PDA.Reaches { state := Sum.inl q, input := simInput, stack := simStack } { state := Sum.inr 1, input := drainInput, stack := drainStack }

A useful simulation cut precedes a useful drain cut even when the two global prefixes expose different remaining inputs. Drain usefulness forces its input to be empty. A nonempty simulation input orients the normalized comparison by input monotonicity; the empty-input case is the existing first-final comparison.

theorem DPDA_to_LR.emptyStack_global_productive_extension {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {u z sOne sTwo : List T} {qOne qTwo : EState M} {stackOne stackTwo : List (EStack M)} {finalOne finalTwo : EState M} (hz : z ≠ []) (hOne : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := u, stack := [(emptyStackPDA M).start_symbol] } { state := qOne, input := [], stack := stackOne }) (hTwo : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := u ++ z, stack := [(emptyStackPDA M).start_symbol] } { state := qTwo, input := [], stack := stackTwo }) (useOne : PDA.Reaches { state := qOne, input := sOne, stack := stackOne } { state := finalOne, input := [], stack := [] }) (useTwo : PDA.Reaches { state := qTwo, input := sTwo, stack := stackTwo } { state := finalTwo, input := [], stack := [] }) (hlook : List.take 1 sOne = List.take 1 (z ++ sTwo)) : PDA.Reaches { state := qOne, input := z, stack := stackOne } { state := qTwo, input := [], stack := stackTwo }

If two globally reached productive cuts are separated by a nonempty terminal block, the earlier cut processes exactly that block to the later cut. The proof is phase-aware: simulation cuts use normalized determinism, a later drain cut uses the oriented mixed comparison, and a boot endpoint is inverted to the literal initial configuration.