Prove that A[[a[ya0]]]s = A[[a]](s[yA[[a0]]s]) for all states s.

N[n] A[n]s A[r]s = Table 1.1: The semantics of arithmetic expressions Substitutions We shall later be interested in replacing each occurrence of a variable y in an arithmetic expression a with another arithmetic expression ao. This is called substitution and we write ayao for the arithmetic expression so obtained. The formal definition is as follows: nyao