theorem is_PDA_of_mathlib_cfg {T : Type} [Fintype T] (g : ContextFreeGrammar T) [Fintype g.NT] : PDA.is_PDA g.language

theorem mathlib_cfg_of_PDA {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) : (PDA_to_CFG.G M).language = M.acceptsByEmptyStack

theorem isContextFree_of_is_PDA {T : Type} [Fintype T] {L : Language T} : PDA.is_PDA L → L.IsContextFree

theorem is_CF_of_is_PDA {T : Type} [Fintype T] {L : Language T} : PDA.is_PDA L → is_CF L

theorem is_PDA_of_isContextFree {T : Type} [Fintype T] {L : Language T} (hL : L.IsContextFree) : PDA.is_PDA L

Every context-free language (with possibly infinite NT) is accepted by some PDA. This removes the [Fintype g.NT] requirement from is_PDA_of_mathlib_cfg by first restricting the grammar to one with finite nonterminals.

theorem is_PDA_iff_isContextFree {T : Type} [Fintype T] {L : Language T} : PDA.is_PDA L ↔ L.IsContextFree

The PDA-recognizable languages are exactly the context-free languages.

theorem CF_eq_PDA_Class {T : Type} [Fintype T] : CF = PDA.Class

The class of context-free languages equals the class of PDA-recognizable languages.