Term Rewriting System R:

   [x]
   active(f(x)) -> mark(f(f(x)))
   chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
   chk(no(c)) -> active(c)
   mat(f(x), f(y)) -> f(mat(x, y))
   mat(f(x), c) -> no(c)
   f(active(x)) -> active(f(x))
   f(no(x)) -> no(f(x))
   f(mark(x)) -> mark(f(x))
   tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))

Termination of R to be shown.


R contains the following Dependency Pairs: 


   ACTIVE(f(x)) -> F(f(x))
   F(active(x)) -> ACTIVE(f(x))
   F(active(x)) -> F(x)
   F(mark(x)) -> F(x)
   F(no(x)) -> F(x)
   MAT(f(x), f(y)) -> F(mat(x, y))
   MAT(f(x), f(y)) -> MAT(x, y)
   CHK(no(f(x))) -> F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
   CHK(no(f(x))) -> CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))
   CHK(no(f(x))) -> MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)
   CHK(no(f(x))) -> F(f(f(f(f(f(f(f(f(f(X))))))))))
   CHK(no(f(x))) -> F(f(f(f(f(f(f(f(f(X)))))))))
   CHK(no(f(x))) -> F(f(f(f(f(f(f(f(X))))))))
   CHK(no(f(x))) -> F(f(f(f(f(f(f(X)))))))
   CHK(no(f(x))) -> F(f(f(f(f(f(X))))))
   CHK(no(f(x))) -> F(f(f(f(f(X)))))
   CHK(no(f(x))) -> F(f(f(f(X))))
   CHK(no(f(x))) -> F(f(f(X)))
   CHK(no(f(x))) -> F(f(X))
   CHK(no(f(x))) -> F(X)
   CHK(no(c)) -> ACTIVE(c)
   TP(mark(x)) -> TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
   TP(mark(x)) -> CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))
   TP(mark(x)) -> MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)
   TP(mark(x)) -> F(f(f(f(f(f(f(f(f(f(X))))))))))
   TP(mark(x)) -> F(f(f(f(f(f(f(f(f(X)))))))))
   TP(mark(x)) -> F(f(f(f(f(f(f(f(X))))))))
   TP(mark(x)) -> F(f(f(f(f(f(f(X)))))))
   TP(mark(x)) -> F(f(f(f(f(f(X))))))
   TP(mark(x)) -> F(f(f(f(f(X)))))
   TP(mark(x)) -> F(f(f(f(X))))
   TP(mark(x)) -> F(f(f(X)))
   TP(mark(x)) -> F(f(X))
   TP(mark(x)) -> F(X)

Furthermore, R contains three SCCs.


SCC1:

F(no(x)) -> F(x)
F(mark(x)) -> F(x)
F(active(x)) -> F(x)
F(active(x)) -> ACTIVE(f(x))
ACTIVE(f(x)) -> F(f(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(active(x_1)) = x_1
POL(no(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(F(x_1)) = x_1
POL(ACTIVE(x_1)) = x_1
POL(f(x_1)) = x_1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   mat(f(x), f(y)) -> f(mat(x, y))
   mat(f(x), c) -> no(c)
   chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
   chk(no(c)) -> active(c)
   tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))


 This transformation is resulting in one new subcycle:


SCC1.MRR1:

F(mark(x)) -> F(x)
F(active(x)) -> F(x)
ACTIVE(f(x)) -> F(f(x))
F(active(x)) -> ACTIVE(f(x))
F(no(x)) -> F(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(active(x_1)) = 1 + x_1
POL(no(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(F(x_1)) = x_1
POL(ACTIVE(x_1)) = x_1
POL(f(x_1)) = x_1

The following Dependency Pairs can be deleted:

   F(active(x)) -> F(x)
   F(active(x)) -> ACTIVE(f(x))
   ACTIVE(f(x)) -> F(f(x))

The following rules of R can be deleted: 

   active(f(x)) -> mark(f(f(x)))


 This transformation is resulting in one new subcycle:


SCC1.MRR1.MRR1:

F(no(x)) -> F(x)
F(mark(x)) -> F(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(no(x_1)) = 1 + x_1
POL(mark(x_1)) = 1 + x_1
POL(F(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   F(no(x)) -> F(x)
   F(mark(x)) -> F(x)



 This transformation is resulting in no new subcycles.


SCC2:

CHK(no(f(x))) -> CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), 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(mat(x_1, x_2)) = x_1 + x_2
POL(active(x_1)) = x_1
POL(X) = 0
POL(no(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(CHK(x_1)) = 1 + x_1
POL(f(x_1)) = x_1
POL(c) = 0
POL(y) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
   chk(no(c)) -> active(c)
   tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))


 This transformation is resulting in one new subcycle:


SCC2.MRR1:

CHK(no(f(x))) -> CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), 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(mat(x_1, x_2)) = x_1 + x_2
POL(active(x_1)) = 1 + x_1
POL(X) = 0
POL(no(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(CHK(x_1)) = 1 + x_1
POL(f(x_1)) = x_1
POL(c) = 0
POL(y) = 0

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   active(f(x)) -> mark(f(f(x)))


 This transformation is resulting in one new subcycle:


SCC2.MRR1.MRR1:

CHK(no(f(x))) -> CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   mat(f(x), f(y)) -> f(mat(x, y))
   mat(f(x), c) -> no(c)
   f(active(x)) -> active(f(x))
   f(mark(x)) -> mark(f(x))
   f(no(x)) -> no(f(x))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(mat(x_1, x_2)) = x_2
POL(active(x_1)) = 0
POL(X) = 0
POL(no(x_1)) = x_1
POL(mark(x_1)) = 0
POL(f(x_1)) = 1 + x_1
POL(c) = 0
POL(CHK(x_1)) = 1 + x_1
POL(y) = 1

 resulting in no subcycles.


SCC3:

TP(mark(x)) -> TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), 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(mat(x_1, x_2)) = x_1 + x_2
POL(active(x_1)) = x_1
POL(X) = 0
POL(no(x_1)) = x_1
POL(mark(x_1)) = x_1
POL(f(x_1)) = x_1
POL(c) = 0
POL(chk(x_1)) = x_1
POL(y) = 1
POL(TP(x_1)) = 1 + x_1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))


 This transformation is resulting in one new subcycle:


SCC3.MRR1:

TP(mark(x)) -> TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))

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

   TP(mark(x)) -> TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
two new Dependency Pairs
are created:


   TP(mark(f(y))) -> TP(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y))))
   TP(mark(c)) -> TP(chk(no(c)))

The transformation is resulting in one subcycle:


SCC3.MRR1.Nar1:

TP(mark(c)) -> TP(chk(no(c)))
TP(mark(f(y))) -> TP(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y))))

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

   TP(mark(f(y))) -> TP(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y))))
no new Dependency Pairs
are created.

none
The transformation is resulting in one subcycle:


SCC3.MRR1.Nar1.Nar1:

TP(mark(c)) -> TP(chk(no(c)))

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
   chk(no(c)) -> active(c)
   active(f(x)) -> mark(f(f(x)))
   f(active(x)) -> active(f(x))
   f(mark(x)) -> mark(f(x))
   f(no(x)) -> no(f(x))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(mat(x_1, x_2)) = 0
POL(active(x_1)) = 0
POL(X) = 0
POL(no(x_1)) = 0
POL(mark(x_1)) = x_1
POL(f(x_1)) = 0
POL(c) = 1
POL(chk(x_1)) = 0
POL(y) = 0
POL(TP(x_1)) = x_1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 12.859 seconds.