MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: activate(X) -> X activate(n__g(X)) -> g(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(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#(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#(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(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/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: UsableRules + Details: We replace rewrite rules by usable rules: activate(X) -> X activate(n__g(X)) -> g(X) g(X) -> n__g(X) activate#(X) -> c_1() activate#(n__g(X)) -> c_2(g#(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#(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(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: 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#(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: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__g(X)) -> c_2(g#(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(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: 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__g(X)) -> c_2(g#(X)) 2: f#(X,n__g(X),Y) -> c_4(f#(activate(Y),activate(Y),activate(Y)),activate#(Y),activate#(Y),activate#(Y)) 3: activate#(X) -> c_1() 4: b#() -> c_3() 5: g#(X) -> c_5() * Step 6: 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#(X) -> c_1() activate#(n__g(X)) -> c_2(g#(X)) b#() -> c_3() g#(X) -> c_5() - Weak TRS: activate(X) -> X activate(n__g(X)) -> g(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(g#(X)):3 -->_3 activate#(n__g(X)) -> c_2(g#(X)):3 -->_2 activate#(n__g(X)) -> c_2(g#(X)):3 -->_4 activate#(X) -> c_1():2 -->_3 activate#(X) -> c_1():2 -->_2 activate#(X) -> c_1():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#(X) -> c_1() 3:W:activate#(n__g(X)) -> c_2(g#(X)) -->_1 g#(X) -> c_5():5 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() 2: activate#(X) -> c_1() 3: activate#(n__g(X)) -> c_2(g#(X)) 5: g#(X) -> c_5() * Step 7: 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(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 8: 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(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