Re: [PVS-Help] reversed replace

["Munoz, Cesar Augusto (LARC-D320)" <cesar.a.munoz@xxxxxxxx>]

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