2 files changed, 621 insertions, 0 deletions
diff --git a/Nominal/NameRestriction/Finsupp.lean b/Nominal/NameRestriction/Finsupp.lean
new file mode 100644
index 0000000..3059bba
--- /dev/null
+++ b/Nominal/NameRestriction/Finsupp.lean
@@ -0,0 +1,357 @@
+import Mathlib
+import Nominal.Support
+import Nominal.Equivariance
+import Nominal.Category
+import Nominal.Permutations
+import Nominal.Instances.Basic
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+
+namespace PermSet
+
+/-- Restrict a type to its finitely supported elements -/
+abbrev Finsupp (X : Type) [PermSet 𝔸 X] : Type :=
+  { x : X // ∃ S, PermSet.HasSupport 𝔸 x S ∧ S.Finite }
+
+namespace Finsupp
+
+variable {X : Type} [PermSet 𝔸 X]
+
+instance : PermSet 𝔸 (Finsupp 𝔸 X) where
+  smul π x := ⟨π • x.val, by
+    obtain ⟨S, ⟨hS₁, hS₂⟩⟩ := x.prop
+    use π • S; constructor
+    · rw [← Rel.equivariant 𝔸 (HasSupport 𝔸)]
+      exact hS₁
+    · exact Set.Finite.smul_set hS₂⟩
+  one_smul x := by
+    apply Subtype.eq
+    exact MulAction.one_smul x.val
+  mul_smul π τ x := by
+    apply Subtype.eq
+    exact MulAction.mul_smul π τ x.val
+
+@[simp] lemma smul_val (π : FPerm 𝔸) (x : Finsupp 𝔸 X) : (π • x).val = π • x.val := rfl
+
+instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : Finsupp 𝔸 X → X) := by
+  constructor; simp
+
+instance : NominalSet 𝔸 (Finsupp 𝔸 X) where
+  fin_supp x := by
+    obtain ⟨S, ⟨hS₁, hS₂⟩⟩ := x.prop
+    use S; constructor
+    · intro π hπ
+      apply Subtype.eq
+      exact hS₁ hπ
+    · exact hS₂
+
+end Finsupp
+
+abbrev FinsuppSet (X : Type) [PermSet 𝔸 X] : Type :=
+  Finsupp 𝔸 (Set X)
+
+instance {X Y : Type} [SMul (FPerm 𝔸) X] [SMul (FPerm 𝔸) Y] : SMul (FPerm 𝔸) (X → Y) where
+  smul π f := fun x ↦ π • f (π⁻¹ • x)
+
+@[simp] lemma smul_function {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] (π : FPerm 𝔸)
+    (f : X → Y) (x : X) : (π • f) x = π • f (π⁻¹ • x) :=
+  rfl
+
+instance {X Y : Type} [PermSet 𝔸 X] [PermSet 𝔸 Y] : PermSet 𝔸 (X → Y) where
+  one_smul f := by ext x; simp
+  mul_smul π τ f := by ext x; simp [MulAction.mul_smul]
+
+abbrev FinsuppFunction (X Y : Type) [PermSet 𝔸 X] [PermSet 𝔸 Y] : Type :=
+  Finsupp 𝔸 (X → Y)
+
+variable (X Y : Type) [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
+
+namespace Finsupp
+
+private def flatten' (f : X → PermSet.FinsuppSet 𝔸 Y) : Set (X × Y) :=
+  {p : X × Y | p.snd ∈ (f p.fst).val}
+
+instance : Function.Equivariant 𝔸 (flatten' 𝔸 X Y) := by
+  constructor
+  intro f π; ext ⟨x, y⟩; constructor
+  · simp only [flatten', PermSet.smul_function, PermSet.Finsupp.smul_val, Set.mem_setOf_eq]
+    intro hy
+    have hy' : π⁻¹ • y ∈ π⁻¹ • π • (f (π⁻¹ • x)).val := by
+      rw [Set.smul_mem_smul_set_iff]; exact hy
+    rw [inv_smul_smul] at hy'
+    rw [show (x, y) = π • (π⁻¹ • x, π⁻¹ • y) by simp]
+    rw [Set.smul_mem_smul_set_iff]
+    exact hy'
+  · intro hxy
+    have hxy' : π⁻¹ • (x, y) ∈ π⁻¹ • π • flatten' 𝔸 X Y f := by
+      rw [Set.smul_mem_smul_set_iff]; exact hxy
+    simp only [inv_smul_smul, Prod.smul_mk, flatten', Set.mem_setOf_eq] at hxy'
+    simp only [flatten', PermSet.smul_function, PermSet.Finsupp.smul_val, Set.mem_setOf_eq]
+    have hy : π • π⁻¹ • y ∈ π • (f (π⁻¹ • x)).val := by
+      rw [Set.smul_mem_smul_set_iff]; exact hxy'
+    simp only [smul_inv_smul] at hy
+    exact hy
+
+def flatten (f : PermSet.FinsuppFunction 𝔸 X (PermSet.FinsuppSet 𝔸 Y)) :
+    PermSet.FinsuppSet 𝔸 (X × Y) :=
+  ⟨flatten' 𝔸 X Y f.val, by
+    obtain ⟨S, ⟨hS₁, hS₂⟩⟩ := f.prop
+    use S; constructor
+    · apply Function.Equivariant.preserve_support
+      exact hS₁
+    · exact hS₂⟩
+
+instance : Function.Equivariant 𝔸 (flatten 𝔸 X Y) := by
+  constructor; intro p π
+  apply Subtype.eq
+  simp only [flatten, Finsupp.smul_val]
+  apply Function.equivariant
+
+private def unflatten' (S : PermSet.FinsuppSet 𝔸 (X × Y)) : X → (PermSet.FinsuppSet 𝔸 Y) :=
+  fun x ↦ ⟨{y : Y | (x, y) ∈ S.val}, by
+    -- Pitts
+    sorry⟩
+
+instance : Function.Equivariant 𝔸 (unflatten' 𝔸 X Y) := by
+  constructor
+  intro S π
+  -- Pitts
+  sorry
+
+def unflatten (S : PermSet.FinsuppSet 𝔸 (X × Y)) : PermSet.FinsuppFunction 𝔸 X (PermSet.FinsuppSet 𝔸 Y) :=
+  ⟨unflatten' 𝔸 X Y S, by
+    obtain ⟨A, ⟨hS₁, hS₂⟩⟩ := S.prop
+    use A; constructor
+    · apply Function.Equivariant.preserve_support
+      rw [← Function.Equivariant.preserve_support_inj 𝔸 Subtype.val_injective] at hS₁
+      exact hS₁
+    · exact hS₂⟩
+
+instance : Function.Equivariant 𝔸 (unflatten 𝔸 X Y) := by
+  constructor; intro p π
+  apply Subtype.eq
+  simp only [unflatten, Finsupp.smul_val]
+  apply Function.equivariant
+
+def flattenEquiv  :
+    EquivariantEquiv 𝔸
+      (PermSet.FinsuppFunction 𝔸 X (PermSet.FinsuppSet 𝔸 Y))
+      (PermSet.FinsuppSet 𝔸 (X × Y)) where
+  toFun := flatten 𝔸 X Y
+  invFun := unflatten 𝔸 X Y
+  toFun_equivariant := inferInstance
+
+end Finsupp
+
+namespace FinsuppSet
+
+private def union' : (FinsuppSet 𝔸 X × FinsuppSet 𝔸 X) → Set X :=
+  fun (S₁, S₂) ↦ S₁.val ∪ S₂.val
+
+instance : Function.Equivariant 𝔸 (union' 𝔸 X) := by
+  constructor; intro (S₁, S₂) π
+  simp only [union', PermSet.Finsupp.smul_val]
+  exact Eq.symm Set.smul_set_union
+
+def union : (FinsuppSet 𝔸 X × FinsuppSet 𝔸 X) → FinsuppSet 𝔸 X :=
+  fun p ↦ ⟨union' 𝔸 X p, by
+    use NominalSet.supp 𝔸 p; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+instance : Function.Equivariant 𝔸 (union 𝔸 X) := by
+  constructor; intro p π
+  apply Subtype.eq
+  simp only [union, Finsupp.smul_val]
+  apply Function.equivariant
+
+instance : Union (FinsuppSet 𝔸 X) := ⟨Function.curry (union 𝔸 X)⟩
+
+@[simp] lemma union_val {S₁ S₂ : FinsuppSet 𝔸 X} :
+    (S₁ ∪ S₂).val = S₁.val ∪ S₂.val := rfl
+
+@[simp] lemma union_equivariant {S₁ S₂ : FinsuppSet 𝔸 X} {π : FPerm 𝔸} :
+    π • (S₁ ∪ S₂) = π • S₁ ∪ π • S₂ := by
+  show π • (union _ _ (S₁, S₂)) = union _ _ (π • (S₁, S₂))
+  rw [← Function.equivariant]
+
+private def inter' : (FinsuppSet 𝔸 X × FinsuppSet 𝔸 X) → Set X :=
+  fun (S₁, S₂) ↦ S₁.val ∩ S₂.val
+
+instance : Function.Equivariant 𝔸 (inter' 𝔸 X) := by
+  constructor; intro (S₁, S₂) π
+  simp only [inter', PermSet.Finsupp.smul_val]
+  exact Eq.symm Set.smul_set_inter
+
+def inter : (FinsuppSet 𝔸 X × FinsuppSet 𝔸 X) → FinsuppSet 𝔸 X :=
+  fun p ↦ ⟨inter' 𝔸 X p, by
+    use NominalSet.supp 𝔸 p; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+instance : Function.Equivariant 𝔸 (inter 𝔸 X) := by
+  constructor; intro p π
+  apply Subtype.eq
+  simp only [inter, Finsupp.smul_val]
+  apply Function.equivariant
+
+instance : Inter (FinsuppSet 𝔸 X) := ⟨Function.curry (inter 𝔸 X)⟩
+
+@[simp] lemma inter_val {S₁ S₂ : FinsuppSet 𝔸 X} :
+    (S₁ ∩ S₂).val = S₁.val ∩ S₂.val := rfl
+
+@[simp] lemma inter_equivariant {S₁ S₂ : FinsuppSet 𝔸 X} {π : FPerm 𝔸} :
+    π • (S₁ ∩ S₂) = π • S₁ ∩ π • S₂ := by
+  show π • (inter _ _ (S₁, S₂)) = inter _ _ (π • (S₁, S₂))
+  rw [← Function.equivariant]
+
+private def sdiff' : (FinsuppSet 𝔸 X × FinsuppSet 𝔸 X) → Set X :=
+  fun (S₁, S₂) ↦ S₁.val \ S₂.val
+
+instance : Function.Equivariant 𝔸 (sdiff' 𝔸 X) := by
+  constructor; intro (S₁, S₂) π
+  simp only [sdiff', PermSet.Finsupp.smul_val]
+  exact Eq.symm Set.smul_set_sdiff
+
+def sdiff : (FinsuppSet 𝔸 X × FinsuppSet 𝔸 X) → FinsuppSet 𝔸 X :=
+  fun p ↦ ⟨sdiff' 𝔸 X p, by
+    use NominalSet.supp 𝔸 p; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+instance : Function.Equivariant 𝔸 (sdiff 𝔸 X) := by
+  constructor; intro p π
+  apply Subtype.eq
+  simp only [sdiff, Finsupp.smul_val]
+  apply Function.equivariant
+
+instance : SDiff (FinsuppSet 𝔸 X) := ⟨Function.curry (sdiff 𝔸 X)⟩
+
+@[simp] lemma sdiff_val {S₁ S₂ : FinsuppSet 𝔸 X} :
+    (S₁ \ S₂).val = S₁.val \ S₂.val := rfl
+
+@[simp] lemma sdiff_equivariant {S₁ S₂ : FinsuppSet 𝔸 X} {π : FPerm 𝔸} :
+    π • (S₁ \ S₂) = π • S₁ \ π • S₂ := by
+  show π • (sdiff _ _ (S₁, S₂)) = sdiff _ _ (π • (S₁, S₂))
+  rw [← Function.equivariant]
+
+end FinsuppSet
+
+abbrev FinSet (X : Type) [PermSet 𝔸 X] :=
+  { S : Set X // S.Finite }
+
+namespace FinSet
+
+variable {X : Type} [PermSet 𝔸 X]
+
+instance : PermSet 𝔸 (FinSet 𝔸 X) where
+  smul π S := ⟨π • S.val, by
+    rw [Set.finite_smul_set]
+    exact S.prop⟩
+  one_smul x := by
+    apply Subtype.eq
+    exact MulAction.one_smul x.val
+  mul_smul π τ x := by
+    apply Subtype.eq
+    exact MulAction.mul_smul π τ x.val
+
+@[simp] lemma smul_val (π : FPerm 𝔸) (S : FinSet 𝔸 X) : (π • S).val = π • S.val := rfl
+
+instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : FinSet 𝔸 X → Set X) := by
+  constructor; simp
+
+variable {X : Type} [NominalSet 𝔸 X]
+
+instance : NominalSet 𝔸 (FinSet 𝔸 X) where
+  fin_supp := by sorry
+
+@[simp] lemma supp {S : FinSet 𝔸 X} : NominalSet.supp 𝔸 S = ⋃₀ {NominalSet.supp 𝔸 x | x ∈ S.val} := by sorry
+
+@[simp] lemma fresh {a : 𝔸} {S : FinSet 𝔸 X} : a # S ↔ ∀ x ∈ S.val, a # x := by
+  simp [NominalSet.IsFresh]
+
+def toFinsuppSet (S : FinSet 𝔸 X) : FinsuppSet 𝔸 X :=
+  ⟨S.val, by
+    use NominalSet.supp 𝔸 S; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+@[simp] lemma toFinsuppSet_val (S : FinSet 𝔸 X) : S.toFinsuppSet.val = S.val := rfl
+
+noncomputable def toFinset (S : FinSet 𝔸 X) : Finset X :=
+  S.prop.toFinset
+
+def union : (FinSet 𝔸 X × FinSet 𝔸 X) → FinSet 𝔸 X :=
+  fun (S₁, S₂) ↦ ⟨S₁.val ∪ S₂.val, Set.Finite.union S₁.prop S₂.prop⟩
+
+instance : Union (FinSet 𝔸 X) := ⟨Function.curry (union 𝔸)⟩
+
+instance : Function.Equivariant 𝔸 (union 𝔸 : (FinSet 𝔸 X × FinSet 𝔸 X → FinSet 𝔸 X)) := by
+  constructor; intro (S₁, S₂) π
+  apply Subtype.eq
+  simp only [union, smul_val]
+  exact Eq.symm Set.smul_set_union
+
+@[simp] lemma union_val {S₁ S₂ : FinSet 𝔸 X} :
+    (S₁ ∪ S₂).val = S₁.val ∪ S₂.val := rfl
+
+@[simp] lemma union_equivariant {S₁ S₂ : FinSet 𝔸 X} {π : FPerm 𝔸} :
+    π • (S₁ ∪ S₂) = π • S₁ ∪ π • S₂ := by
+  show π • (union _ (S₁, S₂)) = union _ (π • (S₁, S₂))
+  rw [← Function.equivariant]
+
+def inter : (FinSet 𝔸 X × FinSet 𝔸 X) → FinSet 𝔸 X :=
+  fun (S₁, S₂) ↦ ⟨S₁.val ∩ S₂.val, Set.Finite.inter_of_left S₁.prop S₂.val⟩
+
+instance : Function.Equivariant 𝔸 (inter 𝔸 : (FinSet 𝔸 X × FinSet 𝔸 X → FinSet 𝔸 X)) := by
+  constructor; intro (S₁, S₂) π
+  apply Subtype.eq
+  simp only [inter, smul_val]
+  exact Eq.symm Set.smul_set_inter
+
+instance : Inter (FinSet 𝔸 X) := ⟨Function.curry (inter 𝔸)⟩
+
+@[simp] lemma inter_val {S₁ S₂ : FinSet 𝔸 X} :
+    (S₁ ∩ S₂).val = S₁.val ∩ S₂.val := rfl
+
+@[simp] lemma inter_equivariant {S₁ S₂ : FinSet 𝔸 X} {π : FPerm 𝔸} :
+    π • (S₁ ∩ S₂) = π • S₁ ∩ π • S₂ := by
+  show π • (inter _ (S₁, S₂)) = inter _ (π • (S₁, S₂))
+  rw [← Function.equivariant]
+
+def sdiff : (FinSet 𝔸 X × FinSet 𝔸 X) → FinSet 𝔸 X :=
+  fun (S₁, S₂) ↦ ⟨S₁.val \ S₂.val, Set.Finite.diff S₁.prop⟩
+
+instance : Function.Equivariant 𝔸 (sdiff 𝔸 : (FinSet 𝔸 X × FinSet 𝔸 X → FinSet 𝔸 X)) := by
+  constructor; intro (S₁, S₂) π
+  apply Subtype.eq
+  simp only [sdiff, smul_val]
+  exact Eq.symm Set.smul_set_sdiff
+
+def empty : FinSet 𝔸 X :=
+  ⟨∅, Set.finite_empty⟩
+
+instance : EmptyCollection (FinSet 𝔸 X) := ⟨empty 𝔸⟩
+
+@[simp] lemma empty_val : (∅ : FinSet 𝔸 X).val = ∅ := rfl
+
+instance : SDiff (FinSet 𝔸 X) := ⟨Function.curry (sdiff 𝔸)⟩
+
+@[simp] lemma sdiff_val {S₁ S₂ : FinSet 𝔸 X} :
+    (S₁ \ S₂).val = S₁.val \ S₂.val := rfl
+
+@[simp] lemma sdiff_equivariant {S₁ S₂ : FinSet 𝔸 X} {π : FPerm 𝔸} :
+    π • (S₁ \ S₂) = π • S₁ \ π • S₂ := by
+  show π • (sdiff _ (S₁, S₂)) = sdiff _ (π • (S₁, S₂))
+  rw [← Function.equivariant]
+
+end FinSet
+
+def Finset.toPermFinSet {S : Finset X} : PermSet.FinSet 𝔸 X :=
+  ⟨S, Finset.finite_toSet S⟩
+
+end PermSet
diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
new file mode 100644
index 0000000..8ef60fe
--- /dev/null
+++ b/Nominal/NameRestriction/Model.lean
@@ -0,0 +1,264 @@
+import Mathlib
+import Nominal.Support
+import Nominal.Equivariance
+import Nominal.Category
+import Nominal.Permutations
+import Nominal.Instances.Basic
+import Nominal.Instances.Abstraction
+import Nominal.NameRestriction.Finsupp
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+
+-- M₀ algebra structure: Equivariant join semilattices with name restriction
+
+class AlgebraStructure (X : Type) [NominalSet 𝔸 X] where
+  bot : Unit →ₑ[𝔸] X
+  join : (X × X) →ₑ[𝔸] X
+  res : NameAbstraction 𝔸 X →ₑ[𝔸] X
+  ax_neutral : ∀ x, join (x, bot ()) = x
+  ax_idempotent : ∀ x, join (x, x) = x
+  ax_commutative : ∀ x y, join (x, y) = join (y, x)
+  ax_associative : ∀ x y z, join (join (x, y), z) = join (x, join (y, z))
+  ax_fresh : ∀ a x, a # x → res (⟪a⟫ x) = x
+  ax_swap : ∀ a b x, res (⟪a⟫ res (⟪b⟫ x)) = res (⟪b⟫ res (⟪a⟫ x))
+  ax_distributive : ∀ a x y, res (⟪a⟫ join (x, y)) = join (res (⟪a⟫ x), res (⟪a⟫ y))
+  ax_redundant : ∀ a x, x = join (x, res (⟪a⟫ x))
+
+private abbrev AlgebraStructure.bot' {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
+  (AlgebraStructure.bot : Unit →ₑ[𝔸] X)
+private abbrev AlgebraStructure.join' {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
+  (AlgebraStructure.join : (X × X) →ₑ[𝔸] X)
+
+notation "⊥[" A "]" => AlgebraStructure.bot' A ()
+notation:60 x " ∨[" A "] " y => AlgebraStructure.join' A (x, y)
+infixl:60 " \\ " => fun a x => AlgebraStructure.res (⟪a⟫ x)
+
+namespace AlgebraStructure
+
+variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X]
+
+lemma bot_supp : NominalSet.supp 𝔸 (⊥[𝔸] : X) = ∅ := by
+  rw [← Set.subset_empty_iff]
+  show NominalSet.supp 𝔸 ((bot' 𝔸).toFun ()) ⊆ ∅
+  grw [Function.Equivariant.supp_subset]
+  simp
+
+lemma join_equivariant {x y : X} {π : FPerm 𝔸} : π • (x ∨[𝔸] y) = (π • x) ∨[𝔸] (π • y) := by
+  show π • (join' 𝔸).toFun (x, y) = (join' 𝔸).toFun (π • (x, y))
+  rw [← Function.equivariant]
+
+lemma res_equivariant {a : 𝔸} {x : X} {π : FPerm 𝔸} : π • (a \ x) = (π • a) \ (π • x) := by
+  show π • res.toFun (⟪a⟫ x) = res.toFun (π • (⟪a⟫ x))
+  rw [← Function.equivariant]
+
+end AlgebraStructure
+
+-- Base Model: M₀ X
+
+def BaseModel (X : Type) [NominalSet 𝔸 X] : Type :=
+  PermSet.FinSet 𝔸 X
+
+namespace BaseModel
+
+variable {X : Type} [NominalSet 𝔸 X]
+
+instance : NominalSet 𝔸 (BaseModel 𝔸 X) := PermSet.FinSet.instNominalSet 𝔸
+instance : EmptyCollection (BaseModel 𝔸 X) := PermSet.FinSet.instEmptyCollection 𝔸
+instance : Union (BaseModel 𝔸 X) := PermSet.FinSet.instUnion 𝔸
+instance : Inter (BaseModel 𝔸 X) := PermSet.FinSet.instInter 𝔸
+instance : SDiff (BaseModel 𝔸 X) := PermSet.FinSet.instSDiff 𝔸
+
+@[simp] lemma empty_val : (∅ : BaseModel 𝔸 X).val = ∅ := rfl
+@[simp] lemma union_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∪ S₂).val = S₁.val ∪ S₂.val := rfl
+@[simp] lemma inter_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∩ S₂).val = S₁.val ∩ S₂.val := rfl
+@[simp] lemma sdiff_val {S₁ S₂ : BaseModel 𝔸 X} : (S₁ \ S₂).val = S₁.val \ S₂.val := rfl
+@[simp] lemma smul_val {L : BaseModel 𝔸 X} {π : FPerm 𝔸} : (π • L).val = π • L.val := rfl
+
+def bot : Unit → BaseModel 𝔸 X :=
+  fun _ ↦ ∅
+
+instance : Function.Equivariant 𝔸 (bot 𝔸 : Unit → BaseModel 𝔸 X) := by
+  constructor; intro _ π
+  apply Subtype.eq; simp [bot]
+
+def union : (BaseModel 𝔸 X × BaseModel 𝔸 X) → BaseModel 𝔸 X := PermSet.FinSet.union 𝔸
+
+instance : Function.Equivariant 𝔸 (union 𝔸 : (BaseModel 𝔸 X × BaseModel 𝔸 X) → BaseModel 𝔸 X) :=
+  PermSet.FinSet.instEquivariantProdUnion 𝔸
+
+
+def restrict : NameAbstraction 𝔸 (BaseModel 𝔸 X) → BaseModel 𝔸 X := Quotient.lift
+  (fun ⟨a, S⟩ ↦ ⟨{x ∈ S.val | a # x}, by
+    apply Set.Finite.subset S.prop; simp⟩)
+  (by
+    intro ⟨a₁, S₁⟩ ⟨a₂, S₂⟩ haeq
+    apply Subtype.eq
+    simp only
+    rw [← NameAbstraction.eq_iff_alpha_eq 𝔸 (BaseModel 𝔸 X), NameAbstraction.eq_iff_cases] at haeq
+    cases haeq with
+    | inl h => rw [h.left, h.right]
+    | inr h =>
+      ext x; constructor
+      · intro ⟨hx, ha₁⟩
+        have hx' : ⸨a₁, a₂⸩ • x ∈ S₂.val := by
+          rw [← Set.mem_inv_smul_set_iff, FPerm.swap_inv]
+          show x ∈ (⸨a₁, a₂⸩ • S₂).val
+          rw [← h.right.right]; exact hx
+        have ha₂ := h.right.left
+        rw [PermSet.FinSet.fresh] at ha₂
+        specialize ha₂ (⸨a₁, a₂⸩ • x) hx'
+        nth_rw 1 [show a₁ = ⸨a₁, a₂⸩ • a₂ by simp] at ha₂
+        rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] at ha₂
+        constructor
+        · rw [← show ⸨a₁, a₂⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 ha₁ ha₂]
+          exact hx'
+        · exact ha₂
+      · intro ⟨hx, ha₂⟩
+        have hx' : ⸨a₁, a₂⸩ • x ∈ S₁.val := by
+          rw [← Set.mem_inv_smul_set_iff, FPerm.swap_inv]
+          show x ∈ (⸨a₁, a₂⸩ • S₁).val
+          rw [h.right.right, ← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul]
+          exact hx
+        have ha₁ := h.right.left
+        rw [PermSet.FinSet.fresh] at ha₁
+        specialize ha₁ x hx
+        rw [← show ⸨a₁, a₂⸩ • x = x from NominalSet.fresh_swap_fix 𝔸 ha₁ ha₂] at hx'
+        rw [← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul] at hx'
+        exact ⟨hx', ha₁⟩)
+
+instance : Function.Equivariant 𝔸 (restrict 𝔸 : NameAbstraction 𝔸 (BaseModel 𝔸 X) → BaseModel 𝔸 X) := by
+  constructor
+  apply Quotient.ind
+  intro ⟨a, S⟩ π
+  apply Subtype.eq
+  simp only [restrict, NameAbstraction.smul, Quotient.lift_mk, smul_val]
+  ext x; constructor
+  · intro ⟨hx, hfresh⟩
+    rw [Set.mem_smul_set_iff_inv_smul_mem]; constructor
+    · rw [← Set.mem_smul_set_iff_inv_smul_mem]; exact hx
+    · rw [show a = π⁻¹ • π • a by simp, ← Rel.equivariant 𝔸 NominalSet.IsFresh]
+      exact hfresh
+  · rw [Set.mem_smul_set_iff_inv_smul_mem]
+    intro ⟨hx, hfresh⟩; constructor
+    · rw [Set.mem_smul_set_iff_inv_smul_mem]; exact hx
+    · rw [show x = π • π⁻¹ • x by simp, ← Rel.equivariant 𝔸 NominalSet.IsFresh]
+      exact hfresh
+
+lemma restrict_eq {a : 𝔸} {S : BaseModel 𝔸 X} :
+    (restrict 𝔸 (⟪a⟫ S)).val = {x ∈ S.val | a # x} := rfl
+
+instance : AlgebraStructure 𝔸 (BaseModel 𝔸 X) where
+  bot := ⟨bot 𝔸, inferInstance⟩
+  join := ⟨union 𝔸, inferInstance⟩
+  res := ⟨restrict 𝔸, inferInstance⟩
+  ax_neutral x := by
+    apply Subtype.eq
+    show x.val ∪ ∅ = x.val
+    simp
+  ax_idempotent x := by
+    apply Subtype.eq
+    show x.val ∪ x.val = x.val
+    simp
+  ax_commutative x y := by
+    apply Subtype.eq
+    show x.val ∪ y.val = y.val ∪ x.val
+    apply Set.union_comm
+  ax_associative x y z := by
+    apply Subtype.eq
+    show (x.val ∪ y.val) ∪ z.val = x.val ∪ (y.val ∪ z.val)
+    apply Set.union_assoc
+  ax_fresh a S := by
+    intro hfresh
+    show restrict 𝔸 (⟪a⟫ S) = S
+    apply Subtype.eq
+    rw [restrict_eq]
+    rw [PermSet.FinSet.fresh] at hfresh
+    ext x; constructor
+    · intro ⟨hS, _⟩; exact hS
+    · intro hS; exact ⟨hS, hfresh x hS⟩
+  ax_swap a b S := by
+    show restrict 𝔸 (⟪a⟫ restrict 𝔸 (⟪b⟫ S)) = restrict 𝔸 (⟪b⟫ restrict 𝔸 (⟪a⟫ S))
+    apply Subtype.eq
+    ext x
+    simp only [restrict_eq, Set.mem_setOf_eq]
+    ac_nf
+  ax_distributive a S₁ S₂ := by
+    show restrict 𝔸 (⟪a⟫ S₁ ∪ S₂) = restrict 𝔸 (⟪a⟫ S₁) ∪ restrict 𝔸 (⟪a⟫ S₂)
+    apply Subtype.eq
+    simp [restrict_eq]
+  ax_redundant a S := by
+    show S = S ∪ restrict 𝔸 (⟪a⟫ S)
+    apply Subtype.eq; ext x
+    simp only [union_val, restrict_eq, Set.mem_union, Set.mem_setOf_eq, iff_self_or, and_imp]
+    intro h _; exact h
+
+@[simp] lemma bot_eq : (⊥[𝔸] : BaseModel 𝔸 X) = ∅ := rfl
+@[simp] lemma join_eq {S₁ S₂ : BaseModel 𝔸 X} : (S₁ ∨[𝔸] S₂) = S₁ ∪ S₂ := rfl
+@[simp] lemma res_eq {a : 𝔸} {S : BaseModel 𝔸 X} : (a \ S) = restrict 𝔸 (⟪a⟫ S) := rfl
+
+end BaseModel
+
+-- Step Model: \bar{M₁} X
+
+def permissibleFunctions (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
+  { f : PermSet.FinsuppFunction 𝔸 𝔸 X |
+    ∀ a,
+      PermSet.HasSupport 𝔸 (f.val a) (NominalSet.supp 𝔸 f ∪ {a}) ∧
+      ∀ c, c # f → c ≠ a → f.val a = f.val a ∨[𝔸] (c \ (⸨a, c⸩ • f).val a) }
+
+def StepModel (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] : Type :=
+  permissibleFunctions 𝔸 X
+
+namespace StepModel
+
+variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X]
+
+instance : Set.Equivariant 𝔸 (permissibleFunctions 𝔸 X) := by
+  constructor; intro f π hf a
+  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv,
+    PermSet.atom_swap, Equiv.swap_apply_left]
+  constructor
+  · have hf₁ := (hf (π⁻¹ • a)).left
+    rw [show NominalSet.supp 𝔸 (π • f) = π • NominalSet.supp 𝔸 f from Function.equivariant _ _ _ _]
+    rw [show ({a} : Set 𝔸) = π • {π⁻¹ • a} by simp]
+    rw [← Set.smul_set_union]
+    rw [← Rel.equivariant 𝔸 (PermSet.HasSupport 𝔸)]
+    exact hf₁
+  · intro c hcf hca
+    have hf₂ := (hf (π⁻¹ • a)).right (π⁻¹ • c)
+    specialize hf₂ (by
+      rw [show f = π⁻¹ • π • f by simp]
+      rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
+      exact hcf)
+    specialize hf₂ (by
+      intro hcontra
+      have : π • π⁻¹ • c = π • π⁻¹ • a := by rw [hcontra]
+      simp only [smul_inv_smul] at this
+      exact hca this)
+    nth_rw 1 [hf₂]
+    rw [AlgebraStructure.join_equivariant, AlgebraStructure.res_equivariant]
+    simp only [smul_inv_smul, PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv,
+      PermSet.atom_swap, Equiv.swap_apply_left]
+    suffices π • ⸨π⁻¹ • a,π⁻¹ • c⸩ • f.val (π⁻¹ • c) = ⸨a, c⸩ • π • f.val (π⁻¹ • c) by rw [this]
+    rw [← MulAction.mul_smul, ← MulAction.mul_smul]
+    suffices π * ⸨π⁻¹ • a,π⁻¹ • c⸩ = ⸨a,c⸩ * π by rw [this]
+    rw [FPerm.mul_swap_eq_swap_mul, show π⁻¹ • a = π⁻¹ a from rfl, show π⁻¹ • c = π⁻¹ c from rfl]
+    simp
+
+instance : NominalSet 𝔸 (StepModel 𝔸 X) := Subtype.instNominalSetElem 𝔸
+
+@[simp] lemma smul_val (π : FPerm 𝔸) (f : StepModel 𝔸 X) : (π • f).val = π • f.val :=
+  Subtype.smul_val 𝔸 π f
+
+instance instValEquivariant : Function.Equivariant 𝔸 (Subtype.val : StepModel 𝔸 X → PermSet.FinsuppFunction 𝔸 𝔸 X) :=
+  Subtype.instValEquivariant 𝔸
+
+@[simp] lemma supp {f : StepModel 𝔸 X} : NominalSet.supp 𝔸 f = NominalSet.supp 𝔸 f.val :=
+  Subtype.supp 𝔸
+
+@[simp] lemma fresh {a : 𝔸} {f : StepModel 𝔸 X} : a # f ↔ a # f.val :=
+  Subtype.fresh 𝔸
+
+
+
+end StepModel