Term Rewriting System R:

   [Y, X]
   plus(0, Y) -> Y
   plus(s(X), Y) -> s(plus(X, Y))
   min(X, 0) -> X
   min(s(X), s(Y)) -> min(X, Y)
   min(min(X, Y), Z) -> min(X, plus(Y, Z))
   quot(0, s(Y)) -> 0
   quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   PLUS(s(X), Y) -> PLUS(X, Y)
   QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
   QUOT(s(X), s(Y)) -> MIN(X, Y)
   MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
   MIN(min(X, Y), Z) -> PLUS(Y, Z)
   MIN(s(X), s(Y)) -> MIN(X, Y)

Furthermore, R contains three SCCs.


SCC1:

PLUS(s(X), Y) -> PLUS(X, Y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(PLUS(x_1, x_2)) = 1 + x_1 + x_2
POL(s(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   PLUS(s(X), Y) -> PLUS(X, Y)



 This transformation is resulting in no new subcycles.


SCC2:

MIN(s(X), s(Y)) -> MIN(X, Y)
MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = x_1
POL(plus(x_1, x_2)) = x_1 + x_2
POL(MIN(x_1, x_2)) = x_1 + x_2
POL(Z) = 0
POL(min(x_1, x_2)) = x_1 + x_2
POL(0) = 1

The following Dependency Pairs can be deleted:

   MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))

The following rules of R can be deleted: 

   quot(0, s(Y)) -> 0
   quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
   min(min(X, Y), Z) -> min(X, plus(Y, Z))
   min(s(X), s(Y)) -> min(X, Y)
   min(X, 0) -> X
   plus(0, Y) -> Y


 This transformation is resulting in one new subcycle:


SCC2.MRR1:

MIN(s(X), s(Y)) -> MIN(X, Y)

Removing rules from R by ordering and analyzing Dependency Pairs, Usable Rules, and Usable Equations.

This is possible by using the following (C_E-compatible) Polynomial ordering.

Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(MIN(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   MIN(s(X), s(Y)) -> MIN(X, Y)



 This transformation is resulting in no new subcycles.


SCC3:

QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))

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

Additionally, the following rules can be oriented: 

   min(min(X, Y), Z) -> min(X, plus(Y, Z))
   min(s(X), s(Y)) -> min(X, Y)
   min(X, 0) -> X


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(plus(x_1, x_2)) = 0
POL(s(x_1)) = 1 + x_1
POL(Z) = 0
POL(QUOT(x_1, x_2)) = 1 + x_1
POL(min(x_1, x_2)) = x_1
POL(0) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.643 seconds.