MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { incr(X) -> n__incr(X) , incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__adx(X)) -> adx(activate(X)) , activate(n__zeros()) -> zeros() , adx(X) -> n__adx(X) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))) , nats() -> adx(zeros()) , zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , head(cons(X, L)) -> X , tail(cons(X, L)) -> activate(L) } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { incr^#(X) -> c_1() , incr^#(nil()) -> c_2() , incr^#(cons(X, L)) -> c_3(activate^#(L)) , activate^#(X) -> c_4() , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X)) , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X)) , activate^#(n__zeros()) -> c_7(zeros^#()) , adx^#(X) -> c_8() , adx^#(nil()) -> c_9() , adx^#(cons(X, L)) -> c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , zeros^#() -> c_12() , zeros^#() -> c_13() , nats^#() -> c_11(adx^#(zeros()), zeros^#()) , head^#(cons(X, L)) -> c_14() , tail^#(cons(X, L)) -> c_15(activate^#(L)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(X) -> c_1() , incr^#(nil()) -> c_2() , incr^#(cons(X, L)) -> c_3(activate^#(L)) , activate^#(X) -> c_4() , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X)) , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X)) , activate^#(n__zeros()) -> c_7(zeros^#()) , adx^#(X) -> c_8() , adx^#(nil()) -> c_9() , adx^#(cons(X, L)) -> c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , zeros^#() -> c_12() , zeros^#() -> c_13() , nats^#() -> c_11(adx^#(zeros()), zeros^#()) , head^#(cons(X, L)) -> c_14() , tail^#(cons(X, L)) -> c_15(activate^#(L)) } Weak Trs: { incr(X) -> n__incr(X) , incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__adx(X)) -> adx(activate(X)) , activate(n__zeros()) -> zeros() , adx(X) -> n__adx(X) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))) , nats() -> adx(zeros()) , zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , head(cons(X, L)) -> X , tail(cons(X, L)) -> activate(L) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,4,8,9,11,12,14} by applications of Pre({1,2,4,8,9,11,12,14}) = {3,5,6,7,10,13,15}. Here rules are labeled as follows: DPs: { 1: incr^#(X) -> c_1() , 2: incr^#(nil()) -> c_2() , 3: incr^#(cons(X, L)) -> c_3(activate^#(L)) , 4: activate^#(X) -> c_4() , 5: activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X)) , 6: activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X)) , 7: activate^#(n__zeros()) -> c_7(zeros^#()) , 8: adx^#(X) -> c_8() , 9: adx^#(nil()) -> c_9() , 10: adx^#(cons(X, L)) -> c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , 11: zeros^#() -> c_12() , 12: zeros^#() -> c_13() , 13: nats^#() -> c_11(adx^#(zeros()), zeros^#()) , 14: head^#(cons(X, L)) -> c_14() , 15: tail^#(cons(X, L)) -> c_15(activate^#(L)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_3(activate^#(L)) , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X)) , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X)) , activate^#(n__zeros()) -> c_7(zeros^#()) , adx^#(cons(X, L)) -> c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , nats^#() -> c_11(adx^#(zeros()), zeros^#()) , tail^#(cons(X, L)) -> c_15(activate^#(L)) } Weak DPs: { incr^#(X) -> c_1() , incr^#(nil()) -> c_2() , activate^#(X) -> c_4() , adx^#(X) -> c_8() , adx^#(nil()) -> c_9() , zeros^#() -> c_12() , zeros^#() -> c_13() , head^#(cons(X, L)) -> c_14() } Weak Trs: { incr(X) -> n__incr(X) , incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__adx(X)) -> adx(activate(X)) , activate(n__zeros()) -> zeros() , adx(X) -> n__adx(X) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))) , nats() -> adx(zeros()) , zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , head(cons(X, L)) -> X , tail(cons(X, L)) -> activate(L) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4} by applications of Pre({4}) = {1,2,3,5,7}. Here rules are labeled as follows: DPs: { 1: incr^#(cons(X, L)) -> c_3(activate^#(L)) , 2: activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X)) , 3: activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X)) , 4: activate^#(n__zeros()) -> c_7(zeros^#()) , 5: adx^#(cons(X, L)) -> c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , 6: nats^#() -> c_11(adx^#(zeros()), zeros^#()) , 7: tail^#(cons(X, L)) -> c_15(activate^#(L)) , 8: incr^#(X) -> c_1() , 9: incr^#(nil()) -> c_2() , 10: activate^#(X) -> c_4() , 11: adx^#(X) -> c_8() , 12: adx^#(nil()) -> c_9() , 13: zeros^#() -> c_12() , 14: zeros^#() -> c_13() , 15: head^#(cons(X, L)) -> c_14() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_3(activate^#(L)) , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X)) , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X)) , adx^#(cons(X, L)) -> c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , nats^#() -> c_11(adx^#(zeros()), zeros^#()) , tail^#(cons(X, L)) -> c_15(activate^#(L)) } Weak DPs: { incr^#(X) -> c_1() , incr^#(nil()) -> c_2() , activate^#(X) -> c_4() , activate^#(n__zeros()) -> c_7(zeros^#()) , adx^#(X) -> c_8() , adx^#(nil()) -> c_9() , zeros^#() -> c_12() , zeros^#() -> c_13() , head^#(cons(X, L)) -> c_14() } Weak Trs: { incr(X) -> n__incr(X) , incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__adx(X)) -> adx(activate(X)) , activate(n__zeros()) -> zeros() , adx(X) -> n__adx(X) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))) , nats() -> adx(zeros()) , zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , head(cons(X, L)) -> X , tail(cons(X, L)) -> activate(L) } 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. { incr^#(X) -> c_1() , incr^#(nil()) -> c_2() , activate^#(X) -> c_4() , activate^#(n__zeros()) -> c_7(zeros^#()) , adx^#(X) -> c_8() , adx^#(nil()) -> c_9() , zeros^#() -> c_12() , zeros^#() -> c_13() , head^#(cons(X, L)) -> c_14() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_3(activate^#(L)) , activate^#(n__incr(X)) -> c_5(incr^#(activate(X)), activate^#(X)) , activate^#(n__adx(X)) -> c_6(adx^#(activate(X)), activate^#(X)) , adx^#(cons(X, L)) -> c_10(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , nats^#() -> c_11(adx^#(zeros()), zeros^#()) , tail^#(cons(X, L)) -> c_15(activate^#(L)) } Weak Trs: { incr(X) -> n__incr(X) , incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__adx(X)) -> adx(activate(X)) , activate(n__zeros()) -> zeros() , adx(X) -> n__adx(X) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))) , nats() -> adx(zeros()) , zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , head(cons(X, L)) -> X , tail(cons(X, L)) -> activate(L) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { nats^#() -> c_11(adx^#(zeros()), zeros^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_1(activate^#(L)) , activate^#(n__incr(X)) -> c_2(incr^#(activate(X)), activate^#(X)) , activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , nats^#() -> c_5(adx^#(zeros())) , tail^#(cons(X, L)) -> c_6(activate^#(L)) } Weak Trs: { incr(X) -> n__incr(X) , incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__adx(X)) -> adx(activate(X)) , activate(n__zeros()) -> zeros() , adx(X) -> n__adx(X) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))) , nats() -> adx(zeros()) , zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , head(cons(X, L)) -> X , tail(cons(X, L)) -> activate(L) } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { incr(X) -> n__incr(X) , incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__adx(X)) -> adx(activate(X)) , activate(n__zeros()) -> zeros() , adx(X) -> n__adx(X) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))) , zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_1(activate^#(L)) , activate^#(n__incr(X)) -> c_2(incr^#(activate(X)), activate^#(X)) , activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , nats^#() -> c_5(adx^#(zeros())) , tail^#(cons(X, L)) -> c_6(activate^#(L)) } Weak Trs: { incr(X) -> n__incr(X) , incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__adx(X)) -> adx(activate(X)) , activate(n__zeros()) -> zeros() , adx(X) -> n__adx(X) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))) , zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: incr^#(cons(X, L)) -> c_1(activate^#(L)) -->_1 activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X)) :3 -->_1 activate^#(n__incr(X)) -> c_2(incr^#(activate(X)), activate^#(X)) :2 2: activate^#(n__incr(X)) -> c_2(incr^#(activate(X)), activate^#(X)) -->_2 activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X)) :3 -->_2 activate^#(n__incr(X)) -> c_2(incr^#(activate(X)), activate^#(X)) :2 -->_1 incr^#(cons(X, L)) -> c_1(activate^#(L)) :1 3: activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X)) -->_1 adx^#(cons(X, L)) -> c_4(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) :4 -->_2 activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X)) :3 -->_2 activate^#(n__incr(X)) -> c_2(incr^#(activate(X)), activate^#(X)) :2 4: adx^#(cons(X, L)) -> c_4(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) -->_2 activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X)) :3 -->_2 activate^#(n__incr(X)) -> c_2(incr^#(activate(X)), activate^#(X)) :2 -->_1 incr^#(cons(X, L)) -> c_1(activate^#(L)) :1 5: nats^#() -> c_5(adx^#(zeros())) -->_1 adx^#(cons(X, L)) -> c_4(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) :4 6: tail^#(cons(X, L)) -> c_6(activate^#(L)) -->_1 activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X)) :3 -->_1 activate^#(n__incr(X)) -> c_2(incr^#(activate(X)), activate^#(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). { tail^#(cons(X, L)) -> c_6(activate^#(L)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { incr^#(cons(X, L)) -> c_1(activate^#(L)) , activate^#(n__incr(X)) -> c_2(incr^#(activate(X)), activate^#(X)) , activate^#(n__adx(X)) -> c_3(adx^#(activate(X)), activate^#(X)) , adx^#(cons(X, L)) -> c_4(incr^#(cons(X, n__adx(activate(L)))), activate^#(L)) , nats^#() -> c_5(adx^#(zeros())) } Weak Trs: { incr(X) -> n__incr(X) , incr(nil()) -> nil() , incr(cons(X, L)) -> cons(s(X), n__incr(activate(L))) , activate(X) -> X , activate(n__incr(X)) -> incr(activate(X)) , activate(n__adx(X)) -> adx(activate(X)) , activate(n__zeros()) -> zeros() , adx(X) -> n__adx(X) , adx(nil()) -> nil() , adx(cons(X, L)) -> incr(cons(X, n__adx(activate(L)))) , zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() } 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..