Lazi

Se calcul implique égal par calcul

Contexte

Théorème de base sur la relation entre le calcul (→c) et l'égalité par calcul (=c).

Énoncé

Variables

x, y

Conditions

  • x et y sont des formules
  • x →c y ou y →c x

Conclusion

x =c y

Preuve

Reprenons la définition de =c.

Montrons d'abord que si x ou y est calculable alors x et y sont calculables: il suffit d'appliquer le théorème "Se calcul et calculabilité".

Si x et y sont calculables, soit xc et yc les résultats de leur calcul respectif. On a xc = yc (pour la preuve, voir la démonstration de "Se calcul et calculabilité").

Donc x =c y.