I use => to denote PCF evaluation. I omit the subscript type (tau)

(1) (Part Exercise 6.5.1.) Prove the Propositions on Slide 38 for the
cases M' = fn y:sigma. P and for the case M' = P Q.

(2) Prove Theorem 6.4.1 for the cases of (=>pred) and (=>if1)

(3) (Exercise 6.5.2.) Defining Omega_{tau} = fix(fn x : tau . x), show
that [[Omega_{tau}]] is the least element of the domain
[[tau]]. Deduce that [[fn x : tau . Omega_{tau} ]] = [[Omega_{tau->tau}]].

(4) (i) Compute the denotational semantics of 
    M = fn x :bool . fn y: nat . if x then y else y
    (ii) Define a term N such that [[M]] = [[N]] but N does not
    evaluate to M
    
(5) Verify that [[V]] = [[V']] as stated in Example 5.5.1, by
    computing the denotational semantics of V and V'.
    NB V = fn x : nat.(fn y : nat. y)0 and V' = fn x : nat.0