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

[PVS-Help] Rewriting using Replace


I am using PVS 2.3

In the course of a proof effort I decide to run "use" to make use of the 
lemma. "Use" comes up with the correct instance of the lemma which I would 
in the normal way proceed to use using "Replace".

However there is a problem, even though "Use" correctly comes up with the 
lemma instance I want to use, "Replace" fails in replacing the left hand 
side with the right hand side of the equality. I have searched the prover 
guide for any problems regarding "replace" and I havent found any 
documentation regarding this.

Can anyone point out what the problem could be?I will be happy to provide 
the details if so needed.



Easiest Money Transfer to India. Send Money To 6000 Indian Towns. 
http://go.msnserver.com/IN/42198.asp Easiest Way To Send Money Home!