Term Rewriting System R:

   [Y, X, N, M, L, K]
   eq(0, 0) -> true
   eq(0, s(Y)) -> false
   eq(s(X), 0) -> false
   eq(s(X), s(Y)) -> eq(X, Y)
   le(0, Y) -> true
   le(s(X), 0) -> false
   le(s(X), s(Y)) -> le(X, Y)
   min(cons(0, nil)) -> 0
   min(cons(s(N), nil)) -> s(N)
   min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
   ifmin(true, cons(N, cons(M, L))) -> min(cons(N, L))
   ifmin(false, cons(N, cons(M, L))) -> min(cons(M, L))
   replace(N, M, nil) -> nil
   replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
   ifrepl(true, N, M, cons(K, L)) -> cons(M, L)
   ifrepl(false, N, M, cons(K, L)) -> cons(K, replace(N, M, L))
   selsort(nil) -> nil
   selsort(cons(N, L)) -> ifselsort(eq(N, min(cons(N, L))), cons(N, L))
   ifselsort(true, cons(N, L)) -> cons(N, selsort(L))
   ifselsort(false, cons(N, L)) -> cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   SELSORT(cons(N, L)) -> IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))
   SELSORT(cons(N, L)) -> EQ(N, min(cons(N, L)))
   SELSORT(cons(N, L)) -> MIN(cons(N, L))
   IFSELSORT(false, cons(N, L)) -> MIN(cons(N, L))
   IFSELSORT(false, cons(N, L)) -> SELSORT(replace(min(cons(N, L)), N, L))
   IFSELSORT(false, cons(N, L)) -> REPLACE(min(cons(N, L)), N, L)
   IFSELSORT(true, cons(N, L)) -> SELSORT(L)
   EQ(s(X), s(Y)) -> EQ(X, Y)
   MIN(cons(N, cons(M, L))) -> IFMIN(le(N, M), cons(N, cons(M, L)))
   MIN(cons(N, cons(M, L))) -> LE(N, M)
   REPLACE(N, M, cons(K, L)) -> IFREPL(eq(N, K), N, M, cons(K, L))
   REPLACE(N, M, cons(K, L)) -> EQ(N, K)
   IFMIN(false, cons(N, cons(M, L))) -> MIN(cons(M, L))
   IFMIN(true, cons(N, cons(M, L))) -> MIN(cons(N, L))
   IFREPL(false, N, M, cons(K, L)) -> REPLACE(N, M, L)
   LE(s(X), s(Y)) -> LE(X, Y)

Furthermore, R contains five SCCs.


SCC1:

LE(s(X), s(Y)) -> LE(X, Y)

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(X), s(Y)) -> LE(X, Y)



 This transformation is resulting in no new subcycles.


SCC2:

EQ(s(X), s(Y)) -> EQ(X, Y)

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(X), s(Y)) -> EQ(X, Y)



 This transformation is resulting in no new subcycles.


SCC3:

IFMIN(true, cons(N, cons(M, L))) -> MIN(cons(N, L))
IFMIN(false, cons(N, cons(M, L))) -> MIN(cons(M, L))
MIN(cons(N, cons(M, L))) -> IFMIN(le(N, M), cons(N, cons(M, L)))

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(le(x_1, x_2)) = 0
POL(MIN(x_1)) = x_1
POL(true) = 0
POL(IFMIN(x_1, x_2)) = x_2
POL(0) = 0
POL(false) = 0
POL(cons(x_1, x_2)) = 1 + x_2

 resulting in no subcycles.


SCC4:

IFREPL(false, N, M, cons(K, L)) -> REPLACE(N, M, L)
REPLACE(N, M, cons(K, L)) -> IFREPL(eq(N, K), N, M, cons(K, L))

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(eq(x_1, x_2)) = 0
POL(IFREPL(x_1, x_2, x_3, x_4)) = x_4
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:

IFSELSORT(true, cons(N, L)) -> SELSORT(L)
IFSELSORT(false, cons(N, L)) -> SELSORT(replace(min(cons(N, L)), N, L))
SELSORT(cons(N, L)) -> IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

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

Additionally, the following rules can be oriented: 

   ifrepl(false, N, M, cons(K, L)) -> cons(K, replace(N, M, L))
   ifrepl(true, N, M, cons(K, L)) -> cons(M, L)
   replace(N, M, nil) -> nil
   replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 0
POL(s(x_1)) = 0
POL(eq(x_1, x_2)) = 0
POL(IFSELSORT(x_1, x_2)) = x_2
POL(min(x_1)) = 0
POL(SELSORT(x_1)) = x_1
POL(0) = 0
POL(replace(x_1, x_2, x_3)) = x_3
POL(cons(x_1, x_2)) = 1 + x_2
POL(ifmin(x_1, x_2)) = 0
POL(le(x_1, x_2)) = 0
POL(ifrepl(x_1, x_2, x_3, x_4)) = x_4
POL(true) = 0
POL(false) = 0

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 2.313 seconds.