Term Rewriting System R:

   [f, n, x, xs]
   app(app(f, 0), n) -> app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
   app(app(map, f), nil) -> nil
   app(app(map, f), app(app(cons, x), xs)) -> app(app(cons, app(f, x)), app(app(map, f), xs))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   APP(app(map, f), app(app(cons, x), xs)) -> APP(app(cons, app(f, x)), app(app(map, f), xs))
   APP(app(map, f), app(app(cons, x), xs)) -> APP(cons, app(f, x))
   APP(app(map, f), app(app(cons, x), xs)) -> APP(f, x)
   APP(app(map, f), app(app(cons, x), xs)) -> APP(app(map, f), xs)
   APP(app(f, 0), n) -> APP(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
   APP(app(f, 0), n) -> APP(hd, app(app(map, f), app(app(cons, 0), nil)))
   APP(app(f, 0), n) -> APP(app(map, f), app(app(cons, 0), nil))
   APP(app(f, 0), n) -> APP(map, f)
   APP(app(f, 0), n) -> APP(app(cons, 0), nil)
   APP(app(f, 0), n) -> APP(cons, 0)

Furthermore, R contains one SCC.


SCC1:

APP(app(f, 0), n) -> APP(app(cons, 0), nil)
APP(app(f, 0), n) -> APP(app(map, f), app(app(cons, 0), nil))
APP(app(f, 0), n) -> APP(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
APP(app(map, f), app(app(cons, x), xs)) -> APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) -> APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) -> APP(app(cons, app(f, x)), app(app(map, f), xs))

Found an infinite P-chain over R:
P = APP(app(f, 0), n) -> APP(app(cons, 0), nil)
APP(app(f, 0), n) -> APP(app(map, f), app(app(cons, 0), nil))
APP(app(f, 0), n) -> APP(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
APP(app(map, f), app(app(cons, x), xs)) -> APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) -> APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) -> APP(app(cons, app(f, x)), app(app(map, f), xs))
R = [app(app(map, f), app(app(cons, x), xs)) -> app(app(cons, app(f, x)), app(app(map, f), xs)), app(app(map, f), nil) -> nil, app(app(f, 0), n) -> app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)]
s = APP(app(cons, 0), nil) evaluates to t = APP(app(cons, 0), nil)
Thus, s starts an infinite reduction.


Non-Termination of R could be shown.

Duration: 1.138 seconds.