(VAR x ) (RULES d(0) -> 0 d(s(x)) -> s(s(d(x))) e(0) -> s(0) e(r(x)) -> d(e(x)) )