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

Equations

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

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

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

Equations

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

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

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

Equations

• LO.System.imply_box_box_of_imply_boxdot_axiomT h = LO.System.impTrans'' LO.System.imply_Box_BoxBoxdot (LO.System.impTrans'' (LO.System.implyBoxDistribute' h) LO.System.axiomL)

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

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

theorem LO.Modal.Hilbert.GL.imply_boxdot_plain_of_imply_box_box {φ ψ : LO.Modal.Formula ℕ} : LO.Modal.Hilbert.GL ℕ ⊢! □φ ➝ □ψ → LO.Modal.Hilbert.GL ℕ ⊢! ⊡φ ➝ ψ

theorem LO.Modal.Hilbert.GL.unnecessitation! {φ : LO.Modal.Formula ℕ} : LO.Modal.Hilbert.GL ℕ ⊢! □φ → LO.Modal.Hilbert.GL ℕ ⊢! φ

noncomputable instance LO.Modal.Hilbert.GL.instUnnecessitationNatFormula : LO.System.Unnecessitation (LO.Modal.Hilbert.GL ℕ)

Equations

• LO.Modal.Hilbert.GL.instUnnecessitationNatFormula = { unnec := fun {φ : LO.Modal.Formula ℕ} (h : LO.Modal.Hilbert.GL ℕ ⊢ □φ) => Nonempty.some ⋯ }