Für eine zweistellige Relation auf M
(zum Beispiel eine Ersetzungsrelation auf Term())
heißt x M eine -Normalform, falls ¬y M : (x, y).
Beachte: für passende und x kann vorkommen: