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

*To*: <pvs-help@csl.sri.com>*Subject*: really basic question*From*: Eric Klavins <klavins@cs.caltech.edu>*Date*: Mon, 21 Jan 2002 17:01:38 -0800 (PST)*Sender*: pvs-help-owner@csl.sri.com

Hi, I'm trying to prove the theorem "simple" below, but can't get it to go through. Am I missing something about what this theorem means in PVS? simple: THEORY BEGIN UNIVERSE : TYPE+ PRED : TYPE = [ UNIVERSE -> bool ] Q : VAR PRED x: VAR UNIVERSE simple: THEOREM ( ( FORALL x : Q(x) ) => ( EXISTS x : Q(x) ) ) END simple Thanks! -eric o---- | Eric Klavins | Postdoctoral Scholar Caltech Computer Science klavins@cs.caltech.edu (626)395-4858

- Prev by Date:
**Help** - Next by Date:
**Re: really basic question** - Prev by thread:
**Re: Generalizations** - Next by thread:
**Re: really basic question** - Index(es):