Notation: I use
*  =>_tau to denote PCF evaluation.
*  <==> to denote "if and only if"

(1) In the lecture, we discussed "stability": a function f is stable
if f(x /\ y) = f(x) /\ f(y) for all x, y, where /\ denotes the
"greatest lower bound" (glb):
   (i)  x/\y <= x and x/\y <= y
   (ii) if z' <= x and z' <= y, then z' <= x/\y
We assume that we are in a domain where each pair of elements has a glb.

(a) Show that x <= y  <===>  x = x /\ y
(b) Show that, if f is stable, then it is monotone.

(2) (Exercise 8.4.1) Suppose that a monotonic function p : (B_bot x
B_bot⊥) -> B_bot satisfies
p(true, bot) = true,
p(bot, true) = true,
and p(false, false) = false.
Show that p coincides with the parallel-or function on Slide 45 in the
sense that p(d1 , d2 ) = por (d1 )(d2 ), for all d1 , d2 in B_bot.

(3) (Exercise 8.4.2) Show that even though there are two evaluation
rules on Slide 50 with conclusion por(M1,M2 ) =>_bool true,
nevertheless the evaluation relation for PCF+por is still
deterministic (in the sense of Proposition 5.4.1).

(4) (Exercise 8.4.3) Give the axioms and rules for an inductively
defined transition relation for PCF+por. This should take the form of
a binary relation M -> M' between closed PCF+por terms. It should
satisfy
	M => V  <===>  M ->* V
(where ->* is the reflexive-transitive closure of ->).