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