theorem LO.Modal.Kripke.mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass {F : LO.Kripke.FiniteFrame} (hF : F ∈ LO.Kripke.TransitiveIrreflexiveFrameClassꟳ) : LO.Kripke.FiniteFrame.mk (F.toFrame^=) ∈ LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClassꟳ

theorem LO.Modal.Kripke.mem_irreflClosure_GLFiniteFrameClass_of_mem_GrzFiniteFrameClass {F : LO.Kripke.FiniteFrame} (hF : F ∈ LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClassꟳ) : LO.Kripke.FiniteFrame.mk (F.toFrame^≠) ∈ LO.Kripke.TransitiveIrreflexiveFrameClassꟳ

theorem LO.Modal.Kripke.iff_boxdot_reflexive_closure {α : Type u_2} {p : LO.Modal.Formula α} {F : LO.Kripke.Frame} {V : LO.Kripke.Valuation F α} {x : { Frame := F, Valuation := V }.World} : LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x (pᵇ) ↔ LO.Modal.Formula.Kripke.Satisfies { Frame := F^=, Valuation := V } x p

theorem LO.Modal.Kripke.iff_frame_boxdot_reflexive_closure {α : Type u_2} {p : LO.Modal.Formula α} {F : LO.Kripke.Frame} : F#α ⊧ pᵇ ↔ (F^=)#α ⊧ p

theorem LO.Modal.Kripke.iff_reflexivize_irreflexivize {α : Type u_2} {p : LO.Modal.Formula α} {F : LO.Kripke.Frame} (F_Refl : Reflexive F.Rel) {x : F.World} {V : LO.Kripke.Valuation F α} : LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p ↔ LO.Modal.Formula.Kripke.Satisfies { Frame := F^≠^=, Valuation := V } x p

theorem LO.Modal.boxdotTranslatedGL_of_Grz {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} : 𝐆𝐫𝐳 ⊢! p → 𝐆𝐋 ⊢! pᵇ

theorem LO.Modal.Grz_of_boxdotTranslatedGL {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} : 𝐆𝐋 ⊢! pᵇ → 𝐆𝐫𝐳 ⊢! p

theorem LO.Modal.iff_Grz_boxdotTranslatedGL {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} : 𝐆𝐫𝐳 ⊢! p ↔ 𝐆𝐋 ⊢! pᵇ

instance LO.Modal.instBoxdotPropertyGrzGL {α : Type u} [Inhabited α] [DecidableEq α] : LO.Modal.BoxdotProperty 𝐆𝐫𝐳 𝐆𝐋

Equations

• LO.Modal.instBoxdotPropertyGrzGL = { bdp := ⋯ }