# [isabelle] [Isabelle2007] Function termination measures

```Hello all,

```
I am a bit confused with function termination. In particular on the manner the sum of types for mutually recursive functions are defined.
```
```
For example consider the attached toy theory (although none of them is mutually recursive I believe they illustrate my confusion). Can someone show me how I can prove termination for the quartet t1,t2,t3,and t4 functions? I know it can be proven using lexicographic_order. However, I am more interested in proving termination via a measure function in order to additionally understand how the summation of the types is packaged together.
```
TIA,

George
```
```theory FunTerm imports Main begin

function tst1 :: "nat \<Rightarrow> nat"
and tst2 :: "nat \<Rightarrow> nat"
where
"tst1 n = (tst2 n) + 1"
| "tst2 n = n + 1"
by pat_completeness auto

fun tstMeasure :: "nat + nat => nat" where
"tstMeasure n =
(case n of Inl n1 \<Rightarrow> 1
| Inr n2 \<Rightarrow> 0
)"

termination tst1
apply(relation "measure tstMeasure")
apply(auto)
done

function tst1' :: "nat \<Rightarrow> nat"
and tst2' :: "nat \<Rightarrow> nat"
and tst3' :: "nat \<Rightarrow> nat"
where
"tst1' n = (tst2' n) + 1"
| "tst2' n = (tst3' n) + 1"
| "tst3' n = n + 1"
by pat_completeness auto

fun tstMeasure' :: "nat + nat + nat => nat" where
"tstMeasure' n =
(case n of Inl n1 \<Rightarrow> 2
| Inr n1 \<Rightarrow> (case n1 of Inl n2 \<Rightarrow> 1
| Inr n2 \<Rightarrow> 0
)
)"

termination tst1'
apply(relation "measure tstMeasure'")
apply(auto)
done

function t1 :: "nat \<Rightarrow> nat"
and t2 :: "nat \<Rightarrow> nat"
and t3 :: "nat \<Rightarrow> nat"
and t4 :: "nat \<Rightarrow> nat"
where
"t1 n = (t2 n) + 1"
| "t2 n = (t3 n) + 1"
| "t3 n = (t4 n) + 1"
| "t4 n = n + 1"
by pat_completeness auto

fun tMeasure :: "nat + nat + nat + nat \<Rightarrow> nat"
where
"tMeasure v = (case v of Inl x \<Rightarrow> 3
| Inr x \<Rightarrow> (case x of Inl y \<Rightarrow> 2
| Inr y \<Rightarrow> (case y of Inl z \<Rightarrow> 1
| Inr z \<Rightarrow> 0
)
)
)"

termination t1
apply(relation "measure tMeasure")

end
```

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