Translation of Nondeterministic Automata into Nondeterministic Automata with ε-transitions

An NA is an εNA whose ε-transitions are self-loops.

def Cslib.Automata.NA.toEpsilonNA {State : Type u_1} {Symbol : Type u_2} (a : NA State Symbol) : εNA State Symbol

NA is a special case of εNA, through LTS.mapHom and Language.Hom.reduceOption: the transitions on some x are the runs of the NA on [x], and the ε-transitions are self-loops.

Equations

• a.toEpsilonNA = { toLTS := a.mapHom Language.Hom.reduceOption, start := a.start }

def Cslib.Automata.NA.FinAcc.toEpsilonNAFinAcc {State : Type u_1} {Symbol : Type u_2} (a : FinAcc State Symbol) : εNA.FinAcc State Symbol

NA.FinAcc is a special case of εNA.FinAcc.

Equations

• a.toEpsilonNAFinAcc = { toεNA := a.toEpsilonNA, accept := a.accept }

@[simp]

theorem Cslib.Automata.NA.FinAcc.toEpsilonNAFinAcc_language_eq {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} : Acceptor.language a.toEpsilonNAFinAcc = Acceptor.language a

The εNA.FinAcc constructed from an NA.FinAcc has the same language.