Indexed Languages

This file defines the class of indexed languages via indexed grammars.

Main declarations

• is_Indexed
• Indexed

def is_Indexed {T : Type} (L : Language T) : Prop

Predicate that a language is an indexed language.

Equations

• is_Indexed L = ∃ (g : IndexedGrammar T), g.Language = L

def Indexed {T : Type} : Set (Language T)

The class of indexed languages.

Equations

• Indexed = setOf is_Indexed

def is_Indexed_noEpsilon {T : Type} (L : Language T) : Prop

Predicate that a language has an indexed-grammar witness with no ε-productions.

Equations

• is_Indexed_noEpsilon L = ∃ (g : IndexedGrammar T), g.NoEpsilon' ∧ g.Language = L

def IndexedNoEpsilon {T : Type} : Set (Language T)

The class of indexed languages with an ε-free indexed-grammar witness.

Equations

• IndexedNoEpsilon = setOf is_Indexed_noEpsilon

theorem is_Indexed_of_is_Indexed_noEpsilon {T : Type} {L : Language T} (h : is_Indexed_noEpsilon L) : is_Indexed L

theorem not_nil_mem_of_is_Indexed_noEpsilon {T : Type} {L : Language T} (h : is_Indexed_noEpsilon L) : [] ∉ L

An ε-free indexed language does not contain the empty word.

theorem diff_empty_of_is_Indexed_noEpsilon {T : Type} {L : Language T} (h : is_Indexed_noEpsilon L) : L \ {[]} = L

Removing ε from an ε-free indexed language leaves the same language.

theorem IndexedNoEpsilon_subclass_Indexed {T : Type} : IndexedNoEpsilon ⊆ Indexed