WORST_CASE(?,O(n^1)) * Step 1: Sum. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__add(X1,X2)) -> add(X1,X2) activate(n__from(X)) -> from(X) activate(n__fst(X1,X2)) -> fst(X1,X2) activate(n__len(X)) -> len(X) add(X1,X2) -> n__add(X1,X2) add(0(),X) -> X add(s(X),Y) -> s(n__add(activate(X),Y)) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) fst(X1,X2) -> n__fst(X1,X2) fst(0(),Z) -> nil() fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z))) len(X) -> n__len(X) len(cons(X,Z)) -> s(n__len(activate(Z))) len(nil()) -> 0() - Signature: {activate/1,add/2,from/1,fst/2,len/1} / {0/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,from,fst,len} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__add(X1,X2)) -> add(X1,X2) activate(n__from(X)) -> from(X) activate(n__fst(X1,X2)) -> fst(X1,X2) activate(n__len(X)) -> len(X) add(X1,X2) -> n__add(X1,X2) add(0(),X) -> X add(s(X),Y) -> s(n__add(activate(X),Y)) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) fst(X1,X2) -> n__fst(X1,X2) fst(0(),Z) -> nil() fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z))) len(X) -> n__len(X) len(cons(X,Z)) -> s(n__len(activate(Z))) len(nil()) -> 0() - Signature: {activate/1,add/2,from/1,fst/2,len/1} / {0/0,cons/2,n__add/2,n__from/1,n__fst/2,n__len/1,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {activate,add,from,fst,len} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs activate#(X) -> c_1() activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__from(X)) -> c_3(from#(X)) activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(X1,X2) -> c_6() add#(0(),X) -> c_7() add#(s(X),Y) -> c_8(activate#(X)) from#(X) -> c_9() from#(X) -> c_10() fst#(X1,X2) -> c_11() fst#(0(),Z) -> c_12() fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) len#(X) -> c_14() len#(cons(X,Z)) -> c_15(activate#(Z)) len#(nil()) -> c_16() Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(X) -> c_1() activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__from(X)) -> c_3(from#(X)) activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(X1,X2) -> c_6() add#(0(),X) -> c_7() add#(s(X),Y) -> c_8(activate#(X)) from#(X) -> c_9() from#(X) -> c_10() fst#(X1,X2) -> c_11() fst#(0(),Z) -> c_12() fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) len#(X) -> c_14() len#(cons(X,Z)) -> c_15(activate#(Z)) len#(nil()) -> c_16() - Weak TRS: activate(X) -> X activate(n__add(X1,X2)) -> add(X1,X2) activate(n__from(X)) -> from(X) activate(n__fst(X1,X2)) -> fst(X1,X2) activate(n__len(X)) -> len(X) add(X1,X2) -> n__add(X1,X2) add(0(),X) -> X add(s(X),Y) -> s(n__add(activate(X),Y)) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) fst(X1,X2) -> n__fst(X1,X2) fst(0(),Z) -> nil() fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z))) len(X) -> n__len(X) len(cons(X,Z)) -> s(n__len(activate(Z))) len(nil()) -> 0() - Signature: {activate/1,add/2,from/1,fst/2,len/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,cons/2,n__add/2 ,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0 ,c_12/0,c_13/2,c_14/0,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,from#,fst#,len#} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,6,7,9,10,11,12,14,16} by application of Pre({1,6,7,9,10,11,12,14,16}) = {2,3,4,5,8,13,15}. Here rules are labelled as follows: 1: activate#(X) -> c_1() 2: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) 3: activate#(n__from(X)) -> c_3(from#(X)) 4: activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) 5: activate#(n__len(X)) -> c_5(len#(X)) 6: add#(X1,X2) -> c_6() 7: add#(0(),X) -> c_7() 8: add#(s(X),Y) -> c_8(activate#(X)) 9: from#(X) -> c_9() 10: from#(X) -> c_10() 11: fst#(X1,X2) -> c_11() 12: fst#(0(),Z) -> c_12() 13: fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) 14: len#(X) -> c_14() 15: len#(cons(X,Z)) -> c_15(activate#(Z)) 16: len#(nil()) -> c_16() * Step 4: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__from(X)) -> c_3(from#(X)) activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(s(X),Y) -> c_8(activate#(X)) fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) len#(cons(X,Z)) -> c_15(activate#(Z)) - Weak DPs: activate#(X) -> c_1() add#(X1,X2) -> c_6() add#(0(),X) -> c_7() from#(X) -> c_9() from#(X) -> c_10() fst#(X1,X2) -> c_11() fst#(0(),Z) -> c_12() len#(X) -> c_14() len#(nil()) -> c_16() - Weak TRS: activate(X) -> X activate(n__add(X1,X2)) -> add(X1,X2) activate(n__from(X)) -> from(X) activate(n__fst(X1,X2)) -> fst(X1,X2) activate(n__len(X)) -> len(X) add(X1,X2) -> n__add(X1,X2) add(0(),X) -> X add(s(X),Y) -> s(n__add(activate(X),Y)) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) fst(X1,X2) -> n__fst(X1,X2) fst(0(),Z) -> nil() fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z))) len(X) -> n__len(X) len(cons(X,Z)) -> s(n__len(activate(Z))) len(nil()) -> 0() - Signature: {activate/1,add/2,from/1,fst/2,len/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,cons/2,n__add/2 ,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0 ,c_12/0,c_13/2,c_14/0,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,from#,fst#,len#} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2} by application of Pre({2}) = {5,6,7}. Here rules are labelled as follows: 1: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) 2: activate#(n__from(X)) -> c_3(from#(X)) 3: activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) 4: activate#(n__len(X)) -> c_5(len#(X)) 5: add#(s(X),Y) -> c_8(activate#(X)) 6: fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) 7: len#(cons(X,Z)) -> c_15(activate#(Z)) 8: activate#(X) -> c_1() 9: add#(X1,X2) -> c_6() 10: add#(0(),X) -> c_7() 11: from#(X) -> c_9() 12: from#(X) -> c_10() 13: fst#(X1,X2) -> c_11() 14: fst#(0(),Z) -> c_12() 15: len#(X) -> c_14() 16: len#(nil()) -> c_16() * Step 5: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(s(X),Y) -> c_8(activate#(X)) fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) len#(cons(X,Z)) -> c_15(activate#(Z)) - Weak DPs: activate#(X) -> c_1() activate#(n__from(X)) -> c_3(from#(X)) add#(X1,X2) -> c_6() add#(0(),X) -> c_7() from#(X) -> c_9() from#(X) -> c_10() fst#(X1,X2) -> c_11() fst#(0(),Z) -> c_12() len#(X) -> c_14() len#(nil()) -> c_16() - Weak TRS: activate(X) -> X activate(n__add(X1,X2)) -> add(X1,X2) activate(n__from(X)) -> from(X) activate(n__fst(X1,X2)) -> fst(X1,X2) activate(n__len(X)) -> len(X) add(X1,X2) -> n__add(X1,X2) add(0(),X) -> X add(s(X),Y) -> s(n__add(activate(X),Y)) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) fst(X1,X2) -> n__fst(X1,X2) fst(0(),Z) -> nil() fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z))) len(X) -> n__len(X) len(cons(X,Z)) -> s(n__len(activate(Z))) len(nil()) -> 0() - Signature: {activate/1,add/2,from/1,fst/2,len/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,cons/2,n__add/2 ,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0 ,c_12/0,c_13/2,c_14/0,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,from#,fst#,len#} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) -->_1 add#(s(X),Y) -> c_8(activate#(X)):4 -->_1 add#(0(),X) -> c_7():10 -->_1 add#(X1,X2) -> c_6():9 2:S:activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) -->_1 fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)):5 -->_1 fst#(0(),Z) -> c_12():14 -->_1 fst#(X1,X2) -> c_11():13 3:S:activate#(n__len(X)) -> c_5(len#(X)) -->_1 len#(cons(X,Z)) -> c_15(activate#(Z)):6 -->_1 len#(nil()) -> c_16():16 -->_1 len#(X) -> c_14():15 4:S:add#(s(X),Y) -> c_8(activate#(X)) -->_1 activate#(n__from(X)) -> c_3(from#(X)):8 -->_1 activate#(X) -> c_1():7 -->_1 activate#(n__len(X)) -> c_5(len#(X)):3 -->_1 activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 5:S:fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) -->_2 activate#(n__from(X)) -> c_3(from#(X)):8 -->_1 activate#(n__from(X)) -> c_3(from#(X)):8 -->_2 activate#(X) -> c_1():7 -->_1 activate#(X) -> c_1():7 -->_2 activate#(n__len(X)) -> c_5(len#(X)):3 -->_1 activate#(n__len(X)) -> c_5(len#(X)):3 -->_2 activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)):2 -->_1 activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)):2 -->_2 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 6:S:len#(cons(X,Z)) -> c_15(activate#(Z)) -->_1 activate#(n__from(X)) -> c_3(from#(X)):8 -->_1 activate#(X) -> c_1():7 -->_1 activate#(n__len(X)) -> c_5(len#(X)):3 -->_1 activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)):2 -->_1 activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)):1 7:W:activate#(X) -> c_1() 8:W:activate#(n__from(X)) -> c_3(from#(X)) -->_1 from#(X) -> c_10():12 -->_1 from#(X) -> c_9():11 9:W:add#(X1,X2) -> c_6() 10:W:add#(0(),X) -> c_7() 11:W:from#(X) -> c_9() 12:W:from#(X) -> c_10() 13:W:fst#(X1,X2) -> c_11() 14:W:fst#(0(),Z) -> c_12() 15:W:len#(X) -> c_14() 16:W:len#(nil()) -> c_16() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: add#(X1,X2) -> c_6() 10: add#(0(),X) -> c_7() 15: len#(X) -> c_14() 16: len#(nil()) -> c_16() 13: fst#(X1,X2) -> c_11() 14: fst#(0(),Z) -> c_12() 7: activate#(X) -> c_1() 8: activate#(n__from(X)) -> c_3(from#(X)) 11: from#(X) -> c_9() 12: from#(X) -> c_10() * Step 6: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(s(X),Y) -> c_8(activate#(X)) fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) len#(cons(X,Z)) -> c_15(activate#(Z)) - Weak TRS: activate(X) -> X activate(n__add(X1,X2)) -> add(X1,X2) activate(n__from(X)) -> from(X) activate(n__fst(X1,X2)) -> fst(X1,X2) activate(n__len(X)) -> len(X) add(X1,X2) -> n__add(X1,X2) add(0(),X) -> X add(s(X),Y) -> s(n__add(activate(X),Y)) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) fst(X1,X2) -> n__fst(X1,X2) fst(0(),Z) -> nil() fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z))) len(X) -> n__len(X) len(cons(X,Z)) -> s(n__len(activate(Z))) len(nil()) -> 0() - Signature: {activate/1,add/2,from/1,fst/2,len/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,cons/2,n__add/2 ,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0 ,c_12/0,c_13/2,c_14/0,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,from#,fst#,len#} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(s(X),Y) -> c_8(activate#(X)) fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) len#(cons(X,Z)) -> c_15(activate#(Z)) * Step 7: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(s(X),Y) -> c_8(activate#(X)) fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) len#(cons(X,Z)) -> c_15(activate#(Z)) - Signature: {activate/1,add/2,from/1,fst/2,len/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,cons/2,n__add/2 ,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0 ,c_12/0,c_13/2,c_14/0,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,from#,fst#,len#} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1,2}, uargs(c_15) = {1} Following symbols are considered usable: {activate#,add#,from#,fst#,len#} TcT has computed the following interpretation: p(0) = [0] p(activate) = [0] p(add) = [2] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [0] p(from) = [2] p(fst) = [1] x2 + [1] p(len) = [1] p(n__add) = [1] x1 + [1] x2 + [2] p(n__from) = [1] p(n__fst) = [1] x1 + [1] x2 + [2] p(n__len) = [1] x1 + [2] p(nil) = [2] p(s) = [1] x1 + [0] p(activate#) = [8] x1 + [0] p(add#) = [8] x1 + [1] x2 + [12] p(from#) = [1] x1 + [0] p(fst#) = [8] x1 + [8] x2 + [7] p(len#) = [8] x1 + [0] p(c_1) = [0] p(c_2) = [1] x1 + [4] p(c_3) = [8] x1 + [1] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [14] p(c_6) = [0] p(c_7) = [0] p(c_8) = [1] x1 + [2] p(c_9) = [1] p(c_10) = [0] p(c_11) = [1] p(c_12) = [4] p(c_13) = [1] x1 + [1] x2 + [2] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [0] Following rules are strictly oriented: activate#(n__fst(X1,X2)) = [8] X1 + [8] X2 + [16] > [8] X1 + [8] X2 + [7] = c_4(fst#(X1,X2)) activate#(n__len(X)) = [8] X + [16] > [8] X + [14] = c_5(len#(X)) add#(s(X),Y) = [8] X + [1] Y + [12] > [8] X + [2] = c_8(activate#(X)) fst#(s(X),cons(Y,Z)) = [8] X + [8] Y + [8] Z + [7] > [8] X + [8] Z + [2] = c_13(activate#(X),activate#(Z)) Following rules are (at-least) weakly oriented: activate#(n__add(X1,X2)) = [8] X1 + [8] X2 + [16] >= [8] X1 + [1] X2 + [16] = c_2(add#(X1,X2)) len#(cons(X,Z)) = [8] X + [8] Z + [0] >= [8] Z + [0] = c_15(activate#(Z)) * Step 8: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) len#(cons(X,Z)) -> c_15(activate#(Z)) - Weak DPs: activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(s(X),Y) -> c_8(activate#(X)) fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) - Signature: {activate/1,add/2,from/1,fst/2,len/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,cons/2,n__add/2 ,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0 ,c_12/0,c_13/2,c_14/0,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,from#,fst#,len#} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1,2}, uargs(c_15) = {1} Following symbols are considered usable: {activate#,add#,from#,fst#,len#} TcT has computed the following interpretation: p(0) = [1] p(activate) = [4] p(add) = [2] x1 + [1] p(cons) = [1] x2 + [0] p(from) = [2] x1 + [0] p(fst) = [1] x1 + [0] p(len) = [0] p(n__add) = [1] x1 + [0] p(n__from) = [1] x1 + [1] p(n__fst) = [1] x1 + [1] x2 + [2] p(n__len) = [1] x1 + [2] p(nil) = [0] p(s) = [1] x1 + [2] p(activate#) = [8] x1 + [0] p(add#) = [8] x1 + [0] p(from#) = [1] p(fst#) = [8] x1 + [8] x2 + [1] p(len#) = [8] x1 + [1] p(c_1) = [1] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [8] p(c_4) = [1] x1 + [7] p(c_5) = [1] x1 + [15] p(c_6) = [1] p(c_7) = [1] p(c_8) = [1] x1 + [14] p(c_9) = [1] p(c_10) = [2] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [1] x2 + [0] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] Following rules are strictly oriented: len#(cons(X,Z)) = [8] Z + [1] > [8] Z + [0] = c_15(activate#(Z)) Following rules are (at-least) weakly oriented: activate#(n__add(X1,X2)) = [8] X1 + [0] >= [8] X1 + [0] = c_2(add#(X1,X2)) activate#(n__fst(X1,X2)) = [8] X1 + [8] X2 + [16] >= [8] X1 + [8] X2 + [8] = c_4(fst#(X1,X2)) activate#(n__len(X)) = [8] X + [16] >= [8] X + [16] = c_5(len#(X)) add#(s(X),Y) = [8] X + [16] >= [8] X + [14] = c_8(activate#(X)) fst#(s(X),cons(Y,Z)) = [8] X + [8] Z + [17] >= [8] X + [8] Z + [0] = c_13(activate#(X),activate#(Z)) * Step 9: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) - Weak DPs: activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(s(X),Y) -> c_8(activate#(X)) fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) len#(cons(X,Z)) -> c_15(activate#(Z)) - Signature: {activate/1,add/2,from/1,fst/2,len/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,cons/2,n__add/2 ,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0 ,c_12/0,c_13/2,c_14/0,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,from#,fst#,len#} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1,2}, uargs(c_15) = {1} Following symbols are considered usable: {activate#,add#,from#,fst#,len#} TcT has computed the following interpretation: p(0) = [2] p(activate) = [1] p(add) = [1] x1 + [1] p(cons) = [1] x2 + [1] p(from) = [1] p(fst) = [1] x1 + [8] x2 + [1] p(len) = [1] x1 + [2] p(n__add) = [1] x1 + [2] p(n__from) = [1] p(n__fst) = [1] x1 + [1] x2 + [0] p(n__len) = [1] x1 + [2] p(nil) = [1] p(s) = [1] x1 + [0] p(activate#) = [8] x1 + [0] p(add#) = [8] x1 + [0] p(from#) = [1] x1 + [0] p(fst#) = [8] x1 + [8] x2 + [0] p(len#) = [8] x1 + [3] p(c_1) = [0] p(c_2) = [1] x1 + [14] p(c_3) = [2] x1 + [1] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [13] p(c_6) = [2] p(c_7) = [0] p(c_8) = [1] x1 + [0] p(c_9) = [1] p(c_10) = [2] p(c_11) = [0] p(c_12) = [2] p(c_13) = [1] x1 + [1] x2 + [8] p(c_14) = [1] p(c_15) = [1] x1 + [3] p(c_16) = [0] Following rules are strictly oriented: activate#(n__add(X1,X2)) = [8] X1 + [16] > [8] X1 + [14] = c_2(add#(X1,X2)) Following rules are (at-least) weakly oriented: activate#(n__fst(X1,X2)) = [8] X1 + [8] X2 + [0] >= [8] X1 + [8] X2 + [0] = c_4(fst#(X1,X2)) activate#(n__len(X)) = [8] X + [16] >= [8] X + [16] = c_5(len#(X)) add#(s(X),Y) = [8] X + [0] >= [8] X + [0] = c_8(activate#(X)) fst#(s(X),cons(Y,Z)) = [8] X + [8] Z + [8] >= [8] X + [8] Z + [8] = c_13(activate#(X),activate#(Z)) len#(cons(X,Z)) = [8] Z + [11] >= [8] Z + [3] = c_15(activate#(Z)) * Step 10: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: activate#(n__add(X1,X2)) -> c_2(add#(X1,X2)) activate#(n__fst(X1,X2)) -> c_4(fst#(X1,X2)) activate#(n__len(X)) -> c_5(len#(X)) add#(s(X),Y) -> c_8(activate#(X)) fst#(s(X),cons(Y,Z)) -> c_13(activate#(X),activate#(Z)) len#(cons(X,Z)) -> c_15(activate#(Z)) - Signature: {activate/1,add/2,from/1,fst/2,len/1,activate#/1,add#/2,from#/1,fst#/2,len#/1} / {0/0,cons/2,n__add/2 ,n__from/1,n__fst/2,n__len/1,nil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0 ,c_12/0,c_13/2,c_14/0,c_15/1,c_16/0} - Obligation: innermost runtime complexity wrt. defined symbols {activate#,add#,from#,fst#,len#} and constructors {0,cons ,n__add,n__from,n__fst,n__len,nil,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))