Accepting paths of the normalized empty-stack PDA

The final-state-to-empty-stack conversion has a fresh boot state and a fresh drain state. A globally reachable configuration with empty input and empty stack cannot still be the boot configuration or a simulated configuration: both of those retain the fresh bottom-of-stack marker. Consequently every globally accepting path ends in the drain state.

theorem DPDA_to_LR.emptyStack_reachable_simulation_shape {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w input : List T} {q : Q × Bool} {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 }) : ∃ (gamma : List S), stack = List.map some gamma ++ [none] ∧ PDA.Reaches { state := M.firstFinal.initial_state, input := w, stack := [M.firstFinal.start_symbol] } { state := q, input := input, stack := gamma }

A globally reachable simulation state still has the fresh bottom marker, and its prefix above that marker is the image of an actual normalized-DPDA stack.

theorem DPDA_to_LR.emptyStack_accepting_state_eq_drain {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {w : List T} {q : Q × Bool ⊕ Fin 2} (h : PDA.Reaches { state := (emptyStackPDA M).initial_state, input := w, stack := [(emptyStackPDA M).start_symbol] } { state := q, input := [], stack := [] }) : q = Sum.inr 1

Every empty-stack computation of the normalized machine, when started at its global initial configuration, finishes in the distinguished drain state.