Lazi

ordre par niveau sur les SFP

Contexte

Nous voulons définir un ordre total, ce qui peut être utile par exemple pour les démonstrations par récurrence. La notion de niveau, qui correspond à la notion traditionnelle d'argument, est utile dans les calculs car elle correspond à des endroit isolés les uns des autres : des calculs sur des FSP différents et de même niveau sont isolés.

Définition

Soit s et t deux SFP. s est plus grand ou égal par niveau que t ssi on a la disjonction :

  • Le niveau de s est strictement plus grand que le niveau de t.
  • s et t ont le même niveau et s est plus grand ou égal à t par l'ordre lexicographique