This was just an example that TLA+ is not executable. You didn't realise that f[x] = -f[x] implies f[x] = 0, and that is how it is often: You have some propert

This was just an example that TLA+ is not executable. You didn't realise that f[x] = -f[x] implies f[x] = 0, and that is how it is often: You have some property, but you don't know what it entails exactly. TLA+ allows you to reason about that.