Normalizing element

Normalizingdef

An element is normalizing when at least one finite rewrite sequence starting from it reaches a Normal form. It may still have other, non-terminating sequences.

def Normalizing {α : Type*} (r : α → α → Prop) (x : α) : Prop :=
  ∃ y, Relation.ReflTransGen r x y ∧ Normal r y

Builds on

Normal form

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