Translation of Deterministic Automata into Nonodeterministic Automata.

This is the general version of the standard translation of DFAs into NFAs.

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

DA is a special case of NA.

Equations

• a.toNA = { toLTS := a.toLTS, start := {a.start} }

@[instance_reducible]

instance Cslib.Automata.DA.instCoeNA {State : Type u_1} {Symbol : Type u_2} : Coe (DA State Symbol) (NA State Symbol)

Equations

• Cslib.Automata.DA.instCoeNA = { coe := Cslib.Automata.DA.toNA }

@[simp]

theorem Cslib.Automata.DA.toNA_run {State : Type u_1} {Symbol : Type u_2} {a : DA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} : a.toNA.Run xs ss ↔ a.run xs = ss

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

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

Equations

• a.toNAFinAcc = { toNA := a.toNA, accept := a.accept }

@[simp]

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

The NA.FinAcc constructed from a DA.FinAcc has the same language.

def Cslib.Automata.DA.Buchi.toNABuchi {State : Type u_1} {Symbol : Type u_2} (a : Buchi State Symbol) : NA.Buchi State Symbol

DA.Buchi is a special case of NA.Buchi.

Equations

• a.toNABuchi = { toNA := a.toNA, accept := a.accept }

@[simp]

theorem Cslib.Automata.DA.Buchi.toNABuchi_language_eq {State : Type u_1} {Symbol : Type u_2} {a : Buchi State Symbol} : ωAcceptor.language a.toNABuchi = ωAcceptor.language a

The NA.Buchi constructed from a DA.Buchi has the same ω-language.