Confluence

Confluentdef

A relation is confluent when its reflexive-transitive closure has the Diamond property: any two finite rewrite sequences out of a common element can be brought back together. Confluence is what makes normal forms unique.

def Confluent {α : Type*} (r : α → α → Prop) : Prop :=
  Diamond (Relation.ReflTransGen r)

Builds on

Diamond property

Used by

Convergent relation

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