WORST_CASE(?,O(n^1)) * Step 1: Sum WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 2nd(cons(X,XS)) -> head(activate(XS)) activate(X) -> X activate(n__from(X)) -> from(X) activate(n__take(X1,X2)) -> take(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) head(cons(X,XS)) -> X sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) - Signature: {2nd/1,activate/1,from/1,head/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__take/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,sel,take} and constructors {0,cons ,n__from,n__take,nil,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 2nd(cons(X,XS)) -> head(activate(XS)) activate(X) -> X activate(n__from(X)) -> from(X) activate(n__take(X1,X2)) -> take(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) head(cons(X,XS)) -> X sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) - Signature: {2nd/1,activate/1,from/1,head/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__take/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,sel,take} and constructors {0,cons ,n__from,n__take,nil,s} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(cons) = {2}, uargs(head) = {1}, uargs(n__take) = {2}, uargs(sel) = {2} Following symbols are considered usable: {2nd,activate,from,head,sel,take} TcT has computed the following interpretation: p(0) = 1 p(2nd) = 11 + 8*x1 p(activate) = x1 p(cons) = x1 + x2 p(from) = 4 + x1 p(head) = 4 + 2*x1 p(n__from) = 4 + x1 p(n__take) = x2 p(nil) = 0 p(s) = 0 p(sel) = 8*x2 p(take) = x2 Following rules are strictly oriented: 2nd(cons(X,XS)) = 11 + 8*X + 8*XS > 4 + 2*XS = head(activate(XS)) head(cons(X,XS)) = 4 + 2*X + 2*XS > X = X Following rules are (at-least) weakly oriented: activate(X) = X >= X = X activate(n__from(X)) = 4 + X >= 4 + X = from(X) activate(n__take(X1,X2)) = X2 >= X2 = take(X1,X2) from(X) = 4 + X >= 4 + X = cons(X,n__from(s(X))) from(X) = 4 + X >= 4 + X = n__from(X) sel(0(),cons(X,XS)) = 8*X + 8*XS >= X = X sel(s(N),cons(X,XS)) = 8*X + 8*XS >= 8*XS = sel(N,activate(XS)) take(X1,X2) = X2 >= X2 = n__take(X1,X2) take(0(),XS) = XS >= 0 = nil() take(s(N),cons(X,XS)) = X + XS >= X + XS = cons(X,n__take(N,activate(XS))) * Step 3: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__from(X)) -> from(X) activate(n__take(X1,X2)) -> take(X1,X2) from(X) -> cons(X,n__from(s(X))) from(X) -> n__from(X) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) - Weak TRS: 2nd(cons(X,XS)) -> head(activate(XS)) head(cons(X,XS)) -> X - Signature: {2nd/1,activate/1,from/1,head/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__take/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,sel,take} and constructors {0,cons ,n__from,n__take,nil,s} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(cons) = {2}, uargs(head) = {1}, uargs(n__take) = {2}, uargs(sel) = {2} Following symbols are considered usable: {2nd,activate,from,head,sel,take} TcT has computed the following interpretation: p(0) = 1 p(2nd) = 12 + 2*x1 p(activate) = 6 + x1 p(cons) = 6 + x1 + x2 p(from) = 7 + x1 p(head) = 2*x1 p(n__from) = 1 + x1 p(n__take) = 5 + x2 p(nil) = 0 p(s) = 0 p(sel) = 4 + 2*x2 p(take) = 11 + x2 Following rules are strictly oriented: activate(X) = 6 + X > X = X from(X) = 7 + X > 1 + X = n__from(X) sel(0(),cons(X,XS)) = 16 + 2*X + 2*XS > X = X take(X1,X2) = 11 + X2 > 5 + X2 = n__take(X1,X2) take(0(),XS) = 11 + XS > 0 = nil() Following rules are (at-least) weakly oriented: 2nd(cons(X,XS)) = 24 + 2*X + 2*XS >= 12 + 2*XS = head(activate(XS)) activate(n__from(X)) = 7 + X >= 7 + X = from(X) activate(n__take(X1,X2)) = 11 + X2 >= 11 + X2 = take(X1,X2) from(X) = 7 + X >= 7 + X = cons(X,n__from(s(X))) head(cons(X,XS)) = 12 + 2*X + 2*XS >= X = X sel(s(N),cons(X,XS)) = 16 + 2*X + 2*XS >= 16 + 2*XS = sel(N,activate(XS)) take(s(N),cons(X,XS)) = 17 + X + XS >= 17 + X + XS = cons(X,n__take(N,activate(XS))) * Step 4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(n__from(X)) -> from(X) activate(n__take(X1,X2)) -> take(X1,X2) from(X) -> cons(X,n__from(s(X))) sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS))) - Weak TRS: 2nd(cons(X,XS)) -> head(activate(XS)) activate(X) -> X from(X) -> n__from(X) head(cons(X,XS)) -> X sel(0(),cons(X,XS)) -> X take(X1,X2) -> n__take(X1,X2) take(0(),XS) -> nil() - Signature: {2nd/1,activate/1,from/1,head/1,sel/2,take/2} / {0/0,cons/2,n__from/1,n__take/2,nil/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,activate,from,head,sel,take} and constructors {0,cons ,n__from,n__take,nil,s} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 5, araRuleShifting = Nothing} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(15) 0 :: [] -(0)-> "A"(9) 2nd :: ["A"(10)] -(15)-> "A"(0) activate :: ["A"(9)] -(13)-> "A"(9) cons :: ["A"(0) x "A"(9)] -(0)-> "A"(9) cons :: ["A"(0) x "A"(10)] -(0)-> "A"(10) cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) from :: ["A"(0)] -(12)-> "A"(9) head :: ["A"(0)] -(0)-> "A"(0) n__from :: ["A"(0)] -(0)-> "A"(9) n__from :: ["A"(0)] -(0)-> "A"(12) n__from :: ["A"(0)] -(0)-> "A"(13) n__take :: ["A"(9) x "A"(9)] -(0)-> "A"(9) nil :: [] -(0)-> "A"(14) s :: ["A"(15)] -(15)-> "A"(15) s :: ["A"(9)] -(9)-> "A"(9) s :: ["A"(0)] -(0)-> "A"(0) sel :: ["A"(15) x "A"(9)] -(3)-> "A"(0) take :: ["A"(9) x "A"(9)] -(12)-> "A"(9) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "cons_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "n__from_A" :: ["A"(0)] -(0)-> "A"(1) "n__take_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "s_A" :: ["A"(1)] -(1)-> "A"(1) WORST_CASE(?,O(n^1))