Lazi

Théorème de la ligne de destins en univocal

Contexte

On cherche à trouver une structure à une ligne de destins.

Énoncé

Variables

x,c,s,l

Conditions

  • x est une formule
  • c est un calcul univocal valide sur x
  • s est un SFP valide sur x
  • l est une ligne de destin de base s

Conclusion

La ligne de destin est un liste, dans l'ordre indiqué ci-dessous :

  • argument : un nombre entier quelconque
  • calculated : un nombre entier quelconque
  • function : entre 0 et 1

Preuve

Comme un SFP de destin "function" n'a pas de trace enfant, on ne peut avoir qu'au plus un "function" et il termine la liste.

Un SFP se trouvant en position de fonction ou représentant la formule entière (SFP ∅l) ne peut destin un argument. Donc après des destin "calculated" on ne peut avoir qu'éventuellement un SFP "function".

@theorem