[tlaplus] Question about evaluation of Sequences

[Tim Soethout <tim@xxxxxxxxxxxxxx>]

Hi,

I'm using TLA+ for some modeling and TLC finds a counter example, but I don't understand why?

This statement:

`Len(committed[r1]) = (Len(committed[r2])+1) => Append(committed[r2], Head(committed[r1])) = committed[r1]`

is FALSE, but I don't see how?

The value of committed is `(r1 :> <<t1, t2>> @@ r2 :> <<t1>>)`.

What I'm trying to do is: If committed[r1] is 1 shorter than committed[r2], check if the last element from committed[r1] appended to committed[r2] makes them equal.

In this example case this should hold, right? What am I missing?

Thanks for potentially helping me.

Best regards,

Tim

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABZ6pRfSwipHCO1kQ0T2JpiA8U3mA7mgza0Y9KR1_%3D2tA-y8JQ%40mail.gmail.com.