(COMMENT Transformation of outermost rewriting to context sensitive rewriting of: Example 5.3 in Matthias Raffelsieper and Hans Zantema "A transformational approach to prove outermost termination automatically" (note that, the transformation used here is not described in this paper) from(x) -> cons(x,from(s(x))) cons(s(x),xs) -> overflow ) (VAR x xs) (STRATEGY CONTEXTSENSITIVE (overflow_0) (s_0 1) (cons_0 1 2) (cons_1) (from_1) (from_3) (from_2)) (RULES from_2 (x) -> cons_0 (x, from_3 (s_0 (x))) from_3 (x) -> cons_1 (x, from_3 (s_0 (x))) from_1 (x) -> cons_0 (x, from_3 (s_0 (x))) cons_1 (s_0 (x), xs) -> overflow_0)