WORST_CASE(?,O(1)) * Step 1: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'())) f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'())) - Signature: {f/2} / {./2,a/0,b/0,b'/0,c/0,d/0,d'/0,e/0,g/2,h/2,i/3,if/3} - Obligation: innermost runtime complexity wrt. defined symbols {f} and constructors {.,a,b,b',c,d,d',e,g,h,i,if} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'())) f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'())) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'())) f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'())) - Weak TRS: f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'())) f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'())) - Signature: {f/2,f#/2} / {./2,a/0,b/0,b'/0,c/0,d/0,d'/0,e/0,g/2,h/2,i/3,if/3,c_1/2,c_2/2} - Obligation: innermost runtime complexity wrt. defined symbols {f#} and constructors {.,a,b,b',c,d,d',e,g,h,i,if} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2} by application of Pre({1,2}) = {}. Here rules are labelled as follows: 1: f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'())) 2: f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'())) * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'())) f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'())) - Weak TRS: f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'())) f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'())) - Signature: {f/2,f#/2} / {./2,a/0,b/0,b'/0,c/0,d/0,d'/0,e/0,g/2,h/2,i/3,if/3,c_1/2,c_2/2} - Obligation: innermost runtime complexity wrt. defined symbols {f#} and constructors {.,a,b,b',c,d,d',e,g,h,i,if} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'())) 2:W:f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'())) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 2: f#(g(i(a(),b(),b'()),c()),d()) -> c_2(f#(.(b(),c()),d'()),f#(.(b'(),c()),d'())) 1: f#(g(h(a(),b()),c()),d()) -> c_1(f#(.(b(),g(h(a(),b()),c())),d()),f#(c(),d'())) * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: f(g(h(a(),b()),c()),d()) -> if(e(),f(.(b(),g(h(a(),b()),c())),d()),f(c(),d'())) f(g(i(a(),b(),b'()),c()),d()) -> if(e(),f(.(b(),c()),d'()),f(.(b'(),c()),d'())) - Signature: {f/2,f#/2} / {./2,a/0,b/0,b'/0,c/0,d/0,d'/0,e/0,g/2,h/2,i/3,if/3,c_1/2,c_2/2} - Obligation: innermost runtime complexity wrt. defined symbols {f#} and constructors {.,a,b,b',c,d,d',e,g,h,i,if} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))