Modal Frames and LTS

def Cslib.LTS.toFrame {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : Frame State (PFunctor.mkUnary Label)

Transforms lts into a corresponding unary Frame.

Equations

• lts.toFrame = Cslib.Frame.ofRelations fun (μ : (PFunctor.mkUnary Label).A) (s s' : State) => lts.Tr s μ s'

@[instance_reducible]

instance Cslib.LTS.instCoeFrameMkUnary {State : Type u_1} {Label : Type u_2} : Coe (LTS State Label) (Frame State (PFunctor.mkUnary Label))

Equations

• Cslib.LTS.instCoeFrameMkUnary = { coe := Cslib.LTS.toFrame }

@[simp]

theorem Cslib.LTS.toFrame_r_iff_tr {State : Type u_2} {Label : Type u_1} (lts : LTS State Label) {μ : (PFunctor.mkUnary Label).A} {s : State} {f : (PFunctor.mkUnary Label).B μ → State} : lts.toFrame.r μ s f ↔ lts.Tr s μ (f default)

@[simp]

theorem Cslib.LTS.toFrame_diagonal_iff_tr {State : Type u_2} {Label : Type u_1} (lts : LTS State Label) {μ : (PFunctor.mkUnary Label).A} {s s' : State} : lts.toFrame.diagonal μ s s' ↔ lts.Tr s μ s'