Translation of Nondeterministic Automata for finite strings into Deterministic Automata

This file implements the standard subset construction.

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

Converts an NA into a DA using the subset construction.

Equations

• a.toDA = { toFLTS := a.toFLTS, start := a.start }

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

Converts an NA.FinAcc into a DA.FinAcc using the subset construction.

Equations

• a.toDAFinAcc = { toDA := a.toDA, accept := {S : Set State | ∃ s ∈ S, s ∈ a.accept} }

theorem Cslib.Automata.NA.FinAcc.toDAFinAcc_language_eq {State : Type u_1} {Symbol : Type u_2} {na : FinAcc State Symbol} : Acceptor.language na.toDAFinAcc = Acceptor.language na

The DA constructed from an NA has the same language.