Documentation

LSystems.FiniteIndexEDT0L.Defs

def EDT0LGrammar.SymbolIsNonterminal {T : Type u_4} {N : Type u_5} :

Symbol T N → Bool

Equations

Instances For

theorem EDT0LGrammar.SymbolIsNonterminal_nonterminal {T : Type u_1} {N : Type u_2} (n : N) :

SymbolIsNonterminal (Symbol.nonterminal n) = true

theorem EDT0LGrammar.SymbolIsNonterminal_terminal {T : Type u_1} {N : Type u_2} (t : T) :

SymbolIsNonterminal (Symbol.terminal t) = false

theorem EDT0LGrammar.SymbolIsNonterminal_single_nonterminal {T : Type u_1} {N : Type u_2} (n : N) :

List.countP SymbolIsNonterminal [Symbol.nonterminal n] = 1

def EDT0LGrammar.IsIndex {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype N] [Fintype H] (E : EDT0LGrammar T N H) (k : ℕ) :

Equations

E.IsIndex k = ∀ (w : List (Symbol T N)), E.Generates w → List.countP EDT0LGrammar.SymbolIsNonterminal w ≤ k

Instances For

theorem EDT0LGrammar.generates_implies_le_index {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype N] [Fintype H] (E : EDT0LGrammar T N H) {k : ℕ} (w : List (Symbol T N)) (h : E.IsIndex k) :

E.Generates w → List.countP SymbolIsNonterminal w ≤ k

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

Equations

E.IsFiniteIndex = ∃ (k : ℕ), E.IsIndex k

Instances For

theorem EDT0LGrammar.index_at_least_one {T : Type u_1} {N : Type u_2} {H : Type u_3} [Fintype N] [Fintype H] (E : EDT0LGrammar T N H) {k : ℕ} (h : E.IsIndex k) :

k ≥ 1

def Language.IsEDT0LOfIndex {α : Type u_1} (L : Language α) (k : ℕ) :

Equations

L.IsEDT0LOfIndex k = ∃ (n : ℕ) (m : ℕ) (E : EDT0LGrammar α (Fin n) (Fin m)) (_ : E.IsIndex k), E.language = L

Instances For

def Language.IsFiniteIndexEDT0L {α : Type u_1} (L : Language α) :

Equations

L.IsFiniteIndexEDT0L = ∃ (k : ℕ), L.IsEDT0LOfIndex k

Instances For

theorem edt0l_of_index_implies_finite_index {α : Type u_1} (L : Language α) (k : ℕ) :

L.IsEDT0LOfIndex k → L.IsFiniteIndexEDT0L

theorem EDT0LGrammar.EquivData.equiv_symbol_preserves_nonterminal {T : Type u_4} {N : Type u_5} {H : Type u_6} {N' : Type u_7} {H' : Type u_8} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) (a : Symbol T N') :

SymbolIsNonterminal a = SymbolIsNonterminal (𝓖.equiv_symbol.symm a)

theorem EDT0LGrammar.EquivData.equiv_preserves_fi {T : Type u_4} {N : Type u_5} {H : Type u_6} {N' : Type u_7} {H' : Type u_8} [Fintype N] [Fintype H] [Fintype N'] [Fintype H'] (𝓖 : EquivData) {k : ℕ} (h : 𝓖.E.IsIndex k) :

𝓖.grammar.IsIndex k

theorem EDT0LGrammar.fi_edt0l_grammars_generate_fi_edt0l_languages' {T : Type u_4} {N : Type u_5} {H : Type u_6} [Fintype N] [Fintype H] {k : ℕ} (E : EDT0LGrammar T N H) (h : E.IsIndex k) :

E.language.IsEDT0LOfIndex k

theorem EDT0LGrammar.fi_edt0l_grammars_generate_fi_edt0l_languages {T : Type u_4} {N : Type u_5} {H : Type u_6} [Fintype N] [Fintype H] (E : EDT0LGrammar T N H) (h : E.IsFiniteIndex) :

E.language.IsFiniteIndexEDT0L