Concatenation of nondeterministic automata.

def Cslib.Automata.NA.concat {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} (na1 : FinAcc State1 Symbol) (na2 : NA State2 Symbol) : NA (State1 ⊕ State2) Symbol

concat na1 na2 starts by running na1 and then nondeterministically switches to na2 by identifying an accepting state of na1 with an initial state of na2. If na1 accepts the empty word, it may also start running na2 from the beginning. Once it starts running na2, it cannot go back to na1.

Equations

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

theorem Cslib.Automata.NA.concat_start_right {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} {na1 : FinAcc State1 Symbol} {na2 : NA State2 Symbol} {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} (hc : (concat na1 na2).Run xs ss) (hr : (ss 0).isRight = true) : [] ∈ Acceptor.language na1

theorem Cslib.Automata.NA.concat_run_left {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} {na1 : FinAcc State1 Symbol} {na2 : NA State2 Symbol} {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} (hc : (concat na1 na2).Run xs ss) (n : ℕ) (hl : ∀ k ≤ n, (ss k).isLeft = true) : ∃ (s1 : State1) (t1 : State1), na1.MTr s1 (ωSequence.take n xs) t1 ∧ s1 ∈ na1.start ∧ ss 0 = Sum.inl s1 ∧ ss n = Sum.inl t1

theorem Cslib.Automata.NA.concat_run_left_right {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} {na1 : FinAcc State1 Symbol} {na2 : NA State2 Symbol} {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} (hc : (concat na1 na2).Run xs ss) (n : ℕ) (hn : 0 < n) (hl : ∀ k < n, (ss k).isLeft = true) (hr : (ss n).isRight = true) : ωSequence.take n xs ∈ Acceptor.language na1

theorem Cslib.Automata.NA.concat_run_right {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} {na1 : FinAcc State1 Symbol} {na2 : NA State2 Symbol} {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} (hc : (concat na1 na2).Run xs ss) (n : ℕ) (hl : ∀ k < n, (ss k).isLeft = true) (hr : (ss n).isRight = true) : ∃ (ss2 : ωSequence State2), na2.Run (ωSequence.drop n xs) ss2 ∧ ωSequence.drop n ss = ωSequence.map Sum.inr ss2

theorem Cslib.Automata.NA.concat_run_proj {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} {na1 : FinAcc State1 Symbol} {na2 : NA State2 Symbol} {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} {k : ℕ} (hc : (concat na1 na2).Run xs ss) (hr : (ss k).isRight = true) : ∃ n ≤ k, ωSequence.take n xs ∈ Acceptor.language na1 ∧ ∃ (ss2 : ωSequence State2), na2.Run (ωSequence.drop n xs) ss2 ∧ ωSequence.drop n ss = ωSequence.map Sum.inr ss2

A run of concat na1 na2 containing at least one na2 state is the concatenation of an accepting finite run of na1 followed by a run of na2.

theorem Cslib.Automata.NA.concat_run_exists {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} {na1 : FinAcc State1 Symbol} {na2 : NA State2 Symbol} {xs1 : List Symbol} {xs2 : ωSequence Symbol} {ss2 : ωSequence State2} (h1 : xs1 ∈ Acceptor.language na1) (h2 : na2.Run xs2 ss2) : ∃ (ss : ωSequence (State1 ⊕ State2)), (concat na1 na2).Run (xs1 ++ω xs2) ss ∧ ωSequence.drop xs1.length ss = ωSequence.map Sum.inr ss2

Given an accepting finite run of na1 and a run of na2, there exists a run of concat na1 na2 that is the concatenation of the two runs.

@[simp]

theorem Cslib.Automata.NA.Buchi.concat_language_eq {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} {na1 : FinAcc State1 Symbol} {na2 : NA State2 Symbol} {acc2 : Set State2} : ωAcceptor.language { toNA := concat na1 na2, accept := Sum.inr '' acc2 } = Acceptor.language na1 * ωAcceptor.language { toNA := na2, accept := acc2 }

The Buchi automaton formed from concat na1 na2 accepts the ω-language that is the concatenation of the language of na1 and the ω-language of na2.

def Cslib.Automata.NA.FinAcc.finConcat {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} (na1 : FinAcc State1 Symbol) (na2 : FinAcc State2 Symbol) : NA ((State1 ⊕ Unit) ⊕ State2 ⊕ Unit) Symbol

finConcat na1 na2 is the concatenation of the "totalized" versions of na1 and na2.

Equations

• na1.finConcat na2 = Cslib.Automata.NA.concat { toNA := na1.totalize, accept := Sum.inl '' na1.accept } na2.totalize

instance Cslib.Automata.NA.FinAcc.instTotalSumUnitFinConcat {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} {na1 : FinAcc State1 Symbol} {na2 : FinAcc State2 Symbol} : (na1.finConcat na2).Total

finConcat na1 na2 is total.

theorem Cslib.Automata.NA.FinAcc.finConcat_language_eq {Symbol : Type u_1} {State1 : Type u_2} {State2 : Type u_3} {na1 : FinAcc State1 Symbol} {na2 : FinAcc State2 Symbol} [Inhabited Symbol] : Acceptor.language { toNA := na1.finConcat na2, accept := Sum.inr '' (Sum.inl '' na2.accept) } = Acceptor.language na1 * Acceptor.language na2

finConcat na1 na2 accepts the concatenation of the languages of na1 and na2.