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)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(x, y)) , tower(x, y) -> towerIter(x, y, s(0())) , towerIter(0(), y, z) -> z , towerIter(s(x), y, z) -> towerIter(p(s(x)), y, exp(y, z)) } 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))) , exp^#(x, 0()) -> c_7() , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) , tower^#(x, y) -> c_9(towerIter^#(x, y, s(0()))) , towerIter^#(0(), y, z) -> c_10() , towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) } 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))) , exp^#(x, 0()) -> c_7() , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) , tower^#(x, y) -> c_9(towerIter^#(x, y, s(0()))) , towerIter^#(0(), y, z) -> c_10() , towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) } 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)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(x, y)) , tower(x, y) -> towerIter(x, y, s(0())) , towerIter(0(), y, z) -> z , towerIter(s(x), y, z) -> towerIter(p(s(x)), y, exp(y, z)) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,3,5,7,10} by applications of Pre({1,3,5,7,10}) = {2,4,6,8,9,11}. 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: exp^#(x, 0()) -> c_7() , 8: exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) , 9: tower^#(x, y) -> c_9(towerIter^#(x, y, s(0()))) , 10: towerIter^#(0(), y, z) -> c_10() , 11: towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) } 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))) , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) , tower^#(x, y) -> c_9(towerIter^#(x, y, s(0()))) , towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) } Weak DPs: { plus^#(0(), x) -> c_1() , p^#(s(0())) -> c_3() , times^#(0(), y) -> c_5() , exp^#(x, 0()) -> c_7() , towerIter^#(0(), y, z) -> c_10() } 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)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(x, y)) , tower(x, y) -> towerIter(x, y, s(0())) , towerIter(0(), y, z) -> z , towerIter(s(x), y, z) -> towerIter(p(s(x)), y, exp(y, 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. { plus^#(0(), x) -> c_1() , p^#(s(0())) -> c_3() , times^#(0(), y) -> c_5() , exp^#(x, 0()) -> c_7() , towerIter^#(0(), y, z) -> c_10() } 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))) , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) , tower^#(x, y) -> c_9(towerIter^#(x, y, s(0()))) , towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) } 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)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(x, y)) , tower(x, y) -> towerIter(x, y, s(0())) , towerIter(0(), y, z) -> z , towerIter(s(x), y, z) -> towerIter(p(s(x)), y, exp(y, z)) } 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: exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) -->_2 exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) :4 -->_1 times^#(s(x), y) -> c_6(plus^#(y, times(p(s(x)), y)), times^#(p(s(x)), y), p^#(s(x))) :3 5: tower^#(x, y) -> c_9(towerIter^#(x, y, s(0()))) -->_1 towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) :6 6: towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) -->_1 towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) :6 -->_3 exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) :4 -->_2 p^#(s(s(x))) -> c_4(p^#(s(x))) :2 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). { tower^#(x, y) -> c_9(towerIter^#(x, y, 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))) , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) , towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) } 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)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(x, y)) , tower(x, y) -> towerIter(x, y, s(0())) , towerIter(0(), y, z) -> z , towerIter(s(x), y, z) -> towerIter(p(s(x)), y, exp(y, z)) } 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)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(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))) , exp^#(x, s(y)) -> c_8(times^#(x, exp(x, y)), exp^#(x, y)) , towerIter^#(s(x), y, z) -> c_11(towerIter^#(p(s(x)), y, exp(y, z)), p^#(s(x)), exp^#(y, z)) } 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)) , exp(x, 0()) -> s(0()) , exp(x, s(y)) -> times(x, exp(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..