MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { g(X) -> h(activate(X)) , h(n__d()) -> g(n__c()) , activate(X) -> X , activate(n__d()) -> d() , activate(n__c()) -> c() , c() -> d() , c() -> n__c() , d() -> n__d() } Obligation: innermost runtime complexity Answer: MAYBE We add following weak dependency pairs: Strict DPs: { g^#(X) -> c_1(h^#(activate(X))) , h^#(n__d()) -> c_2(g^#(n__c())) , activate^#(X) -> c_3() , activate^#(n__d()) -> c_4(d^#()) , activate^#(n__c()) -> c_5(c^#()) , d^#() -> c_8() , c^#() -> c_6(d^#()) , c^#() -> c_7() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { g^#(X) -> c_1(h^#(activate(X))) , h^#(n__d()) -> c_2(g^#(n__c())) , activate^#(X) -> c_3() , activate^#(n__d()) -> c_4(d^#()) , activate^#(n__c()) -> c_5(c^#()) , d^#() -> c_8() , c^#() -> c_6(d^#()) , c^#() -> c_7() } Strict Trs: { g(X) -> h(activate(X)) , h(n__d()) -> g(n__c()) , activate(X) -> X , activate(n__d()) -> d() , activate(n__c()) -> c() , c() -> d() , c() -> n__c() , d() -> n__d() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Strict Usable Rules: { activate(X) -> X , activate(n__d()) -> d() , activate(n__c()) -> c() , c() -> d() , c() -> n__c() , d() -> n__d() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { g^#(X) -> c_1(h^#(activate(X))) , h^#(n__d()) -> c_2(g^#(n__c())) , activate^#(X) -> c_3() , activate^#(n__d()) -> c_4(d^#()) , activate^#(n__c()) -> c_5(c^#()) , d^#() -> c_8() , c^#() -> c_6(d^#()) , c^#() -> c_7() } Strict Trs: { activate(X) -> X , activate(n__d()) -> d() , activate(n__c()) -> c() , c() -> d() , c() -> n__c() , d() -> n__d() } Obligation: innermost runtime complexity Answer: MAYBE The weightgap principle applies (using the following constant growth matrix-interpretation) The following argument positions are usable: Uargs(c_1) = {1}, Uargs(h^#) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_6) = {1} TcT has computed following constructor-restricted matrix interpretation. [activate](x1) = [1] x1 + [2] [c] = [2] [d] = [1] [n__d] = [0] [n__c] = [1] [g^#](x1) = [2] x1 + [2] [c_1](x1) = [1] x1 + [0] [h^#](x1) = [1] x1 + [1] [c_2](x1) = [1] x1 + [2] [activate^#](x1) = [1] x1 + [2] [c_3] = [1] [c_4](x1) = [1] x1 + [1] [d^#] = [1] [c_5](x1) = [1] x1 + [2] [c^#] = [1] [c_6](x1) = [1] x1 + [2] [c_7] = [0] [c_8] = [0] This order satisfies following ordering constraints: [activate(X)] = [1] X + [2] > [1] X + [0] = [X] [activate(n__d())] = [2] > [1] = [d()] [activate(n__c())] = [3] > [2] = [c()] [c()] = [2] > [1] = [d()] [c()] = [2] > [1] = [n__c()] [d()] = [1] > [0] = [n__d()] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { g^#(X) -> c_1(h^#(activate(X))) , h^#(n__d()) -> c_2(g^#(n__c())) , activate^#(n__d()) -> c_4(d^#()) , activate^#(n__c()) -> c_5(c^#()) , c^#() -> c_6(d^#()) } Weak DPs: { activate^#(X) -> c_3() , d^#() -> c_8() , c^#() -> c_7() } Weak Trs: { activate(X) -> X , activate(n__d()) -> d() , activate(n__c()) -> c() , c() -> d() , c() -> n__c() , d() -> n__d() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3,5} by applications of Pre({3,5}) = {4}. Here rules are labeled as follows: DPs: { 1: g^#(X) -> c_1(h^#(activate(X))) , 2: h^#(n__d()) -> c_2(g^#(n__c())) , 3: activate^#(n__d()) -> c_4(d^#()) , 4: activate^#(n__c()) -> c_5(c^#()) , 5: c^#() -> c_6(d^#()) , 6: activate^#(X) -> c_3() , 7: d^#() -> c_8() , 8: c^#() -> c_7() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { g^#(X) -> c_1(h^#(activate(X))) , h^#(n__d()) -> c_2(g^#(n__c())) , activate^#(n__c()) -> c_5(c^#()) } Weak DPs: { activate^#(X) -> c_3() , activate^#(n__d()) -> c_4(d^#()) , d^#() -> c_8() , c^#() -> c_6(d^#()) , c^#() -> c_7() } Weak Trs: { activate(X) -> X , activate(n__d()) -> d() , activate(n__c()) -> c() , c() -> d() , c() -> n__c() , d() -> n__d() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {3} by applications of Pre({3}) = {}. Here rules are labeled as follows: DPs: { 1: g^#(X) -> c_1(h^#(activate(X))) , 2: h^#(n__d()) -> c_2(g^#(n__c())) , 3: activate^#(n__c()) -> c_5(c^#()) , 4: activate^#(X) -> c_3() , 5: activate^#(n__d()) -> c_4(d^#()) , 6: d^#() -> c_8() , 7: c^#() -> c_6(d^#()) , 8: c^#() -> c_7() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { g^#(X) -> c_1(h^#(activate(X))) , h^#(n__d()) -> c_2(g^#(n__c())) } Weak DPs: { activate^#(X) -> c_3() , activate^#(n__d()) -> c_4(d^#()) , activate^#(n__c()) -> c_5(c^#()) , d^#() -> c_8() , c^#() -> c_6(d^#()) , c^#() -> c_7() } Weak Trs: { activate(X) -> X , activate(n__d()) -> d() , activate(n__c()) -> c() , c() -> d() , c() -> n__c() , d() -> n__d() } 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() , activate^#(n__d()) -> c_4(d^#()) , activate^#(n__c()) -> c_5(c^#()) , d^#() -> c_8() , c^#() -> c_6(d^#()) , c^#() -> c_7() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { g^#(X) -> c_1(h^#(activate(X))) , h^#(n__d()) -> c_2(g^#(n__c())) } Weak Trs: { activate(X) -> X , activate(n__d()) -> d() , activate(n__c()) -> c() , c() -> d() , c() -> n__c() , d() -> n__d() } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..