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

RE: [PVS-Help] finite sets TCC



Hello,

I'm sorry, I made a mistake. The TCCs are still generated but I wasn't asked to prove them immediately. I have included the source code. While typechecking you will see that about 20 TCCs are generated and have to be proven. Most of them are about the "is_finite" subject. The TCC I told you about is one of the TCCs generated by lemma le_setC61. I hope you can help me.

Thanks in advance.

Best regards,
Thijs


-----Original Message-----
From:	Kuijpers, T.J.H.
Sent:	Thu 6/23/2005 7:04 PM
To:	Hendrik Tews
Cc:	
Subject:	RE: [PVS-Help] finite sets TCC
Hello Hendrik,

Thank you for your reply.

At this moment I do not get the tccs anymore, no idea why not.
First I used (name) to rename parts, so I had to prove that if A implies B and v.v. it can be concluded that A = B. After using (name) I got the TCCs. When I do not use (name) but just (grind) at the large formulas, it works well. Sometimes this won't work, therefore I started to rename the parts. Can you explain why I get TCCs after using (name)? 

If I get this problem again for larger formules where (grind) doesn't work, I will sent another mail with some source code attached.

best regards,
Thijs

-----Original Message-----
From:	Hendrik Tews [mailto:tews@tcs.inf.tu-dresden.de]
Sent:	Thu 6/23/2005 3:58 PM
To:	Kuijpers, T.J.H.
Cc:	pvs-help@csl.sri.com
Subject:	Re: [PVS-Help] finite sets TCC
Kuijpers, T.J.H. writes:
   From: "Kuijpers, T.J.H." <t.j.h.kuijpers@student.tue.nl>
   Date: Thu, 23 Jun 2005 10:48:31 +0200
   Subject: [PVS-Help] finite sets TCC
   
   Hello,
   
   I get a TCC which I don't know how to prove. I hope you can help me.

_Please_ post a piece of PVS code that I can typecheck. Best in an
attachment or post a URL where I can download it (if it is
large). Without this it is very difficult to find the problem. 


   I want to prove the following:
   
   	tr1!1`s = tr2!1`s
   |-----------------------------
   	FORALL (res:R): is_finite[M] (s3(ss,ds)(tr1!1,tr2!1)`ms(res))
   
Looks like it depends on what tr1!1:setC_el and M is.

Bye,

Hendrik




confluence.pvs