YES Problem: f(x,x) -> f(a(),b()) b() -> c() Proof: DP Processor: DPs: f#(x,x) -> b#() f#(x,x) -> f#(a(),b()) TRS: f(x,x) -> f(a(),b()) b() -> c() CDG Processor: DPs: f#(x,x) -> b#() f#(x,x) -> f#(a(),b()) TRS: f(x,x) -> f(a(),b()) b() -> c() graph: Qed