YES(O(1),O(n^2)) 365.16/148.07 YES(O(1),O(n^2)) 365.16/148.07 365.16/148.07 We are left with following problem, upon which TcT provides the 365.16/148.07 certificate YES(O(1),O(n^2)). 365.16/148.07 365.16/148.07 Strict Trs: 365.16/148.07 { bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.07 , bubble(x', Cons(x, xs)) -> 365.16/148.07 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.07 , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs)) 365.16/148.07 , bsort(0(), xs) -> xs 365.16/148.07 , bubblesort(xs) -> bsort(len(xs), xs) 365.16/148.07 , len(Nil()) -> 0() 365.16/148.07 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.07 Weak Trs: 365.16/148.07 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.07 Cons(x', bubble(x, xs)) 365.16/148.07 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.07 Cons(x, bubble(x', xs)) 365.16/148.07 , +(x, S(0())) -> S(x) 365.16/148.07 , +(S(0()), y) -> S(y) 365.16/148.07 , <(x, 0()) -> False() 365.16/148.07 , <(S(x), S(y)) -> <(x, y) 365.16/148.07 , <(0(), S(y)) -> True() } 365.16/148.07 Obligation: 365.16/148.07 innermost runtime complexity 365.16/148.07 Answer: 365.16/148.07 YES(O(1),O(n^2)) 365.16/148.07 365.16/148.07 We add the following dependency tuples: 365.16/148.07 365.16/148.07 Strict DPs: 365.16/148.07 { bubble^#(x, Nil()) -> c_1() 365.16/148.07 , bubble^#(x', Cons(x, xs)) -> 365.16/148.07 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)), 365.16/148.07 <^#(x', x)) 365.16/148.07 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.07 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.07 , bsort^#(0(), xs) -> c_4() 365.16/148.07 , bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.07 , len^#(Nil()) -> c_6() 365.16/148.07 , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) } 365.16/148.07 Weak DPs: 365.16/148.07 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.07 c_8(bubble^#(x, xs)) 365.16/148.07 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.07 c_9(bubble^#(x', xs)) 365.16/148.07 , <^#(x, 0()) -> c_12() 365.16/148.07 , <^#(S(x), S(y)) -> c_13(<^#(x, y)) 365.16/148.07 , <^#(0(), S(y)) -> c_14() 365.16/148.07 , +^#(x, S(0())) -> c_10() 365.16/148.07 , +^#(S(0()), y) -> c_11() } 365.16/148.07 365.16/148.07 and mark the set of starting terms. 365.16/148.07 365.16/148.07 We are left with following problem, upon which TcT provides the 365.16/148.07 certificate YES(O(1),O(n^2)). 365.16/148.07 365.16/148.07 Strict DPs: 365.16/148.07 { bubble^#(x, Nil()) -> c_1() 365.16/148.07 , bubble^#(x', Cons(x, xs)) -> 365.16/148.07 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)), 365.16/148.07 <^#(x', x)) 365.16/148.07 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.07 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.07 , bsort^#(0(), xs) -> c_4() 365.16/148.07 , bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.07 , len^#(Nil()) -> c_6() 365.16/148.07 , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) } 365.16/148.07 Weak DPs: 365.16/148.07 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.07 c_8(bubble^#(x, xs)) 365.16/148.07 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.07 c_9(bubble^#(x', xs)) 365.16/148.07 , <^#(x, 0()) -> c_12() 365.16/148.07 , <^#(S(x), S(y)) -> c_13(<^#(x, y)) 365.16/148.07 , <^#(0(), S(y)) -> c_14() 365.16/148.07 , +^#(x, S(0())) -> c_10() 365.16/148.07 , +^#(S(0()), y) -> c_11() } 365.16/148.07 Weak Trs: 365.16/148.07 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.07 Cons(x', bubble(x, xs)) 365.16/148.07 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.07 Cons(x, bubble(x', xs)) 365.16/148.07 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.07 , bubble(x', Cons(x, xs)) -> 365.16/148.07 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.07 , +(x, S(0())) -> S(x) 365.16/148.07 , +(S(0()), y) -> S(y) 365.16/148.07 , <(x, 0()) -> False() 365.16/148.07 , <(S(x), S(y)) -> <(x, y) 365.16/148.07 , <(0(), S(y)) -> True() 365.16/148.07 , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs)) 365.16/148.07 , bsort(0(), xs) -> xs 365.16/148.07 , bubblesort(xs) -> bsort(len(xs), xs) 365.16/148.07 , len(Nil()) -> 0() 365.16/148.07 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.07 Obligation: 365.16/148.07 innermost runtime complexity 365.16/148.07 Answer: 365.16/148.07 YES(O(1),O(n^2)) 365.16/148.07 365.16/148.07 We estimate the number of application of {4,6} by applications of 365.16/148.07 Pre({4,6}) = {3,5,7}. Here rules are labeled as follows: 365.16/148.07 365.16/148.07 DPs: 365.16/148.07 { 1: bubble^#(x, Nil()) -> c_1() 365.16/148.07 , 2: bubble^#(x', Cons(x, xs)) -> 365.16/148.07 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)), 365.16/148.07 <^#(x', x)) 365.16/148.07 , 3: bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.07 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.07 , 4: bsort^#(0(), xs) -> c_4() 365.16/148.07 , 5: bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.07 , 6: len^#(Nil()) -> c_6() 365.16/148.07 , 7: len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) 365.16/148.07 , 8: bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.07 c_8(bubble^#(x, xs)) 365.16/148.07 , 9: bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.07 c_9(bubble^#(x', xs)) 365.16/148.07 , 10: <^#(x, 0()) -> c_12() 365.16/148.07 , 11: <^#(S(x), S(y)) -> c_13(<^#(x, y)) 365.16/148.07 , 12: <^#(0(), S(y)) -> c_14() 365.16/148.07 , 13: +^#(x, S(0())) -> c_10() 365.16/148.07 , 14: +^#(S(0()), y) -> c_11() } 365.16/148.07 365.16/148.07 We are left with following problem, upon which TcT provides the 365.16/148.07 certificate YES(O(1),O(n^2)). 365.16/148.07 365.16/148.07 Strict DPs: 365.16/148.07 { bubble^#(x, Nil()) -> c_1() 365.16/148.07 , bubble^#(x', Cons(x, xs)) -> 365.16/148.07 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)), 365.16/148.07 <^#(x', x)) 365.16/148.07 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.07 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.07 , bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.07 , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) } 365.16/148.07 Weak DPs: 365.16/148.07 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.07 c_8(bubble^#(x, xs)) 365.16/148.07 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.07 c_9(bubble^#(x', xs)) 365.16/148.07 , <^#(x, 0()) -> c_12() 365.16/148.07 , <^#(S(x), S(y)) -> c_13(<^#(x, y)) 365.16/148.07 , <^#(0(), S(y)) -> c_14() 365.16/148.07 , bsort^#(0(), xs) -> c_4() 365.16/148.07 , len^#(Nil()) -> c_6() 365.16/148.07 , +^#(x, S(0())) -> c_10() 365.16/148.07 , +^#(S(0()), y) -> c_11() } 365.16/148.07 Weak Trs: 365.16/148.07 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.07 Cons(x', bubble(x, xs)) 365.16/148.07 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.07 Cons(x, bubble(x', xs)) 365.16/148.07 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.07 , bubble(x', Cons(x, xs)) -> 365.16/148.07 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.07 , +(x, S(0())) -> S(x) 365.16/148.07 , +(S(0()), y) -> S(y) 365.16/148.07 , <(x, 0()) -> False() 365.16/148.07 , <(S(x), S(y)) -> <(x, y) 365.16/148.07 , <(0(), S(y)) -> True() 365.16/148.07 , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs)) 365.16/148.07 , bsort(0(), xs) -> xs 365.16/148.07 , bubblesort(xs) -> bsort(len(xs), xs) 365.16/148.07 , len(Nil()) -> 0() 365.16/148.07 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.07 Obligation: 365.16/148.07 innermost runtime complexity 365.16/148.07 Answer: 365.16/148.07 YES(O(1),O(n^2)) 365.16/148.07 365.16/148.07 The following weak DPs constitute a sub-graph of the DG that is 365.16/148.07 closed under successors. The DPs are removed. 365.16/148.07 365.16/148.07 { <^#(x, 0()) -> c_12() 365.16/148.07 , <^#(S(x), S(y)) -> c_13(<^#(x, y)) 365.16/148.07 , <^#(0(), S(y)) -> c_14() 365.16/148.07 , bsort^#(0(), xs) -> c_4() 365.16/148.07 , len^#(Nil()) -> c_6() 365.16/148.07 , +^#(x, S(0())) -> c_10() 365.16/148.07 , +^#(S(0()), y) -> c_11() } 365.16/148.07 365.16/148.07 We are left with following problem, upon which TcT provides the 365.16/148.07 certificate YES(O(1),O(n^2)). 365.16/148.07 365.16/148.07 Strict DPs: 365.16/148.07 { bubble^#(x, Nil()) -> c_1() 365.16/148.07 , bubble^#(x', Cons(x, xs)) -> 365.16/148.07 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)), 365.16/148.07 <^#(x', x)) 365.16/148.07 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.07 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.07 , bubblesort^#(xs) -> c_5(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.07 , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) } 365.16/148.07 Weak DPs: 365.16/148.07 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.07 c_8(bubble^#(x, xs)) 365.16/148.07 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.07 c_9(bubble^#(x', xs)) } 365.16/148.07 Weak Trs: 365.16/148.07 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.07 Cons(x', bubble(x, xs)) 365.16/148.07 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.07 Cons(x, bubble(x', xs)) 365.16/148.07 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.07 , bubble(x', Cons(x, xs)) -> 365.16/148.07 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.07 , +(x, S(0())) -> S(x) 365.16/148.07 , +(S(0()), y) -> S(y) 365.16/148.07 , <(x, 0()) -> False() 365.16/148.07 , <(S(x), S(y)) -> <(x, y) 365.16/148.07 , <(0(), S(y)) -> True() 365.16/148.07 , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs)) 365.16/148.07 , bsort(0(), xs) -> xs 365.16/148.07 , bubblesort(xs) -> bsort(len(xs), xs) 365.16/148.07 , len(Nil()) -> 0() 365.16/148.07 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.07 Obligation: 365.16/148.07 innermost runtime complexity 365.16/148.07 Answer: 365.16/148.07 YES(O(1),O(n^2)) 365.16/148.07 365.16/148.07 Due to missing edges in the dependency-graph, the right-hand sides 365.16/148.07 of following rules could be simplified: 365.16/148.07 365.16/148.07 { bubble^#(x', Cons(x, xs)) -> 365.16/148.07 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)), 365.16/148.07 <^#(x', x)) 365.16/148.07 , len^#(Cons(x, xs)) -> c_7(+^#(S(0()), len(xs)), len^#(xs)) } 365.16/148.07 365.16/148.07 We are left with following problem, upon which TcT provides the 365.16/148.07 certificate YES(O(1),O(n^2)). 365.16/148.07 365.16/148.07 Strict DPs: 365.16/148.07 { bubble^#(x, Nil()) -> c_1() 365.16/148.07 , bubble^#(x', Cons(x, xs)) -> 365.16/148.07 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.07 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.08 , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , bsort(S(x'), Cons(x, xs)) -> bsort(x', bubble(x, xs)) 365.16/148.08 , bsort(0(), xs) -> xs 365.16/148.08 , bubblesort(xs) -> bsort(len(xs), xs) 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^2)) 365.16/148.08 365.16/148.08 We replace rewrite rules by usable rules: 365.16/148.08 365.16/148.08 Weak Usable Rules: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^2)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.08 , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^2)) 365.16/148.08 365.16/148.08 We analyse the complexity of following sub-problems (R) and (S). 365.16/148.08 Problem (S) is obtained from the input problem by shifting strict 365.16/148.08 rules from (R) into the weak component: 365.16/148.08 365.16/148.08 Problem (R): 365.16/148.08 ------------ 365.16/148.08 Strict DPs: 365.16/148.08 { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 StartTerms: basic terms 365.16/148.08 Strategy: innermost 365.16/148.08 365.16/148.08 Problem (S): 365.16/148.08 ------------ 365.16/148.08 Strict DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) 365.16/148.08 , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 StartTerms: basic terms 365.16/148.08 Strategy: innermost 365.16/148.08 365.16/148.08 Overall, the transformation results in the following sub-problem(s): 365.16/148.08 365.16/148.08 Generated new problems: 365.16/148.08 ----------------------- 365.16/148.08 R) Strict DPs: 365.16/148.08 { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 StartTerms: basic terms 365.16/148.08 Strategy: innermost 365.16/148.08 365.16/148.08 This problem was proven YES(O(1),O(n^1)). 365.16/148.08 365.16/148.08 S) Strict DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) 365.16/148.08 , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 StartTerms: basic terms 365.16/148.08 Strategy: innermost 365.16/148.08 365.16/148.08 This problem was proven YES(O(1),O(n^2)). 365.16/148.08 365.16/148.08 365.16/148.08 Proofs for generated problems: 365.16/148.08 ------------------------------ 365.16/148.08 R) We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^1)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^1)) 365.16/148.08 365.16/148.08 The following weak DPs constitute a sub-graph of the DG that is 365.16/148.08 closed under successors. The DPs are removed. 365.16/148.08 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^1)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^1)) 365.16/148.08 365.16/148.08 Due to missing edges in the dependency-graph, the right-hand sides 365.16/148.08 of following rules could be simplified: 365.16/148.08 365.16/148.08 { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) } 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^1)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubblesort^#(xs) -> c_1(len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_2(len^#(xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^1)) 365.16/148.08 365.16/148.08 No rule is usable, rules are removed from the input problem. 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^1)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubblesort^#(xs) -> c_1(len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_2(len^#(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^1)) 365.16/148.08 365.16/148.08 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 365.16/148.08 to orient following rules strictly. 365.16/148.08 365.16/148.08 DPs: 365.16/148.08 { 1: bubblesort^#(xs) -> c_1(len^#(xs)) 365.16/148.08 , 2: len^#(Cons(x, xs)) -> c_2(len^#(xs)) } 365.16/148.08 365.16/148.08 Sub-proof: 365.16/148.08 ---------- 365.16/148.08 The input was oriented with the instance of 'Small Polynomial Path 365.16/148.08 Order (PS,1-bounded)' as induced by the safe mapping 365.16/148.08 365.16/148.08 safe(Cons) = {1, 2}, safe(bubblesort^#) = {}, safe(len^#) = {}, 365.16/148.08 safe(c_1) = {}, safe(c_2) = {} 365.16/148.08 365.16/148.08 and precedence 365.16/148.08 365.16/148.08 bubblesort^# > len^# . 365.16/148.08 365.16/148.08 Following symbols are considered recursive: 365.16/148.08 365.16/148.08 {len^#} 365.16/148.08 365.16/148.08 The recursion depth is 1. 365.16/148.08 365.16/148.08 Further, following argument filtering is employed: 365.16/148.08 365.16/148.08 pi(Cons) = [1, 2], pi(bubblesort^#) = [1], pi(len^#) = [1], 365.16/148.08 pi(c_1) = [1], pi(c_2) = [1] 365.16/148.08 365.16/148.08 Usable defined function symbols are a subset of: 365.16/148.08 365.16/148.08 {bubblesort^#, len^#} 365.16/148.08 365.16/148.08 For your convenience, here are the satisfied ordering constraints: 365.16/148.08 365.16/148.08 pi(bubblesort^#(xs)) = bubblesort^#(xs;) 365.16/148.08 > c_1(len^#(xs;);) 365.16/148.08 = pi(c_1(len^#(xs))) 365.16/148.08 365.16/148.08 pi(len^#(Cons(x, xs))) = len^#(Cons(; x, xs);) 365.16/148.08 > c_2(len^#(xs;);) 365.16/148.08 = pi(c_2(len^#(xs))) 365.16/148.08 365.16/148.08 365.16/148.08 The strictly oriented rules are moved into the weak component. 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(1)). 365.16/148.08 365.16/148.08 Weak DPs: 365.16/148.08 { bubblesort^#(xs) -> c_1(len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_2(len^#(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(1)) 365.16/148.08 365.16/148.08 The following weak DPs constitute a sub-graph of the DG that is 365.16/148.08 closed under successors. The DPs are removed. 365.16/148.08 365.16/148.08 { bubblesort^#(xs) -> c_1(len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_2(len^#(xs)) } 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(1)). 365.16/148.08 365.16/148.08 Rules: Empty 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(1)) 365.16/148.08 365.16/148.08 Empty rules are trivially bounded 365.16/148.08 365.16/148.08 S) We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^2)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) 365.16/148.08 , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) 365.16/148.08 , len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^2)) 365.16/148.08 365.16/148.08 The following weak DPs constitute a sub-graph of the DG that is 365.16/148.08 closed under successors. The DPs are removed. 365.16/148.08 365.16/148.08 { len^#(Cons(x, xs)) -> c_5(len^#(xs)) } 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^2)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_6(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_7(bubble^#(x', xs)) 365.16/148.08 , bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^2)) 365.16/148.08 365.16/148.08 Due to missing edges in the dependency-graph, the right-hand sides 365.16/148.08 of following rules could be simplified: 365.16/148.08 365.16/148.08 { bubblesort^#(xs) -> c_4(bsort^#(len(xs), xs), len^#(xs)) } 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^2)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_4(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_5(bubble^#(x', xs)) 365.16/148.08 , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^2)) 365.16/148.08 365.16/148.08 We use the processor 'matrix interpretation of dimension 1' to 365.16/148.08 orient following rules strictly. 365.16/148.08 365.16/148.08 DPs: 365.16/148.08 { 1: bubble^#(x, Nil()) -> c_1() 365.16/148.08 , 6: bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) } 365.16/148.08 Trs: { len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 365.16/148.08 Sub-proof: 365.16/148.08 ---------- 365.16/148.08 The following argument positions are usable: 365.16/148.08 Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1}, 365.16/148.08 Uargs(c_5) = {1}, Uargs(c_6) = {1} 365.16/148.08 365.16/148.08 TcT has computed the following constructor-based matrix 365.16/148.08 interpretation satisfying not(EDA). 365.16/148.08 365.16/148.08 [bubble[Ite][False][Ite]](x1, x2, x3) = [1] x2 + [0] 365.16/148.08 365.16/148.08 [bubble](x1, x2) = [0] 365.16/148.08 365.16/148.08 [True] = [1] 365.16/148.08 365.16/148.08 [Nil] = [0] 365.16/148.08 365.16/148.08 [+](x1, x2) = [1] x1 + [1] x2 + [0] 365.16/148.08 365.16/148.08 [S](x1) = [1] x1 + [1] 365.16/148.08 365.16/148.08 [<](x1, x2) = [1] 365.16/148.08 365.16/148.08 [Cons](x1, x2) = [1] x2 + [4] 365.16/148.08 365.16/148.08 [0] = [0] 365.16/148.08 365.16/148.08 [len](x1) = [1] x1 + [0] 365.16/148.08 365.16/148.08 [False] = [1] 365.16/148.08 365.16/148.08 [bubble^#](x1, x2) = [2] 365.16/148.08 365.16/148.08 [bubble[Ite][False][Ite]^#](x1, x2, x3) = [2] x1 + [0] 365.16/148.08 365.16/148.08 [bsort^#](x1, x2) = [2] x1 + [0] 365.16/148.08 365.16/148.08 [bubblesort^#](x1) = [7] x1 + [7] 365.16/148.08 365.16/148.08 [c_1] = [0] 365.16/148.08 365.16/148.08 [c_2](x1) = [1] x1 + [0] 365.16/148.08 365.16/148.08 [c_3](x1, x2) = [1] x1 + [1] x2 + [0] 365.16/148.08 365.16/148.08 [c_4](x1) = [1] x1 + [0] 365.16/148.08 365.16/148.08 [c_5](x1) = [1] x1 + [0] 365.16/148.08 365.16/148.08 [c_6](x1) = [2] x1 + [3] 365.16/148.08 365.16/148.08 The order satisfies the following ordering constraints: 365.16/148.08 365.16/148.08 [bubble[Ite][False][Ite](True(), x', Cons(x, xs))] = [1] x' + [0] 365.16/148.08 ? [4] 365.16/148.08 = [Cons(x', bubble(x, xs))] 365.16/148.08 365.16/148.08 [bubble[Ite][False][Ite](False(), x', Cons(x, xs))] = [1] x' + [0] 365.16/148.08 ? [4] 365.16/148.08 = [Cons(x, bubble(x', xs))] 365.16/148.08 365.16/148.08 [bubble(x, Nil())] = [0] 365.16/148.08 ? [4] 365.16/148.08 = [Cons(x, Nil())] 365.16/148.08 365.16/148.08 [bubble(x', Cons(x, xs))] = [0] 365.16/148.08 ? [1] x' + [0] 365.16/148.08 = [bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))] 365.16/148.08 365.16/148.08 [+(x, S(0()))] = [1] x + [1] 365.16/148.08 >= [1] x + [1] 365.16/148.08 = [S(x)] 365.16/148.08 365.16/148.08 [+(S(0()), y)] = [1] y + [1] 365.16/148.08 >= [1] y + [1] 365.16/148.08 = [S(y)] 365.16/148.08 365.16/148.08 [<(x, 0())] = [1] 365.16/148.08 >= [1] 365.16/148.08 = [False()] 365.16/148.08 365.16/148.08 [<(S(x), S(y))] = [1] 365.16/148.08 >= [1] 365.16/148.08 = [<(x, y)] 365.16/148.08 365.16/148.08 [<(0(), S(y))] = [1] 365.16/148.08 >= [1] 365.16/148.08 = [True()] 365.16/148.08 365.16/148.08 [len(Nil())] = [0] 365.16/148.08 >= [0] 365.16/148.08 = [0()] 365.16/148.08 365.16/148.08 [len(Cons(x, xs))] = [1] xs + [4] 365.16/148.08 > [1] xs + [1] 365.16/148.08 = [+(S(0()), len(xs))] 365.16/148.08 365.16/148.08 [bubble^#(x, Nil())] = [2] 365.16/148.08 > [0] 365.16/148.08 = [c_1()] 365.16/148.08 365.16/148.08 [bubble^#(x', Cons(x, xs))] = [2] 365.16/148.08 >= [2] 365.16/148.08 = [c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))] 365.16/148.08 365.16/148.08 [bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs))] = [2] 365.16/148.08 >= [2] 365.16/148.08 = [c_4(bubble^#(x, xs))] 365.16/148.08 365.16/148.08 [bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs))] = [2] 365.16/148.08 >= [2] 365.16/148.08 = [c_5(bubble^#(x', xs))] 365.16/148.08 365.16/148.08 [bsort^#(S(x'), Cons(x, xs))] = [2] x' + [2] 365.16/148.08 >= [2] x' + [2] 365.16/148.08 = [c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))] 365.16/148.08 365.16/148.08 [bubblesort^#(xs)] = [7] xs + [7] 365.16/148.08 > [4] xs + [3] 365.16/148.08 = [c_6(bsort^#(len(xs), xs))] 365.16/148.08 365.16/148.08 365.16/148.08 The strictly oriented rules are moved into the weak component. 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^2)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.08 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.08 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.08 Weak DPs: 365.16/148.08 { bubble^#(x, Nil()) -> c_1() 365.16/148.08 , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.08 c_4(bubble^#(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.08 c_5(bubble^#(x', xs)) 365.16/148.08 , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) } 365.16/148.08 Weak Trs: 365.16/148.08 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x', bubble(x, xs)) 365.16/148.08 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.08 Cons(x, bubble(x', xs)) 365.16/148.08 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.08 , bubble(x', Cons(x, xs)) -> 365.16/148.08 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.08 , +(x, S(0())) -> S(x) 365.16/148.08 , +(S(0()), y) -> S(y) 365.16/148.08 , <(x, 0()) -> False() 365.16/148.08 , <(S(x), S(y)) -> <(x, y) 365.16/148.08 , <(0(), S(y)) -> True() 365.16/148.08 , len(Nil()) -> 0() 365.16/148.08 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.08 Obligation: 365.16/148.08 innermost runtime complexity 365.16/148.08 Answer: 365.16/148.08 YES(O(1),O(n^2)) 365.16/148.08 365.16/148.08 The following weak DPs constitute a sub-graph of the DG that is 365.16/148.08 closed under successors. The DPs are removed. 365.16/148.08 365.16/148.08 { bubble^#(x, Nil()) -> c_1() } 365.16/148.08 365.16/148.08 We are left with following problem, upon which TcT provides the 365.16/148.08 certificate YES(O(1),O(n^2)). 365.16/148.08 365.16/148.08 Strict DPs: 365.16/148.08 { bubble^#(x', Cons(x, xs)) -> 365.16/148.08 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.09 , bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.09 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.09 Weak DPs: 365.16/148.09 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.09 c_4(bubble^#(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.09 c_5(bubble^#(x', xs)) 365.16/148.09 , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) } 365.16/148.09 Weak Trs: 365.16/148.09 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x', bubble(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x, bubble(x', xs)) 365.16/148.09 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.09 , bubble(x', Cons(x, xs)) -> 365.16/148.09 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.09 , +(x, S(0())) -> S(x) 365.16/148.09 , +(S(0()), y) -> S(y) 365.16/148.09 , <(x, 0()) -> False() 365.16/148.09 , <(S(x), S(y)) -> <(x, y) 365.16/148.09 , <(0(), S(y)) -> True() 365.16/148.09 , len(Nil()) -> 0() 365.16/148.09 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.09 Obligation: 365.16/148.09 innermost runtime complexity 365.16/148.09 Answer: 365.16/148.09 YES(O(1),O(n^2)) 365.16/148.09 365.16/148.09 We decompose the input problem according to the dependency graph 365.16/148.09 into the upper component 365.16/148.09 365.16/148.09 { bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.09 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.09 , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) } 365.16/148.09 365.16/148.09 and lower component 365.16/148.09 365.16/148.09 { bubble^#(x', Cons(x, xs)) -> 365.16/148.09 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.09 , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.09 c_4(bubble^#(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.09 c_5(bubble^#(x', xs)) } 365.16/148.09 365.16/148.09 Further, following extension rules are added to the lower 365.16/148.09 component. 365.16/148.09 365.16/148.09 { bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs) 365.16/148.09 , bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs)) 365.16/148.09 , bubblesort^#(xs) -> bsort^#(len(xs), xs) } 365.16/148.09 365.16/148.09 TcT solves the upper component with certificate YES(O(1),O(n^1)). 365.16/148.09 365.16/148.09 Sub-proof: 365.16/148.09 ---------- 365.16/148.09 We are left with following problem, upon which TcT provides the 365.16/148.09 certificate YES(O(1),O(n^1)). 365.16/148.09 365.16/148.09 Strict DPs: 365.16/148.09 { bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.09 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) } 365.16/148.09 Weak DPs: { bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) } 365.16/148.09 Weak Trs: 365.16/148.09 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x', bubble(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x, bubble(x', xs)) 365.16/148.09 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.09 , bubble(x', Cons(x, xs)) -> 365.16/148.09 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.09 , +(x, S(0())) -> S(x) 365.16/148.09 , +(S(0()), y) -> S(y) 365.16/148.09 , <(x, 0()) -> False() 365.16/148.09 , <(S(x), S(y)) -> <(x, y) 365.16/148.09 , <(0(), S(y)) -> True() 365.16/148.09 , len(Nil()) -> 0() 365.16/148.09 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.09 Obligation: 365.16/148.09 innermost runtime complexity 365.16/148.09 Answer: 365.16/148.09 YES(O(1),O(n^1)) 365.16/148.09 365.16/148.09 We use the processor 'matrix interpretation of dimension 1' to 365.16/148.09 orient following rules strictly. 365.16/148.09 365.16/148.09 DPs: 365.16/148.09 { 1: bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.09 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.09 , 2: bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) } 365.16/148.09 Trs: 365.16/148.09 { +(S(0()), y) -> S(y) 365.16/148.09 , len(Nil()) -> 0() } 365.16/148.09 365.16/148.09 Sub-proof: 365.16/148.09 ---------- 365.16/148.09 The following argument positions are usable: 365.16/148.09 Uargs(c_3) = {1}, Uargs(c_6) = {1} 365.16/148.09 365.16/148.09 TcT has computed the following constructor-based matrix 365.16/148.09 interpretation satisfying not(EDA). 365.16/148.09 365.16/148.09 [bubble[Ite][False][Ite]](x1, x2, x3) = [1] x2 + [0] 365.16/148.09 365.16/148.09 [bubble](x1, x2) = [0] 365.16/148.09 365.16/148.09 [True] = [0] 365.16/148.09 365.16/148.09 [Nil] = [4] 365.16/148.09 365.16/148.09 [+](x1, x2) = [4] x1 + [1] x2 + [0] 365.16/148.09 365.16/148.09 [S](x1) = [1] x1 + [2] 365.16/148.09 365.16/148.09 [<](x1, x2) = [0] 365.16/148.09 365.16/148.09 [Cons](x1, x2) = [1] x2 + [4] 365.16/148.09 365.16/148.09 [0] = [0] 365.16/148.09 365.16/148.09 [len](x1) = [2] x1 + [0] 365.16/148.09 365.16/148.09 [False] = [0] 365.16/148.09 365.16/148.09 [bubble^#](x1, x2) = [7] x1 + [7] x2 + [7] 365.16/148.09 365.16/148.09 [bsort^#](x1, x2) = [1] x1 + [0] 365.16/148.09 365.16/148.09 [bubblesort^#](x1) = [7] x1 + [7] 365.16/148.09 365.16/148.09 [c_3](x1, x2) = [1] x1 + [1] 365.16/148.09 365.16/148.09 [c_6](x1) = [1] x1 + [3] 365.16/148.09 365.16/148.09 The order satisfies the following ordering constraints: 365.16/148.09 365.16/148.09 [bubble[Ite][False][Ite](True(), x', Cons(x, xs))] = [1] x' + [0] 365.16/148.09 ? [4] 365.16/148.09 = [Cons(x', bubble(x, xs))] 365.16/148.09 365.16/148.09 [bubble[Ite][False][Ite](False(), x', Cons(x, xs))] = [1] x' + [0] 365.16/148.09 ? [4] 365.16/148.09 = [Cons(x, bubble(x', xs))] 365.16/148.09 365.16/148.09 [bubble(x, Nil())] = [0] 365.16/148.09 ? [8] 365.16/148.09 = [Cons(x, Nil())] 365.16/148.09 365.16/148.09 [bubble(x', Cons(x, xs))] = [0] 365.16/148.09 ? [1] x' + [0] 365.16/148.09 = [bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))] 365.16/148.09 365.16/148.09 [+(x, S(0()))] = [4] x + [2] 365.16/148.09 >= [1] x + [2] 365.16/148.09 = [S(x)] 365.16/148.09 365.16/148.09 [+(S(0()), y)] = [1] y + [8] 365.16/148.09 > [1] y + [2] 365.16/148.09 = [S(y)] 365.16/148.09 365.16/148.09 [<(x, 0())] = [0] 365.16/148.09 >= [0] 365.16/148.09 = [False()] 365.16/148.09 365.16/148.09 [<(S(x), S(y))] = [0] 365.16/148.09 >= [0] 365.16/148.09 = [<(x, y)] 365.16/148.09 365.16/148.09 [<(0(), S(y))] = [0] 365.16/148.09 >= [0] 365.16/148.09 = [True()] 365.16/148.09 365.16/148.09 [len(Nil())] = [8] 365.16/148.09 > [0] 365.16/148.09 = [0()] 365.16/148.09 365.16/148.09 [len(Cons(x, xs))] = [2] xs + [8] 365.16/148.09 >= [2] xs + [8] 365.16/148.09 = [+(S(0()), len(xs))] 365.16/148.09 365.16/148.09 [bsort^#(S(x'), Cons(x, xs))] = [1] x' + [2] 365.16/148.09 > [1] x' + [1] 365.16/148.09 = [c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs))] 365.16/148.09 365.16/148.09 [bubblesort^#(xs)] = [7] xs + [7] 365.16/148.09 > [2] xs + [3] 365.16/148.09 = [c_6(bsort^#(len(xs), xs))] 365.16/148.09 365.16/148.09 365.16/148.09 The strictly oriented rules are moved into the weak component. 365.16/148.09 365.16/148.09 We are left with following problem, upon which TcT provides the 365.16/148.09 certificate YES(O(1),O(1)). 365.16/148.09 365.16/148.09 Weak DPs: 365.16/148.09 { bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.09 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.09 , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) } 365.16/148.09 Weak Trs: 365.16/148.09 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x', bubble(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x, bubble(x', xs)) 365.16/148.09 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.09 , bubble(x', Cons(x, xs)) -> 365.16/148.09 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.09 , +(x, S(0())) -> S(x) 365.16/148.09 , +(S(0()), y) -> S(y) 365.16/148.09 , <(x, 0()) -> False() 365.16/148.09 , <(S(x), S(y)) -> <(x, y) 365.16/148.09 , <(0(), S(y)) -> True() 365.16/148.09 , len(Nil()) -> 0() 365.16/148.09 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.09 Obligation: 365.16/148.09 innermost runtime complexity 365.16/148.09 Answer: 365.16/148.09 YES(O(1),O(1)) 365.16/148.09 365.16/148.09 The following weak DPs constitute a sub-graph of the DG that is 365.16/148.09 closed under successors. The DPs are removed. 365.16/148.09 365.16/148.09 { bsort^#(S(x'), Cons(x, xs)) -> 365.16/148.09 c_3(bsort^#(x', bubble(x, xs)), bubble^#(x, xs)) 365.16/148.09 , bubblesort^#(xs) -> c_6(bsort^#(len(xs), xs)) } 365.16/148.09 365.16/148.09 We are left with following problem, upon which TcT provides the 365.16/148.09 certificate YES(O(1),O(1)). 365.16/148.09 365.16/148.09 Weak Trs: 365.16/148.09 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x', bubble(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x, bubble(x', xs)) 365.16/148.09 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.09 , bubble(x', Cons(x, xs)) -> 365.16/148.09 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.09 , +(x, S(0())) -> S(x) 365.16/148.09 , +(S(0()), y) -> S(y) 365.16/148.09 , <(x, 0()) -> False() 365.16/148.09 , <(S(x), S(y)) -> <(x, y) 365.16/148.09 , <(0(), S(y)) -> True() 365.16/148.09 , len(Nil()) -> 0() 365.16/148.09 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.09 Obligation: 365.16/148.09 innermost runtime complexity 365.16/148.09 Answer: 365.16/148.09 YES(O(1),O(1)) 365.16/148.09 365.16/148.09 No rule is usable, rules are removed from the input problem. 365.16/148.09 365.16/148.09 We are left with following problem, upon which TcT provides the 365.16/148.09 certificate YES(O(1),O(1)). 365.16/148.09 365.16/148.09 Rules: Empty 365.16/148.09 Obligation: 365.16/148.09 innermost runtime complexity 365.16/148.09 Answer: 365.16/148.09 YES(O(1),O(1)) 365.16/148.09 365.16/148.09 Empty rules are trivially bounded 365.16/148.09 365.16/148.09 We return to the main proof. 365.16/148.09 365.16/148.09 We are left with following problem, upon which TcT provides the 365.16/148.09 certificate YES(O(1),O(n^1)). 365.16/148.09 365.16/148.09 Strict DPs: 365.16/148.09 { bubble^#(x', Cons(x, xs)) -> 365.16/148.09 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) } 365.16/148.09 Weak DPs: 365.16/148.09 { bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.09 c_4(bubble^#(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.09 c_5(bubble^#(x', xs)) 365.16/148.09 , bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs) 365.16/148.09 , bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs)) 365.16/148.09 , bubblesort^#(xs) -> bsort^#(len(xs), xs) } 365.16/148.09 Weak Trs: 365.16/148.09 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x', bubble(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x, bubble(x', xs)) 365.16/148.09 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.09 , bubble(x', Cons(x, xs)) -> 365.16/148.09 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.09 , +(x, S(0())) -> S(x) 365.16/148.09 , +(S(0()), y) -> S(y) 365.16/148.09 , <(x, 0()) -> False() 365.16/148.09 , <(S(x), S(y)) -> <(x, y) 365.16/148.09 , <(0(), S(y)) -> True() 365.16/148.09 , len(Nil()) -> 0() 365.16/148.09 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.09 Obligation: 365.16/148.09 innermost runtime complexity 365.16/148.09 Answer: 365.16/148.09 YES(O(1),O(n^1)) 365.16/148.09 365.16/148.09 We use the processor 'matrix interpretation of dimension 1' to 365.16/148.09 orient following rules strictly. 365.16/148.09 365.16/148.09 DPs: 365.16/148.09 { 1: bubble^#(x', Cons(x, xs)) -> 365.16/148.09 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.09 , 4: bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs) 365.16/148.09 , 5: bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs)) 365.16/148.09 , 6: bubblesort^#(xs) -> bsort^#(len(xs), xs) } 365.16/148.09 Trs: 365.16/148.09 { bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.09 , +(S(0()), y) -> S(y) 365.16/148.09 , len(Nil()) -> 0() } 365.16/148.09 365.16/148.09 Sub-proof: 365.16/148.09 ---------- 365.16/148.09 The following argument positions are usable: 365.16/148.09 Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1} 365.16/148.09 365.16/148.09 TcT has computed the following constructor-based matrix 365.16/148.09 interpretation satisfying not(EDA). 365.16/148.09 365.16/148.09 [bubble[Ite][False][Ite]](x1, x2, x3) = [1] x3 + [6] 365.16/148.09 365.16/148.09 [bubble](x1, x2) = [1] x2 + [6] 365.16/148.09 365.16/148.09 [True] = [0] 365.16/148.09 365.16/148.09 [Nil] = [2] 365.16/148.09 365.16/148.09 [+](x1, x2) = [2] x1 + [1] x2 + [0] 365.16/148.09 365.16/148.09 [S](x1) = [1] x1 + [3] 365.16/148.09 365.16/148.09 [<](x1, x2) = [0] 365.16/148.09 365.16/148.09 [Cons](x1, x2) = [1] x2 + [2] 365.16/148.09 365.16/148.09 [0] = [0] 365.16/148.09 365.16/148.09 [len](x1) = [3] x1 + [0] 365.16/148.09 365.16/148.09 [False] = [0] 365.16/148.09 365.16/148.09 [bubble^#](x1, x2) = [1] x2 + [2] 365.16/148.09 365.16/148.09 [bubble[Ite][False][Ite]^#](x1, x2, x3) = [1] x3 + [0] 365.16/148.09 365.16/148.09 [bsort^#](x1, x2) = [2] x1 + [1] x2 + [0] 365.16/148.09 365.16/148.09 [bubblesort^#](x1) = [7] x1 + [7] 365.16/148.09 365.16/148.09 [c_2](x1) = [1] x1 + [0] 365.16/148.09 365.16/148.09 [c_4](x1) = [1] x1 + [0] 365.16/148.09 365.16/148.09 [c_5](x1) = [1] x1 + [0] 365.16/148.09 365.16/148.09 The order satisfies the following ordering constraints: 365.16/148.09 365.16/148.09 [bubble[Ite][False][Ite](True(), x', Cons(x, xs))] = [1] xs + [8] 365.16/148.09 >= [1] xs + [8] 365.16/148.09 = [Cons(x', bubble(x, xs))] 365.16/148.09 365.16/148.09 [bubble[Ite][False][Ite](False(), x', Cons(x, xs))] = [1] xs + [8] 365.16/148.09 >= [1] xs + [8] 365.16/148.09 = [Cons(x, bubble(x', xs))] 365.16/148.09 365.16/148.09 [bubble(x, Nil())] = [8] 365.16/148.09 > [4] 365.16/148.09 = [Cons(x, Nil())] 365.16/148.09 365.16/148.09 [bubble(x', Cons(x, xs))] = [1] xs + [8] 365.16/148.09 >= [1] xs + [8] 365.16/148.09 = [bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs))] 365.16/148.09 365.16/148.09 [+(x, S(0()))] = [2] x + [3] 365.16/148.09 >= [1] x + [3] 365.16/148.09 = [S(x)] 365.16/148.09 365.16/148.09 [+(S(0()), y)] = [1] y + [6] 365.16/148.09 > [1] y + [3] 365.16/148.09 = [S(y)] 365.16/148.09 365.16/148.09 [<(x, 0())] = [0] 365.16/148.09 >= [0] 365.16/148.09 = [False()] 365.16/148.09 365.16/148.09 [<(S(x), S(y))] = [0] 365.16/148.09 >= [0] 365.16/148.09 = [<(x, y)] 365.16/148.09 365.16/148.09 [<(0(), S(y))] = [0] 365.16/148.09 >= [0] 365.16/148.09 = [True()] 365.16/148.09 365.16/148.09 [len(Nil())] = [6] 365.16/148.09 > [0] 365.16/148.09 = [0()] 365.16/148.09 365.16/148.09 [len(Cons(x, xs))] = [3] xs + [6] 365.16/148.09 >= [3] xs + [6] 365.16/148.09 = [+(S(0()), len(xs))] 365.16/148.09 365.16/148.09 [bubble^#(x', Cons(x, xs))] = [1] xs + [4] 365.16/148.09 > [1] xs + [2] 365.16/148.09 = [c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))] 365.16/148.09 365.16/148.09 [bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs))] = [1] xs + [2] 365.16/148.09 >= [1] xs + [2] 365.16/148.09 = [c_4(bubble^#(x, xs))] 365.16/148.09 365.16/148.09 [bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs))] = [1] xs + [2] 365.16/148.09 >= [1] xs + [2] 365.16/148.09 = [c_5(bubble^#(x', xs))] 365.16/148.09 365.16/148.09 [bsort^#(S(x'), Cons(x, xs))] = [2] x' + [1] xs + [8] 365.16/148.09 > [1] xs + [2] 365.16/148.09 = [bubble^#(x, xs)] 365.16/148.09 365.16/148.09 [bsort^#(S(x'), Cons(x, xs))] = [2] x' + [1] xs + [8] 365.16/148.09 > [2] x' + [1] xs + [6] 365.16/148.09 = [bsort^#(x', bubble(x, xs))] 365.16/148.09 365.16/148.09 [bubblesort^#(xs)] = [7] xs + [7] 365.16/148.09 > [7] xs + [0] 365.16/148.09 = [bsort^#(len(xs), xs)] 365.16/148.09 365.16/148.09 365.16/148.09 We return to the main proof. Consider the set of all dependency 365.16/148.09 pairs 365.16/148.09 365.16/148.09 : 365.16/148.09 { 1: bubble^#(x', Cons(x, xs)) -> 365.16/148.09 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.09 , 2: bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.09 c_4(bubble^#(x, xs)) 365.16/148.09 , 3: bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.09 c_5(bubble^#(x', xs)) 365.16/148.09 , 4: bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs) 365.16/148.09 , 5: bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs)) 365.16/148.09 , 6: bubblesort^#(xs) -> bsort^#(len(xs), xs) } 365.16/148.09 365.16/148.09 Processor 'matrix interpretation of dimension 1' induces the 365.16/148.09 complexity certificate YES(?,O(n^1)) on application of dependency 365.16/148.09 pairs {1,4,5,6}. These cover all (indirect) predecessors of 365.16/148.09 dependency pairs {1,2,3,4,5,6}, their number of application is 365.16/148.09 equally bounded. The dependency pairs are shifted into the weak 365.16/148.09 component. 365.16/148.09 365.16/148.09 We are left with following problem, upon which TcT provides the 365.16/148.09 certificate YES(O(1),O(1)). 365.16/148.09 365.16/148.09 Weak DPs: 365.16/148.09 { bubble^#(x', Cons(x, xs)) -> 365.16/148.09 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.09 , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.09 c_4(bubble^#(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.09 c_5(bubble^#(x', xs)) 365.16/148.09 , bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs) 365.16/148.09 , bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs)) 365.16/148.09 , bubblesort^#(xs) -> bsort^#(len(xs), xs) } 365.16/148.09 Weak Trs: 365.16/148.09 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x', bubble(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x, bubble(x', xs)) 365.16/148.09 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.09 , bubble(x', Cons(x, xs)) -> 365.16/148.09 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.09 , +(x, S(0())) -> S(x) 365.16/148.09 , +(S(0()), y) -> S(y) 365.16/148.09 , <(x, 0()) -> False() 365.16/148.09 , <(S(x), S(y)) -> <(x, y) 365.16/148.09 , <(0(), S(y)) -> True() 365.16/148.09 , len(Nil()) -> 0() 365.16/148.09 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.09 Obligation: 365.16/148.09 innermost runtime complexity 365.16/148.09 Answer: 365.16/148.09 YES(O(1),O(1)) 365.16/148.09 365.16/148.09 The following weak DPs constitute a sub-graph of the DG that is 365.16/148.09 closed under successors. The DPs are removed. 365.16/148.09 365.16/148.09 { bubble^#(x', Cons(x, xs)) -> 365.16/148.09 c_2(bubble[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) 365.16/148.09 , bubble[Ite][False][Ite]^#(True(), x', Cons(x, xs)) -> 365.16/148.09 c_4(bubble^#(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite]^#(False(), x', Cons(x, xs)) -> 365.16/148.09 c_5(bubble^#(x', xs)) 365.16/148.09 , bsort^#(S(x'), Cons(x, xs)) -> bubble^#(x, xs) 365.16/148.09 , bsort^#(S(x'), Cons(x, xs)) -> bsort^#(x', bubble(x, xs)) 365.16/148.09 , bubblesort^#(xs) -> bsort^#(len(xs), xs) } 365.16/148.09 365.16/148.09 We are left with following problem, upon which TcT provides the 365.16/148.09 certificate YES(O(1),O(1)). 365.16/148.09 365.16/148.09 Weak Trs: 365.16/148.09 { bubble[Ite][False][Ite](True(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x', bubble(x, xs)) 365.16/148.09 , bubble[Ite][False][Ite](False(), x', Cons(x, xs)) -> 365.16/148.09 Cons(x, bubble(x', xs)) 365.16/148.09 , bubble(x, Nil()) -> Cons(x, Nil()) 365.16/148.09 , bubble(x', Cons(x, xs)) -> 365.16/148.09 bubble[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 365.16/148.09 , +(x, S(0())) -> S(x) 365.16/148.09 , +(S(0()), y) -> S(y) 365.16/148.09 , <(x, 0()) -> False() 365.16/148.09 , <(S(x), S(y)) -> <(x, y) 365.16/148.09 , <(0(), S(y)) -> True() 365.16/148.09 , len(Nil()) -> 0() 365.16/148.09 , len(Cons(x, xs)) -> +(S(0()), len(xs)) } 365.16/148.09 Obligation: 365.16/148.09 innermost runtime complexity 365.16/148.09 Answer: 365.16/148.09 YES(O(1),O(1)) 365.16/148.09 365.16/148.09 No rule is usable, rules are removed from the input problem. 365.16/148.09 365.16/148.09 We are left with following problem, upon which TcT provides the 365.16/148.09 certificate YES(O(1),O(1)). 365.16/148.09 365.16/148.09 Rules: Empty 365.16/148.09 Obligation: 365.16/148.09 innermost runtime complexity 365.16/148.09 Answer: 365.16/148.09 YES(O(1),O(1)) 365.16/148.09 365.16/148.09 Empty rules are trivially bounded 365.16/148.09 365.16/148.09 365.16/148.09 Hurray, we answered YES(O(1),O(n^2)) 365.41/148.11 EOF