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 ℕ. Nous l'utiliserons pour prouver le théorème =c est une relation d'équivalence.
Énoncé
Il existe une fonction Icp allant des couples vérifiant la relation →c+= et ℕ tq :
- si x →c= y alors Icp x y = Ice x y
- sinon, si il existe a1,a2,y1,y2 vérifiant la deuxième condition de la disjonction définissant →c+ et tq Ice x (a1 +f a2) soit minimal. Alors Icp x y = Ice x (a1 +f a2) + Icp a1 y1 + Icp a2 y2
Preuve
On définit Icp x y par :
Soit xy tq :
- x →c+⁼ xy
- y→c+⁼ xy
- Ice x xy + Ice y xy soit minimal
@theorem