[auggierose]

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.

[zekrioca]

Thanks, that makes sense!