Ordering useful cuts across changed input suffixes

Equal-length cross-input synchronization also compares cuts reached after different numbers of steps. If both cuts have consumed the same visible prefix and the first count is smaller, the second run contains a genuinely nonempty, input-preserving segment between the corresponding physical cuts.

theorem DPDA_to_LR.emptyStack_cross_input_strict_extension {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {pre tail₁ tail₂ : List T} {n m : ℕ} {q₁ q₂ final₁ final₂ : EState M} {gamma₁ gamma₂ : List (EStack M)} (h₁ : PDA.ReachesIn n { state := (emptyStackPDA M).initial_state, input := pre ++ tail₁, stack := [(emptyStackPDA M).start_symbol] } { state := q₁, input := tail₁, stack := gamma₁ }) (h₂ : PDA.ReachesIn m { state := (emptyStackPDA M).initial_state, input := pre ++ tail₂, stack := [(emptyStackPDA M).start_symbol] } { state := q₂, input := tail₂, stack := gamma₂ }) (huseful₁ : PDA.Reaches { state := q₁, input := tail₁, stack := gamma₁ } { state := final₁, input := [], stack := [] }) (huseful₂ : PDA.Reaches { state := q₂, input := tail₂, stack := gamma₂ } { state := final₂, input := [], stack := [] }) (hlook : List.take 1 tail₁ = List.take 1 tail₂) (hlt : n < m) : ∃ (k : ℕ), 0 < k ∧ PDA.ReachesIn k { state := q₁, input := tail₁, stack := gamma₁ } { state := q₂, input := tail₁, stack := gamma₂ }

A later useful cut at the same consumed prefix is reached from the earlier corresponding cut by a positive epsilon-only segment. The segment is transported to the first run's untouched suffix.

theorem DPDA_to_LR.emptyStack_cross_input_strict_extension_symm {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {pre tail₁ tail₂ : List T} {n m : ℕ} {q₁ q₂ final₁ final₂ : EState M} {gamma₁ gamma₂ : List (EStack M)} (h₁ : PDA.ReachesIn n { state := (emptyStackPDA M).initial_state, input := pre ++ tail₁, stack := [(emptyStackPDA M).start_symbol] } { state := q₁, input := tail₁, stack := gamma₁ }) (h₂ : PDA.ReachesIn m { state := (emptyStackPDA M).initial_state, input := pre ++ tail₂, stack := [(emptyStackPDA M).start_symbol] } { state := q₂, input := tail₂, stack := gamma₂ }) (huseful₁ : PDA.Reaches { state := q₁, input := tail₁, stack := gamma₁ } { state := final₁, input := [], stack := [] }) (huseful₂ : PDA.Reaches { state := q₂, input := tail₂, stack := gamma₂ } { state := final₂, input := [], stack := [] }) (hlook : List.take 1 tail₁ = List.take 1 tail₂) (hlt : m < n) : ∃ (k : ℕ), 0 < k ∧ PDA.ReachesIn k { state := q₂, input := tail₂, stack := gamma₂ } { state := q₁, input := tail₂, stack := gamma₁ }

Symmetric orientation of emptyStack_cross_input_strict_extension.