Exercise 7.3: order of logical steps for L-evaluation of *z


in the solution to exercise 7.3 C0p - Basics the expression L[*z]\sigma (I don’t know what the latex shortcut for the special bracket is) is immediately transformed into R[z]\sigma without proving that the later term is an address. Obviously the following calculation of R[z]\sigma proves this, however reading the equations from left to right we are using something before we have established it.

This seems like something a student might do in the exam (because it is fast and it is done in the lecture/exercises) and then get points deducted for it.

Also the & operator in this solution doesn’t render correctly.

This is the justification. To be formally correct, one should add the justification explicitly at the end (a small sentence, nothing fancy).

The \LaTeX version looks fine to me.

The ampersands also appear in the HTML version. (Although with escape characters for \LaTeX.)

A very useful tool for \LaTeX symbols is Detexify.
The [\![ bracket is \llbracket from the stmaryrd package.
But this is not supported in (the forum subset of) MathJax. Instead you can hack it together with -0.5 spaces $[\![$.