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

*To*: pvs-help@csl.sri.com*Subject*: Re: Moving existential quantifiers out over universal quantifiers*From*: Natarajan Shankar <shankar@csl.sri.com>*Date*: Fri, 01 Oct 1999 17:06:21 -0700*cc*: pvs-help@csl.sri.com*In-reply-to*: Your message of "Thu, 30 Sep 1999 15:07:08 PDT." <199909302207.PAA02125@heavengate.eng.sun.com>

Paul: You should be able to state the choice principle FORALL (P: [a -> [b -> boolean]]): (FORALL (x:a): EXISTS (y:b): P (x) (y)) IMPLIES (EXISTS (z:[a -> b]): FORALL (x:a): P (x) (z (x))) as a rewrite rule with equality instead of implies. You can then invoke it either by installing it an applying ASSERT, or manually through REWRITE. The only hitch is that when I tried it, I found a bug in the higher-order matching that would cause the match to fail. I've fixed this and it will appear in the patch file shortly. The fix, in case you need it right away is: (defun make-lambda-expr-iter (args* instance) (if (null args*) instance (make!-lambda-expr (car args*) (make-lambda-expr-iter (cdr args*) instance)))) Cheers, Shankar

**References**:**Moving existential quantifiers out over universal quantifiers***From:*Paul Loewenstein <pnl@heavengate.eng.sun.com>

- Prev by Date:
**Re: Moving existential quantifiers out over universal quantifiers** - Next by Date:
**another TCC question** - Prev by thread:
**Re: Moving existential quantifiers out over universal quantifiers** - Next by thread:
**sorry, slight slip in my query** - Index(es):