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

Re: [PVS-Help] reversed replace

Hi All,

Thanks for all the expanations. It worked.

On Fri, Apr 22, 2011 at 12:58 PM, John Rushby <rushby@csl.sri.com> wrote:

Rule? (help replace)

(replace fnum &optional ((fnums *) dir hide? actuals? dont-delete?)):
   Rewrites the given formulas in FNUMS with the formula FNUM.  If FNUM is
an antecedent equality, then it rewrites left-to-right if DIR is LR (the
default), and right-to-left if DIR is RL.  If FNUM is not an antecedent
equality, then any occurrence of the formula FNUM in FNUMS is replaced by
TRUE if FNUM is an antecedent, FALSE for a succedent.  If HIDE? is T, then
FNUM is hidden afterward.  When ACTUALS?  is T, the replacement is done
within actuals of names in addition to the expression level replacements,
including in types.  When the DONT-DELETE? flag is T, top-level sequent
formulas are not deleted through being replaced by TRUE/FALSE.

So (replace -1 :dir RL) will do what you want


On 04/22/2011 01:04 AM, Devarshi Ghoshal 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

Thanks & regards,