Translation of εNA into NA

theorem Cslib.LTS.noε_saturate_mTr {State : Type u_1} {Label : Type u_2} {s : State} {μs : List Label} {lts : LTS State (Option Label)} : lts.saturate.MTr s (List.map some μs) = (Cslib.LTS.noε✝ lts.saturate).MTr s μs

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 := Cslib.LTS.noε✝ a.saturate, start := a.εClosure a.start, accept := a.accept }

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

Correctness of toNAFinAcc.