YES (VAR x0 x) (RULES e(e(c(x0))) -> e(c(e(x0))) e(c(c(x0))) -> e(c(x0)) d(e(c(x))) -> e(c(x)) e(d(x)) -> e(c(x)) c(d(x0)) -> c(c(c(x0))) c(e(c(x0))) -> e(c(x0)) c(c(c(e(x)))) -> e(c(x)) c(c(c(c(x)))) -> c(c(c(x))) d(c(c(x))) -> c(c(c(x))) b(x) -> d(d(x)) d(d(d(x))) -> c(c(x)) a(x) -> c(c(c(x))) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers a_A(x1) = 2 b_A(x1) = x1 + 4 c_A(x1) = 1 d_A(x1) = 3 e_A(x1) = 0 a#_A(x1) = 0 weights w0 = 1 w(a) = 8 w(b) = 11 w(c) = 2 w(d) = 5 w(e) = 1 and precedence: e > b > a > c > d )