0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 DependencyGraphProof (⇔)
↳11 QDP
↳12 QDPOrderProof (⇔)
↳13 QDP
↳14 PisEmptyProof (⇔)
↳15 TRUE
↳16 QDP
↳17 QDPOrderProof (⇔)
↳18 QDP
↳19 PisEmptyProof (⇔)
↳20 TRUE
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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CHOOSE(x, cons(v, w), 0, s(z)) → INSERT(x, w)
0 > [CHOOSE1, cons1, INSERT1, nil, insert1, choose1]
s1 > [CHOOSE1, cons1, INSERT1, nil, insert1, choose1]
sort1 > [CHOOSE1, cons1, INSERT1, nil, insert1, choose1]
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)
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), 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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CHOOSE(x, cons(v, w), s(y), s(z)) → CHOOSE(x, cons(v, w), y, z)
[CHOOSE1, s1] > [cons, nil, insert]
sort1 > [cons, nil, insert]
0 > [cons, nil, insert]
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)) → 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))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SORT(cons(x, y)) → SORT(y)
sort1 > [cons1, nil, insert1, choose1, 0]
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))