Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Joinable elements

Conjectura.Defs.ComputerScience.Rewriting.Joinable

/-
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 Mathlib.Logic.Relation

/-! # Joinable elements

## 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

/-- Two elements are **joinable** under `r` when some common element is reachable from both in
finitely many steps. This is the sense in which two divergent computations can reconverge. -/
def Joinable {α : Type*} (r : α → α → Prop) (a b : α) : Prop :=
  Relation.Join (Relation.ReflTransGen r) a b

end Conjectura.Rewriting