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

*To*: John Rushby <RUSHBY@csl.sri.com>*Subject*: Re: What have I missed ? (a proof failed)*From*: Natarajan Shankar <shankar@csl.sri.com>*Date*: Wed, 06 May 1998 12:07:38 -0700*cc*: yechiel@cs.technion.ac.il, pvs-help@csl.sri.com*In-reply-to*: Your message of "Wed, 06 May 1998 10:01:47 PDT." <894474107.0.RUSHBY@csl.sri.com>

Yechiel: Here's some more information to add to what has already been said in response to your query. 1. As John Hoffman noted, the axiom is false, as is the theorem. 2. The axiom is a well-formed rewrite rule: it rewrites s = st to TRUE when size(s) = size(st) and (FORALL i: (i < size(s) => lmnts(s)(i) = lmnts(st)(i))). A well-formed rewrite rule is one which is of the form H => l = r or its universal closure (with H possibly empty), where the free variables in H and r are a subset of those in l. In this case, l is s = st and r is TRUE. 3. The reason it doesn't get rewritten is that the simplifier does not have the smarts to simplify the universally quantified hypothesis to TRUE. The simplifier might be strengthened to do this in a future patch release. 4. If rewrite rules (say "equal_ax" and "equal_ax2") appear to not have been triggered, then give the proof command (track-rewrite "equal_ax" "equal_ax2") before invoking assert or grind. This displays the reason why the rewrite rule wasn't triggered. -Shankar

**References**:**Re: What have I missed ? (a proof failed)***From:*John Rushby <RUSHBY@csl.sri.com>

- Prev by Date:
**Re: What have I missed ? (a proof failed)** - Next by Date:
**Help with choose and epsilon** - Prev by thread:
**Re: What have I missed ? (a proof failed)** - Next by thread:
**Re: What have I missed ? (a proof failed)** - Index(es):