Sometimes, we want to enforce invariants *between* processes. For example, only one thread may have a lock at the same time, or the total values across all processes must be less than a certain threshold. Here’s one example:

```
process foo \in 1..2
variable x \in 1..2
begin
Skip:
skip
end process
```

How do we assert the variant “the sum of x between the two processes is not 4?” With a single process algorithm, we could write `x /= 4`

. But to do the same with multiple processes, we have to let the PlusCal abstraction leak.

When we translate an algorithm, TLA+ will create all of the corresponding variables. When we have multiple processes, TLA+ will instead create a function with a domain on the process identifiers and the range the actual values of x per process. So instead of having for example `x \in 1..2`

, we instead have `x == [ProcSet -> 1..2]`

. So in this case, the appropriate invariant is `x[1] + x[2] /= 4`

.