# Another Problem during a proof !

```My retrieve Function looks like:
retrDictc (d_c): Dicta = {w:Word | length(w)<length(d_c) and
(member(w,(d_c(length(w)))))}

Where Dicta is a finite_set of Word, and
Section : TYPE = finite_set[Word]
Dictc : TYPE = {d:finite_sequence[Section] | inv_Dictc(d)}

This yields a TCC:
retrDictc_TCC1: OBLIGATION
(FORALL (d_c: Dictc):
is_finite[Word]({w: Word |
length[character](w) < length(d_c)
AND (member[list[character]](w,
(finseq_appl[Section](d_c)(length[character](w)))))}));

which i have to proof !!

I tried this by a finite_sequence induction of the form:

fsinduction[T : TYPE]: THEORY
BEGIN

empty_fin_seq : TYPE = {fs: finite_sequence[T] | length(fs) = 0}
p : VAR pred[finite_sequence[T]]
e : VAR T
fs : VAR finite_sequence[T]
empty_fs : VAR empty_fin_seq

finite_sequence_induction : THEOREM
FORALL (p : pred[finseq[T]]) :
((FORALL (fs : finseq[T] | length(fs) = 0) : p(fs)) AND
(FORALL (l : nat) :
(FORALL (fs : finseq[T] | length(fs) = l)
: p(fs)) =>
(FORALL (fs : finseq[T] | length(fs) = l + 1) :
p(fs))))
IMPLIES FORALL (fs : finseq[T]) : p(fs)
END fsinduction

the proof leeds me to this subgoal:

[-1]    length(fs!1) = 1 + l!1
[-2]    (FORALL (fs: finseq[Section] | length(fs) = l!1):
inv_Dictc(fs)
IMPLIES
is_finite[Word]({w: Word |
length[character](w) < length(fs)
AND (member[list[character]](w,
(finseq_appl[Section](fs)(length[character](w)))))}))
{-3}    inv_Dictc(fs!1)
|-------
{1}    is_finite[Word]({w: Word |
length[character](w) < length(fs!1)
AND (member[list[character]](w,
(finseq_appl[Section](fs!1)(length[character](w)))))})

which i tried to proof with (inst?), this yields two subgoals.
The first one is easily proofed with (ground). But the second one looks
like:

[-1]    length(fs!1) = 1 + l!1
[-2]    inv_Dictc(fs!1)
|-------
[1]    is_finite[Word]({w: Word |
length[character](w) < length(fs!1)
AND (member[list[character]](w,
(finseq_appl[Section](fs!1)(length[character](w)))))})

Which is nearly the expression i wanted to proof at the beginning.
Can i do a workaround at this problem, by defining an AXIOM: is_finite
(retrDictc), or would this cause inconsitance ? If this is the fact, has
anyone an idea, how i can proof the above expression ?

Thanks to all

--
---------------------------------------------------------
("\''/").__..-''"`-. .         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.

```