[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[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
this.what is the solution to towards resolving this.I know i am providing
very little data apart from what i have said already.
Any solution will be of great help.
All the news that matters. All the gossip from home.
http://www.msn.co.in/NRI/ Specially for NRIs!