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

[PVS-Help] beta



>From pvs-prover-guide:

 (f WITH [..., (i) := e, ...])(j ) reduces to e if it can be shown that
  i = j , and the assignments following (i) := e do not affect f (j ). If it can
  be shown using the decision procedures that none of the updates affect the
  value of f at j , then the expression simply reduces to f (j ).

What are the decision procedures mentioned in the latter case where the 
expression reduces to f(j)?  I have a consequent of the form:

{1}   p /= q2 AND
       (TRUE OR FALSE OR FALSE OR FALSE) AND
        (pcPush2?(pc(c0) WITH [p := pcPush2](q2)) OR
          pcPush4?(pc(c0) WITH [p := pcPush2](q2)) OR
           pcPush5?(pc(c0) WITH [p := pcPush2](q2)) OR
            pcPush6?(pc(c0) WITH [p := pcPush2](q2)))
       IMPLIES
       NOT ptr(nextfree(unallocated(c0))) =
            n(c0) WITH [p := ptr(nextfree(unallocated(c0)))](q2)


I'd like the expressions on lines 3,4,5 and 6 to simplify to
        (pcPush2?(pc(c0)(q2)) OR
          pcPush4?(pc(c0)(q2)) OR
           pcPush5?(pc(c0)(q2)) OR
            pcPush6?(pc(c0)(q2)))

ie, the function update 'WITH' is irrelevant because we have p /= q2 
from the conjunction on line 1.  
Applying (beta) does not do the trick.  How should I massage the
expression so that beta will recognise the the function application
can be reduced?

Thanks,
Rob