Lazi

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