prove depth-0 axioms

1 files changed, 25 insertions, 11 deletions

diff --git a/Nominal/NameRestriction/Model.lean b/Nominal/NameRestriction/Model.lean
index adefdb4..6195099 100644
--- a/Nominal/NameRestriction/Model.lean
+++ b/Nominal/NameRestriction/Model.lean
@@ -706,18 +706,16 @@ lemma restrict_supp (f : StepModel 𝔸 X) (a c : 𝔸) :
   rw [← supp] at this
   contradiction
 
-lemma restrict_mem_supp (f : StepModel 𝔸 X) (a b c : 𝔸) :
-    c # f → c ≠ b → c # (restrict 𝔸 (⟪a⟫ f)).val.val b := by
+lemma mem_fresh (f : StepModel 𝔸 X) (a c : 𝔸) : c # f → c ≠ a → c # f.val.val a := by
   intro hf hb hcontra
-  have h₁ : NominalSet.supp 𝔸 ((restrict 𝔸 (⟪a⟫ f)).val.val b) ⊆ NominalSet.supp 𝔸 (restrict 𝔸 (⟪a⟫ f)).val ∪ {b} :=
-    NominalSet.support_subset_supp 𝔸 (((restrict 𝔸 (⟪a⟫ f)).prop.left b)) (by
+  rw [fresh] at hf
+  have h : NominalSet.supp 𝔸 (f.val.val a) ⊆ NominalSet.supp 𝔸 f.val ∪ {a} :=
+    NominalSet.support_subset_supp 𝔸 (f.prop.left a) (by
       simp only [Set.union_singleton, Set.finite_insert]
       apply NominalSet.supp_finite)
-  specialize h₁ hcontra
-  simp only [Set.union_singleton, Set.mem_insert_iff] at h₁
-  cases h₁ with
-  | inl h => contradiction
-  | inr h => rw [← supp] at h; exact restrict_supp 𝔸 f a c hf h
+  specialize h hcontra
+  simp only [Set.union_singleton, Set.mem_insert_iff] at h
+  cases h <;> contradiction
 
 noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where
   bot := ⟨bot 𝔸, inferInstance⟩
@@ -852,7 +850,23 @@ noncomputable instance : AlgebraStructure 𝔸 (StepModel 𝔸 X) where
   ax_redundant a f := by
     show f = union 𝔸 (f, restrict 𝔸 (⟪a⟫ f))
     apply Subtype.eq; apply Subtype.eq; ext b
-    rw [union_eq, restrict_eq']
-    sorry
+    rw [union_eq]
+    by_cases heq : a = b
+    · rw [heq, restrict_eq']
+      have ⟨hcf, hcb, _⟩ := chooseFresh_fresh 𝔸 f b b
+      exact f.prop.right b _ hcf hcb
+    · rw [restrict_eq']
+      let c := chooseFresh 𝔸 f a b
+      have ⟨hcf, hca, hcb⟩ := chooseFresh_fresh 𝔸 f a b
+      rw [← fresh] at hcf
+      rw [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 heq) (Ne.symm hcb)]
+      rw [show ⟪c⟫ ⸨a,c⸩ • f.val.val b = ⸨a,c⸩ • ⟪a⟫ f.val.val b by simp]
+      rw [show ⸨a,c⸩ • ⟪a⟫ f.val.val b = ⟪a⟫ f.val.val b by
+        apply NominalSet.fresh_swap_fix
+        · rw [NameAbstraction.fresh]; right; rfl
+        · rw [NameAbstraction.fresh]; left
+          apply mem_fresh 𝔸 f b c hcf hcb]
+      apply AlgebraStructure.ax_redundant
 
 end StepModel