structure EDT0LGrammar.DFAData (T : Type u_1) (Q : Type u_2) [Fintype T] [Fintype Q] : Type (max u_1 u_2)

• M : DFA T Q

noncomputable def EDT0LGrammar.DFAData.grammar {T : Type u_1} {Q : Type u_2} [Fintype T] [Fintype Q] (𝓓 : DFAData T Q) : EDT0LGrammar T Q (T ⊕ Unit)

Equations

• One or more equations did not get rendered due to their size.

theorem EDT0LGrammar.DFAData.generated_words {T : Type u_1} {Q : Type u_2} [Fintype T] [Fintype Q] (𝓓 : DFAData T Q) (w : List (Symbol T Q)) : 𝓓.grammar.Generates w → ∃ (u : List T), List.map Symbol.terminal u = w ∧ 𝓓.M.evalFrom 𝓓.M.start u ∈ 𝓓.M.accept ∨ w = List.map Symbol.terminal u ++ [Symbol.nonterminal (𝓓.M.evalFrom 𝓓.M.start u)]

theorem EDT0LGrammar.DFAData.generated_words' {T : Type u_1} {Q : Type u_2} [Fintype T] [Fintype Q] (𝓓 : DFAData T Q) (w : List T) : 𝓓.grammar.Generates (List.map Symbol.terminal w ++ [Symbol.nonterminal (𝓓.M.evalFrom 𝓓.M.start w)])

theorem EDT0LGrammar.DFAData.languages_are_identical {T : Type u_1} {Q : Type u_2} [Fintype T] [Fintype Q] (𝓓 : DFAData T Q) (w : List T) : 𝓓.grammar.Generates (List.map Symbol.terminal w) ↔ 𝓓.M.evalFrom 𝓓.M.start w ∈ 𝓓.M.accept

theorem EDT0LGrammar.regular_languages_are_edt0l {T : Type u_1} [Fintype T] (L : Language T) : L.IsRegular → L.IsEDT0L