WORST_CASE(?,O(1)) * Step 1: DependencyPairs WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: a__c() -> c() a__c() -> d() a__g(X) -> a__h(X) a__g(X) -> g(X) a__h(X) -> h(X) a__h(d()) -> a__g(c()) mark(c()) -> a__c() mark(d()) -> d() mark(g(X)) -> a__g(X) mark(h(X)) -> a__h(X) - Signature: {a__c/0,a__g/1,a__h/1,mark/1} / {c/0,d/0,g/1,h/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c,a__g,a__h,mark} and constructors {c,d,g,h} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__c#() -> c_1() a__c#() -> c_2() a__g#(X) -> c_3(a__h#(X)) a__g#(X) -> c_4() a__h#(X) -> c_5() a__h#(d()) -> c_6(a__g#(c())) mark#(c()) -> c_7(a__c#()) mark#(d()) -> c_8() mark#(g(X)) -> c_9(a__g#(X)) mark#(h(X)) -> c_10(a__h#(X)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: a__c#() -> c_1() a__c#() -> c_2() a__g#(X) -> c_3(a__h#(X)) a__g#(X) -> c_4() a__h#(X) -> c_5() a__h#(d()) -> c_6(a__g#(c())) mark#(c()) -> c_7(a__c#()) mark#(d()) -> c_8() mark#(g(X)) -> c_9(a__g#(X)) mark#(h(X)) -> c_10(a__h#(X)) - Weak TRS: a__c() -> c() a__c() -> d() a__g(X) -> a__h(X) a__g(X) -> g(X) a__h(X) -> h(X) a__h(d()) -> a__g(c()) mark(c()) -> a__c() mark(d()) -> d() mark(g(X)) -> a__g(X) mark(h(X)) -> a__h(X) - Signature: {a__c/0,a__g/1,a__h/1,mark/1,a__c#/0,a__g#/1,a__h#/1,mark#/1} / {c/0,d/0,g/1,h/1,c_1/0,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/1,c_7/1,c_8/0,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__g#,a__h#,mark#} and constructors {c,d,g,h} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: a__c#() -> c_1() a__c#() -> c_2() a__g#(X) -> c_3(a__h#(X)) a__g#(X) -> c_4() a__h#(X) -> c_5() a__h#(d()) -> c_6(a__g#(c())) mark#(c()) -> c_7(a__c#()) mark#(d()) -> c_8() mark#(g(X)) -> c_9(a__g#(X)) mark#(h(X)) -> c_10(a__h#(X)) * Step 3: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: a__c#() -> c_1() a__c#() -> c_2() a__g#(X) -> c_3(a__h#(X)) a__g#(X) -> c_4() a__h#(X) -> c_5() a__h#(d()) -> c_6(a__g#(c())) mark#(c()) -> c_7(a__c#()) mark#(d()) -> c_8() mark#(g(X)) -> c_9(a__g#(X)) mark#(h(X)) -> c_10(a__h#(X)) - Signature: {a__c/0,a__g/1,a__h/1,mark/1,a__c#/0,a__g#/1,a__h#/1,mark#/1} / {c/0,d/0,g/1,h/1,c_1/0,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/1,c_7/1,c_8/0,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__g#,a__h#,mark#} and constructors {c,d,g,h} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,4,5,8} by application of Pre({1,2,4,5,8}) = {3,6,7,9,10}. Here rules are labelled as follows: 1: a__c#() -> c_1() 2: a__c#() -> c_2() 3: a__g#(X) -> c_3(a__h#(X)) 4: a__g#(X) -> c_4() 5: a__h#(X) -> c_5() 6: a__h#(d()) -> c_6(a__g#(c())) 7: mark#(c()) -> c_7(a__c#()) 8: mark#(d()) -> c_8() 9: mark#(g(X)) -> c_9(a__g#(X)) 10: mark#(h(X)) -> c_10(a__h#(X)) * Step 4: PredecessorEstimation WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: a__g#(X) -> c_3(a__h#(X)) a__h#(d()) -> c_6(a__g#(c())) mark#(c()) -> c_7(a__c#()) mark#(g(X)) -> c_9(a__g#(X)) mark#(h(X)) -> c_10(a__h#(X)) - Weak DPs: a__c#() -> c_1() a__c#() -> c_2() a__g#(X) -> c_4() a__h#(X) -> c_5() mark#(d()) -> c_8() - Signature: {a__c/0,a__g/1,a__h/1,mark/1,a__c#/0,a__g#/1,a__h#/1,mark#/1} / {c/0,d/0,g/1,h/1,c_1/0,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/1,c_7/1,c_8/0,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__g#,a__h#,mark#} and constructors {c,d,g,h} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3} by application of Pre({3}) = {}. Here rules are labelled as follows: 1: a__g#(X) -> c_3(a__h#(X)) 2: a__h#(d()) -> c_6(a__g#(c())) 3: mark#(c()) -> c_7(a__c#()) 4: mark#(g(X)) -> c_9(a__g#(X)) 5: mark#(h(X)) -> c_10(a__h#(X)) 6: a__c#() -> c_1() 7: a__c#() -> c_2() 8: a__g#(X) -> c_4() 9: a__h#(X) -> c_5() 10: mark#(d()) -> c_8() * Step 5: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: a__g#(X) -> c_3(a__h#(X)) a__h#(d()) -> c_6(a__g#(c())) mark#(g(X)) -> c_9(a__g#(X)) mark#(h(X)) -> c_10(a__h#(X)) - Weak DPs: a__c#() -> c_1() a__c#() -> c_2() a__g#(X) -> c_4() a__h#(X) -> c_5() mark#(c()) -> c_7(a__c#()) mark#(d()) -> c_8() - Signature: {a__c/0,a__g/1,a__h/1,mark/1,a__c#/0,a__g#/1,a__h#/1,mark#/1} / {c/0,d/0,g/1,h/1,c_1/0,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/1,c_7/1,c_8/0,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__g#,a__h#,mark#} and constructors {c,d,g,h} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a__g#(X) -> c_3(a__h#(X)) -->_1 a__h#(d()) -> c_6(a__g#(c())):2 -->_1 a__h#(X) -> c_5():8 2:S:a__h#(d()) -> c_6(a__g#(c())) -->_1 a__g#(X) -> c_4():7 -->_1 a__g#(X) -> c_3(a__h#(X)):1 3:S:mark#(g(X)) -> c_9(a__g#(X)) -->_1 a__g#(X) -> c_4():7 -->_1 a__g#(X) -> c_3(a__h#(X)):1 4:S:mark#(h(X)) -> c_10(a__h#(X)) -->_1 a__h#(X) -> c_5():8 -->_1 a__h#(d()) -> c_6(a__g#(c())):2 5:W:a__c#() -> c_1() 6:W:a__c#() -> c_2() 7:W:a__g#(X) -> c_4() 8:W:a__h#(X) -> c_5() 9:W:mark#(c()) -> c_7(a__c#()) -->_1 a__c#() -> c_2():6 -->_1 a__c#() -> c_1():5 10:W:mark#(d()) -> c_8() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: mark#(d()) -> c_8() 9: mark#(c()) -> c_7(a__c#()) 6: a__c#() -> c_2() 5: a__c#() -> c_1() 8: a__h#(X) -> c_5() 7: a__g#(X) -> c_4() * Step 6: RemoveHeads WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: a__g#(X) -> c_3(a__h#(X)) a__h#(d()) -> c_6(a__g#(c())) mark#(g(X)) -> c_9(a__g#(X)) mark#(h(X)) -> c_10(a__h#(X)) - Signature: {a__c/0,a__g/1,a__h/1,mark/1,a__c#/0,a__g#/1,a__h#/1,mark#/1} / {c/0,d/0,g/1,h/1,c_1/0,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/1,c_7/1,c_8/0,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__g#,a__h#,mark#} and constructors {c,d,g,h} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:a__g#(X) -> c_3(a__h#(X)) -->_1 a__h#(d()) -> c_6(a__g#(c())):2 2:S:a__h#(d()) -> c_6(a__g#(c())) -->_1 a__g#(X) -> c_3(a__h#(X)):1 3:S:mark#(g(X)) -> c_9(a__g#(X)) -->_1 a__g#(X) -> c_3(a__h#(X)):1 4:S:mark#(h(X)) -> c_10(a__h#(X)) -->_1 a__h#(d()) -> c_6(a__g#(c())):2 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(3,mark#(g(X)) -> c_9(a__g#(X))),(4,mark#(h(X)) -> c_10(a__h#(X)))] * Step 7: NaturalMI WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: a__g#(X) -> c_3(a__h#(X)) a__h#(d()) -> c_6(a__g#(c())) - Signature: {a__c/0,a__g/1,a__h/1,mark/1,a__c#/0,a__g#/1,a__h#/1,mark#/1} / {c/0,d/0,g/1,h/1,c_1/0,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/1,c_7/1,c_8/0,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__g#,a__h#,mark#} and constructors {c,d,g,h} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: 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_3) = {1}, uargs(c_6) = {1} Following symbols are considered usable: {a__c#,a__g#,a__h#,mark#} TcT has computed the following interpretation: p(a__c) = [1] p(a__g) = [0] p(a__h) = [1] x1 + [0] p(c) = [0] p(d) = [12] p(g) = [2] p(h) = [0] p(mark) = [8] x1 + [2] p(a__c#) = [0] p(a__g#) = [12] x1 + [1] p(a__h#) = [1] x1 + [0] p(mark#) = [2] x1 + [1] p(c_1) = [8] p(c_2) = [1] p(c_3) = [8] x1 + [1] p(c_4) = [0] p(c_5) = [1] p(c_6) = [4] x1 + [4] p(c_7) = [1] x1 + [1] p(c_8) = [2] p(c_9) = [1] p(c_10) = [1] Following rules are strictly oriented: a__h#(d()) = [12] > [8] = c_6(a__g#(c())) Following rules are (at-least) weakly oriented: a__g#(X) = [12] X + [1] >= [8] X + [1] = c_3(a__h#(X)) * Step 8: WeightGap WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: a__g#(X) -> c_3(a__h#(X)) - Weak DPs: a__h#(d()) -> c_6(a__g#(c())) - Signature: {a__c/0,a__g/1,a__h/1,mark/1,a__c#/0,a__g#/1,a__h#/1,mark#/1} / {c/0,d/0,g/1,h/1,c_1/0,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/1,c_7/1,c_8/0,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__g#,a__h#,mark#} and constructors {c,d,g,h} + 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_3) = {1}, uargs(c_6) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(a__c) = [0] p(a__g) = [0] p(a__h) = [0] p(c) = [0] p(d) = [3] p(g) = [0] p(h) = [0] p(mark) = [0] p(a__c#) = [0] p(a__g#) = [5] x1 + [15] p(a__h#) = [5] x1 + [0] p(mark#) = [2] x1 + [0] p(c_1) = [8] p(c_2) = [8] p(c_3) = [1] x1 + [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] x1 + [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] Following rules are strictly oriented: a__g#(X) = [5] X + [15] > [5] X + [0] = c_3(a__h#(X)) Following rules are (at-least) weakly oriented: a__h#(d()) = [15] >= [15] = c_6(a__g#(c())) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 9: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: a__g#(X) -> c_3(a__h#(X)) a__h#(d()) -> c_6(a__g#(c())) - Signature: {a__c/0,a__g/1,a__h/1,mark/1,a__c#/0,a__g#/1,a__h#/1,mark#/1} / {c/0,d/0,g/1,h/1,c_1/0,c_2/0,c_3/1,c_4/0 ,c_5/0,c_6/1,c_7/1,c_8/0,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__c#,a__g#,a__h#,mark#} and constructors {c,d,g,h} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))