WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__ISNAT(z0) -> c35() A__ISNAT(0()) -> c32() A__ISNAT(length(z0)) -> c33(A__U11(a__isNatList(z0)),A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c34(A__U21(a__isNat(z0)),A__ISNAT(z0)) A__ISNATILIST(z0) -> c36(A__U31(a__isNatList(z0)),A__ISNATLIST(z0)) A__ISNATILIST(z0) -> c39() A__ISNATILIST(cons(z0,z1)) -> c38(A__U41(a__isNat(z0),z1),A__ISNAT(z0)) A__ISNATILIST(zeros()) -> c37() A__ISNATLIST(z0) -> c43() A__ISNATLIST(cons(z0,z1)) -> c41(A__U51(a__isNat(z0),z1),A__ISNAT(z0)) A__ISNATLIST(nil()) -> c40() A__ISNATLIST(take(z0,z1)) -> c42(A__U61(a__isNat(z0),z1),A__ISNAT(z0)) A__LENGTH(z0) -> c46() A__LENGTH(cons(z0,z1)) -> c45(A__U71(a__isNatList(z1),z1,z0),A__ISNATLIST(z1)) A__LENGTH(nil()) -> c44() A__TAKE(z0,z1) -> c49() A__TAKE(0(),z0) -> c47(A__U81(a__isNatIList(z0)),A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c48(A__U91(a__isNatIList(z2),z2,z0,z1),A__ISNATILIST(z2)) A__U11(z0) -> c3() A__U11(tt()) -> c2() A__U21(z0) -> c5() A__U21(tt()) -> c4() A__U31(z0) -> c7() A__U31(tt()) -> c6() A__U41(z0,z1) -> c9() A__U41(tt(),z0) -> c8(A__U42(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U42(z0) -> c11() A__U42(tt()) -> c10() A__U51(z0,z1) -> c13() A__U51(tt(),z0) -> c12(A__U52(a__isNatList(z0)),A__ISNATLIST(z0)) A__U52(z0) -> c15() A__U52(tt()) -> c14() A__U61(z0,z1) -> c17() A__U61(tt(),z0) -> c16(A__U62(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U62(z0) -> c19() A__U62(tt()) -> c18() A__U71(z0,z1,z2) -> c21() A__U71(tt(),z0,z1) -> c20(A__U72(a__isNat(z1),z0),A__ISNAT(z1)) A__U72(z0,z1) -> c23() A__U72(tt(),z0) -> c22(A__LENGTH(mark(z0)),MARK(z0)) A__U81(z0) -> c25() A__U81(tt()) -> c24() A__U91(z0,z1,z2,z3) -> c27() A__U91(tt(),z0,z1,z2) -> c26(A__U92(a__isNat(z1),z0,z1,z2),A__ISNAT(z1)) A__U92(z0,z1,z2,z3) -> c29() A__U92(tt(),z0,z1,z2) -> c28(A__U93(a__isNat(z2),z0,z1,z2),A__ISNAT(z2)) A__U93(z0,z1,z2,z3) -> c31() A__U93(tt(),z0,z1,z2) -> c30(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c73() MARK(U11(z0)) -> c51(A__U11(mark(z0)),MARK(z0)) MARK(U21(z0)) -> c52(A__U21(mark(z0)),MARK(z0)) MARK(U31(z0)) -> c53(A__U31(mark(z0)),MARK(z0)) MARK(U41(z0,z1)) -> c54(A__U41(mark(z0),z1),MARK(z0)) MARK(U42(z0)) -> c55(A__U42(mark(z0)),MARK(z0)) MARK(U51(z0,z1)) -> c57(A__U51(mark(z0),z1),MARK(z0)) MARK(U52(z0)) -> c58(A__U52(mark(z0)),MARK(z0)) MARK(U61(z0,z1)) -> c60(A__U61(mark(z0),z1),MARK(z0)) MARK(U62(z0)) -> c61(A__U62(mark(z0)),MARK(z0)) MARK(U71(z0,z1,z2)) -> c62(A__U71(mark(z0),z1,z2),MARK(z0)) MARK(U72(z0,z1)) -> c63(A__U72(mark(z0),z1),MARK(z0)) MARK(U81(z0)) -> c66(A__U81(mark(z0)),MARK(z0)) MARK(U91(z0,z1,z2,z3)) -> c67(A__U91(mark(z0),z1,z2,z3),MARK(z0)) MARK(U92(z0,z1,z2,z3)) -> c68(A__U92(mark(z0),z1,z2,z3),MARK(z0)) MARK(U93(z0,z1,z2,z3)) -> c69(A__U93(mark(z0),z1,z2,z3),MARK(z0)) MARK(cons(z0,z1)) -> c72(MARK(z0)) MARK(isNat(z0)) -> c64(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c56(A__ISNATILIST(z0)) MARK(isNatList(z0)) -> c59(A__ISNATLIST(z0)) MARK(length(z0)) -> c65(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c76() MARK(s(z0)) -> c75(MARK(z0)) MARK(take(z0,z1)) -> c70(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c71(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c74() MARK(zeros()) -> c50(A__ZEROS()) - Weak TRS: a__U11(z0) -> U11(z0) a__U11(tt()) -> tt() a__U21(z0) -> U21(z0) a__U21(tt()) -> tt() a__U31(z0) -> U31(z0) a__U31(tt()) -> tt() a__U41(z0,z1) -> U41(z0,z1) a__U41(tt(),z0) -> a__U42(a__isNatIList(z0)) a__U42(z0) -> U42(z0) a__U42(tt()) -> tt() a__U51(z0,z1) -> U51(z0,z1) a__U51(tt(),z0) -> a__U52(a__isNatList(z0)) a__U52(z0) -> U52(z0) a__U52(tt()) -> tt() a__U61(z0,z1) -> U61(z0,z1) a__U61(tt(),z0) -> a__U62(a__isNatIList(z0)) a__U62(z0) -> U62(z0) a__U62(tt()) -> tt() a__U71(z0,z1,z2) -> U71(z0,z1,z2) a__U71(tt(),z0,z1) -> a__U72(a__isNat(z1),z0) a__U72(z0,z1) -> U72(z0,z1) a__U72(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) -> a__U92(a__isNat(z1),z0,z1,z2) a__U92(z0,z1,z2,z3) -> U92(z0,z1,z2,z3) a__U92(tt(),z0,z1,z2) -> a__U93(a__isNat(z2),z0,z1,z2) a__U93(z0,z1,z2,z3) -> U93(z0,z1,z2,z3) a__U93(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(length(z0)) -> a__U11(a__isNatList(z0)) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNatIList(z0) -> a__U31(a__isNatList(z0)) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__U41(a__isNat(z0),z1) a__isNatIList(zeros()) -> tt() a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__U51(a__isNat(z0),z1) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__U61(a__isNat(z0),z1) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U71(a__isNatList(z1),z1,z0) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__U81(a__isNatIList(z0)) a__take(s(z0),cons(z1,z2)) -> a__U91(a__isNatIList(z2),z2,z0,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0)) -> a__U11(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0)) -> a__U31(mark(z0)) mark(U41(z0,z1)) -> a__U41(mark(z0),z1) mark(U42(z0)) -> a__U42(mark(z0)) mark(U51(z0,z1)) -> a__U51(mark(z0),z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(U61(z0,z1)) -> a__U61(mark(z0),z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0,z1,z2)) -> a__U71(mark(z0),z1,z2) mark(U72(z0,z1)) -> a__U72(mark(z0),z1) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0,z1,z2,z3)) -> a__U91(mark(z0),z1,z2,z3) mark(U92(z0,z1,z2,z3)) -> a__U92(mark(z0),z1,z2,z3) mark(U93(z0,z1,z2,z3)) -> a__U93(mark(z0),z1,z2,z3) 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(zeros()) -> a__zeros() - Signature: {A__ISNAT/1,A__ISNATILIST/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2,A__U11/1,A__U21/1,A__U31/1,A__U41/2 ,A__U42/1,A__U51/2,A__U52/1,A__U61/2,A__U62/1,A__U71/3,A__U72/2,A__U81/1,A__U91/4,A__U92/4,A__U93/4 ,A__ZEROS/0,MARK/1,a__U11/1,a__U21/1,a__U31/1,a__U41/2,a__U42/1,a__U51/2,a__U52/1,a__U61/2,a__U62/1,a__U71/3 ,a__U72/2,a__U81/1,a__U91/4,a__U92/4,a__U93/4,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1 ,a__take/2,a__zeros/0,mark/1} / {0/0,U11/1,U21/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/2,U62/1,U71/3,U72/2,U81/1 ,U91/4,U92/4,U93/4,c/0,c1/0,c10/0,c11/0,c12/2,c13/0,c14/0,c15/0,c16/2,c17/0,c18/0,c19/0,c2/0,c20/2,c21/0 ,c22/2,c23/0,c24/0,c25/0,c26/2,c27/0,c28/2,c29/0,c3/0,c30/1,c31/0,c32/0,c33/2,c34/2,c35/0,c36/2,c37/0,c38/2 ,c39/0,c4/0,c40/0,c41/2,c42/2,c43/0,c44/0,c45/2,c46/0,c47/2,c48/2,c49/0,c5/0,c50/1,c51/2,c52/2,c53/2,c54/2 ,c55/2,c56/1,c57/2,c58/2,c59/1,c6/0,c60/2,c61/2,c62/2,c63/2,c64/1,c65/2,c66/2,c67/2,c68/2,c69/2,c7/0,c70/2 ,c71/2,c72/1,c73/0,c74/0,c75/1,c76/0,c8/2,c9/0,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1 ,take/2,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ISNAT,A__ISNATILIST,A__ISNATLIST,A__LENGTH,A__TAKE ,A__U11,A__U21,A__U31,A__U41,A__U42,A__U51,A__U52,A__U61,A__U62,A__U71,A__U72,A__U81,A__U91,A__U92,A__U93 ,A__ZEROS,MARK,a__U11,a__U21,a__U31,a__U41,a__U42,a__U51,a__U52,a__U61,a__U62,a__U71,a__U72,a__U81,a__U91 ,a__U92,a__U93,a__isNat,a__isNatIList,a__isNatList,a__length,a__take,a__zeros,mark} and constructors {0,U11 ,U21,U31,U41,U42,U51,U52,U61,U62,U71,U72,U81,U91,U92,U93,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,c8,c9,cons,isNat,isNatIList,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__ISNAT(z0) -> c35() A__ISNAT(0()) -> c32() A__ISNAT(length(z0)) -> c33(A__U11(a__isNatList(z0)),A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c34(A__U21(a__isNat(z0)),A__ISNAT(z0)) A__ISNATILIST(z0) -> c36(A__U31(a__isNatList(z0)),A__ISNATLIST(z0)) A__ISNATILIST(z0) -> c39() A__ISNATILIST(cons(z0,z1)) -> c38(A__U41(a__isNat(z0),z1),A__ISNAT(z0)) A__ISNATILIST(zeros()) -> c37() A__ISNATLIST(z0) -> c43() A__ISNATLIST(cons(z0,z1)) -> c41(A__U51(a__isNat(z0),z1),A__ISNAT(z0)) A__ISNATLIST(nil()) -> c40() A__ISNATLIST(take(z0,z1)) -> c42(A__U61(a__isNat(z0),z1),A__ISNAT(z0)) A__LENGTH(z0) -> c46() A__LENGTH(cons(z0,z1)) -> c45(A__U71(a__isNatList(z1),z1,z0),A__ISNATLIST(z1)) A__LENGTH(nil()) -> c44() A__TAKE(z0,z1) -> c49() A__TAKE(0(),z0) -> c47(A__U81(a__isNatIList(z0)),A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c48(A__U91(a__isNatIList(z2),z2,z0,z1),A__ISNATILIST(z2)) A__U11(z0) -> c3() A__U11(tt()) -> c2() A__U21(z0) -> c5() A__U21(tt()) -> c4() A__U31(z0) -> c7() A__U31(tt()) -> c6() A__U41(z0,z1) -> c9() A__U41(tt(),z0) -> c8(A__U42(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U42(z0) -> c11() A__U42(tt()) -> c10() A__U51(z0,z1) -> c13() A__U51(tt(),z0) -> c12(A__U52(a__isNatList(z0)),A__ISNATLIST(z0)) A__U52(z0) -> c15() A__U52(tt()) -> c14() A__U61(z0,z1) -> c17() A__U61(tt(),z0) -> c16(A__U62(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U62(z0) -> c19() A__U62(tt()) -> c18() A__U71(z0,z1,z2) -> c21() A__U71(tt(),z0,z1) -> c20(A__U72(a__isNat(z1),z0),A__ISNAT(z1)) A__U72(z0,z1) -> c23() A__U72(tt(),z0) -> c22(A__LENGTH(mark(z0)),MARK(z0)) A__U81(z0) -> c25() A__U81(tt()) -> c24() A__U91(z0,z1,z2,z3) -> c27() A__U91(tt(),z0,z1,z2) -> c26(A__U92(a__isNat(z1),z0,z1,z2),A__ISNAT(z1)) A__U92(z0,z1,z2,z3) -> c29() A__U92(tt(),z0,z1,z2) -> c28(A__U93(a__isNat(z2),z0,z1,z2),A__ISNAT(z2)) A__U93(z0,z1,z2,z3) -> c31() A__U93(tt(),z0,z1,z2) -> c30(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c73() MARK(U11(z0)) -> c51(A__U11(mark(z0)),MARK(z0)) MARK(U21(z0)) -> c52(A__U21(mark(z0)),MARK(z0)) MARK(U31(z0)) -> c53(A__U31(mark(z0)),MARK(z0)) MARK(U41(z0,z1)) -> c54(A__U41(mark(z0),z1),MARK(z0)) MARK(U42(z0)) -> c55(A__U42(mark(z0)),MARK(z0)) MARK(U51(z0,z1)) -> c57(A__U51(mark(z0),z1),MARK(z0)) MARK(U52(z0)) -> c58(A__U52(mark(z0)),MARK(z0)) MARK(U61(z0,z1)) -> c60(A__U61(mark(z0),z1),MARK(z0)) MARK(U62(z0)) -> c61(A__U62(mark(z0)),MARK(z0)) MARK(U71(z0,z1,z2)) -> c62(A__U71(mark(z0),z1,z2),MARK(z0)) MARK(U72(z0,z1)) -> c63(A__U72(mark(z0),z1),MARK(z0)) MARK(U81(z0)) -> c66(A__U81(mark(z0)),MARK(z0)) MARK(U91(z0,z1,z2,z3)) -> c67(A__U91(mark(z0),z1,z2,z3),MARK(z0)) MARK(U92(z0,z1,z2,z3)) -> c68(A__U92(mark(z0),z1,z2,z3),MARK(z0)) MARK(U93(z0,z1,z2,z3)) -> c69(A__U93(mark(z0),z1,z2,z3),MARK(z0)) MARK(cons(z0,z1)) -> c72(MARK(z0)) MARK(isNat(z0)) -> c64(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c56(A__ISNATILIST(z0)) MARK(isNatList(z0)) -> c59(A__ISNATLIST(z0)) MARK(length(z0)) -> c65(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c76() MARK(s(z0)) -> c75(MARK(z0)) MARK(take(z0,z1)) -> c70(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c71(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c74() MARK(zeros()) -> c50(A__ZEROS()) - Weak TRS: a__U11(z0) -> U11(z0) a__U11(tt()) -> tt() a__U21(z0) -> U21(z0) a__U21(tt()) -> tt() a__U31(z0) -> U31(z0) a__U31(tt()) -> tt() a__U41(z0,z1) -> U41(z0,z1) a__U41(tt(),z0) -> a__U42(a__isNatIList(z0)) a__U42(z0) -> U42(z0) a__U42(tt()) -> tt() a__U51(z0,z1) -> U51(z0,z1) a__U51(tt(),z0) -> a__U52(a__isNatList(z0)) a__U52(z0) -> U52(z0) a__U52(tt()) -> tt() a__U61(z0,z1) -> U61(z0,z1) a__U61(tt(),z0) -> a__U62(a__isNatIList(z0)) a__U62(z0) -> U62(z0) a__U62(tt()) -> tt() a__U71(z0,z1,z2) -> U71(z0,z1,z2) a__U71(tt(),z0,z1) -> a__U72(a__isNat(z1),z0) a__U72(z0,z1) -> U72(z0,z1) a__U72(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) -> a__U92(a__isNat(z1),z0,z1,z2) a__U92(z0,z1,z2,z3) -> U92(z0,z1,z2,z3) a__U92(tt(),z0,z1,z2) -> a__U93(a__isNat(z2),z0,z1,z2) a__U93(z0,z1,z2,z3) -> U93(z0,z1,z2,z3) a__U93(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(length(z0)) -> a__U11(a__isNatList(z0)) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNatIList(z0) -> a__U31(a__isNatList(z0)) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__U41(a__isNat(z0),z1) a__isNatIList(zeros()) -> tt() a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__U51(a__isNat(z0),z1) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__U61(a__isNat(z0),z1) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U71(a__isNatList(z1),z1,z0) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__U81(a__isNatIList(z0)) a__take(s(z0),cons(z1,z2)) -> a__U91(a__isNatIList(z2),z2,z0,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0)) -> a__U11(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0)) -> a__U31(mark(z0)) mark(U41(z0,z1)) -> a__U41(mark(z0),z1) mark(U42(z0)) -> a__U42(mark(z0)) mark(U51(z0,z1)) -> a__U51(mark(z0),z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(U61(z0,z1)) -> a__U61(mark(z0),z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0,z1,z2)) -> a__U71(mark(z0),z1,z2) mark(U72(z0,z1)) -> a__U72(mark(z0),z1) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0,z1,z2,z3)) -> a__U91(mark(z0),z1,z2,z3) mark(U92(z0,z1,z2,z3)) -> a__U92(mark(z0),z1,z2,z3) mark(U93(z0,z1,z2,z3)) -> a__U93(mark(z0),z1,z2,z3) 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(zeros()) -> a__zeros() - Signature: {A__ISNAT/1,A__ISNATILIST/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2,A__U11/1,A__U21/1,A__U31/1,A__U41/2 ,A__U42/1,A__U51/2,A__U52/1,A__U61/2,A__U62/1,A__U71/3,A__U72/2,A__U81/1,A__U91/4,A__U92/4,A__U93/4 ,A__ZEROS/0,MARK/1,a__U11/1,a__U21/1,a__U31/1,a__U41/2,a__U42/1,a__U51/2,a__U52/1,a__U61/2,a__U62/1,a__U71/3 ,a__U72/2,a__U81/1,a__U91/4,a__U92/4,a__U93/4,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1 ,a__take/2,a__zeros/0,mark/1} / {0/0,U11/1,U21/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/2,U62/1,U71/3,U72/2,U81/1 ,U91/4,U92/4,U93/4,c/0,c1/0,c10/0,c11/0,c12/2,c13/0,c14/0,c15/0,c16/2,c17/0,c18/0,c19/0,c2/0,c20/2,c21/0 ,c22/2,c23/0,c24/0,c25/0,c26/2,c27/0,c28/2,c29/0,c3/0,c30/1,c31/0,c32/0,c33/2,c34/2,c35/0,c36/2,c37/0,c38/2 ,c39/0,c4/0,c40/0,c41/2,c42/2,c43/0,c44/0,c45/2,c46/0,c47/2,c48/2,c49/0,c5/0,c50/1,c51/2,c52/2,c53/2,c54/2 ,c55/2,c56/1,c57/2,c58/2,c59/1,c6/0,c60/2,c61/2,c62/2,c63/2,c64/1,c65/2,c66/2,c67/2,c68/2,c69/2,c7/0,c70/2 ,c71/2,c72/1,c73/0,c74/0,c75/1,c76/0,c8/2,c9/0,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1 ,take/2,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ISNAT,A__ISNATILIST,A__ISNATLIST,A__LENGTH,A__TAKE ,A__U11,A__U21,A__U31,A__U41,A__U42,A__U51,A__U52,A__U61,A__U62,A__U71,A__U72,A__U81,A__U91,A__U92,A__U93 ,A__ZEROS,MARK,a__U11,a__U21,a__U31,a__U41,a__U42,a__U51,a__U52,a__U61,a__U62,a__U71,a__U72,a__U81,a__U91 ,a__U92,a__U93,a__isNat,a__isNatIList,a__isNatList,a__length,a__take,a__zeros,mark} and constructors {0,U11 ,U21,U31,U41,U42,U51,U52,U61,U62,U71,U72,U81,U91,U92,U93,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,c8,c9,cons,isNat,isNatIList,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__ISNAT(z0) -> c35() A__ISNAT(0()) -> c32() A__ISNAT(length(z0)) -> c33(A__U11(a__isNatList(z0)),A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c34(A__U21(a__isNat(z0)),A__ISNAT(z0)) A__ISNATILIST(z0) -> c36(A__U31(a__isNatList(z0)),A__ISNATLIST(z0)) A__ISNATILIST(z0) -> c39() A__ISNATILIST(cons(z0,z1)) -> c38(A__U41(a__isNat(z0),z1),A__ISNAT(z0)) A__ISNATILIST(zeros()) -> c37() A__ISNATLIST(z0) -> c43() A__ISNATLIST(cons(z0,z1)) -> c41(A__U51(a__isNat(z0),z1),A__ISNAT(z0)) A__ISNATLIST(nil()) -> c40() A__ISNATLIST(take(z0,z1)) -> c42(A__U61(a__isNat(z0),z1),A__ISNAT(z0)) A__LENGTH(z0) -> c46() A__LENGTH(cons(z0,z1)) -> c45(A__U71(a__isNatList(z1),z1,z0),A__ISNATLIST(z1)) A__LENGTH(nil()) -> c44() A__TAKE(z0,z1) -> c49() A__TAKE(0(),z0) -> c47(A__U81(a__isNatIList(z0)),A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c48(A__U91(a__isNatIList(z2),z2,z0,z1),A__ISNATILIST(z2)) A__U11(z0) -> c3() A__U11(tt()) -> c2() A__U21(z0) -> c5() A__U21(tt()) -> c4() A__U31(z0) -> c7() A__U31(tt()) -> c6() A__U41(z0,z1) -> c9() A__U41(tt(),z0) -> c8(A__U42(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U42(z0) -> c11() A__U42(tt()) -> c10() A__U51(z0,z1) -> c13() A__U51(tt(),z0) -> c12(A__U52(a__isNatList(z0)),A__ISNATLIST(z0)) A__U52(z0) -> c15() A__U52(tt()) -> c14() A__U61(z0,z1) -> c17() A__U61(tt(),z0) -> c16(A__U62(a__isNatIList(z0)),A__ISNATILIST(z0)) A__U62(z0) -> c19() A__U62(tt()) -> c18() A__U71(z0,z1,z2) -> c21() A__U71(tt(),z0,z1) -> c20(A__U72(a__isNat(z1),z0),A__ISNAT(z1)) A__U72(z0,z1) -> c23() A__U72(tt(),z0) -> c22(A__LENGTH(mark(z0)),MARK(z0)) A__U81(z0) -> c25() A__U81(tt()) -> c24() A__U91(z0,z1,z2,z3) -> c27() A__U91(tt(),z0,z1,z2) -> c26(A__U92(a__isNat(z1),z0,z1,z2),A__ISNAT(z1)) A__U92(z0,z1,z2,z3) -> c29() A__U92(tt(),z0,z1,z2) -> c28(A__U93(a__isNat(z2),z0,z1,z2),A__ISNAT(z2)) A__U93(z0,z1,z2,z3) -> c31() A__U93(tt(),z0,z1,z2) -> c30(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c73() MARK(U11(z0)) -> c51(A__U11(mark(z0)),MARK(z0)) MARK(U21(z0)) -> c52(A__U21(mark(z0)),MARK(z0)) MARK(U31(z0)) -> c53(A__U31(mark(z0)),MARK(z0)) MARK(U41(z0,z1)) -> c54(A__U41(mark(z0),z1),MARK(z0)) MARK(U42(z0)) -> c55(A__U42(mark(z0)),MARK(z0)) MARK(U51(z0,z1)) -> c57(A__U51(mark(z0),z1),MARK(z0)) MARK(U52(z0)) -> c58(A__U52(mark(z0)),MARK(z0)) MARK(U61(z0,z1)) -> c60(A__U61(mark(z0),z1),MARK(z0)) MARK(U62(z0)) -> c61(A__U62(mark(z0)),MARK(z0)) MARK(U71(z0,z1,z2)) -> c62(A__U71(mark(z0),z1,z2),MARK(z0)) MARK(U72(z0,z1)) -> c63(A__U72(mark(z0),z1),MARK(z0)) MARK(U81(z0)) -> c66(A__U81(mark(z0)),MARK(z0)) MARK(U91(z0,z1,z2,z3)) -> c67(A__U91(mark(z0),z1,z2,z3),MARK(z0)) MARK(U92(z0,z1,z2,z3)) -> c68(A__U92(mark(z0),z1,z2,z3),MARK(z0)) MARK(U93(z0,z1,z2,z3)) -> c69(A__U93(mark(z0),z1,z2,z3),MARK(z0)) MARK(cons(z0,z1)) -> c72(MARK(z0)) MARK(isNat(z0)) -> c64(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c56(A__ISNATILIST(z0)) MARK(isNatList(z0)) -> c59(A__ISNATLIST(z0)) MARK(length(z0)) -> c65(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c76() MARK(s(z0)) -> c75(MARK(z0)) MARK(take(z0,z1)) -> c70(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c71(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c74() MARK(zeros()) -> c50(A__ZEROS()) - Weak TRS: a__U11(z0) -> U11(z0) a__U11(tt()) -> tt() a__U21(z0) -> U21(z0) a__U21(tt()) -> tt() a__U31(z0) -> U31(z0) a__U31(tt()) -> tt() a__U41(z0,z1) -> U41(z0,z1) a__U41(tt(),z0) -> a__U42(a__isNatIList(z0)) a__U42(z0) -> U42(z0) a__U42(tt()) -> tt() a__U51(z0,z1) -> U51(z0,z1) a__U51(tt(),z0) -> a__U52(a__isNatList(z0)) a__U52(z0) -> U52(z0) a__U52(tt()) -> tt() a__U61(z0,z1) -> U61(z0,z1) a__U61(tt(),z0) -> a__U62(a__isNatIList(z0)) a__U62(z0) -> U62(z0) a__U62(tt()) -> tt() a__U71(z0,z1,z2) -> U71(z0,z1,z2) a__U71(tt(),z0,z1) -> a__U72(a__isNat(z1),z0) a__U72(z0,z1) -> U72(z0,z1) a__U72(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) -> a__U92(a__isNat(z1),z0,z1,z2) a__U92(z0,z1,z2,z3) -> U92(z0,z1,z2,z3) a__U92(tt(),z0,z1,z2) -> a__U93(a__isNat(z2),z0,z1,z2) a__U93(z0,z1,z2,z3) -> U93(z0,z1,z2,z3) a__U93(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(length(z0)) -> a__U11(a__isNatList(z0)) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNatIList(z0) -> a__U31(a__isNatList(z0)) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__U41(a__isNat(z0),z1) a__isNatIList(zeros()) -> tt() a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__U51(a__isNat(z0),z1) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__U61(a__isNat(z0),z1) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U71(a__isNatList(z1),z1,z0) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__U81(a__isNatIList(z0)) a__take(s(z0),cons(z1,z2)) -> a__U91(a__isNatIList(z2),z2,z0,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0)) -> a__U11(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0)) -> a__U31(mark(z0)) mark(U41(z0,z1)) -> a__U41(mark(z0),z1) mark(U42(z0)) -> a__U42(mark(z0)) mark(U51(z0,z1)) -> a__U51(mark(z0),z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(U61(z0,z1)) -> a__U61(mark(z0),z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0,z1,z2)) -> a__U71(mark(z0),z1,z2) mark(U72(z0,z1)) -> a__U72(mark(z0),z1) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0,z1,z2,z3)) -> a__U91(mark(z0),z1,z2,z3) mark(U92(z0,z1,z2,z3)) -> a__U92(mark(z0),z1,z2,z3) mark(U93(z0,z1,z2,z3)) -> a__U93(mark(z0),z1,z2,z3) 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(zeros()) -> a__zeros() - Signature: {A__ISNAT/1,A__ISNATILIST/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2,A__U11/1,A__U21/1,A__U31/1,A__U41/2 ,A__U42/1,A__U51/2,A__U52/1,A__U61/2,A__U62/1,A__U71/3,A__U72/2,A__U81/1,A__U91/4,A__U92/4,A__U93/4 ,A__ZEROS/0,MARK/1,a__U11/1,a__U21/1,a__U31/1,a__U41/2,a__U42/1,a__U51/2,a__U52/1,a__U61/2,a__U62/1,a__U71/3 ,a__U72/2,a__U81/1,a__U91/4,a__U92/4,a__U93/4,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1 ,a__take/2,a__zeros/0,mark/1} / {0/0,U11/1,U21/1,U31/1,U41/2,U42/1,U51/2,U52/1,U61/2,U62/1,U71/3,U72/2,U81/1 ,U91/4,U92/4,U93/4,c/0,c1/0,c10/0,c11/0,c12/2,c13/0,c14/0,c15/0,c16/2,c17/0,c18/0,c19/0,c2/0,c20/2,c21/0 ,c22/2,c23/0,c24/0,c25/0,c26/2,c27/0,c28/2,c29/0,c3/0,c30/1,c31/0,c32/0,c33/2,c34/2,c35/0,c36/2,c37/0,c38/2 ,c39/0,c4/0,c40/0,c41/2,c42/2,c43/0,c44/0,c45/2,c46/0,c47/2,c48/2,c49/0,c5/0,c50/1,c51/2,c52/2,c53/2,c54/2 ,c55/2,c56/1,c57/2,c58/2,c59/1,c6/0,c60/2,c61/2,c62/2,c63/2,c64/1,c65/2,c66/2,c67/2,c68/2,c69/2,c7/0,c70/2 ,c71/2,c72/1,c73/0,c74/0,c75/1,c76/0,c8/2,c9/0,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1 ,take/2,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__ISNAT,A__ISNATILIST,A__ISNATLIST,A__LENGTH,A__TAKE ,A__U11,A__U21,A__U31,A__U41,A__U42,A__U51,A__U52,A__U61,A__U62,A__U71,A__U72,A__U81,A__U91,A__U92,A__U93 ,A__ZEROS,MARK,a__U11,a__U21,a__U31,a__U41,a__U42,a__U51,a__U52,a__U61,a__U62,a__U71,a__U72,a__U81,a__U91 ,a__U92,a__U93,a__isNat,a__isNatIList,a__isNatList,a__length,a__take,a__zeros,mark} and constructors {0,U11 ,U21,U31,U41,U42,U51,U52,U61,U62,U71,U72,U81,U91,U92,U93,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,c8,c9,cons,isNat,isNatIList,isNatList,length,nil,s,take,tt,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)) ->^+ c34(A__U21(a__isNat(x)),A__ISNAT(x)) = C[A__ISNAT(x) = A__ISNAT(x){}] WORST_CASE(Omega(n^1),?)