Church–Rosser property

Conjectura.Defs.ComputerScience.Rewriting.ChurchRosser

/-
Copyright (c) 2025 Fabrizio Montesi and Thomas Waring. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Fabrizio Montesi, Thomas Waring, Chris Henson
-/

import Conjectura.Defs.ComputerScience.Rewriting.Joinable

/-! # Church–Rosser property

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), `Cslib/Foundations/Relation/Defs.lean`, split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Rewriting

/-- A relation has the **Church–Rosser property** when any two elements connected by the
equivalence it generates are `Joinable`. Equivalently: provable equality can always be decided
by rewriting both sides. -/
def ChurchRosser {α : Type*} (r : α → α → Prop) : Prop :=
  ∀ ⦃a b : α⦄, Relation.EqvGen r a b → Joinable r a b

end Conjectura.Rewriting