R
↳Dependency Pair Analysis
LT(s(X), s(Y)) -> LT(X, Y)
APPEND(add(N, X), Y) -> APPEND(X, Y)
SPLIT(N, add(M, Y)) -> F1(split(N, Y), N, M, Y)
SPLIT(N, add(M, Y)) -> SPLIT(N, Y)
F1(pair(X, Z), N, M, Y) -> F2(lt(N, M), N, M, Y, X, Z)
F1(pair(X, Z), N, M, Y) -> LT(N, M)
QSORT(add(N, X)) -> F3(split(N, X), N, X)
QSORT(add(N, X)) -> SPLIT(N, X)
F3(pair(Y, Z), N, X) -> APPEND(qsort(Y), add(X, qsort(Z)))
F3(pair(Y, Z), N, X) -> QSORT(Y)
F3(pair(Y, Z), N, X) -> QSORT(Z)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳Remaining
LT(s(X), s(Y)) -> LT(X, Y)
lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))
LT(s(X), s(Y)) -> LT(X, Y)
LT(x1, x2) -> LT(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 5
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳Remaining
lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳AFS
→DP Problem 4
↳Remaining
APPEND(add(N, X), Y) -> APPEND(X, Y)
lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))
APPEND(add(N, X), Y) -> APPEND(X, Y)
APPEND(x1, x2) -> APPEND(x1, x2)
add(x1, x2) -> add(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 6
↳Dependency Graph
→DP Problem 3
↳AFS
→DP Problem 4
↳Remaining
lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Argument Filtering and Ordering
→DP Problem 4
↳Remaining
SPLIT(N, add(M, Y)) -> SPLIT(N, Y)
lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))
SPLIT(N, add(M, Y)) -> SPLIT(N, Y)
SPLIT(x1, x2) -> SPLIT(x1, x2)
add(x1, x2) -> add(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 7
↳Dependency Graph
→DP Problem 4
↳Remaining
lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳Remaining Obligation(s)
F3(pair(Y, Z), N, X) -> QSORT(Z)
F3(pair(Y, Z), N, X) -> QSORT(Y)
QSORT(add(N, X)) -> F3(split(N, X), N, X)
lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))