Semi-confluence

SemiConfluentdef

A relation is semi-confluent when a single step and a finite sequence out of a common element are always Joinable. An intermediate notion between local confluence and confluence, and equivalent to Confluent.

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

Builds on

Joinable elements

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