Product of functional labelled transition systems

def Cslib.FLTS.prod {Label : Type u_2} {State1 : Type u_3} {State2 : Type u_4} (flts1 : FLTS State1 Label) (flts2 : FLTS State2 Label) : FLTS (State1 × State2) Label

The product of two FLTS with the same label type.

Equations

• flts1.prod flts2 = { tr := fun (x : State1 × State2) (μ : Label) => match x with | (s1, s2) => (flts1.tr s1 μ, flts2.tr s2 μ) }

@[simp]

theorem Cslib.FLTS.prod_mtr_eq {Label : Type u_2} {State1 : Type u_3} {State2 : Type u_4} (flts1 : FLTS State1 Label) (flts2 : FLTS State2 Label) (s : State1 × State2) (μs : List Label) : (flts1.prod flts2).mtr s μs = (flts1.mtr s.fst μs, flts2.mtr s.snd μs)

A state is reachable by the product FLTS iff its components are reachable by the respective FLTS components.