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

"<" on a subset of nat is well_founded



  Hi everybody,

I want to do an induction proof starting from the index "i!1+2" so
I used the induction scheme (induct "j" :name 
"wf_induction[upfrom(i!1+2),<]")

but I cannot get rid of the subgoal in which PVS asks me to show that 
the "<" is wellfounded on the set upfrom(i!1 + 2):

|-------

[1]   well_founded?[upfrom(i!1 + 2)]

         (restrict[[real, real], [upfrom(i!1 + 2), upfrom(i!1 + 2)],

                   boolean]

              (<))


How can I instantiate properly the wf_nat axiom?




Thanks in advance,
Mauro.


-- 
---------------------------------------------------------------------------
  Mauro Gargano
  University of Saarland, Saarbruecken, DE
  Computer Architecture and Parallel Computing
  building 45, room 320                            mauro@wjp.cs.uni-sb.de
---------------------------------------------------------------------------