Documentation

Cslib.Computability.Automata.EpsilonNA.ToSingleStartAccept

Translation of εNA into εNA with a single start and a single accept state #

Defines the transformation toSingleStartAccept for εNA.FinAcc, which adds a start state with ε-transitions to the original start states and no incoming transitions, and an accept state with ε-transitions from the original accept states and no outgoing transitions. The transformation preserves the language of the automaton.

source
def Cslib.Automata.εNA.FinAcc.toSingleStartAccept {State : Type u_1} {Symbol : Type u_2} (a : FinAcc State Symbol) :
FinAcc (Bool ⊕ State) Symbol

Any εNA.FinAcc can be converted into an εNA.FinAcc with a single start state and a single accept state. The original states are wrapped in inr, and the fresh state inl b is accepting exactly when b: the start state inl false has ε-transitions to the original start states, and the original accept states have ε-transitions to the accept state inl true.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_start {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} :
    a.toSingleStartAccept.start = {Sum.inl false}
    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_accept {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} :
    a.toSingleStartAccept.accept = {Sum.inl true}
    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_tr_inr_inr {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} {s s' : State} {μ : Option Symbol} :
    a.toSingleStartAccept.Tr (Sum.inr s) μ (Sum.inr s') ↔ a.Tr s μ s'
    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_tr_start {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} {s : State} (hs : s ∈ a.start) :
    a.toSingleStartAccept.Tr (Sum.inl false) none (Sum.inr s)
    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_tr_accept {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} {s : State} (hs : s ∈ a.accept) :
    a.toSingleStartAccept.Tr (Sum.inr s) none (Sum.inl true)
    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_tr_inl_false {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} {μ : Option Symbol} {y : Bool ⊕ State} (h : a.toSingleStartAccept.Tr (Sum.inl false) μ y) :
    μ = none ∧ ∃ (s : State), y = Sum.inr s ∧ s ∈ a.start

    The transitions from the start state are ε-transitions to the original start states.

    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_not_tr_inl_false {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} {x : Bool ⊕ State} {μ : Option Symbol} :
    ¬a.toSingleStartAccept.Tr x μ (Sum.inl false)

    No transition leads to the start state.

    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_not_tr_inl_true {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} {μ : Option Symbol} {y : Bool ⊕ State} :
    ¬a.toSingleStartAccept.Tr (Sum.inl true) μ y

    No transition leaves the accept state.

    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_mTr_inr_inl_true {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} {s : State} {μs : List (Option Symbol)} (h : a.toSingleStartAccept.MTr (Sum.inr s) μs (Sum.inl true)) :
    ∃ t ∈ a.accept, ∃ (μs' : List (Option Symbol)), μs = μs' ++ [none] ∧ a.MTr s μs' t

    A run from an original state to the accept state is a run of the original automaton to an original accept state, followed by the ε-transition to the accept state.

    source
    theorem Cslib.Automata.εNA.FinAcc.toSingleStartAccept_language_eq {State : Type u_1} {Symbol : Type u_2} {a : FinAcc State Symbol} :
    Acceptor.language a.toSingleStartAccept = Acceptor.language a

    toSingleStartAccept preserves the language of the input automaton.