WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c1() A__AND(tt(),z0) -> c(MARK(z0)) A__ISNAT(z0) -> c10() A__ISNAT(0()) -> c7() A__ISNAT(length(z0)) -> c9(A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c8(A__ISNAT(z0)) A__ISNATILIST(z0) -> c2(A__ISNATLIST(z0)) A__ISNATILIST(z0) -> c6() A__ISNATILIST(cons(z0,z1)) -> c4(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNAT(z0)) A__ISNATILIST(cons(z0,z1)) -> c5(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNATILIST(z1)) A__ISNATILIST(zeros()) -> c3() A__ISNATLIST(z0) -> c16() A__ISNATLIST(cons(z0,z1)) -> c12(A__AND(a__isNat(z0),a__isNatList(z1)),A__ISNAT(z0)) A__ISNATLIST(cons(z0,z1)) -> c13(A__AND(a__isNat(z0),a__isNatList(z1)),A__ISNATLIST(z1)) A__ISNATLIST(nil()) -> c11() A__ISNATLIST(take(z0,z1)) -> c14(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNAT(z0)) A__ISNATLIST(take(z0,z1)) -> c15(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNATILIST(z1)) A__LENGTH(z0) -> c30() A__LENGTH(cons(z0,z1)) -> c28(A__ULENGTH(a__and(a__isNat(z0),a__isNatList(z1)),z1) ,A__AND(a__isNat(z0),a__isNatList(z1)) ,A__ISNAT(z0)) A__LENGTH(cons(z0,z1)) -> c29(A__ULENGTH(a__and(a__isNat(z0),a__isNatList(z1)),z1) ,A__AND(a__isNat(z0),a__isNatList(z1)) ,A__ISNATLIST(z1)) A__TAKE(z0,z1) -> c23() A__TAKE(0(),z0) -> c19(A__UTAKE1(a__isNatIList(z0)),A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c20(A__UTAKE2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) ,A__AND(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,A__ISNAT(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c21(A__UTAKE2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) ,A__AND(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,A__AND(a__isNat(z1),a__isNatIList(z2)) ,A__ISNAT(z1)) A__TAKE(s(z0),cons(z1,z2)) -> c22(A__UTAKE2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) ,A__AND(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,A__AND(a__isNat(z1),a__isNatIList(z2)) ,A__ISNATILIST(z2)) A__ULENGTH(z0,z1) -> c32() A__ULENGTH(tt(),z0) -> c31(A__LENGTH(mark(z0)),MARK(z0)) A__UTAKE1(z0) -> c25() A__UTAKE1(tt()) -> c24() A__UTAKE2(z0,z1,z2,z3) -> c27() A__UTAKE2(tt(),z0,z1,z2) -> c26(MARK(z1)) A__ZEROS() -> c17() A__ZEROS() -> c18() MARK(0()) -> c46() MARK(and(z0,z1)) -> c33(A__AND(mark(z0),mark(z1)),MARK(z0)) MARK(and(z0,z1)) -> c34(A__AND(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c48(MARK(z0)) MARK(isNat(z0)) -> c37(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c35(A__ISNATILIST(z0)) MARK(isNatList(z0)) -> c36(A__ISNATLIST(z0)) MARK(length(z0)) -> c38(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c49() MARK(s(z0)) -> c47(MARK(z0)) MARK(take(z0,z1)) -> c40(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c41(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c45() MARK(uLength(z0,z1)) -> c44(A__ULENGTH(mark(z0),z1),MARK(z0)) MARK(uTake1(z0)) -> c42(A__UTAKE1(mark(z0)),MARK(z0)) MARK(uTake2(z0,z1,z2,z3)) -> c43(A__UTAKE2(mark(z0),z1,z2,z3),MARK(z0)) MARK(zeros()) -> c39(A__ZEROS()) - Weak TRS: a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(length(z0)) -> a__isNatList(z0) a__isNat(s(z0)) -> a__isNat(z0) a__isNatIList(z0) -> a__isNatList(z0) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__and(a__isNat(z0),a__isNatIList(z1)) a__isNatIList(zeros()) -> tt() a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__and(a__isNat(z0),a__isNatList(z1)) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__and(a__isNat(z0),a__isNatIList(z1)) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__uLength(a__and(a__isNat(z0),a__isNatList(z1)),z1) a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__uTake1(a__isNatIList(z0)) a__take(s(z0),cons(z1,z2)) -> a__uTake2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) a__uLength(z0,z1) -> uLength(z0,z1) a__uLength(tt(),z0) -> s(a__length(mark(z0))) a__uTake1(z0) -> uTake1(z0) a__uTake1(tt()) -> nil() a__uTake2(z0,z1,z2,z3) -> uTake2(z0,z1,z2,z3) a__uTake2(tt(),z0,z1,z2) -> cons(mark(z1),take(z0,z2)) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(and(z0,z1)) -> a__and(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(isNatList(z0)) -> a__isNatList(z0) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() mark(uLength(z0,z1)) -> a__uLength(mark(z0),z1) mark(uTake1(z0)) -> a__uTake1(mark(z0)) mark(uTake2(z0,z1,z2,z3)) -> a__uTake2(mark(z0),z1,z2,z3) mark(zeros()) -> a__zeros() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATILIST/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2,A__ULENGTH/2,A__UTAKE1/1 ,A__UTAKE2/4,A__ZEROS/0,MARK/1,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1,a__take/2 ,a__uLength/2,a__uTake1/1,a__uTake2/4,a__zeros/0,mark/1} / {0/0,and/2,c/1,c1/0,c10/0,c11/0,c12/2,c13/2,c14/2 ,c15/2,c16/0,c17/0,c18/0,c19/2,c2/1,c20/3,c21/4,c22/4,c23/0,c24/0,c25/0,c26/1,c27/0,c28/3,c29/3,c3/0,c30/0 ,c31/2,c32/0,c33/2,c34/2,c35/1,c36/1,c37/1,c38/2,c39/1,c4/2,c40/2,c41/2,c42/2,c43/2,c44/2,c45/0,c46/0,c47/1 ,c48/1,c49/0,c5/2,c6/0,c7/0,c8/1,c9/1,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,tt/0 ,uLength/2,uTake1/1,uTake2/4,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATILIST,A__ISNATLIST,A__LENGTH ,A__TAKE,A__ULENGTH,A__UTAKE1,A__UTAKE2,A__ZEROS,MARK,a__and,a__isNat,a__isNatIList,a__isNatList,a__length ,a__take,a__uLength,a__uTake1,a__uTake2,a__zeros,mark} and constructors {0,and,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4 ,c40,c41,c42,c43,c44,c45,c46,c47,c48,c49,c5,c6,c7,c8,c9,cons,isNat,isNatIList,isNatList,length,nil,s,take,tt ,uLength,uTake1,uTake2,zeros} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c1() A__AND(tt(),z0) -> c(MARK(z0)) A__ISNAT(z0) -> c10() A__ISNAT(0()) -> c7() A__ISNAT(length(z0)) -> c9(A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c8(A__ISNAT(z0)) A__ISNATILIST(z0) -> c2(A__ISNATLIST(z0)) A__ISNATILIST(z0) -> c6() A__ISNATILIST(cons(z0,z1)) -> c4(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNAT(z0)) A__ISNATILIST(cons(z0,z1)) -> c5(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNATILIST(z1)) A__ISNATILIST(zeros()) -> c3() A__ISNATLIST(z0) -> c16() A__ISNATLIST(cons(z0,z1)) -> c12(A__AND(a__isNat(z0),a__isNatList(z1)),A__ISNAT(z0)) A__ISNATLIST(cons(z0,z1)) -> c13(A__AND(a__isNat(z0),a__isNatList(z1)),A__ISNATLIST(z1)) A__ISNATLIST(nil()) -> c11() A__ISNATLIST(take(z0,z1)) -> c14(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNAT(z0)) A__ISNATLIST(take(z0,z1)) -> c15(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNATILIST(z1)) A__LENGTH(z0) -> c30() A__LENGTH(cons(z0,z1)) -> c28(A__ULENGTH(a__and(a__isNat(z0),a__isNatList(z1)),z1) ,A__AND(a__isNat(z0),a__isNatList(z1)) ,A__ISNAT(z0)) A__LENGTH(cons(z0,z1)) -> c29(A__ULENGTH(a__and(a__isNat(z0),a__isNatList(z1)),z1) ,A__AND(a__isNat(z0),a__isNatList(z1)) ,A__ISNATLIST(z1)) A__TAKE(z0,z1) -> c23() A__TAKE(0(),z0) -> c19(A__UTAKE1(a__isNatIList(z0)),A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c20(A__UTAKE2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) ,A__AND(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,A__ISNAT(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c21(A__UTAKE2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) ,A__AND(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,A__AND(a__isNat(z1),a__isNatIList(z2)) ,A__ISNAT(z1)) A__TAKE(s(z0),cons(z1,z2)) -> c22(A__UTAKE2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) ,A__AND(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,A__AND(a__isNat(z1),a__isNatIList(z2)) ,A__ISNATILIST(z2)) A__ULENGTH(z0,z1) -> c32() A__ULENGTH(tt(),z0) -> c31(A__LENGTH(mark(z0)),MARK(z0)) A__UTAKE1(z0) -> c25() A__UTAKE1(tt()) -> c24() A__UTAKE2(z0,z1,z2,z3) -> c27() A__UTAKE2(tt(),z0,z1,z2) -> c26(MARK(z1)) A__ZEROS() -> c17() A__ZEROS() -> c18() MARK(0()) -> c46() MARK(and(z0,z1)) -> c33(A__AND(mark(z0),mark(z1)),MARK(z0)) MARK(and(z0,z1)) -> c34(A__AND(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c48(MARK(z0)) MARK(isNat(z0)) -> c37(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c35(A__ISNATILIST(z0)) MARK(isNatList(z0)) -> c36(A__ISNATLIST(z0)) MARK(length(z0)) -> c38(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c49() MARK(s(z0)) -> c47(MARK(z0)) MARK(take(z0,z1)) -> c40(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c41(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c45() MARK(uLength(z0,z1)) -> c44(A__ULENGTH(mark(z0),z1),MARK(z0)) MARK(uTake1(z0)) -> c42(A__UTAKE1(mark(z0)),MARK(z0)) MARK(uTake2(z0,z1,z2,z3)) -> c43(A__UTAKE2(mark(z0),z1,z2,z3),MARK(z0)) MARK(zeros()) -> c39(A__ZEROS()) - Weak TRS: a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(length(z0)) -> a__isNatList(z0) a__isNat(s(z0)) -> a__isNat(z0) a__isNatIList(z0) -> a__isNatList(z0) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__and(a__isNat(z0),a__isNatIList(z1)) a__isNatIList(zeros()) -> tt() a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__and(a__isNat(z0),a__isNatList(z1)) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__and(a__isNat(z0),a__isNatIList(z1)) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__uLength(a__and(a__isNat(z0),a__isNatList(z1)),z1) a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__uTake1(a__isNatIList(z0)) a__take(s(z0),cons(z1,z2)) -> a__uTake2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) a__uLength(z0,z1) -> uLength(z0,z1) a__uLength(tt(),z0) -> s(a__length(mark(z0))) a__uTake1(z0) -> uTake1(z0) a__uTake1(tt()) -> nil() a__uTake2(z0,z1,z2,z3) -> uTake2(z0,z1,z2,z3) a__uTake2(tt(),z0,z1,z2) -> cons(mark(z1),take(z0,z2)) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(and(z0,z1)) -> a__and(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(isNatList(z0)) -> a__isNatList(z0) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() mark(uLength(z0,z1)) -> a__uLength(mark(z0),z1) mark(uTake1(z0)) -> a__uTake1(mark(z0)) mark(uTake2(z0,z1,z2,z3)) -> a__uTake2(mark(z0),z1,z2,z3) mark(zeros()) -> a__zeros() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATILIST/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2,A__ULENGTH/2,A__UTAKE1/1 ,A__UTAKE2/4,A__ZEROS/0,MARK/1,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1,a__take/2 ,a__uLength/2,a__uTake1/1,a__uTake2/4,a__zeros/0,mark/1} / {0/0,and/2,c/1,c1/0,c10/0,c11/0,c12/2,c13/2,c14/2 ,c15/2,c16/0,c17/0,c18/0,c19/2,c2/1,c20/3,c21/4,c22/4,c23/0,c24/0,c25/0,c26/1,c27/0,c28/3,c29/3,c3/0,c30/0 ,c31/2,c32/0,c33/2,c34/2,c35/1,c36/1,c37/1,c38/2,c39/1,c4/2,c40/2,c41/2,c42/2,c43/2,c44/2,c45/0,c46/0,c47/1 ,c48/1,c49/0,c5/2,c6/0,c7/0,c8/1,c9/1,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,tt/0 ,uLength/2,uTake1/1,uTake2/4,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATILIST,A__ISNATLIST,A__LENGTH ,A__TAKE,A__ULENGTH,A__UTAKE1,A__UTAKE2,A__ZEROS,MARK,a__and,a__isNat,a__isNatIList,a__isNatList,a__length ,a__take,a__uLength,a__uTake1,a__uTake2,a__zeros,mark} and constructors {0,and,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4 ,c40,c41,c42,c43,c44,c45,c46,c47,c48,c49,c5,c6,c7,c8,c9,cons,isNat,isNatIList,isNatList,length,nil,s,take,tt ,uLength,uTake1,uTake2,zeros} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c1() A__AND(tt(),z0) -> c(MARK(z0)) A__ISNAT(z0) -> c10() A__ISNAT(0()) -> c7() A__ISNAT(length(z0)) -> c9(A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c8(A__ISNAT(z0)) A__ISNATILIST(z0) -> c2(A__ISNATLIST(z0)) A__ISNATILIST(z0) -> c6() A__ISNATILIST(cons(z0,z1)) -> c4(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNAT(z0)) A__ISNATILIST(cons(z0,z1)) -> c5(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNATILIST(z1)) A__ISNATILIST(zeros()) -> c3() A__ISNATLIST(z0) -> c16() A__ISNATLIST(cons(z0,z1)) -> c12(A__AND(a__isNat(z0),a__isNatList(z1)),A__ISNAT(z0)) A__ISNATLIST(cons(z0,z1)) -> c13(A__AND(a__isNat(z0),a__isNatList(z1)),A__ISNATLIST(z1)) A__ISNATLIST(nil()) -> c11() A__ISNATLIST(take(z0,z1)) -> c14(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNAT(z0)) A__ISNATLIST(take(z0,z1)) -> c15(A__AND(a__isNat(z0),a__isNatIList(z1)),A__ISNATILIST(z1)) A__LENGTH(z0) -> c30() A__LENGTH(cons(z0,z1)) -> c28(A__ULENGTH(a__and(a__isNat(z0),a__isNatList(z1)),z1) ,A__AND(a__isNat(z0),a__isNatList(z1)) ,A__ISNAT(z0)) A__LENGTH(cons(z0,z1)) -> c29(A__ULENGTH(a__and(a__isNat(z0),a__isNatList(z1)),z1) ,A__AND(a__isNat(z0),a__isNatList(z1)) ,A__ISNATLIST(z1)) A__TAKE(z0,z1) -> c23() A__TAKE(0(),z0) -> c19(A__UTAKE1(a__isNatIList(z0)),A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c20(A__UTAKE2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) ,A__AND(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,A__ISNAT(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c21(A__UTAKE2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) ,A__AND(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,A__AND(a__isNat(z1),a__isNatIList(z2)) ,A__ISNAT(z1)) A__TAKE(s(z0),cons(z1,z2)) -> c22(A__UTAKE2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) ,A__AND(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,A__AND(a__isNat(z1),a__isNatIList(z2)) ,A__ISNATILIST(z2)) A__ULENGTH(z0,z1) -> c32() A__ULENGTH(tt(),z0) -> c31(A__LENGTH(mark(z0)),MARK(z0)) A__UTAKE1(z0) -> c25() A__UTAKE1(tt()) -> c24() A__UTAKE2(z0,z1,z2,z3) -> c27() A__UTAKE2(tt(),z0,z1,z2) -> c26(MARK(z1)) A__ZEROS() -> c17() A__ZEROS() -> c18() MARK(0()) -> c46() MARK(and(z0,z1)) -> c33(A__AND(mark(z0),mark(z1)),MARK(z0)) MARK(and(z0,z1)) -> c34(A__AND(mark(z0),mark(z1)),MARK(z1)) MARK(cons(z0,z1)) -> c48(MARK(z0)) MARK(isNat(z0)) -> c37(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c35(A__ISNATILIST(z0)) MARK(isNatList(z0)) -> c36(A__ISNATLIST(z0)) MARK(length(z0)) -> c38(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c49() MARK(s(z0)) -> c47(MARK(z0)) MARK(take(z0,z1)) -> c40(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c41(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c45() MARK(uLength(z0,z1)) -> c44(A__ULENGTH(mark(z0),z1),MARK(z0)) MARK(uTake1(z0)) -> c42(A__UTAKE1(mark(z0)),MARK(z0)) MARK(uTake2(z0,z1,z2,z3)) -> c43(A__UTAKE2(mark(z0),z1,z2,z3),MARK(z0)) MARK(zeros()) -> c39(A__ZEROS()) - Weak TRS: a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(length(z0)) -> a__isNatList(z0) a__isNat(s(z0)) -> a__isNat(z0) a__isNatIList(z0) -> a__isNatList(z0) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__and(a__isNat(z0),a__isNatIList(z1)) a__isNatIList(zeros()) -> tt() a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__and(a__isNat(z0),a__isNatList(z1)) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__and(a__isNat(z0),a__isNatIList(z1)) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__uLength(a__and(a__isNat(z0),a__isNatList(z1)),z1) a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__uTake1(a__isNatIList(z0)) a__take(s(z0),cons(z1,z2)) -> a__uTake2(a__and(a__isNat(z0),a__and(a__isNat(z1),a__isNatIList(z2))) ,z0 ,z1 ,z2) a__uLength(z0,z1) -> uLength(z0,z1) a__uLength(tt(),z0) -> s(a__length(mark(z0))) a__uTake1(z0) -> uTake1(z0) a__uTake1(tt()) -> nil() a__uTake2(z0,z1,z2,z3) -> uTake2(z0,z1,z2,z3) a__uTake2(tt(),z0,z1,z2) -> cons(mark(z1),take(z0,z2)) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(and(z0,z1)) -> a__and(mark(z0),mark(z1)) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(isNatList(z0)) -> a__isNatList(z0) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() mark(uLength(z0,z1)) -> a__uLength(mark(z0),z1) mark(uTake1(z0)) -> a__uTake1(mark(z0)) mark(uTake2(z0,z1,z2,z3)) -> a__uTake2(mark(z0),z1,z2,z3) mark(zeros()) -> a__zeros() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATILIST/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2,A__ULENGTH/2,A__UTAKE1/1 ,A__UTAKE2/4,A__ZEROS/0,MARK/1,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1,a__take/2 ,a__uLength/2,a__uTake1/1,a__uTake2/4,a__zeros/0,mark/1} / {0/0,and/2,c/1,c1/0,c10/0,c11/0,c12/2,c13/2,c14/2 ,c15/2,c16/0,c17/0,c18/0,c19/2,c2/1,c20/3,c21/4,c22/4,c23/0,c24/0,c25/0,c26/1,c27/0,c28/3,c29/3,c3/0,c30/0 ,c31/2,c32/0,c33/2,c34/2,c35/1,c36/1,c37/1,c38/2,c39/1,c4/2,c40/2,c41/2,c42/2,c43/2,c44/2,c45/0,c46/0,c47/1 ,c48/1,c49/0,c5/2,c6/0,c7/0,c8/1,c9/1,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,tt/0 ,uLength/2,uTake1/1,uTake2/4,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATILIST,A__ISNATLIST,A__LENGTH ,A__TAKE,A__ULENGTH,A__UTAKE1,A__UTAKE2,A__ZEROS,MARK,a__and,a__isNat,a__isNatIList,a__isNatList,a__length ,a__take,a__uLength,a__uTake1,a__uTake2,a__zeros,mark} and constructors {0,and,c,c1,c10,c11,c12,c13,c14,c15 ,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4 ,c40,c41,c42,c43,c44,c45,c46,c47,c48,c49,c5,c6,c7,c8,c9,cons,isNat,isNatIList,isNatList,length,nil,s,take,tt ,uLength,uTake1,uTake2,zeros} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: A__ISNAT(x){x -> s(x)} = A__ISNAT(s(x)) ->^+ c8(A__ISNAT(x)) = C[A__ISNAT(x) = A__ISNAT(x){}] WORST_CASE(Omega(n^1),?)