commutativité de =c
Contexte
La démonstration du théorème "Toute vérité se calcule en une égalité" utilise la commutativité de =c.
Énoncé
Conditions
x et y sont deux formules Lazi telles que x =c y
Conclusion
y =c x
Preuve
Pour prouver y =c x : il faut prouver les deux conditions.
La première
(si x ou y est calculable alors x et y sont calculables) est symétrique, donc elle reste vrai quand on échange x et y.
La deuxième
"si x et y sont calculables" est équivalent à "si y et x sont calculables" , il nous suffit donc de montrer l'équivalance pour les deux parties de la disjonction:
Cas de l'égalité
On a xc = yc, donc on a yc = xc.
Cas du split
On a pour hypothèse :
xc et yc sont des applications respectivement xc1 +f xc2 et yc1 +f yc2 où:
- xc1 =c yc1
- xc2 =c yc2
Il nous faut montrer :
- yc1 =c xc1
- yc2 =c xc2
Il est donc nécessaire d'utiliser une récurrence car on retombe sur l'hypothèse de départ.
@todo