Théorème du calcul semi-terminé
Contexte
On cherche à déduire des vérités dans le cas d'une égalité par calcul ou une fonction minimale de l'un des membres ne permet pas de calcul (donc si c'est autre chose que if ou distribute).
Énoncé
Variables
x, y1, ... , yn
Conditions
- x =c (y1 +f ... +f yn)
- y1 est un mot différent de "if" et "distribute"
Conclusion
Il existe des formules z2,....,zn tq :
- x →c[univocal] (y1 +f z2 +f ... +f zn)
- pour tout k tq 2 ≤ k ≤ n on a yk →c[loose] zk.
Preuve
Par définition de =c, il existe des calculs c et d et il existe une formule z tq :
- calculate loose c x = z
- calculate loose d (y1 +f ... +f yn) = z
Du fait que y1 est un mot différent de "if" et "distribute" d ne peut contenir des calculs élémentaires de niveau 0. Donc les calculs élémentaires de d sont à l'intérieur des arguments y2 ... yn. Donc le calcul est constitué de n - 1 calculs indépendants sur les arguments y2...yn. Donc z est de la forme y1 +f z2 +f ... +f zn où pour tout k tq 2 ≤ k ≤ n on a yk →c[loose] zk.
On a donc calculate loose c x = y1 +f z2 +f ... +f zn
@theorem