EDT0L Grammars

An EDT0L grammar consists of the following data:

• a finite alphabet of terminal letters T;
• a finite alphabet of nonterminal letters N;
• an initial nonterminal letter; and
• a finite number of maps of the form N → List (Symbol T N) which we refer to as tables. Notice that Symbol T N is a type, provided by Mathlib, which corresponds to a disjoint union of the types T and N.

To simplify proofs in this project, we index the tables of the grammar using a finite type H.

Applying tables

Suppose we are given some word w : List (Symbol T N), then we may apply a table of the form τ : N → List (Symbol T N) by replacing each nonterminal in w with the corresponding word given by τ, and leaving all the terminal letters along.

Let E be an EDT0L grammar. Then, a word w : List T is then accepted by the grammar if the word w.map Symbol.terminal can be reached from the initial word [Symbol.nonterminal E.intial] by applying a finite sequence of tables. The set of all such words is known as an EDT0L language.

structure EDT0LGrammar (T : Type u_1) (N : Type u_2) (H : Type u_3) [Fintype N] [Fintype H] : Type (max (max u_1 u_2) u_3)

EDT0L grammar with terminals T, nonterminals N, and tables H.

• initial : N

  Initial nonterminal of the grammar

• tables : H → N → List (Symbol T N)

  The finite set of tables, as indexed by H.

theorem EDT0LGrammar.ext_iff {T : Type u_1} {N : Type u_2} {H : Type u_3} {inst✝ : Fintype N} {inst✝¹ : Fintype H} {x y : EDT0LGrammar T N H} : x = y ↔ x.initial = y.initial ∧ x.tables = y.tables

theorem EDT0LGrammar.ext {T : Type u_1} {N : Type u_2} {H : Type u_3} {inst✝ : Fintype N} {inst✝¹ : Fintype H} {x y : EDT0LGrammar T N H} (initial : x.initial = y.initial) (tables : x.tables = y.tables) : x = y

def EDT0LGrammar.RewriteSymbol {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (τ : H) : Symbol T N → List (Symbol T N)

Rewrites a symbol with respect to a given table.

Equations

• E.RewriteSymbol τ (Symbol.terminal t) = [Symbol.terminal t]
• E.RewriteSymbol τ (Symbol.nonterminal n) = E.tables τ n

def EDT0LGrammar.RewriteWord {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (τ : H) (w : List (Symbol T N)) : List (Symbol T N)

Applies a given table to the given word.

Equations

• E.RewriteWord τ w = List.flatMap (E.RewriteSymbol τ) w

def EDT0LGrammar.Rewrites {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (source target : List (Symbol T N)) : Prop

A relation which holds if there exists a table which rewrites the word source to the word target.

Equations

• E.Rewrites source target = ∃ (τ : H), E.RewriteWord τ source = target

def EDT0LGrammar.Derives {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : List (Symbol T N) → List (Symbol T N) → Prop

The reflexive transitive closure of EDT0LGrammar.Rewrites.

Equations

• E.Derives = Relation.ReflTransGen E.Rewrites

def EDT0LGrammar.Generates {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (w : List (Symbol T N)) : Prop

The given word can be derived from the inital word.

Equations

• E.Generates w = E.Derives [Symbol.nonterminal E.initial] w

def EDT0LGrammar.language {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : Language T

The language produced by the EDT0L grammar

Equations

• E.language = {w : List T | E.Generates (List.map Symbol.terminal w)}

def Language.IsEDT0L {T : Type u_1} (L : Language T) : Prop

The language is EDT0L.

Notice that this definition requries that the language is generated by an EDT0L language where the set of nonterminals and terminals are of the form Fin n and Fin m, respectively, for some n m : ℕ. Our main goal in this file is to show that we can assume without loss of generality that any given EDT0L grammar is of this form. We prove this fact in the theorem edt0l_grammars_generate_edt0l_languages, at the end of this file.

Equations

• L.IsEDT0L = ∃ (n : ℕ) (m : ℕ) (E : EDT0LGrammar T (Fin n) (Fin m)), E.language = L

@[simp]

theorem EDT0LGrammar.RewriteSymbol.terminal {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (τ : H) (a : T) : E.RewriteSymbol τ (Symbol.terminal a) = [Symbol.terminal a]

@[simp]

theorem EDT0LGrammar.RewriteSymbol.nonterminal {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (τ : H) (n : N) : E.RewriteSymbol τ (Symbol.nonterminal n) = E.tables τ n

@[simp]

theorem EDT0LGrammar.RewriteWord.nil {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (τ : H) : E.RewriteWord τ [] = []

@[simp]

theorem EDT0LGrammar.RewriteWord.cons {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (τ : H) {a : Symbol T N} {as : List (Symbol T N)} : E.RewriteWord τ (a :: as) = E.RewriteSymbol τ a ++ E.RewriteWord τ as

@[simp]

theorem EDT0LGrammar.RewriteWord.append {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (τ : H) {a b : List (Symbol T N)} : E.RewriteWord τ (a ++ b) = E.RewriteWord τ a ++ E.RewriteWord τ b

@[simp]

theorem EDT0LGrammar.RewriteWord.single {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (τ : H) {a : Symbol T N} : E.RewriteWord τ [a] = E.RewriteSymbol τ a

@[simp]

theorem EDT0LGrammar.RewriteWord.terminal_word {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) (τ : H) {w : List T} : E.RewriteWord τ (List.map Symbol.terminal w) = List.map Symbol.terminal w

theorem EDT0LGrammar.Rewrites.nil {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) {w : List (Symbol T N)} : E.Rewrites [] w → w = []

theorem EDT0LGrammar.Rewrites.terminal_word {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) {w : List T} {w' : List (Symbol T N)} (h : E.Rewrites (List.map Symbol.terminal w) w') : w' = List.map Symbol.terminal w

theorem EDT0LGrammar.Derives.trans {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] {a b c : List (Symbol T N)} {E : EDT0LGrammar T N H} (h₁ : E.Derives a b) (h₂ : E.Derives b c) : E.Derives a c

theorem EDT0LGrammar.Derives.single {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] {a b : List (Symbol T N)} {E : EDT0LGrammar T N H} (h : E.Rewrites a b) : E.Derives a b

theorem EDT0LGrammar.Derives.head {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] {a b c : List (Symbol T N)} {E : EDT0LGrammar T N H} (h₁ : E.Rewrites a b) (h₂ : E.Derives b c) : E.Derives a c

theorem EDT0LGrammar.Derives.tail {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] {a b c : List (Symbol T N)} {E : EDT0LGrammar T N H} (h₁ : E.Derives a b) (h₂ : E.Rewrites b c) : E.Derives a c

theorem EDT0LGrammar.Derives.refl {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] {a : List (Symbol T N)} {E : EDT0LGrammar T N H} : E.Derives a a

instance EDT0LGrammar.Derives.instTransListSymbol {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : Trans E.Derives E.Derives E.Derives

Equations

• EDT0LGrammar.Derives.instTransListSymbol E = { trans := ⋯ }

instance EDT0LGrammar.Derives.instTransListSymbolRewrites {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : Trans E.Derives E.Rewrites E.Derives

Equations

• EDT0LGrammar.Derives.instTransListSymbolRewrites E = { trans := ⋯ }

instance EDT0LGrammar.Derives.instTransListSymbolRewrites_1 {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : Trans E.Rewrites E.Derives E.Derives

Equations

• EDT0LGrammar.Derives.instTransListSymbolRewrites_1 E = { trans := ⋯ }

instance EDT0LGrammar.Derives.instTransListSymbolRewrites_2 {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : Trans E.Rewrites E.Rewrites E.Derives

Equations

• EDT0LGrammar.Derives.instTransListSymbolRewrites_2 E = { trans := ⋯ }

instance EDT0LGrammar.Derives.instIsTransListSymbol {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : IsTrans (List (Symbol T N)) E.Derives

instance EDT0LGrammar.Derives.instIsReflListSymbol {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : IsRefl (List (Symbol T N)) E.Derives

instance EDT0LGrammar.Derives.instIsPreorderListSymbol {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : IsPreorder (List (Symbol T N)) E.Derives

theorem EDT0LGrammar.Derives.nil {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) {w : List (Symbol T N)} : E.Derives [] w → w = []

theorem EDT0LGrammar.Derives.terminal_word {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) {w : List T} {w' : List (Symbol T N)} (h : E.Rewrites (List.map Symbol.terminal w) w') : w' = List.map Symbol.terminal w

theorem EDT0LGrammar.generates_initial {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype H] [Fintype N] (E : EDT0LGrammar T N H) : E.Generates [Symbol.nonterminal E.initial]

structure EDT0LGrammar.EquivData {T : Type u_1} {N : Type u_2} {H : Type u_3} {N' : Type u_4} {H' : Type u_5} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] : Type (max (max (max (max u_1 u_2) u_3) u_4) u_5)

Defines an equivalent EDT0L grammar.

This structure holds the data needed to construct an EDT0L grammar which can be used in the proof of edt0l_grammars_generate_edt0l_languages. We provide this construction as its own structure as this construction is to be reused when defining EDT0L grammars with finite index

• E : EDT0LGrammar T N H

  The grammar for which we want to find an equivalent grammar.

• equivN : N ≃ N'

  An equivalence relation between nonterminals.

• equivH : H ≃ H'

  An equivalence relation between tables.

def EDT0LGrammar.EquivData.equiv_symbol {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : Symbol T N ≃ Symbol T N'

An equivalence relation between symbols of terminals and nonterminals.

This equivalence relation is constructed from the equivalence relation between nonterminals, as stored in the EquivData structure.

Equations

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

def EDT0LGrammar.EquivData.equiv_word {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : List (Symbol T N) ≃ List (Symbol T N')

An equivalence relation between words.

This equivalence relation is constructed from the equivalence relation between nonterminals, as stored in the EquivData structure.

Equations

• 𝓖.equiv_word = { toFun := List.map ⇑𝓖.equiv_symbol, invFun := List.map ⇑𝓖.equiv_symbol.symm, left_inv := ⋯, right_inv := ⋯ }

def EDT0LGrammar.EquivData.grammar {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : EDT0LGrammar T N' H'

Constructs an EDT0L grammar equivalent to the one store in EquivData.

Equations

• 𝓖.grammar = { initial := 𝓖.equivN 𝓖.E.initial, tables := fun (h : H') (n : N') => 𝓖.equiv_word (𝓖.E.tables (𝓖.equivH.symm h) (𝓖.equivN.symm n)) }

theorem EDT0LGrammar.EquivData.equiv_symbol_terminal {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (a : T) : 𝓖.equiv_symbol (Symbol.terminal a) = Symbol.terminal a

theorem EDT0LGrammar.EquivData.equiv_symbol_nonterminal {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (n : N) : 𝓖.equiv_symbol (Symbol.nonterminal n) = Symbol.nonterminal (𝓖.equivN n)

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_nil {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : 𝓖.equiv_word [] = []

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_singleton {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (a : Symbol T N) : 𝓖.equiv_word [a] = [𝓖.equiv_symbol a]

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_cons {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) {a : Symbol T N} {as : List (Symbol T N)} : 𝓖.equiv_word (a :: as) = 𝓖.equiv_symbol a :: 𝓖.equiv_word as

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_append {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) {a b : List (Symbol T N)} : 𝓖.equiv_word (a ++ b) = 𝓖.equiv_word a ++ 𝓖.equiv_word b

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_terminal {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (w : List T) : 𝓖.equiv_word (List.map Symbol.terminal w) = List.map Symbol.terminal w

def EDT0LGrammar.EquivData.symm {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : EquivData

Equations

• 𝓖.symm = { E := 𝓖.grammar, equivN := 𝓖.equivN.symm, equivH := 𝓖.equivH.symm }

@[simp]

theorem EDT0LGrammar.EquivData.symm_equiv_symbol {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : 𝓖.symm.equiv_symbol = 𝓖.equiv_symbol.symm

@[simp]

theorem EDT0LGrammar.EquivData.symm_equiv_word {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : 𝓖.symm.equiv_word = 𝓖.equiv_word.symm

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_nil' {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : 𝓖.equiv_word.symm [] = []

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_singleton' {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (a : Symbol T N') : 𝓖.equiv_word.symm [a] = [𝓖.equiv_symbol.symm a]

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_cons' {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) {a : Symbol T N'} {as : List (Symbol T N')} : 𝓖.equiv_word.symm (a :: as) = 𝓖.equiv_symbol.symm a :: 𝓖.equiv_word.symm as

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_append' {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) {a b : List (Symbol T N')} : 𝓖.equiv_word.symm (a ++ b) = 𝓖.equiv_word.symm a ++ 𝓖.equiv_word.symm b

@[simp]

theorem EDT0LGrammar.EquivData.equiv_word_terminal' {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (w : List T) : 𝓖.equiv_word.symm (List.map Symbol.terminal w) = List.map Symbol.terminal w

@[simp]

theorem EDT0LGrammar.EquivData.symm_grammar {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : 𝓖.symm.grammar = 𝓖.E

@[simp]

theorem EDT0LGrammar.EquivData.grammar_rewrite_symbol_iff {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (τ : H') (s : Symbol T N') : 𝓖.grammar.RewriteSymbol τ s = 𝓖.equiv_word (𝓖.E.RewriteSymbol (𝓖.equivH.symm τ) (𝓖.equiv_symbol.symm s))

theorem EDT0LGrammar.EquivData.grammar_rewrite_word_iff {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (τ : H') (w : List (Symbol T N')) : 𝓖.grammar.RewriteWord τ w = 𝓖.equiv_word (𝓖.E.RewriteWord (𝓖.equivH.symm τ) (𝓖.equiv_word.symm w))

theorem EDT0LGrammar.EquivData.grammar_rewrites_iff {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (u v : List (Symbol T N')) : 𝓖.grammar.Rewrites u v ↔ 𝓖.E.Rewrites (𝓖.equiv_word.symm u) (𝓖.equiv_word.symm v)

theorem EDT0LGrammar.EquivData.grammar_derives_iff_mp {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (u v : List (Symbol T N')) : 𝓖.grammar.Derives u v → 𝓖.E.Derives (𝓖.equiv_word.symm u) (𝓖.equiv_word.symm v)

theorem EDT0LGrammar.EquivData.grammar_derives_iff_mpr {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (u v : List (Symbol T N')) : 𝓖.E.Derives (𝓖.equiv_word.symm u) (𝓖.equiv_word.symm v) → 𝓖.grammar.Derives u v

theorem EDT0LGrammar.EquivData.grammar_derives_iff {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (u v : List (Symbol T N')) : 𝓖.grammar.Derives u v ↔ 𝓖.E.Derives (𝓖.equiv_word.symm u) (𝓖.equiv_word.symm v)

theorem EDT0LGrammar.EquivData.grammar_derives_iff' {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (u v : List (Symbol T N)) : 𝓖.E.Derives u v ↔ 𝓖.grammar.Derives (𝓖.equiv_word u) (𝓖.equiv_word v)

theorem EDT0LGrammar.EquivData.grammar_generates_iff {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (w : List (Symbol T N)) : 𝓖.E.Generates w ↔ 𝓖.grammar.Generates (𝓖.equiv_word w)

theorem EDT0LGrammar.EquivData.grammar_language_iff {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (w : List T) : 𝓖.E.Generates (List.map Symbol.terminal w) ↔ 𝓖.grammar.Generates (List.map Symbol.terminal w)

theorem EDT0LGrammar.EquivData.equiv_has_same_language {T : Type u_1} {N : Type u_3} {H : Type u_4} {N' : Type u_5} {H' : Type u_6} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) : 𝓖.E.language = 𝓖.grammar.language

theorem EDT0LGrammar.fin_nonterminals_and_tables {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype N] [Fintype H] (E : EDT0LGrammar T N H) : ∃ (E' : EDT0LGrammar T (Fin (Fintype.card N)) (Fin (Fintype.card H))), E'.language = E.language

theorem EDT0LGrammar.edt0l_grammars_generate_edt0l_languages {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype N] [Fintype H] (E : EDT0LGrammar T N H) : E.language.IsEDT0L