[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.