Term Rewriting System R:

   [x, y, z]
   app(app(app(f, 0), 1), x) -> app(app(app(f, app(s, x)), x), x)
   app(app(app(f, x), y), app(s, z)) -> app(s, app(app(app(f, 0), 1), z))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   APP(app(app(f, 0), 1), x) -> APP(app(app(f, app(s, x)), x), x)
   APP(app(app(f, 0), 1), x) -> APP(app(f, app(s, x)), x)
   APP(app(app(f, 0), 1), x) -> APP(f, app(s, x))
   APP(app(app(f, 0), 1), x) -> APP(s, x)
   APP(app(app(f, x), y), app(s, z)) -> APP(s, app(app(app(f, 0), 1), z))
   APP(app(app(f, x), y), app(s, z)) -> APP(app(app(f, 0), 1), z)
   APP(app(app(f, x), y), app(s, z)) -> APP(app(f, 0), 1)
   APP(app(app(f, x), y), app(s, z)) -> APP(f, 0)

Furthermore, R contains one SCC.


SCC1:

APP(app(app(f, x), y), app(s, z)) -> APP(app(f, 0), 1)
APP(app(app(f, x), y), app(s, z)) -> APP(app(app(f, 0), 1), z)
APP(app(app(f, 0), 1), x) -> APP(app(f, app(s, x)), x)
APP(app(app(f, 0), 1), x) -> APP(app(app(f, app(s, x)), x), x)

On this Scc, a Narrowing SCC transformation can be performed.
 
As a result of transforming the rule 

   APP(app(app(f, x), y), app(s, z)) -> APP(app(f, 0), 1)
no new Dependency Pairs
are created.

none
The transformation is resulting in one subcycle:


SCC1.Nar1:

APP(app(app(f, 0), 1), x) -> APP(app(f, app(s, x)), x)
APP(app(app(f, 0), 1), x) -> APP(app(app(f, app(s, x)), x), x)
APP(app(app(f, x), y), app(s, z)) -> APP(app(app(f, 0), 1), z)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   app(app(app(f, 0), 1), x) -> app(app(app(f, app(s, x)), x), x)
   app(app(app(f, x), y), app(s, z)) -> app(s, app(app(app(f, 0), 1), z))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(1) = 0
POL(s) = 0
POL(APP(x_1, x_2)) = 1 + x_1
POL(f) = 0
POL(app(x_1, x_2)) = 1 + x_1
POL(0) = 0

 resulting in one subcycle.


SCC1.Nar1.Polo1:

APP(app(app(f, x), y), app(s, z)) -> APP(app(app(f, 0), 1), z)
APP(app(app(f, 0), 1), x) -> APP(app(app(f, app(s, x)), x), x)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(1) = 0
POL(s) = 0
POL(APP(x_1, x_2)) = x_2
POL(f) = 0
POL(app(x_1, x_2)) = 1 + x_2
POL(0) = 0

 resulting in one subcycle.


SCC1.Nar1.Polo1.Polo1:

APP(app(app(f, 0), 1), x) -> APP(app(app(f, app(s, x)), x), x)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   app(app(app(f, 0), 1), x) -> app(app(app(f, app(s, x)), x), x)
   app(app(app(f, x), y), app(s, z)) -> app(s, app(app(app(f, 0), 1), z))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(1) = 1
POL(s) = 0
POL(APP(x_1, x_2)) = x_1
POL(f) = 1
POL(app(x_1, x_2)) = x_1*x_2
POL(0) = 1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 10.950 seconds.