From 72d53e1435c80fc2b92dd59881488e7c195db756 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Tue, 13 Jan 2026 00:59:43 +0100 Subject: add M_1 model structure --- Nominal/NameRestriction/Model.lean | 375 +++++++++++++++++++++++++++++++++++-- 1 file changed, 361 insertions(+), 14 deletions(-) (limited to 'Nominal/NameRestriction') 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)) -- cgit v1.3.1