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

Instantiation hints

I have to prove a number of theorems of the form

  (exists(a,b,c,...) : P(a,b,c,...))  => (exists(a,b,c,...) : Q(a,b,c,...))

where P=>Q is trivial once I get rid of the quantifications. The order
of the quantified variables may not be the same in the two
quantifications, but they have the same variables.

Is there a way to tell PVS that it should instantiate "a" with "a!1",
"b" with "b!1" etc.?