MAYBE 737.83/297.12 MAYBE 737.83/297.12 737.83/297.12 We are left with following problem, upon which TcT provides the 737.83/297.12 certificate MAYBE. 737.83/297.12 737.83/297.12 Strict Trs: 737.83/297.12 { ge(x, 0()) -> true() 737.83/297.12 , ge(0(), s(y)) -> false() 737.83/297.12 , ge(s(x), s(y)) -> ge(x, y) 737.83/297.12 , rev(x) -> if(x, eq(0(), length(x)), nil(), 0(), length(x)) 737.83/297.12 , if(x, true(), z, c, l) -> z 737.83/297.12 , if(x, false(), z, c, l) -> help(s(c), l, x, z) 737.83/297.12 , length(nil()) -> 0() 737.83/297.12 , length(cons(x, y)) -> s(length(y)) 737.83/297.12 , help(c, l, cons(x, y), z) -> 737.83/297.12 if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l) 737.83/297.12 , append(nil(), y) -> y 737.83/297.12 , append(cons(x, y), z) -> cons(x, append(y, z)) } 737.83/297.12 Obligation: 737.83/297.12 runtime complexity 737.83/297.12 Answer: 737.83/297.12 MAYBE 737.83/297.12 737.83/297.12 None of the processors succeeded. 737.83/297.12 737.83/297.12 Details of failed attempt(s): 737.83/297.12 ----------------------------- 737.83/297.12 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 737.83/297.12 following reason: 737.83/297.12 737.83/297.12 Computation stopped due to timeout after 297.0 seconds. 737.83/297.12 737.83/297.12 2) 'Best' failed due to the following reason: 737.83/297.12 737.83/297.12 None of the processors succeeded. 737.83/297.12 737.83/297.12 Details of failed attempt(s): 737.83/297.12 ----------------------------- 737.83/297.12 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 737.83/297.12 seconds)' failed due to the following reason: 737.83/297.12 737.83/297.12 Computation stopped due to timeout after 148.0 seconds. 737.83/297.12 737.83/297.12 2) 'Best' failed due to the following reason: 737.83/297.12 737.83/297.12 None of the processors succeeded. 737.83/297.12 737.83/297.12 Details of failed attempt(s): 737.83/297.12 ----------------------------- 737.83/297.12 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 737.83/297.12 to the following reason: 737.83/297.12 737.83/297.12 The processor is inapplicable, reason: 737.83/297.12 Processor only applicable for innermost runtime complexity analysis 737.83/297.12 737.83/297.12 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 737.83/297.12 following reason: 737.83/297.12 737.83/297.12 The processor is inapplicable, reason: 737.83/297.12 Processor only applicable for innermost runtime complexity analysis 737.83/297.12 737.83/297.12 737.83/297.12 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 737.83/297.12 failed due to the following reason: 737.83/297.12 737.83/297.12 None of the processors succeeded. 737.83/297.12 737.83/297.12 Details of failed attempt(s): 737.83/297.12 ----------------------------- 737.83/297.12 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 737.83/297.12 failed due to the following reason: 737.83/297.12 737.83/297.12 match-boundness of the problem could not be verified. 737.83/297.12 737.83/297.12 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 737.83/297.12 failed due to the following reason: 737.83/297.12 737.83/297.12 match-boundness of the problem could not be verified. 737.83/297.12 737.83/297.12 737.83/297.12 737.83/297.12 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 737.83/297.12 the following reason: 737.83/297.12 737.83/297.12 We add the following weak dependency pairs: 737.83/297.12 737.83/297.12 Strict DPs: 737.83/297.12 { ge^#(x, 0()) -> c_1() 737.83/297.12 , ge^#(0(), s(y)) -> c_2() 737.83/297.12 , ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) 737.83/297.12 , rev^#(x) -> 737.83/297.12 c_4(if^#(x, eq(0(), length(x)), nil(), 0(), length(x))) 737.83/297.12 , if^#(x, true(), z, c, l) -> c_5(z) 737.83/297.12 , if^#(x, false(), z, c, l) -> c_6(help^#(s(c), l, x, z)) 737.83/297.12 , help^#(c, l, cons(x, y), z) -> 737.83/297.12 c_9(if^#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)) 737.83/297.12 , length^#(nil()) -> c_7() 737.83/297.12 , length^#(cons(x, y)) -> c_8(length^#(y)) 737.83/297.12 , append^#(nil(), y) -> c_10(y) 737.83/297.12 , append^#(cons(x, y), z) -> c_11(x, append^#(y, z)) } 737.83/297.12 737.83/297.12 and mark the set of starting terms. 737.83/297.12 737.83/297.12 We are left with following problem, upon which TcT provides the 737.83/297.12 certificate MAYBE. 737.83/297.12 737.83/297.12 Strict DPs: 737.83/297.12 { ge^#(x, 0()) -> c_1() 737.83/297.12 , ge^#(0(), s(y)) -> c_2() 737.83/297.12 , ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) 737.83/297.12 , rev^#(x) -> 737.83/297.12 c_4(if^#(x, eq(0(), length(x)), nil(), 0(), length(x))) 737.83/297.12 , if^#(x, true(), z, c, l) -> c_5(z) 737.83/297.12 , if^#(x, false(), z, c, l) -> c_6(help^#(s(c), l, x, z)) 737.83/297.12 , help^#(c, l, cons(x, y), z) -> 737.83/297.12 c_9(if^#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)) 737.83/297.12 , length^#(nil()) -> c_7() 737.83/297.12 , length^#(cons(x, y)) -> c_8(length^#(y)) 737.83/297.12 , append^#(nil(), y) -> c_10(y) 737.83/297.12 , append^#(cons(x, y), z) -> c_11(x, append^#(y, z)) } 737.83/297.12 Strict Trs: 737.83/297.12 { ge(x, 0()) -> true() 737.83/297.12 , ge(0(), s(y)) -> false() 737.83/297.12 , ge(s(x), s(y)) -> ge(x, y) 737.83/297.12 , rev(x) -> if(x, eq(0(), length(x)), nil(), 0(), length(x)) 737.83/297.12 , if(x, true(), z, c, l) -> z 737.83/297.12 , if(x, false(), z, c, l) -> help(s(c), l, x, z) 737.83/297.12 , length(nil()) -> 0() 737.83/297.12 , length(cons(x, y)) -> s(length(y)) 737.83/297.12 , help(c, l, cons(x, y), z) -> 737.83/297.12 if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l) 737.83/297.12 , append(nil(), y) -> y 737.83/297.12 , append(cons(x, y), z) -> cons(x, append(y, z)) } 737.83/297.12 Obligation: 737.83/297.12 runtime complexity 737.83/297.12 Answer: 737.83/297.12 MAYBE 737.83/297.12 737.83/297.12 We estimate the number of application of {1,2,4,8} by applications 737.83/297.12 of Pre({1,2,4,8}) = {3,5,9,10,11}. Here rules are labeled as 737.83/297.12 follows: 737.83/297.12 737.83/297.12 DPs: 737.83/297.12 { 1: ge^#(x, 0()) -> c_1() 737.83/297.12 , 2: ge^#(0(), s(y)) -> c_2() 737.83/297.12 , 3: ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) 737.83/297.12 , 4: rev^#(x) -> 737.83/297.12 c_4(if^#(x, eq(0(), length(x)), nil(), 0(), length(x))) 737.83/297.12 , 5: if^#(x, true(), z, c, l) -> c_5(z) 737.83/297.12 , 6: if^#(x, false(), z, c, l) -> c_6(help^#(s(c), l, x, z)) 737.83/297.12 , 7: help^#(c, l, cons(x, y), z) -> 737.83/297.12 c_9(if^#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)) 737.83/297.12 , 8: length^#(nil()) -> c_7() 737.83/297.12 , 9: length^#(cons(x, y)) -> c_8(length^#(y)) 737.83/297.12 , 10: append^#(nil(), y) -> c_10(y) 737.83/297.12 , 11: append^#(cons(x, y), z) -> c_11(x, append^#(y, z)) } 737.83/297.12 737.83/297.12 We are left with following problem, upon which TcT provides the 737.83/297.12 certificate MAYBE. 737.83/297.12 737.83/297.12 Strict DPs: 737.83/297.12 { ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) 737.83/297.12 , if^#(x, true(), z, c, l) -> c_5(z) 737.83/297.12 , if^#(x, false(), z, c, l) -> c_6(help^#(s(c), l, x, z)) 737.83/297.12 , help^#(c, l, cons(x, y), z) -> 737.83/297.12 c_9(if^#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)) 737.83/297.12 , length^#(cons(x, y)) -> c_8(length^#(y)) 737.83/297.12 , append^#(nil(), y) -> c_10(y) 737.83/297.12 , append^#(cons(x, y), z) -> c_11(x, append^#(y, z)) } 737.83/297.12 Strict Trs: 737.83/297.12 { ge(x, 0()) -> true() 737.83/297.12 , ge(0(), s(y)) -> false() 737.83/297.12 , ge(s(x), s(y)) -> ge(x, y) 737.83/297.12 , rev(x) -> if(x, eq(0(), length(x)), nil(), 0(), length(x)) 737.83/297.12 , if(x, true(), z, c, l) -> z 737.83/297.12 , if(x, false(), z, c, l) -> help(s(c), l, x, z) 737.83/297.12 , length(nil()) -> 0() 737.83/297.12 , length(cons(x, y)) -> s(length(y)) 737.83/297.12 , help(c, l, cons(x, y), z) -> 737.83/297.12 if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l) 737.83/297.12 , append(nil(), y) -> y 737.83/297.12 , append(cons(x, y), z) -> cons(x, append(y, z)) } 737.83/297.12 Weak DPs: 737.83/297.12 { ge^#(x, 0()) -> c_1() 737.83/297.12 , ge^#(0(), s(y)) -> c_2() 737.83/297.12 , rev^#(x) -> 737.83/297.12 c_4(if^#(x, eq(0(), length(x)), nil(), 0(), length(x))) 737.83/297.12 , length^#(nil()) -> c_7() } 737.83/297.12 Obligation: 737.83/297.12 runtime complexity 737.83/297.12 Answer: 737.83/297.12 MAYBE 737.83/297.12 737.83/297.12 Empty strict component of the problem is NOT empty. 737.83/297.12 737.83/297.12 737.83/297.12 Arrrr.. 738.13/297.45 EOF