* Step 1: Sum WORST_CASE(Omega(n^1),O(n^2))
+ Considered Problem:
- Strict TRS:
bsort(0(),xs) -> xs
bsort(S(x'),Cons(x,xs)) -> bsort(x',bubble(x,xs))
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubblesort(xs) -> bsort(len(xs),xs)
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
- Signature:
{+/2, xs
bsort(S(x'),Cons(x,xs)) -> bsort(x',bubble(x,xs))
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubblesort(xs) -> bsort(len(xs),xs)
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
- Signature:
{+/2, Cons(x,y)} =
len(Cons(x,y)) ->^+ +(S(0()),len(y))
= C[len(y) = len(y){}]
** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
bsort(0(),xs) -> xs
bsort(S(x'),Cons(x,xs)) -> bsort(x',bubble(x,xs))
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubblesort(xs) -> bsort(len(xs),xs)
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
- Signature:
{+/2, c_1()
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs))
len#(Nil()) -> c_7()
Weak DPs
+#(x,S(0())) -> c_8()
+#(S(0()),y) -> c_9()
<#(x,0()) -> c_10()
<#(0(),S(y)) -> c_11()
<#(S(x),S(y)) -> c_12(<#(x,y))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
and mark the set of starting terms.
** Step 1.b:2: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bsort#(0(),xs) -> c_1()
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs))
len#(Nil()) -> c_7()
- Weak DPs:
+#(x,S(0())) -> c_8()
+#(S(0()),y) -> c_9()
<#(x,0()) -> c_10()
<#(0(),S(y)) -> c_11()
<#(S(x),S(y)) -> c_12(<#(x,y))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bsort(0(),xs) -> xs
bsort(S(x'),Cons(x,xs)) -> bsort(x',bubble(x,xs))
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
bubblesort(xs) -> bsort(len(xs),xs)
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
+#(x,S(0())) -> c_8()
+#(S(0()),y) -> c_9()
<#(x,0()) -> c_10()
<#(0(),S(y)) -> c_11()
<#(S(x),S(y)) -> c_12(<#(x,y))
bsort#(0(),xs) -> c_1()
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs))
len#(Nil()) -> c_7()
** Step 1.b:3: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bsort#(0(),xs) -> c_1()
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs))
len#(Nil()) -> c_7()
- Weak DPs:
+#(x,S(0())) -> c_8()
+#(S(0()),y) -> c_9()
<#(x,0()) -> c_10()
<#(0(),S(y)) -> c_11()
<#(S(x),S(y)) -> c_12(<#(x,y))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_1()
2: bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
3: bubble#(x,Nil()) -> c_3()
4: bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
5: bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
6: len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs))
7: len#(Nil()) -> c_7()
8: +#(x,S(0())) -> c_8()
9: +#(S(0()),y) -> c_9()
10: <#(x,0()) -> c_10()
11: <#(0(),S(y)) -> c_11()
12: <#(S(x),S(y)) -> c_12(<#(x,y))
13: bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
14: bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
** Step 1.b:4: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs))
- Weak DPs:
+#(x,S(0())) -> c_8()
+#(S(0()),y) -> c_9()
<#(x,0()) -> c_10()
<#(0(),S(y)) -> c_11()
<#(S(x),S(y)) -> c_12(<#(x,y))
bsort#(0(),xs) -> c_1()
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
len#(Nil()) -> c_7()
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
-->_2 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):3
-->_1 bsort#(0(),xs) -> c_1():11
-->_2 bubble#(x,Nil()) -> c_3():2
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
2:S:bubble#(x,Nil()) -> c_3()
3:S:bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
-->_1 bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs)):13
-->_1 bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs)):12
-->_2 <#(S(x),S(y)) -> c_12(<#(x,y)):10
-->_2 <#(0(),S(y)) -> c_11():9
-->_2 <#(x,0()) -> c_10():8
4:S:bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
-->_2 len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs)):5
-->_2 len#(Nil()) -> c_7():14
-->_1 bsort#(0(),xs) -> c_1():11
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
5:S:len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs))
-->_2 len#(Nil()) -> c_7():14
-->_1 +#(S(0()),y) -> c_9():7
-->_1 +#(x,S(0())) -> c_8():6
-->_2 len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs)):5
6:W:+#(x,S(0())) -> c_8()
7:W:+#(S(0()),y) -> c_9()
8:W:<#(x,0()) -> c_10()
9:W:<#(0(),S(y)) -> c_11()
10:W:<#(S(x),S(y)) -> c_12(<#(x,y))
-->_1 <#(S(x),S(y)) -> c_12(<#(x,y)):10
-->_1 <#(0(),S(y)) -> c_11():9
-->_1 <#(x,0()) -> c_10():8
11:W:bsort#(0(),xs) -> c_1()
12:W:bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):3
-->_1 bubble#(x,Nil()) -> c_3():2
13:W:bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):3
-->_1 bubble#(x,Nil()) -> c_3():2
14:W:len#(Nil()) -> c_7()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
6: +#(x,S(0())) -> c_8()
7: +#(S(0()),y) -> c_9()
14: len#(Nil()) -> c_7()
11: bsort#(0(),xs) -> c_1()
10: <#(S(x),S(y)) -> c_12(<#(x,y))
8: <#(x,0()) -> c_10()
9: <#(0(),S(y)) -> c_11()
** Step 1.b:5: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs))
- Weak DPs:
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
-->_2 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):3
-->_2 bubble#(x,Nil()) -> c_3():2
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
2:S:bubble#(x,Nil()) -> c_3()
3:S:bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
-->_1 bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs)):13
-->_1 bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs)):12
4:S:bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
-->_2 len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs)):5
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
5:S:len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs))
-->_2 len#(Cons(x,xs)) -> c_6(+#(S(0()),len(xs)),len#(xs)):5
12:W:bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):3
-->_1 bubble#(x,Nil()) -> c_3():2
13:W:bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):3
-->_1 bubble#(x,Nil()) -> c_3():2
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
len#(Cons(x,xs)) -> c_6(len#(xs))
** Step 1.b:6: Decompose WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Weak DPs:
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
-->_2 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):3
-->_2 bubble#(x,Nil()) -> c_3():2
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
2:S:bubble#(x,Nil()) -> c_3()
3:S:bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs)):7
-->_1 bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs)):6
4:W:bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
-->_2 len#(Cons(x,xs)) -> c_6(len#(xs)):5
5:W:len#(Cons(x,xs)) -> c_6(len#(xs))
-->_1 len#(Cons(x,xs)) -> c_6(len#(xs)):5
6:W:bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
-->_1 bubble#(x,Nil()) -> c_3():2
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):3
7:W:bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
-->_1 bubble#(x,Nil()) -> c_3():2
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
5: len#(Cons(x,xs)) -> c_6(len#(xs))
*** Step 1.b:6.a:2: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
-->_2 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):3
-->_2 bubble#(x,Nil()) -> c_3():2
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
2:S:bubble#(x,Nil()) -> c_3()
3:S:bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs)):7
-->_1 bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs)):6
4:W:bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
6:W:bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
-->_1 bubble#(x,Nil()) -> c_3():2
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):3
7:W:bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
-->_1 bubble#(x,Nil()) -> c_3():2
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
*** Step 1.b:6.a:3: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
Consider the set of all dependency pairs
1: bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
2: bubble#(x,Nil()) -> c_3()
3: bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
4: bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
5: bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
6: bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,6}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
**** Step 1.b:6.a:3.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, [1] x' + [0]
= c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
Following rules are (at-least) weakly oriented:
bubble#(x,Nil()) = [0]
>= [0]
= c_3()
bubble#(x',Cons(x,xs)) = [0]
>= [0]
= c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) = [0]
>= [0]
= c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) = [0]
>= [0]
= c_14(bubble#(x,xs))
bubblesort#(xs) = [2] xs + [4]
>= [2] xs + [4]
= c_5(bsort#(len(xs),xs))
+(x,S(0())) = [1] x + [1]
>= [1] x + [1]
= S(x)
+(S(0()),y) = [1] y + [1]
>= [1] y + [1]
= S(y)
len(Cons(x,xs)) = [1] xs + [1]
>= [1] xs + [1]
= +(S(0()),len(xs))
len(Nil()) = [2]
>= [0]
= 0()
**** Step 1.b:6.a:3.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_3()
Consider the set of all dependency pairs
1: bubble#(x,Nil()) -> c_3()
2: bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
3: bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
4: bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
5: bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
6: bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,6}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
***** Step 1.b:6.a:3.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, [0]
= c_3()
Following rules are (at-least) weakly oriented:
bsort#(S(x'),Cons(x,xs)) = [1] x' + [6]
>= [1] x' + [6]
= c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x',Cons(x,xs)) = [1]
>= [1]
= c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) = [1]
>= [1]
= c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) = [1]
>= [1]
= c_14(bubble#(x,xs))
bubblesort#(xs) = [4] xs + [7]
>= [4] xs + [7]
= c_5(bsort#(len(xs),xs))
+(x,S(0())) = [1] x + [2]
>= [1] x + [2]
= S(x)
+(S(0()),y) = [1] y + [2]
>= [1] y + [2]
= S(y)
len(Cons(x,xs)) = [4] xs + [4]
>= [4] xs + [2]
= +(S(0()),len(xs))
len(Nil()) = [0]
>= [0]
= 0()
***** Step 1.b:6.a:3.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs)):5
-->_1 bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs)):4
2:W:bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
-->_2 bubble#(x,Nil()) -> c_3():3
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):2
-->_2 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):1
3:W:bubble#(x,Nil()) -> c_3()
4:W:bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
-->_1 bubble#(x,Nil()) -> c_3():3
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):1
5:W:bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
-->_1 bubble#(x,Nil()) -> c_3():3
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):1
6:W:bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: bubble#(x,Nil()) -> c_3()
***** Step 1.b:6.a:3.b:1.b:2: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Consider the set of all dependency pairs
1: bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
2: bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
4: bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
5: bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
6: bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,4,5,6}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
****** Step 1.b:6.a:3.b:1.b:2.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, 2 + 2*x + 2*xs
= c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Following rules are (at-least) weakly oriented:
bsort#(S(x'),Cons(x,xs)) = 3 + 2*x + 2*x*x' + 2*x' + 2*x'*xs + 2*xs
>= 2 + 2*x*x' + 2*x' + 2*x'*xs + 2*xs
= c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) = 2 + 2*x + 2*xs
>= 2 + 2*xs
= c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) = 2 + 2*x + 2*xs
>= 1 + 2*xs
= c_14(bubble#(x,xs))
bubblesort#(xs) = 3 + 2*xs + 2*xs^2
>= 2 + 2*xs^2
= c_5(bsort#(len(xs),xs))
+(x,S(0())) = 1 + x
>= 1 + x
= S(x)
+(S(0()),y) = 1 + y
>= 1 + y
= S(y)
bubble(x,Nil()) = 1 + x
>= 1 + x
= Cons(x,Nil())
bubble(x',Cons(x,xs)) = 2 + x + x' + xs
>= 2 + x + x' + xs
= bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) = 2 + x + x' + xs
>= 2 + x + x' + xs
= Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) = 2 + x + x' + xs
>= 2 + x + x' + xs
= Cons(x',bubble(x,xs))
len(Cons(x,xs)) = 1 + x + xs
>= 1 + xs
= +(S(0()),len(xs))
len(Nil()) = 0
>= 0
= 0()
****** Step 1.b:6.a:3.b:1.b:2.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
-->_2 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):2
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
2:W:bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs)):4
-->_1 bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs)):3
3:W:bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):2
4:W:bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):2
5:W:bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
5: bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
1: bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
2: bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
4: bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
3: bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
****** Step 1.b:6.a:3.b:1.b:2.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Weak DPs:
bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_5(bsort#(len(xs),xs),len#(xs))
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):3
-->_2 len#(Cons(x,xs)) -> c_6(len#(xs)):2
2:S:len#(Cons(x,xs)) -> c_6(len#(xs))
-->_1 len#(Cons(x,xs)) -> c_6(len#(xs)):2
3:W:bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
-->_2 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):5
-->_2 bubble#(x,Nil()) -> c_3():4
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):3
4:W:bubble#(x,Nil()) -> c_3()
5:W:bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs)):7
-->_1 bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs)):6
6:W:bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):5
-->_1 bubble#(x,Nil()) -> c_3():4
7:W:bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
-->_1 bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):5
-->_1 bubble#(x,Nil()) -> c_3():4
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs))
5: bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
7: bubble[Ite][False][Ite]#(True(),x',Cons(x,xs)) -> c_14(bubble#(x,xs))
6: bubble[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_13(bubble#(x',xs))
4: bubble#(x,Nil()) -> c_3()
*** Step 1.b:6.b:2: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_5(bsort#(len(xs),xs),len#(xs))
-->_2 len#(Cons(x,xs)) -> c_6(len#(xs)):2
2:S:len#(Cons(x,xs)) -> c_6(len#(xs))
-->_1 len#(Cons(x,xs)) -> c_6(len#(xs)):2
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
bubblesort#(xs) -> c_5(len#(xs))
*** Step 1.b:6.b:3: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
bubblesort#(xs) -> c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Weak TRS:
+(x,S(0())) -> S(x)
+(S(0()),y) -> S(y)
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
bubble(x,Nil()) -> Cons(x,Nil())
bubble(x',Cons(x,xs)) -> bubble[Ite][False][Ite](<(x',x),x',Cons(x,xs))
bubble[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True(),x',Cons(x,xs)) -> Cons(x',bubble(x,xs))
len(Cons(x,xs)) -> +(S(0()),len(xs))
len(Nil()) -> 0()
- Signature:
{+/2, c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
*** Step 1.b:6.b:4: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
bubblesort#(xs) -> c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Signature:
{+/2, c_5(len#(xs))
2: len#(Cons(x,xs)) -> c_6(len#(xs))
The strictly oriented rules are moved into the weak component.
**** Step 1.b:6.b:4.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
bubblesort#(xs) -> c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Signature:
{+/2, [4] xs + [5]
= c_5(len#(xs))
len#(Cons(x,xs)) = [2] x + [2] xs + [4]
> [2] xs + [3]
= c_6(len#(xs))
Following rules are (at-least) weakly oriented:
**** Step 1.b:6.b:4.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
bubblesort#(xs) -> c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Signature:
{+/2, c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
- Signature:
{+/2, c_5(len#(xs))
-->_1 len#(Cons(x,xs)) -> c_6(len#(xs)):2
2:W:len#(Cons(x,xs)) -> c_6(len#(xs))
-->_1 len#(Cons(x,xs)) -> c_6(len#(xs)):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: bubblesort#(xs) -> c_5(len#(xs))
2: len#(Cons(x,xs)) -> c_6(len#(xs))
**** Step 1.b:6.b:4.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Signature:
{+/2,