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

[PVS-Help] partly replace



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.

thanks in advance.


Qingguo XU


                       qgxu@xxxxxxxxxxxxxxx
                       2008-05-22