WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c39() A__AND(tt(),z0) -> c38(MARK(z0)) A__ISNAT(z0) -> c43() A__ISNAT(0()) -> c40() A__ISNAT(length(z0)) -> c41(A__U11(a__isNatIListKind(z0),z0),A__ISNATILISTKIND(z0)) A__ISNAT(s(z0)) -> c42(A__U21(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__ISNATILIST(z0) -> c44(A__U31(a__isNatIListKind(z0),z0),A__ISNATILISTKIND(z0)) A__ISNATILIST(z0) -> c47() A__ISNATILIST(cons(z0,z1)) -> c46(A__U41(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatIListKind(z1)) ,A__ISNATKIND(z0)) A__ISNATILIST(zeros()) -> c45() A__ISNATILISTKIND(z0) -> c52() A__ISNATILISTKIND(cons(z0,z1)) -> c50(A__AND(a__isNatKind(z0),isNatIListKind(z1)),A__ISNATKIND(z0)) A__ISNATILISTKIND(nil()) -> c48() A__ISNATILISTKIND(take(z0,z1)) -> c51(A__AND(a__isNatKind(z0),isNatIListKind(z1)),A__ISNATKIND(z0)) A__ISNATILISTKIND(zeros()) -> c49() A__ISNATKIND(z0) -> c56() A__ISNATKIND(0()) -> c53() A__ISNATKIND(length(z0)) -> c54(A__ISNATILISTKIND(z0)) A__ISNATKIND(s(z0)) -> c55(A__ISNATKIND(z0)) A__ISNATLIST(z0) -> c60() A__ISNATLIST(cons(z0,z1)) -> c58(A__U51(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatIListKind(z1)) ,A__ISNATKIND(z0)) A__ISNATLIST(nil()) -> c57() A__ISNATLIST(take(z0,z1)) -> c59(A__U61(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatIListKind(z1)) ,A__ISNATKIND(z0)) A__LENGTH(z0) -> c63() A__LENGTH(cons(z0,z1)) -> c62(A__U71(a__and(a__and(a__isNatList(z1),isNatIListKind(z1)) ,and(isNat(z0),isNatKind(z0))) ,z1) ,A__AND(a__and(a__isNatList(z1),isNatIListKind(z1)) ,and(isNat(z0),isNatKind(z0))) ,A__AND(a__isNatList(z1),isNatIListKind(z1)) ,A__ISNATLIST(z1)) A__LENGTH(nil()) -> c61() A__TAKE(z0,z1) -> c66() A__TAKE(0(),z0) -> c64(A__U81(a__and(a__isNatIList(z0),isNatIListKind(z0))) ,A__AND(a__isNatIList(z0),isNatIListKind(z0)) ,A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c65(A__U91(a__and(a__and(a__isNatIList(z2),isNatIListKind(z2)) ,and(and(isNat(z0),isNatKind(z0)) ,and(isNat(z1),isNatKind(z1)))) ,z2 ,z0 ,z1) ,A__AND(a__and(a__isNatIList(z2),isNatIListKind(z2)) ,and(and(isNat(z0),isNatKind(z0)),and(isNat(z1),isNatKind(z1)))) ,A__AND(a__isNatIList(z2),isNatIListKind(z2)) ,A__ISNATILIST(z2)) A__U11(z0,z1) -> c3() A__U11(tt(),z0) -> c2(A__U12(a__isNatList(z0)),A__ISNATLIST(z0)) A__U12(z0) -> c5() A__U12(tt()) -> c4() A__U21(z0,z1) -> c7() A__U21(tt(),z0) -> c6(A__U22(a__isNat(z0)),A__ISNAT(z0)) A__U22(z0) -> c9() A__U22(tt()) -> c8() A__U31(z0,z1) -> c11() A__U31(tt(),z0) -> c10(A__U32(a__isNatList(z0)),A__ISNATLIST(z0)) A__U32(z0) -> c13() A__U32(tt()) -> c12() A__U41(z0,z1,z2) -> c15() A__U41(tt(),z0,z1) -> c14(A__U42(a__isNat(z0),z1),A__ISNAT(z0)) A__U42(z0,z1) -> c17() A__U42(tt(),z0) -> c16(A__U43(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U43(z0) -> c19() A__U43(tt()) -> c18() A__U51(z0,z1,z2) -> c21() A__U51(tt(),z0,z1) -> c20(A__U52(a__isNat(z0),z1),A__ISNAT(z0)) A__U52(z0,z1) -> c23() A__U52(tt(),z0) -> c22(A__U53(a__isNatList(z0)),A__ISNATLIST(z0)) A__U53(z0) -> c25() A__U53(tt()) -> c24() A__U61(z0,z1,z2) -> c27() A__U61(tt(),z0,z1) -> c26(A__U62(a__isNat(z0),z1),A__ISNAT(z0)) A__U62(z0,z1) -> c29() A__U62(tt(),z0) -> c28(A__U63(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U63(z0) -> c31() A__U63(tt()) -> c30() A__U71(z0,z1) -> c33() A__U71(tt(),z0) -> c32(A__LENGTH(mark(z0)),MARK(z0)) A__U81(z0) -> c35() A__U81(tt()) -> c34() A__U91(z0,z1,z2,z3) -> c37() A__U91(tt(),z0,z1,z2) -> c36(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c96() MARK(U11(z0,z1)) -> c68(A__U11(mark(z0),z1),MARK(z0)) MARK(U12(z0)) -> c69(A__U12(mark(z0)),MARK(z0)) MARK(U21(z0,z1)) -> c71(A__U21(mark(z0),z1),MARK(z0)) MARK(U22(z0)) -> c72(A__U22(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c74(A__U31(mark(z0),z1),MARK(z0)) MARK(U32(z0)) -> c75(A__U32(mark(z0)),MARK(z0)) MARK(U41(z0,z1,z2)) -> c76(A__U41(mark(z0),z1,z2),MARK(z0)) MARK(U42(z0,z1)) -> c77(A__U42(mark(z0),z1),MARK(z0)) MARK(U43(z0)) -> c78(A__U43(mark(z0)),MARK(z0)) MARK(U51(z0,z1,z2)) -> c80(A__U51(mark(z0),z1,z2),MARK(z0)) MARK(U52(z0,z1)) -> c81(A__U52(mark(z0),z1),MARK(z0)) MARK(U53(z0)) -> c82(A__U53(mark(z0)),MARK(z0)) MARK(U61(z0,z1,z2)) -> c83(A__U61(mark(z0),z1,z2),MARK(z0)) MARK(U62(z0,z1)) -> c84(A__U62(mark(z0),z1),MARK(z0)) MARK(U63(z0)) -> c85(A__U63(mark(z0)),MARK(z0)) MARK(U71(z0,z1)) -> c86(A__U71(mark(z0),z1),MARK(z0)) MARK(U81(z0)) -> c88(A__U81(mark(z0)),MARK(z0)) MARK(U91(z0,z1,z2,z3)) -> c89(A__U91(mark(z0),z1,z2,z3),MARK(z0)) MARK(and(z0,z1)) -> c92(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c95(MARK(z0)) MARK(isNat(z0)) -> c73(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c79(A__ISNATILIST(z0)) MARK(isNatIListKind(z0)) -> c93(A__ISNATILISTKIND(z0)) MARK(isNatKind(z0)) -> c94(A__ISNATKIND(z0)) MARK(isNatList(z0)) -> c70(A__ISNATLIST(z0)) MARK(length(z0)) -> c87(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c99() MARK(s(z0)) -> c98(MARK(z0)) MARK(take(z0,z1)) -> c90(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c91(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c97() MARK(zeros()) -> c67(A__ZEROS()) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> a__U12(a__isNatList(z0)) a__U12(z0) -> U12(z0) a__U12(tt()) -> tt() a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> a__U22(a__isNat(z0)) a__U22(z0) -> U22(z0) a__U22(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> a__U32(a__isNatList(z0)) a__U32(z0) -> U32(z0) a__U32(tt()) -> tt() a__U41(z0,z1,z2) -> U41(z0,z1,z2) a__U41(tt(),z0,z1) -> a__U42(a__isNat(z0),z1) a__U42(z0,z1) -> U42(z0,z1) a__U42(tt(),z0) -> a__U43(a__isNatIList(z0)) a__U43(z0) -> U43(z0) a__U43(tt()) -> tt() a__U51(z0,z1,z2) -> U51(z0,z1,z2) a__U51(tt(),z0,z1) -> a__U52(a__isNat(z0),z1) a__U52(z0,z1) -> U52(z0,z1) a__U52(tt(),z0) -> a__U53(a__isNatList(z0)) a__U53(z0) -> U53(z0) a__U53(tt()) -> tt() a__U61(z0,z1,z2) -> U61(z0,z1,z2) a__U61(tt(),z0,z1) -> a__U62(a__isNat(z0),z1) a__U62(z0,z1) -> U62(z0,z1) a__U62(tt(),z0) -> a__U63(a__isNatIList(z0)) a__U63(z0) -> U63(z0) a__U63(tt()) -> tt() a__U71(z0,z1) -> U71(z0,z1) a__U71(tt(),z0) -> s(a__length(mark(z0))) a__U81(z0) -> U81(z0) a__U81(tt()) -> nil() a__U91(z0,z1,z2,z3) -> U91(z0,z1,z2,z3) a__U91(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) 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__U11(a__isNatIListKind(z0),z0) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0),z0) a__isNatIList(z0) -> a__U31(a__isNatIListKind(z0),z0) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__U41(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) a__isNatIList(zeros()) -> tt() a__isNatIListKind(z0) -> isNatIListKind(z0) a__isNatIListKind(cons(z0,z1)) -> a__and(a__isNatKind(z0),isNatIListKind(z1)) a__isNatIListKind(nil()) -> tt() a__isNatIListKind(take(z0,z1)) -> a__and(a__isNatKind(z0),isNatIListKind(z1)) a__isNatIListKind(zeros()) -> tt() a__isNatKind(z0) -> isNatKind(z0) a__isNatKind(0()) -> tt() a__isNatKind(length(z0)) -> a__isNatIListKind(z0) a__isNatKind(s(z0)) -> a__isNatKind(z0) a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__U51(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__U61(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U71(a__and(a__and(a__isNatList(z1),isNatIListKind(z1)) ,and(isNat(z0),isNatKind(z0))) ,z1) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__U81(a__and(a__isNatIList(z0),isNatIListKind(z0))) a__take(s(z0),cons(z1,z2)) -> a__U91(a__and(a__and(a__isNatIList(z2),isNatIListKind(z2)) ,and(and(isNat(z0),isNatKind(z0)),and(isNat(z1),isNatKind(z1)))) ,z2 ,z0 ,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U12(z0)) -> a__U12(mark(z0)) mark(U21(z0,z1)) -> a__U21(mark(z0),z1) mark(U22(z0)) -> a__U22(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U32(z0)) -> a__U32(mark(z0)) mark(U41(z0,z1,z2)) -> a__U41(mark(z0),z1,z2) mark(U42(z0,z1)) -> a__U42(mark(z0),z1) mark(U43(z0)) -> a__U43(mark(z0)) mark(U51(z0,z1,z2)) -> a__U51(mark(z0),z1,z2) mark(U52(z0,z1)) -> a__U52(mark(z0),z1) mark(U53(z0)) -> a__U53(mark(z0)) mark(U61(z0,z1,z2)) -> a__U61(mark(z0),z1,z2) mark(U62(z0,z1)) -> a__U62(mark(z0),z1) mark(U63(z0)) -> a__U63(mark(z0)) mark(U71(z0,z1)) -> a__U71(mark(z0),z1) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0,z1,z2,z3)) -> a__U91(mark(z0),z1,z2,z3) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(isNatIListKind(z0)) -> a__isNatIListKind(z0) mark(isNatKind(z0)) -> a__isNatKind(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(zeros()) -> a__zeros() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATILIST/1,A__ISNATILISTKIND/1,A__ISNATKIND/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2 ,A__U11/2,A__U12/1,A__U21/2,A__U22/1,A__U31/2,A__U32/1,A__U41/3,A__U42/2,A__U43/1,A__U51/3,A__U52/2,A__U53/1 ,A__U61/3,A__U62/2,A__U63/1,A__U71/2,A__U81/1,A__U91/4,A__ZEROS/0,MARK/1,a__U11/2,a__U12/1,a__U21/2,a__U22/1 ,a__U31/2,a__U32/1,a__U41/3,a__U42/2,a__U43/1,a__U51/3,a__U52/2,a__U53/1,a__U61/3,a__U62/2,a__U63/1,a__U71/2 ,a__U81/1,a__U91/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatIListKind/1,a__isNatKind/1,a__isNatList/1 ,a__length/1,a__take/2,a__zeros/0,mark/1} / {0/0,U11/2,U12/1,U21/2,U22/1,U31/2,U32/1,U41/3,U42/2,U43/1,U51/3 ,U52/2,U53/1,U61/3,U62/2,U63/1,U71/2,U81/1,U91/4,and/2,c/0,c1/0,c10/2,c11/0,c12/0,c13/0,c14/2,c15/0,c16/2 ,c17/0,c18/0,c19/0,c2/2,c20/2,c21/0,c22/2,c23/0,c24/0,c25/0,c26/2,c27/0,c28/2,c29/0,c3/0,c30/0,c31/0,c32/2 ,c33/0,c34/0,c35/0,c36/1,c37/0,c38/1,c39/0,c4/0,c40/0,c41/2,c42/2,c43/0,c44/2,c45/0,c46/3,c47/0,c48/0,c49/0 ,c5/0,c50/2,c51/2,c52/0,c53/0,c54/1,c55/1,c56/0,c57/0,c58/3,c59/3,c6/2,c60/0,c61/0,c62/4,c63/0,c64/3,c65/4 ,c66/0,c67/1,c68/2,c69/2,c7/0,c70/1,c71/2,c72/2,c73/1,c74/2,c75/2,c76/2,c77/2,c78/2,c79/1,c8/0,c80/2,c81/2 ,c82/2,c83/2,c84/2,c85/2,c86/2,c87/2,c88/2,c89/2,c9/0,c90/2,c91/2,c92/2,c93/1,c94/1,c95/1,c96/0,c97/0,c98/1 ,c99/0,cons/2,isNat/1,isNatIList/1,isNatIListKind/1,isNatKind/1,isNatList/1,length/1,nil/0,s/1,take/2,tt/0 ,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATILIST,A__ISNATILISTKIND ,A__ISNATKIND,A__ISNATLIST,A__LENGTH,A__TAKE,A__U11,A__U12,A__U21,A__U22,A__U31,A__U32,A__U41,A__U42,A__U43 ,A__U51,A__U52,A__U53,A__U61,A__U62,A__U63,A__U71,A__U81,A__U91,A__ZEROS,MARK,a__U11,a__U12,a__U21,a__U22 ,a__U31,a__U32,a__U41,a__U42,a__U43,a__U51,a__U52,a__U53,a__U61,a__U62,a__U63,a__U71,a__U81,a__U91,a__and ,a__isNat,a__isNatIList,a__isNatIListKind,a__isNatKind,a__isNatList,a__length,a__take,a__zeros ,mark} and constructors {0,U11,U12,U21,U22,U31,U32,U41,U42,U43,U51,U52,U53,U61,U62,U63,U71,U81,U91,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,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59 ,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83 ,c84,c85,c86,c87,c88,c89,c9,c90,c91,c92,c93,c94,c95,c96,c97,c98,c99,cons,isNat,isNatIList,isNatIListKind ,isNatKind,isNatList,length,nil,s,take,tt,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) -> c39() A__AND(tt(),z0) -> c38(MARK(z0)) A__ISNAT(z0) -> c43() A__ISNAT(0()) -> c40() A__ISNAT(length(z0)) -> c41(A__U11(a__isNatIListKind(z0),z0),A__ISNATILISTKIND(z0)) A__ISNAT(s(z0)) -> c42(A__U21(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__ISNATILIST(z0) -> c44(A__U31(a__isNatIListKind(z0),z0),A__ISNATILISTKIND(z0)) A__ISNATILIST(z0) -> c47() A__ISNATILIST(cons(z0,z1)) -> c46(A__U41(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatIListKind(z1)) ,A__ISNATKIND(z0)) A__ISNATILIST(zeros()) -> c45() A__ISNATILISTKIND(z0) -> c52() A__ISNATILISTKIND(cons(z0,z1)) -> c50(A__AND(a__isNatKind(z0),isNatIListKind(z1)),A__ISNATKIND(z0)) A__ISNATILISTKIND(nil()) -> c48() A__ISNATILISTKIND(take(z0,z1)) -> c51(A__AND(a__isNatKind(z0),isNatIListKind(z1)),A__ISNATKIND(z0)) A__ISNATILISTKIND(zeros()) -> c49() A__ISNATKIND(z0) -> c56() A__ISNATKIND(0()) -> c53() A__ISNATKIND(length(z0)) -> c54(A__ISNATILISTKIND(z0)) A__ISNATKIND(s(z0)) -> c55(A__ISNATKIND(z0)) A__ISNATLIST(z0) -> c60() A__ISNATLIST(cons(z0,z1)) -> c58(A__U51(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatIListKind(z1)) ,A__ISNATKIND(z0)) A__ISNATLIST(nil()) -> c57() A__ISNATLIST(take(z0,z1)) -> c59(A__U61(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatIListKind(z1)) ,A__ISNATKIND(z0)) A__LENGTH(z0) -> c63() A__LENGTH(cons(z0,z1)) -> c62(A__U71(a__and(a__and(a__isNatList(z1),isNatIListKind(z1)) ,and(isNat(z0),isNatKind(z0))) ,z1) ,A__AND(a__and(a__isNatList(z1),isNatIListKind(z1)) ,and(isNat(z0),isNatKind(z0))) ,A__AND(a__isNatList(z1),isNatIListKind(z1)) ,A__ISNATLIST(z1)) A__LENGTH(nil()) -> c61() A__TAKE(z0,z1) -> c66() A__TAKE(0(),z0) -> c64(A__U81(a__and(a__isNatIList(z0),isNatIListKind(z0))) ,A__AND(a__isNatIList(z0),isNatIListKind(z0)) ,A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c65(A__U91(a__and(a__and(a__isNatIList(z2),isNatIListKind(z2)) ,and(and(isNat(z0),isNatKind(z0)) ,and(isNat(z1),isNatKind(z1)))) ,z2 ,z0 ,z1) ,A__AND(a__and(a__isNatIList(z2),isNatIListKind(z2)) ,and(and(isNat(z0),isNatKind(z0)),and(isNat(z1),isNatKind(z1)))) ,A__AND(a__isNatIList(z2),isNatIListKind(z2)) ,A__ISNATILIST(z2)) A__U11(z0,z1) -> c3() A__U11(tt(),z0) -> c2(A__U12(a__isNatList(z0)),A__ISNATLIST(z0)) A__U12(z0) -> c5() A__U12(tt()) -> c4() A__U21(z0,z1) -> c7() A__U21(tt(),z0) -> c6(A__U22(a__isNat(z0)),A__ISNAT(z0)) A__U22(z0) -> c9() A__U22(tt()) -> c8() A__U31(z0,z1) -> c11() A__U31(tt(),z0) -> c10(A__U32(a__isNatList(z0)),A__ISNATLIST(z0)) A__U32(z0) -> c13() A__U32(tt()) -> c12() A__U41(z0,z1,z2) -> c15() A__U41(tt(),z0,z1) -> c14(A__U42(a__isNat(z0),z1),A__ISNAT(z0)) A__U42(z0,z1) -> c17() A__U42(tt(),z0) -> c16(A__U43(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U43(z0) -> c19() A__U43(tt()) -> c18() A__U51(z0,z1,z2) -> c21() A__U51(tt(),z0,z1) -> c20(A__U52(a__isNat(z0),z1),A__ISNAT(z0)) A__U52(z0,z1) -> c23() A__U52(tt(),z0) -> c22(A__U53(a__isNatList(z0)),A__ISNATLIST(z0)) A__U53(z0) -> c25() A__U53(tt()) -> c24() A__U61(z0,z1,z2) -> c27() A__U61(tt(),z0,z1) -> c26(A__U62(a__isNat(z0),z1),A__ISNAT(z0)) A__U62(z0,z1) -> c29() A__U62(tt(),z0) -> c28(A__U63(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U63(z0) -> c31() A__U63(tt()) -> c30() A__U71(z0,z1) -> c33() A__U71(tt(),z0) -> c32(A__LENGTH(mark(z0)),MARK(z0)) A__U81(z0) -> c35() A__U81(tt()) -> c34() A__U91(z0,z1,z2,z3) -> c37() A__U91(tt(),z0,z1,z2) -> c36(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c96() MARK(U11(z0,z1)) -> c68(A__U11(mark(z0),z1),MARK(z0)) MARK(U12(z0)) -> c69(A__U12(mark(z0)),MARK(z0)) MARK(U21(z0,z1)) -> c71(A__U21(mark(z0),z1),MARK(z0)) MARK(U22(z0)) -> c72(A__U22(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c74(A__U31(mark(z0),z1),MARK(z0)) MARK(U32(z0)) -> c75(A__U32(mark(z0)),MARK(z0)) MARK(U41(z0,z1,z2)) -> c76(A__U41(mark(z0),z1,z2),MARK(z0)) MARK(U42(z0,z1)) -> c77(A__U42(mark(z0),z1),MARK(z0)) MARK(U43(z0)) -> c78(A__U43(mark(z0)),MARK(z0)) MARK(U51(z0,z1,z2)) -> c80(A__U51(mark(z0),z1,z2),MARK(z0)) MARK(U52(z0,z1)) -> c81(A__U52(mark(z0),z1),MARK(z0)) MARK(U53(z0)) -> c82(A__U53(mark(z0)),MARK(z0)) MARK(U61(z0,z1,z2)) -> c83(A__U61(mark(z0),z1,z2),MARK(z0)) MARK(U62(z0,z1)) -> c84(A__U62(mark(z0),z1),MARK(z0)) MARK(U63(z0)) -> c85(A__U63(mark(z0)),MARK(z0)) MARK(U71(z0,z1)) -> c86(A__U71(mark(z0),z1),MARK(z0)) MARK(U81(z0)) -> c88(A__U81(mark(z0)),MARK(z0)) MARK(U91(z0,z1,z2,z3)) -> c89(A__U91(mark(z0),z1,z2,z3),MARK(z0)) MARK(and(z0,z1)) -> c92(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c95(MARK(z0)) MARK(isNat(z0)) -> c73(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c79(A__ISNATILIST(z0)) MARK(isNatIListKind(z0)) -> c93(A__ISNATILISTKIND(z0)) MARK(isNatKind(z0)) -> c94(A__ISNATKIND(z0)) MARK(isNatList(z0)) -> c70(A__ISNATLIST(z0)) MARK(length(z0)) -> c87(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c99() MARK(s(z0)) -> c98(MARK(z0)) MARK(take(z0,z1)) -> c90(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c91(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c97() MARK(zeros()) -> c67(A__ZEROS()) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> a__U12(a__isNatList(z0)) a__U12(z0) -> U12(z0) a__U12(tt()) -> tt() a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> a__U22(a__isNat(z0)) a__U22(z0) -> U22(z0) a__U22(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> a__U32(a__isNatList(z0)) a__U32(z0) -> U32(z0) a__U32(tt()) -> tt() a__U41(z0,z1,z2) -> U41(z0,z1,z2) a__U41(tt(),z0,z1) -> a__U42(a__isNat(z0),z1) a__U42(z0,z1) -> U42(z0,z1) a__U42(tt(),z0) -> a__U43(a__isNatIList(z0)) a__U43(z0) -> U43(z0) a__U43(tt()) -> tt() a__U51(z0,z1,z2) -> U51(z0,z1,z2) a__U51(tt(),z0,z1) -> a__U52(a__isNat(z0),z1) a__U52(z0,z1) -> U52(z0,z1) a__U52(tt(),z0) -> a__U53(a__isNatList(z0)) a__U53(z0) -> U53(z0) a__U53(tt()) -> tt() a__U61(z0,z1,z2) -> U61(z0,z1,z2) a__U61(tt(),z0,z1) -> a__U62(a__isNat(z0),z1) a__U62(z0,z1) -> U62(z0,z1) a__U62(tt(),z0) -> a__U63(a__isNatIList(z0)) a__U63(z0) -> U63(z0) a__U63(tt()) -> tt() a__U71(z0,z1) -> U71(z0,z1) a__U71(tt(),z0) -> s(a__length(mark(z0))) a__U81(z0) -> U81(z0) a__U81(tt()) -> nil() a__U91(z0,z1,z2,z3) -> U91(z0,z1,z2,z3) a__U91(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) 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__U11(a__isNatIListKind(z0),z0) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0),z0) a__isNatIList(z0) -> a__U31(a__isNatIListKind(z0),z0) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__U41(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) a__isNatIList(zeros()) -> tt() a__isNatIListKind(z0) -> isNatIListKind(z0) a__isNatIListKind(cons(z0,z1)) -> a__and(a__isNatKind(z0),isNatIListKind(z1)) a__isNatIListKind(nil()) -> tt() a__isNatIListKind(take(z0,z1)) -> a__and(a__isNatKind(z0),isNatIListKind(z1)) a__isNatIListKind(zeros()) -> tt() a__isNatKind(z0) -> isNatKind(z0) a__isNatKind(0()) -> tt() a__isNatKind(length(z0)) -> a__isNatIListKind(z0) a__isNatKind(s(z0)) -> a__isNatKind(z0) a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__U51(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__U61(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U71(a__and(a__and(a__isNatList(z1),isNatIListKind(z1)) ,and(isNat(z0),isNatKind(z0))) ,z1) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__U81(a__and(a__isNatIList(z0),isNatIListKind(z0))) a__take(s(z0),cons(z1,z2)) -> a__U91(a__and(a__and(a__isNatIList(z2),isNatIListKind(z2)) ,and(and(isNat(z0),isNatKind(z0)),and(isNat(z1),isNatKind(z1)))) ,z2 ,z0 ,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U12(z0)) -> a__U12(mark(z0)) mark(U21(z0,z1)) -> a__U21(mark(z0),z1) mark(U22(z0)) -> a__U22(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U32(z0)) -> a__U32(mark(z0)) mark(U41(z0,z1,z2)) -> a__U41(mark(z0),z1,z2) mark(U42(z0,z1)) -> a__U42(mark(z0),z1) mark(U43(z0)) -> a__U43(mark(z0)) mark(U51(z0,z1,z2)) -> a__U51(mark(z0),z1,z2) mark(U52(z0,z1)) -> a__U52(mark(z0),z1) mark(U53(z0)) -> a__U53(mark(z0)) mark(U61(z0,z1,z2)) -> a__U61(mark(z0),z1,z2) mark(U62(z0,z1)) -> a__U62(mark(z0),z1) mark(U63(z0)) -> a__U63(mark(z0)) mark(U71(z0,z1)) -> a__U71(mark(z0),z1) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0,z1,z2,z3)) -> a__U91(mark(z0),z1,z2,z3) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(isNatIListKind(z0)) -> a__isNatIListKind(z0) mark(isNatKind(z0)) -> a__isNatKind(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(zeros()) -> a__zeros() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATILIST/1,A__ISNATILISTKIND/1,A__ISNATKIND/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2 ,A__U11/2,A__U12/1,A__U21/2,A__U22/1,A__U31/2,A__U32/1,A__U41/3,A__U42/2,A__U43/1,A__U51/3,A__U52/2,A__U53/1 ,A__U61/3,A__U62/2,A__U63/1,A__U71/2,A__U81/1,A__U91/4,A__ZEROS/0,MARK/1,a__U11/2,a__U12/1,a__U21/2,a__U22/1 ,a__U31/2,a__U32/1,a__U41/3,a__U42/2,a__U43/1,a__U51/3,a__U52/2,a__U53/1,a__U61/3,a__U62/2,a__U63/1,a__U71/2 ,a__U81/1,a__U91/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatIListKind/1,a__isNatKind/1,a__isNatList/1 ,a__length/1,a__take/2,a__zeros/0,mark/1} / {0/0,U11/2,U12/1,U21/2,U22/1,U31/2,U32/1,U41/3,U42/2,U43/1,U51/3 ,U52/2,U53/1,U61/3,U62/2,U63/1,U71/2,U81/1,U91/4,and/2,c/0,c1/0,c10/2,c11/0,c12/0,c13/0,c14/2,c15/0,c16/2 ,c17/0,c18/0,c19/0,c2/2,c20/2,c21/0,c22/2,c23/0,c24/0,c25/0,c26/2,c27/0,c28/2,c29/0,c3/0,c30/0,c31/0,c32/2 ,c33/0,c34/0,c35/0,c36/1,c37/0,c38/1,c39/0,c4/0,c40/0,c41/2,c42/2,c43/0,c44/2,c45/0,c46/3,c47/0,c48/0,c49/0 ,c5/0,c50/2,c51/2,c52/0,c53/0,c54/1,c55/1,c56/0,c57/0,c58/3,c59/3,c6/2,c60/0,c61/0,c62/4,c63/0,c64/3,c65/4 ,c66/0,c67/1,c68/2,c69/2,c7/0,c70/1,c71/2,c72/2,c73/1,c74/2,c75/2,c76/2,c77/2,c78/2,c79/1,c8/0,c80/2,c81/2 ,c82/2,c83/2,c84/2,c85/2,c86/2,c87/2,c88/2,c89/2,c9/0,c90/2,c91/2,c92/2,c93/1,c94/1,c95/1,c96/0,c97/0,c98/1 ,c99/0,cons/2,isNat/1,isNatIList/1,isNatIListKind/1,isNatKind/1,isNatList/1,length/1,nil/0,s/1,take/2,tt/0 ,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATILIST,A__ISNATILISTKIND ,A__ISNATKIND,A__ISNATLIST,A__LENGTH,A__TAKE,A__U11,A__U12,A__U21,A__U22,A__U31,A__U32,A__U41,A__U42,A__U43 ,A__U51,A__U52,A__U53,A__U61,A__U62,A__U63,A__U71,A__U81,A__U91,A__ZEROS,MARK,a__U11,a__U12,a__U21,a__U22 ,a__U31,a__U32,a__U41,a__U42,a__U43,a__U51,a__U52,a__U53,a__U61,a__U62,a__U63,a__U71,a__U81,a__U91,a__and ,a__isNat,a__isNatIList,a__isNatIListKind,a__isNatKind,a__isNatList,a__length,a__take,a__zeros ,mark} and constructors {0,U11,U12,U21,U22,U31,U32,U41,U42,U43,U51,U52,U53,U61,U62,U63,U71,U81,U91,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,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59 ,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83 ,c84,c85,c86,c87,c88,c89,c9,c90,c91,c92,c93,c94,c95,c96,c97,c98,c99,cons,isNat,isNatIList,isNatIListKind ,isNatKind,isNatList,length,nil,s,take,tt,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) -> c39() A__AND(tt(),z0) -> c38(MARK(z0)) A__ISNAT(z0) -> c43() A__ISNAT(0()) -> c40() A__ISNAT(length(z0)) -> c41(A__U11(a__isNatIListKind(z0),z0),A__ISNATILISTKIND(z0)) A__ISNAT(s(z0)) -> c42(A__U21(a__isNatKind(z0),z0),A__ISNATKIND(z0)) A__ISNATILIST(z0) -> c44(A__U31(a__isNatIListKind(z0),z0),A__ISNATILISTKIND(z0)) A__ISNATILIST(z0) -> c47() A__ISNATILIST(cons(z0,z1)) -> c46(A__U41(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatIListKind(z1)) ,A__ISNATKIND(z0)) A__ISNATILIST(zeros()) -> c45() A__ISNATILISTKIND(z0) -> c52() A__ISNATILISTKIND(cons(z0,z1)) -> c50(A__AND(a__isNatKind(z0),isNatIListKind(z1)),A__ISNATKIND(z0)) A__ISNATILISTKIND(nil()) -> c48() A__ISNATILISTKIND(take(z0,z1)) -> c51(A__AND(a__isNatKind(z0),isNatIListKind(z1)),A__ISNATKIND(z0)) A__ISNATILISTKIND(zeros()) -> c49() A__ISNATKIND(z0) -> c56() A__ISNATKIND(0()) -> c53() A__ISNATKIND(length(z0)) -> c54(A__ISNATILISTKIND(z0)) A__ISNATKIND(s(z0)) -> c55(A__ISNATKIND(z0)) A__ISNATLIST(z0) -> c60() A__ISNATLIST(cons(z0,z1)) -> c58(A__U51(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatIListKind(z1)) ,A__ISNATKIND(z0)) A__ISNATLIST(nil()) -> c57() A__ISNATLIST(take(z0,z1)) -> c59(A__U61(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) ,A__AND(a__isNatKind(z0),isNatIListKind(z1)) ,A__ISNATKIND(z0)) A__LENGTH(z0) -> c63() A__LENGTH(cons(z0,z1)) -> c62(A__U71(a__and(a__and(a__isNatList(z1),isNatIListKind(z1)) ,and(isNat(z0),isNatKind(z0))) ,z1) ,A__AND(a__and(a__isNatList(z1),isNatIListKind(z1)) ,and(isNat(z0),isNatKind(z0))) ,A__AND(a__isNatList(z1),isNatIListKind(z1)) ,A__ISNATLIST(z1)) A__LENGTH(nil()) -> c61() A__TAKE(z0,z1) -> c66() A__TAKE(0(),z0) -> c64(A__U81(a__and(a__isNatIList(z0),isNatIListKind(z0))) ,A__AND(a__isNatIList(z0),isNatIListKind(z0)) ,A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c65(A__U91(a__and(a__and(a__isNatIList(z2),isNatIListKind(z2)) ,and(and(isNat(z0),isNatKind(z0)) ,and(isNat(z1),isNatKind(z1)))) ,z2 ,z0 ,z1) ,A__AND(a__and(a__isNatIList(z2),isNatIListKind(z2)) ,and(and(isNat(z0),isNatKind(z0)),and(isNat(z1),isNatKind(z1)))) ,A__AND(a__isNatIList(z2),isNatIListKind(z2)) ,A__ISNATILIST(z2)) A__U11(z0,z1) -> c3() A__U11(tt(),z0) -> c2(A__U12(a__isNatList(z0)),A__ISNATLIST(z0)) A__U12(z0) -> c5() A__U12(tt()) -> c4() A__U21(z0,z1) -> c7() A__U21(tt(),z0) -> c6(A__U22(a__isNat(z0)),A__ISNAT(z0)) A__U22(z0) -> c9() A__U22(tt()) -> c8() A__U31(z0,z1) -> c11() A__U31(tt(),z0) -> c10(A__U32(a__isNatList(z0)),A__ISNATLIST(z0)) A__U32(z0) -> c13() A__U32(tt()) -> c12() A__U41(z0,z1,z2) -> c15() A__U41(tt(),z0,z1) -> c14(A__U42(a__isNat(z0),z1),A__ISNAT(z0)) A__U42(z0,z1) -> c17() A__U42(tt(),z0) -> c16(A__U43(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U43(z0) -> c19() A__U43(tt()) -> c18() A__U51(z0,z1,z2) -> c21() A__U51(tt(),z0,z1) -> c20(A__U52(a__isNat(z0),z1),A__ISNAT(z0)) A__U52(z0,z1) -> c23() A__U52(tt(),z0) -> c22(A__U53(a__isNatList(z0)),A__ISNATLIST(z0)) A__U53(z0) -> c25() A__U53(tt()) -> c24() A__U61(z0,z1,z2) -> c27() A__U61(tt(),z0,z1) -> c26(A__U62(a__isNat(z0),z1),A__ISNAT(z0)) A__U62(z0,z1) -> c29() A__U62(tt(),z0) -> c28(A__U63(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U63(z0) -> c31() A__U63(tt()) -> c30() A__U71(z0,z1) -> c33() A__U71(tt(),z0) -> c32(A__LENGTH(mark(z0)),MARK(z0)) A__U81(z0) -> c35() A__U81(tt()) -> c34() A__U91(z0,z1,z2,z3) -> c37() A__U91(tt(),z0,z1,z2) -> c36(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c96() MARK(U11(z0,z1)) -> c68(A__U11(mark(z0),z1),MARK(z0)) MARK(U12(z0)) -> c69(A__U12(mark(z0)),MARK(z0)) MARK(U21(z0,z1)) -> c71(A__U21(mark(z0),z1),MARK(z0)) MARK(U22(z0)) -> c72(A__U22(mark(z0)),MARK(z0)) MARK(U31(z0,z1)) -> c74(A__U31(mark(z0),z1),MARK(z0)) MARK(U32(z0)) -> c75(A__U32(mark(z0)),MARK(z0)) MARK(U41(z0,z1,z2)) -> c76(A__U41(mark(z0),z1,z2),MARK(z0)) MARK(U42(z0,z1)) -> c77(A__U42(mark(z0),z1),MARK(z0)) MARK(U43(z0)) -> c78(A__U43(mark(z0)),MARK(z0)) MARK(U51(z0,z1,z2)) -> c80(A__U51(mark(z0),z1,z2),MARK(z0)) MARK(U52(z0,z1)) -> c81(A__U52(mark(z0),z1),MARK(z0)) MARK(U53(z0)) -> c82(A__U53(mark(z0)),MARK(z0)) MARK(U61(z0,z1,z2)) -> c83(A__U61(mark(z0),z1,z2),MARK(z0)) MARK(U62(z0,z1)) -> c84(A__U62(mark(z0),z1),MARK(z0)) MARK(U63(z0)) -> c85(A__U63(mark(z0)),MARK(z0)) MARK(U71(z0,z1)) -> c86(A__U71(mark(z0),z1),MARK(z0)) MARK(U81(z0)) -> c88(A__U81(mark(z0)),MARK(z0)) MARK(U91(z0,z1,z2,z3)) -> c89(A__U91(mark(z0),z1,z2,z3),MARK(z0)) MARK(and(z0,z1)) -> c92(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c95(MARK(z0)) MARK(isNat(z0)) -> c73(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c79(A__ISNATILIST(z0)) MARK(isNatIListKind(z0)) -> c93(A__ISNATILISTKIND(z0)) MARK(isNatKind(z0)) -> c94(A__ISNATKIND(z0)) MARK(isNatList(z0)) -> c70(A__ISNATLIST(z0)) MARK(length(z0)) -> c87(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c99() MARK(s(z0)) -> c98(MARK(z0)) MARK(take(z0,z1)) -> c90(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c91(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c97() MARK(zeros()) -> c67(A__ZEROS()) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> a__U12(a__isNatList(z0)) a__U12(z0) -> U12(z0) a__U12(tt()) -> tt() a__U21(z0,z1) -> U21(z0,z1) a__U21(tt(),z0) -> a__U22(a__isNat(z0)) a__U22(z0) -> U22(z0) a__U22(tt()) -> tt() a__U31(z0,z1) -> U31(z0,z1) a__U31(tt(),z0) -> a__U32(a__isNatList(z0)) a__U32(z0) -> U32(z0) a__U32(tt()) -> tt() a__U41(z0,z1,z2) -> U41(z0,z1,z2) a__U41(tt(),z0,z1) -> a__U42(a__isNat(z0),z1) a__U42(z0,z1) -> U42(z0,z1) a__U42(tt(),z0) -> a__U43(a__isNatIList(z0)) a__U43(z0) -> U43(z0) a__U43(tt()) -> tt() a__U51(z0,z1,z2) -> U51(z0,z1,z2) a__U51(tt(),z0,z1) -> a__U52(a__isNat(z0),z1) a__U52(z0,z1) -> U52(z0,z1) a__U52(tt(),z0) -> a__U53(a__isNatList(z0)) a__U53(z0) -> U53(z0) a__U53(tt()) -> tt() a__U61(z0,z1,z2) -> U61(z0,z1,z2) a__U61(tt(),z0,z1) -> a__U62(a__isNat(z0),z1) a__U62(z0,z1) -> U62(z0,z1) a__U62(tt(),z0) -> a__U63(a__isNatIList(z0)) a__U63(z0) -> U63(z0) a__U63(tt()) -> tt() a__U71(z0,z1) -> U71(z0,z1) a__U71(tt(),z0) -> s(a__length(mark(z0))) a__U81(z0) -> U81(z0) a__U81(tt()) -> nil() a__U91(z0,z1,z2,z3) -> U91(z0,z1,z2,z3) a__U91(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) 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__U11(a__isNatIListKind(z0),z0) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0),z0) a__isNatIList(z0) -> a__U31(a__isNatIListKind(z0),z0) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__U41(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) a__isNatIList(zeros()) -> tt() a__isNatIListKind(z0) -> isNatIListKind(z0) a__isNatIListKind(cons(z0,z1)) -> a__and(a__isNatKind(z0),isNatIListKind(z1)) a__isNatIListKind(nil()) -> tt() a__isNatIListKind(take(z0,z1)) -> a__and(a__isNatKind(z0),isNatIListKind(z1)) a__isNatIListKind(zeros()) -> tt() a__isNatKind(z0) -> isNatKind(z0) a__isNatKind(0()) -> tt() a__isNatKind(length(z0)) -> a__isNatIListKind(z0) a__isNatKind(s(z0)) -> a__isNatKind(z0) a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__U51(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__U61(a__and(a__isNatKind(z0),isNatIListKind(z1)),z0,z1) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U71(a__and(a__and(a__isNatList(z1),isNatIListKind(z1)) ,and(isNat(z0),isNatKind(z0))) ,z1) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__U81(a__and(a__isNatIList(z0),isNatIListKind(z0))) a__take(s(z0),cons(z1,z2)) -> a__U91(a__and(a__and(a__isNatIList(z2),isNatIListKind(z2)) ,and(and(isNat(z0),isNatKind(z0)),and(isNat(z1),isNatKind(z1)))) ,z2 ,z0 ,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U12(z0)) -> a__U12(mark(z0)) mark(U21(z0,z1)) -> a__U21(mark(z0),z1) mark(U22(z0)) -> a__U22(mark(z0)) mark(U31(z0,z1)) -> a__U31(mark(z0),z1) mark(U32(z0)) -> a__U32(mark(z0)) mark(U41(z0,z1,z2)) -> a__U41(mark(z0),z1,z2) mark(U42(z0,z1)) -> a__U42(mark(z0),z1) mark(U43(z0)) -> a__U43(mark(z0)) mark(U51(z0,z1,z2)) -> a__U51(mark(z0),z1,z2) mark(U52(z0,z1)) -> a__U52(mark(z0),z1) mark(U53(z0)) -> a__U53(mark(z0)) mark(U61(z0,z1,z2)) -> a__U61(mark(z0),z1,z2) mark(U62(z0,z1)) -> a__U62(mark(z0),z1) mark(U63(z0)) -> a__U63(mark(z0)) mark(U71(z0,z1)) -> a__U71(mark(z0),z1) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0,z1,z2,z3)) -> a__U91(mark(z0),z1,z2,z3) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(isNatIListKind(z0)) -> a__isNatIListKind(z0) mark(isNatKind(z0)) -> a__isNatKind(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(zeros()) -> a__zeros() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATILIST/1,A__ISNATILISTKIND/1,A__ISNATKIND/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2 ,A__U11/2,A__U12/1,A__U21/2,A__U22/1,A__U31/2,A__U32/1,A__U41/3,A__U42/2,A__U43/1,A__U51/3,A__U52/2,A__U53/1 ,A__U61/3,A__U62/2,A__U63/1,A__U71/2,A__U81/1,A__U91/4,A__ZEROS/0,MARK/1,a__U11/2,a__U12/1,a__U21/2,a__U22/1 ,a__U31/2,a__U32/1,a__U41/3,a__U42/2,a__U43/1,a__U51/3,a__U52/2,a__U53/1,a__U61/3,a__U62/2,a__U63/1,a__U71/2 ,a__U81/1,a__U91/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatIListKind/1,a__isNatKind/1,a__isNatList/1 ,a__length/1,a__take/2,a__zeros/0,mark/1} / {0/0,U11/2,U12/1,U21/2,U22/1,U31/2,U32/1,U41/3,U42/2,U43/1,U51/3 ,U52/2,U53/1,U61/3,U62/2,U63/1,U71/2,U81/1,U91/4,and/2,c/0,c1/0,c10/2,c11/0,c12/0,c13/0,c14/2,c15/0,c16/2 ,c17/0,c18/0,c19/0,c2/2,c20/2,c21/0,c22/2,c23/0,c24/0,c25/0,c26/2,c27/0,c28/2,c29/0,c3/0,c30/0,c31/0,c32/2 ,c33/0,c34/0,c35/0,c36/1,c37/0,c38/1,c39/0,c4/0,c40/0,c41/2,c42/2,c43/0,c44/2,c45/0,c46/3,c47/0,c48/0,c49/0 ,c5/0,c50/2,c51/2,c52/0,c53/0,c54/1,c55/1,c56/0,c57/0,c58/3,c59/3,c6/2,c60/0,c61/0,c62/4,c63/0,c64/3,c65/4 ,c66/0,c67/1,c68/2,c69/2,c7/0,c70/1,c71/2,c72/2,c73/1,c74/2,c75/2,c76/2,c77/2,c78/2,c79/1,c8/0,c80/2,c81/2 ,c82/2,c83/2,c84/2,c85/2,c86/2,c87/2,c88/2,c89/2,c9/0,c90/2,c91/2,c92/2,c93/1,c94/1,c95/1,c96/0,c97/0,c98/1 ,c99/0,cons/2,isNat/1,isNatIList/1,isNatIListKind/1,isNatKind/1,isNatList/1,length/1,nil/0,s/1,take/2,tt/0 ,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATILIST,A__ISNATILISTKIND ,A__ISNATKIND,A__ISNATLIST,A__LENGTH,A__TAKE,A__U11,A__U12,A__U21,A__U22,A__U31,A__U32,A__U41,A__U42,A__U43 ,A__U51,A__U52,A__U53,A__U61,A__U62,A__U63,A__U71,A__U81,A__U91,A__ZEROS,MARK,a__U11,a__U12,a__U21,a__U22 ,a__U31,a__U32,a__U41,a__U42,a__U43,a__U51,a__U52,a__U53,a__U61,a__U62,a__U63,a__U71,a__U81,a__U91,a__and ,a__isNat,a__isNatIList,a__isNatIListKind,a__isNatKind,a__isNatList,a__length,a__take,a__zeros ,mark} and constructors {0,U11,U12,U21,U22,U31,U32,U41,U42,U43,U51,U52,U53,U61,U62,U63,U71,U81,U91,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,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59 ,c6,c60,c61,c62,c63,c64,c65,c66,c67,c68,c69,c7,c70,c71,c72,c73,c74,c75,c76,c77,c78,c79,c8,c80,c81,c82,c83 ,c84,c85,c86,c87,c88,c89,c9,c90,c91,c92,c93,c94,c95,c96,c97,c98,c99,cons,isNat,isNatIList,isNatIListKind ,isNatKind,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: A__ISNATKIND(x){x -> s(x)} = A__ISNATKIND(s(x)) ->^+ c55(A__ISNATKIND(x)) = C[A__ISNATKIND(x) = A__ISNATKIND(x){}] WORST_CASE(Omega(n^1),?)