noncomputable def LO.System.lem₁_boxdot_Grz_of_L {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ : F} : 𝓢 ⊢ ⊡(⊡(φ ➝ ⊡φ) ➝ φ) ➝ □(φ ➝ ⊡φ) ➝ φ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LO.System.boxdot_Grz_of_L {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ : F} : 𝓢 ⊢ ⊡(⊡(φ ➝ ⊡φ) ➝ φ) ➝ φ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.System.boxdot_Grz_of_L! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.GL 𝓢] {φ : F} : 𝓢 ⊢! ⊡(⊡(φ ➝ ⊡φ) ➝ φ) ➝ φ

theorem LO.Modal.Kripke.mem_reflClosure_GrzFiniteFrameClass_of_mem_GLFiniteFrameClass {F : FiniteFrame} (hF : F ∈ TransitiveIrreflexiveFiniteFrameClass) : FiniteFrame.mk (F.toFrame^=) ∈ ReflexiveTransitiveAntiSymmetricFiniteFrameClass

theorem LO.Modal.Kripke.mem_irreflClosure_GLFiniteFrameClass_of_mem_GrzFiniteFrameClass {F : FiniteFrame} (hF : F ∈ ReflexiveTransitiveAntiSymmetricFiniteFrameClass) : FiniteFrame.mk (F.toFrame^≠) ∈ TransitiveIrreflexiveFiniteFrameClass

theorem LO.Modal.Kripke.iff_boxdot_reflexive_closure {φ : Formula ℕ} {F : Frame} {V : Valuation F} {x : { toFrame := F, Val := V }.World} : Formula.Kripke.Satisfies { toFrame := F, Val := V } x (φᵇ) ↔ Formula.Kripke.Satisfies { toFrame := F^=, Val := V } x φ

theorem LO.Modal.Kripke.iff_frame_boxdot_reflexive_closure {φ : Formula ℕ} {F : Frame} : F ⊧ φᵇ ↔ F^= ⊧ φ

theorem LO.Modal.Kripke.iff_reflexivize_irreflexivize {φ : Formula ℕ} {F : Frame} (F_Refl : Reflexive F.Rel) {x : F.World} {V : Valuation F} : Formula.Kripke.Satisfies { toFrame := F, Val := V } x φ ↔ Formula.Kripke.Satisfies { toFrame := F^≠^=, Val := V } x φ

theorem LO.Modal.Hilbert.boxdotTranslatedGL_of_Grz {φ : Formula ℕ} : Hilbert.Grz ℕ ⊢! φ → Hilbert.GL ℕ ⊢! φᵇ

theorem LO.Modal.Hilbert.Grz_of_boxdotTranslatedGL {φ : Formula ℕ} : Hilbert.GL ℕ ⊢! φᵇ → Hilbert.Grz ℕ ⊢! φ

theorem LO.Modal.Hilbert.iff_Grz_boxdotTranslatedGL {φ : Formula ℕ} : Hilbert.GL ℕ ⊢! φᵇ ↔ Hilbert.Grz ℕ ⊢! φ

instance LO.Modal.Hilbert.instBoxdotPropertyNatGLGrz : BoxdotProperty (Hilbert.GL ℕ) (Hilbert.Grz ℕ)