Termination Proof using AProVE

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.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

EQ(s(X), s(Y)) -> EQ(X, Y)
LE(s(X), s(Y)) -> LE(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)
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, cons(K, L)) -> IFREPL(eq(N, K), N, M, cons(K, L))
REPLACE(N, M, cons(K, L)) -> EQ(N, K)
IFREPL(false, N, M, cons(K, L)) -> REPLACE(N, M, L)
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(true, cons(N, L)) -> SELSORT(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)

Furthermore, R contains five SCCs.

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
EQ(s(X), s(Y)) -> EQ(X, Y)

Rules:

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

Rules:

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)))
Dependency Pairs:
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))

Rules:

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)))
Dependency Pairs:
IFMIN(false, cons(N, cons(M, L))) -> MIN(cons(M, L))
IFMIN(true, cons(N, cons(M, L))) -> MIN(cons(N, L))
MIN(cons(N, cons(M, L))) -> IFMIN(le(N, M), cons(N, cons(M, L)))

Rules:

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)))
Dependency Pairs:
IFSELSORT(false, cons(N, L)) -> SELSORT(replace(min(cons(N, L)), N, L))
IFSELSORT(true, cons(N, L)) -> SELSORT(L)
SELSORT(cons(N, L)) -> IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

Rules:

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)))

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
EQ(s(X), s(Y)) -> EQ(X, Y)

Rules:

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

Rules:

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)))
Dependency Pairs:
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))

Rules:

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)))
Dependency Pairs:
IFMIN(false, cons(N, cons(M, L))) -> MIN(cons(M, L))
IFMIN(true, cons(N, cons(M, L))) -> MIN(cons(N, L))
MIN(cons(N, cons(M, L))) -> IFMIN(le(N, M), cons(N, cons(M, L)))

Rules:

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)))
Dependency Pairs:
IFSELSORT(false, cons(N, L)) -> SELSORT(replace(min(cons(N, L)), N, L))
IFSELSORT(true, cons(N, L)) -> SELSORT(L)
SELSORT(cons(N, L)) -> IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

Rules:

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)))

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
EQ(s(X), s(Y)) -> EQ(X, Y)

Rules:

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

Rules:

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)))
Dependency Pairs:
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))

Rules:

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)))
Dependency Pairs:
IFMIN(false, cons(N, cons(M, L))) -> MIN(cons(M, L))
IFMIN(true, cons(N, cons(M, L))) -> MIN(cons(N, L))
MIN(cons(N, cons(M, L))) -> IFMIN(le(N, M), cons(N, cons(M, L)))

Rules:

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)))
Dependency Pairs:
IFSELSORT(false, cons(N, L)) -> SELSORT(replace(min(cons(N, L)), N, L))
IFSELSORT(true, cons(N, L)) -> SELSORT(L)
SELSORT(cons(N, L)) -> IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

Rules:

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)))

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
EQ(s(X), s(Y)) -> EQ(X, Y)

Rules:

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

Rules:

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)))
Dependency Pairs:
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))

Rules:

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)))
Dependency Pairs:
IFMIN(false, cons(N, cons(M, L))) -> MIN(cons(M, L))
IFMIN(true, cons(N, cons(M, L))) -> MIN(cons(N, L))
MIN(cons(N, cons(M, L))) -> IFMIN(le(N, M), cons(N, cons(M, L)))

Rules:

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)))
Dependency Pairs:
IFSELSORT(false, cons(N, L)) -> SELSORT(replace(min(cons(N, L)), N, L))
IFSELSORT(true, cons(N, L)) -> SELSORT(L)
SELSORT(cons(N, L)) -> IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

Rules:

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)))

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pair:
EQ(s(X), s(Y)) -> EQ(X, Y)

Rules:

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

Rules:

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)))
Dependency Pairs:
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))

Rules:

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)))
Dependency Pairs:
IFMIN(false, cons(N, cons(M, L))) -> MIN(cons(M, L))
IFMIN(true, cons(N, cons(M, L))) -> MIN(cons(N, L))
MIN(cons(N, cons(M, L))) -> IFMIN(le(N, M), cons(N, cons(M, L)))

Rules:

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)))
Dependency Pairs:
IFSELSORT(false, cons(N, L)) -> SELSORT(replace(min(cons(N, L)), N, L))
IFSELSORT(true, cons(N, L)) -> SELSORT(L)
SELSORT(cons(N, L)) -> IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

Rules:

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 could not be shown.
Duration:
0:00 minutes