Term Rewriting System R:

   [x, y]
   nats_active -> add_active(zeros_active)
   nats_active -> nats
   hd_active(x) -> hd(x)
   hd_active(cons(x, y)) -> mark(x)
   zeros_active -> cons(0, zeros)
   zeros_active -> zeros
   tl_active(x) -> tl(x)
   tl_active(cons(x, y)) -> mark(y)
   incr_active(cons(x, y)) -> cons(s(x), incr(y))
   incr_active(x) -> incr(x)
   mark(nats) -> nats_active
   mark(zeros) -> zeros_active
   mark(incr(x)) -> incr_active(mark(x))
   mark(add(x)) -> add_active(mark(x))
   mark(hd(x)) -> hd_active(mark(x))
   mark(tl(x)) -> tl_active(mark(x))
   mark(0) -> 0
   mark(s(x)) -> s(x)
   mark(cons(x, y)) -> cons(x, y)
   add_active(cons(x, y)) -> incr_active(cons(x, add(y)))
   add_active(x) -> add(x)

Termination of R to be shown.


Removing the following rules from R which fullfill a polynomial ordering: 

   nats_active -> add_active(zeros_active)

where the Polynomial interpretation:
POL(add(x_1)) = x_1
POL(s(x_1)) = x_1
POL(nats) = 1
POL(hd(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(tl(x_1)) = x_1
POL(zeros) = 0
POL(0) = 0
POL(add_active(x_1)) = x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(incr_active(x_1)) = x_1
POL(tl_active(x_1)) = x_1
POL(hd_active(x_1)) = x_1
POL(nats_active) = 1
POL(incr(x_1)) = x_1
POL(zeros_active) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   nats_active -> nats
   mark(0) -> 0
   mark(s(x)) -> s(x)
   mark(cons(x, y)) -> cons(x, y)
   zeros_active -> zeros

where the Polynomial interpretation:
POL(add(x_1)) = x_1
POL(s(x_1)) = x_1
POL(nats) = 0
POL(hd(x_1)) = x_1
POL(mark(x_1)) = 1 + x_1
POL(tl(x_1)) = x_1
POL(zeros) = 0
POL(0) = 0
POL(add_active(x_1)) = x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2
POL(incr_active(x_1)) = x_1
POL(tl_active(x_1)) = x_1
POL(hd_active(x_1)) = x_1
POL(nats_active) = 1
POL(incr(x_1)) = x_1
POL(zeros_active) = 1
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   hd_active(x) -> hd(x)
   hd_active(cons(x, y)) -> mark(x)

where the Polynomial interpretation:
POL(add(x_1)) = x_1
POL(s(x_1)) = x_1
POL(nats) = 0
POL(mark(x_1)) = 2*x_1
POL(hd(x_1)) = 1 + 2*x_1
POL(tl(x_1)) = 2*x_1
POL(zeros) = 0
POL(0) = 0
POL(add_active(x_1)) = x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(incr_active(x_1)) = x_1
POL(tl_active(x_1)) = 2*x_1
POL(hd_active(x_1)) = 2 + 2*x_1
POL(nats_active) = 0
POL(incr(x_1)) = x_1
POL(zeros_active) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   mark(nats) -> nats_active

where the Polynomial interpretation:
POL(add(x_1)) = x_1
POL(s(x_1)) = x_1
POL(nats) = 1
POL(mark(x_1)) = x_1
POL(hd(x_1)) = x_1
POL(tl(x_1)) = x_1
POL(zeros) = 0
POL(0) = 0
POL(add_active(x_1)) = x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(incr_active(x_1)) = x_1
POL(tl_active(x_1)) = x_1
POL(hd_active(x_1)) = x_1
POL(nats_active) = 0
POL(incr(x_1)) = x_1
POL(zeros_active) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   mark(zeros) -> zeros_active

where the Polynomial interpretation:
POL(add(x_1)) = x_1
POL(s(x_1)) = x_1
POL(mark(x_1)) = 2*x_1
POL(hd(x_1)) = x_1
POL(tl(x_1)) = 2*x_1
POL(zeros) = 1
POL(0) = 0
POL(add_active(x_1)) = x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(incr_active(x_1)) = x_1
POL(tl_active(x_1)) = 2*x_1
POL(hd_active(x_1)) = x_1
POL(incr(x_1)) = x_1
POL(zeros_active) = 1
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   mark(incr(x)) -> incr_active(mark(x))
   add_active(x) -> add(x)

where the Polynomial interpretation:
POL(add(x_1)) = 1 + x_1
POL(s(x_1)) = x_1
POL(mark(x_1)) = 2*x_1
POL(hd(x_1)) = x_1
POL(tl(x_1)) = 2*x_1
POL(zeros) = 0
POL(0) = 0
POL(add_active(x_1)) = 2 + x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(incr_active(x_1)) = 1 + x_1
POL(tl_active(x_1)) = 2*x_1
POL(hd_active(x_1)) = x_1
POL(incr(x_1)) = 1 + x_1
POL(zeros_active) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   mark(add(x)) -> add_active(mark(x))

where the Polynomial interpretation:
POL(add(x_1)) = 1 + x_1
POL(s(x_1)) = x_1
POL(mark(x_1)) = 2*x_1
POL(hd(x_1)) = x_1
POL(tl(x_1)) = 2*x_1
POL(zeros) = 0
POL(0) = 0
POL(add_active(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(incr_active(x_1)) = x_1
POL(tl_active(x_1)) = 2*x_1
POL(hd_active(x_1)) = x_1
POL(incr(x_1)) = x_1
POL(zeros_active) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   mark(hd(x)) -> hd_active(mark(x))

where the Polynomial interpretation:
POL(add(x_1)) = x_1
POL(s(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(tl(x_1)) = x_1
POL(hd(x_1)) = 1 + x_1
POL(zeros) = 0
POL(0) = 0
POL(add_active(x_1)) = x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(incr_active(x_1)) = x_1
POL(tl_active(x_1)) = x_1
POL(hd_active(x_1)) = x_1
POL(incr(x_1)) = x_1
POL(zeros_active) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   mark(tl(x)) -> tl_active(mark(x))
   tl_active(cons(x, y)) -> mark(y)

where the Polynomial interpretation:
POL(add(x_1)) = x_1
POL(s(x_1)) = x_1
POL(incr_active(x_1)) = x_1
POL(tl_active(x_1)) = 1 + 2*x_1
POL(tl(x_1)) = 1 + 2*x_1
POL(mark(x_1)) = 2*x_1
POL(zeros) = 0
POL(0) = 0
POL(add_active(x_1)) = x_1
POL(incr(x_1)) = x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(zeros_active) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   tl_active(x) -> tl(x)

where the Polynomial interpretation:
POL(add(x_1)) = x_1
POL(s(x_1)) = x_1
POL(incr_active(x_1)) = x_1
POL(tl_active(x_1)) = 1 + x_1
POL(tl(x_1)) = x_1
POL(zeros) = 0
POL(0) = 0
POL(add_active(x_1)) = x_1
POL(incr(x_1)) = x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(zeros_active) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   add_active(cons(x, y)) -> incr_active(cons(x, add(y)))

where the Polynomial interpretation:
POL(add(x_1)) = x_1
POL(s(x_1)) = x_1
POL(incr_active(x_1)) = x_1
POL(zeros) = 0
POL(0) = 0
POL(incr(x_1)) = x_1
POL(add_active(x_1)) = 1 + x_1
POL(cons(x_1, x_2)) = x_1 + x_2
POL(zeros_active) = 0
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   incr_active(cons(x, y)) -> cons(s(x), incr(y))
   incr_active(x) -> incr(x)

where the Polynomial interpretation:
POL(s(x_1)) = x_1
POL(incr_active(x_1)) = 1 + x_1
POL(zeros) = 0
POL(0) = 0
POL(incr(x_1)) = x_1
POL(zeros_active) = 0
POL(cons(x_1, x_2)) = x_1 + x_2
was used. 



Not all Rules of R can be deleted, so we still have to regard a part of R.


Removing the following rules from R which fullfill a polynomial ordering: 

   zeros_active -> cons(0, zeros)

where the Polynomial interpretation:
POL(zeros) = 0
POL(0) = 0
POL(zeros_active) = 1
POL(cons(x_1, x_2)) = x_1 + x_2
was used. 



All Rules of R can be deleted.



Termination of R successfully shown.


Duration: 0.655 seconds.