Hello,
Suppose I have a function a, that has domain Z. Suppose x and y are in Z.
I'm writing an action where both a[x] and a[y] must be changed.
I have one line of the following form:
a' = [a EXCEPT ![x] = ...]
and another like so:
a' = [a EXCEPT ![y] = ...]
How would I be able to write this altogether as one? Having both doesn't seem to work with Model Checking as count = 0 for those lines.
I apologize if I'm using the wrong terms to explain my problem.
Thanks for any help