Determinism of DPDA computations

The Option-valued transition functions and DPDA.no_mixed make the embedded PDA transition relation functional. This file records the corresponding one-step, fixed-length-run, and prefix-comparison theorems for arbitrary DPDAs.

theorem DPDA.toPDA_step_deterministic {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c d₁ d₂ : M.toPDA.conf} (h₁ : PDA.Reaches₁ c d₁) (h₂ : PDA.Reaches₁ c d₂) : d₁ = d₂

The PDA step relation underlying a DPDA is functional.

theorem DPDA.toPDA_reachesIn_deterministic {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {n : ℕ} {c c₁ c₂ : M.toPDA.conf} (h₁ : PDA.ReachesIn n c c₁) (h₂ : PDA.ReachesIn n c c₂) : c₁ = c₂

Two computations of the same length from the same configuration have the same endpoint.

theorem DPDA.toPDA_reachesIn_prefix_of_le {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {n m : ℕ} {c c₁ c₂ : M.toPDA.conf} (hnm : n ≤ m) (h₁ : PDA.ReachesIn n c c₁) (h₂ : PDA.ReachesIn m c c₂) : PDA.Reaches c₁ c₂

A shorter deterministic computation is the unique prefix of a longer one.

theorem DPDA.toPDA_reaches_comparable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c c₁ c₂ : M.toPDA.conf} (h₁ : PDA.Reaches c c₁) (h₂ : PDA.Reaches c c₂) : PDA.Reaches c₁ c₂ ∨ PDA.Reaches c₂ c₁

Any two finite computations from one configuration are prefix-comparable.