Term Rewriting System R:
[Y, X]
minus(n0, Y) -> 0
minus(ns(X), ns(Y)) -> minus(activate(X), activate(Y))
geq(X, n0) -> true
geq(n0, ns(Y)) -> false
geq(ns(X), ns(Y)) -> geq(activate(X), activate(Y))
div(0, ns(Y)) -> 0
div(s(X), ns(Y)) -> if(geq(X, activate(Y)), ns(div(minus(X, activate(Y)), ns(activate(Y)))), n0)
if(true, X, Y) -> activate(X)
if(false, X, Y) -> activate(Y)
0 -> n0
s(X) -> ns(X)
activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

MINUS(n0, Y) -> 0'
MINUS(ns(X), ns(Y)) -> MINUS(activate(X), activate(Y))
MINUS(ns(X), ns(Y)) -> ACTIVATE(X)
MINUS(ns(X), ns(Y)) -> ACTIVATE(Y)
GEQ(ns(X), ns(Y)) -> GEQ(activate(X), activate(Y))
GEQ(ns(X), ns(Y)) -> ACTIVATE(X)
GEQ(ns(X), ns(Y)) -> ACTIVATE(Y)
DIV(s(X), ns(Y)) -> IF(geq(X, activate(Y)), ns(div(minus(X, activate(Y)), ns(activate(Y)))), n0)
DIV(s(X), ns(Y)) -> GEQ(X, activate(Y))
DIV(s(X), ns(Y)) -> ACTIVATE(Y)
DIV(s(X), ns(Y)) -> DIV(minus(X, activate(Y)), ns(activate(Y)))
DIV(s(X), ns(Y)) -> MINUS(X, activate(Y))
IF(true, X, Y) -> ACTIVATE(X)
IF(false, X, Y) -> ACTIVATE(Y)
ACTIVATE(n0) -> 0'
ACTIVATE(ns(X)) -> S(X)

Furthermore, R contains three SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Modular Removal of Rules
       →DP Problem 2
         ↳MRR
       →DP Problem 3
         ↳Neg POLO


Dependency Pair:

MINUS(ns(X), ns(Y)) -> MINUS(activate(X), activate(Y))


Rules:


minus(n0, Y) -> 0
minus(ns(X), ns(Y)) -> minus(activate(X), activate(Y))
geq(X, n0) -> true
geq(n0, ns(Y)) -> false
geq(ns(X), ns(Y)) -> geq(activate(X), activate(Y))
div(0, ns(Y)) -> 0
div(s(X), ns(Y)) -> if(geq(X, activate(Y)), ns(div(minus(X, activate(Y)), ns(activate(Y)))), n0)
if(true, X, Y) -> activate(X)
if(false, X, Y) -> activate(Y)
0 -> n0
s(X) -> ns(X)
activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X





We have the following set of usable rules:

activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X
0 -> n0
s(X) -> ns(X)
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(activate(x1))=  x1  
  POL(0)=  0  
  POL(MINUS(x1, x2))=  x1 + x2  
  POL(n__s(x1))=  x1  
  POL(n__0)=  0  
  POL(s(x1))=  x1  

We have the following set D of usable symbols: {activate, 0, MINUS, ns, n0, s}
No Dependency Pairs can be deleted.
9 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 4
             ↳Modular Removal of Rules
       →DP Problem 2
         ↳MRR
       →DP Problem 3
         ↳Neg POLO


Dependency Pair:

MINUS(ns(X), ns(Y)) -> MINUS(activate(X), activate(Y))


Rules:


activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X
0 -> n0
s(X) -> ns(X)





We have the following set of usable rules:

activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X
0 -> n0
s(X) -> ns(X)
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(activate(x1))=  x1  
  POL(0)=  0  
  POL(MINUS(x1, x2))=  1 + x1 + x2  
  POL(n__s(x1))=  1 + x1  
  POL(n__0)=  0  
  POL(s(x1))=  1 + x1  

We have the following set D of usable symbols: {activate, 0, MINUS, ns, n0, s}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

MINUS(ns(X), ns(Y)) -> MINUS(activate(X), activate(Y))

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved. 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳Modular Removal of Rules
       →DP Problem 3
         ↳Neg POLO


Dependency Pair:

GEQ(ns(X), ns(Y)) -> GEQ(activate(X), activate(Y))


Rules:


minus(n0, Y) -> 0
minus(ns(X), ns(Y)) -> minus(activate(X), activate(Y))
geq(X, n0) -> true
geq(n0, ns(Y)) -> false
geq(ns(X), ns(Y)) -> geq(activate(X), activate(Y))
div(0, ns(Y)) -> 0
div(s(X), ns(Y)) -> if(geq(X, activate(Y)), ns(div(minus(X, activate(Y)), ns(activate(Y)))), n0)
if(true, X, Y) -> activate(X)
if(false, X, Y) -> activate(Y)
0 -> n0
s(X) -> ns(X)
activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X





We have the following set of usable rules:

activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X
0 -> n0
s(X) -> ns(X)
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(GEQ(x1, x2))=  x1 + x2  
  POL(activate(x1))=  x1  
  POL(0)=  0  
  POL(n__s(x1))=  x1  
  POL(n__0)=  0  
  POL(s(x1))=  x1  

We have the following set D of usable symbols: {GEQ, activate, 0, ns, n0, s}
No Dependency Pairs can be deleted.
9 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳MRR
           →DP Problem 5
             ↳Modular Removal of Rules
       →DP Problem 3
         ↳Neg POLO


Dependency Pair:

GEQ(ns(X), ns(Y)) -> GEQ(activate(X), activate(Y))


Rules:


activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X
0 -> n0
s(X) -> ns(X)





We have the following set of usable rules:

activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X
0 -> n0
s(X) -> ns(X)
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(GEQ(x1, x2))=  1 + x1 + x2  
  POL(activate(x1))=  x1  
  POL(0)=  0  
  POL(n__s(x1))=  1 + x1  
  POL(n__0)=  0  
  POL(s(x1))=  1 + x1  

We have the following set D of usable symbols: {GEQ, activate, 0, ns, n0, s}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

GEQ(ns(X), ns(Y)) -> GEQ(activate(X), activate(Y))

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved. 



   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳MRR
       →DP Problem 3
         ↳Negative Polynomial Order


Dependency Pair:

DIV(s(X), ns(Y)) -> DIV(minus(X, activate(Y)), ns(activate(Y)))


Rules:


minus(n0, Y) -> 0
minus(ns(X), ns(Y)) -> minus(activate(X), activate(Y))
geq(X, n0) -> true
geq(n0, ns(Y)) -> false
geq(ns(X), ns(Y)) -> geq(activate(X), activate(Y))
div(0, ns(Y)) -> 0
div(s(X), ns(Y)) -> if(geq(X, activate(Y)), ns(div(minus(X, activate(Y)), ns(activate(Y)))), n0)
if(true, X, Y) -> activate(X)
if(false, X, Y) -> activate(Y)
0 -> n0
s(X) -> ns(X)
activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X





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

DIV(s(X), ns(Y)) -> DIV(minus(X, activate(Y)), ns(activate(Y)))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

minus(n0, Y) -> 0
minus(ns(X), ns(Y)) -> minus(activate(X), activate(Y))
activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X
0 -> n0
s(X) -> ns(X)


Used ordering:
Polynomial Order with Interpretation:

POL( DIV(x1, x2) ) = x1

POL( s(x1) ) = 1

POL( minus(x1, x2) ) = 0

POL( 0 ) = 0

POL( activate(x1) ) = x1

POL( ns(x1) ) = 1

POL( n0 ) = 0


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
       →DP Problem 2
         ↳MRR
       →DP Problem 3
         ↳Neg POLO
           →DP Problem 6
             ↳Dependency Graph


Dependency Pair:


Rules:


minus(n0, Y) -> 0
minus(ns(X), ns(Y)) -> minus(activate(X), activate(Y))
geq(X, n0) -> true
geq(n0, ns(Y)) -> false
geq(ns(X), ns(Y)) -> geq(activate(X), activate(Y))
div(0, ns(Y)) -> 0
div(s(X), ns(Y)) -> if(geq(X, activate(Y)), ns(div(minus(X, activate(Y)), ns(activate(Y)))), n0)
if(true, X, Y) -> activate(X)
if(false, X, Y) -> activate(Y)
0 -> n0
s(X) -> ns(X)
activate(n0) -> 0
activate(ns(X)) -> s(X)
activate(X) -> X





Using the Dependency Graph resulted in no new DP problems.

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