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

*To*: pvs-help@csl.sri.com*Subject*: "<" on a subset of nat is well_founded*From*: Mauro Gargano <mauro@wjpserver.cs.uni-sb.de>*Date*: Wed, 12 Feb 2003 17:15:32 +0100*Sender*: pvs-help-owner@csl.sri.com*User-Agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.2) Gecko/20021120 Netscape/7.01

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 ---------------------------------------------------------------------------

- Prev by Date:
**Re: intersection, implication, predicate problem, specific example problem** - Next by Date:
**Dependent types lost in reduce combinators** - Prev by thread:
**Dependent types lost in reduce combinators** - Next by thread:
**Re: "<" on a subset of nat is well_founded** - Index(es):