MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , id_inc(x) -> x , id_inc(x) -> s(x) , div(x, y) -> if(ge(y, s(0())), ge(x, y), x, y) , if(true(), true(), x, y) -> id_inc(div(minus(x, y), y)) , if(true(), false(), x, y) -> 0() , if(false(), b, x, y) -> div_by_zero() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { ge^#(x, 0()) -> c_1() , ge^#(0(), s(y)) -> c_2() , ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) , minus^#(x, 0()) -> c_4() , minus^#(0(), y) -> c_5() , minus^#(s(x), s(y)) -> c_6(minus^#(x, y)) , id_inc^#(x) -> c_7() , id_inc^#(x) -> c_8() , div^#(x, y) -> c_9(if^#(ge(y, s(0())), ge(x, y), x, y), ge^#(y, s(0())), ge^#(x, y)) , if^#(true(), true(), x, y) -> c_10(id_inc^#(div(minus(x, y), y)), div^#(minus(x, y), y), minus^#(x, y)) , if^#(true(), false(), x, y) -> c_11() , if^#(false(), b, x, y) -> c_12() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(x, 0()) -> c_1() , ge^#(0(), s(y)) -> c_2() , ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) , minus^#(x, 0()) -> c_4() , minus^#(0(), y) -> c_5() , minus^#(s(x), s(y)) -> c_6(minus^#(x, y)) , id_inc^#(x) -> c_7() , id_inc^#(x) -> c_8() , div^#(x, y) -> c_9(if^#(ge(y, s(0())), ge(x, y), x, y), ge^#(y, s(0())), ge^#(x, y)) , if^#(true(), true(), x, y) -> c_10(id_inc^#(div(minus(x, y), y)), div^#(minus(x, y), y), minus^#(x, y)) , if^#(true(), false(), x, y) -> c_11() , if^#(false(), b, x, y) -> c_12() } Weak Trs: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , id_inc(x) -> x , id_inc(x) -> s(x) , div(x, y) -> if(ge(y, s(0())), ge(x, y), x, y) , if(true(), true(), x, y) -> id_inc(div(minus(x, y), y)) , if(true(), false(), x, y) -> 0() , if(false(), b, x, y) -> div_by_zero() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,4,5,7,8,11,12} by applications of Pre({1,2,4,5,7,8,11,12}) = {3,6,9,10}. Here rules are labeled as follows: DPs: { 1: ge^#(x, 0()) -> c_1() , 2: ge^#(0(), s(y)) -> c_2() , 3: ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) , 4: minus^#(x, 0()) -> c_4() , 5: minus^#(0(), y) -> c_5() , 6: minus^#(s(x), s(y)) -> c_6(minus^#(x, y)) , 7: id_inc^#(x) -> c_7() , 8: id_inc^#(x) -> c_8() , 9: div^#(x, y) -> c_9(if^#(ge(y, s(0())), ge(x, y), x, y), ge^#(y, s(0())), ge^#(x, y)) , 10: if^#(true(), true(), x, y) -> c_10(id_inc^#(div(minus(x, y), y)), div^#(minus(x, y), y), minus^#(x, y)) , 11: if^#(true(), false(), x, y) -> c_11() , 12: if^#(false(), b, x, y) -> c_12() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) , minus^#(s(x), s(y)) -> c_6(minus^#(x, y)) , div^#(x, y) -> c_9(if^#(ge(y, s(0())), ge(x, y), x, y), ge^#(y, s(0())), ge^#(x, y)) , if^#(true(), true(), x, y) -> c_10(id_inc^#(div(minus(x, y), y)), div^#(minus(x, y), y), minus^#(x, y)) } Weak DPs: { ge^#(x, 0()) -> c_1() , ge^#(0(), s(y)) -> c_2() , minus^#(x, 0()) -> c_4() , minus^#(0(), y) -> c_5() , id_inc^#(x) -> c_7() , id_inc^#(x) -> c_8() , if^#(true(), false(), x, y) -> c_11() , if^#(false(), b, x, y) -> c_12() } Weak Trs: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , id_inc(x) -> x , id_inc(x) -> s(x) , div(x, y) -> if(ge(y, s(0())), ge(x, y), x, y) , if(true(), true(), x, y) -> id_inc(div(minus(x, y), y)) , if(true(), false(), x, y) -> 0() , if(false(), b, x, y) -> div_by_zero() } 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. { ge^#(x, 0()) -> c_1() , ge^#(0(), s(y)) -> c_2() , minus^#(x, 0()) -> c_4() , minus^#(0(), y) -> c_5() , id_inc^#(x) -> c_7() , id_inc^#(x) -> c_8() , if^#(true(), false(), x, y) -> c_11() , if^#(false(), b, x, y) -> c_12() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(s(x), s(y)) -> c_3(ge^#(x, y)) , minus^#(s(x), s(y)) -> c_6(minus^#(x, y)) , div^#(x, y) -> c_9(if^#(ge(y, s(0())), ge(x, y), x, y), ge^#(y, s(0())), ge^#(x, y)) , if^#(true(), true(), x, y) -> c_10(id_inc^#(div(minus(x, y), y)), div^#(minus(x, y), y), minus^#(x, y)) } Weak Trs: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , id_inc(x) -> x , id_inc(x) -> s(x) , div(x, y) -> if(ge(y, s(0())), ge(x, y), x, y) , if(true(), true(), x, y) -> id_inc(div(minus(x, y), y)) , if(true(), false(), x, y) -> 0() , if(false(), b, x, y) -> div_by_zero() } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { if^#(true(), true(), x, y) -> c_10(id_inc^#(div(minus(x, y), y)), div^#(minus(x, y), y), minus^#(x, y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(s(x), s(y)) -> c_1(ge^#(x, y)) , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , div^#(x, y) -> c_3(if^#(ge(y, s(0())), ge(x, y), x, y), ge^#(y, s(0())), ge^#(x, y)) , if^#(true(), true(), x, y) -> c_4(div^#(minus(x, y), y), minus^#(x, y)) } Weak Trs: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) , id_inc(x) -> x , id_inc(x) -> s(x) , div(x, y) -> if(ge(y, s(0())), ge(x, y), x, y) , if(true(), true(), x, y) -> id_inc(div(minus(x, y), y)) , if(true(), false(), x, y) -> 0() , if(false(), b, x, y) -> div_by_zero() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { ge^#(s(x), s(y)) -> c_1(ge^#(x, y)) , minus^#(s(x), s(y)) -> c_2(minus^#(x, y)) , div^#(x, y) -> c_3(if^#(ge(y, s(0())), ge(x, y), x, y), ge^#(y, s(0())), ge^#(x, y)) , if^#(true(), true(), x, y) -> c_4(div^#(minus(x, y), y), minus^#(x, y)) } Weak Trs: { ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , minus(x, 0()) -> x , minus(0(), y) -> 0() , minus(s(x), s(y)) -> minus(x, y) } 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..