Я написал функцию нестандартного размера size2 для своего типа данных. Используя эту функцию, я могу вручную доказать прекращение моей функции:
termination
apply (relation "measure (λ(a,b,c). size2 c)")
apply auto
done
Есть ли способ заставить fun использовать мою функцию альтернативного размера для подтверждения автоматического завершения?
Функцию f можно зарегистрировать как функцию меры для средства доказательства завершения, объявив лемму is_measure f с атрибутом measure_function. В вашем случае это выглядит следующим образом.
lemma is_measure_size2 [measure_function]: "is_measure size2" ..
Затем lexicographic_order, который использует fun, и size_change попробуйте size2 тоже.
