Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Others/bubblesort)

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

bsort(S(x'),Cons(x,xs)) → bsort(x',bubble(x,xs)) (1)
len(Cons(x,xs)) → +(S(0),len(xs)) (2)
bubble(x',Cons(x,xs)) → bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs)) (3)
len(Nil) → 0 (4)
bubble(x,Nil) → Cons(x,Nil) (5)
bsort(0,xs) → xs (6)
bubblesort(xs) → bsort(len(xs),xs) (7)

and S is the following TRS.

+(x,S(0)) → S(x) (8)
+(S(0),y) → S(y) (9)
<(S(x),S(y)) → <(x,y) (10)
<(0,S(y)) → True (11)
<(x,0) → False (12)
bubble[Ite][False][Ite](False,x',Cons(x,xs)) → Cons(x,bubble(x',xs)) (13)
bubble[Ite][False][Ite](True,x',Cons(x,xs)) → Cons(x',bubble(x,xs)) (14)
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:
bsort#(S(z0),Cons(z1,z2)) → c7(bsort#(z0,bubble(z1,z2)),bubble#(z1,z2)) (16)
originates from
bsort(S(z0),Cons(z1,z2)) → bsort(z0,bubble(z1,z2)) (15)
bsort#(0,z0) → c8 (18)
originates from
bsort(0,z0) → z0 (17)
len#(Cons(z0,z1)) → c9(+#(S(0),len(z1)),len#(z1)) (20)
originates from
len(Cons(z0,z1)) → +(S(0),len(z1)) (19)
len#(Nil) → c10 (21)
originates from
len(Nil) → 0 (4)
bubble#(z0,Cons(z1,z2)) → c11(bubble[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) (23)
originates from
bubble(z0,Cons(z1,z2)) → bubble[Ite][False][Ite](<(z0,z1),z0,Cons(z1,z2)) (22)
bubble#(z0,Nil) → c12 (25)
originates from
bubble(z0,Nil) → Cons(z0,Nil) (24)
bubblesort#(z0) → c13(bsort#(len(z0),z0),len#(z0)) (27)
originates from
bubblesort(z0) → bsort(len(z0),z0) (26)
+#(z0,S(0)) → c (29)
originates from
+(z0,S(0)) → S(z0) (28)
+#(S(0),z0) → c1 (31)
originates from
+(S(0),z0) → S(z0) (30)
<#(S(z0),S(z1)) → c2(<#(z0,z1)) (33)
originates from
<(S(z0),S(z1)) → <(z0,z1) (32)
<#(0,S(z0)) → c3 (35)
originates from
<(0,S(z0)) → True (34)
<#(z0,0) → c4 (37)
originates from
<(z0,0) → False (36)
bubble[Ite][False][Ite]#(False,z0,Cons(z1,z2)) → c5(bubble#(z0,z2)) (39)
originates from
bubble[Ite][False][Ite](False,z0,Cons(z1,z2)) → Cons(z1,bubble(z0,z2)) (38)
bubble[Ite][False][Ite]#(True,z0,Cons(z1,z2)) → c6(bubble#(z1,z2)) (41)
originates from
bubble[Ite][False][Ite](True,z0,Cons(z1,z2)) → Cons(z0,bubble(z1,z2)) (40)
Moreover, we add the following terms to the innermost strategy.
+#(z0,S(0))
+#(S(0),z0)
<#(S(z0),S(z1))
<#(0,S(z0))
<#(z0,0)
bubble[Ite][False][Ite]#(False,z0,Cons(z1,z2))
bubble[Ite][False][Ite]#(True,z0,Cons(z1,z2))
bsort#(S(z0),Cons(z1,z2))
bsort#(0,z0)
len#(Cons(z0,z1))
len#(Nil)
bubble#(z0,Cons(z1,z2))
bubble#(z0,Nil)
bubblesort#(z0)

1.1 Usable Rules

We remove the following rules since they are not usable.
bsort(S(z0),Cons(z1,z2)) → bsort(z0,bubble(z1,z2)) (15)
bsort(0,z0) → z0 (17)
bubblesort(z0) → bsort(len(z0),z0) (26)

1.1.1 Rule Shifting

The rules
bsort#(0,z0) → c8 (18)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13(x1, x2)] = 1 · x1 + 0 + 1 · x2
[bubble(x1, x2)] = 1 + 1 · x1 + 1 · x2
[bubble[Ite][False][Ite](x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[<(x1, x2)] = 1 + 1 · x2
[len(x1)] = 1 + 1 · x1
[+(x1, x2)] = 1 + 1 · x1 + 1 · x2
[+#(x1, x2)] = 1 · x1 + 0
[<#(x1, x2)] = 0
[bubble[Ite][False][Ite]#(x1, x2, x3)] = 0
[bsort#(x1, x2)] = 1
[len#(x1)] = 0
[bubble#(x1, x2)] = 0
[bubblesort#(x1)] = 1
[Cons(x1, x2)] = 1 · x1 + 0
[S(x1)] = 0
[0] = 0
[Nil] = 0
[True] = 1
[False] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
+#(z0,S(0)) → c (29)
+#(S(0),z0) → c1 (31)
<#(S(z0),S(z1)) → c2(<#(z0,z1)) (33)
<#(0,S(z0)) → c3 (35)
<#(z0,0) → c4 (37)
bubble[Ite][False][Ite]#(False,z0,Cons(z1,z2)) → c5(bubble#(z0,z2)) (39)
bubble[Ite][False][Ite]#(True,z0,Cons(z1,z2)) → c6(bubble#(z1,z2)) (41)
bsort#(S(z0),Cons(z1,z2)) → c7(bsort#(z0,bubble(z1,z2)),bubble#(z1,z2)) (16)
bsort#(0,z0) → c8 (18)
len#(Cons(z0,z1)) → c9(+#(S(0),len(z1)),len#(z1)) (20)
len#(Nil) → c10 (21)
bubble#(z0,Cons(z1,z2)) → c11(bubble[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) (23)
bubble#(z0,Nil) → c12 (25)
bubblesort#(z0) → c13(bsort#(len(z0),z0),len#(z0)) (27)

1.1.1.1 Rule Shifting

The rules
len#(Nil) → c10 (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] = 0
[c5(x1)] = 1 · x1 + 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13(x1, x2)] = 1 · x1 + 0 + 1 · x2
[bubble(x1, x2)] = 1 + 1 · x1 + 1 · x2
[bubble[Ite][False][Ite](x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[<(x1, x2)] = 1 + 1 · x2
[len(x1)] = 1 + 1 · x1
[+(x1, x2)] = 1 + 1 · x1 + 1 · x2
[+#(x1, x2)] = 1 · x1 + 0
[<#(x1, x2)] = 0
[bubble[Ite][False][Ite]#(x1, x2, x3)] = 0
[bsort#(x1, x2)] = 0
[len#(x1)] = 1
[bubble#(x1, x2)] = 0
[bubblesort#(x1)] = 1
[Cons(x1, x2)] = 1 · x1 + 0
[S(x1)] = 0
[0] = 0
[Nil] = 0
[True] = 1
[False] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
+#(z0,S(0)) → c (29)
+#(S(0),z0) → c1 (31)
<#(S(z0),S(z1)) → c2(<#(z0,z1)) (33)
<#(0,S(z0)) → c3 (35)
<#(z0,0) → c4 (37)
bubble[Ite][False][Ite]#(False,z0,Cons(z1,z2)) → c5(bubble#(z0,z2)) (39)
bubble[Ite][False][Ite]#(True,z0,Cons(z1,z2)) → c6(bubble#(z1,z2)) (41)
bsort#(S(z0),Cons(z1,z2)) → c7(bsort#(z0,bubble(z1,z2)),bubble#(z1,z2)) (16)
bsort#(0,z0) → c8 (18)
len#(Cons(z0,z1)) → c9(+#(S(0),len(z1)),len#(z1)) (20)
len#(Nil) → c10 (21)
bubble#(z0,Cons(z1,z2)) → c11(bubble[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) (23)
bubble#(z0,Nil) → c12 (25)
bubblesort#(z0) → c13(bsort#(len(z0),z0),len#(z0)) (27)

1.1.1.1.1 Rule Shifting

The rules
bubblesort#(z0) → c13(bsort#(len(z0),z0),len#(z0)) (27)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13(x1, x2)] = 1 · x1 + 0 + 1 · x2
[bubble(x1, x2)] = 2 + 2 · x2
[bubble[Ite][False][Ite](x1, x2, x3)] = 0
[<(x1, x2)] = 0
[len(x1)] = 0
[+(x1, x2)] = 3 + 3 · x1
[+#(x1, x2)] = 3 · x1 + 0
[<#(x1, x2)] = 0
[bubble[Ite][False][Ite]#(x1, x2, x3)] = 0
[bsort#(x1, x2)] = 0
[len#(x1)] = 2
[bubble#(x1, x2)] = 0
[bubblesort#(x1)] = 3
[Cons(x1, x2)] = 0
[S(x1)] = 0
[0] = 0
[Nil] = 2
[True] = 0
[False] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
+#(z0,S(0)) → c (29)
+#(S(0),z0) → c1 (31)
<#(S(z0),S(z1)) → c2(<#(z0,z1)) (33)
<#(0,S(z0)) → c3 (35)
<#(z0,0) → c4 (37)
bubble[Ite][False][Ite]#(False,z0,Cons(z1,z2)) → c5(bubble#(z0,z2)) (39)
bubble[Ite][False][Ite]#(True,z0,Cons(z1,z2)) → c6(bubble#(z1,z2)) (41)
bsort#(S(z0),Cons(z1,z2)) → c7(bsort#(z0,bubble(z1,z2)),bubble#(z1,z2)) (16)
bsort#(0,z0) → c8 (18)
len#(Cons(z0,z1)) → c9(+#(S(0),len(z1)),len#(z1)) (20)
len#(Nil) → c10 (21)
bubble#(z0,Cons(z1,z2)) → c11(bubble[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) (23)
bubble#(z0,Nil) → c12 (25)
bubblesort#(z0) → c13(bsort#(len(z0),z0),len#(z0)) (27)

1.1.1.1.1.1 Rule Shifting

The rules
len#(Cons(z0,z1)) → c9(+#(S(0),len(z1)),len#(z1)) (20)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13(x1, x2)] = 1 · x1 + 0 + 1 · x2
[bubble(x1, x2)] = 1 + 1 · x1 + 1 · x2
[bubble[Ite][False][Ite](x1, x2, x3)] = 1 + 1 · x2 + 1 · x3
[<(x1, x2)] = 1 + 1 · x2
[len(x1)] = 1 + 1 · x1
[+(x1, x2)] = 1 + 1 · x1 + 1 · x2
[+#(x1, x2)] = 1 · x1 + 0
[<#(x1, x2)] = 0
[bubble[Ite][False][Ite]#(x1, x2, x3)] = 0
[bsort#(x1, x2)] = 1
[len#(x1)] = 1 · x1 + 0
[bubble#(x1, x2)] = 0
[bubblesort#(x1)] = 1 + 1 · x1
[Cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[S(x1)] = 0
[0] = 0
[Nil] = 1
[True] = 1
[False] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
+#(z0,S(0)) → c (29)
+#(S(0),z0) → c1 (31)
<#(S(z0),S(z1)) → c2(<#(z0,z1)) (33)
<#(0,S(z0)) → c3 (35)
<#(z0,0) → c4 (37)
bubble[Ite][False][Ite]#(False,z0,Cons(z1,z2)) → c5(bubble#(z0,z2)) (39)
bubble[Ite][False][Ite]#(True,z0,Cons(z1,z2)) → c6(bubble#(z1,z2)) (41)
bsort#(S(z0),Cons(z1,z2)) → c7(bsort#(z0,bubble(z1,z2)),bubble#(z1,z2)) (16)
bsort#(0,z0) → c8 (18)
len#(Cons(z0,z1)) → c9(+#(S(0),len(z1)),len#(z1)) (20)
len#(Nil) → c10 (21)
bubble#(z0,Cons(z1,z2)) → c11(bubble[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) (23)
bubble#(z0,Nil) → c12 (25)
bubblesort#(z0) → c13(bsort#(len(z0),z0),len#(z0)) (27)

1.1.1.1.1.1.1 Rule Shifting

The rules
bsort#(S(z0),Cons(z1,z2)) → c7(bsort#(z0,bubble(z1,z2)),bubble#(z1,z2)) (16)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c] = 0
[c1] = 0
[c2(x1)] = 1 · x1 + 0
[c3] = 0
[c4] = 0
[c5(x1)] = 1 · x1 + 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13(x1, x2)] = 1 · x1 + 0 + 1 · x2
[bubble(x1, x2)] = 3 + 2 · x1 + 2 · x2
[bubble[Ite][False][Ite](x1, x2, x3)] = 3 + 3 · x2
[<(x1, x2)] = 0
[len(x1)] = 2 · x1 + 0
[+(x1, x2)] = 1 · x1 + 0 + 1 · x2
[+#(x1, x2)] = 0
[<#(x1, x2)] = 0
[bubble[Ite][False][Ite]#(x1, x2, x3)] = 0
[bsort#(x1, x2)] = 1 + 1 · x1
[len#(x1)] = 1
[bubble#(x1, x2)] = 0
[bubblesort#(x1)] = 2 + 3 · x1
[Cons(x1, x2)] = 2 + 1 · x2
[S(x1)] = 1 + 1 · x1
[0] = 0
[Nil] = 0
[True] = 0
[False] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
+#(z0,S(0)) → c (29)
+#(S(0),z0) → c1 (31)
<#(S(z0),S(z1)) → c2(<#(z0,z1)) (33)
<#(0,S(z0)) → c3 (35)
<#(z0,0) → c4 (37)
bubble[Ite][False][Ite]#(False,z0,Cons(z1,z2)) → c5(bubble#(z0,z2)) (39)
bubble[Ite][False][Ite]#(True,z0,Cons(z1,z2)) → c6(bubble#(z1,z2)) (41)
bsort#(S(z0),Cons(z1,z2)) → c7(bsort#(z0,bubble(z1,z2)),bubble#(z1,z2)) (16)
bsort#(0,z0) → c8 (18)
len#(Cons(z0,z1)) → c9(+#(S(0),len(z1)),len#(z1)) (20)
len#(Nil) → c10 (21)
bubble#(z0,Cons(z1,z2)) → c11(bubble[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) (23)
bubble#(z0,Nil) → c12 (25)
bubblesort#(z0) → c13(bsort#(len(z0),z0),len#(z0)) (27)
len(Nil) → 0 (4)
len(Cons(z0,z1)) → +(S(0),len(z1)) (19)
+(z0,S(0)) → S(z0) (28)
+(S(0),z0) → S(z0) (30)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
bubble#(z0,Nil) → c12 (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] = 0
[c5(x1)] = 1 · x1 + 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13(x1, x2)] = 1 · x1 + 0 + 1 · x2
[bubble(x1, x2)] = 3 + 2 · x1 + 2 · x2
[bubble[Ite][False][Ite](x1, x2, x3)] = 3 + 3 · x2
[<(x1, x2)] = 0
[len(x1)] = 1 · x1 + 0
[+(x1, x2)] = 1 · x1 + 0 + 1 · x2
[+#(x1, x2)] = 0
[<#(x1, x2)] = 0
[bubble[Ite][False][Ite]#(x1, x2, x3)] = 1
[bsort#(x1, x2)] = 1 + 1 · x1
[len#(x1)] = 1
[bubble#(x1, x2)] = 1
[bubblesort#(x1)] = 2 + 1 · x1
[Cons(x1, x2)] = 1 + 1 · x2
[S(x1)] = 1 + 1 · x1
[0] = 0
[Nil] = 0
[True] = 0
[False] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
+#(z0,S(0)) → c (29)
+#(S(0),z0) → c1 (31)
<#(S(z0),S(z1)) → c2(<#(z0,z1)) (33)
<#(0,S(z0)) → c3 (35)
<#(z0,0) → c4 (37)
bubble[Ite][False][Ite]#(False,z0,Cons(z1,z2)) → c5(bubble#(z0,z2)) (39)
bubble[Ite][False][Ite]#(True,z0,Cons(z1,z2)) → c6(bubble#(z1,z2)) (41)
bsort#(S(z0),Cons(z1,z2)) → c7(bsort#(z0,bubble(z1,z2)),bubble#(z1,z2)) (16)
bsort#(0,z0) → c8 (18)
len#(Cons(z0,z1)) → c9(+#(S(0),len(z1)),len#(z1)) (20)
len#(Nil) → c10 (21)
bubble#(z0,Cons(z1,z2)) → c11(bubble[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) (23)
bubble#(z0,Nil) → c12 (25)
bubblesort#(z0) → c13(bsort#(len(z0),z0),len#(z0)) (27)
len(Nil) → 0 (4)
len(Cons(z0,z1)) → +(S(0),len(z1)) (19)
+(z0,S(0)) → S(z0) (28)
+(S(0),z0) → S(z0) (30)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules
bubble#(z0,Cons(z1,z2)) → c11(bubble[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) (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] = 0
[c5(x1)] = 1 · x1 + 0
[c6(x1)] = 1 · x1 + 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[c9(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c10] = 0
[c11(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c12] = 0
[c13(x1, x2)] = 1 · x1 + 0 + 1 · x2
[bubble(x1, x2)] = 2 + 1 · x2
[bubble[Ite][False][Ite](x1, x2, x3)] = 2 + 1 · x3
[<(x1, x2)] = 0
[len(x1)] = 1 · x1 + 0
[+(x1, x2)] = 1 · x1 + 0 + 1 · x2
[+#(x1, x2)] = 0
[<#(x1, x2)] = 0
[bubble[Ite][False][Ite]#(x1, x2, x3)] = 2 · x3 + 0
[bsort#(x1, x2)] = 1 + 2 · x1 · x2
[len#(x1)] = 1
[bubble#(x1, x2)] = 2 + 2 · x2
[bubblesort#(x1)] = 2 + 1 · x1 + 2 · x1 · x1
[Cons(x1, x2)] = 2 + 1 · x2
[S(x1)] = 1 + 1 · x1
[0] = 0
[Nil] = 0
[True] = 0
[False] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
+#(z0,S(0)) → c (29)
+#(S(0),z0) → c1 (31)
<#(S(z0),S(z1)) → c2(<#(z0,z1)) (33)
<#(0,S(z0)) → c3 (35)
<#(z0,0) → c4 (37)
bubble[Ite][False][Ite]#(False,z0,Cons(z1,z2)) → c5(bubble#(z0,z2)) (39)
bubble[Ite][False][Ite]#(True,z0,Cons(z1,z2)) → c6(bubble#(z1,z2)) (41)
bsort#(S(z0),Cons(z1,z2)) → c7(bsort#(z0,bubble(z1,z2)),bubble#(z1,z2)) (16)
bsort#(0,z0) → c8 (18)
len#(Cons(z0,z1)) → c9(+#(S(0),len(z1)),len#(z1)) (20)
len#(Nil) → c10 (21)
bubble#(z0,Cons(z1,z2)) → c11(bubble[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) (23)
bubble#(z0,Nil) → c12 (25)
bubblesort#(z0) → c13(bsort#(len(z0),z0),len#(z0)) (27)
bubble[Ite][False][Ite](True,z0,Cons(z1,z2)) → Cons(z0,bubble(z1,z2)) (40)
len(Nil) → 0 (4)
bubble(z0,Nil) → Cons(z0,Nil) (24)
len(Cons(z0,z1)) → +(S(0),len(z1)) (19)
bubble(z0,Cons(z1,z2)) → bubble[Ite][False][Ite](<(z0,z1),z0,Cons(z1,z2)) (22)
+(z0,S(0)) → S(z0) (28)
+(S(0),z0) → S(z0) (30)
bubble[Ite][False][Ite](False,z0,Cons(z1,z2)) → Cons(z1,bubble(z0,z2)) (38)

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