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 = x₁ +f ... +f x_n et x = y₁ +f ... +f y_n où :

• x₁ est un mot
• pour 1 ≤ k ≤ n, x_k =s y_k

Remarque: cela implique que x₁ = y_1.

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