Product of automata.

def Cslib.Automata.DA.prod {State1 : Type u_1} {State2 : Type u_2} {Symbol : Type u_3} (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) : DA (State1 × State2) Symbol

The product of two deterministic automata. TODO: This operation could be generalised to FLTS and lifted here.

Equations

• da1.prod da2 = { tr := fun (x : State1 × State2) (x_1 : Symbol) => match x with | (s1, s2) => (da1.tr s1 x_1, da2.tr s2 x_1), start := (da1.start, da2.start) }

@[simp]

theorem Cslib.Automata.DA.prod_mtr_eq {State1 : Type u_1} {State2 : Type u_2} {Symbol : Type u_3} (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) (s : State1 × State2) (xs : List Symbol) : (da1.prod da2).mtr s xs = (da1.mtr s.1 xs, da2.mtr s.2 xs)

A state is reachable by the product automaton iff its components are reachable by the respective component automata.