R
↳Dependency Pair Analysis
SORT(cons(x, y)) -> INSERT(x, sort(y))
SORT(cons(x, y)) -> SORT(y)
INSERT(x, cons(v, w)) -> CHOOSE(x, cons(v, w), x, v)
CHOOSE(x, cons(v, w), 0, s(z)) -> INSERT(x, w)
CHOOSE(x, cons(v, w), s(y), s(z)) -> CHOOSE(x, cons(v, w), y, z)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
CHOOSE(x, cons(v, w), s(y), s(z)) -> CHOOSE(x, cons(v, w), y, z)
CHOOSE(x, cons(v, w), 0, s(z)) -> INSERT(x, w)
INSERT(x, cons(v, w)) -> CHOOSE(x, cons(v, w), x, v)
sort(nil) -> nil
sort(cons(x, y)) -> insert(x, sort(y))
insert(x, nil) -> cons(x, nil)
insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
choose(x, cons(v, w), y, 0) -> cons(x, cons(v, w))
choose(x, cons(v, w), 0, s(z)) -> cons(v, insert(x, w))
choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)
CHOOSE(x, cons(v, w), 0, s(z)) -> INSERT(x, w)
POL(cons(x1, x2)) = 1 + x1 + x2
CHOOSE(x1, x2, x3, x4) -> x2
cons(x1, x2) -> cons(x1, x2)
INSERT(x1, x2) -> x2
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳AFS
CHOOSE(x, cons(v, w), s(y), s(z)) -> CHOOSE(x, cons(v, w), y, z)
INSERT(x, cons(v, w)) -> CHOOSE(x, cons(v, w), x, v)
sort(nil) -> nil
sort(cons(x, y)) -> insert(x, sort(y))
insert(x, nil) -> cons(x, nil)
insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
choose(x, cons(v, w), y, 0) -> cons(x, cons(v, w))
choose(x, cons(v, w), 0, s(z)) -> cons(v, insert(x, w))
choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳DGraph
...
→DP Problem 4
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
CHOOSE(x, cons(v, w), s(y), s(z)) -> CHOOSE(x, cons(v, w), y, z)
sort(nil) -> nil
sort(cons(x, y)) -> insert(x, sort(y))
insert(x, nil) -> cons(x, nil)
insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
choose(x, cons(v, w), y, 0) -> cons(x, cons(v, w))
choose(x, cons(v, w), 0, s(z)) -> cons(v, insert(x, w))
choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)
CHOOSE(x, cons(v, w), s(y), s(z)) -> CHOOSE(x, cons(v, w), y, z)
POL(CHOOSE(x1, x2, x3, x4)) = x1 + x2 + x3 + x4 POL(cons(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1
CHOOSE(x1, x2, x3, x4) -> CHOOSE(x1, x2, x3, x4)
cons(x1, x2) -> cons(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳DGraph
...
→DP Problem 5
↳Dependency Graph
→DP Problem 2
↳AFS
sort(nil) -> nil
sort(cons(x, y)) -> insert(x, sort(y))
insert(x, nil) -> cons(x, nil)
insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
choose(x, cons(v, w), y, 0) -> cons(x, cons(v, w))
choose(x, cons(v, w), 0, s(z)) -> cons(v, insert(x, w))
choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
SORT(cons(x, y)) -> SORT(y)
sort(nil) -> nil
sort(cons(x, y)) -> insert(x, sort(y))
insert(x, nil) -> cons(x, nil)
insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
choose(x, cons(v, w), y, 0) -> cons(x, cons(v, w))
choose(x, cons(v, w), 0, s(z)) -> cons(v, insert(x, w))
choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)
SORT(cons(x, y)) -> SORT(y)
POL(cons(x1, x2)) = 1 + x1 + x2 POL(SORT(x1)) = x1
SORT(x1) -> SORT(x1)
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 6
↳Dependency Graph
sort(nil) -> nil
sort(cons(x, y)) -> insert(x, sort(y))
insert(x, nil) -> cons(x, nil)
insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
choose(x, cons(v, w), y, 0) -> cons(x, cons(v, w))
choose(x, cons(v, w), 0, s(z)) -> cons(v, insert(x, w))
choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)