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

*To*: pvs-help@csl.sri.com*Subject*: higher order sub-term rewriting*From*: Mamoun FILALI-AMINE <filali@irit.fr>*Date*: Fri, 06 Mar 1998 20:15:04 +0100*Organization*: IRIT*Sender*: filali@irit.fr

We have got a problem to apply a higher order rewrite on a subterm: {-1} (FORALL (P: pred[below(N)]): (FORALL (x: below(N)): P(x)) = (FORALL (x: below(N)): P(p!1(x)))) |------- [1] EXISTS (x1: below(N)): FORALL (x2: below(N)): EXISTS (x3: below(N)): P!1((x1 = x2), (x1 = x3), (f!1(x2) = f!1(x3))) Is it possible to rewrite the goal using the hypothesis. Note that such a rewrite is possible within the HOL system, thanks to higher order rewriting. Thanks for any help.

- Prev by Date:
**Re: higher order sub-term rewriting** - Next by Date:
**RE: PVS Installation question** - Prev by thread:
**Re: higher order sub-term rewriting** - Next by thread:
**PVS Installation question** - Index(es):