Elementary indexed languages

This file provides small indexed-grammar witnesses used by structural reductions.

def IndexedGrammar.emptyGrammar (T : Type) : IndexedGrammar T

The indexed grammar with one nonterminal, one flag symbol, and no rules.

Equations

• IndexedGrammar.emptyGrammar T = { nt := PUnit.{1}, flag := PUnit.{1}, initial := PUnit.unit, rules := [] }

instance IndexedGrammar.emptyGrammar_nt_decidableEq (T : Type) : DecidableEq (emptyGrammar T).nt

Equations

• IndexedGrammar.emptyGrammar_nt_decidableEq T = id inferInstance

instance IndexedGrammar.emptyGrammar_nt_fintype (T : Type) : Fintype (emptyGrammar T).nt

Equations

• IndexedGrammar.emptyGrammar_nt_fintype T = id inferInstance

instance IndexedGrammar.emptyGrammar_flag_fintype (T : Type) : Fintype (emptyGrammar T).flag

Equations

• IndexedGrammar.emptyGrammar_flag_fintype T = id inferInstance

theorem IndexedGrammar.emptyGrammar_noEpsilon (T : Type) : (emptyGrammar T).NoEpsilon'

theorem IndexedGrammar.emptyGrammar_isNormalForm (T : Type) : (emptyGrammar T).IsNormalForm

theorem IndexedGrammar.emptyGrammar_language (T : Type) : (emptyGrammar T).Language = 0

The no-rule indexed grammar generates the empty language.

theorem is_Indexed_empty {T : Type} : is_Indexed 0

The empty language is indexed.

theorem is_Indexed_noEpsilon_empty {T : Type} : is_Indexed_noEpsilon 0

The empty language has an ε-free indexed-grammar witness.