MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { fact(X) -> if(zero(X), s(0()), prod(X, fact(p(X)))) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y , zero(s(X)) -> false() , zero(0()) -> true() , prod(s(X), Y) -> add(Y, prod(X, Y)) , prod(0(), X) -> 0() , p(s(X)) -> X , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { fact^#(X) -> c_1(if^#(zero(X), s(0()), prod(X, fact(p(X)))), zero^#(X), prod^#(X, fact(p(X))), fact^#(p(X)), p^#(X)) , if^#(true(), X, Y) -> c_2() , if^#(false(), X, Y) -> c_3() , zero^#(s(X)) -> c_4() , zero^#(0()) -> c_5() , prod^#(s(X), Y) -> c_6(add^#(Y, prod(X, Y)), prod^#(X, Y)) , prod^#(0(), X) -> c_7() , p^#(s(X)) -> c_8() , add^#(s(X), Y) -> c_9(add^#(X, Y)) , add^#(0(), X) -> c_10() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fact^#(X) -> c_1(if^#(zero(X), s(0()), prod(X, fact(p(X)))), zero^#(X), prod^#(X, fact(p(X))), fact^#(p(X)), p^#(X)) , if^#(true(), X, Y) -> c_2() , if^#(false(), X, Y) -> c_3() , zero^#(s(X)) -> c_4() , zero^#(0()) -> c_5() , prod^#(s(X), Y) -> c_6(add^#(Y, prod(X, Y)), prod^#(X, Y)) , prod^#(0(), X) -> c_7() , p^#(s(X)) -> c_8() , add^#(s(X), Y) -> c_9(add^#(X, Y)) , add^#(0(), X) -> c_10() } Weak Trs: { fact(X) -> if(zero(X), s(0()), prod(X, fact(p(X)))) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y , zero(s(X)) -> false() , zero(0()) -> true() , prod(s(X), Y) -> add(Y, prod(X, Y)) , prod(0(), X) -> 0() , p(s(X)) -> X , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {2,3,4,5,7,8,10} by applications of Pre({2,3,4,5,7,8,10}) = {1,6,9}. Here rules are labeled as follows: DPs: { 1: fact^#(X) -> c_1(if^#(zero(X), s(0()), prod(X, fact(p(X)))), zero^#(X), prod^#(X, fact(p(X))), fact^#(p(X)), p^#(X)) , 2: if^#(true(), X, Y) -> c_2() , 3: if^#(false(), X, Y) -> c_3() , 4: zero^#(s(X)) -> c_4() , 5: zero^#(0()) -> c_5() , 6: prod^#(s(X), Y) -> c_6(add^#(Y, prod(X, Y)), prod^#(X, Y)) , 7: prod^#(0(), X) -> c_7() , 8: p^#(s(X)) -> c_8() , 9: add^#(s(X), Y) -> c_9(add^#(X, Y)) , 10: add^#(0(), X) -> c_10() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fact^#(X) -> c_1(if^#(zero(X), s(0()), prod(X, fact(p(X)))), zero^#(X), prod^#(X, fact(p(X))), fact^#(p(X)), p^#(X)) , prod^#(s(X), Y) -> c_6(add^#(Y, prod(X, Y)), prod^#(X, Y)) , add^#(s(X), Y) -> c_9(add^#(X, Y)) } Weak DPs: { if^#(true(), X, Y) -> c_2() , if^#(false(), X, Y) -> c_3() , zero^#(s(X)) -> c_4() , zero^#(0()) -> c_5() , prod^#(0(), X) -> c_7() , p^#(s(X)) -> c_8() , add^#(0(), X) -> c_10() } Weak Trs: { fact(X) -> if(zero(X), s(0()), prod(X, fact(p(X)))) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y , zero(s(X)) -> false() , zero(0()) -> true() , prod(s(X), Y) -> add(Y, prod(X, Y)) , prod(0(), X) -> 0() , p(s(X)) -> X , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } 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) -> c_2() , if^#(false(), X, Y) -> c_3() , zero^#(s(X)) -> c_4() , zero^#(0()) -> c_5() , prod^#(0(), X) -> c_7() , p^#(s(X)) -> c_8() , add^#(0(), X) -> c_10() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fact^#(X) -> c_1(if^#(zero(X), s(0()), prod(X, fact(p(X)))), zero^#(X), prod^#(X, fact(p(X))), fact^#(p(X)), p^#(X)) , prod^#(s(X), Y) -> c_6(add^#(Y, prod(X, Y)), prod^#(X, Y)) , add^#(s(X), Y) -> c_9(add^#(X, Y)) } Weak Trs: { fact(X) -> if(zero(X), s(0()), prod(X, fact(p(X)))) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y , zero(s(X)) -> false() , zero(0()) -> true() , prod(s(X), Y) -> add(Y, prod(X, Y)) , prod(0(), X) -> 0() , p(s(X)) -> X , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { fact^#(X) -> c_1(if^#(zero(X), s(0()), prod(X, fact(p(X)))), zero^#(X), prod^#(X, fact(p(X))), fact^#(p(X)), p^#(X)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { fact^#(X) -> c_1(prod^#(X, fact(p(X))), fact^#(p(X))) , prod^#(s(X), Y) -> c_2(add^#(Y, prod(X, Y)), prod^#(X, Y)) , add^#(s(X), Y) -> c_3(add^#(X, Y)) } Weak Trs: { fact(X) -> if(zero(X), s(0()), prod(X, fact(p(X)))) , if(true(), X, Y) -> X , if(false(), X, Y) -> Y , zero(s(X)) -> false() , zero(0()) -> true() , prod(s(X), Y) -> add(Y, prod(X, Y)) , prod(0(), X) -> 0() , p(s(X)) -> X , add(s(X), Y) -> s(add(X, Y)) , add(0(), X) -> X } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..