WORST_CASE(?,O(n^1)) * Step 1: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2} / {a/0,b/0,c/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {f,g,h,i} and constructors {a,b,c,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) g#(x,x) -> c_3(g#(a(),b())) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> c_4(g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) ,g#(a(),g(a(),g(x,g(b(),g(b(),y))))) ,g#(a(),g(x,g(b(),g(b(),y)))) ,g#(x,g(b(),g(b(),y))) ,g#(b(),g(b(),y)) ,g#(b(),y)) h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)) h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) i#(x,x) -> c_8(i#(a(),b())) Weak DPs and mark the set of starting terms. * Step 2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) g#(x,x) -> c_3(g#(a(),b())) g#(a(),g(x,g(b(),g(a(),g(x,y))))) -> c_4(g#(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) ,g#(a(),g(a(),g(x,g(b(),g(b(),y))))) ,g#(a(),g(x,g(b(),g(b(),y)))) ,g#(x,g(b(),g(b(),y))) ,g#(b(),g(b(),y)) ,g#(b(),y)) h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)) h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) i#(x,x) -> c_8(i#(a(),b())) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/2,c_2/2,c_3/1,c_4/6,c_5/2,c_6/4,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) g#(x,x) -> c_3(g#(a(),b())) h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)) h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) i#(x,x) -> c_8(i#(a(),b())) * Step 3: PredecessorEstimation WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) g#(x,x) -> c_3(g#(a(),b())) h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)) h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) i#(x,x) -> c_8(i#(a(),b())) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/2,c_2/2,c_3/1,c_4/6,c_5/2,c_6/4,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,7} by application of Pre({3,7}) = {1,4,5}. Here rules are labelled as follows: 1: f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))) 2: f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) 3: g#(x,x) -> c_3(g#(a(),b())) 4: h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)) 5: h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)) 6: h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) 7: i#(x,x) -> c_8(i#(a(),b())) * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)) h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: g#(x,x) -> c_3(g#(a(),b())) i#(x,x) -> c_8(i#(a(),b())) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/2,c_2/2,c_3/1,c_4/6,c_5/2,c_6/4,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))) -->_1 f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))):2 -->_2 g#(x,x) -> c_3(g#(a(),b())):6 -->_1 f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))):1 2:S:f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) -->_2 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))):2 -->_1 f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))):1 3:S:h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)) -->_1 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)):4 -->_2 g#(x,x) -> c_3(g#(a(),b())):6 -->_1 h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)):3 4:S:h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)) -->_4 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_3 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_2 i#(x,x) -> c_8(i#(a(),b())):7 -->_1 i#(x,x) -> c_8(i#(a(),b())):7 -->_4 h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)):4 -->_3 h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)):4 -->_4 h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)):3 -->_3 h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)):3 5:S:h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) -->_1 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)):4 -->_1 h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)):3 -->_2 f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))):2 -->_2 f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))):1 6:W:g#(x,x) -> c_3(g#(a(),b())) 7:W:i#(x,x) -> c_8(i#(a(),b())) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 6: g#(x,x) -> c_3(g#(a(),b())) 7: i#(x,x) -> c_8(i#(a(),b())) * Step 5: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)) h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/2,c_2/2,c_3/1,c_4/6,c_5/2,c_6/4,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))) -->_1 f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))):2 -->_1 f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))):1 2:S:f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) -->_2 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))):2 -->_1 f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))):1 3:S:h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)) -->_1 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)):4 -->_1 h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)):3 4:S:h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)) -->_4 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_3 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_4 h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)):4 -->_3 h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)):4 -->_4 h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)):3 -->_3 h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)):3 5:S:h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) -->_1 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 h#(i(x,y)) -> c_6(i#(i(c(),h(h(y))),x),i#(c(),h(h(y))),h#(h(y)),h#(y)):4 -->_1 h#(g(x,s(y))) -> c_5(h#(g(s(x),y)),g#(s(x),y)):3 -->_2 f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))):2 -->_2 f#(g(s(x),y)) -> c_1(f#(g(x,s(y))),g#(x,s(y))):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) * Step 6: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) The strictly oriented rules are moved into the weak component. ** Step 6.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {2} Following symbols are considered usable: {f,g,h,i,f#,g#,h#,i#} TcT has computed the following interpretation: p(a) = [0] [0] p(b) = [0] [0] p(c) = [0] [0] p(f) = [1 0] x1 + [0] [1 0] [0] p(g) = [0] [0] p(h) = [0 0] x1 + [0] [2 0] [0] p(i) = [2 2] x1 + [0 0] x2 + [0] [0 0] [2 2] [0] p(s) = [0 3] x1 + [2] [0 1] [0] p(f#) = [1 0] x1 + [0] [1 0] [0] p(g#) = [1 0] x1 + [0] [0 0] [0] p(h#) = [0 2] x1 + [0] [1 0] [2] p(i#) = [0 0] x1 + [1 1] x2 + [0] [0 1] [0 1] [0] p(c_1) = [2 0] x1 + [0] [0 0] [0] p(c_2) = [1 1] x1 + [1 0] x2 + [1] [2 1] [0 0] [1] p(c_3) = [1 1] x1 + [0] [2 2] [1] p(c_4) = [1 2] x2 + [0 0] x4 + [0 0] x5 + [2 2] x6 + [2] [0 0] [0 2] [0 2] [1 0] [0] p(c_5) = [2 0] x1 + [0] [2 0] [0] p(c_6) = [1 0] x1 + [2 0] x2 + [0] [0 0] [0 0] [2] p(c_7) = [1 1] x2 + [0] [0 2] [0] p(c_8) = [0 2] x1 + [0] [0 2] [0] Following rules are strictly oriented: f#(s(x)) = [0 3] x + [2] [0 3] [2] > [0 2] x + [1] [0 0] [1] = c_2(f#(h(s(x))),h#(s(x))) Following rules are (at-least) weakly oriented: f#(g(s(x),y)) = [0] [0] >= [0] [0] = c_1(f#(g(x,s(y)))) h#(g(x,s(y))) = [0] [2] >= [0] [0] = c_5(h#(g(s(x),y))) h#(i(x,y)) = [0 0] x + [4 4] y + [0] [2 2] [0 0] [2] >= [4 4] y + [0] [0 0] [2] = c_6(h#(h(y)),h#(y)) h#(s(f(x))) = [2 0] x + [0] [3 0] [4] >= [2 0] x + [0] [2 0] [0] = c_7(h#(f(x)),f#(x)) f(g(s(x),y)) = [0] [0] >= [0] [0] = f(g(x,s(y))) f(s(x)) = [0 3] x + [2] [0 3] [2] >= [2] [0] = s(s(f(h(s(x))))) g(x,x) = [0] [0] >= [0] [0] = g(a(),b()) h(g(x,s(y))) = [0] [0] >= [0] [0] = h(g(s(x),y)) h(i(x,y)) = [0 0] x + [0] [4 4] [0] >= [0 0] x + [0] [2 2] [0] = i(i(c(),h(h(y))),x) h(s(f(x))) = [0 0] x + [0] [6 0] [4] >= [0 0] x + [0] [2 0] [0] = h(f(x)) i(x,x) = [2 2] x + [0] [2 2] [0] >= [0] [0] = i(a(),b()) ** Step 6.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ** Step 6.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) The strictly oriented rules are moved into the weak component. *** Step 6.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {2} Following symbols are considered usable: {f,g,h,i,f#,g#,h#,i#} TcT has computed the following interpretation: p(a) = [0] [0] p(b) = [0] [0] p(c) = [0] [0] p(f) = [0 0] x1 + [0] [2 2] [2] p(g) = [0 0] x1 + [0 1] x2 + [0] [0 2] [0 0] [0] p(h) = [0 0] x1 + [0] [1 0] [0] p(i) = [3 1] x1 + [0 0] x2 + [0] [0 0] [3 1] [0] p(s) = [0 0] x1 + [0] [0 1] [1] p(f#) = [2 2] x1 + [3] [0 0] [1] p(g#) = [2 1] x1 + [1 2] x2 + [0] [0 0] [0 0] [1] p(h#) = [2 1] x1 + [0] [0 0] [1] p(i#) = [0 0] x2 + [0] [0 1] [1] p(c_1) = [1 1] x1 + [0] [0 1] [0] p(c_2) = [1 0] x1 + [1 0] x2 + [1] [0 0] [0 0] [1] p(c_3) = [0] [0] p(c_4) = [0 0] x2 + [0 0] x3 + [0 0] x6 + [0] [2 0] [0 2] [2 0] [1] p(c_5) = [1 0] x1 + [0] [0 1] [0] p(c_6) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(c_7) = [1 0] x2 + [0] [0 1] [0] p(c_8) = [2] [0] Following rules are strictly oriented: f#(g(s(x),y)) = [0 4] x + [0 2] y + [7] [0 0] [0 0] [1] > [0 4] x + [0 2] y + [6] [0 0] [0 0] [1] = c_1(f#(g(x,s(y)))) Following rules are (at-least) weakly oriented: f#(s(x)) = [0 2] x + [5] [0 0] [1] >= [0 1] x + [5] [0 0] [1] = c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) = [0 2] x + [0 2] y + [2] [0 0] [0 0] [1] >= [0 2] x + [0 2] y + [2] [0 0] [0 0] [1] = c_5(h#(g(s(x),y))) h#(i(x,y)) = [6 2] x + [3 1] y + [0] [0 0] [0 0] [1] >= [3 1] y + [0] [0 0] [0] = c_6(h#(h(y)),h#(y)) h#(s(f(x))) = [2 2] x + [3] [0 0] [1] >= [2 2] x + [3] [0 0] [1] = c_7(h#(f(x)),f#(x)) f(g(s(x),y)) = [0 0] x + [0 0] y + [0] [0 4] [0 2] [6] >= [0 0] x + [0 0] y + [0] [0 4] [0 2] [4] = f(g(x,s(y))) f(s(x)) = [0 0] x + [0] [0 2] [4] >= [0] [4] = s(s(f(h(s(x))))) g(x,x) = [0 1] x + [0] [0 2] [0] >= [0] [0] = g(a(),b()) h(g(x,s(y))) = [0 0] y + [0] [0 1] [1] >= [0 0] y + [0] [0 1] [0] = h(g(s(x),y)) h(i(x,y)) = [0 0] x + [0] [3 1] [0] >= [0 0] x + [0] [3 1] [0] = i(i(c(),h(h(y))),x) h(s(f(x))) = [0] [0] >= [0] [0] = h(f(x)) i(x,x) = [3 1] x + [0] [3 1] [0] >= [0] [0] = i(a(),b()) *** Step 6.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 6.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) The strictly oriented rules are moved into the weak component. **** Step 6.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {2} Following symbols are considered usable: {f,g,h,i,f#,g#,h#,i#} TcT has computed the following interpretation: p(a) = [0] [0] p(b) = [0] [0] p(c) = [0] [0] p(f) = [3 0] x1 + [1] [0 0] [0] p(g) = [1 0] x1 + [1 0] x2 + [0] [0 0] [2 0] [1] p(h) = [0 0] x1 + [0] [2 0] [0] p(i) = [1 1] x1 + [0 0] x2 + [0] [0 0] [2 1] [0] p(s) = [1 0] x1 + [2] [0 0] [0] p(f#) = [0 0] x1 + [0] [1 1] [0] p(g#) = [0 0] x2 + [2] [0 1] [1] p(h#) = [0 1] x1 + [0] [0 0] [0] p(i#) = [0] [0] p(c_1) = [2 0] x1 + [0] [0 0] [3] p(c_2) = [2 0] x1 + [2 0] x2 + [0] [0 0] [0 0] [0] p(c_3) = [2] [0] p(c_4) = [0 1] x2 + [0] [2 0] [0] p(c_5) = [1 0] x1 + [2] [0 0] [0] p(c_6) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 0] [0] p(c_7) = [1 0] x2 + [0] [0 0] [0] p(c_8) = [0 0] x1 + [1] [0 1] [1] Following rules are strictly oriented: h#(g(x,s(y))) = [2 0] y + [5] [0 0] [0] > [2 0] y + [3] [0 0] [0] = c_5(h#(g(s(x),y))) Following rules are (at-least) weakly oriented: f#(g(s(x),y)) = [0 0] x + [0 0] y + [0] [1 0] [3 0] [3] >= [0] [3] = c_1(f#(g(x,s(y)))) f#(s(x)) = [0 0] x + [0] [1 0] [2] >= [0] [0] = c_2(f#(h(s(x))),h#(s(x))) h#(i(x,y)) = [2 1] y + [0] [0 0] [0] >= [2 1] y + [0] [0 0] [0] = c_6(h#(h(y)),h#(y)) h#(s(f(x))) = [0] [0] >= [0] [0] = c_7(h#(f(x)),f#(x)) f(g(s(x),y)) = [3 0] x + [3 0] y + [7] [0 0] [0 0] [0] >= [3 0] x + [3 0] y + [7] [0 0] [0 0] [0] = f(g(x,s(y))) f(s(x)) = [3 0] x + [7] [0 0] [0] >= [5] [0] = s(s(f(h(s(x))))) g(x,x) = [2 0] x + [0] [2 0] [1] >= [0] [1] = g(a(),b()) h(g(x,s(y))) = [0 0] x + [0 0] y + [0] [2 0] [2 0] [4] >= [0 0] x + [0 0] y + [0] [2 0] [2 0] [4] = h(g(s(x),y)) h(i(x,y)) = [0 0] x + [0] [2 2] [0] >= [0 0] x + [0] [2 1] [0] = i(i(c(),h(h(y))),x) h(s(f(x))) = [0 0] x + [0] [6 0] [6] >= [0 0] x + [0] [6 0] [2] = h(f(x)) i(x,x) = [1 1] x + [0] [2 1] [0] >= [0] [0] = i(a(),b()) **** Step 6.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 6.b:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) The strictly oriented rules are moved into the weak component. ***** Step 6.b:1.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {2} Following symbols are considered usable: {f,g,h,i,f#,g#,h#,i#} TcT has computed the following interpretation: p(a) = [0] [0] p(b) = [0] [0] p(c) = [0] [0] p(f) = [3 2] x1 + [3] [3 2] [3] p(g) = [0 2] x1 + [0] [0 0] [2] p(h) = [0 0] x1 + [0] [1 0] [0] p(i) = [1 2] x1 + [0 0] x2 + [0] [0 0] [1 2] [0] p(s) = [0 1] x1 + [1] [0 1] [0] p(f#) = [3 2] x1 + [2] [0 0] [1] p(g#) = [2 0] x2 + [0] [0 0] [0] p(h#) = [0 2] x1 + [0] [0 0] [0] p(i#) = [0 0] x2 + [0] [1 0] [0] p(c_1) = [1 0] x1 + [0] [0 1] [0] p(c_2) = [1 1] x1 + [1 0] x2 + [0] [0 0] [0 1] [1] p(c_3) = [1] [0] p(c_4) = [0 2] x1 + [0 2] x2 + [2 1] x4 + [1] [0 2] [2 0] [0 0] [1] p(c_5) = [1 1] x1 + [0] [0 0] [0] p(c_6) = [1 0] x1 + [2 0] x2 + [0] [0 0] [0 0] [0] p(c_7) = [2 0] x2 + [0] [0 0] [0] p(c_8) = [0] [2] Following rules are strictly oriented: h#(s(f(x))) = [6 4] x + [6] [0 0] [0] > [6 4] x + [4] [0 0] [0] = c_7(h#(f(x)),f#(x)) Following rules are (at-least) weakly oriented: f#(g(s(x),y)) = [0 6] x + [6] [0 0] [1] >= [0 6] x + [6] [0 0] [1] = c_1(f#(g(x,s(y)))) f#(s(x)) = [0 5] x + [5] [0 0] [1] >= [0 4] x + [5] [0 0] [1] = c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) = [4] [0] >= [4] [0] = c_5(h#(g(s(x),y))) h#(i(x,y)) = [2 4] y + [0] [0 0] [0] >= [2 4] y + [0] [0 0] [0] = c_6(h#(h(y)),h#(y)) f(g(s(x),y)) = [0 6] x + [7] [0 6] [7] >= [0 6] x + [7] [0 6] [7] = f(g(x,s(y))) f(s(x)) = [0 5] x + [6] [0 5] [6] >= [0 2] x + [6] [0 2] [5] = s(s(f(h(s(x))))) g(x,x) = [0 2] x + [0] [0 0] [2] >= [0] [2] = g(a(),b()) h(g(x,s(y))) = [0 0] x + [0] [0 2] [0] >= [0 0] x + [0] [0 2] [0] = h(g(s(x),y)) h(i(x,y)) = [0 0] x + [0] [1 2] [0] >= [0 0] x + [0] [1 2] [0] = i(i(c(),h(h(y))),x) h(s(f(x))) = [0 0] x + [0] [3 2] [4] >= [0 0] x + [0] [3 2] [3] = h(f(x)) i(x,x) = [1 2] x + [0] [1 2] [0] >= [0] [0] = i(a(),b()) ***** Step 6.b:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 6.b:1.b:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) The strictly oriented rules are moved into the weak component. ****** Step 6.b:1.b:1.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 1 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1,2}, uargs(c_5) = {1}, uargs(c_6) = {1,2}, uargs(c_7) = {2} Following symbols are considered usable: {f,g,h,i,f#,g#,h#,i#} TcT has computed the following interpretation: p(a) = [0] [0] p(b) = [0] [0] p(c) = [0] [0] p(f) = [0] [0] p(g) = [1 2] x1 + [1] [0 2] [0] p(h) = [0 3] x1 + [0] [1 0] [0] p(i) = [1 1] x1 + [0 0] x2 + [1] [0 0] [1 1] [1] p(s) = [0] [0] p(f#) = [0 0] x1 + [0] [0 1] [2] p(g#) = [0 0] x1 + [0] [1 0] [1] p(h#) = [0 2] x1 + [0] [0 0] [3] p(i#) = [0] [0] p(c_1) = [2 0] x1 + [0] [0 0] [2] p(c_2) = [2 0] x1 + [2 0] x2 + [0] [0 0] [0 0] [1] p(c_3) = [0] [0] p(c_4) = [0] [0] p(c_5) = [1 0] x1 + [0] [0 0] [0] p(c_6) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 1] [0] p(c_7) = [2 0] x2 + [0] [0 0] [0] p(c_8) = [0] [0] Following rules are strictly oriented: h#(i(x,y)) = [2 2] y + [2] [0 0] [3] > [2 2] y + [0] [0 0] [3] = c_6(h#(h(y)),h#(y)) Following rules are (at-least) weakly oriented: f#(g(s(x),y)) = [0] [2] >= [0] [2] = c_1(f#(g(x,s(y)))) f#(s(x)) = [0] [2] >= [0] [1] = c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) = [0 4] x + [0] [0 0] [3] >= [0] [0] = c_5(h#(g(s(x),y))) h#(s(f(x))) = [0] [3] >= [0] [0] = c_7(h#(f(x)),f#(x)) f(g(s(x),y)) = [0] [0] >= [0] [0] = f(g(x,s(y))) f(s(x)) = [0] [0] >= [0] [0] = s(s(f(h(s(x))))) g(x,x) = [1 2] x + [1] [0 2] [0] >= [1] [0] = g(a(),b()) h(g(x,s(y))) = [0 6] x + [0] [1 2] [1] >= [0] [1] = h(g(s(x),y)) h(i(x,y)) = [0 0] x + [3 3] y + [3] [1 1] [0 0] [1] >= [0 0] x + [3 3] y + [3] [1 1] [0 0] [1] = i(i(c(),h(h(y))),x) h(s(f(x))) = [0] [0] >= [0] [0] = h(f(x)) i(x,x) = [1 1] x + [1] [1 1] [1] >= [1] [1] = i(a(),b()) ****** Step 6.b:1.b:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ****** Step 6.b:1.b:1.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) -->_1 f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))):2 -->_1 f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))):1 2:W:f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) -->_2 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))):2 -->_1 f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))):1 3:W:h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) -->_1 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 h#(i(x,y)) -> c_6(h#(h(y)),h#(y)):4 -->_1 h#(g(x,s(y))) -> c_5(h#(g(s(x),y))):3 4:W:h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) -->_2 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_2 h#(i(x,y)) -> c_6(h#(h(y)),h#(y)):4 -->_1 h#(i(x,y)) -> c_6(h#(h(y)),h#(y)):4 -->_2 h#(g(x,s(y))) -> c_5(h#(g(s(x),y))):3 -->_1 h#(g(x,s(y))) -> c_5(h#(g(s(x),y))):3 5:W:h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) -->_1 h#(s(f(x))) -> c_7(h#(f(x)),f#(x)):5 -->_1 h#(i(x,y)) -> c_6(h#(h(y)),h#(y)):4 -->_1 h#(g(x,s(y))) -> c_5(h#(g(s(x),y))):3 -->_2 f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))):2 -->_2 f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: f#(g(s(x),y)) -> c_1(f#(g(x,s(y)))) 5: h#(s(f(x))) -> c_7(h#(f(x)),f#(x)) 4: h#(i(x,y)) -> c_6(h#(h(y)),h#(y)) 3: h#(g(x,s(y))) -> c_5(h#(g(s(x),y))) 2: f#(s(x)) -> c_2(f#(h(s(x))),h#(s(x))) ****** Step 6.b:1.b:1.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) h(s(f(x))) -> h(f(x)) i(x,x) -> i(a(),b()) - Signature: {f/1,g/2,h/1,i/2,f#/1,g#/2,h#/1,i#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/2,c_3/1,c_4/6,c_5/1,c_6/2,c_7/2,c_8/1} - Obligation: innermost runtime complexity wrt. defined symbols {f#,g#,h#,i#} and constructors {a,b,c,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))