theorem DPDA.is_PDA_acceptsByFinalState {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : PDA.is_PDA M.acceptsByFinalState

Every language accepted by a DPDA via final-state acceptance is accepted by some PDA via empty-stack acceptance.

theorem DPDA_subclass_PDA {T : Type} [Fintype T] : DPDA.Class ⊆ PDA.Class

The class of DPDA-recognizable languages is contained in the class of PDA-recognizable languages.