Théorème de la décomposition par égalité structurelle
Contexte
Pour montrer le théorème des calculs et de l'égalité structurelle, nous avons besoin de caractériser l'égalité entre deux formules au calculs terminés.
Énoncé
Variables
x,y
Conditions
- x et y sont des formules ayant leur calcul terminé
- x =s y
Conclusion
Il existe un entier n tq x = x1 +f ... +f xn et x = y1 +f ... +f yn où :
- x1 est un mot
- pour 1 ≤ k ≤ n, xk =s yk
Remarque: cela implique que x1 = y1.
Preuve
Nous allons utiliser une propriété découlant de la définition du 1-calcul : si le calcul de a +f b est terminé alors le calcul de a est terminé.
Si x est un mot, alors par définition de =s, y =x.
Sinon x est une application x1 +f x2. Par la définition de =s on voit que y est une application y1 +f y2 avec x1 =s y1 et x2 =s y2. x1 et y1 sont des calculs terminés. Donc on voit que par récurrence sur la profondeur des formules on décompose récursivement les fonctions des applications.
CQFD
@theorem