MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { times(x, y) -> sum(generate(x, y)) , sum(xs) -> sum2(xs, 0()) , generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) , ifsum(true(), b, xs, y) -> y , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , ifsum2(true(), xs, y) -> sum2(tail(xs), y) , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { times^#(x, y) -> c_1(sum^#(generate(x, y)), generate^#(x, y)) , sum^#(xs) -> c_2(sum2^#(xs, 0())) , generate^#(x, y) -> c_3(gen^#(x, y, 0())) , sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y), isNil^#(xs), isZero^#(head(xs)), head^#(xs)) , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z), ge^#(z, x)) , if^#(true(), x, y, z) -> c_5() , if^#(false(), x, y, z) -> c_6(gen^#(x, y, s(z))) , ge^#(x, 0()) -> c_7() , ge^#(0(), s(y)) -> c_8() , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , ifsum^#(true(), b, xs, y) -> c_11() , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y)) , isNil^#(nil()) -> c_13() , isNil^#(cons(x, xs)) -> c_14() , isZero^#(0()) -> c_15() , isZero^#(s(0())) -> c_16() , isZero^#(s(s(x))) -> c_17(isZero^#(s(x))) , head^#(nil()) -> c_18() , head^#(cons(x, xs)) -> c_19() , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y), tail^#(xs)) , ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)), p^#(head(xs)), head^#(xs), tail^#(xs)) , tail^#(nil()) -> c_22() , tail^#(cons(x, xs)) -> c_23() , p^#(0()) -> c_24() , p^#(s(0())) -> c_25() , p^#(s(s(x))) -> c_26(p^#(s(x))) , a^#() -> c_27() , a^#() -> c_28() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { times^#(x, y) -> c_1(sum^#(generate(x, y)), generate^#(x, y)) , sum^#(xs) -> c_2(sum2^#(xs, 0())) , generate^#(x, y) -> c_3(gen^#(x, y, 0())) , sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y), isNil^#(xs), isZero^#(head(xs)), head^#(xs)) , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z), ge^#(z, x)) , if^#(true(), x, y, z) -> c_5() , if^#(false(), x, y, z) -> c_6(gen^#(x, y, s(z))) , ge^#(x, 0()) -> c_7() , ge^#(0(), s(y)) -> c_8() , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , ifsum^#(true(), b, xs, y) -> c_11() , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y)) , isNil^#(nil()) -> c_13() , isNil^#(cons(x, xs)) -> c_14() , isZero^#(0()) -> c_15() , isZero^#(s(0())) -> c_16() , isZero^#(s(s(x))) -> c_17(isZero^#(s(x))) , head^#(nil()) -> c_18() , head^#(cons(x, xs)) -> c_19() , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y), tail^#(xs)) , ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)), p^#(head(xs)), head^#(xs), tail^#(xs)) , tail^#(nil()) -> c_22() , tail^#(cons(x, xs)) -> c_23() , p^#(0()) -> c_24() , p^#(s(0())) -> c_25() , p^#(s(s(x))) -> c_26(p^#(s(x))) , a^#() -> c_27() , a^#() -> c_28() } Weak Trs: { times(x, y) -> sum(generate(x, y)) , sum(xs) -> sum2(xs, 0()) , generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) , ifsum(true(), b, xs, y) -> y , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , ifsum2(true(), xs, y) -> sum2(tail(xs), y) , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {6,8,9,11,13,14,15,16,18,19,22,23,24,25,27,28} by applications of Pre({6,8,9,11,13,14,15,16,18,19,22,23,24,25,27,28}) = {4,5,10,17,20,21,26}. Here rules are labeled as follows: DPs: { 1: times^#(x, y) -> c_1(sum^#(generate(x, y)), generate^#(x, y)) , 2: sum^#(xs) -> c_2(sum2^#(xs, 0())) , 3: generate^#(x, y) -> c_3(gen^#(x, y, 0())) , 4: sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y), isNil^#(xs), isZero^#(head(xs)), head^#(xs)) , 5: gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z), ge^#(z, x)) , 6: if^#(true(), x, y, z) -> c_5() , 7: if^#(false(), x, y, z) -> c_6(gen^#(x, y, s(z))) , 8: ge^#(x, 0()) -> c_7() , 9: ge^#(0(), s(y)) -> c_8() , 10: ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , 11: ifsum^#(true(), b, xs, y) -> c_11() , 12: ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y)) , 13: isNil^#(nil()) -> c_13() , 14: isNil^#(cons(x, xs)) -> c_14() , 15: isZero^#(0()) -> c_15() , 16: isZero^#(s(0())) -> c_16() , 17: isZero^#(s(s(x))) -> c_17(isZero^#(s(x))) , 18: head^#(nil()) -> c_18() , 19: head^#(cons(x, xs)) -> c_19() , 20: ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y), tail^#(xs)) , 21: ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)), p^#(head(xs)), head^#(xs), tail^#(xs)) , 22: tail^#(nil()) -> c_22() , 23: tail^#(cons(x, xs)) -> c_23() , 24: p^#(0()) -> c_24() , 25: p^#(s(0())) -> c_25() , 26: p^#(s(s(x))) -> c_26(p^#(s(x))) , 27: a^#() -> c_27() , 28: a^#() -> c_28() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { times^#(x, y) -> c_1(sum^#(generate(x, y)), generate^#(x, y)) , sum^#(xs) -> c_2(sum2^#(xs, 0())) , generate^#(x, y) -> c_3(gen^#(x, y, 0())) , sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y), isNil^#(xs), isZero^#(head(xs)), head^#(xs)) , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z), ge^#(z, x)) , if^#(false(), x, y, z) -> c_6(gen^#(x, y, s(z))) , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y)) , isZero^#(s(s(x))) -> c_17(isZero^#(s(x))) , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y), tail^#(xs)) , ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)), p^#(head(xs)), head^#(xs), tail^#(xs)) , p^#(s(s(x))) -> c_26(p^#(s(x))) } Weak DPs: { if^#(true(), x, y, z) -> c_5() , ge^#(x, 0()) -> c_7() , ge^#(0(), s(y)) -> c_8() , ifsum^#(true(), b, xs, y) -> c_11() , isNil^#(nil()) -> c_13() , isNil^#(cons(x, xs)) -> c_14() , isZero^#(0()) -> c_15() , isZero^#(s(0())) -> c_16() , head^#(nil()) -> c_18() , head^#(cons(x, xs)) -> c_19() , tail^#(nil()) -> c_22() , tail^#(cons(x, xs)) -> c_23() , p^#(0()) -> c_24() , p^#(s(0())) -> c_25() , a^#() -> c_27() , a^#() -> c_28() } Weak Trs: { times(x, y) -> sum(generate(x, y)) , sum(xs) -> sum2(xs, 0()) , generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) , ifsum(true(), b, xs, y) -> y , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , ifsum2(true(), xs, y) -> sum2(tail(xs), y) , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { if^#(true(), x, y, z) -> c_5() , ge^#(x, 0()) -> c_7() , ge^#(0(), s(y)) -> c_8() , ifsum^#(true(), b, xs, y) -> c_11() , isNil^#(nil()) -> c_13() , isNil^#(cons(x, xs)) -> c_14() , isZero^#(0()) -> c_15() , isZero^#(s(0())) -> c_16() , head^#(nil()) -> c_18() , head^#(cons(x, xs)) -> c_19() , tail^#(nil()) -> c_22() , tail^#(cons(x, xs)) -> c_23() , p^#(0()) -> c_24() , p^#(s(0())) -> c_25() , a^#() -> c_27() , a^#() -> c_28() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { times^#(x, y) -> c_1(sum^#(generate(x, y)), generate^#(x, y)) , sum^#(xs) -> c_2(sum2^#(xs, 0())) , generate^#(x, y) -> c_3(gen^#(x, y, 0())) , sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y), isNil^#(xs), isZero^#(head(xs)), head^#(xs)) , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z), ge^#(z, x)) , if^#(false(), x, y, z) -> c_6(gen^#(x, y, s(z))) , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y)) , isZero^#(s(s(x))) -> c_17(isZero^#(s(x))) , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y), tail^#(xs)) , ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)), p^#(head(xs)), head^#(xs), tail^#(xs)) , p^#(s(s(x))) -> c_26(p^#(s(x))) } Weak Trs: { times(x, y) -> sum(generate(x, y)) , sum(xs) -> sum2(xs, 0()) , generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) , ifsum(true(), b, xs, y) -> y , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , ifsum2(true(), xs, y) -> sum2(tail(xs), y) , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y), isNil^#(xs), isZero^#(head(xs)), head^#(xs)) , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y), tail^#(xs)) , ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y)), p^#(head(xs)), head^#(xs), tail^#(xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { times^#(x, y) -> c_1(sum^#(generate(x, y)), generate^#(x, y)) , sum^#(xs) -> c_2(sum2^#(xs, 0())) , generate^#(x, y) -> c_3(gen^#(x, y, 0())) , sum2^#(xs, y) -> c_4(ifsum^#(isNil(xs), isZero(head(xs)), xs, y), isZero^#(head(xs))) , gen^#(x, y, z) -> c_5(if^#(ge(z, x), x, y, z), ge^#(z, x)) , if^#(false(), x, y, z) -> c_6(gen^#(x, y, s(z))) , ge^#(s(x), s(y)) -> c_7(ge^#(x, y)) , ifsum^#(false(), b, xs, y) -> c_8(ifsum2^#(b, xs, y)) , isZero^#(s(s(x))) -> c_9(isZero^#(s(x))) , ifsum2^#(true(), xs, y) -> c_10(sum2^#(tail(xs), y)) , ifsum2^#(false(), xs, y) -> c_11(sum2^#(cons(p(head(xs)), tail(xs)), s(y)), p^#(head(xs))) , p^#(s(s(x))) -> c_12(p^#(s(x))) } Weak Trs: { times(x, y) -> sum(generate(x, y)) , sum(xs) -> sum2(xs, 0()) , generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) , ifsum(true(), b, xs, y) -> y , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , ifsum2(true(), xs, y) -> sum2(tail(xs), y) , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { times^#(x, y) -> c_1(sum^#(generate(x, y)), generate^#(x, y)) , sum^#(xs) -> c_2(sum2^#(xs, 0())) , generate^#(x, y) -> c_3(gen^#(x, y, 0())) , sum2^#(xs, y) -> c_4(ifsum^#(isNil(xs), isZero(head(xs)), xs, y), isZero^#(head(xs))) , gen^#(x, y, z) -> c_5(if^#(ge(z, x), x, y, z), ge^#(z, x)) , if^#(false(), x, y, z) -> c_6(gen^#(x, y, s(z))) , ge^#(s(x), s(y)) -> c_7(ge^#(x, y)) , ifsum^#(false(), b, xs, y) -> c_8(ifsum2^#(b, xs, y)) , isZero^#(s(s(x))) -> c_9(isZero^#(s(x))) , ifsum2^#(true(), xs, y) -> c_10(sum2^#(tail(xs), y)) , ifsum2^#(false(), xs, y) -> c_11(sum2^#(cons(p(head(xs)), tail(xs)), s(y)), p^#(head(xs))) , p^#(s(s(x))) -> c_12(p^#(s(x))) } Weak Trs: { generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrices' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'matrix interpretation of dimension 4' failed due to the following reason: Following exception was raised: stack overflow 2) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 3) 'matrix interpretation of dimension 3' failed due to the following reason: The input cannot be shown compatible 4) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 5) 'matrix interpretation of dimension 2' failed due to the following reason: The input cannot be shown compatible 6) 'matrix interpretation of dimension 1' failed due to the following reason: The input cannot be shown compatible 2) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. Arrrr..