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) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
<#(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) |
notEmpty(Cons(z0,z1)) | → | True | (36) |
notEmpty(Nil) | → | False | (10) |
notEmpty#(Cons(z0,z1)) | → | c18 | (37) |
notEmpty#(Nil) | → | c19 | (38) |
[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 |
<#(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) |
quicksort#(Cons(z0,Nil)) | → | c12 | (26) |
quicksort#(Nil) | → | c13 | (27) |
[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 |
<#(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) |
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) |
[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 |
<#(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) |
part#(z0,Nil,z1,z2) | → | c15(app#(z1,z2)) | (31) |
[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 |
<#(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) |
app#(Nil,z0) | → | c17 | (35) |
[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 |
<#(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) |
part#(z0,Cons(z1,z2),z3,z4) | → | c14(part[Ite]#(>(z0,z1),z0,Cons(z1,z2),z3,z4),>#(z0,z1)) | (29) |
[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 |
<#(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) |
app#(Cons(z0,z1),z2) | → | c16(app#(z1,z2)) | (33) |
[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 |
<#(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) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).