Label homomorphism map for LTS.

def Cslib.LTS.mapHom {State : Type u_1} {Label₁ : Type u_2} {Label₂ : Type u_3} (lts : LTS State Label₁) (f : Language.Hom Label₂ Label₁) : LTS State Label₂

Given a language homomorphism f from Label₂ to Label₁ and an LTS lts that uses Label₁, lts.mapHom f is an LTS with the same state space but uses Label₂, whose step on a single label μ is the composition of the steps taken by lts on the sequence of labels f [μ]. Note that f [μ] can be empty or consists of many labels.

Equations

• lts.mapHom f = { Tr := fun (s : State) (μ : Label₂) (s' : State) => lts.MTr s (f [μ]) s' }

@[simp]

theorem Cslib.LTS.mapHom_tr {State : Type u_1} {Label₁ : Type u_2} {Label₂ : Type u_3} {s s' : State} {f : Language.Hom Label₂ Label₁} {lts : LTS State Label₁} {μ : Label₂} : (lts.mapHom f).Tr s μ s' ↔ lts.MTr s (f [μ]) s'

@[simp]

theorem Cslib.LTS.mapHom_mTr {State : Type u_1} {Label₁ : Type u_2} {Label₂ : Type u_3} {s s' : State} {f : Language.Hom Label₂ Label₁} {lts : LTS State Label₁} {μs : List Label₂} : (lts.mapHom f).MTr s μs s' ↔ lts.MTr s (f μs) s'

This theorem says basically that lts.mapHom f is well-defined because f is a language homomorphism.

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₂

This is the special case of LTS.mapHom when the language homomorphism maps single labels to single labels.

Equations

• lts.mapLabel f = lts.mapHom (Language.Hom.lift fun (x : Label₂) => [f x])

@[simp]

theorem Cslib.LTS.mapLabel_tr {State : Type u_1} {Label₁ : Type u_2} {Label✝ : Type u_4} {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'