Lambda the Ultimate

Lately I started learning by myself the domain theory approach to semantics using G. Plotkin's "Domains" (1983). While doing the excercises, I bumped into the next question regarding fixed-point induction:

Let f,g: D -> D be continuous functions, such that f.f.g = g.f, and f _|_ = g_|_. Show that Yf = Yg.

(Here `.' is the analytic function composition: f.g(x) = f(g(x)) and _|_ denotes the least element, of course).

[Chap. 2 question 21]

It is more or less clear how to prove it using normal induction and the least fixed point formula, but I have no idea which inclusive predicates to choose. I was hoping someone here could supply some hints\directions.

On a more general note: Is there an intuition as to how to choose these inclusive predicates? I imagine it is acquired in time and practice, so do you know of a list of properties that can be proved using fixed-point induction?

Thanks in advance,
Ohad.

Via Mitch Wand's R6RS announcements mailing list:

I am extremely pleased to announce that a draft version of R6RS is now available at www.r6rs.org. A copy will also be posted on schemers.org.

The charter provides for a six-month public comment period. Therefore the editors, in consultation with the steering committee, have provided a mechanism for comment and discussion. Details are also at www.r6rs.org.

The comment period is now open and will continue until March 15, 2007.

The steering committee thanks the editors for their intensive work on the draft R6RS, and looks forward to the public comment period.

Enjoy!

For the Steering Committee,
--Mitch Wand