Théorème de recomposition par égalité structurelle
Contexte
Pour montrer le théorème des calculs et de l'égalité structurelle, nous avons besoin de prouver une égalité structurelle dans un cas simple où le calcul de la formule global est terminé.
Énoncé
Variables
- n, un entier >1
- x1,...,xn
- y1,...,yn
Conditions
- x1,...,xn et y1,...,yn sont des formules
- pour 1 ≤ k ≤ n xk =s yk
- les calculs de x1 +f ... +f xn et y1 +f ... +f yn sont terminés
Conclusion
x1 +f ... +f xn =s y1 +f ... +f yn
Preuve
Comme les calculs des formules globales sont terminés, les calculs de x1 +f ... +f xk et y1 +f ... +f yk sont terminés pour 1 ≤ k ≤ n.
Par la définition de =s, on a x1 +f x2 =s y1 +f y2.
x1 +f x2 et y1 +f y2 sont des calculs terminés. On voit qu'en appliquant une récurrence au arrive à la conclusion.
@theorem