[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 

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)],



How can I instantiate properly the wf_nat axiom?

Thanks in advance,

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