Uniqueness of productive first moves

The empty-stack PDA has one apparent source of nondeterminism: at a normalized final state it may either keep simulating or enter the drain state. A drain move can only complete on empty input. If a simulated epsilon move could also complete there, it would give a nonempty epsilon-only path between two normalized final configurations, contradicting first-final normalization. Thus one symbol of lookahead determines every productive first move.

theorem DPDA_to_LR.productiveFirstMove_unique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q target : EState M} {Z : EStack M} {x y : List T} {sig₁ sig₂ : FirstMoveSignature M} (hlook : List.take 1 x = List.take 1 y) (h₁ : ProductiveFirstMove M q Z x target sig₁) (h₂ : ProductiveFirstMove M q Z y target sig₂) : sig₁ = sig₂

One symbol of lookahead uniquely determines a productive first move for a fixed characteristic-nonterminal target.