Determinism of useful paths in the normalized empty-stack wrapper

The final-state-to-empty-stack wrapper has one deliberate source of nondeterminism: a normalized final state may either keep simulating or enter the fresh drain state. On a globally reachable computation, two successor steps which both retain an empty-stack continuation nevertheless agree. A simulation step competing with the drain step would give a nonempty path from a normalized final configuration to a later normalized final configuration, contrary to first-final normalization.

theorem DPDA_to_LR.normalized_epsilon_output_unique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p₁ p₂ : Q × Bool} {Z : S} {α₁ α₂ : List S} (h₁ : (p₁, α₁) ∈ M.firstFinal.toPDA.transition_fun' q Z) (h₂ : (p₂, α₂) ∈ M.firstFinal.toPDA.transition_fun' q Z) : (p₁, α₁) = (p₂, α₂)

theorem DPDA_to_LR.emptyStack_read_output_unique_local {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q next₁ next₂ : EState M} {a : T} {Z : EStack M} {gamma₁ gamma₂ : List (EStack M)} (h₁ : (next₁, gamma₁) ∈ (emptyStackPDA M).transition_fun q a Z) (h₂ : (next₂, gamma₂) ∈ (emptyStackPDA M).transition_fun q a Z) : (next₁, gamma₁) = (next₂, gamma₂)

theorem DPDA_to_LR.read_epsilon_not_both_useful {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {a : T} {tail : List T} {q : EState M} {Z : EStack M} {pRead pEps : EState M} {alphaRead alphaEps rest : List (EStack M)} {final : EState M} (hread : (pRead, alphaRead) ∈ (emptyStackPDA M).transition_fun q a Z) (hepsilon : (pEps, alphaEps) ∈ (emptyStackPDA M).transition_fun' q Z) (huseful : PDA.Reaches { state := pEps, input := a :: tail, stack := alphaEps ++ rest } { state := final, input := [], stack := [] }) : False

theorem DPDA_to_LR.emptyStack_globally_useful_step_deterministic {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w : List T} {source next₁ next₂ : (emptyStackPDA M).conf} {final₁ final₂ : EState M} (hglobal : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } source) (hstep₁ : PDA.Reaches₁ source next₁) (hstep₂ : PDA.Reaches₁ source next₂) (huseful₁ : PDA.Reaches next₁ { state := final₁, input := [], stack := [] }) (huseful₂ : PDA.Reaches next₂ { state := final₂, input := [], stack := [] }) : next₁ = next₂

From a globally reachable source, two one-step successors which both have an empty-stack continuation are equal.

theorem DPDA_to_LR.emptyStack_globally_useful_reachesIn_deterministic {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w : List T} {n : ℕ} {c₁ c₂ : (emptyStackPDA M).conf} {final₁ final₂ : EState M} (h₁ : PDA.ReachesIn n { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } c₁) (h₂ : PDA.ReachesIn n { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } c₂) (huseful₁ : PDA.Reaches c₁ { state := final₁, input := [], stack := [] }) (huseful₂ : PDA.Reaches c₂ { state := final₂, input := [], stack := [] }) : c₁ = c₂

Two equal-length paths from the same global initial configuration have the same endpoint whenever both endpoints still have an empty-stack continuation.