Théorème d'index de →c=

Contexte

Pour faire des preuves par récurrence sur →c=, nous définissons une fonction entre les couples de formules vérifiant la relation et ℕ.

Énoncé

Il existe une fonction Ice allant des couples vérifiant la relation →c= vers ℕ tq :

• si x = y alors Ice x y = 0
• si x →c1 xc1 alors Ice x xc1 = 1
• si x →c= y et y →c= z alors : Ice x z = Ice x y + Ice y z

Preuve

Soit x,y tq x →c= y. On définit Ice x y par:

• si x = y, Ice x y = 0
• sinon Ice x y = 1 + Ice (1calculate x) y

Le calcul par →c= est linéaire car c'est l'application en boucle de 1calculate. Un calcul bouclant peut passer plusieurs fois par la même valeur, mais la définition de Ice s'arrête à la première valeur correspondant. C'est pourquoi Ice est bien défini et les propriétés en découlent.

@theorem