Term Rewriting System R:

   [y, x, z]
   minus_active(0, y) -> 0
   minus_active(s(x), s(y)) -> minus_active(x, y)
   minus_active(x, y) -> minus(x, y)
   mark(0) -> 0
   mark(s(x)) -> s(mark(x))
   mark(minus(x, y)) -> minus_active(x, y)
   mark(ge(x, y)) -> ge_active(x, y)
   mark(div(x, y)) -> div_active(mark(x), y)
   mark(if(x, y, z)) -> if_active(mark(x), y, z)
   ge_active(x, 0) -> true
   ge_active(0, s(y)) -> false
   ge_active(s(x), s(y)) -> ge_active(x, y)
   ge_active(x, y) -> ge(x, y)
   div_active(0, s(y)) -> 0
   div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
   div_active(x, y) -> div(x, y)
   if_active(true, x, y) -> mark(x)
   if_active(false, x, y) -> mark(y)
   if_active(x, y, z) -> if(x, y, z)

Termination of R to be shown.


R contains the following Dependency Pairs: 


   IF_ACTIVE(true, x, y) -> MARK(x)
   IF_ACTIVE(false, x, y) -> MARK(y)
   MARK(div(x, y)) -> DIV_ACTIVE(mark(x), y)
   MARK(div(x, y)) -> MARK(x)
   MARK(minus(x, y)) -> MINUS_ACTIVE(x, y)
   MARK(s(x)) -> MARK(x)
   MARK(ge(x, y)) -> GE_ACTIVE(x, y)
   MARK(if(x, y, z)) -> IF_ACTIVE(mark(x), y, z)
   MARK(if(x, y, z)) -> MARK(x)
   DIV_ACTIVE(s(x), s(y)) -> IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
   DIV_ACTIVE(s(x), s(y)) -> GE_ACTIVE(x, y)
   MINUS_ACTIVE(s(x), s(y)) -> MINUS_ACTIVE(x, y)
   GE_ACTIVE(s(x), s(y)) -> GE_ACTIVE(x, y)

Furthermore, R contains three SCCs.


SCC1:

MINUS_ACTIVE(s(x), s(y)) -> MINUS_ACTIVE(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(MINUS_ACTIVE(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   MINUS_ACTIVE(s(x), s(y)) -> MINUS_ACTIVE(x, y)



 This transformation is resulting in no new subcycles.


SCC2:

GE_ACTIVE(s(x), s(y)) -> GE_ACTIVE(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(GE_ACTIVE(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   GE_ACTIVE(s(x), s(y)) -> GE_ACTIVE(x, y)



 This transformation is resulting in no new subcycles.


SCC3:

MARK(if(x, y, z)) -> MARK(x)
MARK(if(x, y, z)) -> IF_ACTIVE(mark(x), y, z)
MARK(s(x)) -> MARK(x)
MARK(div(x, y)) -> MARK(x)
IF_ACTIVE(false, x, y) -> MARK(y)
DIV_ACTIVE(s(x), s(y)) -> IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(x, y)) -> DIV_ACTIVE(mark(x), y)
IF_ACTIVE(true, x, y) -> MARK(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(s(x_1)) = x_1
POL(IF_ACTIVE(x_1, x_2, x_3)) = x_2 + x_3
POL(minus(x_1, x_2)) = 0
POL(MARK(x_1)) = x_1
POL(mark(x_1)) = 0
POL(div_active(x_1, x_2)) = 0
POL(0) = 0
POL(if_active(x_1, x_2, x_3)) = 0
POL(DIV_ACTIVE(x_1, x_2)) = 0
POL(div(x_1, x_2)) = x_1
POL(ge(x_1, x_2)) = 0
POL(true) = 0
POL(if(x_1, x_2, x_3)) = 1 + x_1 + x_2 + x_3
POL(ge_active(x_1, x_2)) = 0
POL(false) = 0
POL(minus_active(x_1, x_2)) = 0

 resulting in one subcycle.


SCC3.Polo1:

IF_ACTIVE(false, x, y) -> MARK(y)
MARK(div(x, y)) -> MARK(x)
IF_ACTIVE(true, x, y) -> MARK(x)
DIV_ACTIVE(s(x), s(y)) -> IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(x, y)) -> DIV_ACTIVE(mark(x), y)
MARK(s(x)) -> MARK(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(s(x_1)) = x_1
POL(IF_ACTIVE(x_1, x_2, x_3)) = x_2 + x_3
POL(minus(x_1, x_2)) = 0
POL(MARK(x_1)) = x_1
POL(mark(x_1)) = 0
POL(div_active(x_1, x_2)) = 0
POL(0) = 0
POL(if_active(x_1, x_2, x_3)) = 0
POL(DIV_ACTIVE(x_1, x_2)) = 1
POL(true) = 0
POL(ge(x_1, x_2)) = 0
POL(div(x_1, x_2)) = 1 + x_1
POL(if(x_1, x_2, x_3)) = 0
POL(ge_active(x_1, x_2)) = 0
POL(minus_active(x_1, x_2)) = 0
POL(false) = 0

 resulting in one subcycle.


SCC3.Polo1.Polo1:

MARK(s(x)) -> MARK(x)
IF_ACTIVE(true, x, y) -> MARK(x)
DIV_ACTIVE(s(x), s(y)) -> IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(x, y)) -> DIV_ACTIVE(mark(x), y)
IF_ACTIVE(false, x, y) -> MARK(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: 

   if_active(true, x, y) -> mark(x)
   if_active(x, y, z) -> if(x, y, z)
   if_active(false, x, y) -> mark(y)
   mark(div(x, y)) -> div_active(mark(x), y)
   mark(minus(x, y)) -> minus_active(x, y)
   mark(s(x)) -> s(mark(x))
   mark(ge(x, y)) -> ge_active(x, y)
   mark(if(x, y, z)) -> if_active(mark(x), y, z)
   mark(0) -> 0
   div_active(0, s(y)) -> 0
   div_active(x, y) -> div(x, y)
   div_active(s(x), s(y)) -> if_active(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
   ge_active(s(x), s(y)) -> ge_active(x, y)
   ge_active(x, 0) -> true
   ge_active(0, s(y)) -> false
   ge_active(x, y) -> ge(x, y)
   minus_active(s(x), s(y)) -> minus_active(x, y)
   minus_active(0, y) -> 0
   minus_active(x, y) -> minus(x, y)


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(s(x_1)) = 1 + x_1
POL(IF_ACTIVE(x_1, x_2, x_3)) = x_2 + x_3
POL(minus(x_1, x_2)) = 0
POL(MARK(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(div_active(x_1, x_2)) = x_1
POL(0) = 0
POL(if_active(x_1, x_2, x_3)) = x_2 + x_3
POL(DIV_ACTIVE(x_1, x_2)) = x_1
POL(true) = 0
POL(ge(x_1, x_2)) = 0
POL(div(x_1, x_2)) = x_1
POL(if(x_1, x_2, x_3)) = x_2 + x_3
POL(ge_active(x_1, x_2)) = 0
POL(minus_active(x_1, x_2)) = 0
POL(false) = 0

 resulting in one subcycle.


SCC3.Polo1.Polo1.Polo1:

IF_ACTIVE(false, x, y) -> MARK(y)
DIV_ACTIVE(s(x), s(y)) -> IF_ACTIVE(ge_active(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(x, y)) -> DIV_ACTIVE(mark(x), y)
IF_ACTIVE(true, x, y) -> MARK(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(s(x_1)) = 0
POL(IF_ACTIVE(x_1, x_2, x_3)) = 1 + x_2 + x_3
POL(minus(x_1, x_2)) = 0
POL(MARK(x_1)) = x_1
POL(mark(x_1)) = 0
POL(div_active(x_1, x_2)) = 0
POL(0) = 0
POL(if_active(x_1, x_2, x_3)) = 0
POL(DIV_ACTIVE(x_1, x_2)) = 1
POL(true) = 0
POL(ge(x_1, x_2)) = 0
POL(div(x_1, x_2)) = 1
POL(if(x_1, x_2, x_3)) = 0
POL(ge_active(x_1, x_2)) = 0
POL(minus_active(x_1, x_2)) = 0
POL(false) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 2.584 seconds.