Product of nondeterministic automata.

def Cslib.Automata.NA.iProd {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 product 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.iProd_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)} : (iProd na).Run xs ss ↔ ∀ (i : I), (na i).Run xs (ωSequence.map (fun (x : (i : I) → State i) => x i) ss)

Every run of the product automaton projects onto runs of its component automata, and vice versa.