Term Rewriting System R:

   [y, x]
   app(app(ack, 0), y) -> app(succ, y)
   app(app(ack, app(succ, x)), y) -> app(app(ack, x), app(succ, 0))
   app(app(ack, app(succ, x)), app(succ, y)) -> app(app(ack, x), app(app(ack, app(succ, x)), y))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   APP(app(ack, app(succ, x)), y) -> APP(app(ack, x), app(succ, 0))
   APP(app(ack, app(succ, x)), y) -> APP(ack, x)
   APP(app(ack, app(succ, x)), y) -> APP(succ, 0)
   APP(app(ack, 0), y) -> APP(succ, y)
   APP(app(ack, app(succ, x)), app(succ, y)) -> APP(app(ack, x), app(app(ack, app(succ, x)), y))
   APP(app(ack, app(succ, x)), app(succ, y)) -> APP(ack, x)
   APP(app(ack, app(succ, x)), app(succ, y)) -> APP(app(ack, app(succ, x)), y)

Furthermore, R contains one SCC.


SCC1:

APP(app(ack, app(succ, x)), app(succ, y)) -> APP(app(ack, app(succ, x)), y)
APP(app(ack, app(succ, x)), app(succ, y)) -> APP(app(ack, x), app(app(ack, app(succ, x)), y))
APP(app(ack, app(succ, x)), y) -> APP(app(ack, x), app(succ, 0))

At least one Dependency Pair of this SCC can be strictly oriented.


The following rules can be oriented: 

   app(app(ack, app(succ, x)), y) -> app(app(ack, x), app(succ, 0))
   app(app(ack, 0), y) -> app(succ, y)
   app(app(ack, app(succ, x)), app(succ, y)) -> app(app(ack, x), app(app(ack, app(succ, x)), y))


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
[app, 0, APP] > succ

 resulting in no new SCCs.

Used Argument Filtering System: ([APP(x_1, x_2) -> APP(x_1, x_2), app(x_1, x_2) -> app(x_1, x_2)])

Termination of R successfully shown.


Duration: 15.453 seconds.