YES We show the termination of the TRS R: c() -> f() f() -> g() -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: c#() -> f#() and R consists of: r1: c() -> f() r2: f() -> g() The estimated dependency graph contains the following SCCs: (no SCCs)