YES Problem: f(X,X) -> f(a(),n__b()) b() -> a() b() -> n__b() activate(n__b()) -> b() activate(X) -> X Proof: DP Processor: DPs: f#(X,X) -> f#(a(),n__b()) activate#(n__b()) -> b#() TRS: f(X,X) -> f(a(),n__b()) b() -> a() b() -> n__b() activate(n__b()) -> b() activate(X) -> X TDG Processor: DPs: f#(X,X) -> f#(a(),n__b()) activate#(n__b()) -> b#() TRS: f(X,X) -> f(a(),n__b()) b() -> a() b() -> n__b() activate(n__b()) -> b() activate(X) -> X graph: f#(X,X) -> f#(a(),n__b()) -> f#(X,X) -> f#(a(),n__b()) EDG Processor: DPs: f#(X,X) -> f#(a(),n__b()) activate#(n__b()) -> b#() TRS: f(X,X) -> f(a(),n__b()) b() -> a() b() -> n__b() activate(n__b()) -> b() activate(X) -> X graph: Qed