Lazi

Théorème des traces disjointes

Contexte

Pour montrer le théorème de jonction des sous-calculs il nous faut étudier quand deux calculs élémentaires s-loose au départ de SFP disjoints peuvent être déplacés par les équilibrages de sorte que leurs SFP deviennet imbriqués. Lors de l'équilibrage, les déplacements de calculs se produisent quand la sous-formules qu'ils calculent est un argument déplacé. Donc étudier les déplacements des calculs revient à étudier les déplacements des sous-formules lors des calculs. C'est pourquoi ici nous étudions si deux SFP disjoints subissent des déplacements par calcul qui les amènent à dévenir imbriqués.

Énoncé

Variables

x, c, s1, s2, l1, l2, n

Conditions

  • x est une formule
  • c est un calcul loose
  • s1 et s2 sont des SFP disjoints de x
  • lt1 est une ligne de trace de c de premier élément s1
  • lt2 est une ligne de trace de c de premier élément s2
  • n∈ℕ et n est inférieur ou égale aux longueurs de lt1 et lt2

Conclusion

Les SFP en position n de lt1 et lt2 sont disjoints.

Preuve

On le prouve par récurrence sur n. Pour n = 0 c'est vrai par les conditions. Supposons que la conclusion est vraie pour n et montrons la pour n + 1 :
Puisque lt1 et lt2 ont une taille ≥ n + 1 cela implique que leur destin au niveau n n'est pas "function" car un destin "function" arrête la ligne de trace. Hors pour les autres destins les SFP d'élément disjoints sont gardés disjoints, donc on obtient la conclusion au niveau n + 1.

@theorem