Help with finding minimum in an array recursively

```
Hello,

I tried to find out the minimum in an array recursively but am facing
problems. Could someone help me out with this.

I am sending the pvs code and the tcc generated.

Nikhil

-------------PVS CODE------------------------------------

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% math resolution to find min in array of real numbers
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

lower, upper, current: VAR posnat
Sequence: TYPE = ARRAY[nat -> real]
TypeSeq: VAR Sequence
lowerupperAX: AXIOM lower <= upper

RecSeqMin(TypeSeq,lower,current,upper):RECURSIVE nat = if (current <
upper) then RecSeqMin(TypeSeq,if TypeSeq(current+1) < TypeSeq(lower)THEN current+1
ELSE
lower ENDIF,current+1,upper) ELSE lower ENDIF

MEASURE lower

%basic function to be called
SeqMin(TypeSeq, lower, upper): real = TypeSeq(RecSeqMin(TypeSeq,lower,lower,upper))

-----------------------TCC generated----------------------------
% Termination TCC generated (at line 52, column 82) for
% RecSeqMin(TypeSeq,
%           IF TypeSeq(current + 1) < TypeSeq(lower)
%             THEN current + 1
%           ELSE lower
%           ENDIF,
%           current + 1, upper)
% unfinished
RecSeqMin_TCC1: OBLIGATION
FORALL (TypeSeq: Sequence, current: posnat, lower: posnat,
upper: posnat):
(current < upper) IMPLIES
IF TypeSeq(current + 1) < TypeSeq(lower)
THEN current + 1
ELSE lower
ENDIF
< lower;

```