Loop construction on nondeterministic automata.

def Cslib.Automata.NA.FinAcc.loop {Symbol : Type u_1} {State : Type u_2} (na : FinAcc State Symbol) : NA (Unit ⊕ State) Symbol

na.loop mimics na, but can nondeterministically decide to "loop back" by identifing an accepting state of na with a starting state of na. This identification is achieved via a new dummy state (), which is the sole starting state and the sole accepting state of na.loop.

Equations

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

theorem Cslib.Automata.NA.loop_run_left_left {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)} (h : na.loop.Run xs ss) (h1 : (ss 1).isLeft = true) : [xs 0] ∈ Acceptor.language na

theorem Cslib.Automata.NA.loop_run_left_right {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)} (h : na.loop.Run xs ss) (n : ℕ) (h1 : 0 < n) (h2 : ∀ (k : ℕ), 0 < k → k ≤ n → (ss k).isRight = true) : ∃ (s : State) (t : State), na.MTr s (ωSequence.take n xs) t ∧ s ∈ na.start ∧ ss n = Sum.inr t

theorem Cslib.Automata.NA.loop_run_left_right_left {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)} (h : na.loop.Run xs ss) (n : ℕ) (h1 : 0 < n ∧ (ss n).isLeft = true) (h2 : ∀ (k : ℕ), 0 < k → k < n → (ss k).isRight = true) : ωSequence.take n xs ∈ Acceptor.language na

theorem Cslib.Automata.NA.loop_run_from_left {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)} (h : na.loop.Run xs ss) (n : ℕ) (h1 : (ss n).isLeft = true) : na.loop.Run (ωSequence.drop n xs) (ωSequence.drop n ss)

theorem Cslib.Automata.NA.loop_run_one_iter {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ State)} {k : ℕ} (h : na.loop.Run xs ss) (h1 : 0 < k) (h2 : (ss k).isLeft = true) : ∃ n ≤ k, ωSequence.take n xs ∈ Acceptor.language na - 1 ∧ na.loop.Run (ωSequence.drop n xs) (ωSequence.drop n ss)

A run of na.loop containing at least one non-initial () state is the concatenation of a nonempty finite run of na followed by a run of na.loop.

theorem Cslib.Automata.NA.loop_fin_run_exists {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} {xl : List Symbol} (h : xl ∈ Acceptor.language na) : ∃ (sl : List (Unit ⊕ State)) (x : sl.length = xl.length + 1), sl[0] = Sum.inl () ∧ sl[xl.length] = Sum.inl () ∧ ∀ (k : ℕ) (x_1 : k < xl.length), na.loop.Tr sl[k] xl[k] sl[k + 1]

For any finite word in language na, there is a corresponding finite run of na.loop.

theorem Cslib.Automata.NA.loop_fin_run_mtr {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} {xl : List Symbol} (h : xl ∈ Acceptor.language na) : na.loop.MTr (Sum.inl ()) xl (Sum.inl ())

For any finite word in language na, there is a corresponding multistep transition of na.loop.

theorem Cslib.Automata.NA.loop_run_exists {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} [Inhabited Symbol] {xls : ωSequence (List Symbol)} (h : ∀ (k : ℕ), xls k ∈ Acceptor.language na - 1) : ∃ (ss : ωSequence (Unit ⊕ State)), na.loop.Run xls.flatten ss ∧ ∀ (k : ℕ), ss (xls.cumLen k) = Sum.inl ()

For any infinite sequence xls of nonempty finite words from language na, there is an infinite run of na.loop corresponding to xls.flatten in which the state () marks the boundaries between the finite words in xls.

@[simp]

theorem Cslib.Automata.NA.Buchi.loop_language_eq {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} [Inhabited Symbol] : ωAcceptor.language { toNA := na.loop, accept := {Sum.inl ()} } = (Acceptor.language na)^ω

The Buchi ω-language accepted by na.loop is the ω-power of the language accepted by na.

def Cslib.Automata.NA.FinAcc.finLoop {Symbol : Type u_1} {State : Type u_2} (na : FinAcc State Symbol) : NA (Unit ⊕ State ⊕ Unit) Symbol

finLoop na is the loop construction applied to the "totalized" version of na.

Equations

• na.finLoop = { toNA := na.totalize, accept := Sum.inl '' na.accept }.loop

instance Cslib.Automata.NA.FinAcc.instTotalSumUnitFinLoopOfNonemptyElemStart {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} [h : Nonempty ↑na.start] : na.finLoop.Total

finLoop na is total, assuming that na has at least one start state.

theorem Cslib.Automata.NA.FinAcc.loop_language_eq {Symbol : Type u_1} {State : Type u_2} {na : FinAcc State Symbol} [Inhabited Symbol] (h : ¬Acceptor.language na = 0) : Acceptor.language { toNA := na.finLoop, accept := {Sum.inl ()} } = KStar.kstar (Acceptor.language na)

finLoop na accepts the Kleene star of the language of na, assuming that the latter is nonempty.