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

Re: Unclear TLC evaluation behavior

Sorry again, obviously it's a partial relation induced by the formula on all pairs of states... :)

On Wednesday, October 21, 2015 at 12:40:19 AM UTC+3, Ron Pressler wrote:
My mistake was not realizing that Next is a full relation on the entire universe of states (I thought that it was a "constructive" partial relation), that for _every_ two states s and t, must determine whether t can be a next state of s or not. Then, on top of that, there's TLC's evaluation rules about the first encounter with a primed variable that must uniquely determine its value, and therefore cannot be a negation of the sort ~(x' = ...).

Do I have it right?