Term Rewriting System R:
[X]
active(f(X)) -> mark(g(h(f(X))))
active(f(X)) -> f(active(X))
active(h(X)) -> h(active(X))
f(mark(X)) -> mark(f(X))
f(ok(X)) -> ok(f(X))
h(mark(X)) -> mark(h(X))
h(ok(X)) -> ok(h(X))
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
proper(h(X)) -> h(proper(X))
g(ok(X)) -> ok(g(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))

Termination of R to be shown.



   TRS
Removing Redundant Rules



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

top(ok(X)) -> top(active(X))

where the Polynomial interpretation:
  POL(top(x1))=  1 + x1  
  POL(active(x1))=  x1  
  POL(proper(x1))=  x1  
  POL(g(x1))=  x1  
  POL(h(x1))=  x1  
  POL(mark(x1))=  x1  
  POL(ok(x1))=  1 + x1  
  POL(f(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:

active(f(X)) -> f(active(X))
active(f(X)) -> mark(g(h(f(X))))

where the Polynomial interpretation:
  POL(top(x1))=  1 + x1  
  POL(active(x1))=  2·x1  
  POL(proper(x1))=  x1  
  POL(g(x1))=  x1  
  POL(h(x1))=  x1  
  POL(mark(x1))=  x1  
  POL(ok(x1))=  x1  
  POL(f(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:

proper(g(X)) -> g(proper(X))

where the Polynomial interpretation:
  POL(top(x1))=  x1  
  POL(proper(x1))=  2·x1  
  POL(active(x1))=  x1  
  POL(g(x1))=  1 + x1  
  POL(h(x1))=  x1  
  POL(mark(x1))=  2·x1  
  POL(ok(x1))=  x1  
  POL(f(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
Removing Redundant Rules



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

active(h(X)) -> h(active(X))

where the Polynomial interpretation:
  POL(top(x1))=  x1  
  POL(proper(x1))=  x1  
  POL(active(x1))=  2·x1  
  POL(g(x1))=  x1  
  POL(h(x1))=  1 + x1  
  POL(mark(x1))=  x1  
  POL(ok(x1))=  x1  
  POL(f(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
             ...
               →TRS5
Removing Redundant Rules



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

top(mark(X)) -> top(proper(X))

where the Polynomial interpretation:
  POL(top(x1))=  x1  
  POL(proper(x1))=  x1  
  POL(g(x1))=  x1  
  POL(h(x1))=  x1  
  POL(mark(x1))=  1 + x1  
  POL(ok(x1))=  x1  
  POL(f(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
             ...
               →TRS6
Removing Redundant Rules



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

h(mark(X)) -> mark(h(X))

where the Polynomial interpretation:
  POL(proper(x1))=  x1  
  POL(g(x1))=  x1  
  POL(h(x1))=  2·x1  
  POL(mark(x1))=  1 + x1  
  POL(ok(x1))=  x1  
  POL(f(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
             ...
               →TRS7
Removing Redundant Rules



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

proper(h(X)) -> h(proper(X))

where the Polynomial interpretation:
  POL(proper(x1))=  2·x1  
  POL(g(x1))=  x1  
  POL(h(x1))=  1 + x1  
  POL(mark(x1))=  x1  
  POL(ok(x1))=  x1  
  POL(f(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
             ...
               →TRS8
Removing Redundant Rules



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

f(mark(X)) -> mark(f(X))

where the Polynomial interpretation:
  POL(proper(x1))=  x1  
  POL(g(x1))=  x1  
  POL(h(x1))=  x1  
  POL(mark(x1))=  1 + x1  
  POL(ok(x1))=  x1  
  POL(f(x1))=  2·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
             ...
               →TRS9
Removing Redundant Rules



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

proper(f(X)) -> f(proper(X))

where the Polynomial interpretation:
  POL(proper(x1))=  2·x1  
  POL(g(x1))=  x1  
  POL(h(x1))=  x1  
  POL(ok(x1))=  x1  
  POL(f(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
RRRPolo
             ...
               →TRS10
Removing Redundant Rules



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

f(ok(X)) -> ok(f(X))

where the Polynomial interpretation:
  POL(g(x1))=  x1  
  POL(h(x1))=  x1  
  POL(ok(x1))=  1 + x1  
  POL(f(x1))=  2·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
             ...
               →TRS11
Removing Redundant Rules



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

g(ok(X)) -> ok(g(X))

where the Polynomial interpretation:
  POL(g(x1))=  2·x1  
  POL(h(x1))=  x1  
  POL(ok(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
RRRPolo
             ...
               →TRS12
Removing Redundant Rules



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

h(ok(X)) -> ok(h(X))

where the Polynomial interpretation:
  POL(h(x1))=  2·x1  
  POL(ok(x1))=  1 + x1  
was used.

All Rules of R can be deleted.


   TRS
RRRPolo
       →TRS2
RRRPolo
           →TRS3
RRRPolo
             ...
               →TRS13
Dependency Pair Analysis



R contains no Dependency Pairs and therefore no SCCs.

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