Sum of nondeterministic automata.

def Cslib.Automata.NA.iSum {Symbol : Type u_1} {I : Type u_2} {State : I → Type u_3} (na : (i : I) → NA (State i) Symbol) : NA ((i : I) × State i) Symbol

The sum of an indexed family of nondeterministic automata.

Equations

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

@[simp]

theorem Cslib.Automata.NA.iSum_run_iff {Symbol : Type u_1} {I : Type u_2} {State : I → Type u_3} {na : (i : I) → NA (State i) Symbol} {xs : ωSequence Symbol} {ss : ωSequence ((i : I) × State i)} : (iSum na).Run xs ss ↔ ∃ (i : I) (ss_i : ωSequence (State i)), (na i).Run xs ss_i ∧ ωSequence.map (Sigma.mk i) ss_i = ss

An infinite run of the sum automaton is an infinite run of one of its component automata.

@[simp]

theorem Cslib.Automata.NA.Buchi.iSum_language_eq {Symbol : Type u_1} {I : Type u_2} {State : I → Type u_3} {na : (i : I) → NA (State i) Symbol} {acc : (i : I) → Set (State i)} : ωAcceptor.language { toNA := iSum na, accept := ⋃ (i : I), Sigma.mk i '' acc i } = ⨆ (i : I), ωAcceptor.language { toNA := na i, accept := acc i }

The ω-language accepted by the Buchi sum automata is the union of the ω-languages accepted by its component automata.