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

Typing!

To: pvs-help@csl.sri.com
Subject: Typing!
From: Abdel Mokkedem <mokkedem@durga.cs.utah.edu>
Date: Thu, 16 Apr 1998 19:48:00 -0600 (MDT)
cc: pvs-bugs@csl.sri.com
Reply-To: Abdel Mokkedem <mokkedem@durga.cs.utah.edu>


Hi,

I tried to do (assert) to prove this sequent but it doesn't go true.
The premisse and conclusion are syntactically the same but I think 
it does not go true because of typing!

I did a show-expand-sequent to check the naming context, the formula
were still exactly the same. Thx for any help.

a


[-1]    member(nth(channel(s!1)(node!1), choose_DR(channel(s!1)(node!1)))
WITH [(committed) := TRUE],
             replace(channel(s!1)(node!1),
                     nth(channel(s!1)(node!1),
choose_DR(channel(s!1)(node!1))) WITH [(committed) := TRUE],
                     choose_DR(channel(s!1)(node!1))))
  |-------
[1]    member(nth(channel(s!1)(node!1), choose_DR(channel(s!1)(node!1)))
WITH [(committed) := TRUE],
             replace(channel(s!1)(node!1),
                     nth(channel(s!1)(node!1),
choose_DR(channel(s!1)(node!1))) WITH [(committed) := TRUE],
                     choose_DR(channel(s!1)(node!1))))

Prev by Date: protocol verification
Next by Date: Re: Typing!
Prev by thread: Re: problem with pvs
Next by thread: Re: Typing!
Index(es):
- Date
- Thread