lambda calculus: delta rules
 > I don't understand this last line at all. How can you get from
 > `(lambda xy.deltaC xy)II' to `(lambda xyzw.w)II'?

 Simply by redycing deltaC x y first.

 deltaC x y > lambda xy. y
 (which, by alpha) = lambda zw . w
Well,
deltaC x y > lambda xy.y
only if x is not syntactically equivalent to y.
I think I'm missing something completely here. To me x and y seem to
be syntactically equivalent in the above reductions and if they indeed
are syntactically equivalent, then the complete form would reduce like
this:
(lambda xy.deltaC x y)II > (lambda xyzw.z)II >> lambda zw.z
which would be correct.
Although, I think a related example proves the point that you must not
apply delta rules to open terms:
(lambda xy.deltaC x y)IK > (lambda xyzw.z)IK > lambda zw.z
which is clearly incorrect, since I is not equivalent to K.
Still not getting the original example and probably completely
misunderstanding something,
Boris

To err is human,
To purr feline.
 Robert Byrne