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

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

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 prove 

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.