[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Re: measure induction

>   th[N: posnat]
>  begin
>      i : var below[N]
>      f: var [below[N]-> noneg_real]
>      maxf(f,r: nonneg_real)(i): recursive  noneg_real =
>        if i = N then max(f(i),r) else maxf(f,max(f(i),r))(i+1) endif
>       measure N - i

I don't think this is correct. The typechecker should generate a TCC
that asks you to prove
FORALL (i: below[N]): i /=N IMPLIES i+1 < N   , which is obviously not
correct. How could i=N be valid if i is of type below[N]?