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.