Term Rewriting System R:

   [x, y, p, f]
   app(app(app(if, true), x), y) -> x
   app(app(app(if, false), x), y) -> y
   app(app(app(until, p), f), x) -> app(app(app(if, app(p, x)), x), app(app(app(until, p), 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(app(until, p), f), x) -> APP(app(app(if, app(p, x)), x), app(app(app(until, p), f), app(f, x)))
   APP(app(app(until, p), f), x) -> APP(app(if, app(p, x)), x)
   APP(app(app(until, p), f), x) -> APP(if, app(p, x))
   APP(app(app(until, p), f), x) -> APP(p, x)
   APP(app(app(until, p), f), x) -> APP(app(app(until, p), f), app(f, x))
   APP(app(app(until, p), f), x) -> APP(f, x)

Furthermore, R contains one SCC.


SCC1:

APP(app(app(until, p), f), x) -> APP(f, x)
APP(app(app(until, p), f), x) -> APP(app(app(until, p), f), app(f, x))
APP(app(app(until, p), f), x) -> APP(p, x)
APP(app(app(until, p), f), x) -> APP(app(if, app(p, x)), x)
APP(app(app(until, p), f), x) -> APP(app(app(if, app(p, x)), x), app(app(app(until, p), f), app(f, x)))

Found an infinite P-chain over R:
P = APP(app(app(until, p), f), x) -> APP(f, x)
APP(app(app(until, p), f), x) -> APP(app(app(until, p), f), app(f, x))
APP(app(app(until, p), f), x) -> APP(p, x)
APP(app(app(until, p), f), x) -> APP(app(if, app(p, x)), x)
APP(app(app(until, p), f), x) -> APP(app(app(if, app(p, x)), x), app(app(app(until, p), f), app(f, x)))
R = [app(app(app(until, p), f), x) -> app(app(app(if, app(p, x)), x), app(app(app(until, p), f), app(f, x))), app(app(app(if, false), x), y) -> y, app(app(app(if, true), x), y) -> x]
s = APP(app(app(until, p), f), x) evaluates to t = APP(app(app(until, p), f), app(f, x))
Thus, s starts an infinite reduction as s matches t.


Non-Termination of R could be shown.

Duration: 1.419 seconds.