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 } [] ----