Сделать автоматическое доказательство завершения использования другой размер функции

Question

Я написал функцию нестандартного размера size2 для моего типа данных. Используя эту функцию, я могу вручную доказать завершение своей функции:

termination 
apply (relation "measure (λ(a,b,c). size2 c)")
apply auto
done

Есть ли способ сделать fun использовать мою функцию альтернативного размера для автоматического подтверждения завершения?

Answer 1

Функция f можно зарегистрировать как функцию измерения для средства проверки завершения, объявив лемму is_measure f с атрибутом measure_function, В вашем случае это выглядит следующим образом.

lemma is_measure_size2 [measure_function]: "is_measure size2" ..

Затем, lexicographic_order, который fun использует и size_change пытаться size2, тоже.