Automatischen Terminierungsnachweis erstellen, andere Größenfunktion verwenden

Ich habe eine benutzerdefinierte Größenfunktion geschriebensize2 für meinen Datentyp. Mit dieser Funktion kann ich die Beendigung meiner Funktion manuell nachweisen:

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

Gibt es eine Möglichkeit, @ zu machfun Meine alternative Größenfunktion für den automatischen Terminierungsnachweis verwenden?