# [isabelle] Base case in termination proof..

```
I have the following function:

function (domintros) index:: "int â int" where
"index a = (if (a<0) then (index (a+5)) else (a mod 5))"

```
and have been trying to prove the result is always >=0 and <= 4. Ran into a bit of trouble and after some investigation found that it was because Isabelle couldn't automatically prove termination..
```
```
The intention is to prove that this condition is true for all ints, so I need to prove "â a. index_dom a".
```
Print_theorems gives the following:

index.cases: (âa. ?x = a â ?P) â ?P
index.domintros: (?a < 0 â index_dom (?a + 5)) â index_dom ?a
```
index.pelims: index ?x = ?y â index_dom ?x â (âa. ?x = a â ?y = (if a < 0 then index (a + 5) else a mod 5) â index_dom a â ?P) â ?P index.pinduct: index_dom ?a0.0 â (âa. index_dom a â (a < 0 â ?P (a + 5)) â ?P a) â ?P ?a0.0 index.psimps: index_dom ?a â index ?a = (if ?a < 0 then index (?a + 5) else ?a mod 5)
```
with which I've managed to prove this inductive rule:

lemma ddda: "index_dom a â index_dom (a-5)"
apply(induction a rule:index.pinduct)
done

```
Which is well and good for negative numbers as long as I have an appropriate base case. I'd been thinking of doing 1: index_dom (a) /\ a<5 /\ a>=0 as a base case. Can do for each individual value of a, as it's a small enough range
```2: index_dom a â index_dom (a-5) to extend over negative numbers
```
3: a >= 0 ==> index_dom a ==> index_dom a+5 to extend over positives using cyclic nature of mod operation.
```
```
The problem is that I don't see any way in the theorems that mention index_dom that I could establish index_dom 0, for example. I can assume it and succeed in calculating the result - which would be sufficient to prove to a human that it terminates for that value, but I don't know how I'd mechanise that reasoning.
```
Any clues?

--
DH

```

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