SFP terminal pour x

Contexte

Pour une formule donnée on cherche à déterminer l'ensemble des SFP qui ne désigne pas une application (et donc qui désignent un mot si on est dans une formule sans notation).

Définition

Soit x une formule et s un SFP valide sur x, on dit que s est terminal pour x si l'endroit désigné par x dans x n'est pas une application.