Joinable elements

Joinabledef

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

Used by

Church–Rosser property
Local confluence
Semi-confluence

From Mathlib

Logic.Relation

import Conjectura.Defs.ComputerScience.Rewriting.Joinable · maintainer — open · raw source

Adapted for Conjectura from cslib, `Cslib/Foundations/Relation/Defs.lean`, split into one concept per module. Released by its authors under Apache 2.0.

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

Full credits