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

[PVS-Help] measure induction

Title: foxmail 5.0
     I have a sample theory:
  th[N: posnat]
     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).
 thanks you in advance.