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, y₁, ... , y_n

Conditions

• x =c (y₁ +f ... +f y_n)
• y₁ est un mot différent de "if" et "distribute"

Conclusion

Il existe des formules z₂,....,z_n tq :

• x →c[univocal] (y₁ +f z₂ +f ... +f z_n)
• pour tout k tq 2 ≤ k ≤ n on a y_k →c[loose] z_k.

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