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() TDG Processor: DPs: f#(X,X) -> b#() f#(X,X) -> f#(a(),b()) TRS: f(X,X) -> f(a(),b()) b() -> c() graph: f#(X,X) -> f#(a(),b()) -> f#(X,X) -> f#(a(),b()) f#(X,X) -> f#(a(),b()) -> f#(X,X) -> b#() CDG Processor: DPs: f#(X,X) -> b#() f#(X,X) -> f#(a(),b()) TRS: f(X,X) -> f(a(),b()) b() -> c() graph: Qed