ну. reduceToNF, насколько я понимаю, обнаружит этот случай и остановится. То есть, результат работы reduceToNF не всегда NF. Ладно, но другие термы тоже могут не иметь NF, но редуцироваться в термы, которые не равны терму на предыдущем или следующем шаге редукции, и, в частности, повесят проверялку.