Consider the TRS R consisting of the rewrite rules 1: flatten(nil) -> nil 2: flatten(unit(x)) -> flatten(x) 3: flatten(x ++ y) -> flatten(x) ++ flatten(y) 4: flatten(unit(x) ++ y) -> flatten(x) ++ flatten(y) 5: flatten(flatten(x)) -> flatten(x) 6: rev(nil) -> nil 7: rev(unit(x)) -> unit(x) 8: rev(x ++ y) -> rev(y) ++ rev(x) 9: rev(rev(x)) -> x 10: x ++ nil -> x 11: nil ++ y -> y 12: (x ++ y) ++ z -> x ++ (y ++ z) There are 12 dependency pairs: 13: FLATTEN(unit(x)) -> FLATTEN(x) 14: FLATTEN(x ++ y) -> flatten(x) ++# flatten(y) 15: FLATTEN(x ++ y) -> FLATTEN(x) 16: FLATTEN(x ++ y) -> FLATTEN(y) 17: FLATTEN(unit(x) ++ y) -> flatten(x) ++# flatten(y) 18: FLATTEN(unit(x) ++ y) -> FLATTEN(x) 19: FLATTEN(unit(x) ++ y) -> FLATTEN(y) 20: REV(x ++ y) -> rev(y) ++# rev(x) 21: REV(x ++ y) -> REV(y) 22: REV(x ++ y) -> REV(x) 23: (x ++ y) ++# z -> x ++# (y ++ z) 24: (x ++ y) ++# z -> y ++# z The approximated dependency graph contains 3 SCCs: {23,24}, {13,15,16,18,19} and {21,22}. - Consider the SCC {23,24}. The usable rules are {10-12}. By taking the polynomial interpretation [nil] = 1 and [++](x,y) = [++#](x,y) = x + y + 1, the rules in {12,23} are weakly decreasing and the rules in {10,11,24} are strictly decreasing. There is one new SCC. - Consider the SCC {23}. By taking the polynomial interpretation [nil] = 1, [++#](x,y) = x + 1 and [++](x,y) = x + y + 1, rule 12 is weakly decreasing and the rules in {10,11,23} are strictly decreasing. - Consider the SCC {13,15,16,18,19}. There are no usable rules. By taking the polynomial interpretation [FLATTEN](x) = [unit](x) = x + 1 and [++](x,y) = x + y + 1, the rules in {13,15,16,18,19} are strictly decreasing. - Consider the SCC {21,22}. There are no usable rules. By taking the polynomial interpretation [REV](x) = x + 1 and [++](x,y) = x + y + 1, the rules in {21,22} are strictly decreasing. Hence the TRS is terminating.