Сделать автоматическое завершение доказательства использования другой функции размера
Я написал функцию нестандартного размераsize2 для моего типа данных. Используя эту функцию, я могу вручную доказать завершение своей функции:
termination
apply (relation "measure (λ(a,b,c). size2 c)")
apply auto
done
Есть ли способ сделатьfun использовать мою функцию альтернативного размера для автоматического подтверждения завершения?