x: = cons (1, nil); 1 nil y: = cons (2, x) 2 1 nil hd (x): =3

When x is printed it is (3) and y when printed is (2, 3) rather than (2, 1) as it would have been had the last assignment left it undisturbed. How are we to prove assertions about such programs?