Reduction Paths

With proof 1, I (I x) ⇒ I x, show that it can be reduced two different ways. With proof 2, W W W ⇒ dummy, understand that the W W W can be reduced forever. With proofs 3 and 4, K x (W W W) ⇒ x and K x (W W W) ⇒ K x (W W W), understand that the K x (W W W) reduces to a normal form under one reduction strategy (i.e. normal order (leftmost redex first or 'function' before 'arguments')). Whereas it is non-terminating under a different strategy (i.e applicative order (some internal redexes first or 'arguments' before 'function')). The system is set up not to permit rewrites that do nothing so it will pass on rewriting K x (W W W) to K x (W W W).