[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!