diff --git a/Cslib/Foundations/Relation/Basic.lean b/Cslib/Foundations/Relation/Basic.lean
index aafcddac21..9369e346cf 100644
--- a/Cslib/Foundations/Relation/Basic.lean
+++ b/Cslib/Foundations/Relation/Basic.lean
@@ -9,7 +9,13 @@ module
 public import Cslib.Foundations.Relation.Defs
 public import Mathlib.Order.WellFounded
 
-/-! # Basic properties of relations -/
+/-! # Basic properties of relations
+
+## TODO:
+Many of the results here could be upstreamed to Mathlib. In particular:
+- `ReflGen.le_reflGen` and relatives,
+- `ReflGen.to_eqvGen` and relatives.
+-/
 
 @[expose] public section
 
@@ -24,6 +30,8 @@ theorem WellFounded.iff_transGen : WellFounded (Relation.TransGen r) ↔ WellFou
 
 namespace Relation
 
+open Function
+
 /-- A pair of subrelations lifts to transitivity on the relation. -/
 @[implicit_reducible]
 def transLeftRight (s s' r : α → α → Prop) [IsTrans α r] (h : s ≤ r) (h' : s' ≤ r) :
@@ -40,28 +48,105 @@ def transLeft (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans s
 def transRight (s r : α → α → Prop) [IsTrans α r] (h : s ≤ r) : Trans r s r where
   trans hab hbc := _root_.trans hab (h _ _ hbc)
 
+@[scoped grind .]
+theorem comp_le_comp {s s' r r' : α → α → Prop} (hs : s ≤ s') (hr : r ≤ r') :
+    Comp s r ≤ Comp s' r' := fun a c ⟨b, hab, hbc⟩ ↦ ⟨b, hs a b hab, hr b c hbc⟩
+
+theorem comp_self_le (r : α → α → Prop) [IsTrans α r] : Comp r r ≤ r :=
+  fun _ _ ⟨_, hab, hbc⟩ ↦ _root_.trans hab hbc
+
+theorem swap_le_iff_le_swap {r₁ r₂ : α → α → Prop} : swap r₁ ≤ r₂ ↔ r₁ ≤ swap r₂ := by
+  constructor <;> intro h a b hab <;> exact h b a hab
+
 attribute [scoped grind] ReflGen TransGen ReflTransGen EqvGen
 
+@[scoped grind .]
+theorem ReflGen.le_reflGen : r ≤ ReflGen r := fun _ _ => ReflGen.single
+
 theorem ReflGen.to_eqvGen (h : ReflGen r a b) : EqvGen r a b :=
   EqvGen.reflGen_le_eqvGen r _ _ h
 
+@[scoped grind .]
+theorem TransGen.le_transGen : r ≤ TransGen r := fun _ _ => TransGen.single
+
 theorem TransGen.to_eqvGen (h : TransGen r a b) : EqvGen r a b :=
   EqvGen.transGen_le_eqvGen r _ _ h
 
 theorem ReflTransGen.to_eqvGen (h : ReflTransGen r a b) : EqvGen r a b :=
   EqvGen.reflTransGen_le_eqvGen r _ _ h
 
+@[scoped grind .]
+theorem SymmGen.le_symmGen : r ≤ SymmGen r := fun _ _ => Or.inl
+
 theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b :=
   EqvGen.symmGen_le_eqvGen r _ _ h
 
+@[simp, scoped grind =] theorem sup_swap_eq_symmGen : r ⊔ Function.swap r = SymmGen r := rfl
+
+@[scoped grind .]
+theorem EqvGen.le_eqvGen : r ≤ EqvGen r := EqvGen.rel
+
+theorem _root_.Equivalence.eqvGen_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) : EqvGen r₁ ≤ r₂ :=
+  have := h.isEquiv
+  EqvGen.eqvGen_le hle
+
 attribute [scoped grind →] ReflGen.to_eqvGen TransGen.to_eqvGen ReflTransGen.to_eqvGen
   SymmGen.to_eqvGen
 
-@[deprecated _root_.refl (since := "2026-09-07")]
+theorem Join.single [Std.Refl r] (h : r a b) : Join r a b := ⟨b, h, refl b⟩
+
+@[simp, scoped grind =] theorem join₂_eq_join : Join₂ r r = Join r := rfl
+
+theorem join₂_eq_comp_swap : Join₂ r₁ r₂ = Comp r₁ (swap r₂) := rfl
+
+instance [Std.Refl r₁] [Std.Refl r₂] : Std.Refl (Join₂ r₁ r₂) where
+  refl a := ⟨a, refl a, refl a⟩
+
+theorem Join₂.single_left [Std.Refl r₂] (h : r₁ a b) : Join₂ r₁ r₂ a b := ⟨b, h, refl b⟩
+
+theorem Join₂.single_right [Std.Refl r₁] (h : r₂ a b) : Join₂ r₁ r₂ b a := ⟨b, refl b, h⟩
+
+theorem Join₂.join₂_le [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) : Join₂ r₁ r₂ ≤ r :=
+  (comp_le_comp h₁ h₂).trans (comp_self_le r)
+
+theorem Join₂.swap_iff {a b : α} : Join₂ r₁ r₂ b a ↔ Join₂ r₂ r₁ a b := by grind [Join₂]
+
+protected theorem Join₂.mono (h₁ : r₁ ≤ r₁') (h₂ : r₂ ≤ r₂') : Join₂ r₁ r₂ ≤ Join₂ r₁' r₂' :=
+  fun x y ⟨z, hxz, hyz⟩ => ⟨z, h₁ x z hxz, h₂ y z hyz⟩
+
+@[deprecated _root_.refl +typeChanged (since := "2026-09-07")]
 theorem MJoin.refl (a : α) : MJoin r a a := _root_.refl a
 
-theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := by
-  use b
+@[deprecated Join.single +typeChanged (since := "2026-09-07")]
+theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := Join.single h
+
+theorem _root_.Equivalence.join_reflTransGen_le (h : Equivalence r₂) (hle : r₁ ≤ r₂) :
+    Join (ReflTransGen r₁) ≤ r₂ :=
+  have := h.isEquiv
+  join_le_of_equivalence_of_le h <| reflTransGen_le_of_le hle
+
+theorem join_reflTransGen_le_eqvGen : Join (ReflTransGen r) ≤ EqvGen r :=
+    (EqvGen.is_equivalence r).join_reflTransGen_le EqvGen.le_eqvGen
+
+theorem join₂_reflTransGen_le [Std.Refl r] [IsTrans α r] (h₁ : r₁ ≤ r) (h₂ : swap r₂ ≤ r) :
+    Join₂ (ReflTransGen r₁) (ReflTransGen r₂) ≤ r := by
+  refine Join₂.join₂_le ?_ (ReflTransGen.swap.trans ?_)
+    <;> apply reflTransGen_le_of_le <;> assumption
+
+theorem join₂_reflTransGen_le_of_isEquiv [IsEquiv α r] (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) :
+    Join₂ (ReflTransGen r₁) (ReflTransGen r₂) ≤ r :=
+  join₂_reflTransGen_le h₁ (by rwa [swap_le_iff_le_swap, Std.Symm.swap_eq])
+
+theorem _root_.Equivalence.join₂_reflTransGen_le (h : Equivalence r) (h₁ : r₁ ≤ r) (h₂ : r₂ ≤ r) :
+    Join₂ (ReflTransGen r₁) (ReflTransGen r₂) ≤ r :=
+  have := h.isEquiv
+  join₂_reflTransGen_le_of_isEquiv h₁ h₂
+
+theorem left_le_join₂_reflTransGen : r₁ ≤ Join₂ (ReflTransGen r₁) (ReflTransGen r₂) :=
+  fun _ _ h => Join₂.single_left (.single h)
+
+theorem swap_right_le_join₂_reflTransGen : swap r₂ ≤ Join₂ (ReflTransGen r₁) (ReflTransGen r₂) :=
+    fun _ _ h => Join₂.single_right (.single h)
 
 /-- If a relation is squeezed by a relation and its multi-step closure, they are multi-step equal -/
 theorem reflTransGen_mono_closed (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTransGen r₁) :
@@ -69,11 +154,27 @@ theorem reflTransGen_mono_closed (h₁ : r₁ ≤ r₂) (h₂ : r₂ ≤ ReflTra
   ext a b
   exact ⟨ReflTransGen.mono h₁ a b, reflTransGen_closed h₂ a b⟩
 
-@[deprecated Relation.ReflGen.stdSymm (since := "2026-09-03")]
+@[deprecated Relation.ReflGen.stdSymm +typeChanged (since := "2026-09-03")]
 lemma ReflGen.symmGen_symm : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a :=
   Std.Symm.symm a b
 
-@[simp, grind =]
+@[simp, scoped grind =]
 theorem reflTransGen_symmGen : ReflTransGen (SymmGen r) = EqvGen r := EqvGen.reflTransGen_symmGen r
 
+@[scoped grind <=]
+theorem join_inl (r₁_ab : r₁ a b) : (r₁ ⊔ r₂) a b :=
+  Or.inl r₁_ab
+
+@[scoped grind <=]
+theorem join_inr (r₂_ab : r₂ a b) : (r₁ ⊔ r₂) a b :=
+  Or.inr r₂_ab
+
+@[scoped grind <=]
+theorem join_inl_reflTransGen (r₁_ab : ReflTransGen r₁ a b) : ReflTransGen (r₁ ⊔ r₂) a b :=
+  ReflTransGen.mono le_sup_left _ _ r₁_ab
+
+@[scoped grind <=]
+theorem join_inr_reflTransGen (r₂_ab : ReflTransGen r₂ a b) : ReflTransGen (r₁ ⊔ r₂) a b :=
+  ReflTransGen.mono le_sup_right _ _ r₂_ab
+
 end Relation
diff --git a/Cslib/Foundations/Relation/Confluence.lean b/Cslib/Foundations/Relation/Confluence.lean
index bdfb8b8576..94b0288244 100644
--- a/Cslib/Foundations/Relation/Confluence.lean
+++ b/Cslib/Foundations/Relation/Confluence.lean
@@ -7,9 +7,9 @@ Authors: Fabrizio Montesi, Thomas Waring, Chris Henson
 module
 
 public import Cslib.Foundations.Relation.Termination
-public import Mathlib.Data.List.Pairwise
+public import Mathlib.Tactic.TFAE
 
-/-! # Relations: Confluence and Termination
+/-! # Relations: Confluence
 
 This module proves some properties regarding confluence that are used for both lambda calculi and
 combinatory logic. Some notable theorems:
@@ -17,6 +17,9 @@ combinatory logic. Some notable theorems:
 * `Diamond.to_confluent`: the diamond property implies confluence
 * `LocallyConfluent.terminating_toConfluent`: Newman's lemma
 
+We prove most results first for two relations, where `Confluent r` becomes `Commute r₁ r₂`, then
+specialize to the classical case where `r₁ = r₂`.
+
 ## References
 
 * [*Term Rewriting and All That*][Baader1998]
@@ -29,60 +32,115 @@ variable {α : Type*} {r r₁ r₂ : α → α → Prop}
 
 namespace Relation
 
+open Function ReflTransGen
+
+theorem Commute.to_confluent : Commute r r = Confluent r := rfl
+
+@[deprecated (since := "2026-09-03")] alias Commute.toConfluent := Commute.to_confluent
+
+@[simp] theorem StronglyCommute.to_stronglyConfluent :
+  StronglyCommute r r = StronglyConfluent r := rfl
+
+@[deprecated (since := "2026-09-03")] alias StronglyCommute.toStronglyConfluent :=
+  StronglyCommute.to_stronglyConfluent
+
+@[simp] theorem DiamondCommute.to_diamond : DiamondCommute r r = Diamond r := rfl
+
+@[deprecated (since := "2026-09-03")] alias DiamondCommute.toDiamond := DiamondCommute.to_diamond
+
+@[simp] theorem SemiCommute.to_semiConfluent : SemiCommute r r = SemiConfluent r := rfl
+
+@[simp] theorem LocallyCommute.to_locallyConfluent : LocallyCommute r r = LocallyConfluent r := rfl
+
+instance : Std.Symm (@DiamondCommute α) where
+  symm _ _ h _ _ _ h₁ h₂ := Join₂.swap_iff.mp <| h h₂ h₁
+
+instance : Std.Symm (@LocallyCommute α) where
+  symm _ _ h _ _ _ h₁ h₂ := Join₂.swap_iff.mp <| h h₂ h₁
+
+lemma DiamondCommute.diamond_commute_reflTransGen_right (h : DiamondCommute r₁ r₂) :
+    DiamondCommute r₁ (ReflTransGen r₂) := by
+  intro a b c h₁ h₂
+  induction h₂ using ReflTransGen.head_induction_on generalizing b with
+  | refl => exact Join₂.single_right h₁
+  | head ha _ ih =>
+    obtain ⟨d, hbd, hcd⟩ := h h₁ ha
+    obtain ⟨d', hdd', hcd'⟩ := ih hcd
+    exact ⟨d', hdd'.head hbd, hcd'⟩
+
+lemma DiamondCommute.diamond_commute_reflTransGen_left (h : DiamondCommute r₁ r₂) :
+    DiamondCommute (ReflTransGen r₁) r₂ := by
+  rw [comm (r := DiamondCommute)] at h ⊢
+  exact h.diamond_commute_reflTransGen_right
+
+lemma DiamondCommute.to_semiCommute (h : DiamondCommute r₁ r₂) : SemiCommute r₁ r₂ :=
+  fun h₁ h₂ => Join₂.mono le_rfl ReflTransGen.le_reflTransGen _ _ <|
+    h.diamond_commute_reflTransGen_right h₁ h₂
+
 /-- Extending a multistep reduction by a single step preserves multi-joinability. -/
-lemma Diamond.extend (h : Diamond r) :
-    ReflTransGen r a b → r a c → Join (ReflTransGen r) b c := by
-  intros ab ac
-  induction ab using ReflTransGen.head_induction_on generalizing c
-  case refl => exists c, .single ac
-  case head a'_c' _ ih =>
-    obtain ⟨d, cd, c'_d⟩ := h ac a'_c'
-    obtain ⟨d', b_d', d_d'⟩ := ih c'_d
-    exact ⟨d', b_d', .head cd d_d'⟩
-
-/-- The diamond property implies confluence. -/
-theorem Diamond.to_confluent (h : Diamond r) : Confluent r := by
-  intros a b c ab bc
-  induction ab using ReflTransGen.head_induction_on generalizing c
-  case refl => exists c
-  case head _ _ a'_c' _ ih =>
-    obtain ⟨d, cd, c'_d⟩ := h.extend bc a'_c'
-    obtain ⟨d', b_d', d_d'⟩ := ih c'_d
-    exact ⟨d', b_d', .trans cd d_d'⟩
+lemma Diamond.to_semiConfluent (h : Diamond r) : SemiConfluent r := DiamondCommute.to_semiCommute h
 
-@[deprecated (since := "2026-09-03")] alias Diamond.toConfluent := Diamond.to_confluent
+@[deprecated (since := "2026-09-12")] alias Diamond.extend := Diamond.to_semiConfluent
 
-theorem Confluent.to_churchRosser (h : Confluent r) : ChurchRosser r := by
-  intro x y h_eqv
-  induction h_eqv with
-  | rel _ b => exists b; grind [ReflTransGen.single]
-  | refl a => exists a
-  | symm a b _ ih => exact symm ih
-  | trans _ _ _ _ _ ih1 ih2 =>
-      obtain ⟨u, _, hbu⟩ := ih1
-      obtain ⟨v, hbv, _⟩ := ih2
-      obtain ⟨w, _, _⟩ := h hbu hbv
-      exists w
-      grind [ReflTransGen.trans]
-
-@[deprecated (since := "2026-09-03")] alias Confluent.toChurchRosser := Confluent.to_churchRosser
-
-theorem SemiConfluent.to_confluent (h : SemiConfluent r) : Confluent r := by
-  intro x y1 y2 h_xy1 h_xy2
-  induction h_xy1 with
-  | refl => use y2
-  | tail h_xz h_zy1 ih =>
-      obtain ⟨u, h_zu, _⟩ := ih
-      obtain ⟨v, _, _⟩ := h h_zu h_zy1
-      exists v
-      grind [ReflTransGen.trans]
+theorem Commute.isTrans_join₂_reflTransGen (h : Commute r₁ r₂) :
+    IsTrans α (Join₂ (ReflTransGen r₁) (ReflTransGen r₂)) where
+  trans a b c := by
+    intro ⟨d, had, hbd⟩ ⟨d', hbd', hcd'⟩
+    obtain ⟨e, he, he'⟩ := h hbd' hbd
+    exact ⟨e, had.trans he', hcd'.trans he⟩
 
-@[deprecated (since := "2026-09-03")] alias SemiConfluent.toConfluent := SemiConfluent.to_confluent
+theorem Confluent.isTrans_join_reflTransGen (h : Confluent r) : IsTrans α (Join (ReflTransGen r)) :=
+  Commute.isTrans_join₂_reflTransGen h
 
-attribute [scoped grind →] Confluent.to_churchRosser SemiConfluent.to_confluent
+theorem SemiCommute.to_commute (h : SemiCommute r₁ r₂) : Commute r₁ r₂ := by
+  intro a b₁ b₂ hab₁ hab₂
+  induction hab₁ with
+  | refl => use b₂
+  | tail hab hbb' ih =>
+    obtain ⟨d, hd, hd'⟩ := ih
+    obtain ⟨e, he, he'⟩ := h hbb' hd
+    use e, he, hd'.trans he'
+
+theorem SemiConfluent.to_confluent (h : SemiConfluent r) : Confluent r := SemiCommute.to_commute h
+
+@[deprecated (since := "2026-09-03")] alias SemiConfluent.toConfluent := SemiConfluent.to_confluent
 
-private theorem confluent_equivalents : [ChurchRosser r, SemiConfluent r, Confluent r].TFAE := by
-  grind [List.tfae_cons_cons, List.tfae_singleton]
+theorem commute_equivalents :
+    [SemiCommute r₁ r₂, Commute r₁ r₂, IsTrans α (Join₂ (ReflTransGen r₁) (ReflTransGen r₂)),
+      ReflTransGen (r₁ ⊔ swap r₂) ≤ Join₂ (ReflTransGen r₁) (ReflTransGen r₂),
+      ReflTransGen (r₁ ⊔ swap r₂) = Join₂ (ReflTransGen r₁) (ReflTransGen r₂)].TFAE := by
+  tfae_have 1 → 2 := SemiCommute.to_commute
+  tfae_have 2 → 3 := Commute.isTrans_join₂_reflTransGen
+  tfae_have 3 → 4 := fun h => reflTransGen_le_of_le <|
+    sup_le left_le_join₂_reflTransGen swap_right_le_join₂_reflTransGen
+  tfae_have 4 → 5 := fun h => h.antisymm <|
+    join₂_reflTransGen_le (le_sup_left.trans le_reflTransGen) (le_sup_right.trans le_reflTransGen)
+  tfae_have 5 → 1 := by
+    intro h a b₁ b₂ h₁ h₂
+    rw [Join₂.swap_iff, ← h]
+    exact (ReflTransGen.mono le_sup_right _ _ <| reflTransGen_swap.mpr h₂).tail (Or.inl h₁)
+  tfae_finish
+
+theorem semiCommute_iff_commute : SemiCommute r₁ r₂ ↔ Commute r₁ r₂ := commute_equivalents.out 1 2
+
+theorem DiamondCommute.to_commute (h : DiamondCommute r₁ r₂) : Commute r₁ r₂ :=
+  semiCommute_iff_commute.mp h.to_semiCommute
+
+instance : Std.Symm (@SemiCommute α) where
+  symm r₁ r₂ h := by
+    rw [semiCommute_iff_commute] at h ⊢
+    exact symm (r := Commute) h
+
+theorem churchRosser_iff_eqvGen_le_join_reflTransGen :
+    ChurchRosser r ↔ EqvGen r ≤ Join (ReflTransGen r) :=
+  Iff.rfl
+
+theorem confluent_equivalents :
+    [ChurchRosser r, SemiConfluent r, Confluent r, IsTrans α (Join (ReflTransGen r)),
+      EqvGen r ≤ Join (ReflTransGen r), EqvGen r = Join (ReflTransGen r)].TFAE := by
+  refine (List.tfae_cons ?_).mpr ⟨churchRosser_iff_eqvGen_le_join_reflTransGen, ?_⟩
+  · grind
+  · simpa [reflTransGen_symmGen] using commute_equivalents (r₁ := r) (r₂ := r)
 
 theorem semiConfluent_iff_churchRosser : SemiConfluent r ↔ ChurchRosser r :=
   List.TFAE.out confluent_equivalents 2 1
@@ -93,14 +151,22 @@ theorem semiConfluent_iff_churchRosser : SemiConfluent r ↔ ChurchRosser r :=
 theorem confluent_iff_churchRosser : Confluent r ↔ ChurchRosser r :=
   List.TFAE.out confluent_equivalents 3 1
 
+alias ⟨_, Confluent.to_churchRosser⟩ := confluent_iff_churchRosser
+
 @[deprecated (since := "2026-09-03")] alias Confluent_iff_ChurchRosser := confluent_iff_churchRosser
 
+attribute [scoped grind →] Confluent.to_churchRosser SemiConfluent.to_confluent
+
 theorem confluent_iff_semiConfluent : Confluent r ↔ SemiConfluent r :=
   List.TFAE.out confluent_equivalents 3 2
 
 @[deprecated (since := "2026-09-03")] alias Confluent_iff_SemiConfluent :=
   confluent_iff_semiConfluent
 
+theorem Diamond.to_confluent (h : Diamond r) : Confluent r := DiamondCommute.to_commute h
+
+@[deprecated (since := "2026-09-03")] alias Diamond.toConfluent := Diamond.to_confluent
+
 theorem confluent_of_unique_end {x : α} (h : ∀ y : α, ReflTransGen r y x) : Confluent r := by
   intro a b c hab hac
   exact ⟨x, h b, h c⟩
@@ -125,9 +191,8 @@ theorem Confluent.equivalence_join_reflTransGen (h : Confluent r) :
   apply equivalence_join
   grind
 
-theorem Terminating.confluent_iff_forall_unique_normal (ht : Terminating r) :
+theorem Normalizing.confluent_iff_forall_unique_normal (hn : Normalizing r) :
     Confluent r ↔ ∀ a : α, ∃! n : α, ReflTransGen r a n ∧ Normal r n := by
-  have hn : Normalizing r := ht.to_normalizing
   constructor
   · intro hc a
     apply existsUnique_of_exists_of_unique (hn a)
@@ -142,11 +207,11 @@ theorem Terminating.confluent_iff_forall_unique_normal (ht : Terminating r) :
     obtain ⟨nc, hcnc, hnc⟩ := hn c
     have hanb : (ReflTransGen r) a nb := ReflTransGen.trans hab hbnb
     have hanc : (ReflTransGen r) a nc := ReflTransGen.trans hac hcnc
-    have hnanb : nb = na := H nb ⟨hanb, hnb⟩
-    have hnanc : nc = na := H nc ⟨hanc, hnc⟩
-    rw [hnanb] at hbnb
-    rw [hnanc] at hcnc
-    exact ⟨hbnb, hcnc⟩
+    grind
+
+theorem Terminating.confluent_iff_forall_unique_normal (ht : Terminating r) :
+    Confluent r ↔ ∀ a : α, ∃! n : α, ReflTransGen r a n ∧ Normal r n :=
+  ht.to_normalizing.confluent_iff_forall_unique_normal
 
 @[deprecated (since := "2026-09-03")] alias Terminating.isConfluent_iff_all_unique_Normal :=
   Terminating.confluent_iff_forall_unique_normal
@@ -177,45 +242,28 @@ theorem Confluent.to_locallyConfluent (h : Confluent r) : LocallyConfluent r :=
 @[deprecated (since := "2026-09-03")] alias Confluent.toLocallyConfluent :=
   Confluent.to_locallyConfluent
 
-/-- Newman's lemma: a terminating, locally confluent relation is confluent. -/
-theorem LocallyConfluent.terminating_toConfluent (hlc : LocallyConfluent r) (ht : Terminating r) :
-    Confluent r := by
+theorem LocallyCommute.commute_of_terminating_sup (hlc : LocallyCommute r₁ r₂)
+    (ht : Terminating (r₁ ⊔ r₂)) : Commute r₁ r₂ := by
   intro x
   induction x using ht.induction with
   | h x ih =>
-    intro y z xy xz
-    cases xy.cases_head with
-    | inl => exists z; grind
-    | inr h =>
-      obtain ⟨y₁, x_y₁, y₁_y⟩ := h
-      cases xz.cases_head with
-      | inl => exists y; grind
-      | inr h =>
-        obtain ⟨z₁, x_z₁, z₁_z⟩ := h
-        have ⟨u, z₁_u, y₁_u⟩ := hlc x_z₁ x_y₁
-        have ⟨v, uv, yv⟩ : Join (ReflTransGen r) u y := by grind
-        have ⟨w, vw, zw⟩ : Join (ReflTransGen r) v z := by grind [ReflTransGen.trans]
-        exact ⟨w, .trans yv vw, zw⟩
+    intro y z hy hz
+    rcases hy.cases_head with (rfl | ⟨y', hy, hy'⟩)
+    · use z
+    · rcases hz.cases_head with (rfl | ⟨z', hz, hz'⟩)
+      · use y
+      · obtain ⟨u, hyu, hzu⟩ := hlc hy hz
+        obtain ⟨v, hyv, huv⟩ := ih y' (join_inl hy) hy' hyu
+        obtain ⟨w, hvw, hzw⟩ := ih z' (join_inr hz) (hzu.trans huv) hz'
+        exact ⟨w, hyv.trans hvw, hzw⟩
+
+/-- Newman's lemma: a terminating, locally confluent relation is confluent. -/
+theorem LocallyConfluent.terminating_toConfluent (hlc : LocallyConfluent r) (ht : Terminating r) :
+    Confluent r := LocallyCommute.commute_of_terminating_sup hlc ((sup_idem r).symm ▸ ht)
 
 @[deprecated (since := "2026-09-03")] alias LocallyConfluent.Terminating_toConfluent :=
   LocallyConfluent.terminating_toConfluent
 
-instance : Std.Symm (@Commute α) where
-  symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁]
-
-theorem Commute.to_confluent : Commute r r = Confluent r := rfl
-
-@[deprecated (since := "2026-09-03")] alias Commute.toConfluent := Commute.to_confluent
-
-theorem StronglyCommute.to_stronglyConfluent : StronglyCommute r r = StronglyConfluent r := rfl
-
-@[deprecated (since := "2026-09-03")] alias StronglyCommute.toStronglyConfluent :=
-  StronglyCommute.to_stronglyConfluent
-
-theorem DiamondCommute.to_diamond : DiamondCommute r r = Diamond r := by rfl
-
-@[deprecated (since := "2026-09-03")] alias DiamondCommute.toDiamond := DiamondCommute.to_diamond
-
 theorem StronglyCommute.extend (h : StronglyCommute r₁ r₂) (xy : ReflTransGen r₁ x y)
     (xz : r₂ x z) : ∃ w, ReflGen r₂ y w ∧ ReflTransGen r₁ z w := by
   induction xy with
@@ -243,37 +291,19 @@ theorem StronglyConfluent.to_confluent (h : StronglyConfluent r) : Confluent r :
 @[deprecated (since := "2026-09-03")] alias StronglyConfluent.toConfluent :=
   StronglyConfluent.to_confluent
 
-variable {r₁ r₂ : α → α → Prop}
-
-@[scoped grind <=]
-theorem join_inl (r₁_ab : r₁ a b) : (r₁ ⊔ r₂) a b :=
-  Or.inl r₁_ab
-
-@[scoped grind <=]
-theorem join_inr (r₂_ab : r₂ a b) : (r₁ ⊔ r₂) a b :=
-  Or.inr r₂_ab
-
-@[scoped grind <=]
-theorem join_inl_reflTransGen (r₁_ab : ReflTransGen r₁ a b) : ReflTransGen (r₁ ⊔ r₂) a b :=
-  ReflTransGen.mono le_sup_left _ _ r₁_ab
-
-@[scoped grind <=]
-theorem join_inr_reflTransGen (r₂_ab : ReflTransGen r₂ a b) : ReflTransGen (r₁ ⊔ r₂) a b :=
-  ReflTransGen.mono le_sup_right _ _ r₂_ab
-
 lemma Commute.join_left (c₁ : Commute r₁ r₃) (c₂ : Commute r₂ r₃) : Commute (r₁ ⊔ r₂) r₃ := by
   intro x y z xy xz
   induction xy with
-  | refl => grind
+  | refl => grind [Join₂]
   | @tail b c _ bc ih =>
     have ⟨w, bw, _⟩ := ih
     cases bc with
     | inl bc =>
       obtain ⟨_, _, _⟩ := c₁ (.single bc) bw
-      grind [ReflTransGen.trans]
+      grind [Join₂, ReflTransGen.trans]
     | inr bc =>
       obtain ⟨_, _, _⟩ := c₂ (.single bc) bw
-      grind [ReflTransGen.trans]
+      grind [Join₂, ReflTransGen.trans]
 
 theorem Commute.join_confluent (c₁ : Confluent r₁) (c₂ : Confluent r₂) (comm : Commute r₁ r₂) :
     Confluent (r₁ ⊔ r₂) := by
diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean
index 10e57bd42d..07a6980e14 100644
--- a/Cslib/Foundations/Relation/Defs.lean
+++ b/Cslib/Foundations/Relation/Defs.lean
@@ -35,8 +35,12 @@ def dom (r : α → β → Prop) : Set α := {a | ∃ b, r a b}
 /-- Codomain of a relation, aka range. -/
 def cod (r : α → β → Prop) : Set β := {b | ∃ a, r a b}
 
+/-- Generalisation of `Join` to two relations. -/
+def Join₂ (r₁ r₂ : α → α → Prop) (a b : α) : Prop := ∃ c, r₁ a c ∧ r₂ b c
+
 /-- The join of the reflexive transitive closure. This is not named in Mathlib, but see
   `#loogle Relation.Join (Relation.ReflTransGen ?r)` -/
+@[deprecated "use `Join (ReflTrasnGen ·)` instead" (since := "2026-09-12")]
 abbrev MJoin (r : α → α → Prop) := Join (ReflTransGen r)
 
 /-- The relation `r` 'up to' the relation `s`. -/
@@ -51,8 +55,8 @@ def Preserves (r : α → α → Prop) (P : α → Prop) : Prop := ∀ ⦃a b⦄
 abbrev Diamond (r : α → α → Prop) := ∀ {a b c : α}, r a b → r a c → Join r b c
 
 /-- Generalization of `Diamond` to two relations. -/
-def DiamondCommute (r₁ r₂ : α → α → Prop) :=
-  ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → ∃ z, r₂ y₁ z ∧ r₁ y₂ z
+abbrev DiamondCommute (r₁ r₂ : α → α → Prop) :=
+  ∀ {x y₁ y₂}, r₁ x y₁ → r₂ x y₂ → Join₂ r₂ r₁ y₁ y₂
 
 /-- A relation is confluent when its reflexive transitive closure has the diamond property. -/
 abbrev Confluent (r : α → α → Prop) := Diamond (ReflTransGen r)
@@ -63,7 +67,11 @@ abbrev Commute (r₁ r₂ : α → α → Prop) := DiamondCommute (ReflTransGen
 /-- A relation is semi-confluent when single and multiple steps with common origin
   are multi-joinable. -/
 abbrev SemiConfluent (r : α → α → Prop) :=
-  ∀ {x y₁ y₂}, ReflTransGen r x y₂ → r x y₁ → Join (ReflTransGen r) y₁ y₂
+  ∀ {x y₁ y₂}, r x y₁ → ReflTransGen r x y₂ → Join (ReflTransGen r) y₁ y₂
+
+/-- Generalisation of `SemiConfluent` to two relations. -/
+abbrev SemiCommute (r₁ r₂ : α → α → Prop) :=
+  ∀ {x y₁ y₂}, r₁ x y₁ → ReflTransGen r₂ x y₂ → Join₂ (ReflTransGen r₂) (ReflTransGen r₁) y₁ y₂
 
 /-- A relation has the Church Rosser property when equivalence implies multi-joinability. -/
 abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → Join (ReflTransGen r) x y
@@ -72,6 +80,10 @@ abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → Join
 abbrev LocallyConfluent (r : α → α → Prop) :=
   ∀ {a b c : α}, r a b → r a c → Join (ReflTransGen r) b c
 
+/-- Generalization of `LocallyConfluent` to two relations. -/
+def LocallyCommute (r₁ r₂ : α → α → Prop) :=
+  ∀ {a b c : α}, r₁ a b → r₂ a c → Join₂ (ReflTransGen r₂) (ReflTransGen r₁) b c
+
 /-- A relation is strongly confluent when single steps are reflexive- and multi-joinable. -/
 abbrev StronglyConfluent (r : α → α → Prop) :=
   ∀ {x y₁ y₂}, r x y₁ → r x y₂ → ∃ z, ReflGen r y₁ z ∧ ReflTransGen r y₂ z
diff --git a/Cslib/Languages/CombinatoryLogic/Basic.lean b/Cslib/Languages/CombinatoryLogic/Basic.lean
index 579fb5aa41..04488c220f 100644
--- a/Cslib/Languages/CombinatoryLogic/Basic.lean
+++ b/Cslib/Languages/CombinatoryLogic/Basic.lean
@@ -223,7 +223,7 @@ theorem Y_def (f : SKI) : (Y ⬝ f) ↠ H ⬝ f ⬝ (H ⬝ f) :=
   YPoly.toSKI_correct [f] (by simp)
 
 /-- The fixed-point property of the Y-combinator -/
-theorem Y_correct (f : SKI) : MJoin Red (Y ⬝ f) (f ⬝ (Y ⬝ f)) := by
+theorem Y_correct (f : SKI) : Join (ReflTransGen Red) (Y ⬝ f) (f ⬝ (Y ⬝ f)) := by
   use f ⬝ (H ⬝ f ⬝ (H ⬝ f))
   constructor
   · exact Trans.trans (Y_def f) (H_def f (H ⬝ f))
diff --git a/Cslib/Languages/CombinatoryLogic/Confluence.lean b/Cslib/Languages/CombinatoryLogic/Confluence.lean
index 97c48458da..a59ea5cfc5 100644
--- a/Cslib/Languages/CombinatoryLogic/Confluence.lean
+++ b/Cslib/Languages/CombinatoryLogic/Confluence.lean
@@ -16,8 +16,8 @@ This file proves the **Church-Rosser** theorem for the SKI calculus, that is, if
 `a ↠ c`, `b ↠ d` and `c ↠ d` for some term `d`. More strongly (though equivalently), we show
 that the relation of having a common reduct is transitive — in the above situation, `a` and `b`,
 and `a` and `c` have common reducts, so the result implies the same of `b` and `c`. Note that
-`MJoin Red` is symmetric (trivially) and reflexive (since `↠` is), so we in fact show that
-`MJoin Red` is an equivalence.
+`Join (ReflTransGen Red)` is symmetric (trivially) and reflexive (since `↠` is), so we in fact show
+that `Join (ReflTransGen Red)` is an equivalence.
 
 Our proof
 follows the method of Tait and Martin-Löf for the lambda calculus, as presented for instance in
@@ -33,7 +33,7 @@ reduction on the head and tail of a term.
 
 - `parallelReduction_diamond` : parallel reduction satisfies the diamond property, that is, it is
 confluent in a single step.
-- `mJoin_red_equivalence` : by a general result, the diamond property for `⭢ₚ` implies the same
+- `join_mRed_equivalence` : by a general result, the diamond property for `⭢ₚ` implies the same
 for its reflexive-transitive closure. This closure is exactly `↠`, which implies the
 **Church-Rosser** theorem as sketched above.
 -/
@@ -205,20 +205,20 @@ theorem parallelReduction_diamond : Diamond ParallelReduction := by
     case red_S => exact ⟨a ⬝ c ⬝ (b ⬝ c), .refl _, .refl _,⟩
 
 theorem join_parallelReduction_equivalence :
-    Equivalence (MJoin ParallelReduction) :=
+    Equivalence (Join (ReflTransGen ParallelReduction)) :=
   Confluent.equivalence_join_reflTransGen <| Diamond.to_confluent parallelReduction_diamond
 
 /-- The **Church-Rosser** theorem in its general form. -/
-theorem mJoin_red_equivalence : Equivalence (MJoin Red) := by
-  rw [MJoin, ←reflTransGen_parallelReduction_mRed]
+theorem join_mRed_equivalence : Equivalence (Join (ReflTransGen Red)) := by
+  rw [←reflTransGen_parallelReduction_mRed]
   exact join_parallelReduction_equivalence
 
 /-- The **Church-Rosser** theorem in the form it is usually stated. -/
 theorem MRed.diamond : Confluent Red := by
   intro a b c hab hac
-  apply mJoin_red_equivalence.trans (y := a)
-  · exact mJoin_red_equivalence.symm (MJoin.single hab)
-  · exact MJoin.single hac
+  apply join_mRed_equivalence.trans (y := a)
+  · exact join_mRed_equivalence.symm (Join.single hab)
+  · exact Join.single hac
 
 end SKI
 
diff --git a/Cslib/Languages/CombinatoryLogic/Defs.lean b/Cslib/Languages/CombinatoryLogic/Defs.lean
index 7d028d2834..ea8aedce71 100644
--- a/Cslib/Languages/CombinatoryLogic/Defs.lean
+++ b/Cslib/Languages/CombinatoryLogic/Defs.lean
@@ -113,12 +113,18 @@ lemma parallel_mRed {a a' b b' : SKI} (ha : a ↠ a') (hb : b ↠ b') :
 lemma parallel_red {a a' b b' : SKI} (ha : a ⭢ a') (hb : b ⭢ b') : (a ⬝ b) ↠ (a' ⬝ b') := by
   trans a' ⬝ b <;> grind
 
-theorem mJoin_red_head {x x' : SKI} (y : SKI) : MJoin Red x x' → MJoin Red (x ⬝ y) (x' ⬝ y)
+theorem join_mRed_head {x x' : SKI} (y : SKI) :
+    Join (ReflTransGen Red) x x' → Join (ReflTransGen Red) (x ⬝ y) (x' ⬝ y)
   | ⟨z, hz, hz'⟩ => ⟨z ⬝ y, MRed.head y hz, MRed.head y hz'⟩
 
-theorem mJoin_red_tail (x : SKI) {y y' : SKI} : MJoin Red y y' → MJoin Red (x ⬝ y) (x ⬝ y')
+@[deprecated (since := "2026-09-12")] alias mJoin_red_head := join_mRed_head
+
+theorem join_mRed_tail (x : SKI) {y y' : SKI} :
+    Join (ReflTransGen Red) y y' → Join (ReflTransGen Red) (x ⬝ y) (x ⬝ y')
   | ⟨z, hz, hz'⟩ => ⟨x ⬝ z, MRed.tail x hz, MRed.tail x hz'⟩
 
+@[deprecated (since := "2026-09-12")] alias mJoin_red_tail := join_mRed_tail
+
 end SKI
 
 end Cslib
diff --git a/Cslib/Languages/CombinatoryLogic/Evaluation.lean b/Cslib/Languages/CombinatoryLogic/Evaluation.lean
index 8971eebe84..f2fa26a80e 100644
--- a/Cslib/Languages/CombinatoryLogic/Evaluation.lean
+++ b/Cslib/Languages/CombinatoryLogic/Evaluation.lean
@@ -178,10 +178,13 @@ theorem redexFree_iff_mred_eq {x : SKI} : x.RedexFree ↔ ∀ y, (x ↠ y) ↔ x
     exact Red.ne hy (h.1 (Relation.ReflTransGen.single hy))
 
 /-- If a term has a common reduct with a normal term, it in fact reduces to that term. -/
-theorem mJoin_red_redexFree {x y : SKI} (hy : y.RedexFree) (h : MJoin Red x y) : x ↠ y :=
+theorem join_mRed_redexFree {x y : SKI} (hy : y.RedexFree) (h : Join (ReflTransGen Red) x y) :
+    x ↠ y :=
   let ⟨w, hyw, hzw⟩ := h
   (redexFree_iff_mred_eq.1 hy _ |>.1 hzw : y = w) ▸ hyw
 
+@[deprecated (since := "2026-09-12")] alias mJoin_red_redexFree := join_mRed_redexFree
+
 /-- If `x` reduces to both `y` and `z`, and `z` is not reducible, then `y` reduces to `z`. -/
 lemma confluent_redexFree {x y z : SKI} (hxy : x ↠ y) (hxz : x ↠ z) (hz : RedexFree z) : y ↠ z :=
   let ⟨w, hyw, hzw⟩ := MRed.diamond hxy hxz
@@ -195,13 +198,16 @@ lemma unique_normal_form {x y z : SKI}
   (redexFree_iff_mred_eq.1 hy _).1 (confluent_redexFree hxy hxz hz)
 
 /-- If `x` and `y` are normal and have a common reduct, then they are equal. -/
-lemma eq_of_mJoin_red_redexFree {x y : SKI} (h : MJoin Red x y)
+lemma eq_of_join_mRed_redexFree {x y : SKI} (h : Join (ReflTransGen Red) x y)
     (hx : x.RedexFree) (hy : y.RedexFree) : x = y :=
-  (redexFree_iff_mred_eq.1 hx _).1 (mJoin_red_redexFree hy h)
+  (redexFree_iff_mred_eq.1 hx _).1 (join_mRed_redexFree hy h)
+
+@[deprecated (since := "2026-09-12")] alias eq_of_mJoin_red_redexFree := eq_of_join_mRed_redexFree
+
 
 /-! ### Injectivity for datatypes -/
 
-lemma sk_nequiv : ¬ MJoin Red S K := by
+lemma sk_nequiv : ¬ Join (ReflTransGen Red) S K := by
   intro ⟨z, hsz, hkz⟩
   have hS : RedexFree S := by simp [RedexFree]
   have hK : RedexFree K := by simp [RedexFree]
@@ -210,19 +216,19 @@ lemma sk_nequiv : ¬ MJoin Red S K := by
 
 /-- Injectivity for booleans. -/
 theorem isBool_injective (x y : SKI) (u v : Bool) (hx : IsBool u x) (hy : IsBool v y)
-    (hxy : MJoin Red x y) : u = v := by
-  have h : MJoin Red (if u then S else K) (if v then S else K) := by
-    apply mJoin_red_equivalence.trans (y := x ⬝ S ⬝ K)
-    · apply mJoin_red_equivalence.symm
-      apply Relation.MJoin.single
+    (hxy : Join (ReflTransGen Red) x y) : u = v := by
+  have h : Join (ReflTransGen Red) (if u then S else K) (if v then S else K) := by
+    apply join_mRed_equivalence.trans (y := x ⬝ S ⬝ K)
+    · apply join_mRed_equivalence.symm
+      apply Relation.Join.single
       exact hx S K
-    · apply mJoin_red_equivalence.trans (y := y ⬝ S ⬝ K)
-      · exact mJoin_red_head K <| mJoin_red_head S hxy
-      · apply Relation.MJoin.single
+    · apply join_mRed_equivalence.trans (y := y ⬝ S ⬝ K)
+      · exact join_mRed_head K <| join_mRed_head S hxy
+      · apply Relation.Join.single
         exact hy S K
-  grind [sk_nequiv, mJoin_red_equivalence.symm h]
+  grind [sk_nequiv, join_mRed_equivalence.symm h]
 
-lemma TF_nequiv : ¬ MJoin Red TT FF := fun h =>
+lemma TF_nequiv : ¬ Join (ReflTransGen Red) TT FF := fun h =>
   (Bool.eq_not_self true).mp <| isBool_injective TT FF true false TT_correct FF_correct h
 
 /-- A specialisation of `Church : Nat → SKI`. -/
@@ -248,17 +254,17 @@ lemma churchK_injective : Function.Injective churchK :=
 
 /-- Injectivity for Church numerals -/
 theorem isChurch_injective (x y : SKI) (n m : Nat) (hx : IsChurch n x) (hy : IsChurch m y)
-    (hxy : MJoin Red x y) : n = m := by
-  suffices MJoin Red (churchK n) (churchK m) by
+    (hxy : Join (ReflTransGen Red) x y) : n = m := by
+  suffices Join (ReflTransGen Red) (churchK n) (churchK m) by
     apply churchK_injective
-    exact eq_of_mJoin_red_redexFree this (churchK_redexFree n) (churchK_redexFree m)
-  apply mJoin_red_equivalence.trans (y := x ⬝ K ⬝ K)
+    exact eq_of_join_mRed_redexFree this (churchK_redexFree n) (churchK_redexFree m)
+  apply join_mRed_equivalence.trans (y := x ⬝ K ⬝ K)
   · simp_rw [churchK_church]
-    exact mJoin_red_equivalence.symm <| Relation.MJoin.single (hx K K)
-  · apply mJoin_red_equivalence.trans (y := y ⬝ K ⬝ K)
-    · apply mJoin_red_head; apply mJoin_red_head; assumption
+    exact join_mRed_equivalence.symm <| Relation.Join.single (hx K K)
+  · apply join_mRed_equivalence.trans (y := y ⬝ K ⬝ K)
+    · apply join_mRed_head; apply join_mRed_head; assumption
     · simp_rw [churchK_church]
-      exact Relation.MJoin.single (hy K K)
+      exact Relation.Join.single (hy K K)
 
 /--
 **Rice's theorem**: no SKI term is a non-trivial predicate.