restructureHEADmain

4 files changed, 0 insertions, 528 deletions

diff --git a/SymbolicModalLogic/AlternationDepth.lean b/SymbolicModalLogic/AlternationDepth.lean
deleted file mode 100644
index 717c928..0000000
--- a/SymbolicModalLogic/AlternationDepth.lean
+++ /dev/null
@@ -1,165 +0,0 @@
-import SymbolicModalLogic.MuCalculus
-import Mathlib
-
-inductive FixedPointOp where
-  | μ
-  | ν
-  deriving DecidableEq
-
-variable {Λ : Type} [Modalities Λ]
-open Formula
-
-inductive IsAlternationDepthBound : FixedPointOp → ℕ → Formula Λ → Prop where
-  | top {η : FixedPointOp} : IsAlternationDepthBound η 0 .top
-  | bot {η : FixedPointOp} : IsAlternationDepthBound η 0 .bot
-  | var {η : FixedPointOp} (x : ℕ) : IsAlternationDepthBound η 0 (.var x)
-  | or {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} :
-      IsAlternationDepthBound η n φ →
-      IsAlternationDepthBound η n ψ →
-      IsAlternationDepthBound η n (.or φ ψ)
-  | and {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} :
-      IsAlternationDepthBound η n φ →
-      IsAlternationDepthBound η n ψ →
-      IsAlternationDepthBound η n (.and φ ψ)
-  | modality {η : FixedPointOp} {n : ℕ} {l : Λ} {args : Modalities.signature l → Formula Λ} :
-      (∀ l, IsAlternationDepthBound η n (args l)) →
-      IsAlternationDepthBound η n (.modality l args)
-  | lfp {n : ℕ} {φ : Formula Λ} :
-      IsAlternationDepthBound .ν n φ →
-      IsAlternationDepthBound .ν n (μ, φ)
-  | gfp {n : ℕ} {φ : Formula Λ} :
-      IsAlternationDepthBound .μ n φ →
-      IsAlternationDepthBound .μ n (ν, φ)
-  | subst {η : FixedPointOp} {n : ℕ} {φ ψ : Formula Λ} {x : ℕ} :
-      IsAlternationDepthBound η n φ →
-      IsAlternationDepthBound η n ψ →
-      IsAlternationDepthBound η n (φ.subst (x, ψ))
-  | up {η₁ η₂ : FixedPointOp} {n : ℕ} {φ : Formula Λ} :
-      IsAlternationDepthBound η₁ n φ →
-      IsAlternationDepthBound η₂ (n + 1) φ
-
-noncomputable def alternationDepth (φ : Formula Λ) : ℕ :=
-  sInf { n : ℕ | IsAlternationDepthBound .μ n φ ∧ IsAlternationDepthBound .ν n φ }
-
-def Formula.closure : Formula Λ → List (ℕ × Formula Λ)
-  | .top => [(0, ⊤)]
-  | .bot => [(0, ⊥)]
-  | .or φ ψ => [(0, φ ∨ ψ)] ++ closure φ ++ closure ψ
-  | .and φ ψ => [(0, φ ∧ ψ)] ++ closure φ ++ closure ψ
-  | .modality l args =>
-      [(0, .modality l args)] ++ (Modalities.args l |>.flatMap fun a ↦ closure (args a))
-  | .var x => [(0, ^x)]
-  | .lfp φ => [(0, μ, φ)] ++ (closure φ).map (fun ⟨n, ψ⟩ ↦ (n + 1, ψ))
-  | .gfp φ => [(0, ν, φ)] ++ (closure φ).map (fun ⟨n, ψ⟩ ↦ (n + 1, ψ))
-
-def mentionsVar (n : ℕ) : Formula Λ → Bool
-  | .top => false
-  | .bot => false
-  | .or φ ψ => mentionsVar n φ || mentionsVar n ψ
-  | .and φ ψ => mentionsVar n φ || mentionsVar n ψ
-  | .modality l args =>
-      Modalities.args l |>.any fun a ↦ mentionsVar n (args a)
-  | .var x => x == n
-  | .lfp φ => mentionsVar (n + 1) φ
-  | .gfp φ => mentionsVar (n + 1) φ
-
-def size : Formula Λ → ℕ
-  | .top => 1
-  | .bot => 1
-  | .or φ ψ => 1 + size φ + size ψ
-  | .and φ ψ => 1 + size φ + size ψ
-  | .modality l args =>
-      1 + (Modalities.args l |>.map (fun a ↦ size (args a)) |>.sum)
-  | .var _ => 1
-  | .lfp φ => 1 + size φ
-  | .gfp φ => 1 + size φ
-
-lemma closure_mem_size (φ : Formula Λ) : ∀ {n ψ}, (n, ψ) ∈ φ.closure → size ψ ≤ size φ := by
-  intro n χ
-  induction φ generalizing n χ with
-  | top => grind [Formula.closure]
-  | bot => grind [Formula.closure]
-  | or φ ψ hφ hψ =>
-      intro h
-      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_append] at h
-      cases h with
-      | inl eq => rw [eq.right]
-      | inr h => cases h <;> grind [size]
-  | and φ ψ hφ hψ =>
-      intro h
-      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_append] at h
-      cases h with
-      | inl eq => rw [eq.right]
-      | inr h => cases h <;> grind [size]
-  | modality l args hargs =>
-      intro h
-      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_flatMap] at h
-      cases h with
-      | inl eq => rw [eq.right]
-      | inr h =>
-          obtain ⟨a, _, ha⟩ := h
-          simp only [size]
-          grw [hargs _ ha]
-          apply Nat.le_add_left_of_le
-          apply List.le_sum_of_mem
-          apply List.mem_map_of_mem
-          apply Modalities.args_mem
-  | var x => grind [Formula.closure]
-  | lfp φ hφ =>
-      intro h
-      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_map, Prod.exists, exists_eq_right_right] at h
-      cases h with
-      | inl eq => rw [eq.right]
-      | inr h => obtain ⟨_, h, _⟩ := h; grind [size]
-  | gfp φ hφ =>
-      intro h
-      simp only [Formula.closure, List.cons_append, List.nil_append, List.mem_cons, Prod.mk.injEq, List.mem_map, Prod.exists, exists_eq_right_right] at h
-      cases h with
-      | inl eq => rw [eq.right]
-      | inr h => obtain ⟨_, h, _⟩ := h; grind [size]
-
-def ad : Formula Λ → ℕ
-  | .top => 0
-  | .bot => 0
-  | .or φ ψ => Nat.max (ad φ) (ad ψ)
-  | .and φ ψ => Nat.max (ad φ) (ad ψ)
-  | .modality l args =>
-      Modalities.args l
-        |>.map (fun a ↦ ad (args a))
-        |> List.foldr Nat.max 0
-  | .var _ => 0
-  | .lfp φ => Id.run do
-      let mut n := Nat.max 1 (ad φ)
-      for h : (offset, ψ) in closure φ do
-        if h' : mentionsVar offset ψ then
-          if let Formula.gfp χ := ψ then
-            n := Nat.max n (ad (ν, χ) + 1)
-      return n
-  | .gfp φ => Id.run do
-      let mut n := Nat.max 1 (ad φ)
-      for h : (offset, ψ) in closure φ do
-        if h' : mentionsVar offset ψ then
-          if let Formula.lfp χ := ψ then
-            n := Nat.max n (ad (μ, χ) + 1)
-      return n
-  termination_by φ => size φ
-  decreasing_by
-    · grind [size]
-    · grind [size]
-    · grind [size]
-    · grind [size]
-    · rw [size, Nat.lt_one_add_iff]
-      apply List.le_sum_of_mem
-      apply List.mem_map_of_mem
-      apply Modalities.args_mem
-    · grind [size]
-    · rw [show size (μ, φ) = 1 + size φ from rfl, Nat.lt_one_add_iff]
-      apply closure_mem_size
-      exact h
-    · grind [size]
-    · rw [show size (ν, φ) = 1 + size φ from rfl, Nat.lt_one_add_iff]
-      apply closure_mem_size
-      exact h
-
-lemma ad_eq_alternationDepth (φ : Formula Λ) : ad φ = alternationDepth φ := by
-  sorry
diff --git a/SymbolicModalLogic/FixedPoints.lean b/SymbolicModalLogic/FixedPoints.lean
deleted file mode 100644
index 58d768c..0000000
--- a/SymbolicModalLogic/FixedPoints.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-import Mathlib
-
-variable {α : Type} [CompleteLattice α]
-
-structure Function.IsLeastFixedPt (f : α → α) (x : α) : Prop where
-  fixedPt : Function.IsFixedPt f x
-  least : ∀ y, Function.IsFixedPt f y → x ≤ y
-
-structure Function.IsGreatestFixedPt (f : α → α) (x : α) : Prop where
-  fixedPt : Function.IsFixedPt f x
-  greatest : ∀ y, Function.IsFixedPt f y → y ≤ x
-
-namespace FixedPoints
-
-def lfp (f : α → α) : α := sInf { x | f x ≤ x }
-
-def gfp (f : α → α) : α := sSup { x | x ≤ f x }
-
-lemma lfp_isLeastFixedPt (f : α → α) (hf : Monotone f) : Function.IsLeastFixedPt f (lfp f) where
-  fixedPt := by
-    have hmem : f (lfp f) ≤ lfp f := by
-      rw [lfp, le_sInf_iff]
-      intro x hx
-      grw [hf (sInf_le hx)]
-      exact hx
-    apply Std.IsPartialOrder.le_antisymm
-    · exact hmem
-    · exact (sInf_le (hf hmem))
-  least := by
-    intro x hfix
-    apply sInf_le
-    simp [show f x = x from hfix]
-
--- TODO: Avoid repitition
-lemma gfp_isGreatestFixedPt (f : α → α) (hf : Monotone f) : Function.IsGreatestFixedPt f (gfp f) where
-  fixedPt := by
-    have hmem : gfp f ≤ f (gfp f) := by
-      rw [gfp, sSup_le_iff]
-      intro x hx
-      grw [show x ≤ f x from hx]
-      exact hf (le_sSup hx)
-    apply Std.IsPartialOrder.le_antisymm
-    · apply le_sSup
-      exact hf hmem
-    · exact hmem
-  greatest := by
-    intro x hfix
-    apply le_sSup
-    simp [show f x = x from hfix]
-
-end FixedPoints
diff --git a/SymbolicModalLogic/Instances/Relational.lean b/SymbolicModalLogic/Instances/Relational.lean
deleted file mode 100644
index 81d428d..0000000
--- a/SymbolicModalLogic/Instances/Relational.lean
+++ /dev/null
@@ -1,58 +0,0 @@
-import Mathlib
-import SymbolicModalLogic.MuCalculus
-
-inductive Relational where
-  | box
-  | diamond
-  deriving Repr
-
-namespace Relational
-
-instance : Modalities Relational where
-  signature _ := Unit
-  dual
-    | .box     => .diamond
-    | .diamond => .box
-  dualSignature
-    | .box,     f => f
-    | .diamond, f => f
-  dual_involution := by intro l; cases l <;> simp
-
-instance : Model Relational Set where
-  lifting
-    | .box,     A => { B | B ⊆ A () }
-    | .diamond, A => { B | B ∩ A () ≠ ∅ }
-
-@[simp]
-lemma lift_box_iff {X : Type} {A : Unit → Set X} {B : Set X} : B ∈ Model.lift Relational.box Set A ↔ ∀ x ∈ B, x ∈ A () := by
-  show B ∈ { B | B ⊆ A () } ↔ ∀ x ∈ B, x ∈ A ()
-  exact Set.mem_setOf
-
-@[simp]
-lemma lift_diamond_iff {X : Type} {A : Unit → Set X} {B : Set X} : B ∈ Model.lift Relational.diamond Set A ↔ ∃ x ∈ B, x ∈ A () := by
-  show B ∈ { B | B ∩ A () ≠ ∅ } ↔ ∃ x ∈ B, x ∈ A ()
-  rw [Set.mem_setOf_eq, ← Set.nonempty_iff_ne_empty]
-  rfl
-
-instance : LawfulModel Relational Set where
-  lifting_natural {X Y} f l := by
-    cases l
-    all_goals intro A; ext B; simp
-  lifting_monotone {X} l := by
-    cases l with
-    | box =>
-        intro A A' h B hB
-        rw [lift_box_iff]; intro x hx
-        rw [lift_box_iff] at hB
-        exact h () (hB x hx)
-    | diamond =>
-        intro A A' h B hB
-        rw [lift_diamond_iff] at hB
-        obtain ⟨x, hx⟩ := hB
-        rw [lift_diamond_iff]; use x
-        exact ⟨hx.left, h () hx.right⟩
-  lifting_dual {X} l := by
-    cases l
-    all_goals intro A; ext B; simp [Modalities.dual, Modalities.dualSignature]
-
-end Relational
diff --git a/SymbolicModalLogic/MuCalculus.lean b/SymbolicModalLogic/MuCalculus.lean
deleted file mode 100644
index 4722928..0000000
--- a/SymbolicModalLogic/MuCalculus.lean
+++ /dev/null
@@ -1,254 +0,0 @@
-import Mathlib
-import SymbolicModalLogic.FixedPoints
-
-class Modalities (Λ : Type) where
-  signature : Λ → Type
-  [signature_finenum : ∀ l, FinEnum (signature l)]
-  dual : Λ → Λ
-  dualSignature {α : Type} : (l : Λ) → (signature l → α) → (signature (dual l) → α)
-  dual_involution : ∀ l, dual (dual l) = l
-
-def Modalities.args {Λ : Type} [Modalities Λ] (l : Λ) : List (Modalities.signature l) :=
-  have : FinEnum (signature l) := Modalities.signature_finenum l
-  FinEnum.toList (signature l)
-
-def Modalities.args_mem {Λ : Type} [Modalities Λ] (l : Λ) (a : Modalities.signature l) : a ∈ args l := by
-  rw [args]
-  apply @FinEnum.mem_toList _ (Modalities.signature_finenum l)
-
-inductive Formula (Λ : Type) [Modalities Λ] where
-  | top : Formula Λ
-  | bot : Formula Λ
-  | or : Formula Λ → Formula Λ → Formula Λ
-  | and : Formula Λ → Formula Λ → Formula Λ
-  | modality : (l : Λ) → (args : Modalities.signature l → Formula Λ) → Formula Λ
-  | var : ℕ → Formula Λ
-  | lfp : Formula Λ → Formula Λ
-  | gfp : Formula Λ → Formula Λ
-
-namespace Formula
-
-scoped notation "⊤" => Formula.top
-scoped notation "⊥" => Formula.bot
-scoped infixl:30 " ∨ " => Formula.or
-scoped infixl:35 " ∧ " => Formula.and
-scoped notation "^" n:max => Formula.var n
-scoped notation "μ, " φ => Formula.lfp φ
-scoped notation "ν, " φ => Formula.gfp φ
-
-variable {Λ : Type} [Modalities Λ]
-
-instance [Repr Λ] : ToString (Formula Λ) where
-  toString :=
-    let rec impl : Formula Λ → String
-      | .top => "⊤"
-      | .bot => "⊥"
-      | .or φ ψ => s!"({impl φ}) ∨ ({impl ψ})"
-      | .and φ ψ => s!"({impl φ}) ∧ ({impl ψ})"
-      | .var x => s!"^{x}"
-      | .modality l args =>
-          have : FinEnum (Modalities.signature l) := Modalities.signature_finenum l
-          let argsStr := FinEnum.toList (Modalities.signature l)
-            |>.map (fun a ↦ impl (args a))
-            |> String.intercalate ", "
-          s!"{reprStr l}({argsStr})"
-      | .lfp φ => s!"μ, {impl φ}"
-      | .gfp φ => s!"ν, {impl φ}"
-    impl
-
-def not : Formula Λ → Formula Λ
-  | .top             => ⊥
-  | .bot             => ⊤
-  | .or φ ψ          => (not φ) ∧ (not ψ)
-  | .and φ ψ         => (not φ) ∨ (not ψ)
-  | .modality l args => .modality (Modalities.dual l) (Modalities.dualSignature l fun a ↦ not (args a))
-  | .var x           => ^x
-  | .lfp φ           => ν, not φ
-  | .gfp φ           => μ, not φ
-
-scoped notation "¬" φ:60 => Formula.not φ
-scoped infixl:25 " ⇒ " => fun φ ψ ↦ ¬φ ∨ ψ
-
-def up : Formula Λ → (start : ℕ := 0) → Formula Λ
-  | .top,             _     => ⊤
-  | .bot,             _     => ⊥
-  | .or φ ψ,          start => up φ start ∨ up ψ start
-  | .and φ ψ,         start => up φ start ∧ up ψ start
-  | .modality l args, start => .modality l fun a ↦ up (args a) start
-  | .var x,           start => if x < start then ^x else ^(x + 1)
-  | .lfp φ,           start => μ, up φ (start + 1)
-  | .gfp φ,           start => ν, up φ (start + 1)
-
-scoped notation "⇑ " φ => Formula.up φ
-
-def subst : Formula Λ → (ℕ × Formula Λ) → Formula Λ
-  | .top,             _      => ⊤
-  | .bot,             _      => ⊥
-  | .or φ ψ,          σ      => subst φ σ ∨ subst ψ σ
-  | .and φ ψ,         σ      => subst φ σ ∧ subst ψ σ
-  | .modality l args, σ      => .modality l fun a ↦ subst (args a) σ
-  | .var x,           (y, ψ) => if x < y then ^x else
-                                if x > y then ^(x - 1) else
-                                ψ
-  | .lfp φ,           (y, ψ) => μ, subst φ (y + 1, ⇑ψ)
-  | .gfp φ,           (y, ψ) => ν, subst φ (y + 1, ⇑ψ)
-
-macro_rules
-  | `($φ[$ψ/^$n]) => `(Formula.subst $φ ($n, $ψ))
-
-end Formula
-
-section Semantics
-
-class Model (Λ : Type) [Modalities Λ] (F : Type → Type) [Functor F] where
-  lifting {X : Type} (l : Λ) : (args : Modalities.signature l → Set X) → Set (F X)
-
-abbrev Model.lift {Λ : Type} [Modalities Λ] (l : Λ) (F : Type → Type) [Functor F] [Model Λ F] {X : Type} : (args : Modalities.signature l → Set X) → Set (F X) :=
-  Model.lifting l
-
-class LawfulModel (Λ : Type) [Modalities Λ] (F : Type → Type) [Functor F] [LawfulFunctor F] [Model Λ F] where
-  lifting_natural {X Y : Type} (f : X → Y) (l : Λ) (args : Modalities.signature l → Set Y) :
-      (Model.lift l F fun a ↦ f ⁻¹' (args a)) = ((Functor.map f) ⁻¹' (Model.lift l F args))
-  lifting_monotone {X : Type} (l : Λ) (args args' : Modalities.signature l → Set X) :
-      (∀ a, args a ⊆ args' a) → Model.lift l F args ⊆ Model.lift l F args'
-  lifting_dual {X : Type} (l : Λ) (args : Modalities.signature l → Set X) :
-      Model.lift (Modalities.dual l) F (Modalities.dualSignature l args) = (Model.lift l F fun a ↦ (args a)ᶜ)ᶜ
-
-variable {Λ : Type} [Modalities Λ]
-variable {F : Type → Type} [Functor F] [LawfulFunctor F] [Model Λ F]
-
-def Environment (X : Type) : Type := ℕ → Set X
-
-namespace Environment
-
-variable {X : Type}
-
-def empty : Environment X := λ _ ↦ ∅
-
-def up (xs : Environment X) : Environment X
-  | 0     => ∅
-  | n + 1 => xs n
-
-def subst (xs : Environment X) (n : ℕ) (x : Set X) : Environment X :=
-  λ m ↦ if m = n then x else xs m
-
-scoped notation "⇑ " φ => Environment.up φ
-
-def add (x : Set X) (xs : Environment X) : Environment X := subst (⇑ xs) 0 x
-
-infixr:67 " :: " => Environment.add
-
-variable {xs : Environment X} {x y : Set X} {n m : ℕ}
-
-@[simp]
-lemma subst_eq : subst xs n x n = x := by simp [subst]
-
-@[simp]
-lemma subst_neq : m ≠ n → subst xs n x m = xs m := by intro h; simp [subst, h]
-
-@[simp]
-lemma subst_subst_eq : subst (subst xs n x) n y = subst xs n y := by
-  apply funext
-  intro m
-  by_cases h : m = n <;> simp [h]
-
-lemma subst_subst_neq : m ≠ n → subst (subst xs n x) m y = subst (subst xs m y) n x := by
-  intro hneq
-  apply funext
-  intro k
-  by_cases h₁ : k = m <;> by_cases h₂ : k = n <;> simp [h₁, h₂, hneq, Ne.symm hneq]
-
-lemma subst_up : (⇑(subst xs n x)) = subst (⇑xs) (n + 1) x := by
-  apply funext
-  intro m
-  cases m with
-  | zero   => simp [up]
-  | succ m => by_cases h : m = n <;> simp [h, up]
-
-lemma subst_add : x :: subst xs n y = subst (x :: xs) (n + 1) y := by
-  rw [add, add, subst_subst_neq, subst_up]
-  simp
-
-end Environment
-
-def interp {X : Type} (γ : X → F X) : Formula Λ → Environment X → Set X
-  | .top,             _  => Set.univ
-  | .bot,             _  => ∅
-  | .or φ ψ,          xs => (interp γ φ xs) ∪ (interp γ ψ xs)
-  | .and φ ψ,         xs => (interp γ φ xs) ∩ (interp γ ψ xs)
-  | .modality l args, xs => γ ⁻¹' Model.lift l F fun a ↦ interp γ (args a) xs
-  | .var x,           xs => xs x
-  | .lfp φ,           xs => FixedPoints.lfp fun S ↦ interp γ φ (S :: xs)
-  | .gfp φ,           xs => FixedPoints.gfp fun S ↦ interp γ φ (S :: xs)
-
-def interp_subst_monotone [LawfulModel Λ F] {X : Type} {γ : X → F X} (φ : Formula Λ) (xs : Environment X) (n : ℕ) :
-    Monotone fun x ↦ interp γ φ (xs.subst n x) := by
-  induction φ generalizing xs n with
-  | top =>
-      intro S S' hle
-      rfl
-  | bot =>
-      intro S S' hle
-      rfl
-  | or φ ψ ihφ ihψ =>
-      intro S S' hle
-      simp only [Set.le_eq_subset, Set.union_subset_iff, interp]
-      constructor
-      · apply Set.subset_union_of_subset_left
-        exact ihφ xs n hle
-      · apply Set.subset_union_of_subset_right
-        exact ihψ xs n hle
-  | and φ ψ ihφ ihψ =>
-      intro S S' hle
-      simp only [Set.le_eq_subset, Set.subset_inter_iff, interp]
-      constructor
-      · intro x ⟨hx, _⟩
-        exact ihφ xs n hle hx
-      · intro x ⟨_, hx⟩
-        exact ihψ xs n hle hx
-  | modality l args ih =>
-      intro S S' hle
-      simp only [Set.le_eq_subset]
-      apply Set.preimage_mono
-      apply LawfulModel.lifting_monotone
-      intro a
-      exact ih a xs n hle
-  | var x =>
-      intro S S' hle
-      by_cases h : x = n
-      · simp only [interp, h, Environment.subst_eq, Set.le_eq_subset]
-        exact hle
-      · simp [h, interp]
-  | lfp φ ihφ =>
-      intro S S' hle
-      simp only [interp, Set.le_eq_subset, FixedPoints.lfp, Set.sInf_eq_sInter, Set.subset_sInter_iff, Set.mem_setOf_eq]
-      intro U hU x hx
-      apply hx
-      calc
-        interp γ φ (U :: xs.subst n S) = interp γ φ ((U :: xs).subst (n + 1) S)  := by rw [Environment.subst_add]
-        _                              ⊆ interp γ φ ((U :: xs).subst (n + 1) S') := ihφ _ _ hle
-        _                              = interp γ φ (U :: xs.subst n S')         := by rw [Environment.subst_add]
-        _                              ⊆ U                                       := hU
-  | gfp φ ihφ =>
-      intro S S' hle
-      simp only [interp, Set.le_eq_subset, FixedPoints.gfp, Set.sSup_eq_sUnion, Set.sUnion_subset_iff, Set.mem_setOf_eq]
-      intro U hU x hx
-      use U; constructor
-      · calc
-          U ⊆ interp γ φ (U :: xs.subst n S)          := hU
-          _ = interp γ φ ((U :: xs).subst (n + 1) S)  := by rw [Environment.subst_add]
-          _ ⊆ interp γ φ ((U :: xs).subst (n + 1) S') := ihφ _ _ hle
-          _ = interp γ φ (U :: xs.subst n S')         := by rw [Environment.subst_add]
-      · exact hx
-
-lemma interp_lfp_isLeastFixedPt [LawfulModel Λ F] {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) :
-    Function.IsLeastFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.lfp φ) xs) := by
-  apply FixedPoints.lfp_isLeastFixedPt
-  simp [Environment.add, interp_subst_monotone]
-
-lemma interp_gfp_isGreatestFixedPt [LawfulModel Λ F] {X : Type} (γ : X → F X) (φ : Formula Λ) (xs : Environment X) :
-    Function.IsGreatestFixedPt (fun S ↦ interp γ φ (S :: xs)) (interp γ (.gfp φ) xs) := by
-  apply FixedPoints.gfp_isGreatestFixedPt
-  simp [Environment.add, interp_subst_monotone]
-
-end Semantics