Consider the TRS R consisting of the rewrite rules

1: app(app(app(compose,f),g),x) -> app(g,app(f,x))
2: app(reverse,l) -> app(app(reverse2,l),nil)
3: app(app(reverse2,nil),l) -> l
4: app(app(reverse2,app(app(cons,x),xs)),l) -> app(app(reverse2,xs),app(app(cons,x),l))
5: app(hd,app(app(cons,x),xs)) -> x
6: app(tl,app(app(cons,x),xs)) -> xs
7: last -> app(app(compose,hd),reverse)
8: init -> app(app(compose,reverse),app(app(compose,tl),reverse))

There are 13 dependency pairs:

9: APP(app(app(compose,f),g),x) -> APP(g,app(f,x))
10: APP(app(app(compose,f),g),x) -> APP(f,x)
11: APP(reverse,l) -> APP(app(reverse2,l),nil)
12: APP(reverse,l) -> APP(reverse2,l)
13: APP(app(reverse2,app(app(cons,x),xs)),l) -> APP(app(reverse2,xs),app(app(cons,x),l))
14: APP(app(reverse2,app(app(cons,x),xs)),l) -> APP(reverse2,xs)
15: APP(app(reverse2,app(app(cons,x),xs)),l) -> APP(app(cons,x),l)
16: LAST -> APP(app(compose,hd),reverse)
17: LAST -> APP(compose,hd)
18: INIT -> APP(app(compose,reverse),app(app(compose,tl),reverse))
19: INIT -> APP(compose,reverse)
20: INIT -> APP(app(compose,tl),reverse)
21: INIT -> APP(compose,tl)

The approximated dependency graph contains one SCC:
{9-11,13,15}.

- Consider the SCC {9-11,13,15}.
The usable rules are {1-6}.
By taking the polynomial interpretation
[nil] = [reverse2] = 0,
[compose] = [cons] = [hd] = [reverse] = [tl] = 1
and [app](x,y) = [APP](x,y) = x + y + 1,
the rules in {2,4,11,13}
are weakly decreasing and
the rules in {1,3,5,6,9,10,15}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {11,13}.
By taking the polynomial interpretation
[nil] = [reverse2] = 0,
[compose] = [cons] = [hd] = [reverse] = [tl] = 1,
[app](x,y) = x + y
and [APP](x,y) = x + y + 1,
the rules in {3,4,13}
are weakly decreasing and
the rules in {1,2,5,6,11}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {13}.
By taking the polynomial interpretation
[nil] = [reverse2] = 0,
[compose] = [cons] = [hd] = [reverse] = [tl] = 1,
[APP](x,y) = x + 1
and [app](x,y) = x + y + 1,
the rules in {2,4}
are weakly decreasing and
the rules in {1,3,5,6,13}
are strictly decreasing.



Hence the TRS is terminating.