Product of deterministic 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.

Equations

• da1.prod da2 = { toFLTS := da1.prod da2.toFLTS, 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 automaton components.