(RULES a -> b a -> f(a) b -> f(f(b)) ) (COMMENT doi:10.4230/LIPIcs.RTA.2012.165 [37] Example 3.1 (R) )