WORST_CASE(?,O(n^1)) * Step 1: InnermostRuleRemoval WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) natsFrom(X) -> n__natsFrom(X) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) splitAt(s(N),cons(X,XS)) -> u(splitAt(N,activate(XS)),N,X,activate(XS)) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. splitAt(s(N),cons(X,XS)) -> u(splitAt(N,activate(XS)),N,X,activate(XS)) All above mentioned rules can be savely removed. * Step 2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) natsFrom(X) -> n__natsFrom(X) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(22)] -(7)-> A(7) afterNth :: [A(17) x A(15)] -(31)-> A(6) cons :: [A(0) x A(3)] -(0)-> A(3) cons :: [A(0) x A(29)] -(0)-> A(29) cons :: [A(0) x A(7)] -(0)-> A(7) cons :: [A(0) x A(2)] -(0)-> A(2) fst :: [A(0)] -(15)-> A(0) head :: [A(3)] -(0)-> A(0) n__natsFrom :: [A(22)] -(22)-> A(22) n__natsFrom :: [A(7)] -(7)-> A(7) n__s :: [A(22)] -(22)-> A(22) n__s :: [A(7)] -(7)-> A(7) natsFrom :: [A(7)] -(19)-> A(7) nil :: [] -(0)-> A(30) pair :: [A(0) x A(0)] -(0)-> A(0) pair :: [A(14) x A(14)] -(0)-> A(14) pair :: [A(31) x A(31)] -(0)-> A(31) pair :: [A(2) x A(2)] -(0)-> A(2) s :: [A(7)] -(15)-> A(7) sel :: [A(31) x A(19)] -(31)-> A(0) snd :: [A(14)] -(2)-> A(8) splitAt :: [A(2) x A(15)] -(15)-> A(14) tail :: [A(29)] -(16)-> A(0) take :: [A(28) x A(17)] -(31)-> A(0) u :: [A(31) x A(0) x A(24) x A(0)] -(16)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(0)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(1) x A(1)] -(0)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: natsFrom(X) -> n__natsFrom(X) snd(pair(XS,YS)) -> YS tail(cons(N,XS)) -> activate(XS) 2. Weak: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) splitAt(0(),XS) -> pair(nil(),XS) take(N,XS) -> fst(splitAt(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) * Step 3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) splitAt(0(),XS) -> pair(nil(),XS) take(N,XS) -> fst(splitAt(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Weak TRS: natsFrom(X) -> n__natsFrom(X) snd(pair(XS,YS)) -> YS tail(cons(N,XS)) -> activate(XS) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(11)] -(7)-> A(0) afterNth :: [A(17) x A(30)] -(30)-> A(16) cons :: [A(9) x A(9)] -(9)-> A(9) cons :: [A(31) x A(31)] -(31)-> A(31) cons :: [A(0) x A(0)] -(0)-> A(0) fst :: [A(22)] -(15)-> A(0) head :: [A(9)] -(0)-> A(9) n__natsFrom :: [A(11)] -(11)-> A(11) n__natsFrom :: [A(0)] -(0)-> A(0) n__s :: [A(11)] -(11)-> A(11) n__s :: [A(0)] -(0)-> A(0) natsFrom :: [A(0)] -(2)-> A(0) nil :: [] -(0)-> A(28) pair :: [A(0) x A(22)] -(0)-> A(22) pair :: [A(0) x A(0)] -(0)-> A(0) pair :: [A(0) x A(18)] -(0)-> A(18) pair :: [A(0) x A(28)] -(0)-> A(28) s :: [A(0)] -(7)-> A(0) sel :: [A(31) x A(30)] -(31)-> A(2) snd :: [A(18)] -(2)-> A(16) splitAt :: [A(2) x A(29)] -(1)-> A(22) tail :: [A(31)] -(0)-> A(0) take :: [A(28) x A(31)] -(30)-> A(0) u :: [A(0) x A(0) x A(21) x A(0)] -(31)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(1) x A(1)] -(1)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(0) x A(1)] -(0)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: activate(n__s(X)) -> s(activate(X)) splitAt(0(),XS) -> pair(nil(),XS) take(N,XS) -> fst(splitAt(N,XS)) 2. Weak: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) * Step 4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Weak TRS: activate(n__s(X)) -> s(activate(X)) natsFrom(X) -> n__natsFrom(X) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(15)] -(15)-> A(0) afterNth :: [A(9) x A(14)] -(11)-> A(8) cons :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(15) x A(15)] -(0)-> A(15) fst :: [A(8)] -(0)-> A(0) head :: [A(0)] -(0)-> A(0) n__natsFrom :: [A(15)] -(15)-> A(15) n__natsFrom :: [A(0)] -(0)-> A(0) n__s :: [A(15)] -(15)-> A(15) n__s :: [A(0)] -(0)-> A(0) natsFrom :: [A(0)] -(15)-> A(0) nil :: [] -(0)-> A(12) pair :: [A(0) x A(8)] -(8)-> A(8) pair :: [A(0) x A(15)] -(15)-> A(15) pair :: [A(0) x A(3)] -(3)-> A(3) s :: [A(0)] -(7)-> A(0) sel :: [A(15) x A(14)] -(15)-> A(0) snd :: [A(8)] -(1)-> A(8) splitAt :: [A(2) x A(11)] -(8)-> A(8) tail :: [A(15)] -(15)-> A(0) take :: [A(12) x A(15)] -(14)-> A(0) u :: [A(15) x A(0) x A(15) x A(0)] -(11)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(1) x A(1)] -(0)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(0) x A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: fst(pair(XS,YS)) -> XS 2. Weak: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) * Step 5: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Weak TRS: activate(n__s(X)) -> s(activate(X)) fst(pair(XS,YS)) -> XS natsFrom(X) -> n__natsFrom(X) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(15)] -(11)-> A(4) afterNth :: [A(9) x A(14)] -(11)-> A(2) cons :: [A(0) x A(1)] -(0)-> A(1) cons :: [A(0) x A(15)] -(0)-> A(15) cons :: [A(0) x A(4)] -(0)-> A(4) fst :: [A(9)] -(2)-> A(5) head :: [A(1)] -(4)-> A(0) n__natsFrom :: [A(15)] -(15)-> A(15) n__natsFrom :: [A(4)] -(4)-> A(4) n__s :: [A(15)] -(0)-> A(15) n__s :: [A(4)] -(0)-> A(4) natsFrom :: [A(4)] -(15)-> A(4) nil :: [] -(0)-> A(15) pair :: [A(14) x A(14)] -(14)-> A(14) pair :: [A(9) x A(9)] -(9)-> A(9) pair :: [A(0) x A(0)] -(0)-> A(0) s :: [A(4)] -(0)-> A(4) sel :: [A(15) x A(14)] -(15)-> A(0) snd :: [A(9)] -(0)-> A(5) splitAt :: [A(2) x A(13)] -(10)-> A(9) tail :: [A(15)] -(15)-> A(2) take :: [A(12) x A(15)] -(15)-> A(2) u :: [A(14) x A(0) x A(15) x A(0)] -(6)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(0)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(0)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(1) x A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: head(cons(N,XS)) -> N 2. Weak: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) * Step 6: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Weak TRS: activate(n__s(X)) -> s(activate(X)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(X) -> n__natsFrom(X) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(7)] -(4)-> A(0) afterNth :: [A(9) x A(6)] -(7)-> A(0) cons :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(0) x A(15)] -(0)-> A(15) cons :: [A(0) x A(7)] -(0)-> A(7) fst :: [A(0)] -(0)-> A(0) head :: [A(0)] -(1)-> A(0) n__natsFrom :: [A(7)] -(7)-> A(7) n__natsFrom :: [A(0)] -(0)-> A(0) n__s :: [A(7)] -(7)-> A(7) n__s :: [A(0)] -(0)-> A(0) natsFrom :: [A(0)] -(2)-> A(0) nil :: [] -(0)-> A(12) pair :: [A(9) x A(9)] -(9)-> A(9) pair :: [A(0) x A(0)] -(0)-> A(0) pair :: [A(3) x A(3)] -(3)-> A(3) s :: [A(0)] -(1)-> A(0) sel :: [A(15) x A(10)] -(15)-> A(0) snd :: [A(0)] -(0)-> A(0) splitAt :: [A(2) x A(5)] -(1)-> A(0) tail :: [A(15)] -(12)-> A(0) take :: [A(12) x A(11)] -(14)-> A(0) u :: [A(9) x A(0) x A(9) x A(0)] -(7)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(0)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(1) x A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: activate(X) -> X 2. Weak: activate(n__natsFrom(X)) -> natsFrom(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) * Step 7: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: activate(n__natsFrom(X)) -> natsFrom(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Weak TRS: activate(X) -> X activate(n__s(X)) -> s(activate(X)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(X) -> n__natsFrom(X) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(5)] -(1)-> A(0) afterNth :: [A(9) x A(6)] -(11)-> A(0) cons :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(0) x A(15)] -(0)-> A(15) cons :: [A(0) x A(7)] -(0)-> A(7) fst :: [A(0)] -(0)-> A(0) head :: [A(0)] -(0)-> A(0) n__natsFrom :: [A(5)] -(5)-> A(5) n__natsFrom :: [A(0)] -(0)-> A(0) n__s :: [A(5)] -(5)-> A(5) n__s :: [A(0)] -(0)-> A(0) natsFrom :: [A(0)] -(4)-> A(0) nil :: [] -(0)-> A(12) pair :: [A(10) x A(10)] -(10)-> A(10) pair :: [A(0) x A(0)] -(0)-> A(0) pair :: [A(3) x A(3)] -(3)-> A(3) s :: [A(0)] -(0)-> A(0) sel :: [A(15) x A(10)] -(15)-> A(0) snd :: [A(0)] -(2)-> A(0) splitAt :: [A(2) x A(5)] -(3)-> A(0) tail :: [A(15)] -(14)-> A(0) take :: [A(12) x A(11)] -(15)-> A(0) u :: [A(10) x A(0) x A(11) x A(0)] -(15)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(0)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(1) x A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: activate(n__natsFrom(X)) -> natsFrom(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) 2. Weak: natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) * Step 8: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Weak TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(X) -> n__natsFrom(X) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(15)] -(5)-> A(0) afterNth :: [A(9) x A(12)] -(9)-> A(0) cons :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(15) x A(15)] -(15)-> A(15) fst :: [A(1)] -(2)-> A(1) head :: [A(0)] -(0)-> A(0) n__natsFrom :: [A(15)] -(15)-> A(15) n__natsFrom :: [A(0)] -(0)-> A(0) n__s :: [A(15)] -(15)-> A(15) n__s :: [A(0)] -(0)-> A(0) natsFrom :: [A(0)] -(15)-> A(0) nil :: [] -(0)-> A(10) pair :: [A(0) x A(0)] -(0)-> A(0) pair :: [A(1) x A(1)] -(1)-> A(1) pair :: [A(2) x A(2)] -(2)-> A(2) pair :: [A(3) x A(3)] -(3)-> A(3) s :: [A(0)] -(1)-> A(0) sel :: [A(15) x A(14)] -(15)-> A(0) snd :: [A(2)] -(1)-> A(0) splitAt :: [A(2) x A(10)] -(3)-> A(3) tail :: [A(15)] -(15)-> A(0) take :: [A(12) x A(14)] -(15)-> A(0) u :: [A(0) x A(0) x A(15) x A(0)] -(7)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(1) x A(1)] -(1)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(1) x A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: s(X) -> n__s(X) 2. Weak: natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) * Step 9: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Weak TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(X) -> n__natsFrom(X) s(X) -> n__s(X) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(15)] -(11)-> A(4) afterNth :: [A(9) x A(5)] -(8)-> A(0) cons :: [A(0) x A(0)] -(0)-> A(0) cons :: [A(0) x A(15)] -(0)-> A(15) cons :: [A(0) x A(4)] -(0)-> A(4) fst :: [A(1)] -(0)-> A(0) head :: [A(0)] -(1)-> A(0) n__natsFrom :: [A(15)] -(15)-> A(15) n__natsFrom :: [A(4)] -(4)-> A(4) n__s :: [A(15)] -(0)-> A(15) n__s :: [A(4)] -(0)-> A(4) natsFrom :: [A(4)] -(12)-> A(4) nil :: [] -(0)-> A(12) pair :: [A(0) x A(0)] -(10)-> A(10) pair :: [A(0) x A(0)] -(1)-> A(1) pair :: [A(0) x A(0)] -(0)-> A(0) pair :: [A(0) x A(0)] -(2)-> A(2) s :: [A(4)] -(0)-> A(4) sel :: [A(15) x A(11)] -(15)-> A(0) snd :: [A(1)] -(1)-> A(0) splitAt :: [A(2) x A(5)] -(3)-> A(2) tail :: [A(15)] -(15)-> A(2) take :: [A(12) x A(11)] -(15)-> A(0) u :: [A(10) x A(0) x A(15) x A(0)] -(6)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(0)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(0)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(0) x A(0)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) 2. Weak: sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) * Step 10: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: sel(N,XS) -> head(afterNth(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Weak TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) natsFrom(X) -> n__natsFrom(X) s(X) -> n__s(X) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(13)] -(13)-> A(1) afterNth :: [A(9) x A(15)] -(3)-> A(9) cons :: [A(0) x A(9)] -(0)-> A(9) cons :: [A(0) x A(14)] -(0)-> A(14) cons :: [A(0) x A(5)] -(0)-> A(5) cons :: [A(0) x A(1)] -(0)-> A(1) fst :: [A(3)] -(0)-> A(1) head :: [A(9)] -(6)-> A(0) n__natsFrom :: [A(13)] -(13)-> A(13) n__natsFrom :: [A(1)] -(1)-> A(1) n__s :: [A(13)] -(13)-> A(13) n__s :: [A(1)] -(1)-> A(1) natsFrom :: [A(1)] -(8)-> A(1) nil :: [] -(0)-> A(15) pair :: [A(8) x A(8)] -(0)-> A(8) pair :: [A(3) x A(3)] -(0)-> A(3) pair :: [A(9) x A(9)] -(0)-> A(9) pair :: [A(1) x A(1)] -(0)-> A(1) pair :: [A(15) x A(15)] -(0)-> A(15) s :: [A(1)] -(8)-> A(1) sel :: [A(15) x A(15)] -(15)-> A(0) snd :: [A(9)] -(1)-> A(9) splitAt :: [A(2) x A(15)] -(1)-> A(10) tail :: [A(14)] -(13)-> A(0) take :: [A(12) x A(15)] -(15)-> A(0) u :: [A(8) x A(0) x A(15) x A(0)] -(15)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(0)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(1) x A(1)] -(0)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) 2. Weak: sel(N,XS) -> head(afterNth(N,XS)) * Step 11: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: sel(N,XS) -> head(afterNth(N,XS)) - Weak TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) natsFrom(X) -> n__natsFrom(X) s(X) -> n__s(X) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> A(2) activate :: [A(9)] -(11)-> A(4) afterNth :: [A(9) x A(12)] -(9)-> A(1) cons :: [A(0) x A(1)] -(0)-> A(1) cons :: [A(0) x A(15)] -(0)-> A(15) cons :: [A(0) x A(4)] -(0)-> A(4) cons :: [A(0) x A(3)] -(0)-> A(3) fst :: [A(3)] -(0)-> A(1) head :: [A(1)] -(0)-> A(0) n__natsFrom :: [A(9)] -(9)-> A(9) n__natsFrom :: [A(4)] -(4)-> A(4) n__s :: [A(9)] -(9)-> A(9) n__s :: [A(4)] -(4)-> A(4) natsFrom :: [A(4)] -(8)-> A(4) nil :: [] -(0)-> A(15) pair :: [A(3) x A(3)] -(3)-> A(3) pair :: [A(2) x A(2)] -(2)-> A(2) pair :: [A(13) x A(13)] -(13)-> A(13) pair :: [A(5) x A(5)] -(5)-> A(5) s :: [A(4)] -(5)-> A(4) sel :: [A(15) x A(14)] -(15)-> A(0) snd :: [A(2)] -(1)-> A(1) splitAt :: [A(2) x A(10)] -(5)-> A(4) tail :: [A(15)] -(15)-> A(2) take :: [A(12) x A(14)] -(15)-> A(0) u :: [A(13) x A(0) x A(15) x A(0)] -(13)-> A(0) Cost-free Signatures used: -------------------------- activate :: [A_cf(0)] -(0)-> A_cf(0) cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) n__natsFrom :: [A_cf(0)] -(0)-> A_cf(0) n__s :: [A_cf(0)] -(0)-> A_cf(0) natsFrom :: [A_cf(0)] -(0)-> A_cf(0) s :: [A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) cons_A :: [A(0) x A(1)] -(0)-> A(1) n__natsFrom_A :: [A(0)] -(1)-> A(1) n__s_A :: [A(0)] -(1)-> A(1) nil_A :: [] -(0)-> A(1) pair_A :: [A(1) x A(1)] -(1)-> A(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: sel(N,XS) -> head(afterNth(N,XS)) 2. Weak: * Step 12: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: activate(X) -> X activate(n__natsFrom(X)) -> natsFrom(activate(X)) activate(n__s(X)) -> s(activate(X)) afterNth(N,XS) -> snd(splitAt(N,XS)) fst(pair(XS,YS)) -> XS head(cons(N,XS)) -> N natsFrom(N) -> cons(N,n__natsFrom(n__s(N))) natsFrom(X) -> n__natsFrom(X) s(X) -> n__s(X) sel(N,XS) -> head(afterNth(N,XS)) snd(pair(XS,YS)) -> YS splitAt(0(),XS) -> pair(nil(),XS) tail(cons(N,XS)) -> activate(XS) take(N,XS) -> fst(splitAt(N,XS)) u(pair(YS,ZS),N,X,XS) -> pair(cons(activate(X),YS),ZS) - Signature: {activate/1,afterNth/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,cons/2 ,n__natsFrom/1,n__s/1,nil/0,pair/2} - Obligation: innermost runtime complexity wrt. defined symbols {activate,afterNth,fst,head,natsFrom,s,sel,snd,splitAt ,tail,take,u} and constructors {0,cons,n__natsFrom,n__s,nil,pair} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))