MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() g(X) -> h(activate(X)) h(n__d()) -> g(n__c()) - Signature: {activate/1,c/0,d/0,g/1,h/1} / {n__c/0,n__d/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate,c,d,g,h} and constructors {n__c,n__d} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs activate#(X) -> c_1() activate#(n__c()) -> c_2(c#()) activate#(n__d()) -> c_3(d#()) c#() -> c_4(d#()) c#() -> c_5() d#() -> c_6() g#(X) -> c_7(h#(activate(X)),activate#(X)) h#(n__d()) -> c_8(g#(n__c())) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__c()) -> c_2(c#()) activate#(n__d()) -> c_3(d#()) c#() -> c_4(d#()) c#() -> c_5() d#() -> c_6() g#(X) -> c_7(h#(activate(X)),activate#(X)) h#(n__d()) -> c_8(g#(n__c())) - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() g(X) -> h(activate(X)) h(n__d()) -> g(n__c()) - Signature: {activate/1,c/0,d/0,g/1,h/1,activate#/1,c#/0,d#/0,g#/1,h#/1} / {n__c/0,n__d/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0 ,c_6/0,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,d#,g#,h#} and constructors {n__c,n__d} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() activate#(X) -> c_1() activate#(n__c()) -> c_2(c#()) activate#(n__d()) -> c_3(d#()) c#() -> c_4(d#()) c#() -> c_5() d#() -> c_6() g#(X) -> c_7(h#(activate(X)),activate#(X)) h#(n__d()) -> c_8(g#(n__c())) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__c()) -> c_2(c#()) activate#(n__d()) -> c_3(d#()) c#() -> c_4(d#()) c#() -> c_5() d#() -> c_6() g#(X) -> c_7(h#(activate(X)),activate#(X)) h#(n__d()) -> c_8(g#(n__c())) - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() - Signature: {activate/1,c/0,d/0,g/1,h/1,activate#/1,c#/0,d#/0,g#/1,h#/1} / {n__c/0,n__d/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0 ,c_6/0,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,d#,g#,h#} and constructors {n__c,n__d} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,5,6} by application of Pre({1,5,6}) = {2,3,4,7}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__c()) -> c_2(c#()) 3: activate#(n__d()) -> c_3(d#()) 4: c#() -> c_4(d#()) 5: c#() -> c_5() 6: d#() -> c_6() 7: g#(X) -> c_7(h#(activate(X)),activate#(X)) 8: h#(n__d()) -> c_8(g#(n__c())) * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__c()) -> c_2(c#()) activate#(n__d()) -> c_3(d#()) c#() -> c_4(d#()) g#(X) -> c_7(h#(activate(X)),activate#(X)) h#(n__d()) -> c_8(g#(n__c())) - Weak DPs: activate#(X) -> c_1() c#() -> c_5() d#() -> c_6() - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() - Signature: {activate/1,c/0,d/0,g/1,h/1,activate#/1,c#/0,d#/0,g#/1,h#/1} / {n__c/0,n__d/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0 ,c_6/0,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,d#,g#,h#} and constructors {n__c,n__d} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3} by application of Pre({2,3}) = {1,4}. Here rules are labelled as follows: 1: activate#(n__c()) -> c_2(c#()) 2: activate#(n__d()) -> c_3(d#()) 3: c#() -> c_4(d#()) 4: g#(X) -> c_7(h#(activate(X)),activate#(X)) 5: h#(n__d()) -> c_8(g#(n__c())) 6: activate#(X) -> c_1() 7: c#() -> c_5() 8: d#() -> c_6() * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__c()) -> c_2(c#()) g#(X) -> c_7(h#(activate(X)),activate#(X)) h#(n__d()) -> c_8(g#(n__c())) - Weak DPs: activate#(X) -> c_1() activate#(n__d()) -> c_3(d#()) c#() -> c_4(d#()) c#() -> c_5() d#() -> c_6() - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() - Signature: {activate/1,c/0,d/0,g/1,h/1,activate#/1,c#/0,d#/0,g#/1,h#/1} / {n__c/0,n__d/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0 ,c_6/0,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,d#,g#,h#} and constructors {n__c,n__d} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {2}. Here rules are labelled as follows: 1: activate#(n__c()) -> c_2(c#()) 2: g#(X) -> c_7(h#(activate(X)),activate#(X)) 3: h#(n__d()) -> c_8(g#(n__c())) 4: activate#(X) -> c_1() 5: activate#(n__d()) -> c_3(d#()) 6: c#() -> c_4(d#()) 7: c#() -> c_5() 8: d#() -> c_6() * Step 6: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: g#(X) -> c_7(h#(activate(X)),activate#(X)) h#(n__d()) -> c_8(g#(n__c())) - Weak DPs: activate#(X) -> c_1() activate#(n__c()) -> c_2(c#()) activate#(n__d()) -> c_3(d#()) c#() -> c_4(d#()) c#() -> c_5() d#() -> c_6() - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() - Signature: {activate/1,c/0,d/0,g/1,h/1,activate#/1,c#/0,d#/0,g#/1,h#/1} / {n__c/0,n__d/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0 ,c_6/0,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,d#,g#,h#} and constructors {n__c,n__d} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:g#(X) -> c_7(h#(activate(X)),activate#(X)) -->_2 activate#(n__d()) -> c_3(d#()):5 -->_2 activate#(n__c()) -> c_2(c#()):4 -->_1 h#(n__d()) -> c_8(g#(n__c())):2 -->_2 activate#(X) -> c_1():3 2:S:h#(n__d()) -> c_8(g#(n__c())) -->_1 g#(X) -> c_7(h#(activate(X)),activate#(X)):1 3:W:activate#(X) -> c_1() 4:W:activate#(n__c()) -> c_2(c#()) -->_1 c#() -> c_4(d#()):6 -->_1 c#() -> c_5():7 5:W:activate#(n__d()) -> c_3(d#()) -->_1 d#() -> c_6():8 6:W:c#() -> c_4(d#()) -->_1 d#() -> c_6():8 7:W:c#() -> c_5() 8:W:d#() -> c_6() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: activate#(X) -> c_1() 4: activate#(n__c()) -> c_2(c#()) 7: c#() -> c_5() 6: c#() -> c_4(d#()) 5: activate#(n__d()) -> c_3(d#()) 8: d#() -> c_6() * Step 7: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: g#(X) -> c_7(h#(activate(X)),activate#(X)) h#(n__d()) -> c_8(g#(n__c())) - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() - Signature: {activate/1,c/0,d/0,g/1,h/1,activate#/1,c#/0,d#/0,g#/1,h#/1} / {n__c/0,n__d/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0 ,c_6/0,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,d#,g#,h#} and constructors {n__c,n__d} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:g#(X) -> c_7(h#(activate(X)),activate#(X)) -->_1 h#(n__d()) -> c_8(g#(n__c())):2 2:S:h#(n__d()) -> c_8(g#(n__c())) -->_1 g#(X) -> c_7(h#(activate(X)),activate#(X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g#(X) -> c_7(h#(activate(X))) * Step 8: WeightGap MAYBE + Considered Problem: - Strict DPs: g#(X) -> c_7(h#(activate(X))) h#(n__d()) -> c_8(g#(n__c())) - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() - Signature: {activate/1,c/0,d/0,g/1,h/1,activate#/1,c#/0,d#/0,g#/1,h#/1} / {n__c/0,n__d/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0 ,c_6/0,c_7/1,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,d#,g#,h#} and constructors {n__c,n__d} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(h#) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(activate) = [9] x1 + [13] p(c) = [2] p(d) = [2] p(g) = [0] p(h) = [0] p(n__c) = [0] p(n__d) = [2] p(activate#) = [0] p(c#) = [0] p(d#) = [0] p(g#) = [9] x1 + [2] p(h#) = [1] x1 + [9] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [0] Following rules are strictly oriented: h#(n__d()) = [11] > [2] = c_8(g#(n__c())) Following rules are (at-least) weakly oriented: g#(X) = [9] X + [2] >= [9] X + [22] = c_7(h#(activate(X))) activate(X) = [9] X + [13] >= [1] X + [0] = X activate(n__c()) = [13] >= [2] = c() activate(n__d()) = [31] >= [2] = d() c() = [2] >= [2] = d() c() = [2] >= [0] = n__c() d() = [2] >= [2] = n__d() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 9: Failure MAYBE + Considered Problem: - Strict DPs: g#(X) -> c_7(h#(activate(X))) - Weak DPs: h#(n__d()) -> c_8(g#(n__c())) - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__d()) -> d() c() -> d() c() -> n__c() d() -> n__d() - Signature: {activate/1,c/0,d/0,g/1,h/1,activate#/1,c#/0,d#/0,g#/1,h#/1} / {n__c/0,n__d/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0 ,c_6/0,c_7/1,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,d#,g#,h#} and constructors {n__c,n__d} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE