From 7750ccdcb2afebe90da275f96e276a672a3c8a74 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Fri, 5 Dec 2025 23:32:38 +0100
Subject: revise OrbitFinite restriction for equations

---
 Algebra/Derivations.lean | 29 +++++++++++++----------------
 1 file changed, 13 insertions(+), 16 deletions(-)

(limited to 'Algebra/Derivations.lean')

diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean
index e2cd052..717ffe1 100644
--- a/Algebra/Derivations.lean
+++ b/Algebra/Derivations.lean
@@ -12,7 +12,6 @@ variable (sig : Signature)
 structure Equation where
   vars : Type
   [vars_nominal : NominalSet 𝔸 vars]
-  [vars_orbitFinite : OrbitFinite 𝔸 vars]
   left : Term 𝔸 sig vars
   right : Term 𝔸 sig vars
 
@@ -21,9 +20,6 @@ namespace Equation
 instance (eq : Equation 𝔸 sig) : NominalSet 𝔸 eq.vars :=
   eq.vars_nominal
 
-instance (eq : Equation 𝔸 sig) : OrbitFinite 𝔸 eq.vars :=
-  eq.vars_orbitFinite
-
 def HasDepth
     {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {sig : Signature}
     (eq : Equation 𝔸 sig) (n : ℕ) : Prop :=
@@ -37,6 +33,7 @@ def UniformEquation :=
 structure Theory where
   sig : Signature
   axioms : Set (UniformEquation 𝔸 sig)
+  axioms_orbitFinite : ∀ eq ∈ axioms, OrbitFinite 𝔸 eq.val.vars
 
 end Theories
 
@@ -46,7 +43,7 @@ variable {sig : Signature}
 section Helpers
 
 def UniformEquation.mk
-    (X : Type) [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] {n : ℕ} (t u : TermAtDepth 𝔸 sig X n) :
+    (X : Type) [NominalSet 𝔸 X] {n : ℕ} (t u : TermAtDepth 𝔸 sig X n) :
     UniformEquation 𝔸 sig :=
   ⟨⟨X, t.val, u.val⟩, ⟨n, t.prop, u.prop⟩⟩
 
@@ -57,47 +54,47 @@ end Helpers
 section DerivableEquations
 
 inductive Derivable (T : Theory 𝔸) : (eq : UniformEquation 𝔸 T.sig) → Prop
-  | refl {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] {x : X} :
+  | refl {X : Type} [NominalSet 𝔸 X] {x : X} :
       Derivable T (X ⊢ .var x ≣ .var x)
-  | symm {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X]
+  | symm {X : Type} [NominalSet 𝔸 X]
       {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} :
       Derivable T (X ⊢ u ≣ t) →
       Derivable T (X ⊢ t ≣ u)
-  | trans {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X]
+  | trans {X : Type} [NominalSet 𝔸 X]
       {m : ℕ} {t u v : TermAtDepth 𝔸 T.sig X m} :
       Derivable T (X ⊢ t ≣ v) →
       Derivable T (X ⊢ v ≣ u) →
       Derivable T (X ⊢ t ≣ u)
-  | cong_pure {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X]
+  | cong_pure {X : Type} [NominalSet 𝔸 X]
       {f : T.sig.pure} {m : ℕ} {ts us : T.sig.pureArgs f → TermAtDepth 𝔸 T.sig X m} :
       (∀ x, Derivable T (X ⊢ ts x ≣ us x)) →
       Derivable T (X ⊢ .pure f ts ≣ .pure f us)
-  | cong_free {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X]
+  | cong_free {X : Type} [NominalSet 𝔸 X]
       {a : 𝔸} {f : T.sig.free} {m : ℕ} {ts us : T.sig.freeArgs f → TermAtDepth 𝔸 T.sig X m} :
       (∀ x, Derivable T (X ⊢ ts x ≣ us x)) →
       Derivable T (X ⊢ .free a f ts ≣ .free a f us)
-  | cong_bound {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X]
+  | cong_bound {X : Type} [NominalSet 𝔸 X]
       {a : 𝔸} {f : T.sig.bound} {m : ℕ} {ts us : T.sig.boundArgs f → TermAtDepth 𝔸 T.sig X m} :
       (∀ x, Derivable T (X ⊢ ts x ≣ us x)) →
       Derivable T (X ⊢ .bound a f ts ≣ .bound a f us)
-  | ax' {X Y : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] [NominalSet 𝔸 Y] [OrbitFinite 𝔸 Y]
+  | ax' {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
       {m : ℕ} {r s : TermAtDepth 𝔸 T.sig Y m}
       {l : ℕ} {σ : UniformSubstitution 𝔸 T.sig Y X l} {τ : FPerm 𝔸} :
       ((Y ⊢ r ≣ s) ∈ T.axioms) →
       (∀ (y : Y) (π : FPerm 𝔸), Derivable T (X ⊢ σ (π • y) ≣ π • (σ y))) →
       Derivable T (X ⊢ σ.apply (τ • r) ≣ σ.apply (τ • s))
-  | perm {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X]
+  | perm {X : Type} [NominalSet 𝔸 X]
       {a b : 𝔸} {f : T.sig.bound} {m : ℕ} {ts us : T.sig.boundArgs f → TermAtDepth 𝔸 T.sig X m} :
       a ≠ b →
       (∀ x, a # us x) →
       (∀ x, Derivable T (X ⊢ ts x ≣ ⸨a, b⸩ • us x)) →
       Derivable T (X ⊢ .bound a f ts ≣ .bound b f us)
 
-def DerivableEq (T : Theory 𝔸) (X : Type) [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] (n : ℕ) :
+def DerivableEq (T : Theory 𝔸) (X : Type) [NominalSet 𝔸 X] (n : ℕ) :
     Rel (TermAtDepth 𝔸 T.sig X n) (TermAtDepth 𝔸 T.sig X n) :=
   fun t u => Derivable T (X ⊢ t ≣ u)
 
-variable {X Y : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] [NominalSet 𝔸 Y] [OrbitFinite 𝔸 Y]
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
 
 def UniformSubstitution.DerivablyEquivariant
     (T : Theory 𝔸) {l : ℕ} (σ : UniformSubstitution 𝔸 T.sig X Y l) : Prop :=
@@ -157,7 +154,7 @@ lemma Derivable.equivariant {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} :
       let right : TermAtDepth 𝔸 T.sig eq.val.vars n := ⟨eq.val.right, hn₂⟩
       use n; exact ⟨(π • left).prop, (π • right).prop⟩⟩
   have rename_eq
-      {Y : Type} [NominalSet 𝔸 Y] [OrbitFinite 𝔸 Y] {π : FPerm 𝔸} {k : ℕ}
+      {Y : Type} [NominalSet 𝔸 Y] {π : FPerm 𝔸} {k : ℕ}
       {r s : TermAtDepth 𝔸 T.sig Y k} : rename π (Y ⊢ r ≣ s) = (Y ⊢ π • r ≣ π • s) := rfl
   suffices ∀ eq, Derivable T eq → Derivable T (rename π eq) by
     exact this (X ⊢ t ≣ u)
-- 
cgit v1.3.1