YES (VAR x0 x) (RULES a(a(a(a(x0)))) -> a(c(c(x0))) d(a(a(x0))) -> a(c(c(x0))) a(a(d(x0))) -> a(c(c(x0))) a(c(c(a(x0)))) -> a(c(c(x0))) a(c(a(a(x0)))) -> a(c(c(x0))) c(c(a(a(x0)))) -> a(c(c(x0))) a(a(c(x0))) -> c(a(a(x0))) d(a(c(c(x0)))) -> a(c(c(x0))) d(d(x)) -> c(c(a(c(x)))) c(d(x)) -> a(a(x)) c(a(c(c(x)))) -> a(c(c(x))) b(x) -> c(c(x)) c(c(c(x))) -> a(c(c(x))) d(c(x)) -> a(a(x)) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers a_A(x1) = 1 d_A(x1) = 3 c_A(x1) = 1 b_A(x1) = 2 weights w0 = 1 w(a) = 5 w(d) = 14 w(c) = 7 w(b) = 15 and precedence: d > a > c > b )