# Re: [isabelle] about termination of function

```Hi,

```
```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 ...)
```
```
In fact, 2) should be

apply (relation "measure ...")

```
It is the simplest way of specifying a termination relation, by giving a function into the natural numbers, which decreases at each recursive call.
```
```
Example 1) is a bit trickier. It may help you to look at the types of the subexpressions (e.g. finite_psubset). Here, "..." must be a function that maps your function arguments into the type 'a set * nat for some 'a. These pairs are then compared with respect to the relation (finite-psubset <*lex*> less-than), which means that first the sets are compared with the strict subset relation and then the numbers are compared.
```
In other words, the relation

inv_image(finite-psubset<*lex*>less-than) (%x. (f x, g x))

is the same as

{ (x, y).  (finite (f y) & f x \<subset> f y)
| (f x = f y & g x < g y) }

```
While in the second version it is easier to see what is going on, the first version can be proved well-founded automatically, since it is built from combinators (inv_image, <*lex*>, finite_psubset, less_than) that already come with the relevant lemmas.
```
Hope this helps...

Alex

```

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