Lazi

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
alors on définit Icp x y = Ice x xy + Ice y xy

@theorem