WORST_CASE(?,O(n^1)) * Step 1: Sum. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c6() PLUS(z0,0()) -> c4() PLUS(z0,s(z1)) -> c5(U11'(tt(),z1,z0)) U11'(tt(),z0,z1) -> c(U12'(tt(),activate(z0),activate(z1)),ACTIVATE(z0)) U11'(tt(),z0,z1) -> c1(U12'(tt(),activate(z0),activate(z1)),ACTIVATE(z1)) U12'(tt(),z0,z1) -> c2(PLUS(activate(z1),activate(z0)),ACTIVATE(z1)) U12'(tt(),z0,z1) -> c3(PLUS(activate(z1),activate(z0)),ACTIVATE(z0)) - Weak TRS: U11(tt(),z0,z1) -> U12(tt(),activate(z0),activate(z1)) U12(tt(),z0,z1) -> s(plus(activate(z1),activate(z0))) activate(z0) -> z0 plus(z0,0()) -> z0 plus(z0,s(z1)) -> U11(tt(),z1,z0) - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1 ,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,PLUS,U11,U11',U12,U12',activate ,plus} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c6() PLUS(z0,0()) -> c4() PLUS(z0,s(z1)) -> c5(U11'(tt(),z1,z0)) U11'(tt(),z0,z1) -> c(U12'(tt(),activate(z0),activate(z1)),ACTIVATE(z0)) U11'(tt(),z0,z1) -> c1(U12'(tt(),activate(z0),activate(z1)),ACTIVATE(z1)) U12'(tt(),z0,z1) -> c2(PLUS(activate(z1),activate(z0)),ACTIVATE(z1)) U12'(tt(),z0,z1) -> c3(PLUS(activate(z1),activate(z0)),ACTIVATE(z0)) - Weak TRS: U11(tt(),z0,z1) -> U12(tt(),activate(z0),activate(z1)) U12(tt(),z0,z1) -> s(plus(activate(z1),activate(z0))) activate(z0) -> z0 plus(z0,0()) -> z0 plus(z0,s(z1)) -> U11(tt(),z1,z0) - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1 ,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,PLUS,U11,U11',U12,U12',activate ,plus} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: DependencyPairs {dpKind_ = WIDP} + Details: We add the following weak innermost dependency pairs: Strict DPs ACTIVATE#(z0) -> c_1() PLUS#(z0,0()) -> c_2() PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)) Weak DPs U11#(tt(),z0,z1) -> c_8(U12#(tt(),activate(z0),activate(z1))) U12#(tt(),z0,z1) -> c_9(plus#(activate(z1),activate(z0))) activate#(z0) -> c_10() plus#(z0,0()) -> c_11() plus#(z0,s(z1)) -> c_12(U11#(tt(),z1,z0)) and mark the set of starting terms. * Step 3: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(z0) -> c_1() PLUS#(z0,0()) -> c_2() PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)) - Strict TRS: ACTIVATE(z0) -> c6() PLUS(z0,0()) -> c4() PLUS(z0,s(z1)) -> c5(U11'(tt(),z1,z0)) U11'(tt(),z0,z1) -> c(U12'(tt(),activate(z0),activate(z1)),ACTIVATE(z0)) U11'(tt(),z0,z1) -> c1(U12'(tt(),activate(z0),activate(z1)),ACTIVATE(z1)) U12'(tt(),z0,z1) -> c2(PLUS(activate(z1),activate(z0)),ACTIVATE(z1)) U12'(tt(),z0,z1) -> c3(PLUS(activate(z1),activate(z0)),ACTIVATE(z0)) - Weak DPs: U11#(tt(),z0,z1) -> c_8(U12#(tt(),activate(z0),activate(z1))) U12#(tt(),z0,z1) -> c_9(plus#(activate(z1),activate(z0))) activate#(z0) -> c_10() plus#(z0,0()) -> c_11() plus#(z0,s(z1)) -> c_12(U11#(tt(),z1,z0)) - Weak TRS: U11(tt(),z0,z1) -> U12(tt(),activate(z0),activate(z1)) U12(tt(),z0,z1) -> s(plus(activate(z1),activate(z0))) activate(z0) -> z0 plus(z0,0()) -> z0 plus(z0,s(z1)) -> U11(tt(),z1,z0) - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2,ACTIVATE#/1,PLUS#/2,U11#/3,U11'#/3,U12#/3 ,U12'#/3,activate#/1,plus#/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1,tt/0,c_1/0,c_2/0,c_3/1,c_4/2 ,c_5/2,c_6/2,c_7/2,c_8/1,c_9/1,c_10/0,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate# ,plus#} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: activate(z0) -> z0 ACTIVATE#(z0) -> c_1() PLUS#(z0,0()) -> c_2() PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U11#(tt(),z0,z1) -> c_8(U12#(tt(),activate(z0),activate(z1))) U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)) U12#(tt(),z0,z1) -> c_9(plus#(activate(z1),activate(z0))) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)) activate#(z0) -> c_10() plus#(z0,0()) -> c_11() plus#(z0,s(z1)) -> c_12(U11#(tt(),z1,z0)) * Step 4: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: ACTIVATE#(z0) -> c_1() PLUS#(z0,0()) -> c_2() PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)) - Weak DPs: U11#(tt(),z0,z1) -> c_8(U12#(tt(),activate(z0),activate(z1))) U12#(tt(),z0,z1) -> c_9(plus#(activate(z1),activate(z0))) activate#(z0) -> c_10() plus#(z0,0()) -> c_11() plus#(z0,s(z1)) -> c_12(U11#(tt(),z1,z0)) - Weak TRS: activate(z0) -> z0 - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2,ACTIVATE#/1,PLUS#/2,U11#/3,U11'#/3,U12#/3 ,U12'#/3,activate#/1,plus#/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1,tt/0,c_1/0,c_2/0,c_3/1,c_4/2 ,c_5/2,c_6/2,c_7/2,c_8/1,c_9/1,c_10/0,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate# ,plus#} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2} by application of Pre({1,2}) = {4,5,6,7}. Here rules are labelled as follows: 1: ACTIVATE#(z0) -> c_1() 2: PLUS#(z0,0()) -> c_2() 3: PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) 4: U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)) 5: U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)) 6: U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)) 7: U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)) 8: U11#(tt(),z0,z1) -> c_8(U12#(tt(),activate(z0),activate(z1))) 9: U12#(tt(),z0,z1) -> c_9(plus#(activate(z1),activate(z0))) 10: activate#(z0) -> c_10() 11: plus#(z0,0()) -> c_11() 12: plus#(z0,s(z1)) -> c_12(U11#(tt(),z1,z0)) * Step 5: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)) - Weak DPs: ACTIVATE#(z0) -> c_1() PLUS#(z0,0()) -> c_2() U11#(tt(),z0,z1) -> c_8(U12#(tt(),activate(z0),activate(z1))) U12#(tt(),z0,z1) -> c_9(plus#(activate(z1),activate(z0))) activate#(z0) -> c_10() plus#(z0,0()) -> c_11() plus#(z0,s(z1)) -> c_12(U11#(tt(),z1,z0)) - Weak TRS: activate(z0) -> z0 - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2,ACTIVATE#/1,PLUS#/2,U11#/3,U11'#/3,U12#/3 ,U12'#/3,activate#/1,plus#/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1,tt/0,c_1/0,c_2/0,c_3/1,c_4/2 ,c_5/2,c_6/2,c_7/2,c_8/1,c_9/1,c_10/0,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate# ,plus#} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) -->_1 U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)):3 -->_1 U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)):2 2:S:U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)) -->_1 U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)):5 -->_1 U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)):4 -->_2 ACTIVATE#(z0) -> c_1():6 3:S:U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)) -->_1 U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)):5 -->_1 U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)):4 -->_2 ACTIVATE#(z0) -> c_1():6 4:S:U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)) -->_1 PLUS#(z0,0()) -> c_2():7 -->_2 ACTIVATE#(z0) -> c_1():6 -->_1 PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)):1 5:S:U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)) -->_1 PLUS#(z0,0()) -> c_2():7 -->_2 ACTIVATE#(z0) -> c_1():6 -->_1 PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)):1 6:W:ACTIVATE#(z0) -> c_1() 7:W:PLUS#(z0,0()) -> c_2() 8:W:U11#(tt(),z0,z1) -> c_8(U12#(tt(),activate(z0),activate(z1))) -->_1 U12#(tt(),z0,z1) -> c_9(plus#(activate(z1),activate(z0))):9 9:W:U12#(tt(),z0,z1) -> c_9(plus#(activate(z1),activate(z0))) -->_1 plus#(z0,s(z1)) -> c_12(U11#(tt(),z1,z0)):12 -->_1 plus#(z0,0()) -> c_11():11 10:W:activate#(z0) -> c_10() 11:W:plus#(z0,0()) -> c_11() 12:W:plus#(z0,s(z1)) -> c_12(U11#(tt(),z1,z0)) -->_1 U11#(tt(),z0,z1) -> c_8(U12#(tt(),activate(z0),activate(z1))):8 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: activate#(z0) -> c_10() 8: U11#(tt(),z0,z1) -> c_8(U12#(tt(),activate(z0),activate(z1))) 12: plus#(z0,s(z1)) -> c_12(U11#(tt(),z1,z0)) 9: U12#(tt(),z0,z1) -> c_9(plus#(activate(z1),activate(z0))) 11: plus#(z0,0()) -> c_11() 6: ACTIVATE#(z0) -> c_1() 7: PLUS#(z0,0()) -> c_2() * Step 6: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)) - Weak TRS: activate(z0) -> z0 - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2,ACTIVATE#/1,PLUS#/2,U11#/3,U11'#/3,U12#/3 ,U12'#/3,activate#/1,plus#/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1,tt/0,c_1/0,c_2/0,c_3/1,c_4/2 ,c_5/2,c_6/2,c_7/2,c_8/1,c_9/1,c_10/0,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate# ,plus#} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) -->_1 U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)):3 -->_1 U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)):2 2:S:U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z0)) -->_1 U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)):5 -->_1 U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)):4 3:S:U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1)),ACTIVATE#(z1)) -->_1 U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)):5 -->_1 U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)):4 4:S:U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z1)) -->_1 PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)):1 5:S:U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0)),ACTIVATE#(z0)) -->_1 PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))) * Step 7: PredecessorEstimationCP. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))) - Weak TRS: activate(z0) -> z0 - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2,ACTIVATE#/1,PLUS#/2,U11#/3,U11'#/3,U12#/3 ,U12'#/3,activate#/1,plus#/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1,tt/0,c_1/0,c_2/0,c_3/1,c_4/1 ,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate# ,plus#} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))) 3: U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))) Consider the set of all dependency pairs 1: PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) 2: U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))) 3: U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))) 4: U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))) 5: U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) BEST_CASE TIME (?,?) SPACE(?,?)on application of the dependency pairs {2,3} These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. ** Step 7.a:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))) - Weak TRS: activate(z0) -> z0 - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2,ACTIVATE#/1,PLUS#/2,U11#/3,U11'#/3,U12#/3 ,U12'#/3,activate#/1,plus#/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1,tt/0,c_1/0,c_2/0,c_3/1,c_4/1 ,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate# ,plus#} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: NaturalMI {miDimension = 1, 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: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_7) = {1} Following symbols are considered usable: {activate,ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate#,plus#} TcT has computed the following interpretation: p(0) = [0] p(ACTIVATE) = [2] x1 + [2] p(PLUS) = [1] x1 + [1] x2 + [1] p(U11) = [8] x1 + [1] x3 + [1] p(U11') = [1] x1 + [1] x2 + [4] p(U12) = [1] x1 + [1] x2 + [1] x3 + [2] p(U12') = [1] x2 + [1] x3 + [2] p(activate) = [1] x1 + [0] p(c) = [0] p(c1) = [1] p(c2) = [1] p(c3) = [1] x1 + [0] p(c4) = [1] p(c5) = [1] p(c6) = [4] p(plus) = [4] x2 + [0] p(s) = [1] x1 + [3] p(tt) = [10] p(ACTIVATE#) = [1] x1 + [1] p(PLUS#) = [8] x2 + [0] p(U11#) = [8] x1 + [1] x2 + [2] p(U11'#) = [2] x1 + [8] x2 + [4] p(U12#) = [1] x2 + [1] p(U12'#) = [8] x2 + [0] p(activate#) = [4] x1 + [1] p(plus#) = [1] x1 + [8] x2 + [1] p(c_1) = [0] p(c_2) = [4] p(c_3) = [1] x1 + [0] p(c_4) = [1] x1 + [14] p(c_5) = [1] x1 + [12] p(c_6) = [1] x1 + [0] p(c_7) = [1] x1 + [0] p(c_8) = [1] x1 + [1] p(c_9) = [1] x1 + [2] p(c_10) = [1] p(c_11) = [0] p(c_12) = [8] x1 + [0] Following rules are strictly oriented: U11'#(tt(),z0,z1) = [8] z0 + [24] > [8] z0 + [14] = c_4(U12'#(tt(),activate(z0),activate(z1))) U11'#(tt(),z0,z1) = [8] z0 + [24] > [8] z0 + [12] = c_5(U12'#(tt(),activate(z0),activate(z1))) Following rules are (at-least) weakly oriented: PLUS#(z0,s(z1)) = [8] z1 + [24] >= [8] z1 + [24] = c_3(U11'#(tt(),z1,z0)) U12'#(tt(),z0,z1) = [8] z0 + [0] >= [8] z0 + [0] = c_6(PLUS#(activate(z1),activate(z0))) U12'#(tt(),z0,z1) = [8] z0 + [0] >= [8] z0 + [0] = c_7(PLUS#(activate(z1),activate(z0))) activate(z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 ** Step 7.a:2: Assumption. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))) - Weak DPs: U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))) - Weak TRS: activate(z0) -> z0 - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2,ACTIVATE#/1,PLUS#/2,U11#/3,U11'#/3,U12#/3 ,U12'#/3,activate#/1,plus#/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1,tt/0,c_1/0,c_2/0,c_3/1,c_4/1 ,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate# ,plus#} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}} + Details: () ** Step 7.b:1: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))) U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))) U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))) U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))) - Weak TRS: activate(z0) -> z0 - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2,ACTIVATE#/1,PLUS#/2,U11#/3,U11'#/3,U12#/3 ,U12'#/3,activate#/1,plus#/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1,tt/0,c_1/0,c_2/0,c_3/1,c_4/1 ,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate# ,plus#} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) -->_1 U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))):3 -->_1 U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))):2 2:W:U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))) -->_1 U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))):5 -->_1 U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))):4 3:W:U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))) -->_1 U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))):5 -->_1 U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))):4 4:W:U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))) -->_1 PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)):1 5:W:U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))) -->_1 PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: PLUS#(z0,s(z1)) -> c_3(U11'#(tt(),z1,z0)) 5: U12'#(tt(),z0,z1) -> c_7(PLUS#(activate(z1),activate(z0))) 3: U11'#(tt(),z0,z1) -> c_5(U12'#(tt(),activate(z0),activate(z1))) 2: U11'#(tt(),z0,z1) -> c_4(U12'#(tt(),activate(z0),activate(z1))) 4: U12'#(tt(),z0,z1) -> c_6(PLUS#(activate(z1),activate(z0))) ** Step 7.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: activate(z0) -> z0 - Signature: {ACTIVATE/1,PLUS/2,U11/3,U11'/3,U12/3,U12'/3,activate/1,plus/2,ACTIVATE#/1,PLUS#/2,U11#/3,U11'#/3,U12#/3 ,U12'#/3,activate#/1,plus#/2} / {0/0,c/2,c1/2,c2/2,c3/2,c4/0,c5/1,c6/0,s/1,tt/0,c_1/0,c_2/0,c_3/1,c_4/1 ,c_5/1,c_6/1,c_7/1,c_8/1,c_9/1,c_10/0,c_11/0,c_12/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE#,PLUS#,U11#,U11'#,U12#,U12'#,activate# ,plus#} and constructors {0,c,c1,c2,c3,c4,c5,c6,s,tt} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))