WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ADDLIST(z0,z1) -> c29(ADDLISTS(z0,z1,nil())) ADDLISTS(z0,z1,z2) -> c14(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,ISEMPTY(z0)) ADDLISTS(z0,z1,z2) -> c15(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,ISEMPTY(z1)) ADDLISTS(z0,z1,z2) -> c16(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,ISZERO(head(z0)) ,HEAD(z0)) ADDLISTS(z0,z1,z2) -> c17(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z0)) ADDLISTS(z0,z1,z2) -> c18(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z1)) ADDLISTS(z0,z1,z2) -> c19(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,P(head(z0)) ,HEAD(z0)) ADDLISTS(z0,z1,z2) -> c20(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z0)) ADDLISTS(z0,z1,z2) -> c21(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,INC(head(z1)) ,HEAD(z1)) ADDLISTS(z0,z1,z2) -> c22(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z1)) ADDLISTS(z0,z1,z2) -> c23(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,APPEND(z2,head(z1)) ,HEAD(z1)) APPEND(cons(z0,z1),z2) -> c8(APPEND(z1,z2)) APPEND(nil(),z0) -> c7() HEAD(cons(z0,z1)) -> c4() IF(false(),false(),false(),z0,z1,z2,z3,z4,z5) -> c27(ADDLISTS(z2,z3,z4)) IF(false(),false(),true(),z0,z1,z2,z3,z4,z5) -> c28(ADDLISTS(z0,z1,z5)) IF(false(),true(),z0,z1,z2,z3,z4,z5,z6) -> c26() IF(true(),false(),z0,z1,z2,z3,z4,z5,z6) -> c25() IF(true(),true(),z0,z1,z2,z3,z4,z5,z6) -> c24() INC(0()) -> c13() INC(s(z0)) -> c12(INC(z0)) ISEMPTY(cons(z0,z1)) -> c() ISEMPTY(nil()) -> c1() ISZERO(0()) -> c2() ISZERO(s(z0)) -> c3() P(0()) -> c11() P(s(0())) -> c10() P(s(s(z0))) -> c9(P(s(z0))) TAIL(cons(z0,z1)) -> c5() TAIL(nil()) -> c6() - Weak TRS: addList(z0,z1) -> addLists(z0,z1,nil()) addLists(z0,z1,z2) -> if(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) append(cons(z0,z1),z2) -> cons(z0,append(z1,z2)) append(nil(),z0) -> cons(z0,nil()) head(cons(z0,z1)) -> z0 if(false(),false(),false(),z0,z1,z2,z3,z4,z5) -> addLists(z2,z3,z4) if(false(),false(),true(),z0,z1,z2,z3,z4,z5) -> addLists(z0,z1,z5) if(false(),true(),z0,z1,z2,z3,z4,z5,z6) -> differentLengthError() if(true(),false(),z0,z1,z2,z3,z4,z5,z6) -> differentLengthError() if(true(),true(),z0,z1,z2,z3,z4,z5,z6) -> z5 inc(0()) -> s(0()) inc(s(z0)) -> s(inc(z0)) isEmpty(cons(z0,z1)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(z0)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(z0))) -> s(p(s(z0))) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() - Signature: {ADDLIST/2,ADDLISTS/3,APPEND/2,HEAD/1,IF/9,INC/1,ISEMPTY/1,ISZERO/1,P/1,TAIL/1,addList/2,addLists/3,append/2 ,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1} / {0/0,c/0,c1/0,c10/0,c11/0,c12/1,c13/0,c14/2,c15/2,c16/3 ,c17/2,c18/2,c19/3,c2/0,c20/2,c21/3,c22/2,c23/3,c24/0,c25/0,c26/0,c27/1,c28/1,c29/1,c3/0,c4/0,c5/0,c6/0,c7/0 ,c8/1,c9/1,cons/2,differentLengthError/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ADDLIST,ADDLISTS,APPEND,HEAD,IF,INC,ISEMPTY,ISZERO,P,TAIL ,addList,addLists,append,head,if,inc,isEmpty,isZero,p,tail} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c4,c5,c6,c7,c8,c9,cons,differentLengthError ,false,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ADDLIST(z0,z1) -> c29(ADDLISTS(z0,z1,nil())) ADDLISTS(z0,z1,z2) -> c14(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,ISEMPTY(z0)) ADDLISTS(z0,z1,z2) -> c15(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,ISEMPTY(z1)) ADDLISTS(z0,z1,z2) -> c16(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,ISZERO(head(z0)) ,HEAD(z0)) ADDLISTS(z0,z1,z2) -> c17(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z0)) ADDLISTS(z0,z1,z2) -> c18(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z1)) ADDLISTS(z0,z1,z2) -> c19(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,P(head(z0)) ,HEAD(z0)) ADDLISTS(z0,z1,z2) -> c20(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z0)) ADDLISTS(z0,z1,z2) -> c21(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,INC(head(z1)) ,HEAD(z1)) ADDLISTS(z0,z1,z2) -> c22(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z1)) ADDLISTS(z0,z1,z2) -> c23(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,APPEND(z2,head(z1)) ,HEAD(z1)) APPEND(cons(z0,z1),z2) -> c8(APPEND(z1,z2)) APPEND(nil(),z0) -> c7() HEAD(cons(z0,z1)) -> c4() IF(false(),false(),false(),z0,z1,z2,z3,z4,z5) -> c27(ADDLISTS(z2,z3,z4)) IF(false(),false(),true(),z0,z1,z2,z3,z4,z5) -> c28(ADDLISTS(z0,z1,z5)) IF(false(),true(),z0,z1,z2,z3,z4,z5,z6) -> c26() IF(true(),false(),z0,z1,z2,z3,z4,z5,z6) -> c25() IF(true(),true(),z0,z1,z2,z3,z4,z5,z6) -> c24() INC(0()) -> c13() INC(s(z0)) -> c12(INC(z0)) ISEMPTY(cons(z0,z1)) -> c() ISEMPTY(nil()) -> c1() ISZERO(0()) -> c2() ISZERO(s(z0)) -> c3() P(0()) -> c11() P(s(0())) -> c10() P(s(s(z0))) -> c9(P(s(z0))) TAIL(cons(z0,z1)) -> c5() TAIL(nil()) -> c6() - Weak TRS: addList(z0,z1) -> addLists(z0,z1,nil()) addLists(z0,z1,z2) -> if(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) append(cons(z0,z1),z2) -> cons(z0,append(z1,z2)) append(nil(),z0) -> cons(z0,nil()) head(cons(z0,z1)) -> z0 if(false(),false(),false(),z0,z1,z2,z3,z4,z5) -> addLists(z2,z3,z4) if(false(),false(),true(),z0,z1,z2,z3,z4,z5) -> addLists(z0,z1,z5) if(false(),true(),z0,z1,z2,z3,z4,z5,z6) -> differentLengthError() if(true(),false(),z0,z1,z2,z3,z4,z5,z6) -> differentLengthError() if(true(),true(),z0,z1,z2,z3,z4,z5,z6) -> z5 inc(0()) -> s(0()) inc(s(z0)) -> s(inc(z0)) isEmpty(cons(z0,z1)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(z0)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(z0))) -> s(p(s(z0))) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() - Signature: {ADDLIST/2,ADDLISTS/3,APPEND/2,HEAD/1,IF/9,INC/1,ISEMPTY/1,ISZERO/1,P/1,TAIL/1,addList/2,addLists/3,append/2 ,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1} / {0/0,c/0,c1/0,c10/0,c11/0,c12/1,c13/0,c14/2,c15/2,c16/3 ,c17/2,c18/2,c19/3,c2/0,c20/2,c21/3,c22/2,c23/3,c24/0,c25/0,c26/0,c27/1,c28/1,c29/1,c3/0,c4/0,c5/0,c6/0,c7/0 ,c8/1,c9/1,cons/2,differentLengthError/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ADDLIST,ADDLISTS,APPEND,HEAD,IF,INC,ISEMPTY,ISZERO,P,TAIL ,addList,addLists,append,head,if,inc,isEmpty,isZero,p,tail} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c4,c5,c6,c7,c8,c9,cons,differentLengthError ,false,nil,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: ADDLIST(z0,z1) -> c29(ADDLISTS(z0,z1,nil())) ADDLISTS(z0,z1,z2) -> c14(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,ISEMPTY(z0)) ADDLISTS(z0,z1,z2) -> c15(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,ISEMPTY(z1)) ADDLISTS(z0,z1,z2) -> c16(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,ISZERO(head(z0)) ,HEAD(z0)) ADDLISTS(z0,z1,z2) -> c17(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z0)) ADDLISTS(z0,z1,z2) -> c18(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z1)) ADDLISTS(z0,z1,z2) -> c19(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,P(head(z0)) ,HEAD(z0)) ADDLISTS(z0,z1,z2) -> c20(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z0)) ADDLISTS(z0,z1,z2) -> c21(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,INC(head(z1)) ,HEAD(z1)) ADDLISTS(z0,z1,z2) -> c22(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,TAIL(z1)) ADDLISTS(z0,z1,z2) -> c23(IF(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) ,APPEND(z2,head(z1)) ,HEAD(z1)) APPEND(cons(z0,z1),z2) -> c8(APPEND(z1,z2)) APPEND(nil(),z0) -> c7() HEAD(cons(z0,z1)) -> c4() IF(false(),false(),false(),z0,z1,z2,z3,z4,z5) -> c27(ADDLISTS(z2,z3,z4)) IF(false(),false(),true(),z0,z1,z2,z3,z4,z5) -> c28(ADDLISTS(z0,z1,z5)) IF(false(),true(),z0,z1,z2,z3,z4,z5,z6) -> c26() IF(true(),false(),z0,z1,z2,z3,z4,z5,z6) -> c25() IF(true(),true(),z0,z1,z2,z3,z4,z5,z6) -> c24() INC(0()) -> c13() INC(s(z0)) -> c12(INC(z0)) ISEMPTY(cons(z0,z1)) -> c() ISEMPTY(nil()) -> c1() ISZERO(0()) -> c2() ISZERO(s(z0)) -> c3() P(0()) -> c11() P(s(0())) -> c10() P(s(s(z0))) -> c9(P(s(z0))) TAIL(cons(z0,z1)) -> c5() TAIL(nil()) -> c6() - Weak TRS: addList(z0,z1) -> addLists(z0,z1,nil()) addLists(z0,z1,z2) -> if(isEmpty(z0) ,isEmpty(z1) ,isZero(head(z0)) ,tail(z0) ,tail(z1) ,cons(p(head(z0)),tail(z0)) ,cons(inc(head(z1)),tail(z1)) ,z2 ,append(z2,head(z1))) append(cons(z0,z1),z2) -> cons(z0,append(z1,z2)) append(nil(),z0) -> cons(z0,nil()) head(cons(z0,z1)) -> z0 if(false(),false(),false(),z0,z1,z2,z3,z4,z5) -> addLists(z2,z3,z4) if(false(),false(),true(),z0,z1,z2,z3,z4,z5) -> addLists(z0,z1,z5) if(false(),true(),z0,z1,z2,z3,z4,z5,z6) -> differentLengthError() if(true(),false(),z0,z1,z2,z3,z4,z5,z6) -> differentLengthError() if(true(),true(),z0,z1,z2,z3,z4,z5,z6) -> z5 inc(0()) -> s(0()) inc(s(z0)) -> s(inc(z0)) isEmpty(cons(z0,z1)) -> false() isEmpty(nil()) -> true() isZero(0()) -> true() isZero(s(z0)) -> false() p(0()) -> 0() p(s(0())) -> 0() p(s(s(z0))) -> s(p(s(z0))) tail(cons(z0,z1)) -> z1 tail(nil()) -> nil() - Signature: {ADDLIST/2,ADDLISTS/3,APPEND/2,HEAD/1,IF/9,INC/1,ISEMPTY/1,ISZERO/1,P/1,TAIL/1,addList/2,addLists/3,append/2 ,head/1,if/9,inc/1,isEmpty/1,isZero/1,p/1,tail/1} / {0/0,c/0,c1/0,c10/0,c11/0,c12/1,c13/0,c14/2,c15/2,c16/3 ,c17/2,c18/2,c19/3,c2/0,c20/2,c21/3,c22/2,c23/3,c24/0,c25/0,c26/0,c27/1,c28/1,c29/1,c3/0,c4/0,c5/0,c6/0,c7/0 ,c8/1,c9/1,cons/2,differentLengthError/0,false/0,nil/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ADDLIST,ADDLISTS,APPEND,HEAD,IF,INC,ISEMPTY,ISZERO,P,TAIL ,addList,addLists,append,head,if,inc,isEmpty,isZero,p,tail} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c4,c5,c6,c7,c8,c9,cons,differentLengthError ,false,nil,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: APPEND(y,z){y -> cons(x,y)} = APPEND(cons(x,y),z) ->^+ c8(APPEND(y,z)) = C[APPEND(y,z) = APPEND(y,z){}] WORST_CASE(Omega(n^1),?)