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)))
↳ QTRS
↳ DependencyPairsProof
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)))
IFSELSORT(false, cons(N, L)) → REPLACE(min(cons(N, L)), N, L)
SELSORT(cons(N, L)) → EQ(N, min(cons(N, L)))
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))
IFMIN(false, cons(N, cons(M, L))) → MIN(cons(M, L))
LE(s(X), s(Y)) → LE(X, Y)
IFSELSORT(true, cons(N, L)) → SELSORT(L)
SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))
IFMIN(true, cons(N, cons(M, L))) → MIN(cons(N, L))
IFSELSORT(false, cons(N, L)) → MIN(cons(N, L))
EQ(s(X), s(Y)) → EQ(X, Y)
IFREPL(false, N, M, cons(K, L)) → REPLACE(N, M, L)
MIN(cons(N, cons(M, L))) → IFMIN(le(N, M), cons(N, cons(M, L)))
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))
SELSORT(cons(N, L)) → MIN(cons(N, L))
MIN(cons(N, cons(M, L))) → LE(N, M)
REPLACE(N, M, cons(K, L)) → EQ(N, 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)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IFSELSORT(false, cons(N, L)) → REPLACE(min(cons(N, L)), N, L)
SELSORT(cons(N, L)) → EQ(N, min(cons(N, L)))
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))
IFMIN(false, cons(N, cons(M, L))) → MIN(cons(M, L))
LE(s(X), s(Y)) → LE(X, Y)
IFSELSORT(true, cons(N, L)) → SELSORT(L)
SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))
IFMIN(true, cons(N, cons(M, L))) → MIN(cons(N, L))
IFSELSORT(false, cons(N, L)) → MIN(cons(N, L))
EQ(s(X), s(Y)) → EQ(X, Y)
IFREPL(false, N, M, cons(K, L)) → REPLACE(N, M, L)
MIN(cons(N, cons(M, L))) → IFMIN(le(N, M), cons(N, cons(M, L)))
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))
SELSORT(cons(N, L)) → MIN(cons(N, L))
MIN(cons(N, cons(M, L))) → LE(N, M)
REPLACE(N, M, cons(K, L)) → EQ(N, 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)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LE(s(X), s(Y)) → LE(X, Y)
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)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LE(s(X), s(Y)) → LE(X, Y)
The value of delta used in the strict ordering is 12.
POL(s(x1)) = 4 + (2)x_1
POL(LE(x1, x2)) = (3)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
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)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
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)))
IFMIN(false, cons(N, cons(M, L))) → MIN(cons(M, L))
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)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IFMIN(true, cons(N, cons(M, L))) → MIN(cons(N, L))
IFMIN(false, cons(N, cons(M, L))) → MIN(cons(M, L))
Used ordering: Polynomial interpretation [25,35]:
MIN(cons(N, cons(M, L))) → IFMIN(le(N, M), cons(N, cons(M, L)))
The value of delta used in the strict ordering is 1.
POL(cons(x1, x2)) = 1 + x_2
POL(le(x1, x2)) = 0
POL(true) = 0
POL(MIN(x1)) = x_1
POL(false) = 0
POL(s(x1)) = 2 + (2)x_1
POL(0) = 3
POL(IFMIN(x1, x2)) = x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
MIN(cons(N, cons(M, L))) → IFMIN(le(N, M), cons(N, cons(M, L)))
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)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
EQ(s(X), s(Y)) → EQ(X, Y)
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)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EQ(s(X), s(Y)) → EQ(X, Y)
The value of delta used in the strict ordering is 3.
POL(EQ(x1, x2)) = (3)x_2
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
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)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
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))
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)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IFREPL(false, N, M, cons(K, L)) → REPLACE(N, M, L)
Used ordering: Polynomial interpretation [25,35]:
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))
The value of delta used in the strict ordering is 1.
POL(IFREPL(x1, x2, x3, x4)) = x_1 + (2)x_4
POL(cons(x1, x2)) = (2)x_1 + (3)x_2
POL(eq(x1, x2)) = x_2
POL(REPLACE(x1, x2, x3)) = (3)x_3
POL(true) = 3
POL(false) = 1
POL(s(x1)) = 1 + (3)x_1
POL(0) = 4
eq(0, 0) → true
eq(s(X), 0) → false
eq(0, s(Y)) → false
eq(s(X), s(Y)) → eq(X, Y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))
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)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))
IFSELSORT(true, cons(N, L)) → SELSORT(L)
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)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))
IFSELSORT(true, cons(N, L)) → SELSORT(L)
The value of delta used in the strict ordering is 2.
POL(eq(x1, x2)) = 0
POL(le(x1, x2)) = 0
POL(true) = 0
POL(0) = 1
POL(IFSELSORT(x1, x2)) = 2 + (4)x_2
POL(ifmin(x1, x2)) = 1
POL(cons(x1, x2)) = 4 + x_2
POL(ifrepl(x1, x2, x3, x4)) = 2 + x_2 + x_4
POL(false) = 0
POL(s(x1)) = 0
POL(min(x1)) = 1
POL(nil) = 2
POL(replace(x1, x2, x3)) = 2 + x_1 + x_3
POL(SELSORT(x1)) = 4 + (4)x_1
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
min(cons(s(N), nil)) → s(N)
min(cons(0, nil)) → 0
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)))
replace(N, M, nil) → nil
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
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)))