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

(1) (Part of Exercise 6.5.1.) Prove the Proposition on Slide 38 for the
cases 
 * M' = x
 * M' = fn y:sigma. P 
 * M' = P Q.

(2) Prove Theorem 6.4.1 for the case 
 * (=>pred) 
 * (=>if1)

(3) (Exercise 6.5.2.) Define Omega_{tau} = fix(fn x : tau . x)
(i) Show that [[Omega_{tau}]] is the least element of the domain
    [[tau]].
(ii) 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) Define terms M, N : nat -> nat with 
    [[M]] <= [[N]] and not [[M]] = [[N]] 
 
(6) Verify that [[(fn x : sigma.M)N]] = [[M[N/x]]] for M, N with 
    |- N : sigma and x:sigma |- M : tau