Indexed Languages Under Injective Terminal Maps

This file proves that indexed languages are preserved by injective terminal maps.

def IndexedGrammar.mapIRhsSymbol {T₁ T₂ : Type} (f : T₁ → T₂) {N F : Type} : IRhsSymbol T₁ N F → IRhsSymbol T₂ N F

Equations

• IndexedGrammar.mapIRhsSymbol f (IRhsSymbol.terminal t) = IRhsSymbol.terminal (f t)
• IndexedGrammar.mapIRhsSymbol f (IRhsSymbol.nonterminal n push) = IRhsSymbol.nonterminal n push

def IndexedGrammar.mapTerminals {T₁ T₂ : Type} (f : T₁ → T₂) (g : IndexedGrammar T₁) : IndexedGrammar T₂

Equations

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

def IndexedGrammar.mapISym {T₁ T₂ : Type} (f : T₁ → T₂) (g : IndexedGrammar T₁) : g.ISym → (mapTerminals f g).ISym

Equations

• IndexedGrammar.mapISym f g (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal (f t)
• IndexedGrammar.mapISym f g (IndexedGrammar.ISym.indexed n σ) = IndexedGrammar.ISym.indexed n σ

theorem IndexedGrammar.language_mapTerminals {T₁ T₂ : Type} [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) (g : IndexedGrammar T₁) : (mapTerminals f g).Language = (Language.map f) g.Language

theorem Indexed_of_map_injective_Indexed {T₁ T₂ : Type} [Nonempty T₁] {f : T₁ → T₂} (hf : Function.Injective f) (L : Language T₁) : is_Indexed L → is_Indexed ((Language.map f) L)