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