LanglibUseful-path determinism across a changed input suffix #
Two useful wrapper runs may start with different complete input words. If the words share the prefix consumed by one run, their first residual symbols agree, and the runs have the same number of steps, the other run consumes exactly the same prefix and reaches the same control state and stack.
theorem
DPDA_to_LR.emptyStack_globally_useful_reachesIn_cross_input
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{pre tail₁ tail₂ residual₂ : List T}
{n : ℕ}
{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 n
{ state := (emptyStackPDA M).initial_state, input := pre ++ tail₂, stack := [(emptyStackPDA M).start_symbol] }
{ state := q₂, input := residual₂, stack := gamma₂ })
(huseful₁ : PDA.Reaches { state := q₁, input := tail₁, stack := gamma₁ } { state := final₁, input := [], stack := [] })
(huseful₂ :
PDA.Reaches { state := q₂, input := residual₂, stack := gamma₂ } { state := final₂, input := [], stack := [] })
(hlook : List.take 1 tail₁ = List.take 1 tail₂)
:
Equal-length useful runs synchronize even when their untouched input
suffixes differ. The first displayed endpoint is the no-overrun hypothesis:
it has consumed precisely prefix and none of tail₁.
theorem
DPDA_to_LR.emptyStack_globally_useful_reachesIn_cross_input_symm
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : DPDA Q T S)
{pre tail₁ tail₂ residual₁ : List T}
{n : ℕ}
{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 := residual₁, stack := gamma₁ })
(h₂ :
PDA.ReachesIn n
{ 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 := residual₁, 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₂)
:
Symmetric form: the second run is the one known not to consume into its tail.