preuve normalisée

Pour p une preuve Lazi.0.0, on dit que p est normalisée si p est une déduction de type "proof" où la liste des déductions ne contient pas de déduction "proof".

La longueur d'une preuve normalisée est la longueur de la liste de la déduction de type "proof".

Voir aussi:

Normalisation d'une preuve lazi.0.0