This page contains proofs to some assertions that are left as exercises in [Combinator engine].
----
'''Exercise 1.'''
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
----
'''Exercise 2.'''

To prove: 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 }

To prove: 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

To prove: T = C I

We want to have:            
    T x y = y x

Proof:
    C I x y = I y x
            = y x

To prove: W = C S I

We want to have
    W f x = f x x

Proof:
    W f x = C S I f x
          = S f I x
          = f x { I x }
          = f x x
----
'''Exercise 3.'''

To prove: S { K a } I = a

    S { K a } I x = K a x { I x }
                  = a { I x }
                   = x

To prove: S { K a } { K b } = K { a b }

    S { K a } { K b } x = K a x { K b x }
                          = a { K b x }
                          = a b
                          = K { a b } x

To prove: S { K a } = B a

    S { K a } x y = K a y { x y }
                  = a { x y }
                  = B a x y

To prove: S a { K b } = C a b

    S a { K b } x = a x { K b x }
                  = a x b
                  = C a b x