Lazi

x égal par calcul à y (ou x =c y)

Contexte

Nous définissons ici une relation plus large qui sera, tout en restant syntaxique, proche de l'égalité sémantique : deux formules sont égales par calcul si il existe deux calculs loose sur les deux formules aboutissent à une même formule.

Définition

Pour x et y deux formules, x =c y ssi il existe des calculs c et d tq calculate loose c x = calculate loose d y