MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: f(X) -> cons(X,f(g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) - Signature: {f/1,g/1,sel/2} / {0/0,cons/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g,sel} and constructors {0,cons,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(X) -> c_1(f#(g(X)),g#(X)) g#(0()) -> c_2() g#(s(X)) -> c_3(g#(X)) sel#(0(),cons(X,Y)) -> c_4() sel#(s(X),cons(Y,Z)) -> c_5(sel#(X,Z)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: f#(X) -> c_1(f#(g(X)),g#(X)) g#(0()) -> c_2() g#(s(X)) -> c_3(g#(X)) sel#(0(),cons(X,Y)) -> c_4() sel#(s(X),cons(Y,Z)) -> c_5(sel#(X,Z)) - Weak TRS: f(X) -> cons(X,f(g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,Z) - Signature: {f/1,g/1,sel/2,f#/1,g#/1,sel#/2} / {0/0,cons/2,s/1,c_1/2,c_2/0,c_3/1,c_4/0,c_5/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,sel#} and constructors {0,cons,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) f#(X) -> c_1(f#(g(X)),g#(X)) g#(0()) -> c_2() g#(s(X)) -> c_3(g#(X)) sel#(0(),cons(X,Y)) -> c_4() sel#(s(X),cons(Y,Z)) -> c_5(sel#(X,Z)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: f#(X) -> c_1(f#(g(X)),g#(X)) g#(0()) -> c_2() g#(s(X)) -> c_3(g#(X)) sel#(0(),cons(X,Y)) -> c_4() sel#(s(X),cons(Y,Z)) -> c_5(sel#(X,Z)) - Weak TRS: g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) - Signature: {f/1,g/1,sel/2,f#/1,g#/1,sel#/2} / {0/0,cons/2,s/1,c_1/2,c_2/0,c_3/1,c_4/0,c_5/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,sel#} and constructors {0,cons,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4} by application of Pre({2,4}) = {1,3,5}. Here rules are labelled as follows: 1: f#(X) -> c_1(f#(g(X)),g#(X)) 2: g#(0()) -> c_2() 3: g#(s(X)) -> c_3(g#(X)) 4: sel#(0(),cons(X,Y)) -> c_4() 5: sel#(s(X),cons(Y,Z)) -> c_5(sel#(X,Z)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: f#(X) -> c_1(f#(g(X)),g#(X)) g#(s(X)) -> c_3(g#(X)) sel#(s(X),cons(Y,Z)) -> c_5(sel#(X,Z)) - Weak DPs: g#(0()) -> c_2() sel#(0(),cons(X,Y)) -> c_4() - Weak TRS: g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) - Signature: {f/1,g/1,sel/2,f#/1,g#/1,sel#/2} / {0/0,cons/2,s/1,c_1/2,c_2/0,c_3/1,c_4/0,c_5/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,sel#} and constructors {0,cons,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(X) -> c_1(f#(g(X)),g#(X)) -->_2 g#(s(X)) -> c_3(g#(X)):2 -->_2 g#(0()) -> c_2():4 -->_1 f#(X) -> c_1(f#(g(X)),g#(X)):1 2:S:g#(s(X)) -> c_3(g#(X)) -->_1 g#(0()) -> c_2():4 -->_1 g#(s(X)) -> c_3(g#(X)):2 3:S:sel#(s(X),cons(Y,Z)) -> c_5(sel#(X,Z)) -->_1 sel#(0(),cons(X,Y)) -> c_4():5 -->_1 sel#(s(X),cons(Y,Z)) -> c_5(sel#(X,Z)):3 4:W:g#(0()) -> c_2() 5:W:sel#(0(),cons(X,Y)) -> c_4() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: sel#(0(),cons(X,Y)) -> c_4() 4: g#(0()) -> c_2() * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: f#(X) -> c_1(f#(g(X)),g#(X)) g#(s(X)) -> c_3(g#(X)) sel#(s(X),cons(Y,Z)) -> c_5(sel#(X,Z)) - Weak TRS: g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) - Signature: {f/1,g/1,sel/2,f#/1,g#/1,sel#/2} / {0/0,cons/2,s/1,c_1/2,c_2/0,c_3/1,c_4/0,c_5/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,sel#} and constructors {0,cons,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE