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

question about prove


I am a green hand in PVS, now I met a TCC generated by
a theory. The theory is:

dd: TYPE = {r: real | r>=0}containing 1
ii: TYPE = posnat
a: TYPE = [# pr: dd,
             bk: dd #]

aa: TYPE = ARRAY[posnat -> a]

m: ii
i: posnat
T: aa

the TCC is:
FORALL(i, m): pr(T(i)) + m*bk(T(i)) >= 0 

after (grind)

| --------
pr(T(i!1)) + m!1*bk(T(i!1)) >= 0

What should I do next to complete the proof? I can't
find a way to tell the prover pr is a dd and dd is a
real which is eaqul or greater than 0.

Thank in advance.


Terrorist Attacks on U.S. - How can you help?
Donate cash, emergency relief information