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

*To*: pvs-help@csl.sri.com*Subject*: [PVS-Help] elementary prove questions*From*: Vladimir Voevodsky <vladimir@ias.edu>*Date*: Tue, 15 Nov 2005 14:04:04 -0500*Cc*: vladimir voevodsky <vladimir@ias.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>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Hello, could you please help me with the following elementary (I hope!) questions: 1. I am looking at the theory: try1: theory begin t:type a:t end try1 When I try to typecheck I get a tcc asking me to prove that t is non- empty. On the other hand looking at the examples in the wift-tutorial (e.g. the phonebook) I got the impression that a:t would be treated as a declaration of a member in t and that it would imply rather than require that t is non-empty. 2. I am looking at the theory try2: Theory Begin t: type c: axiom exists (x: t): true a: bool = (Forall (x: t): x/=x) b: Theorem not a End try2 How can I prove the theorem? If I add a line d:t then I get (as in 1) a tcc which I can then prove using c. After that (grind) proves the theorem. But I was not able to use c directly without an explicit line saying d:t. Thank you, Vladimir.

- Prev by Date:
**Re: [PVS-Help] Cant Find new pvs script** - Next by Date:
**Re: [PVS-Help] elementary prove questions** - Prev by thread:
**Re: [PVS-Help] Using theory interpretations** - Next by thread:
**Re: [PVS-Help] elementary prove questions** - Index(es):