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