MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: c() -> d() g(X) -> h(X) h(d()) -> g(c()) - Signature: {c/0,g/1,h/1} / {d/0} - Obligation: innermost runtime complexity wrt. defined symbols {c,g,h} and constructors {d} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs c#() -> c_1() g#(X) -> c_2(h#(X)) h#(d()) -> c_3(g#(c()),c#()) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: c#() -> c_1() g#(X) -> c_2(h#(X)) h#(d()) -> c_3(g#(c()),c#()) - Weak TRS: c() -> d() g(X) -> h(X) h(d()) -> g(c()) - Signature: {c/0,g/1,h/1,c#/0,g#/1,h#/1} / {d/0,c_1/0,c_2/1,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {c#,g#,h#} and constructors {d} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: c() -> d() c#() -> c_1() g#(X) -> c_2(h#(X)) h#(d()) -> c_3(g#(c()),c#()) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: c#() -> c_1() g#(X) -> c_2(h#(X)) h#(d()) -> c_3(g#(c()),c#()) - Weak TRS: c() -> d() - Signature: {c/0,g/1,h/1,c#/0,g#/1,h#/1} / {d/0,c_1/0,c_2/1,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {c#,g#,h#} and constructors {d} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {3}. Here rules are labelled as follows: 1: c#() -> c_1() 2: g#(X) -> c_2(h#(X)) 3: h#(d()) -> c_3(g#(c()),c#()) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: g#(X) -> c_2(h#(X)) h#(d()) -> c_3(g#(c()),c#()) - Weak DPs: c#() -> c_1() - Weak TRS: c() -> d() - Signature: {c/0,g/1,h/1,c#/0,g#/1,h#/1} / {d/0,c_1/0,c_2/1,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {c#,g#,h#} and constructors {d} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:g#(X) -> c_2(h#(X)) -->_1 h#(d()) -> c_3(g#(c()),c#()):2 2:S:h#(d()) -> c_3(g#(c()),c#()) -->_2 c#() -> c_1():3 -->_1 g#(X) -> c_2(h#(X)):1 3:W:c#() -> c_1() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: c#() -> c_1() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: g#(X) -> c_2(h#(X)) h#(d()) -> c_3(g#(c()),c#()) - Weak TRS: c() -> d() - Signature: {c/0,g/1,h/1,c#/0,g#/1,h#/1} / {d/0,c_1/0,c_2/1,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {c#,g#,h#} and constructors {d} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:g#(X) -> c_2(h#(X)) -->_1 h#(d()) -> c_3(g#(c()),c#()):2 2:S:h#(d()) -> c_3(g#(c()),c#()) -->_1 g#(X) -> c_2(h#(X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: h#(d()) -> c_3(g#(c())) * Step 6: WeightGap MAYBE + Considered Problem: - Strict DPs: g#(X) -> c_2(h#(X)) h#(d()) -> c_3(g#(c())) - Weak TRS: c() -> d() - Signature: {c/0,g/1,h/1,c#/0,g#/1,h#/1} / {d/0,c_1/0,c_2/1,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {c#,g#,h#} and constructors {d} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(g#) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(c) = [8] p(d) = [8] p(g) = [1] x1 + [1] p(h) = [1] x1 + [1] p(c#) = [1] p(g#) = [1] x1 + [0] p(h#) = [1] x1 + [1] p(c_1) = [1] p(c_2) = [1] x1 + [5] p(c_3) = [1] x1 + [0] Following rules are strictly oriented: h#(d()) = [9] > [8] = c_3(g#(c())) Following rules are (at-least) weakly oriented: g#(X) = [1] X + [0] >= [1] X + [6] = c_2(h#(X)) c() = [8] >= [8] = d() Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: Failure MAYBE + Considered Problem: - Strict DPs: g#(X) -> c_2(h#(X)) - Weak DPs: h#(d()) -> c_3(g#(c())) - Weak TRS: c() -> d() - Signature: {c/0,g/1,h/1,c#/0,g#/1,h#/1} / {d/0,c_1/0,c_2/1,c_3/1} - Obligation: innermost runtime complexity wrt. defined symbols {c#,g#,h#} and constructors {d} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE