MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , sum(xs) -> sumIter(xs, 0()) , sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))) , ifSum(true(), xs, x, y) -> x , ifSum(false(), xs, x, y) -> sumIter(tail(xs), y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , a() -> b() , a() -> c() } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z)) , ifPlus^#(true(), x, y, z) -> c_3(y) , ifPlus^#(false(), x, y, z) -> c_4(plusIter^#(x, s(y), s(z))) , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , sum^#(xs) -> c_8(sumIter^#(xs, 0())) , sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs)))) , ifSum^#(true(), xs, x, y) -> c_10(x) , ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y)) , isempty^#(nil()) -> c_12() , isempty^#(cons(x, xs)) -> c_13() , head^#(nil()) -> c_14() , head^#(cons(x, xs)) -> c_15(x) , tail^#(nil()) -> c_16() , tail^#(cons(x, xs)) -> c_17(xs) , a^#() -> c_18() , a^#() -> c_19() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z)) , ifPlus^#(true(), x, y, z) -> c_3(y) , ifPlus^#(false(), x, y, z) -> c_4(plusIter^#(x, s(y), s(z))) , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , sum^#(xs) -> c_8(sumIter^#(xs, 0())) , sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs)))) , ifSum^#(true(), xs, x, y) -> c_10(x) , ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y)) , isempty^#(nil()) -> c_12() , isempty^#(cons(x, xs)) -> c_13() , head^#(nil()) -> c_14() , head^#(cons(x, xs)) -> c_15(x) , tail^#(nil()) -> c_16() , tail^#(cons(x, xs)) -> c_17(xs) , a^#() -> c_18() , a^#() -> c_19() } Strict Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , sum(xs) -> sumIter(xs, 0()) , sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))) , ifSum(true(), xs, x, y) -> x , ifSum(false(), xs, x, y) -> sumIter(tail(xs), y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , a() -> b() , a() -> c() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,6,12,13,14,16,18,19} by applications of Pre({5,6,12,13,14,16,18,19}) = {3,7,10,15,17}. Here rules are labeled as follows: DPs: { 1: plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , 2: plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z)) , 3: ifPlus^#(true(), x, y, z) -> c_3(y) , 4: ifPlus^#(false(), x, y, z) -> c_4(plusIter^#(x, s(y), s(z))) , 5: le^#(0(), y) -> c_5() , 6: le^#(s(x), 0()) -> c_6() , 7: le^#(s(x), s(y)) -> c_7(le^#(x, y)) , 8: sum^#(xs) -> c_8(sumIter^#(xs, 0())) , 9: sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs)))) , 10: ifSum^#(true(), xs, x, y) -> c_10(x) , 11: ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y)) , 12: isempty^#(nil()) -> c_12() , 13: isempty^#(cons(x, xs)) -> c_13() , 14: head^#(nil()) -> c_14() , 15: head^#(cons(x, xs)) -> c_15(x) , 16: tail^#(nil()) -> c_16() , 17: tail^#(cons(x, xs)) -> c_17(xs) , 18: a^#() -> c_18() , 19: a^#() -> c_19() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { plus^#(x, y) -> c_1(plusIter^#(x, y, 0())) , plusIter^#(x, y, z) -> c_2(ifPlus^#(le(x, z), x, y, z)) , ifPlus^#(true(), x, y, z) -> c_3(y) , ifPlus^#(false(), x, y, z) -> c_4(plusIter^#(x, s(y), s(z))) , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , sum^#(xs) -> c_8(sumIter^#(xs, 0())) , sumIter^#(xs, x) -> c_9(ifSum^#(isempty(xs), xs, x, plus(x, head(xs)))) , ifSum^#(true(), xs, x, y) -> c_10(x) , ifSum^#(false(), xs, x, y) -> c_11(sumIter^#(tail(xs), y)) , head^#(cons(x, xs)) -> c_15(x) , tail^#(cons(x, xs)) -> c_17(xs) } Strict Trs: { plus(x, y) -> plusIter(x, y, 0()) , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) , ifPlus(true(), x, y, z) -> y , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , sum(xs) -> sumIter(xs, 0()) , sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))) , ifSum(true(), xs, x, y) -> x , ifSum(false(), xs, x, y) -> sumIter(tail(xs), y) , isempty(nil()) -> true() , isempty(cons(x, xs)) -> false() , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , a() -> b() , a() -> c() } Weak DPs: { le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , isempty^#(nil()) -> c_12() , isempty^#(cons(x, xs)) -> c_13() , head^#(nil()) -> c_14() , tail^#(nil()) -> c_16() , a^#() -> c_18() , a^#() -> c_19() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..