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

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
   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.