essai 2, th 2
Contexte
É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
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.