(VAR x y z) (RULES a(a(x)) -> b(b(x)) b(b(a(x))) -> a(b(b(x))) ) (COMMENT Example 2.46 in \cite{SK90})