MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) b() -> c() f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y)) g(X) -> n__g(X) g(b()) -> c() - Signature: {activate/1,b/0,f/3,g/1} / {c/0,n__g/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,b,f,g} and constructors {c,n__g} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. g(b()) -> c() All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) b() -> c() f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1} / {c/0,n__g/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,b,f,g} and constructors {c,n__g} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs activate#(X) -> c_1() activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)) b#() -> c_3() f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) g#(X) -> c_5() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)) b#() -> c_3() f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) g#(X) -> c_5() - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) b() -> c() f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/2,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) activate#(X) -> c_1() activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)) b#() -> c_3() f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) g#(X) -> c_5() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)) b#() -> c_3() f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) g#(X) -> c_5() - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/2,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,5} by application of Pre({1,3,5}) = {2,4}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)) 3: b#() -> c_3() 4: f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) 5: g#(X) -> c_5() * Step 5: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)) f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) - Weak DPs: activate#(X) -> c_1() b#() -> c_3() g#(X) -> c_5() - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/2,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)) -->_1 g#(X) -> c_5():5 -->_2 activate#(X) -> c_1():3 -->_2 activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)):1 2:S:f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) -->_4 activate#(X) -> c_1():3 -->_3 activate#(X) -> c_1():3 -->_2 activate#(X) -> c_1():3 -->_1 f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)) ,activate#(Y) ,activate#(Y) ,activate#(Y)):2 -->_4 activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)):1 -->_3 activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)):1 -->_2 activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)):1 3:W:activate#(X) -> c_1() 4:W:b#() -> c_3() 5:W:g#(X) -> c_5() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 4: b#() -> c_3() 3: activate#(X) -> c_1() 5: g#(X) -> c_5() * Step 6: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)) f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/2,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)) -->_2 activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)):1 2:S:f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) -->_1 f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)) ,activate#(Y) ,activate#(Y) ,activate#(Y)):2 -->_4 activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)):1 -->_3 activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)):1 -->_2 activate#(n__g(X)) -> c_2(g#(activate(X)),activate#(X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: activate#(n__g(X)) -> c_2(activate#(X)) * Step 7: Decompose MAYBE + Considered Problem: - Strict DPs: activate#(n__g(X)) -> c_2(activate#(X)) f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/1,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: activate#(n__g(X)) -> c_2(activate#(X)) - Weak DPs: f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/1,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} Problem (S) - Strict DPs: f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) - Weak DPs: activate#(n__g(X)) -> c_2(activate#(X)) - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/1,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} ** Step 7.a:1: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__g(X)) -> c_2(activate#(X)) - Weak DPs: f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/1,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 7.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) - Weak DPs: activate#(n__g(X)) -> c_2(activate#(X)) - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/1,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) -->_4 activate#(n__g(X)) -> c_2(activate#(X)):2 -->_3 activate#(n__g(X)) -> c_2(activate#(X)):2 -->_2 activate#(n__g(X)) -> c_2(activate#(X)):2 -->_1 f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)) ,activate#(Y) ,activate#(Y) ,activate#(Y)):1 2:W:activate#(n__g(X)) -> c_2(activate#(X)) -->_1 activate#(n__g(X)) -> c_2(activate#(X)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: activate#(n__g(X)) -> c_2(activate#(X)) ** Step 7.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/1,c_3/0,c_4/4,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) -->_1 f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)) ,activate#(Y) ,activate#(Y) ,activate#(Y)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y))) ** Step 7.b:3: Failure MAYBE + Considered Problem: - Strict DPs: f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y))) - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(activate(X)) g(X) -> n__g(X) - Signature: {activate/1,b/0,f/3,g/1,activate#/1,b#/0,f#/3,g#/1} / {c/0,n__g/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,b#,f#,g#} and constructors {c,n__g} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE