# Re: Re: [PVS-Help] partly replace

```Cesar Munoz:

Thank you very much!
The strategy you given is very useful to my some same proving processes.

Qingguo Xu
qgxu@xxxxxxxxxxxxxxx
2008-05-23

-------------------------------------------------------------

I don't think that you can do that with replace alone. However, you can
"simulate" that behavior as follows:

(name-replace "AA" "c*a" :hide? nil)
(replace -2 -1)
(replace -1 :dir rl :hide? t)

-------------------------------------------------------------
These commands can't work in the case that both sides of a formula is the same.
-------------------------------------------------------------
On the other hand, if you have the NASA libraries and the Field/Manip
packages, you can define following strategy in pvs-strategies

(defstep replace-in (fnum expr)
(let ((name (newname "RI")))
(then
(relabel "RI:" fnum)
(invoke (name-replace name "%1" :hide? nil) expr)
(replace "RI:" -1)
(replaces -1 :dir rl)
(delabel "RI:")))
"Replaces FNUM in EXPR"
"Replacing ~a in ~a")

{-1}  a = b
{-2}  b * a = c * a
|-------

Rule? (replace-in -1 (! -2 r))
Replacing -1 in (! -2 r),
this simplifies to:
foo :

{-1}  a = b
{-2}  b * a = c * b
|-------

The notation (! -2 r) is explained in the documentation of the Manip
package and means "The right hand side expression in formula -2".

Cesar

> Hi everyone here:
>    Can the prover command (repalce) complete replace some (not all) terms in a certain formula?
> For example, in the following pending sequent
>
> [-1] a = b
> [-2] c * a = c * a
> |----
>  {1} ....
>
> How to convert fnum -2 into c * a = c* b using (replace) command or other command with the help of fnum -1?
>
> I have read the help message about (repalce) command, and haven't find the useful information.
>
>
>
> Qingguo XU
>
>
>                        qgxu@xxxxxxxxxxxxxxx
>                        2008-05-22
>
>
>
>
>
>

--
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4

```