Le prédicat subst(S,T,TS) réussit si TS est le résultat de l'application de la substitution S au terme T.
Lorsque la partie droite d'une règle de réécriture est une variable non instanciée, le résultat de la substitution est la variable originale et non sa copie. Dans les autres cas, on travaille sur une copie de la règle pour éviter de modifier la substitution (en la sur-instanciant).