# Tag Info

Assume we are running program x := e, and let $\sigma$ be the initial state, and $\sigma'$ be the final state. The crucial intuition here is: the value of $x$ in the final state $\sigma'$ is the same as the value of the expression $e$ in the initial state $\sigma$. Indeed, the latter is the value we assign to $x$ with the command x := e. Hence, if $P(-)$ ...
So after reading and thinking about it more this is my explanation (thanks software foundations): The key confusion for me seems to be the meaning of $P[e/x]$ (replaces every free instance of x with e). What this does is wherever you see the symbol $x$ literally remove it and place $e$. e.g. $P[e/x] = (x+y+1)[e/x] \to P[e/x] = (e+y+1)$ so notice how $x$ ...