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

Typing!




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))))