Пример: гипотеза Коллатца

Следующая функция всюду вычислима и всегда возвращает 0.

(defun collatz (n)
  (cond ((<= n 1) 0)
        ((evenp n) (collatz (/ n 2)))   ; n чётное
        (t (collatz (1+ (* 3 n))))))    ; n нечётное

Если бы предикат экстенсионального равенства fun-equal существовал, то вызов

(fun-equal #'collatz (constantly 0))

подтвердил бы гипотезу Коллатца!