# [isabelle] how to proof termination in "function" command?

```hello,
I try to define a funciton:

Premise xs:: nat list

lists(i,j,xs) =  [ ]                               (if j≥size xs)

ists(i,j,xs) =   [ ]                         (if j<size xs and i>j)

lists(i,j,xs) =  (∑k:i≤k≤j xs[i])#lists(i+1.j,xs)

(if j<size xs and i≤j)

Firstly, i use "fun" command, but it fails.
so ,i try to define this function using "function" command.
In order to proof the completeness and compatibilitiy ,i use the method  "pat_completeness" and method "auto".
However, in the process of proofing termination,  method "lexicographic_order" can't work, because the variable i get greater in every step. hence, i choose the method

apply (relation "measure (\<lambda>(i,j). j + 1 - i)"), because j+1-i get smaller in every step.  it still fails, and i don't know where is the promble. the following are my theory file:

----------------------------------------------

theory minsum
imports Main
begin

fun sum :: "nat \<Rightarrow> nat  \<Rightarrow> nat list \<Rightarrow> nat"
where
"sum i j xs = (if j\<ge>size xs then 0 else (if i>j then 0 else (\<Sum>k\<in>{i..<Suc j}. (xs !k))))"

function lists::  "nat \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat list"
where
"lists i j xs =(if j\<ge>size xs then [] else ( if i>j then [] else (sum i j xs)#(lists (Suc i) j xs) ))"
by pat_completeness auto
termination
apply (relation "measure (\<lambda>(i,j). j + 1 - i)")  ??????????

end

need help!
Thank you in advance for any help on this.

yucy```

Attachment: testletter.thy
Description: Binary data

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