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

Re: [PVS-Help] reversed replace



Title: Re: [PVS-Help] reversed replace
Yes, (replace 1). For RHS->LHR replacement, (replace 1 :dir rl).Try (help replace) for documentation on additional options for this strategy.

Cesar

On 4/22/11 4:04 AM, "Devarshi Ghoshal" <dghoshal@umail.iu.edu> wrote:

Hi,

Can you tell me if it is possible to directly use the replace command to replace the consequent by an LHS of an antecedent's matching RHS?

For example, in the following sequent

[-1] a = b
|----
 {1} c * b = d
How can I replace a for b such that the result becomes:


[-1] a = b
|----
 {1} c * a = d

--
Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@nasa.gov                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234