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