Label map operation for LTS.

def Cslib.LTS.mapLabel {State : Type u_1} {Label₁ : Type u_2} {Label₂ : Type u_3} (lts : LTS State Label₁) (f : Label₂ → Label₁) : LTS State Label₂

Constructs an LTS by mapping its labels into those of an existing LTS.

Equations

• lts.mapLabel f = { Tr := fun (s : State) (μ : Label₂) (s' : State) => lts.Tr s (f μ) s' }

@[simp]

theorem Cslib.LTS.mapLabel_tr {State : Type u_1} {Label₁ : Type u_2} {Label✝ : Type u_3} {f : Label✝ → Label₁} {s : State} {μ : Label✝} {s' : State} {lts : LTS State Label₁} : (lts.mapLabel f).Tr s μ s' ↔ lts.Tr s (f μ) s'

@[simp]

theorem Cslib.LTS.mapLabel_mTr {State : Type u_1} {Label₁ : Type u_2} {Label₂ : Type u_3} {s : State} {μs : List Label₂} {s' : State} {lts : LTS State Label₁} {f : Label₂ → Label₁} : (lts.mapLabel f).MTr s μs s' ↔ lts.MTr s (List.map f μs) s'