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

[PVS-Help] measure induction



Title: foxmail 5.0
pvs-help
 
     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).
 
 thanks you in advance.
 
 
 
 
 
                       qgxu@mail.shu.edu.cn
                       2006-03-19