Term Rewriting System R:

   [f, x]
   app(app(iterate, f), x) -> app(app(cons, x), app(app(iterate, f), app(f, x)))

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   APP(app(iterate, f), x) -> APP(app(cons, x), app(app(iterate, f), app(f, x)))
   APP(app(iterate, f), x) -> APP(cons, x)
   APP(app(iterate, f), x) -> APP(app(iterate, f), app(f, x))
   APP(app(iterate, f), x) -> APP(f, x)

Furthermore, R contains one SCC.


SCC1:

APP(app(iterate, f), x) -> APP(f, x)
APP(app(iterate, f), x) -> APP(app(iterate, f), app(f, x))
APP(app(iterate, f), x) -> APP(app(cons, x), app(app(iterate, f), app(f, x)))

Found an infinite P-chain over R:
P = APP(app(iterate, f), x) -> APP(f, x)
APP(app(iterate, f), x) -> APP(app(iterate, f), app(f, x))
APP(app(iterate, f), x) -> APP(app(cons, x), app(app(iterate, f), app(f, x)))
R = [app(app(iterate, f), x) -> app(app(cons, x), app(app(iterate, f), app(f, x)))]
s = APP(app(iterate, f), x) evaluates to t = APP(app(iterate, f), app(f, x))
Thus, s starts an infinite reduction as s matches t.


Non-Termination of R could be shown.

Duration: 0.646 seconds.