# [isabelle] about termination of function

Hi, I am thinking about proving termination of function. Can anyone tell me the differences between the following two:
1)
apply(relation inv_image(finite-psubset<*lex*>less-than) ...)
2) apply(measure ...)
I know the definition of measure is
definition
measure
::
"('a => nat) => ('a * 'a)set"
where
"measure == inv_image less_than"
and the definition of finite-psubset is
definition
finite_psubset
::
"('a set * 'a set) set"
where
"finite_psubset == {(A,B). A < B & finite B}"
But I hope someone can explain the detail meaning of the differences between the above two.
Thanks

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*