I am new to TLA. I have a variable called x which should increase or stay the same at each new state. I thought I would put this in the invariant and it would work but it didn't. x' >= x. It doesn't know what x is. How do I check for this? Thanks.