# problem with induction

```Hi!
I have problems proving the theorem th. Thus I can't prove it, I think I
did a mistake in my specificaton.
Actually I wanted to build a finite array. The function t was intended
to manipulate the array in the way, that every book which titel doesn't
match the given string, is replaced by the constant none.
Though the functions seem right to me, i can't prove the theorem by
induction or measure-induct. Perhaps it's a totally wrong approach to
the problem, but all I want is to change a finite array.
Hopefully anyone can help me.

greetings
Chris```
```test: THEORY
BEGIN

max: posnat
range: TYPE = {x: posnat | x <= max}

book: TYPE = [# id: posnat, titel: string #]
book_array: TYPE = [range -> book]

none: book

b: VAR book
str: VAR string
ba: VAR book_array
i: VAR range

low(str, ba, i): nat = i

chg(str, ba, i): book_array =
IF ba(i)`titel /= str THEN ba WITH [(i) := none]
ELSE ba
ENDIF

rec(str, ba, i): RECURSIVE book_array =
IF i = 1 THEN chg(str, ba, i)
ELSE rec(str, chg(str, ba, i), i - 1)
ENDIF
MEASURE low

t(str, ba): book_array =
rec(str, ba, max)

th: THEOREM
ba(i) = b AND b`titel = str IMPLIES t(str, ba)(i) = b

END test

```