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