Lazi

essai 2, th 2

Contexte

Voir Essai 2

Énoncé

Définitions locales

Soit R la relation définie sur les formules : R x y ssi on a la disjonction :

  • x et y sont calculables et ont le même résultat de calcul.
  • x et y sont incalculables.

Soit =c la relation définie sur les formules par : x =c y ssi on a la disjonction :

  • R x y
  • x, y sont des applications x1 +f x2, y1 +f y2 et x1 =c y1 et x2 =c y2

Conclusion

=c est une relation d'équivalence

Étude

Recherche d'une preuve

Preuve

Réflexivité

Pour x une formule, on a R x x, donc on a x =c x

Symétrie

Nous prouvons la propriété par récurrence sur la profondeur maximale des formules en argument de =c :

Si la profondeur maximale est 1

Soit x, y deux formules de profondeur maximale 1 telles que x =c y.

Comme x et y sont de profondeur 1, il est impossible que x et y soient des applications, donc on a R x y. Comme R est une relation d'équivalence, on a R y x donc y =c x.

Si la profondeur maximale est n+1 et la symétrie prouvée pour la profondeur maximale n

Soit x, y deux formules de profondeur maximale n+1 telles que x =c y.

Si on a R x y, comme R est une relation d'équivalence, on a R y x donc y =c x.

Sinon x et y sont des applications x1 +f x2, y1 +f y2 et x1 =c y1 et x2 =c y2. Comme x1,x2,y1,y2 sont de profondeur maximale n, par récurrence on a y1 =c x1 et y2 =c x2. Donc on a y1 +f y2 =c x1 +f x2, donc on a y =c x.

Transitivité

Nous prouvons la propriété par récurrence sur la profondeur maximale des formules en argument de =c :

Si la profondeur maximale est 1

Soit 3 formules x,y et z tq x =c y et y =c z.

Comme x, y, z sont de profondeur 1, il est impossible que x,y ou z soient des applications, donc on a R x y et R y z. Comme R est une relation d'équivalence, on a R x z, et donc on a x =c z.

Si la profondeur maximale est n+1 et la symétrie prouvée pour la profondeur maximale n

Soit x, y, z des formules de profondeur maximale n+1 telles que x =c y et y =c z.

Si on a R x y et R y z : comme R est une relation d'équivalence, on a R x z, et donc on a x =c z.

Si on a R x y et si y, z sont des applications y1 +f y2, z1 +f z2 tq y1 =c z1 et y2 =c z2.