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