+It's easy to understand these rules based on what S, K and I do. The first rule is obvious.
+The second rule says that if a lambda abstract contains no occurrences of the variable targeted by lambda,
+what the function expressed by that lambda term does it throw away its argument and returns whatever M
+computes: it's the constant function K[M].
+The third and fourth rules say what happens when there are occurrences of the bound variable in the body.
+
+Finally, the fifth rule says what to do for an application (divide and conquer).