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

[PVS-Help] reversed replace


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

Thanks & regards,