WORST_CASE(?,O(1)) * Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) - Signature: {cons/2,f/3,g/1} / {a/0,b/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons,f,g} and constructors {a,b,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) - Signature: {cons/2,f/3,g/1} / {a/0,b/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons,f,g} and constructors {a,b,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs cons#(x,y) -> c_1() cons#(x,y) -> c_2() f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z)),f#(x,y,z)) Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: cons#(x,y) -> c_1() cons#(x,y) -> c_2() f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z)),f#(x,y,z)) - Weak TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) - Signature: {cons/2,f/3,g/1,cons#/2,f#/3,g#/1} / {a/0,b/0,s/1,c_1/0,c_2/0,c_3/1,c_4/2} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,f#,g#} and constructors {a,b,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3} by application of Pre({1,2,3}) = {4}. Here rules are labelled as follows: 1: cons#(x,y) -> c_1() 2: cons#(x,y) -> c_2() 3: f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) 4: g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z)),f#(x,y,z)) * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z)),f#(x,y,z)) - Weak DPs: cons#(x,y) -> c_1() cons#(x,y) -> c_2() f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) - Weak TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) - Signature: {cons/2,f/3,g/1,cons#/2,f#/3,g#/1} / {a/0,b/0,s/1,c_1/0,c_2/0,c_3/1,c_4/2} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,f#,g#} and constructors {a,b,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z)),f#(x,y,z)) -->_2 f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)):4 -->_1 g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z)),f#(x,y,z)):1 2:W:cons#(x,y) -> c_1() 3:W:cons#(x,y) -> c_2() 4:W:f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: cons#(x,y) -> c_2() 2: cons#(x,y) -> c_1() 4: f#(s(a()),s(b()),x) -> c_3(f#(x,x,x)) * Step 5: SimplifyRHS WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z)),f#(x,y,z)) - Weak TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) - Signature: {cons/2,f/3,g/1,cons#/2,f#/3,g#/1} / {a/0,b/0,s/1,c_1/0,c_2/0,c_3/1,c_4/2} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,f#,g#} and constructors {a,b,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z)),f#(x,y,z)) -->_1 g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z)),f#(x,y,z)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z))) * Step 6: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: g#(f(s(x),s(y),z)) -> c_4(g#(f(x,y,z))) - Weak TRS: cons(x,y) -> x cons(x,y) -> y f(s(a()),s(b()),x) -> f(x,x,x) g(f(s(x),s(y),z)) -> g(f(x,y,z)) - Signature: {cons/2,f/3,g/1,cons#/2,f#/3,g#/1} / {a/0,b/0,s/1,c_1/0,c_2/0,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,f#,g#} and constructors {a,b,s} + Applied Processor: UsableRules + Details: No rule is usable, rules are removed from the input problem. * Step 7: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Signature: {cons/2,f/3,g/1,cons#/2,f#/3,g#/1} / {a/0,b/0,s/1,c_1/0,c_2/0,c_3/1,c_4/1} - Obligation: innermost runtime complexity wrt. defined symbols {cons#,f#,g#} and constructors {a,b,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))