# Correct use of reduce_nat

```I have diefined a Datatype for the Dictionary Problem.

BEGIN

empty: emptydict?

Now this Datatype produces this 2 reduce_nat functions:

reduce_nat(emptydict?_fun: nat, nonemptydict?_fun: [[bool, [Letter ->
nat]] -> nat]): [dictadt -> nat] =
empty: emptydict?_fun,
cons(cons1_var, cons2_var):
nonemptydict?_fun(cons1_var,
LAMBDA (x: Letter):
reduce_nat(emptydict?_fun,

nonemptydict?_fun)(cons2_var(x)))
ENDCASES;

[[bool, [Letter -> nat], dictadt] -> nat]):
cons(cons1_var, cons2_var):
nonemptydict?_fun(cons1_var,
LAMBDA (x: Letter):
REDUCE_nat(emptydict?_fun,

nonemptydict?_fun)(cons2_var(x)),
ENDCASES;

How can i use one of this function as a measure function ??
I tried the folowing:

retrDictd (d:dictd): RECURSIVE 	Dicta =
CASES d OF
empty: emptyset,
cons(eow,m): {w:Word | FORALL (l:Letter| member(l,dom(m))):
ENDCASES
MEASURE LET a = (LAMBDA (l:Letter),(n:nat): n + 1) IN
reduce_nat(0, (lambda (b:bool),LAMBDA (l:Letter),(n:nat): n + 1))

But it didnŽ t work ! I know that this function is still not correct
because it wonŽ t produce a Dicta (= set [Word]) but first of all i want
to solve the problem of the measure function !!

PS.: thanks to all who helped me so far !! ( Thanks Thanks )
--
---------------------------------------------------------
("\''/").__..-''"`-. .         Gernot Lepuschitz
`9_ 9  )   `-. (    ).`-._.`)gernot@sbox.tu-graz.ac.at
(_Y_.)' ._   ) `._`.  " -.-'   Telematik - Student
..`-'_..-_/ /-'_.'/               TU - Graz
(l)-'' ((i).' ((!.'
In the softwarerequirements they said Win95 or better
so I installed Linux.

```