Théorème de l'indexation des couples égaux par calcul

Contexte

Pour faire des démonstration par récurrence sur les couples (x,y) tq x =c y, il nous faut trouver une injection de ces couples sur ℕ qui se calque sur la récurrence de la définition de =c.

Énoncé

Il existe une fonction I de l'ensemble des couples égaux par calcul vers ℕ tq si I x y = n alors on a la disjonction :

x = y et n = 0
il existe xc1 tq x →c1 xc1 et xc1 =c y et I xc1 y = n-1
il existe yc1 tq y →c1 yc1 et x =c yc1 et I x yc1 = n-1
x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1, x2 =c y2, I x1 y1 < n et I x2 y2 < n

Preuve

Soit I la fonction partant de l'ensemble des couples égaux par calcul vers ℕ : pour (x,y) un tel couple on définit I x y par :
- soit i0 défini par :

- si x = y : i0 = 0
- sinon i0 = ∞

- soit i1 défini par :

- si il existe xc1 tq x →c1 xc1 et xc1 =c y : i1 = (I xc1 y) + 1
- sinon i1 = ∞

- soit i2 défini par :

- si il existe yc1 tq y →c1 yc1 et x =c yc1 : i2 = (I x yc1) + 1
- sinon i2 = ∞

- soit i3 défini par :

- si x et y sont des applications x1 +f x2 et y1 +f y2 et que l'on a x1 =c y1 et x2 =c y2 : i3 = 1 + max (I x1 y1) (I x2 y2)
- sinon i3 = ∞

on défini I x y = min (i0,i1,i2,i3)

I étant défini par récurrence, il faut nous assurer que la définition est valide (qu'elle ne boucle pas). Comme elle est calquée sur la définition de =c, la finitude de la récursion de la propriété =c implique la finitude de la récursion de I.

Montrons les propriétés de I annoncés dans l'énoncé :

Soit x,y tq x =c y. La valeur de I x y provient de soit i0,i1,i2 ou i3.
- si c'est i0 : on a x = y et n = 0
- si c'est i1 : il existe xc1 tq x →c1 xc1 et xc1 =c y et I x y = (I xc1 y) + 1, donc I xc1 y = n-1
- si c'est i2 : similaire à i1
- si c'est i3 : x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1 et x2 =c y2 et on a n = I x y = 1 + max (I x1 y1) (I x2 y2), donc I x1 y1 < n et I x2 y2 < n

CQFD

Recherche d'une preuve

Essai 1

Si on utilise la définition suivante :

Soit I la fonction partant de l'ensemble des couples égaux par calcul vers ℕ : pour (x,y) un tel couple on définit I x y par :
- si x = y : I x y = 0
- si il existe xc1 tq x →c1 xc1 et xc1 =c y : I x y = (I xc1 y) + 1
- si il existe yc1 tq y →c1 yc1 et x =c yc1 : I x y = (I x yc1) + 1
- si x et y sont des applications x1 +f x2 et y1 +f y2 et que l'on a x1 =c y1 et x2 =c y2 : I x y = 1 + max (I x1 y1) (I x2 y2)

Le problème est que l'on peut avoir x =c y et I x y = infini, car y peut être incalculable et si on applique la dernière règle on peut boucler.
D'autre part les différents cas ne sont pas exclusifs, donc soit on indique qu'il faut les prendre dans l'ordre (par des "sinon..."), soit on les rend exclusifs. Les rendre exclusifs me parait difficile.

On peut peut-être définir I de sorte qu'il prenne les valeurs minimales des différentes voies possibles.

Nouvelle définition :