Diamond property

Diamonddef

A relation has the diamond property when any two single steps out of a common element can be closed by one further step from each side.

def Diamond {α : Type*} (r : α → α → Prop) : Prop :=
  ∀ ⦃a b c : α⦄, r a b → r a c → Relation.Join r b c

Used by

Confluence

From Mathlib

Logic.Relation

import Conjectura.Defs.ComputerScience.Rewriting.Diamond · 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