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

*To*: Jerome <jerome@xxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] Unrecognized equality*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Tue, 24 Jun 2008 15:32:45 -0700*Cc*: pvs-help@xxxxxxxxxxx*Comments*: In-reply-to Jerome <jerome@cs.caltech.edu> message dated "Tue, 24 Jun 2008 15:25:55 -0700."*In-reply-to*: <20080624222555.GA27807@cs.caltech.edu>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <20080624222555.GA27807@cs.caltech.edu>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Jerome, This usually means that the theory instances don't actually match. Try running 'C-u M-x show-expanded-sequent' and see if that shows a difference. Regards, Sam Jerome <jerome@xxxxxxxxxxxxxx> wrote: > Does anyone know why the following doesn't produce Q.E.D in PVS? > > {-1} strict_subset?(K!1, J!1) IMPLIES > fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1)) > [-2] strict_subset?(K!1, J!1) > |------- > [1] fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1)) > > Rerunning step: (ASSERT) > Simplifying, rewriting, and recording with decision procedures, > this simplifies to: > composable : > > {-1} fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1)) > [-2] strict_subset?(K!1, J!1) > |------- > [1] fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1)) > > After I make ASSERT call I would think the proof was finished... am I > missing something? Thanks > > jerome

- Prev by Date:
**[PVS-Help] Unrecognized equality** - Next by Date:
**Re: [PVS-Help] Unrecognized equality** - Prev by thread:
**[PVS-Help] Unrecognized equality** - Next by thread:
**Re: [PVS-Help] Unrecognized equality** - Index(es):