Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Others/quicksortPtime)

The relative rewrite relation R/S is considered where R is the following TRS

qs(x',Cons(x,xs)) → app(Cons(x,Nil),Cons(x',quicksort(xs))) (1)
quicksort(Cons(x,Cons(x',xs))) → qs(x,part(x,Cons(x',xs),Nil,Nil)) (2)
quicksort(Cons(x,Nil)) → Cons(x,Nil) (3)
quicksort(Nil) → Nil (4)
part(x',Cons(x,xs),xs1,xs2) → part[Ite](>(x',x),x',Cons(x,xs),xs1,xs2) (5)
part(x,Nil,xs1,xs2) → app(xs1,xs2) (6)
app(Cons(x,xs),ys) → Cons(x,app(xs,ys)) (7)
app(Nil,ys) → ys (8)
notEmpty(Cons(x,xs)) → True (9)
notEmpty(Nil) → False (10)

and S is the following TRS.

<(S(x),S(y)) → <(x,y) (11)
<(0,S(y)) → True (12)
<(x,0) → False (13)
>(S(x),S(y)) → >(x,y) (14)
>(0,y) → False (15)
>(S(x),0) → True (16)
part[Ite](True,x',Cons(x,xs),xs1,xs2) → part(x',xs,Cons(x,xs1),xs2) (17)
part[False][Ite](True,x',Cons(x,xs),xs1,xs2) → part(x',xs,xs1,Cons(x,xs2)) (18)
part[Ite](False,x',Cons(x,xs),xs1,xs2) → part[False][Ite](<(x',x),x',Cons(x,xs),xs1,xs2) (19)
part[False][Ite](False,x',Cons(x,xs),xs1,xs2) → part(x',xs,xs1,xs2) (20)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n2).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
qs#(z0,Cons(z1,z2)) → c10(app#(Cons(z1,Nil),Cons(z0,quicksort(z2))),quicksort#(z2)) (22)
originates from
qs(z0,Cons(z1,z2)) → app(Cons(z1,Nil),Cons(z0,quicksort(z2))) (21)
quicksort#(Cons(z0,Cons(z1,z2))) → c11(qs#(z0,part(z0,Cons(z1,z2),Nil,Nil)),part#(z0,Cons(z1,z2),Nil,Nil)) (24)
originates from
quicksort(Cons(z0,Cons(z1,z2))) → qs(z0,part(z0,Cons(z1,z2),Nil,Nil)) (23)
quicksort#(Cons(z0,Nil)) → c12 (26)
originates from
quicksort(Cons(z0,Nil)) → Cons(z0,Nil) (25)
quicksort#(Nil) → c13 (27)
originates from
quicksort(Nil) → Nil (4)
part#(z0,Cons(z1,z2),z3,z4) → c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) (29)
originates from
part(z0,Cons(z1,z2),z3,z4) → part[Ite](>(z0,z1),z0,Cons(z1,z2),z3,z4) (28)
part#(z0,Nil,z1,z2) → c15(app#(z1,z2)) (31)
originates from
part(z0,Nil,z1,z2) → app(z1,z2) (30)
app#(Cons(z0,z1),z2) → c16(app#(z1,z2)) (33)
originates from
app(Cons(z0,z1),z2) → Cons(z0,app(z1,z2)) (32)
app#(Nil,z0) → c17 (35)
originates from
app(Nil,z0) → z0 (34)
notEmpty#(Cons(z0,z1)) → c18 (37)
originates from
notEmpty(Cons(z0,z1)) → True (36)
notEmpty#(Nil) → c19 (38)
originates from
notEmpty(Nil) → False (10)
<#(S(z0),S(z1)) → c(<#(z0,z1)) (40)
originates from
<(S(z0),S(z1)) → <(z0,z1) (39)
<#(0,S(z0)) → c1 (42)
originates from
<(0,S(z0)) → True (41)
<#(z0,0) → c2 (44)
originates from
<(z0,0) → False (43)
>#(S(z0),S(z1)) → c3(>#(z0,z1)) (46)
originates from
>(S(z0),S(z1)) → >(z0,z1) (45)
>#(0,z0) → c4 (48)
originates from
>(0,z0) → False (47)
>#(S(z0),0) → c5 (50)
originates from
>(S(z0),0) → True (49)
part[Ite]#(True,z0,Cons(z1,z2),z3,z4) → c6(part#(z0,z2,Cons(z1,z3),z4)) (52)
originates from
part[Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,Cons(z1,z3),z4) (51)
part[Ite]#(False,z0,Cons(z1,z2),z3,z4) → c7(part[False][Ite]#(<(z0,z1),z0,Cons(z1,z2),z3,z4),<#(z0,z1)) (54)
originates from
part[Ite](False,z0,Cons(z1,z2),z3,z4) → part[False][Ite](<(z0,z1),z0,Cons(z1,z2),z3,z4) (53)
part[False][Ite]#(True,z0,Cons(z1,z2),z3,z4) → c8(part#(z0,z2,z3,Cons(z1,z4))) (56)
originates from
part[False][Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,Cons(z1,z4)) (55)
part[False][Ite]#(False,z0,Cons(z1,z2),z3,z4) → c9(part#(z0,z2,z3,z4)) (58)
originates from
part[False][Ite](False,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,z4) (57)
Moreover, we add the following terms to the innermost strategy.
<#(S(z0),S(z1))
<#(0,S(z0))
<#(z0,0)
>#(S(z0),S(z1))
>#(0,z0)
>#(S(z0),0)
part[Ite]#(True,z0,Cons(z1,z2),z3,z4)
part[Ite]#(False,z0,Cons(z1,z2),z3,z4)
part[False][Ite]#(True,z0,Cons(z1,z2),z3,z4)
part[False][Ite]#(False,z0,Cons(z1,z2),z3,z4)
qs#(z0,Cons(z1,z2))
quicksort#(Cons(z0,Cons(z1,z2)))
quicksort#(Cons(z0,Nil))
quicksort#(Nil)
part#(z0,Cons(z1,z2),z3,z4)
part#(z0,Nil,z1,z2)
app#(Cons(z0,z1),z2)
app#(Nil,z0)
notEmpty#(Cons(z0,z1))
notEmpty#(Nil)

1.1 Usable Rules

We remove the following rules since they are not usable.
notEmpty(Cons(z0,z1)) → True (36)
notEmpty(Nil) → False (10)

1.1.1 Rule Shifting

The rules
notEmpty#(Cons(z0,z1)) → c18 (37)
notEmpty#(Nil) → c19 (38)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15(x1)] = 1 · x1 + 0
[c16(x1)] = 1 · x1 + 0
[c17] = 0
[c18] = 0
[c19] = 0
[<(x1, x2)] = 1 + 1 · x1 + 1 · x2
[quicksort(x1)] = 1 + 1 · x1
[qs(x1, x2)] = 1 + 1 · x1
[part(x1,...,x4)] = 1 + 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4
[part[Ite](x1,...,x5)] = 1 + 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5
[>(x1, x2)] = 1 + 1 · x1 + 1 · x2
[app(x1, x2)] = 1 + 1 · x1 + 1 · x2
[part[False][Ite](x1,...,x5)] = 1 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5
[<#(x1, x2)] = 0
[>#(x1, x2)] = 0
[part[Ite]#(x1,...,x5)] = 1 · x3 + 0
[part[False][Ite]#(x1,...,x5)] = 0
[qs#(x1, x2)] = 0
[quicksort#(x1)] = 0
[part#(x1,...,x4)] = 0
[app#(x1, x2)] = 0
[notEmpty#(x1)] = 1 + 1 · x1
[S(x1)] = 1 + 1 · x1
[0] = 1
[False] = 0
[True] = 0
[Cons(x1, x2)] = 0
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
<#(S(z0),S(z1)) → c(<#(z0,z1)) (40)
<#(0,S(z0)) → c1 (42)
<#(z0,0) → c2 (44)
>#(S(z0),S(z1)) → c3(>#(z0,z1)) (46)
>#(0,z0) → c4 (48)
>#(S(z0),0) → c5 (50)
part[Ite]#(True,z0,Cons(z1,z2),z3,z4) → c6(part#(z0,z2,Cons(z1,z3),z4)) (52)
part[Ite]#(False,z0,Cons(z1,z2),z3,z4) → c7(part[False][Ite]#(<(z0,z1),z0,Cons(z1,z2),z3,z4),<#(z0,z1)) (54)
part[False][Ite]#(True,z0,Cons(z1,z2),z3,z4) → c8(part#(z0,z2,z3,Cons(z1,z4))) (56)
part[False][Ite]#(False,z0,Cons(z1,z2),z3,z4) → c9(part#(z0,z2,z3,z4)) (58)
qs#(z0,Cons(z1,z2)) → c10(app#(Cons(z1,Nil),Cons(z0,quicksort(z2))),quicksort#(z2)) (22)
quicksort#(Cons(z0,Cons(z1,z2))) → c11(qs#(z0,part(z0,Cons(z1,z2),Nil,Nil)),part#(z0,Cons(z1,z2),Nil,Nil)) (24)
quicksort#(Cons(z0,Nil)) → c12 (26)
quicksort#(Nil) → c13 (27)
part#(z0,Cons(z1,z2),z3,z4) → c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) (29)
part#(z0,Nil,z1,z2) → c15(app#(z1,z2)) (31)
app#(Cons(z0,z1),z2) → c16(app#(z1,z2)) (33)
app#(Nil,z0) → c17 (35)
notEmpty#(Cons(z0,z1)) → c18 (37)
notEmpty#(Nil) → c19 (38)

1.1.1.1 Rule Shifting

The rules
quicksort#(Cons(z0,Nil)) → c12 (26)
quicksort#(Nil) → c13 (27)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15(x1)] = 1 · x1 + 0
[c16(x1)] = 1 · x1 + 0
[c17] = 0
[c18] = 0
[c19] = 0
[<(x1, x2)] = 1 + 1 · x1
[quicksort(x1)] = 1 + 1 · x1
[qs(x1, x2)] = 1 + 1 · x1
[part(x1,...,x4)] = 1 + 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4
[part[Ite](x1,...,x5)] = 1 + 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5
[>(x1, x2)] = 1 + 1 · x1 + 1 · x2
[app(x1, x2)] = 1 + 1 · x1 + 1 · x2
[part[False][Ite](x1,...,x5)] = 1 + 1 · x1 + 1 · x2 + 1 · x3 + 1 · x4 + 1 · x5
[<#(x1, x2)] = 0
[>#(x1, x2)] = 0
[part[Ite]#(x1,...,x5)] = 0
[part[False][Ite]#(x1,...,x5)] = 0
[qs#(x1, x2)] = 1
[quicksort#(x1)] = 1
[part#(x1,...,x4)] = 0
[app#(x1, x2)] = 0
[notEmpty#(x1)] = 0
[S(x1)] = 1 + 1 · x1
[0] = 1
[False] = 0
[True] = 0
[Cons(x1, x2)] = 0
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
<#(S(z0),S(z1)) → c(<#(z0,z1)) (40)
<#(0,S(z0)) → c1 (42)
<#(z0,0) → c2 (44)
>#(S(z0),S(z1)) → c3(>#(z0,z1)) (46)
>#(0,z0) → c4 (48)
>#(S(z0),0) → c5 (50)
part[Ite]#(True,z0,Cons(z1,z2),z3,z4) → c6(part#(z0,z2,Cons(z1,z3),z4)) (52)
part[Ite]#(False,z0,Cons(z1,z2),z3,z4) → c7(part[False][Ite]#(<(z0,z1),z0,Cons(z1,z2),z3,z4),<#(z0,z1)) (54)
part[False][Ite]#(True,z0,Cons(z1,z2),z3,z4) → c8(part#(z0,z2,z3,Cons(z1,z4))) (56)
part[False][Ite]#(False,z0,Cons(z1,z2),z3,z4) → c9(part#(z0,z2,z3,z4)) (58)
qs#(z0,Cons(z1,z2)) → c10(app#(Cons(z1,Nil),Cons(z0,quicksort(z2))),quicksort#(z2)) (22)
quicksort#(Cons(z0,Cons(z1,z2))) → c11(qs#(z0,part(z0,Cons(z1,z2),Nil,Nil)),part#(z0,Cons(z1,z2),Nil,Nil)) (24)
quicksort#(Cons(z0,Nil)) → c12 (26)
quicksort#(Nil) → c13 (27)
part#(z0,Cons(z1,z2),z3,z4) → c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) (29)
part#(z0,Nil,z1,z2) → c15(app#(z1,z2)) (31)
app#(Cons(z0,z1),z2) → c16(app#(z1,z2)) (33)
app#(Nil,z0) → c17 (35)
notEmpty#(Cons(z0,z1)) → c18 (37)
notEmpty#(Nil) → c19 (38)

1.1.1.1.1 Rule Shifting

The rules
qs#(z0,Cons(z1,z2)) → c10(app#(Cons(z1,Nil),Cons(z0,quicksort(z2))),quicksort#(z2)) (22)
quicksort#(Cons(z0,Cons(z1,z2))) → c11(qs#(z0,part(z0,Cons(z1,z2),Nil,Nil)),part#(z0,Cons(z1,z2),Nil,Nil)) (24)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15(x1)] = 1 · x1 + 0
[c16(x1)] = 1 · x1 + 0
[c17] = 0
[c18] = 0
[c19] = 0
[<(x1, x2)] = 1 + 1 · x1 + 1 · x2
[quicksort(x1)] = 1 + 1 · x1
[qs(x1, x2)] = 1 + 1 · x1
[part(x1,...,x4)] = 1 · x2 + 0 + 1 · x3 + 1 · x4
[part[Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[>(x1, x2)] = 1 + 1 · x1 + 1 · x2
[app(x1, x2)] = 1 · x1 + 0 + 1 · x2
[part[False][Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[<#(x1, x2)] = 0
[>#(x1, x2)] = 0
[part[Ite]#(x1,...,x5)] = 0
[part[False][Ite]#(x1,...,x5)] = 0
[qs#(x1, x2)] = 1 · x2 + 0
[quicksort#(x1)] = 1 · x1 + 0
[part#(x1,...,x4)] = 0
[app#(x1, x2)] = 0
[notEmpty#(x1)] = 0
[S(x1)] = 1 + 1 · x1
[0] = 1
[False] = 0
[True] = 0
[Cons(x1, x2)] = 1 + 1 · x2
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
<#(S(z0),S(z1)) → c(<#(z0,z1)) (40)
<#(0,S(z0)) → c1 (42)
<#(z0,0) → c2 (44)
>#(S(z0),S(z1)) → c3(>#(z0,z1)) (46)
>#(0,z0) → c4 (48)
>#(S(z0),0) → c5 (50)
part[Ite]#(True,z0,Cons(z1,z2),z3,z4) → c6(part#(z0,z2,Cons(z1,z3),z4)) (52)
part[Ite]#(False,z0,Cons(z1,z2),z3,z4) → c7(part[False][Ite]#(<(z0,z1),z0,Cons(z1,z2),z3,z4),<#(z0,z1)) (54)
part[False][Ite]#(True,z0,Cons(z1,z2),z3,z4) → c8(part#(z0,z2,z3,Cons(z1,z4))) (56)
part[False][Ite]#(False,z0,Cons(z1,z2),z3,z4) → c9(part#(z0,z2,z3,z4)) (58)
qs#(z0,Cons(z1,z2)) → c10(app#(Cons(z1,Nil),Cons(z0,quicksort(z2))),quicksort#(z2)) (22)
quicksort#(Cons(z0,Cons(z1,z2))) → c11(qs#(z0,part(z0,Cons(z1,z2),Nil,Nil)),part#(z0,Cons(z1,z2),Nil,Nil)) (24)
quicksort#(Cons(z0,Nil)) → c12 (26)
quicksort#(Nil) → c13 (27)
part#(z0,Cons(z1,z2),z3,z4) → c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) (29)
part#(z0,Nil,z1,z2) → c15(app#(z1,z2)) (31)
app#(Cons(z0,z1),z2) → c16(app#(z1,z2)) (33)
app#(Nil,z0) → c17 (35)
notEmpty#(Cons(z0,z1)) → c18 (37)
notEmpty#(Nil) → c19 (38)
part[False][Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,Cons(z1,z4)) (55)
part[False][Ite](False,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,z4) (57)
app(Nil,z0) → z0 (34)
part(z0,Cons(z1,z2),z3,z4) → part[Ite](>(z0,z1),z0,Cons(z1,z2),z3,z4) (28)
part[Ite](False,z0,Cons(z1,z2),z3,z4) → part[False][Ite](<(z0,z1),z0,Cons(z1,z2),z3,z4) (53)
app(Cons(z0,z1),z2) → Cons(z0,app(z1,z2)) (32)
part[Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,Cons(z1,z3),z4) (51)
part(z0,Nil,z1,z2) → app(z1,z2) (30)

1.1.1.1.1.1 Rule Shifting

The rules
part#(z0,Nil,z1,z2) → c15(app#(z1,z2)) (31)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15(x1)] = 1 · x1 + 0
[c16(x1)] = 1 · x1 + 0
[c17] = 0
[c18] = 0
[c19] = 0
[<(x1, x2)] = 1 + 1 · x1
[quicksort(x1)] = 1 + 1 · x1
[qs(x1, x2)] = 1 + 1 · x1
[part(x1,...,x4)] = 1 · x2 + 0 + 1 · x3 + 1 · x4
[part[Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[>(x1, x2)] = 1 + 1 · x1 + 1 · x2
[app(x1, x2)] = 1 · x1 + 0 + 1 · x2
[part[False][Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[<#(x1, x2)] = 0
[>#(x1, x2)] = 0
[part[Ite]#(x1,...,x5)] = 1
[part[False][Ite]#(x1,...,x5)] = 1
[qs#(x1, x2)] = 1 + 1 · x2
[quicksort#(x1)] = 1 + 1 · x1
[part#(x1,...,x4)] = 1
[app#(x1, x2)] = 0
[notEmpty#(x1)] = 0
[S(x1)] = 1 + 1 · x1
[0] = 1
[False] = 0
[True] = 0
[Cons(x1, x2)] = 1 + 1 · x2
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
<#(S(z0),S(z1)) → c(<#(z0,z1)) (40)
<#(0,S(z0)) → c1 (42)
<#(z0,0) → c2 (44)
>#(S(z0),S(z1)) → c3(>#(z0,z1)) (46)
>#(0,z0) → c4 (48)
>#(S(z0),0) → c5 (50)
part[Ite]#(True,z0,Cons(z1,z2),z3,z4) → c6(part#(z0,z2,Cons(z1,z3),z4)) (52)
part[Ite]#(False,z0,Cons(z1,z2),z3,z4) → c7(part[False][Ite]#(<(z0,z1),z0,Cons(z1,z2),z3,z4),<#(z0,z1)) (54)
part[False][Ite]#(True,z0,Cons(z1,z2),z3,z4) → c8(part#(z0,z2,z3,Cons(z1,z4))) (56)
part[False][Ite]#(False,z0,Cons(z1,z2),z3,z4) → c9(part#(z0,z2,z3,z4)) (58)
qs#(z0,Cons(z1,z2)) → c10(app#(Cons(z1,Nil),Cons(z0,quicksort(z2))),quicksort#(z2)) (22)
quicksort#(Cons(z0,Cons(z1,z2))) → c11(qs#(z0,part(z0,Cons(z1,z2),Nil,Nil)),part#(z0,Cons(z1,z2),Nil,Nil)) (24)
quicksort#(Cons(z0,Nil)) → c12 (26)
quicksort#(Nil) → c13 (27)
part#(z0,Cons(z1,z2),z3,z4) → c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) (29)
part#(z0,Nil,z1,z2) → c15(app#(z1,z2)) (31)
app#(Cons(z0,z1),z2) → c16(app#(z1,z2)) (33)
app#(Nil,z0) → c17 (35)
notEmpty#(Cons(z0,z1)) → c18 (37)
notEmpty#(Nil) → c19 (38)
part[False][Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,Cons(z1,z4)) (55)
part[False][Ite](False,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,z4) (57)
app(Nil,z0) → z0 (34)
part(z0,Cons(z1,z2),z3,z4) → part[Ite](>(z0,z1),z0,Cons(z1,z2),z3,z4) (28)
part[Ite](False,z0,Cons(z1,z2),z3,z4) → part[False][Ite](<(z0,z1),z0,Cons(z1,z2),z3,z4) (53)
app(Cons(z0,z1),z2) → Cons(z0,app(z1,z2)) (32)
part[Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,Cons(z1,z3),z4) (51)
part(z0,Nil,z1,z2) → app(z1,z2) (30)

1.1.1.1.1.1.1 Rule Shifting

The rules
app#(Nil,z0) → c17 (35)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15(x1)] = 1 · x1 + 0
[c16(x1)] = 1 · x1 + 0
[c17] = 0
[c18] = 0
[c19] = 0
[<(x1, x2)] = 1 + 1 · x1 + 1 · x2
[quicksort(x1)] = 1 + 1 · x1
[qs(x1, x2)] = 1 + 1 · x1
[part(x1,...,x4)] = 1 · x2 + 0 + 1 · x3 + 1 · x4
[part[Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[>(x1, x2)] = 1 + 1 · x1 + 1 · x2
[app(x1, x2)] = 1 · x1 + 0 + 1 · x2
[part[False][Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[<#(x1, x2)] = 0
[>#(x1, x2)] = 0
[part[Ite]#(x1,...,x5)] = 1
[part[False][Ite]#(x1,...,x5)] = 1
[qs#(x1, x2)] = 1 · x2 + 0
[quicksort#(x1)] = 1 · x1 + 0
[part#(x1,...,x4)] = 1
[app#(x1, x2)] = 1
[notEmpty#(x1)] = 0
[S(x1)] = 1 + 1 · x1
[0] = 1
[False] = 0
[True] = 0
[Cons(x1, x2)] = 1 + 1 · x2
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
<#(S(z0),S(z1)) → c(<#(z0,z1)) (40)
<#(0,S(z0)) → c1 (42)
<#(z0,0) → c2 (44)
>#(S(z0),S(z1)) → c3(>#(z0,z1)) (46)
>#(0,z0) → c4 (48)
>#(S(z0),0) → c5 (50)
part[Ite]#(True,z0,Cons(z1,z2),z3,z4) → c6(part#(z0,z2,Cons(z1,z3),z4)) (52)
part[Ite]#(False,z0,Cons(z1,z2),z3,z4) → c7(part[False][Ite]#(<(z0,z1),z0,Cons(z1,z2),z3,z4),<#(z0,z1)) (54)
part[False][Ite]#(True,z0,Cons(z1,z2),z3,z4) → c8(part#(z0,z2,z3,Cons(z1,z4))) (56)
part[False][Ite]#(False,z0,Cons(z1,z2),z3,z4) → c9(part#(z0,z2,z3,z4)) (58)
qs#(z0,Cons(z1,z2)) → c10(app#(Cons(z1,Nil),Cons(z0,quicksort(z2))),quicksort#(z2)) (22)
quicksort#(Cons(z0,Cons(z1,z2))) → c11(qs#(z0,part(z0,Cons(z1,z2),Nil,Nil)),part#(z0,Cons(z1,z2),Nil,Nil)) (24)
quicksort#(Cons(z0,Nil)) → c12 (26)
quicksort#(Nil) → c13 (27)
part#(z0,Cons(z1,z2),z3,z4) → c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) (29)
part#(z0,Nil,z1,z2) → c15(app#(z1,z2)) (31)
app#(Cons(z0,z1),z2) → c16(app#(z1,z2)) (33)
app#(Nil,z0) → c17 (35)
notEmpty#(Cons(z0,z1)) → c18 (37)
notEmpty#(Nil) → c19 (38)
part[False][Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,Cons(z1,z4)) (55)
part[False][Ite](False,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,z4) (57)
app(Nil,z0) → z0 (34)
part(z0,Cons(z1,z2),z3,z4) → part[Ite](>(z0,z1),z0,Cons(z1,z2),z3,z4) (28)
part[Ite](False,z0,Cons(z1,z2),z3,z4) → part[False][Ite](<(z0,z1),z0,Cons(z1,z2),z3,z4) (53)
app(Cons(z0,z1),z2) → Cons(z0,app(z1,z2)) (32)
part[Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,Cons(z1,z3),z4) (51)
part(z0,Nil,z1,z2) → app(z1,z2) (30)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
part#(z0,Cons(z1,z2),z3,z4) → c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) (29)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15(x1)] = 1 · x1 + 0
[c16(x1)] = 1 · x1 + 0
[c17] = 0
[c18] = 0
[c19] = 0
[<(x1, x2)] = 0
[quicksort(x1)] = 0
[qs(x1, x2)] = 1 + 1 · x1 + 1 · x1 · x1
[part(x1,...,x4)] = 1 · x2 + 0 + 1 · x3 + 1 · x4
[part[Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[>(x1, x2)] = 0
[app(x1, x2)] = 1 · x1 + 0 + 1 · x2
[part[False][Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[<#(x1, x2)] = 0
[>#(x1, x2)] = 0
[part[Ite]#(x1,...,x5)] = 2 · x3 + 0
[part[False][Ite]#(x1,...,x5)] = 2 · x3 + 0
[qs#(x1, x2)] = 1 · x2 · x2 + 0
[quicksort#(x1)] = 1 · x1 · x1 + 0
[part#(x1,...,x4)] = 1 + 2 · x2
[app#(x1, x2)] = 0
[notEmpty#(x1)] = 0
[S(x1)] = 0
[0] = 0
[False] = 0
[True] = 0
[Cons(x1, x2)] = 2 + 1 · x2
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
<#(S(z0),S(z1)) → c(<#(z0,z1)) (40)
<#(0,S(z0)) → c1 (42)
<#(z0,0) → c2 (44)
>#(S(z0),S(z1)) → c3(>#(z0,z1)) (46)
>#(0,z0) → c4 (48)
>#(S(z0),0) → c5 (50)
part[Ite]#(True,z0,Cons(z1,z2),z3,z4) → c6(part#(z0,z2,Cons(z1,z3),z4)) (52)
part[Ite]#(False,z0,Cons(z1,z2),z3,z4) → c7(part[False][Ite]#(<(z0,z1),z0,Cons(z1,z2),z3,z4),<#(z0,z1)) (54)
part[False][Ite]#(True,z0,Cons(z1,z2),z3,z4) → c8(part#(z0,z2,z3,Cons(z1,z4))) (56)
part[False][Ite]#(False,z0,Cons(z1,z2),z3,z4) → c9(part#(z0,z2,z3,z4)) (58)
qs#(z0,Cons(z1,z2)) → c10(app#(Cons(z1,Nil),Cons(z0,quicksort(z2))),quicksort#(z2)) (22)
quicksort#(Cons(z0,Cons(z1,z2))) → c11(qs#(z0,part(z0,Cons(z1,z2),Nil,Nil)),part#(z0,Cons(z1,z2),Nil,Nil)) (24)
quicksort#(Cons(z0,Nil)) → c12 (26)
quicksort#(Nil) → c13 (27)
part#(z0,Cons(z1,z2),z3,z4) → c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) (29)
part#(z0,Nil,z1,z2) → c15(app#(z1,z2)) (31)
app#(Cons(z0,z1),z2) → c16(app#(z1,z2)) (33)
app#(Nil,z0) → c17 (35)
notEmpty#(Cons(z0,z1)) → c18 (37)
notEmpty#(Nil) → c19 (38)
part[False][Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,Cons(z1,z4)) (55)
part[False][Ite](False,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,z4) (57)
app(Nil,z0) → z0 (34)
part(z0,Cons(z1,z2),z3,z4) → part[Ite](>(z0,z1),z0,Cons(z1,z2),z3,z4) (28)
part[Ite](False,z0,Cons(z1,z2),z3,z4) → part[False][Ite](<(z0,z1),z0,Cons(z1,z2),z3,z4) (53)
app(Cons(z0,z1),z2) → Cons(z0,app(z1,z2)) (32)
part[Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,Cons(z1,z3),z4) (51)
part(z0,Nil,z1,z2) → app(z1,z2) (30)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
app#(Cons(z0,z1),z2) → c16(app#(z1,z2)) (33)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1] = 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8(x1)] = 1 · x1 + 0
[c9(x1)] = 1 · x1 + 0
[c10(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13] = 0
[c14(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c15(x1)] = 1 · x1 + 0
[c16(x1)] = 1 · x1 + 0
[c17] = 0
[c18] = 0
[c19] = 0
[<(x1, x2)] = 0
[quicksort(x1)] = 0
[qs(x1, x2)] = 1 + 1 · x1 + 1 · x1 · x1
[part(x1,...,x4)] = 1 · x2 + 0 + 1 · x3 + 1 · x4
[part[Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[>(x1, x2)] = 0
[app(x1, x2)] = 1 · x1 + 0 + 1 · x2
[part[False][Ite](x1,...,x5)] = 1 · x3 + 0 + 1 · x4 + 1 · x5
[<#(x1, x2)] = 0
[>#(x1, x2)] = 0
[part[Ite]#(x1,...,x5)] = 1 · x3 + 0 + 1 · x4
[part[False][Ite]#(x1,...,x5)] = 1 · x3 + 0 + 1 · x4
[qs#(x1, x2)] = 1 + 1 · x2 · x2
[quicksort#(x1)] = 1 · x1 · x1 + 0
[part#(x1,...,x4)] = 1 · x2 + 0 + 1 · x3
[app#(x1, x2)] = 1 · x1 + 0
[notEmpty#(x1)] = 0
[S(x1)] = 0
[0] = 0
[False] = 0
[True] = 0
[Cons(x1, x2)] = 2 + 1 · x2
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
<#(S(z0),S(z1)) → c(<#(z0,z1)) (40)
<#(0,S(z0)) → c1 (42)
<#(z0,0) → c2 (44)
>#(S(z0),S(z1)) → c3(>#(z0,z1)) (46)
>#(0,z0) → c4 (48)
>#(S(z0),0) → c5 (50)
part[Ite]#(True,z0,Cons(z1,z2),z3,z4) → c6(part#(z0,z2,Cons(z1,z3),z4)) (52)
part[Ite]#(False,z0,Cons(z1,z2),z3,z4) → c7(part[False][Ite]#(<(z0,z1),z0,Cons(z1,z2),z3,z4),<#(z0,z1)) (54)
part[False][Ite]#(True,z0,Cons(z1,z2),z3,z4) → c8(part#(z0,z2,z3,Cons(z1,z4))) (56)
part[False][Ite]#(False,z0,Cons(z1,z2),z3,z4) → c9(part#(z0,z2,z3,z4)) (58)
qs#(z0,Cons(z1,z2)) → c10(app#(Cons(z1,Nil),Cons(z0,quicksort(z2))),quicksort#(z2)) (22)
quicksort#(Cons(z0,Cons(z1,z2))) → c11(qs#(z0,part(z0,Cons(z1,z2),Nil,Nil)),part#(z0,Cons(z1,z2),Nil,Nil)) (24)
quicksort#(Cons(z0,Nil)) → c12 (26)
quicksort#(Nil) → c13 (27)
part#(z0,Cons(z1,z2),z3,z4) → c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) (29)
part#(z0,Nil,z1,z2) → c15(app#(z1,z2)) (31)
app#(Cons(z0,z1),z2) → c16(app#(z1,z2)) (33)
app#(Nil,z0) → c17 (35)
notEmpty#(Cons(z0,z1)) → c18 (37)
notEmpty#(Nil) → c19 (38)
part[False][Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,Cons(z1,z4)) (55)
part[False][Ite](False,z0,Cons(z1,z2),z3,z4) → part(z0,z2,z3,z4) (57)
app(Nil,z0) → z0 (34)
part(z0,Cons(z1,z2),z3,z4) → part[Ite](>(z0,z1),z0,Cons(z1,z2),z3,z4) (28)
part[Ite](False,z0,Cons(z1,z2),z3,z4) → part[False][Ite](<(z0,z1),z0,Cons(z1,z2),z3,z4) (53)
app(Cons(z0,z1),z2) → Cons(z0,app(z1,z2)) (32)
part[Ite](True,z0,Cons(z1,z2),z3,z4) → part(z0,z2,Cons(z1,z3),z4) (51)
part(z0,Nil,z1,z2) → app(z1,z2) (30)

1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).