Totalized Presentations

This file connects the analyzed DPDA totalizer to the language-level deciding presentation used by complement closure.

theorem DPDA.totalizer_is_DCF_total {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} (A : M.RegularEpsilonAnalysis) : is_DCF_total M.acceptsByFinalState

The analyzed totalizer is a deciding DPDA presentation of the same language.

def EveryDPDAHasRegularEpsilonAnalysis (T : Type) [Fintype T] : Prop

Every finite DPDA has the regular epsilon analysis required by the totalizer.

Equations

• EveryDPDAHasRegularEpsilonAnalysis T = ∀ (Q S : Type) [inst : Fintype Q] [inst_1 : Fintype S] (M : DPDA Q T S), M.HasRegularEpsilonAnalysis

theorem everyDPDAHasRegularEpsilonAnalysis {T : Type} [Fintype T] : EveryDPDAHasRegularEpsilonAnalysis T

The saturation construction gives a regular epsilon analysis for every finite DPDA.

theorem everyDCFHasDeciderPresentation_of_regularEpsilonAnalysis {T : Type} [Fintype T] (hanalysis : EveryDPDAHasRegularEpsilonAnalysis T) : EveryDCFHasDeciderPresentation T

Regular epsilon analyses for all DPDAs imply the normal form used by DCF complement closure.

theorem everyDCFHasDeciderPresentation {T : Type} [Fintype T] : EveryDCFHasDeciderPresentation T

Every DCF has an equivalent deciding-DPDA presentation.