# Re: [isabelle] recdef error message talks about :000

The :000 is a variable introduced by recdef to prove termination of test. The definition looks unnecessarily complicated. Here is an alternative:
```

consts test :: "nat list => bool"

recdef test "measure(length)"
"test ([]) = True"

You could then derive your second clause:

lemma test_Cons: "test  ((discard#L)) = (EX L'. (L = L') & test L')"
by simp

```
and prove that test is the constant True function, so you could have defined test = (%x. True).
```
lemma "test xs" by (induct xs, simp_all)

```
You could alternatively use the function package to separate function definition and termination proofs.
```
Hope it helps.
Amine

Dave Cunningham wrote:
```
```I'm trying to use recdef for the first time and I'm getting error
messages I don't understand.  Here is my problem boiled down as small as
I can make it:

consts test :: "nat list => bool"
recdef test "measure(length)"
"test ([]) = True"
"test ((discard#L)) = (EX L'. (L=L') /\ test L')"

*** Proof failed.
*** ALL:000 L. length :000 < Suc (length L)
***  1. ALL:000 L. length :000 < Suc (length L)
*** 1 unsolved goal(s)!
*** The error(s) above occurred for the goal statement:
*** ALL:000 L. length :000 < Suc (length L)
*** At command "recdef".

Have no idea what :000 is, or how to make this work.  Any help
appreciated.
```
```

```

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