# Re: [PVS-Help] measure induction

```
I've corrected the theory so that it typechecks.

th[N: posnat]: THEORY
BEGIN
i, j : var below[N]
f: var [below[N]-> nonneg_real]
r: VAR nonneg_real

maxf(f,r)(i): recursive  nonneg_real =
if i = N-1 then max(f(i),r) else maxf(f,max(f(i),r))(i+1) endif
measure N - i

max_test: conjecture  (j<= i OR f(i)<= r) => f(i) <= maxf(f,r)(j)

END th

Note that you have to generalize the statement replacing parameters
like 0 with variables in order for the induction to work.
Once you do this, it is proved using
(measure-induct-and-simplify "N-j" ("j") :expand "maxf")

-Shankar

>      I have a sample theory:
>
>   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
>    max_test: conjecture  f(i) <= maxf(f,0)(0)
>
>    end th
>
>
>   I think the conjecture "max_test" must hold on, but how can I prove it?
>
>  I generalize the parameter "N" and (induct "N"), but the subgoal require me to prove
>
>   f(i) <= maxf(f,f(0))(1).
>
>  If I give the concrete parameter, for instance 3, to instance "N", and the max_test can be proved using (grind).
>