Term Rewriting System R:
[y, x, z]
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

DIV(x, y) -> QUOT(x, y, y)
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
QUOT(x, 0, s(z)) -> DIV(x, s(z))

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Negative Polynomial Order


Dependency Pairs:

QUOT(x, 0, s(z)) -> DIV(x, s(z))
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
DIV(x, y) -> QUOT(x, y, y)


Rules:


div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))





The following Dependency Pair can be strictly oriented using the given order.

QUOT(s(x), s(y), z) -> QUOT(x, y, z)


There are no usable rules (regarding the implicit AFS).
Used ordering:
Polynomial Order with Interpretation:

POL( QUOT(x1, ..., x3) ) = x1

POL( s(x1) ) = x1 + 1

POL( DIV(x1, x2) ) = x1


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳Neg POLO
           →DP Problem 2
             ↳Instantiation Transformation


Dependency Pairs:

QUOT(x, 0, s(z)) -> DIV(x, s(z))
DIV(x, y) -> QUOT(x, y, y)


Rules:


div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))





On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

DIV(x, y) -> QUOT(x, y, y)
one new Dependency Pair is created:

DIV(x'', s(z'')) -> QUOT(x'', s(z''), s(z''))

The transformation is resulting in no new DP problems.


Termination of R successfully shown.
Duration:
0:00 minutes