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