YES Problem: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) Proof: DP Processor: DPs: v#(a(a(x))) -> v#(x) v#(a(a(x))) -> u#(v(x)) v#(a(c(x))) -> u#(b(d(x))) w#(a(a(x))) -> w#(x) w#(a(a(x))) -> u#(w(x)) w#(a(c(x))) -> u#(b(d(x))) TRS: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) TDG Processor: DPs: v#(a(a(x))) -> v#(x) v#(a(a(x))) -> u#(v(x)) v#(a(c(x))) -> u#(b(d(x))) w#(a(a(x))) -> w#(x) w#(a(a(x))) -> u#(w(x)) w#(a(c(x))) -> u#(b(d(x))) TRS: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) graph: w#(a(a(x))) -> w#(x) -> w#(a(c(x))) -> u#(b(d(x))) w#(a(a(x))) -> w#(x) -> w#(a(a(x))) -> u#(w(x)) w#(a(a(x))) -> w#(x) -> w#(a(a(x))) -> w#(x) v#(a(a(x))) -> v#(x) -> v#(a(c(x))) -> u#(b(d(x))) v#(a(a(x))) -> v#(x) -> v#(a(a(x))) -> u#(v(x)) v#(a(a(x))) -> v#(x) -> v#(a(a(x))) -> v#(x) CDG Processor: DPs: v#(a(a(x))) -> v#(x) v#(a(a(x))) -> u#(v(x)) v#(a(c(x))) -> u#(b(d(x))) w#(a(a(x))) -> w#(x) w#(a(a(x))) -> u#(w(x)) w#(a(c(x))) -> u#(b(d(x))) TRS: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) graph: Qed