POG: State Invariant PO incorrect

[ldcouto]

For a model like:

state S of 
  n : nat
inv s == s = mk_S(0) 
end 
operations

Op: () ==> () 
Op() ==   n := 1;

We get a PO for the state invariant: let s = S in (s = mk_S(0))

But this PO does not correctly represent the state. The idea (I guess) is that let s=S to represents the value of the state at the given point. But in proofs, the value of the state needs to be encoded in a formula and not referrenced like in the interpreter. So the correct PO should be something like: let s =mk_S(1) in (s = mk_S(0)).