MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { div(x, y) -> div2(x, y, 0()) , div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)) , if1(true(), b, x, y, i, j) -> divZeroError() , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , plus(x, y) -> plusIter(x, y, 0()) , inc(0()) -> 0() , inc(s(i)) -> s(inc(i)) , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j) , if2(false(), x, y, i, j) -> i , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , 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)) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { div^#(x, y) -> c_1(div2^#(x, y, 0())) , div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, 0()), le^#(y, x), plus^#(i, 0()), inc^#(i)) , if1^#(true(), b, x, y, i, j) -> c_3() , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j)) , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , plus^#(x, y) -> c_8(plusIter^#(x, y, 0())) , inc^#(0()) -> c_9() , inc^#(s(i)) -> c_10(inc^#(i)) , if2^#(true(), x, y, i, j) -> c_11(div2^#(minus(x, y), y, j), minus^#(x, y)) , if2^#(false(), x, y, i, j) -> c_12() , plusIter^#(x, y, z) -> c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , minus^#(x, 0()) -> c_13() , minus^#(0(), y) -> c_14() , minus^#(s(x), s(y)) -> c_15(minus^#(x, y)) , ifPlus^#(true(), x, y, z) -> c_17() , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) , a^#() -> c_19() , a^#() -> c_20() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { div^#(x, y) -> c_1(div2^#(x, y, 0())) , div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, 0()), le^#(y, x), plus^#(i, 0()), inc^#(i)) , if1^#(true(), b, x, y, i, j) -> c_3() , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j)) , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , plus^#(x, y) -> c_8(plusIter^#(x, y, 0())) , inc^#(0()) -> c_9() , inc^#(s(i)) -> c_10(inc^#(i)) , if2^#(true(), x, y, i, j) -> c_11(div2^#(minus(x, y), y, j), minus^#(x, y)) , if2^#(false(), x, y, i, j) -> c_12() , plusIter^#(x, y, z) -> c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , minus^#(x, 0()) -> c_13() , minus^#(0(), y) -> c_14() , minus^#(s(x), s(y)) -> c_15(minus^#(x, y)) , ifPlus^#(true(), x, y, z) -> c_17() , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) , a^#() -> c_19() , a^#() -> c_20() } Weak Trs: { div(x, y) -> div2(x, y, 0()) , div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)) , if1(true(), b, x, y, i, j) -> divZeroError() , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , plus(x, y) -> plusIter(x, y, 0()) , inc(0()) -> 0() , inc(s(i)) -> s(inc(i)) , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j) , if2(false(), x, y, i, j) -> i , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , 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)) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,5,6,9,12,14,15,17,19,20} by applications of Pre({3,5,6,9,12,14,15,17,19,20}) = {2,4,7,10,11,13,16}. Here rules are labeled as follows: DPs: { 1: div^#(x, y) -> c_1(div2^#(x, y, 0())) , 2: div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, 0()), le^#(y, x), plus^#(i, 0()), inc^#(i)) , 3: if1^#(true(), b, x, y, i, j) -> c_3() , 4: if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j)) , 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: plus^#(x, y) -> c_8(plusIter^#(x, y, 0())) , 9: inc^#(0()) -> c_9() , 10: inc^#(s(i)) -> c_10(inc^#(i)) , 11: if2^#(true(), x, y, i, j) -> c_11(div2^#(minus(x, y), y, j), minus^#(x, y)) , 12: if2^#(false(), x, y, i, j) -> c_12() , 13: plusIter^#(x, y, z) -> c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , 14: minus^#(x, 0()) -> c_13() , 15: minus^#(0(), y) -> c_14() , 16: minus^#(s(x), s(y)) -> c_15(minus^#(x, y)) , 17: ifPlus^#(true(), x, y, z) -> c_17() , 18: ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) , 19: a^#() -> c_19() , 20: a^#() -> c_20() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { div^#(x, y) -> c_1(div2^#(x, y, 0())) , div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, 0()), le^#(y, x), plus^#(i, 0()), inc^#(i)) , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j)) , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , plus^#(x, y) -> c_8(plusIter^#(x, y, 0())) , inc^#(s(i)) -> c_10(inc^#(i)) , if2^#(true(), x, y, i, j) -> c_11(div2^#(minus(x, y), y, j), minus^#(x, y)) , plusIter^#(x, y, z) -> c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , minus^#(s(x), s(y)) -> c_15(minus^#(x, y)) , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) } Weak DPs: { if1^#(true(), b, x, y, i, j) -> c_3() , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , inc^#(0()) -> c_9() , if2^#(false(), x, y, i, j) -> c_12() , minus^#(x, 0()) -> c_13() , minus^#(0(), y) -> c_14() , ifPlus^#(true(), x, y, z) -> c_17() , a^#() -> c_19() , a^#() -> c_20() } Weak Trs: { div(x, y) -> div2(x, y, 0()) , div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)) , if1(true(), b, x, y, i, j) -> divZeroError() , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , plus(x, y) -> plusIter(x, y, 0()) , inc(0()) -> 0() , inc(s(i)) -> s(inc(i)) , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j) , if2(false(), x, y, i, j) -> i , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , 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)) , 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. { if1^#(true(), b, x, y, i, j) -> c_3() , le^#(0(), y) -> c_5() , le^#(s(x), 0()) -> c_6() , inc^#(0()) -> c_9() , if2^#(false(), x, y, i, j) -> c_12() , minus^#(x, 0()) -> c_13() , minus^#(0(), y) -> c_14() , ifPlus^#(true(), x, y, z) -> c_17() , a^#() -> c_19() , a^#() -> c_20() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { div^#(x, y) -> c_1(div2^#(x, y, 0())) , div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, 0()), le^#(y, x), plus^#(i, 0()), inc^#(i)) , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j)) , le^#(s(x), s(y)) -> c_7(le^#(x, y)) , plus^#(x, y) -> c_8(plusIter^#(x, y, 0())) , inc^#(s(i)) -> c_10(inc^#(i)) , if2^#(true(), x, y, i, j) -> c_11(div2^#(minus(x, y), y, j), minus^#(x, y)) , plusIter^#(x, y, z) -> c_16(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , minus^#(s(x), s(y)) -> c_15(minus^#(x, y)) , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) } Weak Trs: { div(x, y) -> div2(x, y, 0()) , div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)) , if1(true(), b, x, y, i, j) -> divZeroError() , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , plus(x, y) -> plusIter(x, y, 0()) , inc(0()) -> 0() , inc(s(i)) -> s(inc(i)) , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j) , if2(false(), x, y, i, j) -> i , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , 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)) , 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: { div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, 0()), le^#(y, x), plus^#(i, 0()), inc^#(i)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { div^#(x, y) -> c_1(div2^#(x, y, 0())) , div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, x), plus^#(i, 0()), inc^#(i)) , if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j)) , le^#(s(x), s(y)) -> c_4(le^#(x, y)) , plus^#(x, y) -> c_5(plusIter^#(x, y, 0())) , inc^#(s(i)) -> c_6(inc^#(i)) , if2^#(true(), x, y, i, j) -> c_7(div2^#(minus(x, y), y, j), minus^#(x, y)) , plusIter^#(x, y, z) -> c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , ifPlus^#(false(), x, y, z) -> c_10(plusIter^#(x, s(y), s(z))) } Weak Trs: { div(x, y) -> div2(x, y, 0()) , div2(x, y, i) -> if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)) , if1(true(), b, x, y, i, j) -> divZeroError() , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j) , le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , plus(x, y) -> plusIter(x, y, 0()) , inc(0()) -> 0() , inc(s(i)) -> s(inc(i)) , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j) , if2(false(), x, y, i, j) -> i , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , 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)) , a() -> c() , a() -> d() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , plus(x, y) -> plusIter(x, y, 0()) , inc(0()) -> 0() , inc(s(i)) -> s(inc(i)) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , 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)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { div^#(x, y) -> c_1(div2^#(x, y, 0())) , div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, x), plus^#(i, 0()), inc^#(i)) , if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j)) , le^#(s(x), s(y)) -> c_4(le^#(x, y)) , plus^#(x, y) -> c_5(plusIter^#(x, y, 0())) , inc^#(s(i)) -> c_6(inc^#(i)) , if2^#(true(), x, y, i, j) -> c_7(div2^#(minus(x, y), y, j), minus^#(x, y)) , plusIter^#(x, y, z) -> c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , ifPlus^#(false(), x, y, z) -> c_10(plusIter^#(x, s(y), s(z))) } Weak Trs: { le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , plus(x, y) -> plusIter(x, y, 0()) , inc(0()) -> 0() , inc(s(i)) -> s(inc(i)) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , 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)) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: div^#(x, y) -> c_1(div2^#(x, y, 0())) -->_1 div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, x), plus^#(i, 0()), inc^#(i)) :2 2: div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, x), plus^#(i, 0()), inc^#(i)) -->_4 inc^#(s(i)) -> c_6(inc^#(i)) :6 -->_3 plus^#(x, y) -> c_5(plusIter^#(x, y, 0())) :5 -->_2 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4 -->_1 if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j)) :3 3: if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j)) -->_1 if2^#(true(), x, y, i, j) -> c_7(div2^#(minus(x, y), y, j), minus^#(x, y)) :7 4: le^#(s(x), s(y)) -> c_4(le^#(x, y)) -->_1 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4 5: plus^#(x, y) -> c_5(plusIter^#(x, y, 0())) -->_1 plusIter^#(x, y, z) -> c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) :8 6: inc^#(s(i)) -> c_6(inc^#(i)) -->_1 inc^#(s(i)) -> c_6(inc^#(i)) :6 7: if2^#(true(), x, y, i, j) -> c_7(div2^#(minus(x, y), y, j), minus^#(x, y)) -->_2 minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) :9 -->_1 div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, x), plus^#(i, 0()), inc^#(i)) :2 8: plusIter^#(x, y, z) -> c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) -->_1 ifPlus^#(false(), x, y, z) -> c_10(plusIter^#(x, s(y), s(z))) :10 -->_2 le^#(s(x), s(y)) -> c_4(le^#(x, y)) :4 9: minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) -->_1 minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) :9 10: ifPlus^#(false(), x, y, z) -> c_10(plusIter^#(x, s(y), s(z))) -->_1 plusIter^#(x, y, z) -> c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) :8 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { div^#(x, y) -> c_1(div2^#(x, y, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { div2^#(x, y, i) -> c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)), le^#(y, x), plus^#(i, 0()), inc^#(i)) , if1^#(false(), b, x, y, i, j) -> c_3(if2^#(b, x, y, i, j)) , le^#(s(x), s(y)) -> c_4(le^#(x, y)) , plus^#(x, y) -> c_5(plusIter^#(x, y, 0())) , inc^#(s(i)) -> c_6(inc^#(i)) , if2^#(true(), x, y, i, j) -> c_7(div2^#(minus(x, y), y, j), minus^#(x, y)) , plusIter^#(x, y, z) -> c_8(ifPlus^#(le(x, z), x, y, z), le^#(x, z)) , minus^#(s(x), s(y)) -> c_9(minus^#(x, y)) , ifPlus^#(false(), x, y, z) -> c_10(plusIter^#(x, s(y), s(z))) } Weak Trs: { le(0(), y) -> true() , le(s(x), 0()) -> false() , le(s(x), s(y)) -> le(x, y) , plus(x, y) -> plusIter(x, y, 0()) , inc(0()) -> 0() , inc(s(i)) -> s(inc(i)) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , 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)) } 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: The input cannot be shown compatible 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..