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

Re: [PVS-Help] question regarding a dependent TCC

Thanks a lot for your quick response.i'll look through my spec again more 
closely to see what might be wrong.



>From: Hendrik Tews <tews@tcs.inf.tu-dresden.de>
>To: "Nikhil D. Kikkeri" <nikhil23@hotmail.com>
>CC: pvs-help@csl.sri.com
>Subject: Re: [PVS-Help] question regarding a dependent TCC
>Date: Mon, 13 Sep 2004 10:11:30 +0200
>Nikhil D. Kikkeri writes:
>    From: "Nikhil D. Kikkeri" <nikhil23@hotmail.com>
>    Date: Mon, 13 Sep 2004 11:26:50 +0530
>    Subject: [PVS-Help] question regarding a dependent TCC
>    in my case i have
>    n - posnat
>    so what does it mean when i have a dependent TCC which is
>    FORALL(x:nat)  x < 1 + n!1 IFF x< n!1
>    at first glance this seems correct to me, but there is no way i can 
>No, this is unprovable, because the implication from left to
>right fails. I guess you have some typing error. However, to say
>more you must post the code that generates the TCC.

The hottest products! The coolest discounts! http://www.msn.co.in/shopping 
Get them all at MSN Shopping!