Lazi

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