YES We show the termination of the TRS R: f(X,X) -> f(a(),n__b()) b() -> a() b() -> n__b() activate(n__b()) -> b() activate(X) -> X -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: f#(X,X) -> f#(a(),n__b()) p2: activate#(n__b()) -> b#() and R consists of: r1: f(X,X) -> f(a(),n__b()) r2: b() -> a() r3: b() -> n__b() r4: activate(n__b()) -> b() r5: activate(X) -> X The estimated dependency graph contains the following SCCs: (no SCCs)