I use => to denote PCF evaluation. I omit the subscript type (tau) (1) Show that, if Q => V, then (fn x:tau. fn y:tau. y) P Q => V (2) To prove that PCF evaluation is deterministic, we prove (in Proposition 5.4.1) that the following set is closed under the rules of Fig.3 {(M, tau, V ) | M =>tau V & forall V' (M =>tau V' -> V = V')} Show this for the cases of (=>if1) and (=>cbn) (3) Given the definition of plus (Exercise 5.6.3.) plus = fix(fn p : nat -> nat -> nat. fn x : nat. fn y : nat. if zero(y) then x else succ(p x pred(y))) prove (by induction on n) that plus succ^m(0) succ^n(0) =>nat succ^{m+n}(0) for all n (4) Prove that the following terms M and N are not contextually equivalent. M = if x then 0 else 1 N = if y then 0 else 1