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