MAYBE 814.46/297.03 MAYBE 814.46/297.03 814.46/297.03 We are left with following problem, upon which TcT provides the 814.46/297.03 certificate MAYBE. 814.46/297.03 814.46/297.03 Strict Trs: 814.46/297.03 { +(0(), y) -> y 814.46/297.03 , +(s(x), y) -> s(+(x, y)) 814.46/297.03 , ++(nil(), ys) -> ys 814.46/297.03 , ++(:(x, xs), ys) -> :(x, ++(xs, ys)) 814.46/297.03 , sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys))))) 814.46/297.03 , sum(:(x, nil())) -> :(x, nil()) 814.46/297.03 , sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs)) 814.46/297.03 , -(x, 0()) -> x 814.46/297.03 , -(0(), s(y)) -> 0() 814.46/297.03 , -(s(x), s(y)) -> -(x, y) 814.46/297.03 , quot(0(), s(y)) -> 0() 814.46/297.03 , quot(s(x), s(y)) -> s(quot(-(x, y), s(y))) 814.46/297.03 , length(nil()) -> 0() 814.46/297.03 , length(:(x, xs)) -> s(length(xs)) 814.46/297.03 , hd(:(x, xs)) -> x 814.46/297.03 , avg(xs) -> quot(hd(sum(xs)), length(xs)) } 814.46/297.03 Obligation: 814.46/297.03 runtime complexity 814.46/297.03 Answer: 814.46/297.03 MAYBE 814.46/297.03 814.46/297.03 None of the processors succeeded. 814.46/297.03 814.46/297.03 Details of failed attempt(s): 814.46/297.03 ----------------------------- 814.46/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 814.46/297.03 following reason: 814.46/297.03 814.46/297.03 Computation stopped due to timeout after 297.0 seconds. 814.46/297.03 814.46/297.03 2) 'Best' failed due to the following reason: 814.46/297.03 814.46/297.03 None of the processors succeeded. 814.46/297.03 814.46/297.03 Details of failed attempt(s): 814.46/297.03 ----------------------------- 814.46/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 814.46/297.03 seconds)' failed due to the following reason: 814.46/297.03 814.46/297.03 Computation stopped due to timeout after 148.0 seconds. 814.46/297.03 814.46/297.03 2) 'Best' failed due to the following reason: 814.46/297.03 814.46/297.03 None of the processors succeeded. 814.46/297.03 814.46/297.03 Details of failed attempt(s): 814.46/297.03 ----------------------------- 814.46/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 814.46/297.03 following reason: 814.46/297.03 814.46/297.03 The processor is inapplicable, reason: 814.46/297.03 Processor only applicable for innermost runtime complexity analysis 814.46/297.03 814.46/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 814.46/297.03 to the following reason: 814.46/297.03 814.46/297.03 The processor is inapplicable, reason: 814.46/297.03 Processor only applicable for innermost runtime complexity analysis 814.46/297.03 814.46/297.03 814.46/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 814.46/297.03 failed due to the following reason: 814.46/297.03 814.46/297.03 None of the processors succeeded. 814.46/297.03 814.46/297.03 Details of failed attempt(s): 814.46/297.03 ----------------------------- 814.46/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 814.46/297.03 failed due to the following reason: 814.46/297.03 814.46/297.03 match-boundness of the problem could not be verified. 814.46/297.03 814.46/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 814.46/297.03 failed due to the following reason: 814.46/297.03 814.46/297.03 match-boundness of the problem could not be verified. 814.46/297.03 814.46/297.03 814.46/297.03 814.46/297.03 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 814.46/297.03 the following reason: 814.46/297.03 814.46/297.03 We add the following weak dependency pairs: 814.46/297.03 814.46/297.03 Strict DPs: 814.46/297.03 { +^#(0(), y) -> c_1(y) 814.46/297.03 , +^#(s(x), y) -> c_2(+^#(x, y)) 814.46/297.03 , ++^#(nil(), ys) -> c_3(ys) 814.46/297.03 , ++^#(:(x, xs), ys) -> c_4(x, ++^#(xs, ys)) 814.46/297.03 , sum^#(++(xs, :(x, :(y, ys)))) -> 814.46/297.03 c_5(sum^#(++(xs, sum(:(x, :(y, ys)))))) 814.46/297.03 , sum^#(:(x, nil())) -> c_6(x) 814.46/297.03 , sum^#(:(x, :(y, xs))) -> c_7(sum^#(:(+(x, y), xs))) 814.46/297.03 , -^#(x, 0()) -> c_8(x) 814.46/297.03 , -^#(0(), s(y)) -> c_9() 814.46/297.03 , -^#(s(x), s(y)) -> c_10(-^#(x, y)) 814.46/297.03 , quot^#(0(), s(y)) -> c_11() 814.46/297.03 , quot^#(s(x), s(y)) -> c_12(quot^#(-(x, y), s(y))) 814.46/297.03 , length^#(nil()) -> c_13() 814.46/297.03 , length^#(:(x, xs)) -> c_14(length^#(xs)) 814.46/297.03 , hd^#(:(x, xs)) -> c_15(x) 814.46/297.03 , avg^#(xs) -> c_16(quot^#(hd(sum(xs)), length(xs))) } 814.46/297.03 814.46/297.03 and mark the set of starting terms. 814.46/297.03 814.46/297.03 We are left with following problem, upon which TcT provides the 814.46/297.03 certificate MAYBE. 814.46/297.03 814.46/297.03 Strict DPs: 814.46/297.03 { +^#(0(), y) -> c_1(y) 814.46/297.03 , +^#(s(x), y) -> c_2(+^#(x, y)) 814.46/297.03 , ++^#(nil(), ys) -> c_3(ys) 814.46/297.03 , ++^#(:(x, xs), ys) -> c_4(x, ++^#(xs, ys)) 814.46/297.03 , sum^#(++(xs, :(x, :(y, ys)))) -> 814.46/297.03 c_5(sum^#(++(xs, sum(:(x, :(y, ys)))))) 814.46/297.03 , sum^#(:(x, nil())) -> c_6(x) 814.46/297.03 , sum^#(:(x, :(y, xs))) -> c_7(sum^#(:(+(x, y), xs))) 814.46/297.03 , -^#(x, 0()) -> c_8(x) 814.46/297.03 , -^#(0(), s(y)) -> c_9() 814.46/297.03 , -^#(s(x), s(y)) -> c_10(-^#(x, y)) 814.46/297.03 , quot^#(0(), s(y)) -> c_11() 814.46/297.03 , quot^#(s(x), s(y)) -> c_12(quot^#(-(x, y), s(y))) 814.46/297.03 , length^#(nil()) -> c_13() 814.46/297.03 , length^#(:(x, xs)) -> c_14(length^#(xs)) 814.46/297.03 , hd^#(:(x, xs)) -> c_15(x) 814.46/297.03 , avg^#(xs) -> c_16(quot^#(hd(sum(xs)), length(xs))) } 814.46/297.03 Strict Trs: 814.46/297.03 { +(0(), y) -> y 814.46/297.03 , +(s(x), y) -> s(+(x, y)) 814.46/297.03 , ++(nil(), ys) -> ys 814.46/297.03 , ++(:(x, xs), ys) -> :(x, ++(xs, ys)) 814.46/297.03 , sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys))))) 814.46/297.03 , sum(:(x, nil())) -> :(x, nil()) 814.46/297.03 , sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs)) 814.46/297.03 , -(x, 0()) -> x 814.46/297.03 , -(0(), s(y)) -> 0() 814.46/297.03 , -(s(x), s(y)) -> -(x, y) 814.46/297.03 , quot(0(), s(y)) -> 0() 814.46/297.03 , quot(s(x), s(y)) -> s(quot(-(x, y), s(y))) 814.46/297.03 , length(nil()) -> 0() 814.46/297.03 , length(:(x, xs)) -> s(length(xs)) 814.46/297.03 , hd(:(x, xs)) -> x 814.46/297.03 , avg(xs) -> quot(hd(sum(xs)), length(xs)) } 814.46/297.03 Obligation: 814.46/297.03 runtime complexity 814.46/297.03 Answer: 814.46/297.03 MAYBE 814.46/297.03 814.46/297.03 We estimate the number of application of {9,11,13} by applications 814.46/297.03 of Pre({9,11,13}) = {1,3,4,6,8,10,12,14,15,16}. Here rules are 814.46/297.03 labeled as follows: 814.46/297.03 814.46/297.03 DPs: 814.46/297.03 { 1: +^#(0(), y) -> c_1(y) 814.46/297.03 , 2: +^#(s(x), y) -> c_2(+^#(x, y)) 814.46/297.03 , 3: ++^#(nil(), ys) -> c_3(ys) 814.46/297.03 , 4: ++^#(:(x, xs), ys) -> c_4(x, ++^#(xs, ys)) 814.46/297.03 , 5: sum^#(++(xs, :(x, :(y, ys)))) -> 814.46/297.03 c_5(sum^#(++(xs, sum(:(x, :(y, ys)))))) 814.46/297.03 , 6: sum^#(:(x, nil())) -> c_6(x) 814.46/297.03 , 7: sum^#(:(x, :(y, xs))) -> c_7(sum^#(:(+(x, y), xs))) 814.46/297.03 , 8: -^#(x, 0()) -> c_8(x) 814.46/297.03 , 9: -^#(0(), s(y)) -> c_9() 814.46/297.03 , 10: -^#(s(x), s(y)) -> c_10(-^#(x, y)) 814.46/297.03 , 11: quot^#(0(), s(y)) -> c_11() 814.46/297.03 , 12: quot^#(s(x), s(y)) -> c_12(quot^#(-(x, y), s(y))) 814.46/297.03 , 13: length^#(nil()) -> c_13() 814.46/297.03 , 14: length^#(:(x, xs)) -> c_14(length^#(xs)) 814.46/297.03 , 15: hd^#(:(x, xs)) -> c_15(x) 814.46/297.03 , 16: avg^#(xs) -> c_16(quot^#(hd(sum(xs)), length(xs))) } 814.46/297.03 814.46/297.03 We are left with following problem, upon which TcT provides the 814.46/297.03 certificate MAYBE. 814.46/297.03 814.46/297.03 Strict DPs: 814.46/297.03 { +^#(0(), y) -> c_1(y) 814.46/297.03 , +^#(s(x), y) -> c_2(+^#(x, y)) 814.46/297.03 , ++^#(nil(), ys) -> c_3(ys) 814.46/297.03 , ++^#(:(x, xs), ys) -> c_4(x, ++^#(xs, ys)) 814.46/297.03 , sum^#(++(xs, :(x, :(y, ys)))) -> 814.46/297.03 c_5(sum^#(++(xs, sum(:(x, :(y, ys)))))) 814.46/297.03 , sum^#(:(x, nil())) -> c_6(x) 814.46/297.03 , sum^#(:(x, :(y, xs))) -> c_7(sum^#(:(+(x, y), xs))) 814.46/297.03 , -^#(x, 0()) -> c_8(x) 814.46/297.03 , -^#(s(x), s(y)) -> c_10(-^#(x, y)) 814.46/297.03 , quot^#(s(x), s(y)) -> c_12(quot^#(-(x, y), s(y))) 814.46/297.03 , length^#(:(x, xs)) -> c_14(length^#(xs)) 814.46/297.03 , hd^#(:(x, xs)) -> c_15(x) 814.46/297.03 , avg^#(xs) -> c_16(quot^#(hd(sum(xs)), length(xs))) } 814.46/297.03 Strict Trs: 814.46/297.03 { +(0(), y) -> y 814.46/297.03 , +(s(x), y) -> s(+(x, y)) 814.46/297.03 , ++(nil(), ys) -> ys 814.46/297.03 , ++(:(x, xs), ys) -> :(x, ++(xs, ys)) 814.46/297.03 , sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys))))) 814.46/297.03 , sum(:(x, nil())) -> :(x, nil()) 814.46/297.03 , sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs)) 814.46/297.03 , -(x, 0()) -> x 814.46/297.03 , -(0(), s(y)) -> 0() 814.46/297.03 , -(s(x), s(y)) -> -(x, y) 814.46/297.03 , quot(0(), s(y)) -> 0() 814.46/297.03 , quot(s(x), s(y)) -> s(quot(-(x, y), s(y))) 814.46/297.03 , length(nil()) -> 0() 814.46/297.03 , length(:(x, xs)) -> s(length(xs)) 814.46/297.03 , hd(:(x, xs)) -> x 814.46/297.03 , avg(xs) -> quot(hd(sum(xs)), length(xs)) } 814.46/297.03 Weak DPs: 814.46/297.03 { -^#(0(), s(y)) -> c_9() 814.46/297.03 , quot^#(0(), s(y)) -> c_11() 814.46/297.03 , length^#(nil()) -> c_13() } 814.46/297.03 Obligation: 814.46/297.03 runtime complexity 814.46/297.03 Answer: 814.46/297.03 MAYBE 814.46/297.03 814.46/297.03 Empty strict component of the problem is NOT empty. 814.46/297.03 814.46/297.03 814.46/297.03 Arrrr.. 814.67/297.29 EOF