Lazi

Théorème des calculs partiellement égaux

Contexte

Pour prouver le théorème de jonction des sous-calculs, nous avons besoins de faire converger les calculs, notre mesure sera l'égalité des calculs élémentaires jusqu'à un certain niveau sur les versions triées des calculs (par ordererCalc). Nous montrons ici que cela implique une convergence des formules résultants des deux calculs, où la mesure est l'égalité :

  • du nombre de NFSFP de niveau n intérieurs toutes deux à un NFSFP de niveau n-1
  • de la fonction minimale (qui est un mot) des sous-formules de niveau n-1 d'un même endroit.
Autrement dit les formules ont une structure identiques jusqu'au niveau n.

Énoncé

Variables

c, d, x, n, yc, yd

Conditions

  • n ∈ ℕ
  • x est une formule
  • c et d sont des calculs loose valides sur x
  • c = ordererCalc c
  • d = ordererCalc d
  • c et d restreints aux calculs élémentaires de niveau ≤ n sont égaux.
  • yc = calculate loose c x
  • yd = calculate loose d x

Conclusions

  1. L'ensemble des NFSFP de niveau ≤ n + 1 valides sur yc est égal à l'ensemble des NFSFP de niveau ≤ n + 1 valides sur yd.
  2. Les FSFP de niveau ≤ n terminaux pour yc sont les mêmes que pour yd.
  3. Si s est FSFP de niveau ≤ n terminal pour yc alors il désigne la même formule dans yc et yc, qui est un mot.

Preuve

Soient :

  • cd la restrictions de c aux calculs élémentaires de niveau ≤ n.
  • y = calculate loose cd x
  • cr tq c = e +ll cr
  • dr tq d = e +ll dr

Remarques :

  • cd est aussi la restrictions de d aux calculs élémentaires de niveau ≤ n.
  • Un calcul élémentaire de niveau k ne change pas l'ensemble des NFSFP valides de niveau ≤ k.
  • cr et dr ne contiennent que des calculs élémentaires de niveau > n.

Preuve de la proposition 1 :
cr et dr ne peuvent changer l'ensemble des NFSFP de niveau ≤ n + 1. Donc l'ensemble des NFSFP de niveau ≤ n + 1 valides sur e est l'ensemble des NFSFP de niveau ≤ n + 1 valides sur yc ou yd.

Preuve de la proposition 2 :
Soit s un FSFP de niveau ≤ n terminal pour yc. Soit s2, s où l'on a enlevé le dernier 0b. Soit s3, s où l'on a remplacé le dernier 0b par 1b. s2 est valide car il désigne l'application contenant la fonction désignée par s. Donc s3 est valide pour yc. s3 étant de niveau ≤ n + 1, il est aussi, d'après la proposition 1, valide sur yd. s 2 est donc valide sur yd et désigne une application, donc s est valide sur yd. s est terminal sur yd, sinon s +le 1b serait un NFSFP de niveau n+1 valide de yd et donc par la proposition 1 il serait valide sur yc, ce qui est contradictoire avec le fait que s est terminal sur yc.
Nous avons démontrer l'implication dans un sens, par symétrie du théorème entre c et d, on déduit l'implication dans l'autre sens. On a donc égalité des ensembles.

Preuve de la proposition 3 :
Les FSFP de niveau ≤ n terminaux ne sont pas inclus ni ne contiennent de NFSFP de niveau > n, les endroits désignés ne peuvent donc pas être modifiés par cr et dr. Donc ces endroits ont la même valeur dans e,yc et yd. Ces valeurs sont des mots car un FSFP terminal désigne pas une application.

@theorem