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