Notation: I use * <_tau to denote the approximation relation (slide 39) * =>_tau to denote PCF evaluation. * <= to denote ordering in a domain * <=_ctx to denote contextual preorder (1) Show that, if d <_nat M, e <_nat N and b <_bool P, then if(b,d,e) <_nat if P then M else N (This is the "if" inductive case in the proof of the Fundamental Property, Slide 40) (2) Prove the following properties (by induction on tau) (a) if d2 <= d1 and d1 <_tau M1, then d2 <_tau M1 (b) if d1 <_tau M1 and forall V(M1 =>_tau V implies M2 =>_tau V), then d1 <_tau M2 These properties constitute Lemma 7.2.1(iii) (3) Prove, using the definition of <=_ctx (slide 42), that Gamma |- M Omega <=_ctx M (succ^n(0)) : tau for any M : nat -> tau, n a number and Omega := fix (fn x:nat.x)