MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__c()) -> c() activate(n__g(X)) -> g(X) c() -> f(n__g(n__c())) c() -> n__c() f(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,c/0,f/1,g/1} / {n__c/0,n__g/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,c,f,g} and constructors {n__c,n__g} + 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__g(X)) -> c_3(g#(X)) c#() -> c_4(f#(n__g(n__c()))) c#() -> c_5() f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)) g#(X) -> c_7() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__c()) -> c_2(c#()) activate#(n__g(X)) -> c_3(g#(X)) c#() -> c_4(f#(n__g(n__c()))) c#() -> c_5() f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)) g#(X) -> c_7() - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__g(X)) -> g(X) c() -> f(n__g(n__c())) c() -> n__c() f(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,c/0,f/1,g/1,activate#/1,c#/0,f#/1,g#/1} / {n__c/0,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2 ,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,f#,g#} and constructors {n__c,n__g} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,5,7} by application of Pre({1,5,7}) = {2,3,6}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__c()) -> c_2(c#()) 3: activate#(n__g(X)) -> c_3(g#(X)) 4: c#() -> c_4(f#(n__g(n__c()))) 5: c#() -> c_5() 6: f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)) 7: g#(X) -> c_7() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__c()) -> c_2(c#()) activate#(n__g(X)) -> c_3(g#(X)) c#() -> c_4(f#(n__g(n__c()))) f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)) - Weak DPs: activate#(X) -> c_1() c#() -> c_5() g#(X) -> c_7() - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__g(X)) -> g(X) c() -> f(n__g(n__c())) c() -> n__c() f(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,c/0,f/1,g/1,activate#/1,c#/0,f#/1,g#/1} / {n__c/0,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2 ,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,f#,g#} and constructors {n__c,n__g} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2} by application of Pre({2}) = {4}. Here rules are labelled as follows: 1: activate#(n__c()) -> c_2(c#()) 2: activate#(n__g(X)) -> c_3(g#(X)) 3: c#() -> c_4(f#(n__g(n__c()))) 4: f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)) 5: activate#(X) -> c_1() 6: c#() -> c_5() 7: g#(X) -> c_7() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__c()) -> c_2(c#()) c#() -> c_4(f#(n__g(n__c()))) f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)) - Weak DPs: activate#(X) -> c_1() activate#(n__g(X)) -> c_3(g#(X)) c#() -> c_5() g#(X) -> c_7() - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__g(X)) -> g(X) c() -> f(n__g(n__c())) c() -> n__c() f(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,c/0,f/1,g/1,activate#/1,c#/0,f#/1,g#/1} / {n__c/0,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2 ,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,f#,g#} and constructors {n__c,n__g} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__c()) -> c_2(c#()) -->_1 c#() -> c_4(f#(n__g(n__c()))):2 -->_1 c#() -> c_5():6 2:S:c#() -> c_4(f#(n__g(n__c()))) -->_1 f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)):3 3:S:f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)) -->_2 activate#(n__g(X)) -> c_3(g#(X)):5 -->_1 g#(X) -> c_7():7 -->_2 activate#(X) -> c_1():4 -->_2 activate#(n__c()) -> c_2(c#()):1 4:W:activate#(X) -> c_1() 5:W:activate#(n__g(X)) -> c_3(g#(X)) -->_1 g#(X) -> c_7():7 6:W:c#() -> c_5() 7:W:g#(X) -> c_7() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: c#() -> c_5() 4: activate#(X) -> c_1() 5: activate#(n__g(X)) -> c_3(g#(X)) 7: g#(X) -> c_7() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__c()) -> c_2(c#()) c#() -> c_4(f#(n__g(n__c()))) f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)) - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__g(X)) -> g(X) c() -> f(n__g(n__c())) c() -> n__c() f(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,c/0,f/1,g/1,activate#/1,c#/0,f#/1,g#/1} / {n__c/0,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2 ,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,f#,g#} and constructors {n__c,n__g} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:activate#(n__c()) -> c_2(c#()) -->_1 c#() -> c_4(f#(n__g(n__c()))):2 2:S:c#() -> c_4(f#(n__g(n__c()))) -->_1 f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)):3 3:S:f#(n__g(X)) -> c_6(g#(activate(X)),activate#(X)) -->_2 activate#(n__c()) -> c_2(c#()):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(n__g(X)) -> c_6(activate#(X)) * Step 6: UsableRules MAYBE + Considered Problem: - Strict DPs: activate#(n__c()) -> c_2(c#()) c#() -> c_4(f#(n__g(n__c()))) f#(n__g(X)) -> c_6(activate#(X)) - Weak TRS: activate(X) -> X activate(n__c()) -> c() activate(n__g(X)) -> g(X) c() -> f(n__g(n__c())) c() -> n__c() f(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,c/0,f/1,g/1,activate#/1,c#/0,f#/1,g#/1} / {n__c/0,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1 ,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,f#,g#} and constructors {n__c,n__g} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: activate#(n__c()) -> c_2(c#()) c#() -> c_4(f#(n__g(n__c()))) f#(n__g(X)) -> c_6(activate#(X)) * Step 7: WeightGap MAYBE + Considered Problem: - Strict DPs: activate#(n__c()) -> c_2(c#()) c#() -> c_4(f#(n__g(n__c()))) f#(n__g(X)) -> c_6(activate#(X)) - Signature: {activate/1,c/0,f/1,g/1,activate#/1,c#/0,f#/1,g#/1} / {n__c/0,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1 ,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,f#,g#} and constructors {n__c,n__g} + 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(c_2) = {1}, uargs(c_4) = {1}, uargs(c_6) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(activate) = [0] p(c) = [0] p(f) = [0] p(g) = [0] p(n__c) = [0] p(n__g) = [0] p(activate#) = [14] p(c#) = [0] p(f#) = [15] p(g#) = [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [0] Following rules are strictly oriented: activate#(n__c()) = [14] > [0] = c_2(c#()) f#(n__g(X)) = [15] > [14] = c_6(activate#(X)) Following rules are (at-least) weakly oriented: c#() = [0] >= [15] = c_4(f#(n__g(n__c()))) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 8: Failure MAYBE + Considered Problem: - Strict DPs: c#() -> c_4(f#(n__g(n__c()))) - Weak DPs: activate#(n__c()) -> c_2(c#()) f#(n__g(X)) -> c_6(activate#(X)) - Signature: {activate/1,c/0,f/1,g/1,activate#/1,c#/0,f#/1,g#/1} / {n__c/0,n__g/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/0,c_6/1 ,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,c#,f#,g#} and constructors {n__c,n__g} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE