MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: c() -> d() g() -> h() h() -> g() - Signature: {c/0,g/0,h/0} / {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#() -> c_2(h#()) h#() -> c_3(g#()) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: c#() -> c_1() g#() -> c_2(h#()) h#() -> c_3(g#()) - Weak TRS: c() -> d() g() -> h() h() -> g() - Signature: {c/0,g/0,h/0,c#/0,g#/0,h#/0} / {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: UsableRules + Details: We replace rewrite rules by usable rules: c#() -> c_1() g#() -> c_2(h#()) h#() -> c_3(g#()) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: c#() -> c_1() g#() -> c_2(h#()) h#() -> c_3(g#()) - Signature: {c/0,g/0,h/0,c#/0,g#/0,h#/0} / {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: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1} by application of Pre({1}) = {}. Here rules are labelled as follows: 1: c#() -> c_1() 2: g#() -> c_2(h#()) 3: h#() -> c_3(g#()) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: g#() -> c_2(h#()) h#() -> c_3(g#()) - Weak DPs: c#() -> c_1() - Signature: {c/0,g/0,h/0,c#/0,g#/0,h#/0} / {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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:g#() -> c_2(h#()) -->_1 h#() -> c_3(g#()):2 2:S:h#() -> c_3(g#()) -->_1 g#() -> c_2(h#()):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: WeightGap MAYBE + Considered Problem: - Strict DPs: g#() -> c_2(h#()) h#() -> c_3(g#()) - Signature: {c/0,g/0,h/0,c#/0,g#/0,h#/0} / {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(c_2) = {1}, uargs(c_3) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(c) = [0] p(d) = [0] p(g) = [0] p(h) = [0] p(c#) = [0] p(g#) = [0] p(h#) = [1] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [0] Following rules are strictly oriented: h#() = [1] > [0] = c_3(g#()) Following rules are (at-least) weakly oriented: g#() = [0] >= [1] = c_2(h#()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: g#() -> c_2(h#()) - Weak DPs: h#() -> c_3(g#()) - Signature: {c/0,g/0,h/0,c#/0,g#/0,h#/0} / {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