Lazi

Théorème d'égalité des arguments pour un calcul terminé

Contexte

On a des résultats sur le calcul loose (comme "Théorème toute vérité lazi.0.0 se calcule en une égalité") que l'on peut traduire en calcul univoque dans certaines circonstances.

Énoncé

Variables

x, y, y1,...,yn, n

Conditions

  • n∈ℕ*
  • le calcul de y est terminé
  • y = y1 +f ... +f yn
  • y1 est un mot.
  • x =c y

Conclusion

Il existe des formules z2, ..., zn tq x →c[univocal] y1 +f z2 +f ... +f zn et pour tout k tq 2 ≤ k ≤ n on a zk =c yk .

Preuve

Comme x =c y, il existe c et d tq calculate loose c x = calculate loose d y.

D'après le théorème du calcul trié il existe un calcul ct trié équivalent à c. Soit ct0 la troncature de ct aux calculs élémentaires de niveau 0 et ctr le reste. On a donc ct = ct0 +ll ctr.

Comme le caclul univocal de y est terminé, d ne peut comporter de calcul élémentaire de niveau 0, donc la fonction minimale de y reste y1 tout au long du calcul, qui ne porte que sur les arguments.

On a calculate loose d y = calculate loose c x = calculate loose ct x = calculate loose ctr \ calculate loose ct0 x

Soit z = calculate loose ct0 x.
Comme d et ctr ne portent que sur les arguments, et comme un calcul élémentaire ne peut porter que sur un argument à la fois, on peut décomposer les calculs d et ctr en cacluls ne portant que sur un des arguments. Donc il existe z2, ..., zn tq z = y1 +f z2 +f ... +f zn et t pour tout k tq 2 ≤ k ≤ n on a zk =c yk .