Théorème =c est une relation d'équivalence
Contexte
Pour prouver le théorème "toute vérité lazi.0.0 se calcule en une égalité", nous avons besoin de la transitivité de =c.
Énoncé
=c est une relation d'équivalence
Preuve
Réflexivité
Pour x une formule, x =c x car x →c[loose]= x.
Symétrie
La définition de =c est symétrique, donc la relation l'est.
Transitivité
Soit x,y,z tq x =c y et y =c z.
Soit xy et yz tq :
- x →c[loose]= xy
- y →c[loose]= xy
- y →c[loose]= xz
- z →c[loose]= xz
D'après le théorème de jonction des sous-calculs, il existe xyz tq xy →c[loose]= xyz et yz →c[loose]= xyz. Comme →c[loose]= est transitif, on a x →c[loose]= xyz et z →c[loose]= xyz. Donc x =c z.