Lazi

Théorème de positionnement entre deux SFP

Contexte

On veut étudier quels sont les propriétés possibles entre deux SFP d'une formule.

Énoncé

Variables

x,s,t

Conditions

  • x est une formule
  • s et t sont des SFP valides sur x

Conclusion

On a la disjonction suivante :

  • s = t
  • s et t sont disjoints
  • s est dans un argument de t ou l'inverse
  • s est une fonction de t ou l'inverse

Preuve

Nous allons prouver que si nous ne sommes pas dans les 3 premiers cas alors nous sommes dans le quatrième :

Comme s et t ne sont pas disjoints on a s intérieur à t ou t intérieur à s. Comme s et t sont différent l'intériorité est stricte.
Supposons s strictement intérieur à t. Comme s n'est pas dans un argument de t cela signifie que, en tant que liste, la partie supplémentaire de s ne comporte pas de 1b. Donc la partie supplémentaire comporte uniquement 0b (il y en a au moins un). Donc s est une fonction de t.
Il nous reste le cas où t est strictement intérieur à s. Par le raisonnement symétrique au précédant on conclue que t est alors une fonction de s.

@theorem