MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: a__U11(X1,X2) -> U11(X1,X2) a__U11(tt(),L) -> s(a__length(mark(L))) a__U21(X) -> U21(X) a__U21(tt()) -> nil() a__U31(X1,X2,X3,X4) -> U31(X1,X2,X3,X4) a__U31(tt(),IL,M,N) -> cons(mark(N),take(M,IL)) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isNat(X) -> isNat(X) a__isNat(0()) -> tt() a__isNat(length(V1)) -> a__isNatList(V1) a__isNat(s(V1)) -> a__isNat(V1) a__isNatIList(V) -> a__isNatList(V) a__isNatIList(X) -> isNatIList(X) a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__isNatIList(zeros()) -> tt() a__isNatList(X) -> isNatList(X) a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) a__isNatList(nil()) -> tt() a__isNatList(take(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__length(X) -> length(X) a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) a__length(nil()) -> 0() a__take(X1,X2) -> take(X1,X2) a__take(0(),IL) -> a__U21(a__isNatIList(IL)) a__take(s(M),cons(N,IL)) -> a__U31(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(X1,X2)) -> a__U11(mark(X1),X2) mark(U21(X)) -> a__U21(mark(X)) mark(U31(X1,X2,X3,X4)) -> a__U31(mark(X1),X2,X3,X4) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(isNat(X)) -> a__isNat(X) mark(isNatIList(X)) -> a__isNatIList(X) mark(isNatList(X)) -> a__isNatList(X) mark(length(X)) -> a__length(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {a__U11/2,a__U21/1,a__U31/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1,a__take/2 ,a__zeros/0,mark/1} / {0/0,U11/2,U21/1,U31/4,and/2,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__U11,a__U21,a__U31,a__and,a__isNat,a__isNatIList ,a__isNatList,a__length,a__take,a__zeros,mark} and constructors {0,U11,U21,U31,and,cons,isNat,isNatIList ,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs a__U11#(X1,X2) -> c_1() a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) a__U21#(X) -> c_3() a__U21#(tt()) -> c_4() a__U31#(X1,X2,X3,X4) -> c_5() a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) a__and#(X1,X2) -> c_7() a__and#(tt(),X) -> c_8(mark#(X)) a__isNat#(X) -> c_9() a__isNat#(0()) -> c_10() a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) a__isNatIList#(V) -> c_13(a__isNatList#(V)) a__isNatIList#(X) -> c_14() a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__isNatIList#(zeros()) -> c_16() a__isNatList#(X) -> c_17() a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) a__isNatList#(nil()) -> c_19() a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__length#(X) -> c_21() a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) a__length#(nil()) -> c_23() a__take#(X1,X2) -> c_24() a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)) a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) a__zeros#() -> c_27() a__zeros#() -> c_28() mark#(0()) -> c_29() mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)) mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) mark#(cons(X1,X2)) -> c_34(mark#(X1)) mark#(isNat(X)) -> c_35(a__isNat#(X)) mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) mark#(isNatList(X)) -> c_37(a__isNatList#(X)) mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) mark#(nil()) -> c_39() mark#(s(X)) -> c_40(mark#(X)) mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(tt()) -> c_42() mark#(zeros()) -> c_43(a__zeros#()) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__U11#(X1,X2) -> c_1() a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) a__U21#(X) -> c_3() a__U21#(tt()) -> c_4() a__U31#(X1,X2,X3,X4) -> c_5() a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) a__and#(X1,X2) -> c_7() a__and#(tt(),X) -> c_8(mark#(X)) a__isNat#(X) -> c_9() a__isNat#(0()) -> c_10() a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) a__isNatIList#(V) -> c_13(a__isNatList#(V)) a__isNatIList#(X) -> c_14() a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__isNatIList#(zeros()) -> c_16() a__isNatList#(X) -> c_17() a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) a__isNatList#(nil()) -> c_19() a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__length#(X) -> c_21() a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) a__length#(nil()) -> c_23() a__take#(X1,X2) -> c_24() a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)) a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) a__zeros#() -> c_27() a__zeros#() -> c_28() mark#(0()) -> c_29() mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)) mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) mark#(cons(X1,X2)) -> c_34(mark#(X1)) mark#(isNat(X)) -> c_35(a__isNat#(X)) mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) mark#(isNatList(X)) -> c_37(a__isNatList#(X)) mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) mark#(nil()) -> c_39() mark#(s(X)) -> c_40(mark#(X)) mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(tt()) -> c_42() mark#(zeros()) -> c_43(a__zeros#()) - Weak TRS: a__U11(X1,X2) -> U11(X1,X2) a__U11(tt(),L) -> s(a__length(mark(L))) a__U21(X) -> U21(X) a__U21(tt()) -> nil() a__U31(X1,X2,X3,X4) -> U31(X1,X2,X3,X4) a__U31(tt(),IL,M,N) -> cons(mark(N),take(M,IL)) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isNat(X) -> isNat(X) a__isNat(0()) -> tt() a__isNat(length(V1)) -> a__isNatList(V1) a__isNat(s(V1)) -> a__isNat(V1) a__isNatIList(V) -> a__isNatList(V) a__isNatIList(X) -> isNatIList(X) a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__isNatIList(zeros()) -> tt() a__isNatList(X) -> isNatList(X) a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) a__isNatList(nil()) -> tt() a__isNatList(take(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__length(X) -> length(X) a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) a__length(nil()) -> 0() a__take(X1,X2) -> take(X1,X2) a__take(0(),IL) -> a__U21(a__isNatIList(IL)) a__take(s(M),cons(N,IL)) -> a__U31(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(X1,X2)) -> a__U11(mark(X1),X2) mark(U21(X)) -> a__U21(mark(X)) mark(U31(X1,X2,X3,X4)) -> a__U31(mark(X1),X2,X3,X4) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(isNat(X)) -> a__isNat(X) mark(isNatIList(X)) -> a__isNatIList(X) mark(isNatList(X)) -> a__isNatList(X) mark(length(X)) -> a__length(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {a__U11/2,a__U21/1,a__U31/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1,a__take/2 ,a__zeros/0,mark/1,a__U11#/2,a__U21#/1,a__U31#/4,a__and#/2,a__isNat#/1,a__isNatIList#/1,a__isNatList#/1 ,a__length#/1,a__take#/2,a__zeros#/0,mark#/1} / {0/0,U11/2,U21/1,U31/4,and/2,cons/2,isNat/1,isNatIList/1 ,isNatList/1,length/1,nil/0,s/1,take/2,tt/0,zeros/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/2,c_16/0,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/3,c_23/0,c_24/0 ,c_25/2,c_26/3,c_27/0,c_28/0,c_29/0,c_30/2,c_31/2,c_32/2,c_33/2,c_34/1,c_35/1,c_36/1,c_37/1,c_38/2,c_39/0 ,c_40/1,c_41/3,c_42/0,c_43/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__U11#,a__U21#,a__U31#,a__and#,a__isNat#,a__isNatIList# ,a__isNatList#,a__length#,a__take#,a__zeros#,mark#} and constructors {0,U11,U21,U31,and,cons,isNat ,isNatIList,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,4,5,7,9,10,14,16,17,19,21,23,24,27,28,29,39,42} by application of Pre({1,3,4,5,7,9,10,14,16,17,19,21,23,24,27,28,29,39,42}) = {2,6,8,11,12,13,15,18,20,22,25,26,30,31,32,33 ,34,35,36,37,38,40,41,43}. Here rules are labelled as follows: 1: a__U11#(X1,X2) -> c_1() 2: a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) 3: a__U21#(X) -> c_3() 4: a__U21#(tt()) -> c_4() 5: a__U31#(X1,X2,X3,X4) -> c_5() 6: a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) 7: a__and#(X1,X2) -> c_7() 8: a__and#(tt(),X) -> c_8(mark#(X)) 9: a__isNat#(X) -> c_9() 10: a__isNat#(0()) -> c_10() 11: a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) 12: a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) 13: a__isNatIList#(V) -> c_13(a__isNatList#(V)) 14: a__isNatIList#(X) -> c_14() 15: a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) 16: a__isNatIList#(zeros()) -> c_16() 17: a__isNatList#(X) -> c_17() 18: a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) 19: a__isNatList#(nil()) -> c_19() 20: a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) 21: a__length#(X) -> c_21() 22: a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) 23: a__length#(nil()) -> c_23() 24: a__take#(X1,X2) -> c_24() 25: a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)) 26: a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) 27: a__zeros#() -> c_27() 28: a__zeros#() -> c_28() 29: mark#(0()) -> c_29() 30: mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) 31: mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)) 32: mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) 33: mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) 34: mark#(cons(X1,X2)) -> c_34(mark#(X1)) 35: mark#(isNat(X)) -> c_35(a__isNat#(X)) 36: mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) 37: mark#(isNatList(X)) -> c_37(a__isNatList#(X)) 38: mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) 39: mark#(nil()) -> c_39() 40: mark#(s(X)) -> c_40(mark#(X)) 41: mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 42: mark#(tt()) -> c_42() 43: mark#(zeros()) -> c_43(a__zeros#()) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) a__and#(tt(),X) -> c_8(mark#(X)) a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) a__isNatIList#(V) -> c_13(a__isNatList#(V)) a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)) a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)) mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) mark#(cons(X1,X2)) -> c_34(mark#(X1)) mark#(isNat(X)) -> c_35(a__isNat#(X)) mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) mark#(isNatList(X)) -> c_37(a__isNatList#(X)) mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) mark#(s(X)) -> c_40(mark#(X)) mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) mark#(zeros()) -> c_43(a__zeros#()) - Weak DPs: a__U11#(X1,X2) -> c_1() a__U21#(X) -> c_3() a__U21#(tt()) -> c_4() a__U31#(X1,X2,X3,X4) -> c_5() a__and#(X1,X2) -> c_7() a__isNat#(X) -> c_9() a__isNat#(0()) -> c_10() a__isNatIList#(X) -> c_14() a__isNatIList#(zeros()) -> c_16() a__isNatList#(X) -> c_17() a__isNatList#(nil()) -> c_19() a__length#(X) -> c_21() a__length#(nil()) -> c_23() a__take#(X1,X2) -> c_24() a__zeros#() -> c_27() a__zeros#() -> c_28() mark#(0()) -> c_29() mark#(nil()) -> c_39() mark#(tt()) -> c_42() - Weak TRS: a__U11(X1,X2) -> U11(X1,X2) a__U11(tt(),L) -> s(a__length(mark(L))) a__U21(X) -> U21(X) a__U21(tt()) -> nil() a__U31(X1,X2,X3,X4) -> U31(X1,X2,X3,X4) a__U31(tt(),IL,M,N) -> cons(mark(N),take(M,IL)) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isNat(X) -> isNat(X) a__isNat(0()) -> tt() a__isNat(length(V1)) -> a__isNatList(V1) a__isNat(s(V1)) -> a__isNat(V1) a__isNatIList(V) -> a__isNatList(V) a__isNatIList(X) -> isNatIList(X) a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__isNatIList(zeros()) -> tt() a__isNatList(X) -> isNatList(X) a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) a__isNatList(nil()) -> tt() a__isNatList(take(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__length(X) -> length(X) a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) a__length(nil()) -> 0() a__take(X1,X2) -> take(X1,X2) a__take(0(),IL) -> a__U21(a__isNatIList(IL)) a__take(s(M),cons(N,IL)) -> a__U31(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(X1,X2)) -> a__U11(mark(X1),X2) mark(U21(X)) -> a__U21(mark(X)) mark(U31(X1,X2,X3,X4)) -> a__U31(mark(X1),X2,X3,X4) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(isNat(X)) -> a__isNat(X) mark(isNatIList(X)) -> a__isNatIList(X) mark(isNatList(X)) -> a__isNatList(X) mark(length(X)) -> a__length(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {a__U11/2,a__U21/1,a__U31/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1,a__take/2 ,a__zeros/0,mark/1,a__U11#/2,a__U21#/1,a__U31#/4,a__and#/2,a__isNat#/1,a__isNatIList#/1,a__isNatList#/1 ,a__length#/1,a__take#/2,a__zeros#/0,mark#/1} / {0/0,U11/2,U21/1,U31/4,and/2,cons/2,isNat/1,isNatIList/1 ,isNatList/1,length/1,nil/0,s/1,take/2,tt/0,zeros/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/2,c_16/0,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/3,c_23/0,c_24/0 ,c_25/2,c_26/3,c_27/0,c_28/0,c_29/0,c_30/2,c_31/2,c_32/2,c_33/2,c_34/1,c_35/1,c_36/1,c_37/1,c_38/2,c_39/0 ,c_40/1,c_41/3,c_42/0,c_43/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__U11#,a__U21#,a__U31#,a__and#,a__isNat#,a__isNatIList# ,a__isNatList#,a__length#,a__take#,a__zeros#,mark#} and constructors {0,U11,U21,U31,and,cons,isNat ,isNatIList,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {24} by application of Pre({24}) = {1,2,3,13,14,15,16,17,21,22,23}. Here rules are labelled as follows: 1: a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) 2: a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) 3: a__and#(tt(),X) -> c_8(mark#(X)) 4: a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) 5: a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) 6: a__isNatIList#(V) -> c_13(a__isNatList#(V)) 7: a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) 8: a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) 9: a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) 10: a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) 11: a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)) 12: a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) 13: mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) 14: mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)) 15: mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) 16: mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) 17: mark#(cons(X1,X2)) -> c_34(mark#(X1)) 18: mark#(isNat(X)) -> c_35(a__isNat#(X)) 19: mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) 20: mark#(isNatList(X)) -> c_37(a__isNatList#(X)) 21: mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) 22: mark#(s(X)) -> c_40(mark#(X)) 23: mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) 24: mark#(zeros()) -> c_43(a__zeros#()) 25: a__U11#(X1,X2) -> c_1() 26: a__U21#(X) -> c_3() 27: a__U21#(tt()) -> c_4() 28: a__U31#(X1,X2,X3,X4) -> c_5() 29: a__and#(X1,X2) -> c_7() 30: a__isNat#(X) -> c_9() 31: a__isNat#(0()) -> c_10() 32: a__isNatIList#(X) -> c_14() 33: a__isNatIList#(zeros()) -> c_16() 34: a__isNatList#(X) -> c_17() 35: a__isNatList#(nil()) -> c_19() 36: a__length#(X) -> c_21() 37: a__length#(nil()) -> c_23() 38: a__take#(X1,X2) -> c_24() 39: a__zeros#() -> c_27() 40: a__zeros#() -> c_28() 41: mark#(0()) -> c_29() 42: mark#(nil()) -> c_39() 43: mark#(tt()) -> c_42() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) a__and#(tt(),X) -> c_8(mark#(X)) a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) a__isNatIList#(V) -> c_13(a__isNatList#(V)) a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)) a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)) mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) mark#(cons(X1,X2)) -> c_34(mark#(X1)) mark#(isNat(X)) -> c_35(a__isNat#(X)) mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) mark#(isNatList(X)) -> c_37(a__isNatList#(X)) mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) mark#(s(X)) -> c_40(mark#(X)) mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak DPs: a__U11#(X1,X2) -> c_1() a__U21#(X) -> c_3() a__U21#(tt()) -> c_4() a__U31#(X1,X2,X3,X4) -> c_5() a__and#(X1,X2) -> c_7() a__isNat#(X) -> c_9() a__isNat#(0()) -> c_10() a__isNatIList#(X) -> c_14() a__isNatIList#(zeros()) -> c_16() a__isNatList#(X) -> c_17() a__isNatList#(nil()) -> c_19() a__length#(X) -> c_21() a__length#(nil()) -> c_23() a__take#(X1,X2) -> c_24() a__zeros#() -> c_27() a__zeros#() -> c_28() mark#(0()) -> c_29() mark#(nil()) -> c_39() mark#(tt()) -> c_42() mark#(zeros()) -> c_43(a__zeros#()) - Weak TRS: a__U11(X1,X2) -> U11(X1,X2) a__U11(tt(),L) -> s(a__length(mark(L))) a__U21(X) -> U21(X) a__U21(tt()) -> nil() a__U31(X1,X2,X3,X4) -> U31(X1,X2,X3,X4) a__U31(tt(),IL,M,N) -> cons(mark(N),take(M,IL)) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isNat(X) -> isNat(X) a__isNat(0()) -> tt() a__isNat(length(V1)) -> a__isNatList(V1) a__isNat(s(V1)) -> a__isNat(V1) a__isNatIList(V) -> a__isNatList(V) a__isNatIList(X) -> isNatIList(X) a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__isNatIList(zeros()) -> tt() a__isNatList(X) -> isNatList(X) a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) a__isNatList(nil()) -> tt() a__isNatList(take(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__length(X) -> length(X) a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) a__length(nil()) -> 0() a__take(X1,X2) -> take(X1,X2) a__take(0(),IL) -> a__U21(a__isNatIList(IL)) a__take(s(M),cons(N,IL)) -> a__U31(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(X1,X2)) -> a__U11(mark(X1),X2) mark(U21(X)) -> a__U21(mark(X)) mark(U31(X1,X2,X3,X4)) -> a__U31(mark(X1),X2,X3,X4) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(isNat(X)) -> a__isNat(X) mark(isNatIList(X)) -> a__isNatIList(X) mark(isNatList(X)) -> a__isNatList(X) mark(length(X)) -> a__length(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {a__U11/2,a__U21/1,a__U31/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1,a__take/2 ,a__zeros/0,mark/1,a__U11#/2,a__U21#/1,a__U31#/4,a__and#/2,a__isNat#/1,a__isNatIList#/1,a__isNatList#/1 ,a__length#/1,a__take#/2,a__zeros#/0,mark#/1} / {0/0,U11/2,U21/1,U31/4,and/2,cons/2,isNat/1,isNatIList/1 ,isNatList/1,length/1,nil/0,s/1,take/2,tt/0,zeros/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/2,c_16/0,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/3,c_23/0,c_24/0 ,c_25/2,c_26/3,c_27/0,c_28/0,c_29/0,c_30/2,c_31/2,c_32/2,c_33/2,c_34/1,c_35/1,c_36/1,c_37/1,c_38/2,c_39/0 ,c_40/1,c_41/3,c_42/0,c_43/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__U11#,a__U21#,a__U31#,a__and#,a__isNat#,a__isNatIList# ,a__isNatList#,a__length#,a__take#,a__zeros#,mark#} and constructors {0,U11,U21,U31,and,cons,isNat ,isNatIList,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) -->_2 mark#(zeros()) -> c_43(a__zeros#()):43 -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)):10 -->_2 mark#(tt()) -> c_42():42 -->_2 mark#(nil()) -> c_39():41 -->_2 mark#(0()) -> c_29():40 -->_1 a__length#(nil()) -> c_23():36 -->_1 a__length#(X) -> c_21():35 2:S:a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) -->_1 mark#(zeros()) -> c_43(a__zeros#()):43 -->_1 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_1 mark#(s(X)) -> c_40(mark#(X)):22 -->_1 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_1 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_1 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_1 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_1 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_1 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_1 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_1 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_1 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 mark#(tt()) -> c_42():42 -->_1 mark#(nil()) -> c_39():41 -->_1 mark#(0()) -> c_29():40 3:S:a__and#(tt(),X) -> c_8(mark#(X)) -->_1 mark#(zeros()) -> c_43(a__zeros#()):43 -->_1 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_1 mark#(s(X)) -> c_40(mark#(X)):22 -->_1 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_1 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_1 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_1 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_1 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_1 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_1 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_1 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_1 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 mark#(tt()) -> c_42():42 -->_1 mark#(nil()) -> c_39():41 -->_1 mark#(0()) -> c_29():40 4:S:a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) -->_1 a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):9 -->_1 a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)):8 -->_1 a__isNatList#(nil()) -> c_19():34 -->_1 a__isNatList#(X) -> c_17():33 5:S:a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) -->_1 a__isNat#(0()) -> c_10():30 -->_1 a__isNat#(X) -> c_9():29 -->_1 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_1 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 6:S:a__isNatIList#(V) -> c_13(a__isNatList#(V)) -->_1 a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):9 -->_1 a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)):8 -->_1 a__isNatList#(nil()) -> c_19():34 -->_1 a__isNatList#(X) -> c_17():33 7:S:a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) -->_2 a__isNat#(0()) -> c_10():30 -->_2 a__isNat#(X) -> c_9():29 -->_1 a__and#(X1,X2) -> c_7():28 -->_2 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_2 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 -->_1 a__and#(tt(),X) -> c_8(mark#(X)):3 8:S:a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) -->_2 a__isNat#(0()) -> c_10():30 -->_2 a__isNat#(X) -> c_9():29 -->_1 a__and#(X1,X2) -> c_7():28 -->_2 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_2 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 -->_1 a__and#(tt(),X) -> c_8(mark#(X)):3 9:S:a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) -->_2 a__isNat#(0()) -> c_10():30 -->_2 a__isNat#(X) -> c_9():29 -->_1 a__and#(X1,X2) -> c_7():28 -->_2 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_2 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 -->_1 a__and#(tt(),X) -> c_8(mark#(X)):3 10:S:a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) -->_3 a__isNatList#(nil()) -> c_19():34 -->_3 a__isNatList#(X) -> c_17():33 -->_2 a__and#(X1,X2) -> c_7():28 -->_1 a__U11#(X1,X2) -> c_1():24 -->_3 a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):9 -->_3 a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)):8 -->_2 a__and#(tt(),X) -> c_8(mark#(X)):3 -->_1 a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)):1 11:S:a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)) -->_2 a__isNatIList#(zeros()) -> c_16():32 -->_2 a__isNatIList#(X) -> c_14():31 -->_1 a__U21#(tt()) -> c_4():26 -->_1 a__U21#(X) -> c_3():25 -->_2 a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):7 -->_2 a__isNatIList#(V) -> c_13(a__isNatList#(V)):6 12:S:a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) -->_3 a__isNatIList#(zeros()) -> c_16():32 -->_3 a__isNatIList#(X) -> c_14():31 -->_2 a__and#(X1,X2) -> c_7():28 -->_1 a__U31#(X1,X2,X3,X4) -> c_5():27 -->_3 a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):7 -->_3 a__isNatIList#(V) -> c_13(a__isNatList#(V)):6 -->_2 a__and#(tt(),X) -> c_8(mark#(X)):3 -->_1 a__U31#(tt(),IL,M,N) -> c_6(mark#(N)):2 13:S:mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) -->_2 mark#(zeros()) -> c_43(a__zeros#()):43 -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(tt()) -> c_42():42 -->_2 mark#(nil()) -> c_39():41 -->_2 mark#(0()) -> c_29():40 -->_1 a__U11#(X1,X2) -> c_1():24 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)):1 14:S:mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)) -->_2 mark#(zeros()) -> c_43(a__zeros#()):43 -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(tt()) -> c_42():42 -->_2 mark#(nil()) -> c_39():41 -->_2 mark#(0()) -> c_29():40 -->_1 a__U21#(tt()) -> c_4():26 -->_1 a__U21#(X) -> c_3():25 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 15:S:mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) -->_2 mark#(zeros()) -> c_43(a__zeros#()):43 -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(tt()) -> c_42():42 -->_2 mark#(nil()) -> c_39():41 -->_2 mark#(0()) -> c_29():40 -->_1 a__U31#(X1,X2,X3,X4) -> c_5():27 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__U31#(tt(),IL,M,N) -> c_6(mark#(N)):2 16:S:mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) -->_2 mark#(zeros()) -> c_43(a__zeros#()):43 -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(tt()) -> c_42():42 -->_2 mark#(nil()) -> c_39():41 -->_2 mark#(0()) -> c_29():40 -->_1 a__and#(X1,X2) -> c_7():28 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__and#(tt(),X) -> c_8(mark#(X)):3 17:S:mark#(cons(X1,X2)) -> c_34(mark#(X1)) -->_1 mark#(zeros()) -> c_43(a__zeros#()):43 -->_1 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_1 mark#(s(X)) -> c_40(mark#(X)):22 -->_1 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_1 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_1 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_1 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_1 mark#(tt()) -> c_42():42 -->_1 mark#(nil()) -> c_39():41 -->_1 mark#(0()) -> c_29():40 -->_1 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_1 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_1 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_1 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_1 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 18:S:mark#(isNat(X)) -> c_35(a__isNat#(X)) -->_1 a__isNat#(0()) -> c_10():30 -->_1 a__isNat#(X) -> c_9():29 -->_1 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_1 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 19:S:mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) -->_1 a__isNatIList#(zeros()) -> c_16():32 -->_1 a__isNatIList#(X) -> c_14():31 -->_1 a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):7 -->_1 a__isNatIList#(V) -> c_13(a__isNatList#(V)):6 20:S:mark#(isNatList(X)) -> c_37(a__isNatList#(X)) -->_1 a__isNatList#(nil()) -> c_19():34 -->_1 a__isNatList#(X) -> c_17():33 -->_1 a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):9 -->_1 a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)):8 21:S:mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) -->_2 mark#(zeros()) -> c_43(a__zeros#()):43 -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(tt()) -> c_42():42 -->_2 mark#(nil()) -> c_39():41 -->_2 mark#(0()) -> c_29():40 -->_1 a__length#(nil()) -> c_23():36 -->_1 a__length#(X) -> c_21():35 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)):10 22:S:mark#(s(X)) -> c_40(mark#(X)) -->_1 mark#(zeros()) -> c_43(a__zeros#()):43 -->_1 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_1 mark#(tt()) -> c_42():42 -->_1 mark#(nil()) -> c_39():41 -->_1 mark#(0()) -> c_29():40 -->_1 mark#(s(X)) -> c_40(mark#(X)):22 -->_1 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_1 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_1 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_1 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_1 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_1 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_1 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_1 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_1 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 23:S:mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(zeros()) -> c_43(a__zeros#()):43 -->_2 mark#(zeros()) -> c_43(a__zeros#()):43 -->_3 mark#(tt()) -> c_42():42 -->_2 mark#(tt()) -> c_42():42 -->_3 mark#(nil()) -> c_39():41 -->_2 mark#(nil()) -> c_39():41 -->_3 mark#(0()) -> c_29():40 -->_2 mark#(0()) -> c_29():40 -->_1 a__take#(X1,X2) -> c_24():37 -->_3 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_3 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_3 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_3 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_3 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_3 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_3 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_3 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_3 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_3 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_3 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)):12 -->_1 a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)):11 24:W:a__U11#(X1,X2) -> c_1() 25:W:a__U21#(X) -> c_3() 26:W:a__U21#(tt()) -> c_4() 27:W:a__U31#(X1,X2,X3,X4) -> c_5() 28:W:a__and#(X1,X2) -> c_7() 29:W:a__isNat#(X) -> c_9() 30:W:a__isNat#(0()) -> c_10() 31:W:a__isNatIList#(X) -> c_14() 32:W:a__isNatIList#(zeros()) -> c_16() 33:W:a__isNatList#(X) -> c_17() 34:W:a__isNatList#(nil()) -> c_19() 35:W:a__length#(X) -> c_21() 36:W:a__length#(nil()) -> c_23() 37:W:a__take#(X1,X2) -> c_24() 38:W:a__zeros#() -> c_27() 39:W:a__zeros#() -> c_28() 40:W:mark#(0()) -> c_29() 41:W:mark#(nil()) -> c_39() 42:W:mark#(tt()) -> c_42() 43:W:mark#(zeros()) -> c_43(a__zeros#()) -->_1 a__zeros#() -> c_28():39 -->_1 a__zeros#() -> c_27():38 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 24: a__U11#(X1,X2) -> c_1() 25: a__U21#(X) -> c_3() 26: a__U21#(tt()) -> c_4() 27: a__U31#(X1,X2,X3,X4) -> c_5() 31: a__isNatIList#(X) -> c_14() 32: a__isNatIList#(zeros()) -> c_16() 28: a__and#(X1,X2) -> c_7() 29: a__isNat#(X) -> c_9() 30: a__isNat#(0()) -> c_10() 33: a__isNatList#(X) -> c_17() 34: a__isNatList#(nil()) -> c_19() 35: a__length#(X) -> c_21() 36: a__length#(nil()) -> c_23() 37: a__take#(X1,X2) -> c_24() 40: mark#(0()) -> c_29() 41: mark#(nil()) -> c_39() 42: mark#(tt()) -> c_42() 43: mark#(zeros()) -> c_43(a__zeros#()) 38: a__zeros#() -> c_27() 39: a__zeros#() -> c_28() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) a__and#(tt(),X) -> c_8(mark#(X)) a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) a__isNatIList#(V) -> c_13(a__isNatList#(V)) a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)) a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)) mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) mark#(cons(X1,X2)) -> c_34(mark#(X1)) mark#(isNat(X)) -> c_35(a__isNat#(X)) mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) mark#(isNatList(X)) -> c_37(a__isNatList#(X)) mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) mark#(s(X)) -> c_40(mark#(X)) mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak TRS: a__U11(X1,X2) -> U11(X1,X2) a__U11(tt(),L) -> s(a__length(mark(L))) a__U21(X) -> U21(X) a__U21(tt()) -> nil() a__U31(X1,X2,X3,X4) -> U31(X1,X2,X3,X4) a__U31(tt(),IL,M,N) -> cons(mark(N),take(M,IL)) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isNat(X) -> isNat(X) a__isNat(0()) -> tt() a__isNat(length(V1)) -> a__isNatList(V1) a__isNat(s(V1)) -> a__isNat(V1) a__isNatIList(V) -> a__isNatList(V) a__isNatIList(X) -> isNatIList(X) a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__isNatIList(zeros()) -> tt() a__isNatList(X) -> isNatList(X) a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) a__isNatList(nil()) -> tt() a__isNatList(take(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__length(X) -> length(X) a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) a__length(nil()) -> 0() a__take(X1,X2) -> take(X1,X2) a__take(0(),IL) -> a__U21(a__isNatIList(IL)) a__take(s(M),cons(N,IL)) -> a__U31(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(X1,X2)) -> a__U11(mark(X1),X2) mark(U21(X)) -> a__U21(mark(X)) mark(U31(X1,X2,X3,X4)) -> a__U31(mark(X1),X2,X3,X4) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(isNat(X)) -> a__isNat(X) mark(isNatIList(X)) -> a__isNatIList(X) mark(isNatList(X)) -> a__isNatList(X) mark(length(X)) -> a__length(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {a__U11/2,a__U21/1,a__U31/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1,a__take/2 ,a__zeros/0,mark/1,a__U11#/2,a__U21#/1,a__U31#/4,a__and#/2,a__isNat#/1,a__isNatIList#/1,a__isNatList#/1 ,a__length#/1,a__take#/2,a__zeros#/0,mark#/1} / {0/0,U11/2,U21/1,U31/4,and/2,cons/2,isNat/1,isNatIList/1 ,isNatList/1,length/1,nil/0,s/1,take/2,tt/0,zeros/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/2,c_16/0,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/3,c_23/0,c_24/0 ,c_25/2,c_26/3,c_27/0,c_28/0,c_29/0,c_30/2,c_31/2,c_32/2,c_33/2,c_34/1,c_35/1,c_36/1,c_37/1,c_38/2,c_39/0 ,c_40/1,c_41/3,c_42/0,c_43/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__U11#,a__U21#,a__U31#,a__and#,a__isNat#,a__isNatIList# ,a__isNatList#,a__length#,a__take#,a__zeros#,mark#} and constructors {0,U11,U21,U31,and,cons,isNat ,isNatIList,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)):10 2:S:a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) -->_1 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_1 mark#(s(X)) -> c_40(mark#(X)):22 -->_1 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_1 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_1 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_1 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_1 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_1 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_1 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_1 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_1 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 3:S:a__and#(tt(),X) -> c_8(mark#(X)) -->_1 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_1 mark#(s(X)) -> c_40(mark#(X)):22 -->_1 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_1 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_1 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_1 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_1 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_1 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_1 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_1 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_1 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 4:S:a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) -->_1 a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):9 -->_1 a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)):8 5:S:a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) -->_1 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_1 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 6:S:a__isNatIList#(V) -> c_13(a__isNatList#(V)) -->_1 a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):9 -->_1 a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)):8 7:S:a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) -->_2 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_2 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 -->_1 a__and#(tt(),X) -> c_8(mark#(X)):3 8:S:a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) -->_2 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_2 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 -->_1 a__and#(tt(),X) -> c_8(mark#(X)):3 9:S:a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) -->_2 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_2 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 -->_1 a__and#(tt(),X) -> c_8(mark#(X)):3 10:S:a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) -->_3 a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):9 -->_3 a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)):8 -->_2 a__and#(tt(),X) -> c_8(mark#(X)):3 -->_1 a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)):1 11:S:a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)) -->_2 a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):7 -->_2 a__isNatIList#(V) -> c_13(a__isNatList#(V)):6 12:S:a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) -->_3 a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):7 -->_3 a__isNatIList#(V) -> c_13(a__isNatList#(V)):6 -->_2 a__and#(tt(),X) -> c_8(mark#(X)):3 -->_1 a__U31#(tt(),IL,M,N) -> c_6(mark#(N)):2 13:S:mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)):1 14:S:mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)) -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 15:S:mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__U31#(tt(),IL,M,N) -> c_6(mark#(N)):2 16:S:mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__and#(tt(),X) -> c_8(mark#(X)):3 17:S:mark#(cons(X1,X2)) -> c_34(mark#(X1)) -->_1 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_1 mark#(s(X)) -> c_40(mark#(X)):22 -->_1 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_1 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_1 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_1 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_1 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_1 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_1 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_1 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_1 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 18:S:mark#(isNat(X)) -> c_35(a__isNat#(X)) -->_1 a__isNat#(s(V1)) -> c_12(a__isNat#(V1)):5 -->_1 a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)):4 19:S:mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) -->_1 a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):7 -->_1 a__isNatIList#(V) -> c_13(a__isNatList#(V)):6 20:S:mark#(isNatList(X)) -> c_37(a__isNatList#(X)) -->_1 a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)):9 -->_1 a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)):8 21:S:mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)):10 22:S:mark#(s(X)) -> c_40(mark#(X)) -->_1 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_1 mark#(s(X)) -> c_40(mark#(X)):22 -->_1 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_1 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_1 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_1 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_1 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_1 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_1 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_1 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_1 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 23:S:mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) -->_3 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_2 mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)):23 -->_3 mark#(s(X)) -> c_40(mark#(X)):22 -->_2 mark#(s(X)) -> c_40(mark#(X)):22 -->_3 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_2 mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)):21 -->_3 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_2 mark#(isNatList(X)) -> c_37(a__isNatList#(X)):20 -->_3 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_2 mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)):19 -->_3 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_2 mark#(isNat(X)) -> c_35(a__isNat#(X)):18 -->_3 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_2 mark#(cons(X1,X2)) -> c_34(mark#(X1)):17 -->_3 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_2 mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)):16 -->_3 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_2 mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)):15 -->_3 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_2 mark#(U21(X)) -> c_31(a__U21#(mark(X)),mark#(X)):14 -->_3 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_2 mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)):13 -->_1 a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)):12 -->_1 a__take#(0(),IL) -> c_25(a__U21#(a__isNatIList(IL)),a__isNatIList#(IL)):11 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: a__take#(0(),IL) -> c_25(a__isNatIList#(IL)) mark#(U21(X)) -> c_31(mark#(X)) * Step 6: Failure MAYBE + Considered Problem: - Strict DPs: a__U11#(tt(),L) -> c_2(a__length#(mark(L)),mark#(L)) a__U31#(tt(),IL,M,N) -> c_6(mark#(N)) a__and#(tt(),X) -> c_8(mark#(X)) a__isNat#(length(V1)) -> c_11(a__isNatList#(V1)) a__isNat#(s(V1)) -> c_12(a__isNat#(V1)) a__isNatIList#(V) -> c_13(a__isNatList#(V)) a__isNatIList#(cons(V1,V2)) -> c_15(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__isNatList#(cons(V1,V2)) -> c_18(a__and#(a__isNat(V1),isNatList(V2)),a__isNat#(V1)) a__isNatList#(take(V1,V2)) -> c_20(a__and#(a__isNat(V1),isNatIList(V2)),a__isNat#(V1)) a__length#(cons(N,L)) -> c_22(a__U11#(a__and(a__isNatList(L),isNat(N)),L) ,a__and#(a__isNatList(L),isNat(N)) ,a__isNatList#(L)) a__take#(0(),IL) -> c_25(a__isNatIList#(IL)) a__take#(s(M),cons(N,IL)) -> c_26(a__U31#(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) ,a__and#(a__isNatIList(IL),and(isNat(M),isNat(N))) ,a__isNatIList#(IL)) mark#(U11(X1,X2)) -> c_30(a__U11#(mark(X1),X2),mark#(X1)) mark#(U21(X)) -> c_31(mark#(X)) mark#(U31(X1,X2,X3,X4)) -> c_32(a__U31#(mark(X1),X2,X3,X4),mark#(X1)) mark#(and(X1,X2)) -> c_33(a__and#(mark(X1),X2),mark#(X1)) mark#(cons(X1,X2)) -> c_34(mark#(X1)) mark#(isNat(X)) -> c_35(a__isNat#(X)) mark#(isNatIList(X)) -> c_36(a__isNatIList#(X)) mark#(isNatList(X)) -> c_37(a__isNatList#(X)) mark#(length(X)) -> c_38(a__length#(mark(X)),mark#(X)) mark#(s(X)) -> c_40(mark#(X)) mark#(take(X1,X2)) -> c_41(a__take#(mark(X1),mark(X2)),mark#(X1),mark#(X2)) - Weak TRS: a__U11(X1,X2) -> U11(X1,X2) a__U11(tt(),L) -> s(a__length(mark(L))) a__U21(X) -> U21(X) a__U21(tt()) -> nil() a__U31(X1,X2,X3,X4) -> U31(X1,X2,X3,X4) a__U31(tt(),IL,M,N) -> cons(mark(N),take(M,IL)) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isNat(X) -> isNat(X) a__isNat(0()) -> tt() a__isNat(length(V1)) -> a__isNatList(V1) a__isNat(s(V1)) -> a__isNat(V1) a__isNatIList(V) -> a__isNatList(V) a__isNatIList(X) -> isNatIList(X) a__isNatIList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__isNatIList(zeros()) -> tt() a__isNatList(X) -> isNatList(X) a__isNatList(cons(V1,V2)) -> a__and(a__isNat(V1),isNatList(V2)) a__isNatList(nil()) -> tt() a__isNatList(take(V1,V2)) -> a__and(a__isNat(V1),isNatIList(V2)) a__length(X) -> length(X) a__length(cons(N,L)) -> a__U11(a__and(a__isNatList(L),isNat(N)),L) a__length(nil()) -> 0() a__take(X1,X2) -> take(X1,X2) a__take(0(),IL) -> a__U21(a__isNatIList(IL)) a__take(s(M),cons(N,IL)) -> a__U31(a__and(a__isNatIList(IL),and(isNat(M),isNat(N))),IL,M,N) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(X1,X2)) -> a__U11(mark(X1),X2) mark(U21(X)) -> a__U21(mark(X)) mark(U31(X1,X2,X3,X4)) -> a__U31(mark(X1),X2,X3,X4) mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(isNat(X)) -> a__isNat(X) mark(isNatIList(X)) -> a__isNatIList(X) mark(isNatList(X)) -> a__isNatList(X) mark(length(X)) -> a__length(mark(X)) mark(nil()) -> nil() mark(s(X)) -> s(mark(X)) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {a__U11/2,a__U21/1,a__U31/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1,a__take/2 ,a__zeros/0,mark/1,a__U11#/2,a__U21#/1,a__U31#/4,a__and#/2,a__isNat#/1,a__isNatIList#/1,a__isNatList#/1 ,a__length#/1,a__take#/2,a__zeros#/0,mark#/1} / {0/0,U11/2,U21/1,U31/4,and/2,cons/2,isNat/1,isNatIList/1 ,isNatList/1,length/1,nil/0,s/1,take/2,tt/0,zeros/0,c_1/0,c_2/2,c_3/0,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0 ,c_10/0,c_11/1,c_12/1,c_13/1,c_14/0,c_15/2,c_16/0,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/3,c_23/0,c_24/0 ,c_25/1,c_26/3,c_27/0,c_28/0,c_29/0,c_30/2,c_31/1,c_32/2,c_33/2,c_34/1,c_35/1,c_36/1,c_37/1,c_38/2,c_39/0 ,c_40/1,c_41/3,c_42/0,c_43/1} - Obligation: innermost runtime complexity wrt. defined symbols {a__U11#,a__U21#,a__U31#,a__and#,a__isNat#,a__isNatIList# ,a__isNatList#,a__length#,a__take#,a__zeros#,mark#} and constructors {0,U11,U21,U31,and,cons,isNat ,isNatIList,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE