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

Problem with "WITH"


I have a consequent, which I think should be trivial to prove,
but I have not succeeded. I have tried simplify, (assert :flush? t),
whatever I could think of, but to no avail.  

The consequent is 

      id(cEntry!1) =
            WITH [v := mem!1(a(cEntry!1)),
                  t := t(procs!1(0))])

where cEntry!1 is of type [# v : VALUE, t : TIME,
                             id : PROC_ID, pc : PC_RANGE#]

Since the id field is not modified by the WITH statement I would expect
the proof to be simple.

Trying (grind) I get an unprovable sequent as follows:

id rewrites id(cEntry!1)
  to cEntry!1
id rewrites 
       WITH [v := mem!1(a(cEntry!1)), t := t(procs!1(0))])
  to cEntry!1
        WITH [v := mem!1(a(cEntry!1)), t := t(procs!1(0))]
Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to: 
idPCunqiue 5.1 :  

      cEntry!1 =
         WITH [message := readRet, v := mem!1(a(cEntry!1)), t := t(procs!1(0))]

Any suggestions would be appreciated.


P.S. I am using PVS 2-3 no patches