[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
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.