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

Problem with "WITH"



Hello, 

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 


 |-------
[1,(idPCunique)]
      id(cEntry!1) =
       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 
  id(cEntry!1
       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 :  

  |-------
{1,(idPCunique)}
      cEntry!1 =
       cEntry!1
         WITH [message := readRet, v := mem!1(a(cEntry!1)), t := t(procs!1(0))]


Any suggestions would be appreciated.

Thanks,
Tamarah

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