I'm using TLA+ for some modeling and TLC finds a counter example, but I don't understand why?
`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.