*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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 DP Rules:
Weak TRS Rules:
+(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.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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()
Strict TRS Rules:
Weak DP Rules:
+#(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 Rules:
+(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()
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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()
Strict TRS Rules:
Weak DP Rules:
+#(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 Rules:
+(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))
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
+#(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 Rules:
+(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()
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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))
*** 1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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))
-->_2 len#(Cons(x,xs)) -> c_6(len#(xs)):5
-->_1 bsort#(S(x'),Cons(x,xs)) -> c_2(bsort#(x',bubble(x,xs)),bubble#(x,xs)):1
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',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):3
-->_1 bubble#(x,Nil()) -> c_3():2
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))):3
-->_1 bubble#(x,Nil()) -> c_3():2
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))
*** 1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):3
-->_1 bubble#(x,Nil()) -> c_3():2
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))):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:
bubblesort#(xs) -> c_5(bsort#(len(xs),xs))
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
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)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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, greedy = NoGreedy}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.
*** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
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)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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] x' + [6]
= 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() = [0]
,x'
,Cons(x,xs))
>= [0]
= c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True() = [0]
,x'
,Cons(x,xs))
>= [0]
= c_14(bubble#(x,xs))
bubblesort#(xs) = [4] xs + [4]
>= [4] xs + [2]
= c_5(bsort#(len(xs),xs))
+(x,S(0())) = [1] x + [7]
>= [1] x + [4]
= S(x)
+(S(0()),y) = [1] y + [7]
>= [1] y + [4]
= S(y)
len(Cons(x,xs)) = [2] xs + [9]
>= [2] xs + [8]
= +(S(0()),len(xs))
len(Nil()) = [1]
>= [0]
= 0()
*** 1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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, greedy = NoGreedy}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.
*** 1.1.1.1.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
bubble#(x,Nil()) -> c_3()
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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)) = [4] x' + [9]
>= [4] x' + [9]
= c_2(bsort#(x',bubble(x,xs))
,bubble#(x,xs))
bubble#(x',Cons(x,xs)) = [2]
>= [2]
= c_4(bubble[Ite][False][Ite]#(<(x'
,x)
,x'
,Cons(x,xs)))
bubble[Ite][False][Ite]#(False() = [2]
,x'
,Cons(x,xs))
>= [2]
= c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True() = [2]
,x'
,Cons(x,xs))
>= [2]
= c_14(bubble#(x,xs))
bubblesort#(xs) = [4] xs + [2]
>= [4] xs + [2]
= c_5(bsort#(len(xs),xs))
+(x,S(0())) = [2] x + [2]
>= [1] x + [2]
= S(x)
+(S(0()),y) = [1] y + [4]
>= [1] y + [2]
= S(y)
<(x,0()) = [0]
>= [0]
= False()
<(0(),S(y)) = [0]
>= [0]
= True()
<(S(x),S(y)) = [0]
>= [0]
= <(x,y)
len(Cons(x,xs)) = [1] xs + [4]
>= [1] xs + [4]
= +(S(0()),len(xs))
len(Nil()) = [0]
>= [0]
= 0()
*** 1.1.1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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()
*** 1.1.1.1.1.1.1.1.1.2.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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, greedy = NoGreedy}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.
*** 1.1.1.1.1.1.1.1.1.2.2.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
bubble#(x',Cons(x,xs)) -> c_4(bubble[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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 + 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)) = 6 + 4*x + 2*x*x' + 2*x' + 2*x'*xs + 4*xs
>= 6 + 3*x + 2*x*x' + 2*x' + 2*x'*xs + 4*xs
= c_2(bsort#(x',bubble(x,xs))
,bubble#(x,xs))
bubble[Ite][False][Ite]#(False() = 2 + 2*x + x' + 2*xs
,x'
,Cons(x,xs))
>= 2 + x' + 2*xs
= c_13(bubble#(x',xs))
bubble[Ite][False][Ite]#(True() = 2 + 2*x + x' + 2*xs
,x'
,Cons(x,xs))
>= 2 + x + 2*xs
= c_14(bubble#(x,xs))
bubblesort#(xs) = 2 + 2*xs + 3*xs^2
>= 2 + 2*xs + 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)
<(x,0()) = 1
>= 1
= False()
<(0(),S(y)) = 1
>= 1
= True()
<(S(x),S(y)) = 1
>= 1
= <(x,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() = 2 + x + x' + xs
,x'
,Cons(x,xs))
>= 2 + x + x' + xs
= Cons(x,bubble(x',xs))
bubble[Ite][False][Ite](True() = 2 + x + x' + xs
,x'
,Cons(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()
*** 1.1.1.1.1.1.1.1.1.2.2.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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 Rules:
+(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))
*** 1.1.1.1.1.1.1.1.1.2.2.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
+(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))
Strict TRS Rules:
Weak DP Rules:
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 Rules:
+(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()
*** 1.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
bubblesort#(xs) -> c_5(bsort#(len(xs),xs),len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
+(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))
*** 1.1.1.1.1.1.2.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
bubblesort#(xs) -> c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
+(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))
*** 1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
bubblesort#(xs) -> c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
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.
*** 1.1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
bubblesort#(xs) -> c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
Signature:
{+/2, [6] xs + [14]
= c_5(len#(xs))
len#(Cons(x,xs)) = [3] x + [3] xs + [31]
> [3] xs + [7]
= c_6(len#(xs))
Following rules are (at-least) weakly oriented:
*** 1.1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
bubblesort#(xs) -> c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
Weak TRS Rules:
Signature:
{+/2, c_5(len#(xs))
len#(Cons(x,xs)) -> c_6(len#(xs))
Weak TRS Rules:
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))
*** 1.1.1.1.1.1.2.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
Signature:
{+/2,