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.