Re: Typing!

[Sam Owre <owre@csl.sri.com>]

Hi Abdel,

Could you send a dump of your specification so I can look into this?  It
sounds like it may be a bug.

Thanks,
Sam Owre


> From:    Abdel Mokkedem <mokkedem@durga.cs.utah.edu>
> Subject: Typing!
> Date:    Thu, 16 Apr 1998 19:48:00 MDT
> To:      pvs-help@csl.sri.com
> cc:      pvs-bugs@csl.sri.com
> 
> 
> 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: Typing!
• Next by Date: Re: Typing!
• Prev by thread: Typing!
• Next by thread: Re: Typing!
• Index(es):
  • Date
  • Thread