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