YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
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(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(nil)
sort(cons(x0, x1))
insert(x0, nil)
insert(x0, cons(x1, x2))
choose(x0, cons(x1, x2), x3, 0)
choose(x0, cons(x1, x2), 0, s(x3))
choose(x0, cons(x1, x2), s(x3), s(x4))
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)
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(nil)
sort(cons(x0, x1))
insert(x0, nil)
insert(x0, cons(x1, x2))
choose(x0, cons(x1, x2), x3, 0)
choose(x0, cons(x1, x2), 0, s(x3))
choose(x0, cons(x1, x2), s(x3), s(x4))
CHOOSE(x, cons(v, w), 0, s(z)) → INSERT(x, w)
INSERT(x, cons(v, w)) → CHOOSE(x, cons(v, w), x, v)
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)
sort(nil)
sort(cons(x0, x1))
insert(x0, nil)
insert(x0, cons(x1, x2))
choose(x0, cons(x1, x2), x3, 0)
choose(x0, cons(x1, x2), 0, s(x3))
choose(x0, cons(x1, x2), s(x3), s(x4))
CHOOSE(x, cons(v, w), 0, s(z)) → INSERT(x, w)
INSERT(x, cons(v, w)) → CHOOSE(x, cons(v, w), x, v)
CHOOSE(x, cons(v, w), s(y), s(z)) → CHOOSE(x, cons(v, w), y, z)
sort(nil)
sort(cons(x0, x1))
insert(x0, nil)
insert(x0, cons(x1, x2))
choose(x0, cons(x1, x2), x3, 0)
choose(x0, cons(x1, x2), 0, s(x3))
choose(x0, cons(x1, x2), s(x3), s(x4))
sort(nil)
sort(cons(x0, x1))
insert(x0, nil)
insert(x0, cons(x1, x2))
choose(x0, cons(x1, x2), x3, 0)
choose(x0, cons(x1, x2), 0, s(x3))
choose(x0, cons(x1, x2), s(x3), s(x4))
CHOOSE(x, cons(v, w), 0, s(z)) → INSERT(x, w)
INSERT(x, cons(v, w)) → CHOOSE(x, cons(v, w), x, v)
CHOOSE(x, cons(v, w), s(y), s(z)) → CHOOSE(x, cons(v, w), y, z)
From the DPs we obtained the following set of size-change graphs:
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(nil)
sort(cons(x0, x1))
insert(x0, nil)
insert(x0, cons(x1, x2))
choose(x0, cons(x1, x2), x3, 0)
choose(x0, cons(x1, x2), 0, s(x3))
choose(x0, cons(x1, x2), s(x3), s(x4))
SORT(cons(x, y)) → SORT(y)
sort(nil)
sort(cons(x0, x1))
insert(x0, nil)
insert(x0, cons(x1, x2))
choose(x0, cons(x1, x2), x3, 0)
choose(x0, cons(x1, x2), 0, s(x3))
choose(x0, cons(x1, x2), s(x3), s(x4))
sort(nil)
sort(cons(x0, x1))
insert(x0, nil)
insert(x0, cons(x1, x2))
choose(x0, cons(x1, x2), x3, 0)
choose(x0, cons(x1, x2), 0, s(x3))
choose(x0, cons(x1, x2), s(x3), s(x4))
SORT(cons(x, y)) → SORT(y)
From the DPs we obtained the following set of size-change graphs: