WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: e(g(X)) -> e(X) f(a()) -> f(c(a())) f(a()) -> f(d(a())) f(c(X)) -> X f(c(a())) -> f(d(b())) f(c(b())) -> f(d(a())) f(d(X)) -> X - Signature: {e/1,f/1} / {a/0,b/0,c/1,d/1,g/1} - Obligation: innermost runtime complexity wrt. defined symbols {e,f} and constructors {a,b,c,d,g} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: e(g(X)) -> e(X) f(a()) -> f(c(a())) f(a()) -> f(d(a())) f(c(X)) -> X f(c(a())) -> f(d(b())) f(c(b())) -> f(d(a())) f(d(X)) -> X - Signature: {e/1,f/1} / {a/0,b/0,c/1,d/1,g/1} - Obligation: innermost runtime complexity wrt. defined symbols {e,f} and constructors {a,b,c,d,g} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: e(x){x -> g(x)} = e(g(x)) ->^+ e(x) = C[e(x) = e(x){}] ** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: e(g(X)) -> e(X) f(a()) -> f(c(a())) f(a()) -> f(d(a())) f(c(X)) -> X f(c(a())) -> f(d(b())) f(c(b())) -> f(d(a())) f(d(X)) -> X - Signature: {e/1,f/1} / {a/0,b/0,c/1,d/1,g/1} - Obligation: innermost runtime complexity wrt. defined symbols {e,f} and constructors {a,b,c,d,g} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs e#(g(X)) -> c_1(e#(X)) f#(a()) -> c_2(f#(c(a()))) f#(a()) -> c_3(f#(d(a()))) f#(c(X)) -> c_4() f#(c(a())) -> c_5(f#(d(b()))) f#(c(b())) -> c_6(f#(d(a()))) f#(d(X)) -> c_7() Weak DPs and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: e#(g(X)) -> c_1(e#(X)) f#(a()) -> c_2(f#(c(a()))) f#(a()) -> c_3(f#(d(a()))) f#(c(X)) -> c_4() f#(c(a())) -> c_5(f#(d(b()))) f#(c(b())) -> c_6(f#(d(a()))) f#(d(X)) -> c_7() - Weak TRS: e(g(X)) -> e(X) f(a()) -> f(c(a())) f(a()) -> f(d(a())) f(c(X)) -> X f(c(a())) -> f(d(b())) f(c(b())) -> f(d(a())) f(d(X)) -> X - Signature: {e/1,f/1,e#/1,f#/1} / {a/0,b/0,c/1,d/1,g/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {e#,f#} and constructors {a,b,c,d,g} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,7} by application of Pre({4,7}) = {2,3,5,6}. Here rules are labelled as follows: 1: e#(g(X)) -> c_1(e#(X)) 2: f#(a()) -> c_2(f#(c(a()))) 3: f#(a()) -> c_3(f#(d(a()))) 4: f#(c(X)) -> c_4() 5: f#(c(a())) -> c_5(f#(d(b()))) 6: f#(c(b())) -> c_6(f#(d(a()))) 7: f#(d(X)) -> c_7() ** Step 1.b:3: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: e#(g(X)) -> c_1(e#(X)) f#(a()) -> c_2(f#(c(a()))) f#(a()) -> c_3(f#(d(a()))) f#(c(a())) -> c_5(f#(d(b()))) f#(c(b())) -> c_6(f#(d(a()))) - Weak DPs: f#(c(X)) -> c_4() f#(d(X)) -> c_7() - Weak TRS: e(g(X)) -> e(X) f(a()) -> f(c(a())) f(a()) -> f(d(a())) f(c(X)) -> X f(c(a())) -> f(d(b())) f(c(b())) -> f(d(a())) f(d(X)) -> X - Signature: {e/1,f/1,e#/1,f#/1} / {a/0,b/0,c/1,d/1,g/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {e#,f#} and constructors {a,b,c,d,g} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,4,5} by application of Pre({3,4,5}) = {2}. Here rules are labelled as follows: 1: e#(g(X)) -> c_1(e#(X)) 2: f#(a()) -> c_2(f#(c(a()))) 3: f#(a()) -> c_3(f#(d(a()))) 4: f#(c(a())) -> c_5(f#(d(b()))) 5: f#(c(b())) -> c_6(f#(d(a()))) 6: f#(c(X)) -> c_4() 7: f#(d(X)) -> c_7() ** Step 1.b:4: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: e#(g(X)) -> c_1(e#(X)) f#(a()) -> c_2(f#(c(a()))) - Weak DPs: f#(a()) -> c_3(f#(d(a()))) f#(c(X)) -> c_4() f#(c(a())) -> c_5(f#(d(b()))) f#(c(b())) -> c_6(f#(d(a()))) f#(d(X)) -> c_7() - Weak TRS: e(g(X)) -> e(X) f(a()) -> f(c(a())) f(a()) -> f(d(a())) f(c(X)) -> X f(c(a())) -> f(d(b())) f(c(b())) -> f(d(a())) f(d(X)) -> X - Signature: {e/1,f/1,e#/1,f#/1} / {a/0,b/0,c/1,d/1,g/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {e#,f#} and constructors {a,b,c,d,g} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2} by application of Pre({2}) = {}. Here rules are labelled as follows: 1: e#(g(X)) -> c_1(e#(X)) 2: f#(a()) -> c_2(f#(c(a()))) 3: f#(a()) -> c_3(f#(d(a()))) 4: f#(c(X)) -> c_4() 5: f#(c(a())) -> c_5(f#(d(b()))) 6: f#(c(b())) -> c_6(f#(d(a()))) 7: f#(d(X)) -> c_7() ** Step 1.b:5: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: e#(g(X)) -> c_1(e#(X)) - Weak DPs: f#(a()) -> c_2(f#(c(a()))) f#(a()) -> c_3(f#(d(a()))) f#(c(X)) -> c_4() f#(c(a())) -> c_5(f#(d(b()))) f#(c(b())) -> c_6(f#(d(a()))) f#(d(X)) -> c_7() - Weak TRS: e(g(X)) -> e(X) f(a()) -> f(c(a())) f(a()) -> f(d(a())) f(c(X)) -> X f(c(a())) -> f(d(b())) f(c(b())) -> f(d(a())) f(d(X)) -> X - Signature: {e/1,f/1,e#/1,f#/1} / {a/0,b/0,c/1,d/1,g/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {e#,f#} and constructors {a,b,c,d,g} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:e#(g(X)) -> c_1(e#(X)) -->_1 e#(g(X)) -> c_1(e#(X)):1 2:W:f#(a()) -> c_2(f#(c(a()))) -->_1 f#(c(a())) -> c_5(f#(d(b()))):5 -->_1 f#(c(X)) -> c_4():4 3:W:f#(a()) -> c_3(f#(d(a()))) -->_1 f#(d(X)) -> c_7():7 4:W:f#(c(X)) -> c_4() 5:W:f#(c(a())) -> c_5(f#(d(b()))) -->_1 f#(d(X)) -> c_7():7 6:W:f#(c(b())) -> c_6(f#(d(a()))) -->_1 f#(d(X)) -> c_7():7 7:W:f#(d(X)) -> c_7() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: f#(c(b())) -> c_6(f#(d(a()))) 3: f#(a()) -> c_3(f#(d(a()))) 2: f#(a()) -> c_2(f#(c(a()))) 4: f#(c(X)) -> c_4() 5: f#(c(a())) -> c_5(f#(d(b()))) 7: f#(d(X)) -> c_7() ** Step 1.b:6: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: e#(g(X)) -> c_1(e#(X)) - Weak TRS: e(g(X)) -> e(X) f(a()) -> f(c(a())) f(a()) -> f(d(a())) f(c(X)) -> X f(c(a())) -> f(d(b())) f(c(b())) -> f(d(a())) f(d(X)) -> X - Signature: {e/1,f/1,e#/1,f#/1} / {a/0,b/0,c/1,d/1,g/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {e#,f#} and constructors {a,b,c,d,g} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: e#(g(X)) -> c_1(e#(X)) ** Step 1.b:7: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: e#(g(X)) -> c_1(e#(X)) - Signature: {e/1,f/1,e#/1,f#/1} / {a/0,b/0,c/1,d/1,g/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {e#,f#} and constructors {a,b,c,d,g} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(c_1) = {1} Following symbols are considered usable: {e#,f#} TcT has computed the following interpretation: p(a) = 0 p(b) = 0 p(c) = x1 p(d) = x1 p(e) = 0 p(f) = 0 p(g) = 1 + x1 p(e#) = 15 + 8*x1 p(f#) = 0 p(c_1) = x1 p(c_2) = x1 p(c_3) = x1 p(c_4) = 0 p(c_5) = x1 p(c_6) = x1 p(c_7) = 4 Following rules are strictly oriented: e#(g(X)) = 23 + 8*X > 15 + 8*X = c_1(e#(X)) Following rules are (at-least) weakly oriented: ** Step 1.b:8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: e#(g(X)) -> c_1(e#(X)) - Signature: {e/1,f/1,e#/1,f#/1} / {a/0,b/0,c/1,d/1,g/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/0} - Obligation: innermost runtime complexity wrt. defined symbols {e#,f#} and constructors {a,b,c,d,g} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))