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. 



   TRS
     ↳Removing Redundant Rules



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

old(serve) -> free(serve)

where the Polynomial interpretation:
  POL(top(x1))=  x1  
  POL(serve)=  1  
  POL(old(x1))=  2·x1  
  POL(free(x1))=  x1  
  POL(check(x1))=  x1  
  POL(new(x1))=  x1  
was used.

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


   TRS
     ↳RRRPolo
       →TRS2
         ↳Removing Redundant Rules



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(x1))=  1 + x1  
  POL(old(x1))=  2·x1  
  POL(check(x1))=  x1  
  POL(free(x1))=  1 + x1  
  POL(new(x1))=  1 + x1  
was used.

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


   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳Removing Redundant Rules



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(x1))=  x1  
  POL(old(x1))=  1 + x1  
  POL(check(x1))=  2·x1  
  POL(free(x1))=  2·x1  
  POL(new(x1))=  x1  
was used.

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


   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳RRRPolo
             ...
               →TRS4
                 ↳Dependency Pair Analysis



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. 


   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳RRRPolo
             ...
               →DP Problem 1
                 ↳Modular Removal of Rules


Dependency Pair:

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


Rules:


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





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(NEW(x1))=  x1  
  POL(free(x1))=  x1  

We have the following set D of usable symbols: {NEW}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

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

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. 



   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳RRRPolo
             ...
               →DP Problem 2
                 ↳Modular Removal of Rules


Dependency Pairs:

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


Rules:


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





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(free(x1))=  x1  
  POL(CHECK(x1))=  x1  
  POL(new(x1))=  x1  

We have the following set D of usable symbols: {CHECK}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

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

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. 



   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳RRRPolo
             ...
               →DP Problem 3
                 ↳Modular Removal of Rules


Dependency Pair:

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


Rules:


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





We have the following set of usable rules:

check(new(x)) -> new(check(x))
check(free(x)) -> free(check(x))
new(free(x)) -> free(new(x))
new(serve) -> free(serve)
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(serve)=  0  
  POL(free(x1))=  x1  
  POL(check(x1))=  x1  
  POL(TOP(x1))=  1 + x1  
  POL(new(x1))=  x1  

We have the following set D of usable symbols: {serve, free, check, TOP, new}
No Dependency Pairs can be deleted.
1 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳RRRPolo
             ...
               →DP Problem 4
                 ↳Narrowing Transformation


Dependency Pair:

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


Rules:


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





On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

TOP(free(x)) -> TOP(check(new(x)))
three new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳RRRPolo
             ...
               →DP Problem 5
                 ↳Negative Polynomial Order


Dependency Pairs:

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


Rules:


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





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

TOP(free(serve)) -> TOP(check(free(serve)))


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

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


Used ordering:
Polynomial Order with Interpretation:

POL( TOP(x1) ) = x1

POL( free(x1) ) = x1

POL( serve ) = 1

POL( check(x1) ) = 0

POL( new(x1) ) = x1


This results in one new DP problem. 


   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳RRRPolo
             ...
               →DP Problem 6
                 ↳Semantic Labelling


Dependency Pairs:

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


Rules:


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





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

From the dependency graph we obtain 1 (labeled) SCCs which each result in correspondingDP problem.


   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳RRRPolo
             ...
               →DP Problem 7
                 ↳Modular Removal of Rules


Dependency Pairs:

TOP1(free1(x'')) -> TOP1(new1(check1(x'')))
TOP1(free1(free1(x''))) -> TOP1(check1(free1(new1(x''))))


Rules:


check0(new0(x)) -> new1(check0(x))
check0(free0(x)) -> free1(check0(x))
new0(free0(x)) -> free0(new0(x))
new0(serve) -> free0(serve)
new1(free1(x)) -> free1(new1(x))
check1(new1(x)) -> new1(check1(x))
check1(free1(x)) -> free1(check1(x))





We have the following set of usable rules:

new1(free1(x)) -> free1(new1(x))
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(free_1(x1))=  x1  
  POL(check_1(x1))=  x1  
  POL(TOP_1(x1))=  1 + x1  
  POL(new_1(x1))=  x1  

We have the following set D of usable symbols: {free1, check1, TOP1, new1}
No Dependency Pairs can be deleted.
4 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   TRS
     ↳RRRPolo
       →TRS2
         ↳RRRPolo
           →TRS3
             ↳RRRPolo
             ...
               →DP Problem 8
                 ↳Modular Removal of Rules


Dependency Pairs:

TOP1(free1(free1(x''))) -> TOP1(check1(free1(new1(x''))))
TOP1(free1(x'')) -> TOP1(new1(check1(x'')))


Rules:


new1(free1(x)) -> free1(new1(x))
check1(free1(x)) -> free1(check1(x))
check1(new1(x)) -> new1(check1(x))





We have the following set of usable rules:

check1(free1(x)) -> free1(check1(x))
new1(free1(x)) -> free1(new1(x))
check1(new1(x)) -> new1(check1(x))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(free_1(x1))=  1 + x1  
  POL(check_1(x1))=  x1  
  POL(TOP_1(x1))=  1 + x1  
  POL(new_1(x1))=  x1  

We have the following set D of usable symbols: {free1, check1, TOP1, new1}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

TOP1(free1(free1(x''))) -> TOP1(check1(free1(new1(x''))))
TOP1(free1(x'')) -> TOP1(new1(check1(x'')))

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.


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