Termination
Terminatingdef
A relation is terminating (strongly normalizing) when it admits no infinite rewrite sequence — formally, when the reversed relation is well-founded.
def Terminating {α : Type*} (r : α → α → Prop) : Prop :=
WellFounded (fun a b => r b a)Used by
From Mathlib
import Conjectura.Defs.ComputerScience.Rewriting.Terminating · 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