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

Existence TCCs



I am trying to familiarize myself with PVS, using the tutorial, and
find myself confused
about the existence TCCs.  They appear with the note
"May need to add an assuming clause to prove this."
But I don't see any discussion of what the assuming clause is, how to
write one, or what one means.

I realize that this is probably something of a frequently asked
question, so I would be more than happy with a simple pointer to a
solution in the PVS
documents!

Thank you very much,
Robert