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
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

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)
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)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Non Termination


Dependency Pairs:

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))
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)


Rules:


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))





Found an infinite P-chain over R:
P =

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))
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)

R =

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))

s = APP(app(cons, 0), nil)
evaluates to t =APP(app(cons, 0), nil)

Thus, s starts an infinite chain.

Non-Termination of R could be shown.
Duration:
0:00 minutes