Translation of εNA into NA

def Cslib.LTS.noε {State : Type u_1} {Label : Type u_2} (lts : LTS State (Option Label)) : LTS State Label

Converts an LTS with Option labels into an LTS on the carried label type, by removing all ε-transitions.

Equations

• lts.noε = { Tr := fun (s : State) (μ : Label) (s' : State) => lts.Tr s (some μ) s' }

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) = lts.saturate.noε.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 := a.saturate.noε, 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.