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