WORST_CASE(?,O(n^1)) * Step 1: Sum. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0)) AFTERNTH(z0,z1) -> c12(SND(splitAt(z0,z1)),SPLITAT(z0,z1)) FST(pair(z0,z1)) -> c2() HEAD(cons(z0,z1)) -> c8() NATSFROM(z0) -> c() NATSFROM(z0) -> c1() SEL(z0,z1) -> c10(HEAD(afterNth(z0,z1)),AFTERNTH(z0,z1)) SND(pair(z0,z1)) -> c3() SPLITAT(0(),z0) -> c4() SPLITAT(s(z0),cons(z1,z2)) -> c5(U(splitAt(z0,activate(z2)),z0,z1,activate(z2)) ,SPLITAT(z0,activate(z2)) ,ACTIVATE(z2)) SPLITAT(s(z0),cons(z1,z2)) -> c6(U(splitAt(z0,activate(z2)),z0,z1,activate(z2)),ACTIVATE(z2)) TAIL(cons(z0,z1)) -> c9(ACTIVATE(z1)) TAKE(z0,z1) -> c11(FST(splitAt(z0,z1)),SPLITAT(z0,z1)) U(pair(z0,z1),z2,z3,z4) -> c7(ACTIVATE(z3)) - Weak TRS: activate(z0) -> z0 activate(n__natsFrom(z0)) -> natsFrom(z0) afterNth(z0,z1) -> snd(splitAt(z0,z1)) fst(pair(z0,z1)) -> z0 head(cons(z0,z1)) -> z0 natsFrom(z0) -> cons(z0,n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0,z1) -> head(afterNth(z0,z1)) snd(pair(z0,z1)) -> z1 splitAt(0(),z0) -> pair(nil(),z0) splitAt(s(z0),cons(z1,z2)) -> u(splitAt(z0,activate(z2)),z0,z1,activate(z2)) tail(cons(z0,z1)) -> activate(z1) take(z0,z1) -> fst(splitAt(z0,z1)) u(pair(z0,z1),z2,z3,z4) -> pair(cons(activate(z3),z0),z1) - Signature: {ACTIVATE/1,AFTERNTH/2,FST/1,HEAD/1,NATSFROM/1,SEL/2,SND/1,SPLITAT/2,TAIL/1,TAKE/2,U/4,activate/1,afterNth/2 ,fst/1,head/1,natsFrom/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,c/0,c1/0,c10/2,c11/2,c12/2,c13/1 ,c14/0,c2/0,c3/0,c4/0,c5/3,c6/2,c7/1,c8/0,c9/1,cons/2,n__natsFrom/1,nil/0,pair/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,AFTERNTH,FST,HEAD,NATSFROM,SEL,SND,SPLITAT,TAIL ,TAKE,U,activate,afterNth,fst,head,natsFrom,sel,snd,splitAt,tail,take,u} and constructors {0,c,c1,c10,c11 ,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__natsFrom,nil,pair,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Ara. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: ACTIVATE(z0) -> c14() ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0)) AFTERNTH(z0,z1) -> c12(SND(splitAt(z0,z1)),SPLITAT(z0,z1)) FST(pair(z0,z1)) -> c2() HEAD(cons(z0,z1)) -> c8() NATSFROM(z0) -> c() NATSFROM(z0) -> c1() SEL(z0,z1) -> c10(HEAD(afterNth(z0,z1)),AFTERNTH(z0,z1)) SND(pair(z0,z1)) -> c3() SPLITAT(0(),z0) -> c4() SPLITAT(s(z0),cons(z1,z2)) -> c5(U(splitAt(z0,activate(z2)),z0,z1,activate(z2)) ,SPLITAT(z0,activate(z2)) ,ACTIVATE(z2)) SPLITAT(s(z0),cons(z1,z2)) -> c6(U(splitAt(z0,activate(z2)),z0,z1,activate(z2)),ACTIVATE(z2)) TAIL(cons(z0,z1)) -> c9(ACTIVATE(z1)) TAKE(z0,z1) -> c11(FST(splitAt(z0,z1)),SPLITAT(z0,z1)) U(pair(z0,z1),z2,z3,z4) -> c7(ACTIVATE(z3)) - Weak TRS: activate(z0) -> z0 activate(n__natsFrom(z0)) -> natsFrom(z0) afterNth(z0,z1) -> snd(splitAt(z0,z1)) fst(pair(z0,z1)) -> z0 head(cons(z0,z1)) -> z0 natsFrom(z0) -> cons(z0,n__natsFrom(s(z0))) natsFrom(z0) -> n__natsFrom(z0) sel(z0,z1) -> head(afterNth(z0,z1)) snd(pair(z0,z1)) -> z1 splitAt(0(),z0) -> pair(nil(),z0) splitAt(s(z0),cons(z1,z2)) -> u(splitAt(z0,activate(z2)),z0,z1,activate(z2)) tail(cons(z0,z1)) -> activate(z1) take(z0,z1) -> fst(splitAt(z0,z1)) u(pair(z0,z1),z2,z3,z4) -> pair(cons(activate(z3),z0),z1) - Signature: {ACTIVATE/1,AFTERNTH/2,FST/1,HEAD/1,NATSFROM/1,SEL/2,SND/1,SPLITAT/2,TAIL/1,TAKE/2,U/4,activate/1,afterNth/2 ,fst/1,head/1,natsFrom/1,sel/2,snd/1,splitAt/2,tail/1,take/2,u/4} / {0/0,c/0,c1/0,c10/2,c11/2,c12/2,c13/1 ,c14/0,c2/0,c3/0,c4/0,c5/3,c6/2,c7/1,c8/0,c9/1,cons/2,n__natsFrom/1,nil/0,pair/2,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ACTIVATE,AFTERNTH,FST,HEAD,NATSFROM,SEL,SND,SPLITAT,TAIL ,TAKE,U,activate,afterNth,fst,head,natsFrom,sel,snd,splitAt,tail,take,u} and constructors {0,c,c1,c10,c11 ,c12,c13,c14,c2,c3,c4,c5,c6,c7,c8,c9,cons,n__natsFrom,nil,pair,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(6) F (TrsFun "0") :: [] -(0)-> "A"(0) F (TrsFun "ACTIVATE") :: ["A"(0)] -(2)-> "A"(0) F (TrsFun "AFTERNTH") :: ["A"(6) x "A"(0)] -(3)-> "A"(0) F (TrsFun "FST") :: ["A"(0)] -(1)-> "A"(0) F (TrsFun "HEAD") :: ["A"(0)] -(1)-> "A"(0) F (TrsFun "NATSFROM") :: ["A"(0)] -(1)-> "A"(0) F (TrsFun "SEL") :: ["A"(6) x "A"(0)] -(5)-> "A"(0) F (TrsFun "SND") :: ["A"(0)] -(1)-> "A"(0) F (TrsFun "SPLITAT") :: ["A"(6) x "A"(0)] -(1)-> "A"(0) F (TrsFun "TAIL") :: ["A"(0)] -(3)-> "A"(0) F (TrsFun "TAKE") :: ["A"(6) x "A"(0)] -(3)-> "A"(0) F (TrsFun "U") :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(3)-> "A"(0) F (TrsFun "activate") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "afterNth") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c") :: [] -(0)-> "A"(0) F (TrsFun "c1") :: [] -(0)-> "A"(0) F (TrsFun "c10") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c11") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c12") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c13") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c14") :: [] -(0)-> "A"(0) F (TrsFun "c2") :: [] -(0)-> "A"(0) F (TrsFun "c3") :: [] -(0)-> "A"(0) F (TrsFun "c4") :: [] -(0)-> "A"(0) F (TrsFun "c5") :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c6") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c7") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c8") :: [] -(0)-> "A"(0) F (TrsFun "c9") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "fst") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "head") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "n__natsFrom") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "natsFrom") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "pair") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "s") :: ["A"(6)] -(6)-> "A"(6) F (TrsFun "s") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "sel") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "snd") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "splitAt") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "tail") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "take") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "u") :: ["A"(0) x "A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: ACTIVATE(z0) -> c14() ACTIVATE(n__natsFrom(z0)) -> c13(NATSFROM(z0)) AFTERNTH(z0,z1) -> c12(SND(splitAt(z0,z1)),SPLITAT(z0,z1)) FST(pair(z0,z1)) -> c2() HEAD(cons(z0,z1)) -> c8() NATSFROM(z0) -> c() NATSFROM(z0) -> c1() SEL(z0,z1) -> c10(HEAD(afterNth(z0,z1)),AFTERNTH(z0,z1)) SND(pair(z0,z1)) -> c3() SPLITAT(0(),z0) -> c4() SPLITAT(s(z0),cons(z1,z2)) -> c5(U(splitAt(z0,activate(z2)),z0,z1,activate(z2)) ,SPLITAT(z0,activate(z2)) ,ACTIVATE(z2)) SPLITAT(s(z0),cons(z1,z2)) -> c6(U(splitAt(z0,activate(z2)),z0,z1,activate(z2)),ACTIVATE(z2)) TAIL(cons(z0,z1)) -> c9(ACTIVATE(z1)) TAKE(z0,z1) -> c11(FST(splitAt(z0,z1)),SPLITAT(z0,z1)) U(pair(z0,z1),z2,z3,z4) -> c7(ACTIVATE(z3)) 2. Weak: WORST_CASE(?,O(n^1))