This page contains proofs to some assertions that are left as exercises in [Combinator engine].
----
I = S K K

To prove this, remember that
    S x y z = x z { y z }
and
    K x y = x
So what is S K K p?
    S K K p = K p { K p }
            = p
----
B = S {K S} K

Remember, we want
    B x y z = x { y z }

So, let's see:
    S { K S } K x y z = K S x { K x } y z
                      = S { K x } y z
                      = K x z { y z }
                      = x { y z }
----
C = S { B B S } { K K }

We want to have
    C f x y = f y x
({C f y} is a notation for currying the ''second'' argument of ''f'', just as {f x} curries the first.)

    S { B B S } { K K } f x y = B B S f { K K f } x y
                              = B { S f } { K K f } x y
                              = S f { K K f x } y
                              = f y { K K f x y }
                              = f y { K x y }
                              = f y x
----