add M_1 model structure

1 files changed, 361 insertions, 14 deletions

diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
index a694c05..e902e58 100644
--- a/Nominal/NameRestriction/Model.lean
+++ b/Nominal/NameRestriction/Model.lean
@@ -33,6 +33,37 @@ notation "⊥[" A "]" => AlgebraStructure.bot' A ()
 notation:60 x " ∨[" A "] " y => AlgebraStructure.join' A (x, y)
 notation:60 a " \\ " x => AlgebraStructure.res (⟪a⟫ x)
 
+-- M₁ algebra structure
+
+class Depth1AlgebraStructure (X : Type) [NominalSet 𝔸 X] (Y : Type) [NominalSet 𝔸 Y] [AlgebraStructure 𝔸 Y] extends AlgebraStructure 𝔸 X where
+  pre : (𝔸 × Y) →ₑ[𝔸] X
+  abs : NameAbstraction 𝔸 Y →ₑ[𝔸] X
+  ax_pre_distributive : ∀ a x y, pre (a, x ∨[𝔸] y) = join (pre (a, x), pre (a, y))
+  ax_pre_bot : ∀ a, pre (a, ⊥[𝔸]) = bot ()
+  ax_pre_restrict_self : ∀ a x, res (⟪a⟫ pre (a, x)) = bot ()
+  ax_pre_restrict_other : ∀ a b x, a ≠ b → res (⟪a⟫ pre (b, x)) = pre (b, a \ x)
+  ax_abs_distributive : ∀ a x y, abs (⟪a⟫ x ∨[𝔸] y) = join (abs (⟪a⟫ x), abs (⟪a⟫ y))
+  ax_abs_bot : ∀ a, abs (⟪a⟫ ⊥[𝔸]) = bot ()
+  ax_abs_restrict_other : ∀ a b x, a ≠ b → abs (⟪a⟫ (b \ x)) = res (⟪b⟫ abs (⟪a⟫ x))
+  ax_local : ∀ a x, abs (⟪a⟫ x) = join (abs (⟪a⟫ x), pre (a, x))
+
+-- Structure Definitions
+
+-- (F'X)₀
+def BaseModel (X : Type) [NominalSet 𝔸 X] : Type :=
+  PermSet.FinSet 𝔸 X
+
+def Req2 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :=
+  -- Traces for all atoms include those from bound traces
+  ∀ a c, c # f → c ≠ a → f.val a = f.val a ∨[𝔸] (c \ (⸨a, c⸩ • f).val a)
+
+def permissibleFunctions (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
+  { f : PermSet.FinsuppFunction 𝔸 𝔸 X | Req2 𝔸 f }
+
+-- (F'X)ₙ₊₁
+def StepModel (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] : Type :=
+  permissibleFunctions 𝔸 X
+
 namespace AlgebraStructure
 
 variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X]
@@ -60,12 +91,22 @@ lemma res_equivariant {a : 𝔸} {x : X} {π : FPerm 𝔸} : π • (a \ x) = (�
   show π • res.toFun (⟪a⟫ x) = res.toFun (π • (⟪a⟫ x))
   rw [← Function.equivariant]
 
-end AlgebraStructure
+lemma res_fresh {a : 𝔸} {x : X} : a # (a \ x) := by
+  show a # res.toFun (⟪a⟫ x)
+  apply Function.Equivariant.preserve_fresh
+  rw [NameAbstraction.fresh]; right; rfl
 
--- Base Model: M₀ X
+lemma res_self {a : 𝔸} {x : X} : (a \ (a \ x)) = (a \ x) := by
+  apply ax_fresh
+  apply res_fresh
 
-def BaseModel (X : Type) [NominalSet 𝔸 X] : Type :=
-  PermSet.FinSet 𝔸 X
+lemma res_bot {a : 𝔸} : (a \ ⊥[𝔸]) = (⊥[𝔸] : X) := by
+  apply ax_fresh
+  apply bot_fresh
+
+end AlgebraStructure
+
+-- Base Model Definitions
 
 namespace BaseModel
 
@@ -278,16 +319,6 @@ lemma choose_restriction'
         simp only [Set.union_singleton, Set.mem_insert_iff] at h
         cases h <;> contradiction]
 
-def Req2 {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] (f : PermSet.FinsuppFunction 𝔸 𝔸 X) :=
-  -- Traces for all atoms include those from bound traces
-  ∀ a c, c # f → c ≠ a → f.val a = f.val a ∨[𝔸] (c \ (⸨a, c⸩ • f).val a)
-
-def permissibleFunctions (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] :=
-  { f : PermSet.FinsuppFunction 𝔸 𝔸 X | Req2 𝔸 f }
-
-def StepModel (X : Type) [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X] : Type :=
-  permissibleFunctions 𝔸 X
-
 namespace StepModel
 
 variable {X : Type} [NominalSet 𝔸 X] [AlgebraStructure 𝔸 X]
@@ -648,6 +679,25 @@ lemma mem_fresh (f : StepModel 𝔸 X) (a c : 𝔸) : c # f → c ≠ a → c #
   simp only [Set.union_singleton, Set.mem_insert_iff] at h
   cases h <;> contradiction
 
+lemma restrict_fresh (f : StepModel 𝔸 X) (a b : 𝔸) :
+    a ≠ b → (restrict 𝔸 (⟪a⟫ f)).val.val b = a \ (f.val.val b) := by
+  intro hne
+  let c := chooseFresh 𝔸 f a b
+  have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
+  simp only [restrict_eq', PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
+  rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hcb)]
+  suffices ⟪a⟫ f.val.val b = ⟪c⟫ ⸨a,c⸩ • f.val.val b by rw [this]
+  rw [NameAbstraction.eq_iff_cases]; right
+  constructor
+  · exact Ne.symm hca
+  · constructor
+    · nth_rw 1 [show a = ⸨a,c⸩ • c by simp]
+      rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
+      apply mem_fresh 𝔸 _ _ _ hcf hcb
+    · rw [← MulAction.mul_smul]
+      rw [FPerm.swap_mul_self]
+      rw [MulAction.one_smul]
+
 noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where
   bot := ⟨bot 𝔸, inferInstance⟩
   join := ⟨union 𝔸, inferInstance⟩
@@ -994,6 +1044,303 @@ lemma abs_eq {a : 𝔸} {x : X} {b : 𝔸} :
   have ⟨hcx, hca, hcb⟩ := chooseFresh_fresh 𝔸 x a b
   apply abs_choice 𝔸 _ _ hcx hdx hca hda hcb hdb
 
+private def pre'' : (𝔸 × X) → 𝔸 → X :=
+  fun (a, x) ↦
+    fun b ↦ if b = a then x else ⊥[𝔸]
+
+instance : Function.Equivariant 𝔸 (pre'' 𝔸 : (𝔸 × X) → 𝔸 → X) := by
+  constructor; intro (a, x) π; ext b
+  simp only [Prod.smul_mk, PermSet.smul_function]
+  by_cases heq : b = π • a
+  · rw [heq]; simp [pre'']
+  · have hne : π⁻¹ • b ≠ a := by
+      intro hcontra
+      rw [← hcontra] at heq
+      simp at heq
+    simp [pre'', heq, hne, AlgebraStructure.bot_equivariant]
+
+private noncomputable def pre' : (𝔸 × X) → PermSet.FinsuppFunction 𝔸 𝔸 X :=
+  fun p ↦ ⟨pre'' 𝔸 p, by
+    use NominalSet.supp 𝔸 p; constructor
+    · apply Function.Equivariant.preserve_support
+      apply NominalSet.supp_is_support
+    · apply NominalSet.supp_finite⟩
+
+private lemma pre_req2 {a : 𝔸} {x : X} : Req2 𝔸 (pre' 𝔸 (a, x)) := by
+  intro b c hcpre hcb
+  have hinf : (NominalSet.supp 𝔸 (pre' 𝔸 (a, x)) ∪ {a} ∪ {b})ᶜ.Infinite := by
+    apply Set.Finite.infinite_compl
+    rw [Set.finite_union, Set.finite_union]
+    constructor
+    · constructor
+      · apply NominalSet.supp_finite
+      · apply Set.finite_singleton
+    · apply Set.finite_singleton
+  obtain ⟨d, hd⟩ := hinf.nonempty
+  simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd
+  have hdpre : d # pre' 𝔸 (a, x) := hd.left.left
+  have hda : d ≠ a := hd.left.right
+  have hdb : d ≠ b := hd.right
+  rw [choose_restriction' 𝔸 _ _ _ _ _ hcpre hdpre hcb hdb hcb hdb]
+  simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left]
+  rw [show (pre' 𝔸 (a, x)).val d = ⊥[𝔸] by simp [pre', pre'', hda]]
+  rw [AlgebraStructure.bot_equivariant]
+  rw [AlgebraStructure.res_bot]
+  rw [AlgebraStructure.ax_neutral]
+
+noncomputable def pre : (𝔸 × X )→ StepModel 𝔸 X :=
+  fun p ↦ ⟨pre' 𝔸 p, by
+    suffices ∀ p, Req2 𝔸 (pre' 𝔸 p) by apply this
+    intro ⟨a, x⟩
+    apply pre_req2⟩
+
+instance : Function.Equivariant 𝔸 (pre 𝔸 : (𝔸 × X) → StepModel 𝔸 X) := by
+  constructor; intro x π
+  apply Subtype.eq; apply Subtype.eq
+  simp only [pre, pre', smul_val, PermSet.Finsupp.smul_val]
+  rw [← Function.equivariant]
+
+@[simp] lemma pre_eq_if_eq {a : 𝔸} {x : X} : (pre 𝔸 (a, x)).val.val a = x := by
+  simp [pre, pre', pre'']
+
+lemma pre_eq_if_ne {a b : 𝔸} {x : X} : a ≠ b → (pre 𝔸 (a, x)).val.val b = ⊥[𝔸] := by
+  intro hne
+  simp [pre, pre', pre'', Ne.symm hne]
+
+noncomputable instance : Depth1AlgebraStructure 𝔸 (StepModel 𝔸 X) X where
+  pre := ⟨pre 𝔸, inferInstance⟩
+  abs := ⟨abs 𝔸, inferInstance⟩
+  ax_pre_distributive a x y := by
+    show pre 𝔸 (a, x ∨[𝔸] y) = union 𝔸 (pre 𝔸 (a, x), pre 𝔸 (a, y))
+    apply Subtype.eq; apply Subtype.eq; ext b
+    by_cases heq : b = a
+    · rw [heq, pre_eq_if_eq, union_eq, pre_eq_if_eq, pre_eq_if_eq]
+    · rw [union_eq]
+      rw [pre_eq_if_ne 𝔸 (Ne.symm heq)]
+      rw [pre_eq_if_ne 𝔸 (Ne.symm heq)]
+      rw [pre_eq_if_ne 𝔸 (Ne.symm heq)]
+      rw [AlgebraStructure.ax_idempotent]
+  ax_pre_bot a := by
+    show pre 𝔸 (a, ⊥[𝔸]) = bot 𝔸 ()
+    apply Subtype.eq; apply Subtype.eq; ext b
+    by_cases heq : b = a
+    · rw [heq, pre_eq_if_eq, bot_eq]
+    · rw [pre_eq_if_ne 𝔸 (Ne.symm heq), bot_eq]
+  ax_pre_restrict_self a x := by
+    show restrict 𝔸 (⟪a⟫ pre 𝔸 (a, x)) = bot 𝔸 ()
+    apply Subtype.eq; apply Subtype.eq; ext b
+    simp only [restrict_eq', PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv,
+      bot_eq]
+    let c := chooseFresh 𝔸 (pre 𝔸 (a, x)) a b
+    have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 (pre 𝔸 (a, x)) a b
+    have hne : ⸨a,chooseFresh 𝔸 (pre 𝔸 (a, x)) a b⸩ • b ≠ a := by
+      by_cases heq : b = a
+      · nth_rw 2 [heq]
+        simp only [PermSet.atom_swap, Equiv.swap_apply_left]
+        exact hca
+      · rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne heq (Ne.symm hcb)]
+        exact heq
+    rw [pre_eq_if_ne 𝔸 (Ne.symm hne)]
+    rw [AlgebraStructure.bot_equivariant]
+    rw [AlgebraStructure.res_bot]
+  ax_pre_restrict_other a b x := by
+    intro hne
+    show restrict 𝔸 (⟪a⟫ pre 𝔸 (b, x)) = pre 𝔸 (b, a \ x)
+    apply Subtype.eq; apply Subtype.eq; ext l
+    have hinf : (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 (pre 𝔸 (b, x)) ∪ {a} ∪ {b} ∪ {l})ᶜ.Infinite := by
+      apply Set.Finite.infinite_compl
+      rw [Set.finite_union, Set.finite_union, Set.finite_union, Set.finite_union]
+      constructor
+      · constructor
+        · constructor
+          · constructor
+            · apply NominalSet.supp_finite
+            · apply NominalSet.supp_finite
+          · apply Set.finite_singleton
+        · apply Set.finite_singleton
+      · apply Set.finite_singleton
+    obtain ⟨c, hc⟩ := hinf.nonempty
+    simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc
+    have hcx : c # x := hc.left.left.left.left
+    have hcpre : c # pre 𝔸 (b, x) := hc.left.left.left.right
+    have hca : c ≠ a := hc.left.left.right
+    have hcb : c ≠ b := hc.left.right
+    have hcl : c ≠ l := hc.right
+    have hcres : c # (a \ x) := by
+      show c # AlgebraStructure.res.toFun (⟪a⟫ x)
+      apply Function.Equivariant.preserve_fresh
+      rw [NameAbstraction.fresh]; left; exact hcx
+    rw [restrict_eq 𝔸 c hcpre hca hcl]
+    simp only [PermSet.Finsupp.smul_val, PermSet.smul_function, FPerm.swap_inv]
+    by_cases heq : l = b
+    · rw [heq]
+      rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hcb)]
+      rw [pre_eq_if_eq, pre_eq_if_eq]
+      nth_rw 1 [← show ⸨a, c⸩ • a = c by simp]
+      rw [← AlgebraStructure.res_equivariant]
+      rw [NominalSet.fresh_swap_fix 𝔸 (AlgebraStructure.res_fresh 𝔸) hcres]
+    · have hne : ⸨a,c⸩ • l ≠ b := by
+        by_cases heq' : l = a
+        · simp [heq', hcb]
+        · rw [show ⸨a,c⸩ • l = l from FPerm.swap_apply_of_ne_of_ne heq' (Ne.symm hcl)]
+          exact heq
+      rw [pre_eq_if_ne 𝔸 (Ne.symm hne)]
+      rw [pre_eq_if_ne 𝔸 (Ne.symm heq)]
+      rw [AlgebraStructure.bot_equivariant]
+      rw [AlgebraStructure.res_bot]
+  ax_abs_distributive a x y := by
+    show abs 𝔸 (⟪a⟫ x ∨[𝔸] y) = union 𝔸 (abs 𝔸 (⟪a⟫ x), abs 𝔸 (⟪a⟫ y))
+    apply Subtype.eq; apply Subtype.eq; ext b
+    have hinf : (NominalSet.supp 𝔸 (x ∨[𝔸] y) ∪ NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 y ∪ {a} ∪ {b})ᶜ.Infinite := by
+      apply Set.Finite.infinite_compl
+      rw [Set.finite_union, Set.finite_union, Set.finite_union, Set.finite_union]
+      constructor
+      · constructor
+        · constructor
+          · constructor
+            · apply NominalSet.supp_finite
+            · apply NominalSet.supp_finite
+          · apply NominalSet.supp_finite
+        · apply Set.finite_singleton
+      · apply Set.finite_singleton
+    obtain ⟨c, hc⟩ := hinf.nonempty
+    simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc
+    have hcxy : c # (x ∨[𝔸] y) := hc.left.left.left.left
+    have hcx : c # x := hc.left.left.left.right
+    have hcy : c # y := hc.left.left.right
+    have hca : c ≠ a := hc.left.right
+    have hcb : c ≠ b := hc.right
+    rw [abs_eq 𝔸 c hcxy hca hcb]
+    rw [union_eq]
+    rw [abs_eq 𝔸 c hcx hca hcb]
+    rw [abs_eq 𝔸 c hcy hca hcb]
+    rw [AlgebraStructure.join_equivariant]
+    rw [AlgebraStructure.ax_distributive]
+    rw [← AlgebraStructure.join_equivariant]
+  ax_abs_bot a := by
+    show abs 𝔸 (⟪a⟫ ⊥[𝔸]) = bot 𝔸 ()
+    apply Subtype.eq; apply Subtype.eq; ext b
+    rw [abs_eq', bot_eq]
+    rw [AlgebraStructure.bot_equivariant]
+    rw [AlgebraStructure.res_bot]
+    rw [AlgebraStructure.bot_equivariant]
+  ax_abs_restrict_other a b x := by
+    intro hne
+    show abs 𝔸 (⟪a⟫ (b \ x)) = restrict 𝔸 (⟪b⟫ abs 𝔸 (⟪a⟫ x))
+    apply Subtype.eq; apply Subtype.eq; ext l
+    by_cases heq : l = b
+    · rw [heq]
+      have hinf : (NominalSet.supp 𝔸 x ∪ {a} ∪ {b})ᶜ.Infinite := by
+        apply Set.Finite.infinite_compl
+        rw [Set.finite_union, Set.finite_union]
+        constructor
+        · constructor
+          · apply NominalSet.supp_finite
+          · apply Set.finite_singleton
+        · apply Set.finite_singleton
+      obtain ⟨c, hc⟩ := hinf.nonempty
+      simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc
+      have hcx : c # x := hc.left.left
+      have hcres : c # b \ x := by
+        show c # AlgebraStructure.res.toFun (⟪b⟫ x)
+        apply Function.Equivariant.preserve_fresh
+        rw [NameAbstraction.fresh]; left; exact hcx
+      have hcabs : c # abs 𝔸 (⟪a⟫ x) := by
+        apply Function.Equivariant.preserve_fresh
+        rw [NameAbstraction.fresh]; left; exact hcx
+      have hca : c ≠ a := hc.left.right
+      have hcb : c ≠ b := hc.right
+      have hinf' : (NominalSet.supp 𝔸 x ∪ {a} ∪ {b} ∪ {c})ᶜ.Infinite := by
+        apply Set.Finite.infinite_compl
+        rw [Set.finite_union, Set.finite_union, Set.finite_union]
+        constructor
+        · constructor
+          · constructor
+            · apply NominalSet.supp_finite
+            · apply Set.finite_singleton
+          · apply Set.finite_singleton
+        · apply Set.finite_singleton
+      obtain ⟨d, hd⟩ := hinf'.nonempty
+      simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hd
+      have hdx : d # x := hd.left.left.left
+      have hdres : d # b \ x := by
+        show d # AlgebraStructure.res.toFun (⟪b⟫ x)
+        apply Function.Equivariant.preserve_fresh
+        rw [NameAbstraction.fresh]; left; exact hdx
+      have hda : d ≠ a := hd.left.left.right
+      have hdb : d ≠ b := hd.left.right
+      have hdc : d ≠ c := hd.right
+      rw [abs_eq 𝔸 c hcres hca hcb]
+      nth_rw 2 [← show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hcb)]
+      rw [← AlgebraStructure.res_equivariant]
+      rw [← MulAction.mul_smul]
+      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne hne (Ne.symm hca)]
+      rw [MulAction.mul_smul]
+      rw [AlgebraStructure.res_self]
+      rw [NominalSet.fresh_swap_fix 𝔸 (AlgebraStructure.res_fresh 𝔸) hcres]
+      rw [restrict_eq 𝔸 c hcabs hcb hcb]
+      simp only [PermSet.atom_swap, Equiv.swap_apply_left, PermSet.Finsupp.smul_val,
+        PermSet.smul_function, FPerm.swap_inv]
+      nth_rw 1 [← show ⸨b, c⸩ • b = c by simp]
+      rw [← AlgebraStructure.res_equivariant]
+      rw [abs_eq 𝔸 d hdx hda hdc]
+      nth_rw 4 [← show ⸨c, d⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hcb) (Ne.symm hdb)]
+      rw [← AlgebraStructure.res_equivariant]
+      nth_rw 3 [← show ⸨a, d⸩ • c = c from FPerm.swap_apply_of_ne_of_ne hca (Ne.symm hdc)]
+      rw [← AlgebraStructure.res_equivariant]
+      rw [show (c \ x) = x from AlgebraStructure.ax_fresh c x hcx]
+      nth_rw 4 [← show ⸨a, d⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hdb)]
+      rw [← AlgebraStructure.res_equivariant]
+      nth_rw 2 [← MulAction.mul_smul]
+      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne (Ne.symm hca) (Ne.symm hda)]
+      rw [MulAction.mul_smul]
+      rw [NominalSet.fresh_swap_fix 𝔸 hcres hdres]
+      rw [← MulAction.mul_smul]
+      rw [FPerm.mul_swap_eq_swap_mul, FPerm.swap_apply_right, FPerm.swap_apply_of_ne_of_ne hne (Ne.symm hca)]
+      rw [MulAction.mul_smul]
+      rw [NominalSet.fresh_swap_fix 𝔸 (AlgebraStructure.res_fresh 𝔸) hcres]
+    · rw [restrict_fresh 𝔸 _ _ _ (Ne.symm heq)]
+      have hinf : (NominalSet.supp 𝔸 x ∪ NominalSet.supp 𝔸 (b \ x) ∪ {a} ∪ {b} ∪ {l})ᶜ.Infinite := by
+        apply Set.Finite.infinite_compl
+        rw [Set.finite_union, Set.finite_union, Set.finite_union, Set.finite_union]
+        constructor
+        · constructor
+          · constructor
+            · constructor
+              · apply NominalSet.supp_finite
+              · apply NominalSet.supp_finite
+            · apply Set.finite_singleton
+          · apply Set.finite_singleton
+        · apply Set.finite_singleton
+      obtain ⟨c, hc⟩ := hinf.nonempty
+      simp only [Set.compl_union, Set.mem_inter_iff, Set.mem_compl_iff] at hc
+      have hcx : c # x := hc.left.left.left.left
+      have hcx' : c # (b \ x) := hc.left.left.left.right
+      have hca : c ≠ a := hc.left.left.right
+      have hcb : c ≠ b := hc.left.right
+      have hcl : c ≠ l := hc.right
+      rw [abs_eq 𝔸 c hcx' hca hcl]
+      rw [abs_eq 𝔸 c hcx hca hcl]
+      nth_rw 2 [AlgebraStructure.res_equivariant]
+      rw [show ⸨a,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm hne) (Ne.symm hcb)]
+      nth_rw 2 [← show ⸨l,c⸩ • b = b from FPerm.swap_apply_of_ne_of_ne (Ne.symm heq) (Ne.symm hcb)]
+      rw [← AlgebraStructure.res_equivariant]
+      rw [AlgebraStructure.ax_swap]
+  ax_local a x := by
+    show abs 𝔸 (⟪a⟫ x) = union 𝔸 (abs 𝔸 (⟪a⟫ x), pre 𝔸 (a, x))
+    apply Subtype.eq; apply Subtype.eq; ext b
+    by_cases heq : b = a
+    · rw [heq, union_eq, pre_eq_if_eq]
+      have ⟨hx, _, _⟩ := chooseFresh_fresh 𝔸 x a a
+      rw [abs_eq']
+      rw [AlgebraStructure.res_equivariant]
+      rw [PermSet.atom_swap, Equiv.swap_apply_left]
+      rw [← MulAction.mul_smul, FPerm.swap_mul_self, MulAction.one_smul]
+      rw [AlgebraStructure.ax_fresh _ x hx]
+      rw [AlgebraStructure.ax_idempotent]
+    · rw [union_eq, pre_eq_if_ne 𝔸 (Ne.symm heq)]
+      rw [AlgebraStructure.ax_neutral]
+
 end StepModel
 
 private noncomputable def ModelBundle (X : Type) [NominalSet 𝔸 X] : ℕ → ((T : Type) × ((_ : NominalSet 𝔸 T) × AlgebraStructure 𝔸 T))