MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s(z)) , f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s(y), z) , gt(s(u), s(v)) -> gt(u, v) , gt(s(u), 0()) -> true() , gt(0(), v) -> false() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { f^#(true(), x, y, z) -> c_1(f^#(gt(x, plus(y, z)), x, y, s(z)), gt^#(x, plus(y, z)), plus^#(y, z)) , f^#(true(), x, y, z) -> c_2(f^#(gt(x, plus(y, z)), x, s(y), z), gt^#(x, plus(y, z)), plus^#(y, z)) , gt^#(s(u), s(v)) -> c_3(gt^#(u, v)) , gt^#(s(u), 0()) -> c_4() , gt^#(0(), v) -> c_5() , plus^#(n, s(m)) -> c_6(plus^#(n, m)) , plus^#(n, 0()) -> c_7() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f^#(true(), x, y, z) -> c_1(f^#(gt(x, plus(y, z)), x, y, s(z)), gt^#(x, plus(y, z)), plus^#(y, z)) , f^#(true(), x, y, z) -> c_2(f^#(gt(x, plus(y, z)), x, s(y), z), gt^#(x, plus(y, z)), plus^#(y, z)) , gt^#(s(u), s(v)) -> c_3(gt^#(u, v)) , gt^#(s(u), 0()) -> c_4() , gt^#(0(), v) -> c_5() , plus^#(n, s(m)) -> c_6(plus^#(n, m)) , plus^#(n, 0()) -> c_7() } Weak Trs: { f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s(z)) , f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s(y), z) , gt(s(u), s(v)) -> gt(u, v) , gt(s(u), 0()) -> true() , gt(0(), v) -> false() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4,5,7} by applications of Pre({4,5,7}) = {1,2,3,6}. Here rules are labeled as follows: DPs: { 1: f^#(true(), x, y, z) -> c_1(f^#(gt(x, plus(y, z)), x, y, s(z)), gt^#(x, plus(y, z)), plus^#(y, z)) , 2: f^#(true(), x, y, z) -> c_2(f^#(gt(x, plus(y, z)), x, s(y), z), gt^#(x, plus(y, z)), plus^#(y, z)) , 3: gt^#(s(u), s(v)) -> c_3(gt^#(u, v)) , 4: gt^#(s(u), 0()) -> c_4() , 5: gt^#(0(), v) -> c_5() , 6: plus^#(n, s(m)) -> c_6(plus^#(n, m)) , 7: plus^#(n, 0()) -> c_7() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f^#(true(), x, y, z) -> c_1(f^#(gt(x, plus(y, z)), x, y, s(z)), gt^#(x, plus(y, z)), plus^#(y, z)) , f^#(true(), x, y, z) -> c_2(f^#(gt(x, plus(y, z)), x, s(y), z), gt^#(x, plus(y, z)), plus^#(y, z)) , gt^#(s(u), s(v)) -> c_3(gt^#(u, v)) , plus^#(n, s(m)) -> c_6(plus^#(n, m)) } Weak DPs: { gt^#(s(u), 0()) -> c_4() , gt^#(0(), v) -> c_5() , plus^#(n, 0()) -> c_7() } Weak Trs: { f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s(z)) , f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s(y), z) , gt(s(u), s(v)) -> gt(u, v) , gt(s(u), 0()) -> true() , gt(0(), v) -> false() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } 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. { gt^#(s(u), 0()) -> c_4() , gt^#(0(), v) -> c_5() , plus^#(n, 0()) -> c_7() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f^#(true(), x, y, z) -> c_1(f^#(gt(x, plus(y, z)), x, y, s(z)), gt^#(x, plus(y, z)), plus^#(y, z)) , f^#(true(), x, y, z) -> c_2(f^#(gt(x, plus(y, z)), x, s(y), z), gt^#(x, plus(y, z)), plus^#(y, z)) , gt^#(s(u), s(v)) -> c_3(gt^#(u, v)) , plus^#(n, s(m)) -> c_6(plus^#(n, m)) } Weak Trs: { f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s(z)) , f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s(y), z) , gt(s(u), s(v)) -> gt(u, v) , gt(s(u), 0()) -> true() , gt(0(), v) -> false() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { gt(s(u), s(v)) -> gt(u, v) , gt(s(u), 0()) -> true() , gt(0(), v) -> false() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { f^#(true(), x, y, z) -> c_1(f^#(gt(x, plus(y, z)), x, y, s(z)), gt^#(x, plus(y, z)), plus^#(y, z)) , f^#(true(), x, y, z) -> c_2(f^#(gt(x, plus(y, z)), x, s(y), z), gt^#(x, plus(y, z)), plus^#(y, z)) , gt^#(s(u), s(v)) -> c_3(gt^#(u, v)) , plus^#(n, s(m)) -> c_6(plus^#(n, m)) } Weak Trs: { gt(s(u), s(v)) -> gt(u, v) , gt(s(u), 0()) -> true() , gt(0(), v) -> false() , plus(n, s(m)) -> s(plus(n, m)) , plus(n, 0()) -> n } 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..