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

Re: [PVS-Help] beta



R. Colvin writes:
   
   {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)))

My experience is that you have to record the inequality p/=q2
with the decision procedures (see 4.12.7 prover manual). This
will happen implicitely with assert (or simplify) IF THERE IS A
ANTECEDENT *JUST* CONTAINING THE INEQUALITY (or a consequent
*just* containing p = q2).

So you have to flatten or split and then try assert again
(possibly twice).

Bye,

Hendrik