SE547: Sequential noninterference [6/23]

A memory μ is a mapping from variables to integers, for example:

{ x = 37, y = 5 }

Write μ(e) for the result of evaluating expression e in memory μ. For example, in the above memory, what are:

μ(x + 1)
μ(x == y)

Write μ[x:=n] for the result of updating memory μ so x now contains n. For example, in the above memory, what are:

μ[y := μ(x + 1)]
μ[y := μ(x == y)]