Translation of εNA into εNA with a single accept state

Defines the transformation toSingleAccept for εNA.FinAcc and proves correctness results in terms of language equivalence and correspondences between the two transition systems.

Note for future work: we could formulate a stronger transformation, whereby also the set of accept states becomes a singleton.

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

Any εNA.FinAcc can be converted into an εNA.FinAcc with a single accept state none. The original states are wrapped in some, and all original accept states have ε-transitions to none.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_accept_def {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} : a.toSingleAccept.accept = {none}

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_accepts_mTr_iff {State : Type u_1} {Symbol : Type u_2} {xs : List Symbol} {a : FinAcc State Symbol} : Acceptor.Accepts a.toSingleAccept xs ↔ ∃ s ∈ a.toSingleAccept.start, a.toSingleAccept.SMTr s (List.map some xs) none

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_tr_antiDerivative_isSome {State : Type u_1} {Symbol : Type u_2} {os : Option State} {x : Option Symbol} {os' : Option State} {a : FinAcc State Symbol} (h : a.toSingleAccept.Tr os x os') : os.isSome = true

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_tr_tr {State : Type u_1} {Symbol : Type u_2} {s : State} {x : Option Symbol} {s' : State} {a : FinAcc State Symbol} : a.toSingleAccept.Tr (some s) x (some s') ↔ a.Tr s x s'

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_tr_none_accept {State : Type u_1} {Symbol : Type u_2} {os : Option State} {x : Option Symbol} {a : FinAcc State Symbol} (h : a.toSingleAccept.Tr os x none) : ∃ (s : State), os = some s ∧ s ∈ a.accept

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_not_tr_none {State : Type u_1} {Symbol : Type u_2} {x : Option Symbol} {os : Option State} {a : FinAcc State Symbol} : ¬a.toSingleAccept.Tr none x os

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_mTr_antiDerivative_isSome {State : Type u_1} {Symbol : Type u_2} {os : Option State} {x : List (Option Symbol)} {s' : State} {a : FinAcc State Symbol} (h : a.toSingleAccept.MTr os x (some s')) : os.isSome = true

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_mTr_mTr {State : Type u_1} {Symbol : Type u_2} {s : State} {xs : List (Option Symbol)} {s' : State} {a : FinAcc State Symbol} : a.toSingleAccept.MTr (some s) xs (some s') ↔ a.MTr s xs s'

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_τSTr_antiDerivative_none {State : Type u_1} {Symbol : Type u_2} {os : Option State} {a : FinAcc State Symbol} (h : a.toSingleAccept.τSTr none os) : os = none

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_τSTr_antiDerivative_isSome {State : Type u_1} {Symbol : Type u_2} {os : Option State} {s' : State} {a : FinAcc State Symbol} (h : a.toSingleAccept.τSTr os (some s')) : os.isSome = true

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_τSTr_τSTr {State : Type u_1} {Symbol : Type u_2} {s s' : State} {a : FinAcc State Symbol} : a.toSingleAccept.τSTr (some s) (some s') ↔ a.τSTr s s'

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_τSTr_none_accept {State : Type u_1} {Symbol : Type u_2} {s : State} {a : FinAcc State Symbol} (h : a.toSingleAccept.τSTr (some s) none) : ∃ s' ∈ a.accept, a.τSTr s s'

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_sTr_antiDerivative_isSome {State : Type u_1} {Symbol : Type u_2} {os : Option State} {x : Option Symbol} {s' : State} {a : FinAcc State Symbol} (h : a.toSingleAccept.STr os x (some s')) : os.isSome = true

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_sTr_sTr {State : Type u_1} {Symbol : Type u_2} {s : State} {x : Option Symbol} {s' : State} {a : FinAcc State Symbol} : a.toSingleAccept.STr (some s) x (some s') ↔ a.STr s x s'

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_sTr_none_accept {State : Type u_1} {Symbol : Type u_2} {s : State} {x : Option Symbol} {a : FinAcc State Symbol} (h : a.toSingleAccept.STr (some s) x none) : ∃ s' ∈ a.accept, a.STr s x s'

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_sTr_none_none {State : Type u_1} {Symbol : Type u_2} {x : Option Symbol} {os : Option State} {a : FinAcc State Symbol} (h : a.toSingleAccept.STr none x os) : x = none ∧ os = none

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_sMTr_antiDerivative_isSome {State : Type u_1} {Symbol : Type u_2} {os : Option State} {xs : List (Option Symbol)} {s' : State} {a : FinAcc State Symbol} (h : a.toSingleAccept.SMTr os xs (some s')) : os.isSome = true

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_sMTr_sMTr {State : Type u_1} {Symbol : Type u_2} {s : State} {x : List (Option Symbol)} {s' : State} {a : FinAcc State Symbol} : a.toSingleAccept.SMTr (some s) x (some s') ↔ a.SMTr s x s'

theorem Cslib.Automata.εNA.FinAcc.toSingleAccept_sMTr_none_accept {State : Type u_1} {Symbol : Type u_2} {s : State} {xs : List Symbol} {a : FinAcc State Symbol} (h : a.toSingleAccept.SMTr (some s) (List.map some xs) none) : ∃ s' ∈ a.accept, a.SMTr s (List.map some xs) s'

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

toSingleAccept preserves the language of the input automaton.