MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() U11(tt(),L) -> s(length(activate(L))) U21(tt()) -> nil() U31(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL))) activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) length(cons(N,L)) -> U11(and(isNatList(activate(L)),n__isNat(N)),activate(L)) length(nil()) -> 0() nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) take(0(),IL) -> U21(isNatIList(IL)) take(s(M),cons(N,IL)) -> U31(and(isNatIList(activate(IL)),n__and(isNat(M),n__isNat(N))),activate(IL),M,N) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1 ,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U21,U31,activate,and,cons,isNat,isNatIList ,isNatList,length,nil,s,take,zeros} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. length(cons(N,L)) -> U11(and(isNatList(activate(L)),n__isNat(N)),activate(L)) length(nil()) -> 0() take(0(),IL) -> U21(isNatIList(IL)) take(s(M),cons(N,IL)) -> U31(and(isNatIList(activate(IL)),n__and(isNat(M),n__isNat(N))),activate(IL),M,N) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() U11(tt(),L) -> s(length(activate(L))) U21(tt()) -> nil() U31(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL))) activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1 ,n__take/2,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U21,U31,activate,and,cons,isNat,isNatIList ,isNatList,length,nil,s,take,zeros} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs 0#() -> c_1() U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) U21#(tt()) -> c_3(nil#()) U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) activate#(X) -> c_5() activate#(n__0()) -> c_6(0#()) activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) activate#(n__length(X)) -> c_12(length#(X)) activate#(n__nil()) -> c_13(nil#()) activate#(n__s(X)) -> c_14(s#(X)) activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) activate#(n__zeros()) -> c_16(zeros#()) and#(X1,X2) -> c_17() and#(tt(),X) -> c_18(activate#(X)) cons#(X1,X2) -> c_19() isNat#(X) -> c_20() isNat#(n__0()) -> c_21() isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(X) -> c_25() isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatIList#(n__zeros()) -> c_27() isNatList#(X) -> c_28() isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__nil()) -> c_30() isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) length#(X) -> c_32() nil#() -> c_33() s#(X) -> c_34() take#(X1,X2) -> c_35() zeros#() -> c_36(cons#(0(),n__zeros()),0#()) zeros#() -> c_37() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) U21#(tt()) -> c_3(nil#()) U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) activate#(X) -> c_5() activate#(n__0()) -> c_6(0#()) activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) activate#(n__length(X)) -> c_12(length#(X)) activate#(n__nil()) -> c_13(nil#()) activate#(n__s(X)) -> c_14(s#(X)) activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) activate#(n__zeros()) -> c_16(zeros#()) and#(X1,X2) -> c_17() and#(tt(),X) -> c_18(activate#(X)) cons#(X1,X2) -> c_19() isNat#(X) -> c_20() isNat#(n__0()) -> c_21() isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(X) -> c_25() isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatIList#(n__zeros()) -> c_27() isNatList#(X) -> c_28() isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__nil()) -> c_30() isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) length#(X) -> c_32() nil#() -> c_33() s#(X) -> c_34() take#(X1,X2) -> c_35() zeros#() -> c_36(cons#(0(),n__zeros()),0#()) zeros#() -> c_37() - Weak TRS: 0() -> n__0() U11(tt(),L) -> s(length(activate(L))) U21(tt()) -> nil() U31(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL))) activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1 ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1 ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1 ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2 ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() 0#() -> c_1() U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) U21#(tt()) -> c_3(nil#()) U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) activate#(X) -> c_5() activate#(n__0()) -> c_6(0#()) activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) activate#(n__length(X)) -> c_12(length#(X)) activate#(n__nil()) -> c_13(nil#()) activate#(n__s(X)) -> c_14(s#(X)) activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) activate#(n__zeros()) -> c_16(zeros#()) and#(X1,X2) -> c_17() and#(tt(),X) -> c_18(activate#(X)) cons#(X1,X2) -> c_19() isNat#(X) -> c_20() isNat#(n__0()) -> c_21() isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(X) -> c_25() isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatIList#(n__zeros()) -> c_27() isNatList#(X) -> c_28() isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__nil()) -> c_30() isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) length#(X) -> c_32() nil#() -> c_33() s#(X) -> c_34() take#(X1,X2) -> c_35() zeros#() -> c_36(cons#(0(),n__zeros()),0#()) zeros#() -> c_37() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) U21#(tt()) -> c_3(nil#()) U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) activate#(X) -> c_5() activate#(n__0()) -> c_6(0#()) activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) activate#(n__length(X)) -> c_12(length#(X)) activate#(n__nil()) -> c_13(nil#()) activate#(n__s(X)) -> c_14(s#(X)) activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) activate#(n__zeros()) -> c_16(zeros#()) and#(X1,X2) -> c_17() and#(tt(),X) -> c_18(activate#(X)) cons#(X1,X2) -> c_19() isNat#(X) -> c_20() isNat#(n__0()) -> c_21() isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(X) -> c_25() isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatIList#(n__zeros()) -> c_27() isNatList#(X) -> c_28() isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__nil()) -> c_30() isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) length#(X) -> c_32() nil#() -> c_33() s#(X) -> c_34() take#(X1,X2) -> c_35() zeros#() -> c_36(cons#(0(),n__zeros()),0#()) zeros#() -> c_37() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1 ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1 ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1 ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2 ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,5,17,19,20,21,25,27,28,30,32,33,34,35,37} by application of Pre({1,5,17,19,20,21,25,27,28,30,32,33,34,35,37}) = {2,3,4,6,7,8,9,10,11,12,13,14,15,16,18,22,23,24,26,29 ,31,36}. Here rules are labelled as follows: 1: 0#() -> c_1() 2: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) 3: U21#(tt()) -> c_3(nil#()) 4: U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) 5: activate#(X) -> c_5() 6: activate#(n__0()) -> c_6(0#()) 7: activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) 8: activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) 9: activate#(n__isNat(X)) -> c_9(isNat#(X)) 10: activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) 11: activate#(n__isNatList(X)) -> c_11(isNatList#(X)) 12: activate#(n__length(X)) -> c_12(length#(X)) 13: activate#(n__nil()) -> c_13(nil#()) 14: activate#(n__s(X)) -> c_14(s#(X)) 15: activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) 16: activate#(n__zeros()) -> c_16(zeros#()) 17: and#(X1,X2) -> c_17() 18: and#(tt(),X) -> c_18(activate#(X)) 19: cons#(X1,X2) -> c_19() 20: isNat#(X) -> c_20() 21: isNat#(n__0()) -> c_21() 22: isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) 23: isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) 24: isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) 25: isNatIList#(X) -> c_25() 26: isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 27: isNatIList#(n__zeros()) -> c_27() 28: isNatList#(X) -> c_28() 29: isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 30: isNatList#(n__nil()) -> c_30() 31: isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 32: length#(X) -> c_32() 33: nil#() -> c_33() 34: s#(X) -> c_34() 35: take#(X1,X2) -> c_35() 36: zeros#() -> c_36(cons#(0(),n__zeros()),0#()) 37: zeros#() -> c_37() * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) U21#(tt()) -> c_3(nil#()) U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) activate#(n__0()) -> c_6(0#()) activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) activate#(n__length(X)) -> c_12(length#(X)) activate#(n__nil()) -> c_13(nil#()) activate#(n__s(X)) -> c_14(s#(X)) activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) activate#(n__zeros()) -> c_16(zeros#()) and#(tt(),X) -> c_18(activate#(X)) isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) zeros#() -> c_36(cons#(0(),n__zeros()),0#()) - Weak DPs: 0#() -> c_1() activate#(X) -> c_5() and#(X1,X2) -> c_17() cons#(X1,X2) -> c_19() isNat#(X) -> c_20() isNat#(n__0()) -> c_21() isNatIList#(X) -> c_25() isNatIList#(n__zeros()) -> c_27() isNatList#(X) -> c_28() isNatList#(n__nil()) -> c_30() length#(X) -> c_32() nil#() -> c_33() s#(X) -> c_34() take#(X1,X2) -> c_35() zeros#() -> c_37() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1 ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1 ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1 ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2 ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,4,6,10,11,12,13,22} by application of Pre({2,4,6,10,11,12,13,22}) = {1,3,14,15,16,17,18,19,20,21}. Here rules are labelled as follows: 1: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) 2: U21#(tt()) -> c_3(nil#()) 3: U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) 4: activate#(n__0()) -> c_6(0#()) 5: activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) 6: activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) 7: activate#(n__isNat(X)) -> c_9(isNat#(X)) 8: activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) 9: activate#(n__isNatList(X)) -> c_11(isNatList#(X)) 10: activate#(n__length(X)) -> c_12(length#(X)) 11: activate#(n__nil()) -> c_13(nil#()) 12: activate#(n__s(X)) -> c_14(s#(X)) 13: activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) 14: activate#(n__zeros()) -> c_16(zeros#()) 15: and#(tt(),X) -> c_18(activate#(X)) 16: isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) 17: isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) 18: isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) 19: isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 20: isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 21: isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 22: zeros#() -> c_36(cons#(0(),n__zeros()),0#()) 23: 0#() -> c_1() 24: activate#(X) -> c_5() 25: and#(X1,X2) -> c_17() 26: cons#(X1,X2) -> c_19() 27: isNat#(X) -> c_20() 28: isNat#(n__0()) -> c_21() 29: isNatIList#(X) -> c_25() 30: isNatIList#(n__zeros()) -> c_27() 31: isNatList#(X) -> c_28() 32: isNatList#(n__nil()) -> c_30() 33: length#(X) -> c_32() 34: nil#() -> c_33() 35: s#(X) -> c_34() 36: take#(X1,X2) -> c_35() 37: zeros#() -> c_37() * Step 6: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) activate#(n__zeros()) -> c_16(zeros#()) and#(tt(),X) -> c_18(activate#(X)) isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: 0#() -> c_1() U21#(tt()) -> c_3(nil#()) activate#(X) -> c_5() activate#(n__0()) -> c_6(0#()) activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) activate#(n__length(X)) -> c_12(length#(X)) activate#(n__nil()) -> c_13(nil#()) activate#(n__s(X)) -> c_14(s#(X)) activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) and#(X1,X2) -> c_17() cons#(X1,X2) -> c_19() isNat#(X) -> c_20() isNat#(n__0()) -> c_21() isNatIList#(X) -> c_25() isNatIList#(n__zeros()) -> c_27() isNatList#(X) -> c_28() isNatList#(n__nil()) -> c_30() length#(X) -> c_32() nil#() -> c_33() s#(X) -> c_34() take#(X1,X2) -> c_35() zeros#() -> c_36(cons#(0(),n__zeros()),0#()) zeros#() -> c_37() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1 ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1 ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1 ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2 ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {7} by application of Pre({7}) = {1,2,8,9,10,11,12,13,14}. Here rules are labelled as follows: 1: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) 2: U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) 3: activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) 4: activate#(n__isNat(X)) -> c_9(isNat#(X)) 5: activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) 6: activate#(n__isNatList(X)) -> c_11(isNatList#(X)) 7: activate#(n__zeros()) -> c_16(zeros#()) 8: and#(tt(),X) -> c_18(activate#(X)) 9: isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) 10: isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) 11: isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) 12: isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 13: isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 14: isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 15: 0#() -> c_1() 16: U21#(tt()) -> c_3(nil#()) 17: activate#(X) -> c_5() 18: activate#(n__0()) -> c_6(0#()) 19: activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) 20: activate#(n__length(X)) -> c_12(length#(X)) 21: activate#(n__nil()) -> c_13(nil#()) 22: activate#(n__s(X)) -> c_14(s#(X)) 23: activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) 24: and#(X1,X2) -> c_17() 25: cons#(X1,X2) -> c_19() 26: isNat#(X) -> c_20() 27: isNat#(n__0()) -> c_21() 28: isNatIList#(X) -> c_25() 29: isNatIList#(n__zeros()) -> c_27() 30: isNatList#(X) -> c_28() 31: isNatList#(n__nil()) -> c_30() 32: length#(X) -> c_32() 33: nil#() -> c_33() 34: s#(X) -> c_34() 35: take#(X1,X2) -> c_35() 36: zeros#() -> c_36(cons#(0(),n__zeros()),0#()) 37: zeros#() -> c_37() * Step 7: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) and#(tt(),X) -> c_18(activate#(X)) isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: 0#() -> c_1() U21#(tt()) -> c_3(nil#()) activate#(X) -> c_5() activate#(n__0()) -> c_6(0#()) activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) activate#(n__length(X)) -> c_12(length#(X)) activate#(n__nil()) -> c_13(nil#()) activate#(n__s(X)) -> c_14(s#(X)) activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) activate#(n__zeros()) -> c_16(zeros#()) and#(X1,X2) -> c_17() cons#(X1,X2) -> c_19() isNat#(X) -> c_20() isNat#(n__0()) -> c_21() isNatIList#(X) -> c_25() isNatIList#(n__zeros()) -> c_27() isNatList#(X) -> c_28() isNatList#(n__nil()) -> c_30() length#(X) -> c_32() nil#() -> c_33() s#(X) -> c_34() take#(X1,X2) -> c_35() zeros#() -> c_36(cons#(0(),n__zeros()),0#()) zeros#() -> c_37() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1 ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1 ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1 ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2 ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) -->_3 activate#(n__zeros()) -> c_16(zeros#()):23 -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_3 activate#(n__s(X)) -> c_14(s#(X)):21 -->_3 activate#(n__nil()) -> c_13(nil#()):20 -->_3 activate#(n__length(X)) -> c_12(length#(X)):19 -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_3 activate#(n__0()) -> c_6(0#()):17 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_1 s#(X) -> c_34():34 -->_2 length#(X) -> c_32():32 -->_3 activate#(X) -> c_5():16 2:S:U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) -->_4 activate#(n__zeros()) -> c_16(zeros#()):23 -->_3 activate#(n__zeros()) -> c_16(zeros#()):23 -->_2 activate#(n__zeros()) -> c_16(zeros#()):23 -->_4 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_2 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_4 activate#(n__s(X)) -> c_14(s#(X)):21 -->_3 activate#(n__s(X)) -> c_14(s#(X)):21 -->_2 activate#(n__s(X)) -> c_14(s#(X)):21 -->_4 activate#(n__nil()) -> c_13(nil#()):20 -->_3 activate#(n__nil()) -> c_13(nil#()):20 -->_2 activate#(n__nil()) -> c_13(nil#()):20 -->_4 activate#(n__length(X)) -> c_12(length#(X)):19 -->_3 activate#(n__length(X)) -> c_12(length#(X)):19 -->_2 activate#(n__length(X)) -> c_12(length#(X)):19 -->_4 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_2 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_4 activate#(n__0()) -> c_6(0#()):17 -->_3 activate#(n__0()) -> c_6(0#()):17 -->_2 activate#(n__0()) -> c_6(0#()):17 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_1 cons#(X1,X2) -> c_19():25 -->_4 activate#(X) -> c_5():16 -->_3 activate#(X) -> c_5():16 -->_2 activate#(X) -> c_5():16 3:S:activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_1 and#(X1,X2) -> c_17():24 4:S:activate#(n__isNat(X)) -> c_9(isNat#(X)) -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 isNat#(n__0()) -> c_21():27 -->_1 isNat#(X) -> c_20():26 5:S:activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) -->_1 isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_1 isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)):10 -->_1 isNatIList#(n__zeros()) -> c_27():29 -->_1 isNatIList#(X) -> c_25():28 6:S:activate#(n__isNatList(X)) -> c_11(isNatList#(X)) -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):12 -->_1 isNatList#(n__nil()) -> c_30():31 -->_1 isNatList#(X) -> c_28():30 7:S:and#(tt(),X) -> c_18(activate#(X)) -->_1 activate#(n__zeros()) -> c_16(zeros#()):23 -->_1 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_1 activate#(n__s(X)) -> c_14(s#(X)):21 -->_1 activate#(n__nil()) -> c_13(nil#()):20 -->_1 activate#(n__length(X)) -> c_12(length#(X)):19 -->_1 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_1 activate#(n__0()) -> c_6(0#()):17 -->_1 activate#(X) -> c_5():16 -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 8:S:isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) -->_2 activate#(n__zeros()) -> c_16(zeros#()):23 -->_2 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_2 activate#(n__s(X)) -> c_14(s#(X)):21 -->_2 activate#(n__nil()) -> c_13(nil#()):20 -->_2 activate#(n__length(X)) -> c_12(length#(X)):19 -->_2 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_2 activate#(n__0()) -> c_6(0#()):17 -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):12 -->_1 isNatList#(n__nil()) -> c_30():31 -->_1 isNatList#(X) -> c_28():30 -->_2 activate#(X) -> c_5():16 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 9:S:isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) -->_2 activate#(n__zeros()) -> c_16(zeros#()):23 -->_2 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_2 activate#(n__s(X)) -> c_14(s#(X)):21 -->_2 activate#(n__nil()) -> c_13(nil#()):20 -->_2 activate#(n__length(X)) -> c_12(length#(X)):19 -->_2 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_2 activate#(n__0()) -> c_6(0#()):17 -->_1 isNat#(n__0()) -> c_21():27 -->_1 isNat#(X) -> c_20():26 -->_2 activate#(X) -> c_5():16 -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 10:S:isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) -->_2 activate#(n__zeros()) -> c_16(zeros#()):23 -->_2 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_2 activate#(n__s(X)) -> c_14(s#(X)):21 -->_2 activate#(n__nil()) -> c_13(nil#()):20 -->_2 activate#(n__length(X)) -> c_12(length#(X)):19 -->_2 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_2 activate#(n__0()) -> c_6(0#()):17 -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):12 -->_1 isNatList#(n__nil()) -> c_30():31 -->_1 isNatList#(X) -> c_28():30 -->_2 activate#(X) -> c_5():16 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 11:S:isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__zeros()) -> c_16(zeros#()):23 -->_3 activate#(n__zeros()) -> c_16(zeros#()):23 -->_4 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_4 activate#(n__s(X)) -> c_14(s#(X)):21 -->_3 activate#(n__s(X)) -> c_14(s#(X)):21 -->_4 activate#(n__nil()) -> c_13(nil#()):20 -->_3 activate#(n__nil()) -> c_13(nil#()):20 -->_4 activate#(n__length(X)) -> c_12(length#(X)):19 -->_3 activate#(n__length(X)) -> c_12(length#(X)):19 -->_4 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_4 activate#(n__0()) -> c_6(0#()):17 -->_3 activate#(n__0()) -> c_6(0#()):17 -->_2 isNat#(n__0()) -> c_21():27 -->_2 isNat#(X) -> c_20():26 -->_1 and#(X1,X2) -> c_17():24 -->_4 activate#(X) -> c_5():16 -->_3 activate#(X) -> c_5():16 -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 12:S:isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__zeros()) -> c_16(zeros#()):23 -->_3 activate#(n__zeros()) -> c_16(zeros#()):23 -->_4 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_4 activate#(n__s(X)) -> c_14(s#(X)):21 -->_3 activate#(n__s(X)) -> c_14(s#(X)):21 -->_4 activate#(n__nil()) -> c_13(nil#()):20 -->_3 activate#(n__nil()) -> c_13(nil#()):20 -->_4 activate#(n__length(X)) -> c_12(length#(X)):19 -->_3 activate#(n__length(X)) -> c_12(length#(X)):19 -->_4 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_4 activate#(n__0()) -> c_6(0#()):17 -->_3 activate#(n__0()) -> c_6(0#()):17 -->_2 isNat#(n__0()) -> c_21():27 -->_2 isNat#(X) -> c_20():26 -->_1 and#(X1,X2) -> c_17():24 -->_4 activate#(X) -> c_5():16 -->_3 activate#(X) -> c_5():16 -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 13:S:isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__zeros()) -> c_16(zeros#()):23 -->_3 activate#(n__zeros()) -> c_16(zeros#()):23 -->_4 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22 -->_4 activate#(n__s(X)) -> c_14(s#(X)):21 -->_3 activate#(n__s(X)) -> c_14(s#(X)):21 -->_4 activate#(n__nil()) -> c_13(nil#()):20 -->_3 activate#(n__nil()) -> c_13(nil#()):20 -->_4 activate#(n__length(X)) -> c_12(length#(X)):19 -->_3 activate#(n__length(X)) -> c_12(length#(X)):19 -->_4 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18 -->_4 activate#(n__0()) -> c_6(0#()):17 -->_3 activate#(n__0()) -> c_6(0#()):17 -->_2 isNat#(n__0()) -> c_21():27 -->_2 isNat#(X) -> c_20():26 -->_1 and#(X1,X2) -> c_17():24 -->_4 activate#(X) -> c_5():16 -->_3 activate#(X) -> c_5():16 -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 14:W:0#() -> c_1() 15:W:U21#(tt()) -> c_3(nil#()) -->_1 nil#() -> c_33():33 16:W:activate#(X) -> c_5() 17:W:activate#(n__0()) -> c_6(0#()) -->_1 0#() -> c_1():14 18:W:activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) -->_1 cons#(X1,X2) -> c_19():25 19:W:activate#(n__length(X)) -> c_12(length#(X)) -->_1 length#(X) -> c_32():32 20:W:activate#(n__nil()) -> c_13(nil#()) -->_1 nil#() -> c_33():33 21:W:activate#(n__s(X)) -> c_14(s#(X)) -->_1 s#(X) -> c_34():34 22:W:activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) -->_1 take#(X1,X2) -> c_35():35 23:W:activate#(n__zeros()) -> c_16(zeros#()) -->_1 zeros#() -> c_36(cons#(0(),n__zeros()),0#()):36 -->_1 zeros#() -> c_37():37 24:W:and#(X1,X2) -> c_17() 25:W:cons#(X1,X2) -> c_19() 26:W:isNat#(X) -> c_20() 27:W:isNat#(n__0()) -> c_21() 28:W:isNatIList#(X) -> c_25() 29:W:isNatIList#(n__zeros()) -> c_27() 30:W:isNatList#(X) -> c_28() 31:W:isNatList#(n__nil()) -> c_30() 32:W:length#(X) -> c_32() 33:W:nil#() -> c_33() 34:W:s#(X) -> c_34() 35:W:take#(X1,X2) -> c_35() 36:W:zeros#() -> c_36(cons#(0(),n__zeros()),0#()) -->_1 cons#(X1,X2) -> c_19():25 -->_2 0#() -> c_1():14 37:W:zeros#() -> c_37() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 15: U21#(tt()) -> c_3(nil#()) 28: isNatIList#(X) -> c_25() 29: isNatIList#(n__zeros()) -> c_27() 30: isNatList#(X) -> c_28() 31: isNatList#(n__nil()) -> c_30() 16: activate#(X) -> c_5() 24: and#(X1,X2) -> c_17() 26: isNat#(X) -> c_20() 27: isNat#(n__0()) -> c_21() 17: activate#(n__0()) -> c_6(0#()) 18: activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)) 19: activate#(n__length(X)) -> c_12(length#(X)) 32: length#(X) -> c_32() 20: activate#(n__nil()) -> c_13(nil#()) 33: nil#() -> c_33() 21: activate#(n__s(X)) -> c_14(s#(X)) 34: s#(X) -> c_34() 22: activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)) 35: take#(X1,X2) -> c_35() 23: activate#(n__zeros()) -> c_16(zeros#()) 37: zeros#() -> c_37() 36: zeros#() -> c_36(cons#(0(),n__zeros()),0#()) 14: 0#() -> c_1() 25: cons#(X1,X2) -> c_19() * Step 8: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) and#(tt(),X) -> c_18(activate#(X)) isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1 ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1 ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1 ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2 ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 2:S:U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 3:S:activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) -->_1 and#(tt(),X) -> c_18(activate#(X)):7 4:S:activate#(n__isNat(X)) -> c_9(isNat#(X)) -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 5:S:activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) -->_1 isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_1 isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)):10 6:S:activate#(n__isNatList(X)) -> c_11(isNatList#(X)) -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):12 7:S:and#(tt(),X) -> c_18(activate#(X)) -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 8:S:isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):12 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 9:S:isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 10:S:isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):12 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 11:S:isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 12:S:isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 13:S:isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: U11#(tt(),L) -> c_2(activate#(L)) U31#(tt(),IL,M,N) -> c_4(activate#(N),activate#(M),activate#(IL)) * Step 9: RemoveHeads MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(activate#(L)) U31#(tt(),IL,M,N) -> c_4(activate#(N),activate#(M),activate#(IL)) activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) and#(tt(),X) -> c_18(activate#(X)) isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1 ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1 ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/1,c_3/1,c_4/3,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1 ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2 ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:U11#(tt(),L) -> c_2(activate#(L)) -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 2:S:U31#(tt(),IL,M,N) -> c_4(activate#(N),activate#(M),activate#(IL)) -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 3:S:activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) -->_1 and#(tt(),X) -> c_18(activate#(X)):7 4:S:activate#(n__isNat(X)) -> c_9(isNat#(X)) -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 5:S:activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) -->_1 isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):11 -->_1 isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)):10 6:S:activate#(n__isNatList(X)) -> c_11(isNatList#(X)) -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):12 7:S:and#(tt(),X) -> c_18(activate#(X)) -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 8:S:isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):12 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 9:S:isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 10:S:isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):12 -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 11:S:isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 12:S:isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 13:S:isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9 -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8 -->_1 and#(tt(),X) -> c_18(activate#(X)):7 -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6 -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5 -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4 -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(1,U11#(tt(),L) -> c_2(activate#(L))) ,(2,U31#(tt(),IL,M,N) -> c_4(activate#(N),activate#(M),activate#(IL)))] * Step 10: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)) activate#(n__isNat(X)) -> c_9(isNat#(X)) activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)) activate#(n__isNatList(X)) -> c_11(isNatList#(X)) and#(tt(),X) -> c_18(activate#(X)) isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__and(X1,X2)) -> and(X1,X2) activate(n__cons(X1,X2)) -> cons(X1,X2) activate(n__isNat(X)) -> isNat(X) activate(n__isNatIList(X)) -> isNatIList(X) activate(n__isNatList(X)) -> isNatList(X) activate(n__length(X)) -> length(X) activate(n__nil()) -> nil() activate(n__s(X)) -> s(X) activate(n__take(X1,X2)) -> take(X1,X2) activate(n__zeros()) -> zeros() and(X1,X2) -> n__and(X1,X2) and(tt(),X) -> activate(X) cons(X1,X2) -> n__cons(X1,X2) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__length(V1)) -> isNatList(activate(V1)) isNat(n__s(V1)) -> isNat(activate(V1)) isNatIList(V) -> isNatList(activate(V)) isNatIList(X) -> n__isNatIList(X) isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) isNatIList(n__zeros()) -> tt() isNatList(X) -> n__isNatList(X) isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2))) isNatList(n__nil()) -> tt() isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2 ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1 ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1 ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/1,c_3/1,c_4/3,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1 ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2 ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE