Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Rubio_04/enno)

The rewrite relation of the following TRS is considered.

lt(0,s(X)) → true (1)
lt(s(X),0) → false (2)
lt(s(X),s(Y)) → lt(X,Y) (3)
append(nil,Y) → Y (4)
append(add(N,X),Y) → add(N,append(X,Y)) (5)
split(N,nil) → pair(nil,nil) (6)
split(N,add(M,Y)) → f_1(split(N,Y),N,M,Y) (7)
f_1(pair(X,Z),N,M,Y) → f_2(lt(N,M),N,M,Y,X,Z) (8)
f_2(true,N,M,Y,X,Z) → pair(X,add(M,Z)) (9)
f_2(false,N,M,Y,X,Z) → pair(add(M,X),Z) (10)
qsort(nil) → nil (11)
qsort(add(N,X)) → f_3(split(N,X),N,X) (12)
f_3(pair(Y,Z),N,X) → append(qsort(Y),add(X,qsort(Z))) (13)
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:
lt#(0,s(z0)) → c (15)
originates from
lt(0,s(z0)) → true (14)
lt#(s(z0),0) → c1 (17)
originates from
lt(s(z0),0) → false (16)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
originates from
lt(s(z0),s(z1)) → lt(z0,z1) (18)
append#(nil,z0) → c3 (21)
originates from
append(nil,z0) → z0 (20)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
originates from
append(add(z0,z1),z2) → add(z0,append(z1,z2)) (22)
split#(z0,nil) → c5 (25)
originates from
split(z0,nil) → pair(nil,nil) (24)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
originates from
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
originates from
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
originates from
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
originates from
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
qsort#(nil) → c10 (34)
originates from
qsort(nil) → nil (11)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
originates from
qsort(add(z0,z1)) → f_3(split(z0,z1),z0,z1) (35)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
originates from
f_3(pair(z0,z1),z2,z3) → append(qsort(z0),add(z3,qsort(z1))) (37)
Moreover, we add the following terms to the innermost strategy.
lt#(0,s(z0))
lt#(s(z0),0)
lt#(s(z0),s(z1))
append#(nil,z0)
append#(add(z0,z1),z2)
split#(z0,nil)
split#(z0,add(z1,z2))
f_1#(pair(z0,z1),z2,z3,z4)
f_2#(true,z0,z1,z2,z3,z4)
f_2#(false,z0,z1,z2,z3,z4)
qsort#(nil)
qsort#(add(z0,z1))
f_3#(pair(z0,z1),z2,z3)

1.1 Rule Shifting

The rules
append#(nil,z0) → c3 (21)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 1 + 1 · x1
[append(x1, x2)] = 1 + 1 · x1
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 1 + 1 · x1
[f_2(x1,...,x6)] = 1 + 1 · x5 + 1 · x6
[qsort(x1)] = 1 + 1 · x1
[f_3(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[lt#(x1, x2)] = 0
[append#(x1, x2)] = 1
[split#(x1, x2)] = 0
[f_1#(x1,...,x4)] = 0
[f_2#(x1,...,x6)] = 0
[qsort#(x1)] = 1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 + 1 · x1
[nil] = 0
[add(x1, x2)] = 1 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 1
[s(x1)] = 1 + 1 · x1
[true] = 1
[false] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)

1.1.1 Rule Shifting

The rules
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 1
[append(x1, x2)] = 3
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 2 + 1 · x1
[f_2(x1,...,x6)] = 1 + 1 · x1 + 1 · x5 + 1 · x6
[qsort(x1)] = 0
[f_3(x1, x2, x3)] = 3 + 3 · x2 + 3 · x3
[lt#(x1, x2)] = 0
[append#(x1, x2)] = 0
[split#(x1, x2)] = 0
[f_1#(x1,...,x4)] = 0
[f_2#(x1,...,x6)] = 0
[qsort#(x1)] = 1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 + 1 · x1
[nil] = 0
[add(x1, x2)] = 2 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 0
[s(x1)] = 1 · x1 + 0
[true] = 1
[false] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
lt(s(z0),0) → false (16)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)
lt(0,s(z0)) → true (14)
lt(s(z0),s(z1)) → lt(z0,z1) (18)

1.1.1.1 Rule Shifting

The rules
qsort#(nil) → c10 (34)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 1 + 1 · x1
[append(x1, x2)] = 1 + 1 · x1
[split(x1, x2)] = 1 + 1 · x2
[f_1(x1,...,x4)] = 1 + 1 · x1
[f_2(x1,...,x6)] = 1 + 1 · x5 + 1 · x6
[qsort(x1)] = 1 + 1 · x1
[f_3(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[lt#(x1, x2)] = 0
[append#(x1, x2)] = 0
[split#(x1, x2)] = 0
[f_1#(x1,...,x4)] = 0
[f_2#(x1,...,x6)] = 0
[qsort#(x1)] = 1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 · x1 + 0
[nil] = 1
[add(x1, x2)] = 1 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 1
[s(x1)] = 1 + 1 · x1
[true] = 1
[false] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)

1.1.1.1.1 Rule Shifting

The rules
split#(z0,nil) → c5 (25)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 1 + 1 · x1
[append(x1, x2)] = 1 + 1 · x1 + 1 · x2
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 1 + 1 · x1
[f_2(x1,...,x6)] = 1 + 1 · x5 + 1 · x6
[qsort(x1)] = 1 + 1 · x1
[f_3(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[lt#(x1, x2)] = 0
[append#(x1, x2)] = 0
[split#(x1, x2)] = 1
[f_1#(x1,...,x4)] = 0
[f_2#(x1,...,x6)] = 0
[qsort#(x1)] = 1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 · x1 + 0
[nil] = 0
[add(x1, x2)] = 1 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 1
[s(x1)] = 1 + 1 · x1
[true] = 1
[false] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)

1.1.1.1.1.1 Rule Shifting

The rules
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 0
[append(x1, x2)] = 1 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 1 · x1 + 0 + 1 · x3
[f_2(x1,...,x6)] = 1 · x3 + 0 + 1 · x5 + 1 · x6
[qsort(x1)] = 0
[f_3(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2
[lt#(x1, x2)] = 1 · x1 · x2 + 0
[append#(x1, x2)] = 0
[split#(x1, x2)] = 1 · x1 · x2 + 0
[f_1#(x1,...,x4)] = 1 · x2 · x3 + 0
[f_2#(x1,...,x6)] = 0
[qsort#(x1)] = 1 · x1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 · x1 · x1 + 0 + 1 · x2 · x2
[nil] = 0
[add(x1, x2)] = 1 · x1 + 0 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 0
[s(x1)] = 2 + 1 · x1
[true] = 0
[false] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)

1.1.1.1.1.1.1 Rule Shifting

The rules
lt#(s(z0),0) → c1 (17)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 0
[append(x1, x2)] = 2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 2 + 1 · x1 + 1 · x3
[f_2(x1,...,x6)] = 2 + 1 · x3 + 1 · x5 + 1 · x6
[qsort(x1)] = 0
[f_3(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2
[lt#(x1, x2)] = 1 · x1 + 0
[append#(x1, x2)] = 0
[split#(x1, x2)] = 1 · x1 + 0 + 1 · x1 · x2
[f_1#(x1,...,x4)] = 2 · x2 + 0
[f_2#(x1,...,x6)] = 0
[qsort#(x1)] = 1 · x1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 · x2 + 0 + 1 · x3 + 1 · x1 · x1
[nil] = 0
[add(x1, x2)] = 2 + 1 · x1 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 0
[s(x1)] = 1 + 1 · x1
[true] = 0
[false] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
lt#(0,s(z0)) → c (15)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 0
[append(x1, x2)] = 2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 1 · x1 + 0 + 1 · x3
[f_2(x1,...,x6)] = 1 · x3 + 0 + 1 · x5 + 1 · x6
[qsort(x1)] = 0
[f_3(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2
[lt#(x1, x2)] = 2 · x1 · x2 + 0
[append#(x1, x2)] = 0
[split#(x1, x2)] = 2 · x1 · x2 + 0
[f_1#(x1,...,x4)] = 2 · x2 · x3 + 0
[f_2#(x1,...,x6)] = 0
[qsort#(x1)] = 1 · x1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 · x1 · x1 + 0
[nil] = 0
[add(x1, x2)] = 1 · x1 + 0 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 1
[s(x1)] = 2 + 1 · x1
[true] = 0
[false] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 1 · x1 · x2 + 0
[append(x1, x2)] = 2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 1 · x1 + 0 + 1 · x3
[f_2(x1,...,x6)] = 1 · x3 + 0 + 1 · x5 + 1 · x6
[qsort(x1)] = 0
[f_3(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2
[lt#(x1, x2)] = 0
[append#(x1, x2)] = 0
[split#(x1, x2)] = 2 · x1 · x2 + 0
[f_1#(x1,...,x4)] = 1 · x2 · x3 + 0
[f_2#(x1,...,x6)] = 1 · x1 + 0
[qsort#(x1)] = 1 · x1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 · x1 · x1 + 0 + 1 · x2 · x2
[nil] = 0
[add(x1, x2)] = 1 · x1 + 0 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 2
[s(x1)] = 2 + 1 · x1
[true] = 0
[false] = 2
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
lt(s(z0),0) → false (16)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)
lt(0,s(z0)) → true (14)
lt(s(z0),s(z1)) → lt(z0,z1) (18)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 1 · x1 · x2 + 0
[append(x1, x2)] = 2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 1 · x1 + 0 + 1 · x3
[f_2(x1,...,x6)] = 1 · x3 + 0 + 1 · x5 + 1 · x6
[qsort(x1)] = 0
[f_3(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2
[lt#(x1, x2)] = 0
[append#(x1, x2)] = 0
[split#(x1, x2)] = 2 · x1 · x2 + 0
[f_1#(x1,...,x4)] = 2 · x2 · x3 + 0
[f_2#(x1,...,x6)] = 2 · x1 + 0
[qsort#(x1)] = 1 · x1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 · x1 · x1 + 0 + 1 · x2 · x2
[nil] = 0
[add(x1, x2)] = 1 · x1 + 0 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 1
[s(x1)] = 1 + 1 · x1
[true] = 1
[false] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
lt(s(z0),0) → false (16)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)
lt(0,s(z0)) → true (14)
lt(s(z0),s(z1)) → lt(z0,z1) (18)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 0
[append(x1, x2)] = 2 + 1 · x2 · x2 + 1 · x1 · x2 + 1 · x1 · x1
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 1 + 1 · x1
[f_2(x1,...,x6)] = 1 + 1 · x5 + 1 · x6
[qsort(x1)] = 0
[f_3(x1, x2, x3)] = 1 + 1 · x2 + 1 · x3 + 1 · x3 · x3 + 1 · x2 · x3 + 1 · x2 · x2
[lt#(x1, x2)] = 0
[append#(x1, x2)] = 0
[split#(x1, x2)] = 2 · x2 + 0
[f_1#(x1,...,x4)] = 1
[f_2#(x1,...,x6)] = 0
[qsort#(x1)] = 1 · x1 · x1 + 0
[f_3#(x1, x2, x3)] = 1 · x1 · x1 + 0
[nil] = 0
[add(x1, x2)] = 1 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 2
[s(x1)] = 0
[true] = 0
[false] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9] = 0
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12(x1, x2, x3)] = 1 · x1 + 0 + 1 · x2 + 1 · x3
[lt(x1, x2)] = 0
[append(x1, x2)] = 1 · x1 + 0 + 1 · x2
[split(x1, x2)] = 1 · x2 + 0
[f_1(x1,...,x4)] = 2 + 1 · x1
[f_2(x1,...,x6)] = 2 + 1 · x5 + 1 · x6
[qsort(x1)] = 1 · x1 + 0
[f_3(x1, x2, x3)] = 2 + 1 · x1
[lt#(x1, x2)] = 0
[append#(x1, x2)] = 2 · x1 + 0
[split#(x1, x2)] = 0
[f_1#(x1,...,x4)] = 0
[f_2#(x1,...,x6)] = 0
[qsort#(x1)] = 1 · x1 · x1 + 0
[f_3#(x1, x2, x3)] = 2 + 2 · x1 + 1 · x1 · x1
[nil] = 0
[add(x1, x2)] = 2 + 1 · x2
[pair(x1, x2)] = 1 · x1 + 0 + 1 · x2
[0] = 2
[s(x1)] = 0
[true] = 0
[false] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
lt#(0,s(z0)) → c (15)
lt#(s(z0),0) → c1 (17)
lt#(s(z0),s(z1)) → c2(lt#(z0,z1)) (19)
append#(nil,z0) → c3 (21)
append#(add(z0,z1),z2) → c4(append#(z1,z2)) (23)
split#(z0,nil) → c5 (25)
split#(z0,add(z1,z2)) → c6(f_1#(split(z0,z2),z0,z1,z2),split#(z0,z2)) (27)
f_1#(pair(z0,z1),z2,z3,z4) → c7(f_2#(lt(z2,z3),z2,z3,z4,z0,z1),lt#(z2,z3)) (29)
f_2#(true,z0,z1,z2,z3,z4) → c8 (31)
f_2#(false,z0,z1,z2,z3,z4) → c9 (33)
qsort#(nil) → c10 (34)
qsort#(add(z0,z1)) → c11(f_3#(split(z0,z1),z0,z1),split#(z0,z1)) (36)
f_3#(pair(z0,z1),z2,z3) → c12(append#(qsort(z0),add(z3,qsort(z1))),qsort#(z0),qsort#(z1)) (38)
f_1(pair(z0,z1),z2,z3,z4) → f_2(lt(z2,z3),z2,z3,z4,z0,z1) (28)
f_2(true,z0,z1,z2,z3,z4) → pair(z3,add(z1,z4)) (30)
split(z0,nil) → pair(nil,nil) (24)
f_3(pair(z0,z1),z2,z3) → append(qsort(z0),add(z3,qsort(z1))) (37)
qsort(nil) → nil (11)
f_2(false,z0,z1,z2,z3,z4) → pair(add(z1,z3),z4) (32)
append(nil,z0) → z0 (20)
split(z0,add(z1,z2)) → f_1(split(z0,z2),z0,z1,z2) (26)
append(add(z0,z1),z2) → add(z0,append(z1,z2)) (22)
qsort(add(z0,z1)) → f_3(split(z0,z1),z0,z1) (35)

1.1.1.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).