Term Rewriting System R:

   [m, n, x, k]
   eq(0, 0) -> true
   eq(0, s(m)) -> false
   eq(s(n), 0) -> false
   eq(s(n), s(m)) -> eq(n, m)
   le(0, m) -> true
   le(s(n), 0) -> false
   le(s(n), s(m)) -> le(n, m)
   min(cons(0, nil)) -> 0
   min(cons(s(n), nil)) -> s(n)
   min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
   if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
   if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
   replace(n, m, nil) -> nil
   replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
   if_replace(true, n, m, cons(k, x)) -> cons(m, x)
   if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
   sort(nil) -> nil
   sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Innermost Termination of R to be shown.


R contains the following Dependency Pairs: 


   IF_MIN(true, cons(n, cons(m, x))) -> MIN(cons(n, x))
   IF_MIN(false, cons(n, cons(m, x))) -> MIN(cons(m, x))
   MIN(cons(n, cons(m, x))) -> IF_MIN(le(n, m), cons(n, cons(m, x)))
   MIN(cons(n, cons(m, x))) -> LE(n, m)
   EQ(s(n), s(m)) -> EQ(n, m)
   LE(s(n), s(m)) -> LE(n, m)
   REPLACE(n, m, cons(k, x)) -> IF_REPLACE(eq(n, k), n, m, cons(k, x))
   REPLACE(n, m, cons(k, x)) -> EQ(n, k)
   IF_REPLACE(false, n, m, cons(k, x)) -> REPLACE(n, m, x)
   SORT(cons(n, x)) -> MIN(cons(n, x))
   SORT(cons(n, x)) -> SORT(replace(min(cons(n, x)), n, x))
   SORT(cons(n, x)) -> REPLACE(min(cons(n, x)), n, x)

Furthermore, R contains five SCCs.


SCC1:

LE(s(n), s(m)) -> LE(n, m)

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(LE(x_1, x_2)) = 1 + x_1 + x_2
POL(s(x_1)) = 1 + x_1

The following Dependency Pairs can be deleted:

   LE(s(n), s(m)) -> LE(n, m)



 This transformation is resulting in no new subcycles.


SCC2:

EQ(s(n), s(m)) -> EQ(n, m)

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(s(x_1)) = 1 + x_1
POL(EQ(x_1, x_2)) = 1 + x_1 + x_2

The following Dependency Pairs can be deleted:

   EQ(s(n), s(m)) -> EQ(n, m)



 This transformation is resulting in no new subcycles.


SCC3:

IF_MIN(false, cons(n, cons(m, x))) -> MIN(cons(m, x))
MIN(cons(n, cons(m, x))) -> IF_MIN(le(n, m), cons(n, cons(m, x)))
IF_MIN(true, cons(n, cons(m, x))) -> MIN(cons(n, x))

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

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(IF_MIN(x_1, x_2)) = x_2
POL(s(x_1)) = 0
POL(le(x_1, x_2)) = 0
POL(MIN(x_1)) = x_1
POL(true) = 0
POL(0) = 0
POL(false) = 0
POL(cons(x_1, x_2)) = 1 + x_2

 resulting in no subcycles.


SCC4:

IF_REPLACE(false, n, m, cons(k, x)) -> REPLACE(n, m, x)
REPLACE(n, m, cons(k, x)) -> IF_REPLACE(eq(n, k), n, m, cons(k, x))

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

No rules need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
POL(s(x_1)) = 0
POL(IF_REPLACE(x_1, x_2, x_3, x_4)) = x_4
POL(eq(x_1, x_2)) = 0
POL(true) = 0
POL(REPLACE(x_1, x_2, x_3)) = x_3
POL(0) = 0
POL(false) = 0
POL(cons(x_1, x_2)) = 1 + x_2

 resulting in no subcycles.


SCC5:

SORT(cons(n, x)) -> SORT(replace(min(cons(n, x)), n, 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: 

   if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
   if_replace(true, n, m, cons(k, x)) -> cons(m, x)
   replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
   replace(n, m, nil) -> nil


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(s(x_1)) = 0
POL(eq(x_1, x_2)) = 0
POL(min(x_1)) = 0
POL(0) = 0
POL(replace(x_1, x_2, x_3)) = x_3
POL(if_replace(x_1, x_2, x_3, x_4)) = x_4
POL(cons(x_1, x_2)) = 1 + x_2
POL(le(x_1, x_2)) = 0
POL(if_min(x_1, x_2)) = 0
POL(SORT(x_1)) = x_1
POL(true) = 0
POL(false) = 0

 resulting in no subcycles.




Innermost Termination of R successfully shown.


Duration: 1.748 seconds.