Translation of εNA into NA

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

Any εNA.FinAcc can be converted into an NA.FinAcc that does not use ε-transitions.

Equations

• a.toNAFinAcc = { toLTS := a.saturate.mapLabel some, start := a.εClosure a.start, accept := a.accept }

theorem Cslib.Automata.εNA.FinAcc.toNAFinAcc_language_eq {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} : Acceptor.language a.toNAFinAcc = Acceptor.language a

Correctness of toNAFinAcc.