Rename ChurchRosser to Confluence

Minimal/ARS.lean

@@ -42,7 +42,7 @@ def DiamondProperty (r : α → α → Type u)
 
 /-- Property that if diverged in any number of steps, the results can be joined in any number of steps -/
 @[simp]
-def ChurchRosser (r : α → α → Type u)
+def Confluence (r : α → α → Type u)
   := ∀ a b c, ReflTransGen r a b → ReflTransGen r a c → Join (ReflTransGen r) b c
 
 def confluence_step
@@ -73,7 +73,7 @@ def confluence
     exact ⟨d, hbd, ReflTransGen.head hcc' hc'd⟩
 
 /-- Diamond property implies Church-Rosser -/
-def diamond_implies_church_rosser : DiamondProperty r → ChurchRosser r := by
+def diamond_implies_church_rosser : DiamondProperty r → Confluence r := by
   simp
   intros h a b c hab hac
   exact confluence h a b c hab hac

Minimal/Calculus.lean

@@ -1806,11 +1806,11 @@ def diamond_preduce : DiamondProperty PReduce
     ⟩
 
 /-- Confluence of `⇛` [KS22, Corollary 3.10], [Krivine93, Lemma 1.17] -/
-def confluence_preduce : ChurchRosser PReduce
+def confluence_preduce : Confluence PReduce
   := diamond_implies_church_rosser diamond_preduce
 
 /-- Confluence of `⇝` [KS22, Theorem 3.11] -/
-def confluence_reduce : ChurchRosser Reduce
+def confluence_reduce : Confluence Reduce
   := λ t u v tu tv =>
   let (tu', tv') := (redMany_to_parMany tu, redMany_to_parMany tv)
   let ⟨w, uw', vw'⟩ := confluence_preduce t u v tu' tv'