0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 PisEmptyProof (⇔)
↳9 TRUE
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 PisEmptyProof (⇔)
↳14 TRUE
↳15 QDP
↳16 QDPOrderProof (⇔)
↳17 QDP
↳18 PisEmptyProof (⇔)
↳19 TRUE
↳20 QDP
↳21 QDPOrderProof (⇔)
↳22 QDP
↳23 PisEmptyProof (⇔)
↳24 TRUE
↳25 QDP
↳26 QDPOrderProof (⇔)
↳27 QDP
↳28 QDPOrderProof (⇔)
↳29 QDP
↳30 PisEmptyProof (⇔)
↳31 TRUE
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)))
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)
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)))
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)
trivial
LE2: multiset
s1: [1]
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)))
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))
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.
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))
[MIN, cons2, IFMIN, le1, true, false, 0]
MIN: multiset
cons2: multiset
IFMIN: multiset
le1: multiset
true: multiset
false: multiset
0: multiset
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)))
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)
trivial
EQ2: multiset
s1: [1]
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)))
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))
IFREPL(false, N, M, cons(K, L)) → REPLACE(N, 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.
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))
IFREPL(false, N, M, cons(K, L)) → REPLACE(N, M, L)
cons2 > [REPLACE3, eq2]
0 > [REPLACE3, eq2]
true > [REPLACE3, eq2]
s > false > [REPLACE3, eq2]
REPLACE3: multiset
cons2: multiset
eq2: [2,1]
false: multiset
0: multiset
true: multiset
s: []
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(true, cons(N, L)) → SELSORT(L)
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))
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.
IFSELSORT(true, cons(N, L)) → SELSORT(L)
[eq2, min, false, s] > le2 > [true, 0] > [cons1, replace1, nil, ifrepl1] > ifmin2
true: multiset
cons1: multiset
eq2: [2,1]
min: []
false: multiset
replace1: multiset
0: multiset
nil: multiset
s: []
ifmin2: multiset
le2: [1,2]
ifrepl1: multiset
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
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))
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))
[SELSORT1, cons1, eq] > IFSELSORT2 > min1 > 0 > false > [s1, le2]
[SELSORT1, cons1, eq] > ifmin2 > min1 > 0 > false > [s1, le2]
[SELSORT1, cons1, eq] > true > min1 > 0 > false > [s1, le2]
nil > [s1, le2]
SELSORT1: multiset
cons1: multiset
IFSELSORT2: multiset
eq: multiset
min1: multiset
false: multiset
0: multiset
nil: multiset
s1: [1]
ifmin2: [1,2]
le2: [1,2]
true: multiset
eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
ifrepl(true, N, M, cons(K, L)) → 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)))