Normal form

Normaldef

An element is in normal form when no rewrite step applies to it, i.e. it is not Reducible. Normal forms are the possible end points of a computation.

def Normal {α : Type*} (r : α → α → Prop) (x : α) : Prop := ¬ Reducible r x

Builds on

Reducible element

Used by

Normalizing element

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