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