Term Rewriting System R:

   [x, y]
   top(sent(x)) -> top(check(rest(x)))
   rest(nil) -> sent(nil)
   rest(cons(x, y)) -> sent(y)
   check(sent(x)) -> sent(check(x))
   check(rest(x)) -> rest(check(x))
   check(cons(x, y)) -> cons(check(x), y)
   check(cons(x, y)) -> cons(x, check(y))
   check(cons(x, y)) -> cons(x, y)

Termination of R to be shown.


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

   rest(cons(x, y)) -> sent(y)

where the Polynomial interpretation:
POL(nil) = 0
POL(top(x_1)) = 1 + x_1
POL(rest(x_1)) = x_1
POL(check(x_1)) = x_1
POL(sent(x_1)) = x_1
POL(cons(x_1, x_2)) = 1 + 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: 

   check(cons(x, y)) -> cons(check(x), y)
   check(cons(x, y)) -> cons(x, check(y))
   check(cons(x, y)) -> cons(x, y)

where the Polynomial interpretation:
POL(nil) = 0
POL(top(x_1)) = 2 + x_1
POL(rest(x_1)) = x_1
POL(check(x_1)) = 2*x_1
POL(sent(x_1)) = 2*x_1
POL(cons(x_1, x_2)) = 1 + x_1 + x_2
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(sent(x)) -> CHECK(x)
   CHECK(rest(x)) -> REST(check(x))
   CHECK(rest(x)) -> CHECK(x)
   TOP(sent(x)) -> TOP(check(rest(x)))
   TOP(sent(x)) -> CHECK(rest(x))
   TOP(sent(x)) -> REST(x)

Furthermore, R contains two SCCs.


SCC1:

CHECK(rest(x)) -> CHECK(x)
CHECK(sent(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)) = 1 + x_1
POL(rest(x_1)) = 1 + x_1
POL(sent(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   CHECK(rest(x)) -> CHECK(x)
   CHECK(sent(x)) -> CHECK(x)



 This transformation is resulting in no new subcycles.


SCC2:

TOP(sent(x)) -> TOP(check(rest(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(nil) = 0
POL(rest(x_1)) = x_1
POL(TOP(x_1)) = 1 + x_1
POL(check(x_1)) = x_1
POL(sent(x_1)) = x_1

No Dependency Pairs can be deleted.

The following rules of R can be deleted: 

   top(sent(x)) -> top(check(rest(x)))


 This transformation is resulting in one new subcycle:


SCC2.MRR1:

TOP(sent(x)) -> TOP(check(rest(x)))

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

   TOP(sent(x)) -> TOP(check(rest(x)))
two new Dependency Pairs
are created:


   TOP(sent(x'')) -> TOP(rest(check(x'')))
   TOP(sent(nil)) -> TOP(check(sent(nil)))

The transformation is resulting in one subcycle:


SCC2.MRR1.Nar1:

TOP(sent(nil)) -> TOP(check(sent(nil)))
TOP(sent(x'')) -> TOP(rest(check(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: 

   check(sent(x)) -> sent(check(x))
   check(rest(x)) -> rest(check(x))
   rest(nil) -> sent(nil)


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 1
POL(rest(x_1)) = x_1
POL(TOP(x_1)) = x_1
POL(check(x_1)) = 0
POL(sent(x_1)) = x_1

 resulting in one subcycle.


SCC2.MRR1.Nar1.Polo1:

TOP(sent(x'')) -> TOP(rest(check(x'')))

The Estimated Dependency Pair Graph for R contains the following SCC: 

TOP(sent(x'')) -> TOP(rest(check(x'')))
Rule(s) before reversing: 

   rest(nil) -> sent(nil)
   check(sent(x)) -> sent(check(x))
   check(rest(x)) -> rest(check(x))
   TOP(sent(x'')) -> TOP(rest(check(x'')))


(Re)applying the dependency pair methods for the following TRS:
   nil(rest(x)) -> nil(sent(x))
   rest(check(x)) -> check(rest(x))
   sent(check(x)) -> check(sent(x))
   sent(TOP(x)) -> check(rest(TOP(x)))
 resulting in three new SCCs:

   REST(check(x)) -> REST(x), SENT(check(x)) -> SENT(x), NIL(rest(x)) -> NIL(sent(x))
SCC2.MRR1.Nar1.Polo1.Rev1:

REST(check(x)) -> REST(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(REST(x_1)) = 1 + x_1
POL(check(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   REST(check(x)) -> REST(x)



 This transformation is resulting in no new subcycles.


SCC2.MRR1.Nar1.Polo1.Rev2:

SENT(check(x)) -> SENT(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(SENT(x_1)) = 1 + x_1
POL(check(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   SENT(check(x)) -> SENT(x)



 This transformation is resulting in no new subcycles.


SCC2.MRR1.Nar1.Polo1.Rev3:

NIL(rest(x)) -> NIL(sent(x))

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

   NIL(rest(x)) -> NIL(sent(x))
two new Dependency Pairs
are created:


   NIL(rest(check(x''))) -> NIL(check(sent(x'')))
   NIL(rest(TOP(x''))) -> NIL(check(rest(TOP(x''))))

The transformation is resulting in no subcycles.




Termination of R successfully shown.


Duration: 21.39 seconds.