MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { division(x, y) -> div(x, y, 0()) , div(x, y, z) -> if(lt(x, y), x, y, inc(z)) , if(true(), x, y, z) -> z , if(false(), x, s(y), z) -> div(minus(x, s(y)), s(y), z) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { division^#(x, y) -> c_1(div^#(x, y, 0())) , div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) , if^#(true(), x, y, z) -> c_3() , if^#(false(), x, s(y), z) -> c_4(div^#(minus(x, s(y)), s(y), z), minus^#(x, s(y))) , lt^#(x, 0()) -> c_5() , lt^#(0(), s(y)) -> c_6() , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , inc^#(0()) -> c_8() , inc^#(s(x)) -> c_9(inc^#(x)) , minus^#(x, 0()) -> c_10() , minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { division^#(x, y) -> c_1(div^#(x, y, 0())) , div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) , if^#(true(), x, y, z) -> c_3() , if^#(false(), x, s(y), z) -> c_4(div^#(minus(x, s(y)), s(y), z), minus^#(x, s(y))) , lt^#(x, 0()) -> c_5() , lt^#(0(), s(y)) -> c_6() , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , inc^#(0()) -> c_8() , inc^#(s(x)) -> c_9(inc^#(x)) , minus^#(x, 0()) -> c_10() , minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) } Weak Trs: { division(x, y) -> div(x, y, 0()) , div(x, y, z) -> if(lt(x, y), x, y, inc(z)) , if(true(), x, y, z) -> z , if(false(), x, s(y), z) -> div(minus(x, s(y)), s(y), z) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,5,6,8,10} by applications of Pre({3,5,6,8,10}) = {2,7,9,11}. Here rules are labeled as follows: DPs: { 1: division^#(x, y) -> c_1(div^#(x, y, 0())) , 2: div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) , 3: if^#(true(), x, y, z) -> c_3() , 4: if^#(false(), x, s(y), z) -> c_4(div^#(minus(x, s(y)), s(y), z), minus^#(x, s(y))) , 5: lt^#(x, 0()) -> c_5() , 6: lt^#(0(), s(y)) -> c_6() , 7: lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , 8: inc^#(0()) -> c_8() , 9: inc^#(s(x)) -> c_9(inc^#(x)) , 10: minus^#(x, 0()) -> c_10() , 11: minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { division^#(x, y) -> c_1(div^#(x, y, 0())) , div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) , if^#(false(), x, s(y), z) -> c_4(div^#(minus(x, s(y)), s(y), z), minus^#(x, s(y))) , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , inc^#(s(x)) -> c_9(inc^#(x)) , minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) } Weak DPs: { if^#(true(), x, y, z) -> c_3() , lt^#(x, 0()) -> c_5() , lt^#(0(), s(y)) -> c_6() , inc^#(0()) -> c_8() , minus^#(x, 0()) -> c_10() } Weak Trs: { division(x, y) -> div(x, y, 0()) , div(x, y, z) -> if(lt(x, y), x, y, inc(z)) , if(true(), x, y, z) -> z , if(false(), x, s(y), z) -> div(minus(x, s(y)), s(y), z) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) } 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_3() , lt^#(x, 0()) -> c_5() , lt^#(0(), s(y)) -> c_6() , inc^#(0()) -> c_8() , minus^#(x, 0()) -> c_10() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { division^#(x, y) -> c_1(div^#(x, y, 0())) , div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) , if^#(false(), x, s(y), z) -> c_4(div^#(minus(x, s(y)), s(y), z), minus^#(x, s(y))) , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , inc^#(s(x)) -> c_9(inc^#(x)) , minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) } Weak Trs: { division(x, y) -> div(x, y, 0()) , div(x, y, z) -> if(lt(x, y), x, y, inc(z)) , if(true(), x, y, z) -> z , if(false(), x, s(y), z) -> div(minus(x, s(y)), s(y), z) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: division^#(x, y) -> c_1(div^#(x, y, 0())) -->_1 div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) :2 2: div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) -->_3 inc^#(s(x)) -> c_9(inc^#(x)) :5 -->_2 lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) :4 -->_1 if^#(false(), x, s(y), z) -> c_4(div^#(minus(x, s(y)), s(y), z), minus^#(x, s(y))) :3 3: if^#(false(), x, s(y), z) -> c_4(div^#(minus(x, s(y)), s(y), z), minus^#(x, s(y))) -->_2 minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) :6 -->_1 div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) :2 4: lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) -->_1 lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) :4 5: inc^#(s(x)) -> c_9(inc^#(x)) -->_1 inc^#(s(x)) -> c_9(inc^#(x)) :5 6: minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) -->_1 minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) :6 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). { division^#(x, y) -> c_1(div^#(x, y, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) , if^#(false(), x, s(y), z) -> c_4(div^#(minus(x, s(y)), s(y), z), minus^#(x, s(y))) , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , inc^#(s(x)) -> c_9(inc^#(x)) , minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) } Weak Trs: { division(x, y) -> div(x, y, 0()) , div(x, y, z) -> if(lt(x, y), x, y, inc(z)) , if(true(), x, y, z) -> z , if(false(), x, s(y), z) -> div(minus(x, s(y)), s(y), z) , lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , minus(x, 0()) -> x , minus(s(x), s(y)) -> minus(x, y) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { div^#(x, y, z) -> c_2(if^#(lt(x, y), x, y, inc(z)), lt^#(x, y), inc^#(z)) , if^#(false(), x, s(y), z) -> c_4(div^#(minus(x, s(y)), s(y), z), minus^#(x, s(y))) , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) , inc^#(s(x)) -> c_9(inc^#(x)) , minus^#(s(x), s(y)) -> c_11(minus^#(x, y)) } Weak Trs: { lt(x, 0()) -> false() , lt(0(), s(y)) -> true() , lt(s(x), s(y)) -> lt(x, y) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , minus(x, 0()) -> x , 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..