Term Rewriting System R:

   [x]
   top(free(x)) -> top(check(new(x)))
   new(free(x)) -> free(new(x))
   new(serve) -> free(serve)
   old(free(x)) -> free(old(x))
   old(serve) -> free(serve)
   check(free(x)) -> free(check(x))
   check(new(x)) -> new(check(x))
   check(old(x)) -> old(check(x))
   check(old(x)) -> old(x)

Termination of R to be shown.


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

   old(serve) -> free(serve)

where the Polynomial interpretation:
POL(serve) = 1
POL(top(x_1)) = x_1
POL(new(x_1)) = x_1
POL(old(x_1)) = 2*x_1
POL(check(x_1)) = x_1
POL(free(x_1)) = x_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: 

   old(free(x)) -> free(old(x))

where the Polynomial interpretation:
POL(serve) = 0
POL(top(x_1)) = 1 + x_1
POL(new(x_1)) = 1 + x_1
POL(old(x_1)) = 2*x_1
POL(check(x_1)) = x_1
POL(free(x_1)) = 1 + x_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: 

   check(old(x)) -> old(check(x))
   check(old(x)) -> old(x)

where the Polynomial interpretation:
POL(serve) = 0
POL(top(x_1)) = x_1
POL(new(x_1)) = x_1
POL(old(x_1)) = 1 + x_1
POL(check(x_1)) = 2*x_1
POL(free(x_1)) = 2*x_1
was used. 



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


R contains the following Dependency Pairs: 


   CHECK(new(x)) -> NEW(check(x))
   CHECK(new(x)) -> CHECK(x)
   CHECK(free(x)) -> CHECK(x)
   NEW(free(x)) -> NEW(x)
   TOP(free(x)) -> TOP(check(new(x)))
   TOP(free(x)) -> CHECK(new(x))
   TOP(free(x)) -> NEW(x)

Furthermore, R contains three SCCs.


SCC1:

NEW(free(x)) -> NEW(x)

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(free(x_1)) = 2 + x_1
POL(NEW(x_1)) = 2 + x_1

The following Dependency Pairs can be deleted:

   NEW(free(x)) -> NEW(x)



 This transformation is resulting in no new subcycles.


SCC2:

CHECK(free(x)) -> CHECK(x)
CHECK(new(x)) -> CHECK(x)

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(CHECK(x_1)) = 2 + x_1
POL(new(x_1)) = 2 + x_1
POL(free(x_1)) = 2 + x_1

The following Dependency Pairs can be deleted:

   CHECK(free(x)) -> CHECK(x)
   CHECK(new(x)) -> CHECK(x)



 This transformation is resulting in no new subcycles.


SCC3:

TOP(free(x)) -> TOP(check(new(x)))

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(serve) = 0
POL(new(x_1)) = x_1
POL(TOP(x_1)) = 1 + x_1
POL(check(x_1)) = x_1
POL(free(x_1)) = x_1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   top(free(x)) -> top(check(new(x)))


 This transformation is resulting in one new subcycle:


SCC3.MRR1:

TOP(free(x)) -> TOP(check(new(x)))

Using Semantic Labelling, the Scc could be transformed. The following model was found:
  check(x_0) = 1
  new(x_0) = x_0
  TOP(x_0) = 0
  free(x_0) = x_0
  serve = 0

The labeled system could be transformed as follows:
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(TOP_1(x_1)) = 1 + x_1
POL(check_1(x_1)) = x_1
POL(new_1(x_1)) = x_1
POL(free_1(x_1)) = x_1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   check_0(new_0(x)) -> new_1(check_0(x))
   check_0(free_0(x)) -> free_1(check_0(x))
   new_0(free_0(x)) -> free_0(new_0(x))
   new_0(serve) -> free_0(serve)


 This transformation is resulting in one new subcycle:


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(TOP_1(x_1)) = x_1
POL(check_1(x_1)) = x_1
POL(new_1(x_1)) = x_1
POL(free_1(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   TOP_1(free_1(x)) -> TOP_1(check_1(new_1(x)))



 This transformation is resulting in no new subcycles.


The new TRS has no more cycles!

Termination of R successfully shown.


Duration: 11.887 seconds.