Question on Combinator Reduction

[linus!watro@husc6.harvard.edu (Ronald J. Watro)]

Is there anywhere in the literature a correctness proof for
combinator reduction using the cyclic Y-rule, as described,
for example, in Peyton-Jones' book on implementing functional
languages?  I have looked at several papers on Graph Rewriting,
including one by Barendregt et. al. in the 87 PARLE conference,
but I cannot find this result.

-- 
Dr. Ronald J. Watro   The MITRE Corporation, MS A040, Burlington RD,
                      Bedford, MA 01730  USA      617-271-8390
ARPA:   watro%linus@mitre-bedford.ARPA
UUCP:   ...{decvax,utzoo,philabs,security,allegra,genrad}!linus!watro