Term Rewriting System R:

   [f, g, x, l, xs]
   app(app(app(compose, f), g), x) -> app(g, app(f, x))
   app(reverse, l) -> app(app(reverse2, l), nil)
   app(app(reverse2, nil), l) -> l
   app(app(reverse2, app(app(cons, x), xs)), l) -> app(app(reverse2, xs), app(app(cons, x), l))
   app(hd, app(app(cons, x), xs)) -> x
   app(tl, app(app(cons, x), xs)) -> xs
   last -> app(app(compose, hd), reverse)
   init -> app(app(compose, reverse), app(app(compose, tl), reverse))

Termination of R to be shown.


Removing the following rules from R which fullfill a polynomial ordering: 

   app(app(app(compose, f), g), x) -> app(g, app(f, x))

where the Polynomial interpretation:
POL(nil) = 0
POL(last) = 1
POL(init) = 2
POL(reverse2) = 0
POL(reverse) = 0
POL(hd) = 0
POL(tl) = 0
POL(app(x_1, x_2)) = x_1 + x_2
POL(cons) = 0
POL(compose) = 1
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   app(reverse, l) -> app(app(reverse2, l), nil)

where the Polynomial interpretation:
POL(nil) = 0
POL(last) = 1
POL(init) = 2
POL(reverse2) = 0
POL(hd) = 0
POL(tl) = 0
POL(reverse) = 1
POL(app(x_1, x_2)) = x_1 + x_2
POL(cons) = 0
POL(compose) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   app(app(reverse2, nil), l) -> l

where the Polynomial interpretation:
POL(nil) = 0
POL(last) = 0
POL(init) = 0
POL(reverse2) = 1
POL(hd) = 0
POL(tl) = 0
POL(reverse) = 0
POL(app(x_1, x_2)) = x_1 + x_2
POL(cons) = 0
POL(compose) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   app(app(reverse2, app(app(cons, x), xs)), l) -> app(app(reverse2, xs), app(app(cons, x), l))
   app(hd, app(app(cons, x), xs)) -> x
   app(tl, app(app(cons, x), xs)) -> xs

where the Polynomial interpretation:
POL(last) = 0
POL(init) = 0
POL(reverse2) = 2
POL(hd) = 0
POL(tl) = 0
POL(reverse) = 0
POL(app(x_1, x_2)) = 2*x_1 + x_2
POL(cons) = 1
POL(compose) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   last -> app(app(compose, hd), reverse)

where the Polynomial interpretation:
POL(last) = 1
POL(init) = 0
POL(reverse) = 0
POL(tl) = 0
POL(hd) = 0
POL(app(x_1, x_2)) = x_1 + x_2
POL(compose) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   init -> app(app(compose, reverse), app(app(compose, tl), reverse))

where the Polynomial interpretation:
POL(init) = 1
POL(reverse) = 0
POL(tl) = 0
POL(app(x_1, x_2)) = x_1 + x_2
POL(compose) = 0
was used. 



All Rules of R can be deleted.



Termination of R successfully shown.


Duration: 0.518 seconds.