structure EDT0LGrammar.UnionData {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)

• E₀ : EDT0LGrammar T N₀ H₀
• E₁ : EDT0LGrammar T N₁ H₁

def EDT0LGrammar.UnionData.extend_alphabet₀ {T : Type u_1} {N₀ : Type u_2} {N₁ : Type u_4} : Symbol T N₀ → Symbol T ((N₀ ⊕ N₁) ⊕ Unit)

Equations

• EDT0LGrammar.UnionData.extend_alphabet₀ (Symbol.terminal t) = Symbol.terminal t
• EDT0LGrammar.UnionData.extend_alphabet₀ (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inl (Sum.inl n))

def EDT0LGrammar.UnionData.extend_alphabet₁ {T : Type u_1} {N₀ : Type u_2} {N₁ : Type u_4} : Symbol T N₁ → Symbol T ((N₀ ⊕ N₁) ⊕ Unit)

Equations

• EDT0LGrammar.UnionData.extend_alphabet₁ (Symbol.terminal t) = Symbol.terminal t
• EDT0LGrammar.UnionData.extend_alphabet₁ (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inl (Sum.inr n))

@[simp]

theorem EDT0LGrammar.UnionData.extend_alphabet₀_terminal {T : Type u_6} {N₀ : Type u_7} {N₁ : Type u_8} (t : T) : extend_alphabet₀ (Symbol.terminal t) = Symbol.terminal t

@[simp]

theorem EDT0LGrammar.UnionData.extend_alphabet₁_terminal {T : Type u_6} {N₀ : Type u_7} {N₁ : Type u_8} (t : T) : extend_alphabet₁ (Symbol.terminal t) = Symbol.terminal t

@[simp]

theorem EDT0LGrammar.UnionData.extend_alphabet₀_nonterminal {T : Type u_6} {N₀ : Type u_7} {N₁ : Type u_8} (n : N₀) : extend_alphabet₀ (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inl (Sum.inl n))

@[simp]

theorem EDT0LGrammar.UnionData.extend_alphabet₁_nonterminal {T : Type u_6} {N₀ : Type u_7} {N₁ : Type u_8} (n : N₁) : extend_alphabet₁ (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inl (Sum.inr n))

@[simp]

theorem EDT0LGrammar.UnionData.extend_alphabet₀_terminal_word {T : Type u_6} {N₀ : Type u_7} {N₁ : Type u_8} (w : List T) : List.map extend_alphabet₀ (List.map Symbol.terminal w) = List.map Symbol.terminal w

@[simp]

theorem EDT0LGrammar.UnionData.extend_alphabet₁_terminal_word {T : Type u_6} {N₀ : Type u_7} {N₁ : Type u_8} (w : List T) : List.map extend_alphabet₁ (List.map Symbol.terminal w) = List.map Symbol.terminal w

def EDT0LGrammar.UnionData.grammar {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₁] (𝓖 : UnionData) : EDT0LGrammar T ((N₀ ⊕ N₁) ⊕ Unit) ((H₀ ⊕ H₁) ⊕ Fin 2)

Equations

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

theorem EDT0LGrammar.UnionData.left_rewrites {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₁] (𝓖 : UnionData) (w w' : List (Symbol T ((N₀ ⊕ N₁) ⊕ Unit))) (h : ∃ (u : List (Symbol T N₀)), w = List.map extend_alphabet₀ u ∧ 𝓖.E₀.Generates u) : 𝓖.grammar.Rewrites w w' → ∃ (u' : List (Symbol T N₀)), w' = List.map extend_alphabet₀ u' ∧ 𝓖.E₀.Generates u'

theorem EDT0LGrammar.UnionData.right_rewrites {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₁] (𝓖 : UnionData) (w w' : List (Symbol T ((N₀ ⊕ N₁) ⊕ Unit))) (h : ∃ (u : List (Symbol T N₁)), w = List.map extend_alphabet₁ u ∧ 𝓖.E₁.Generates u) : 𝓖.grammar.Rewrites w w' → ∃ (u' : List (Symbol T N₁)), w' = List.map extend_alphabet₁ u' ∧ 𝓖.E₁.Generates u'

theorem EDT0LGrammar.UnionData.basic_property {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₁] (𝓖 : UnionData) (w : List (Symbol T ((N₀ ⊕ N₁) ⊕ Unit))) (h : 𝓖.grammar.Generates w) : w = [Symbol.nonterminal 𝓖.grammar.initial] ∨ (∃ (u : List (Symbol T N₀)), w = List.map extend_alphabet₀ u ∧ 𝓖.E₀.Generates u) ∨ ∃ (u : List (Symbol T N₁)), w = List.map extend_alphabet₁ u ∧ 𝓖.E₁.Generates u

theorem EDT0LGrammar.UnionData.basic_property₀ {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₁] (𝓖 : UnionData) (w : List (Symbol T N₀)) (h : 𝓖.E₀.Generates w) : 𝓖.grammar.Generates (List.map extend_alphabet₀ w)

theorem EDT0LGrammar.UnionData.basic_property₁ {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₁] (𝓖 : UnionData) (w : List (Symbol T N₁)) (h : 𝓖.E₁.Generates w) : 𝓖.grammar.Generates (List.map extend_alphabet₁ w)

theorem EDT0LGrammar.UnionData.defines_union {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₁] (𝓖 : UnionData) : 𝓖.grammar.language = 𝓖.E₀.language + 𝓖.E₁.language

theorem EDT0LGrammar.closed_under_union {T : Type u_1} (L₁ L₂ : Language T) (h₁ : L₁.IsEDT0L) (h₂ : L₂.IsEDT0L) : (L₁ + L₂).IsEDT0L