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