MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() U11(tt(),L) -> s(length(activate(L))) activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() 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) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,activate,and,cons,isNat,isNatIList,isNatList,length ,nil,s,zeros} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList,n__length,n__nil,n__s ,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() 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))) activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,activate,and,cons,isNat,isNatIList,isNatList,length ,nil,s,zeros} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList,n__length,n__nil,n__s ,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)) activate#(X) -> c_3() activate#(n__0()) -> c_4(0#()) activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) activate#(n__length(X)) -> c_9(length#(X)) activate#(n__nil()) -> c_10(nil#()) activate#(n__s(X)) -> c_11(s#(X)) activate#(n__zeros()) -> c_12(zeros#()) and#(tt(),X) -> c_13(activate#(X)) cons#(X1,X2) -> c_14() isNat#(X) -> c_15() isNat#(n__0()) -> c_16() isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(X) -> c_20() isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatIList#(n__zeros()) -> c_22() isNatList#(X) -> c_23() isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__nil()) -> c_25() length#(X) -> c_26() nil#() -> c_27() s#(X) -> c_28() zeros#() -> c_29(cons#(0(),n__zeros()),0#()) zeros#() -> c_30() 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)) activate#(X) -> c_3() activate#(n__0()) -> c_4(0#()) activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) activate#(n__length(X)) -> c_9(length#(X)) activate#(n__nil()) -> c_10(nil#()) activate#(n__s(X)) -> c_11(s#(X)) activate#(n__zeros()) -> c_12(zeros#()) and#(tt(),X) -> c_13(activate#(X)) cons#(X1,X2) -> c_14() isNat#(X) -> c_15() isNat#(n__0()) -> c_16() isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(X) -> c_20() isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatIList#(n__zeros()) -> c_22() isNatList#(X) -> c_23() isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__nil()) -> c_25() length#(X) -> c_26() nil#() -> c_27() s#(X) -> c_28() zeros#() -> c_29(cons#(0(),n__zeros()),0#()) zeros#() -> c_30() - Weak TRS: 0() -> n__0() U11(tt(),L) -> s(length(activate(L))) activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0,0#/0,U11#/2 ,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1,zeros#/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/1,c_5/1,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/0,c_15/0,c_16/0,c_17/2,c_18/2 ,c_19/2,c_20/0,c_21/4,c_22/0,c_23/0,c_24/4,c_25/0,c_26/0,c_27/0,c_28/0,c_29/2,c_30/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,zeros#} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList ,n__length,n__nil,n__s,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__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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) 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)) activate#(X) -> c_3() activate#(n__0()) -> c_4(0#()) activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) activate#(n__length(X)) -> c_9(length#(X)) activate#(n__nil()) -> c_10(nil#()) activate#(n__s(X)) -> c_11(s#(X)) activate#(n__zeros()) -> c_12(zeros#()) and#(tt(),X) -> c_13(activate#(X)) cons#(X1,X2) -> c_14() isNat#(X) -> c_15() isNat#(n__0()) -> c_16() isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(X) -> c_20() isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatIList#(n__zeros()) -> c_22() isNatList#(X) -> c_23() isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__nil()) -> c_25() length#(X) -> c_26() nil#() -> c_27() s#(X) -> c_28() zeros#() -> c_29(cons#(0(),n__zeros()),0#()) zeros#() -> c_30() * 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)) activate#(X) -> c_3() activate#(n__0()) -> c_4(0#()) activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) activate#(n__length(X)) -> c_9(length#(X)) activate#(n__nil()) -> c_10(nil#()) activate#(n__s(X)) -> c_11(s#(X)) activate#(n__zeros()) -> c_12(zeros#()) and#(tt(),X) -> c_13(activate#(X)) cons#(X1,X2) -> c_14() isNat#(X) -> c_15() isNat#(n__0()) -> c_16() isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(X) -> c_20() isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatIList#(n__zeros()) -> c_22() isNatList#(X) -> c_23() isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__nil()) -> c_25() length#(X) -> c_26() nil#() -> c_27() s#(X) -> c_28() zeros#() -> c_29(cons#(0(),n__zeros()),0#()) zeros#() -> c_30() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0,0#/0,U11#/2 ,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1,zeros#/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/1,c_5/1,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/0,c_15/0,c_16/0,c_17/2,c_18/2 ,c_19/2,c_20/0,c_21/4,c_22/0,c_23/0,c_24/4,c_25/0,c_26/0,c_27/0,c_28/0,c_29/2,c_30/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,zeros#} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList ,n__length,n__nil,n__s,n__zeros,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,14,15,16,20,22,23,25,26,27,28,30} by application of Pre({1,3,14,15,16,20,22,23,25,26,27,28,30}) = {2,4,5,6,7,8,9,10,11,12,13,17,18,19,21,24,29}. 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: activate#(X) -> c_3() 4: activate#(n__0()) -> c_4(0#()) 5: activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) 6: activate#(n__isNat(X)) -> c_6(isNat#(X)) 7: activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) 8: activate#(n__isNatList(X)) -> c_8(isNatList#(X)) 9: activate#(n__length(X)) -> c_9(length#(X)) 10: activate#(n__nil()) -> c_10(nil#()) 11: activate#(n__s(X)) -> c_11(s#(X)) 12: activate#(n__zeros()) -> c_12(zeros#()) 13: and#(tt(),X) -> c_13(activate#(X)) 14: cons#(X1,X2) -> c_14() 15: isNat#(X) -> c_15() 16: isNat#(n__0()) -> c_16() 17: isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) 18: isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) 19: isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) 20: isNatIList#(X) -> c_20() 21: isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 22: isNatIList#(n__zeros()) -> c_22() 23: isNatList#(X) -> c_23() 24: isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 25: isNatList#(n__nil()) -> c_25() 26: length#(X) -> c_26() 27: nil#() -> c_27() 28: s#(X) -> c_28() 29: zeros#() -> c_29(cons#(0(),n__zeros()),0#()) 30: zeros#() -> c_30() * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) activate#(n__0()) -> c_4(0#()) activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) activate#(n__length(X)) -> c_9(length#(X)) activate#(n__nil()) -> c_10(nil#()) activate#(n__s(X)) -> c_11(s#(X)) activate#(n__zeros()) -> c_12(zeros#()) and#(tt(),X) -> c_13(activate#(X)) isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) zeros#() -> c_29(cons#(0(),n__zeros()),0#()) - Weak DPs: 0#() -> c_1() activate#(X) -> c_3() cons#(X1,X2) -> c_14() isNat#(X) -> c_15() isNat#(n__0()) -> c_16() isNatIList#(X) -> c_20() isNatIList#(n__zeros()) -> c_22() isNatList#(X) -> c_23() isNatList#(n__nil()) -> c_25() length#(X) -> c_26() nil#() -> c_27() s#(X) -> c_28() zeros#() -> c_30() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0,0#/0,U11#/2 ,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1,zeros#/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/1,c_5/1,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/0,c_15/0,c_16/0,c_17/2,c_18/2 ,c_19/2,c_20/0,c_21/4,c_22/0,c_23/0,c_24/4,c_25/0,c_26/0,c_27/0,c_28/0,c_29/2,c_30/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,zeros#} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList ,n__length,n__nil,n__s,n__zeros,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,7,8,9,17} by application of Pre({2,3,7,8,9,17}) = {1,10,11,12,13,14,15,16}. Here rules are labelled as follows: 1: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) 2: activate#(n__0()) -> c_4(0#()) 3: activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) 4: activate#(n__isNat(X)) -> c_6(isNat#(X)) 5: activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) 6: activate#(n__isNatList(X)) -> c_8(isNatList#(X)) 7: activate#(n__length(X)) -> c_9(length#(X)) 8: activate#(n__nil()) -> c_10(nil#()) 9: activate#(n__s(X)) -> c_11(s#(X)) 10: activate#(n__zeros()) -> c_12(zeros#()) 11: and#(tt(),X) -> c_13(activate#(X)) 12: isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) 13: isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) 14: isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) 15: isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 16: isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 17: zeros#() -> c_29(cons#(0(),n__zeros()),0#()) 18: 0#() -> c_1() 19: activate#(X) -> c_3() 20: cons#(X1,X2) -> c_14() 21: isNat#(X) -> c_15() 22: isNat#(n__0()) -> c_16() 23: isNatIList#(X) -> c_20() 24: isNatIList#(n__zeros()) -> c_22() 25: isNatList#(X) -> c_23() 26: isNatList#(n__nil()) -> c_25() 27: length#(X) -> c_26() 28: nil#() -> c_27() 29: s#(X) -> c_28() 30: zeros#() -> c_30() * Step 6: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) activate#(n__zeros()) -> c_12(zeros#()) and#(tt(),X) -> c_13(activate#(X)) isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_3() activate#(n__0()) -> c_4(0#()) activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) activate#(n__length(X)) -> c_9(length#(X)) activate#(n__nil()) -> c_10(nil#()) activate#(n__s(X)) -> c_11(s#(X)) cons#(X1,X2) -> c_14() isNat#(X) -> c_15() isNat#(n__0()) -> c_16() isNatIList#(X) -> c_20() isNatIList#(n__zeros()) -> c_22() isNatList#(X) -> c_23() isNatList#(n__nil()) -> c_25() length#(X) -> c_26() nil#() -> c_27() s#(X) -> c_28() zeros#() -> c_29(cons#(0(),n__zeros()),0#()) zeros#() -> c_30() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0,0#/0,U11#/2 ,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1,zeros#/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/1,c_5/1,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/0,c_15/0,c_16/0,c_17/2,c_18/2 ,c_19/2,c_20/0,c_21/4,c_22/0,c_23/0,c_24/4,c_25/0,c_26/0,c_27/0,c_28/0,c_29/2,c_30/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,zeros#} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList ,n__length,n__nil,n__s,n__zeros,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {5} by application of Pre({5}) = {1,6,7,8,9,10,11}. Here rules are labelled as follows: 1: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) 2: activate#(n__isNat(X)) -> c_6(isNat#(X)) 3: activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) 4: activate#(n__isNatList(X)) -> c_8(isNatList#(X)) 5: activate#(n__zeros()) -> c_12(zeros#()) 6: and#(tt(),X) -> c_13(activate#(X)) 7: isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) 8: isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) 9: isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) 10: isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 11: isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) 12: 0#() -> c_1() 13: activate#(X) -> c_3() 14: activate#(n__0()) -> c_4(0#()) 15: activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) 16: activate#(n__length(X)) -> c_9(length#(X)) 17: activate#(n__nil()) -> c_10(nil#()) 18: activate#(n__s(X)) -> c_11(s#(X)) 19: cons#(X1,X2) -> c_14() 20: isNat#(X) -> c_15() 21: isNat#(n__0()) -> c_16() 22: isNatIList#(X) -> c_20() 23: isNatIList#(n__zeros()) -> c_22() 24: isNatList#(X) -> c_23() 25: isNatList#(n__nil()) -> c_25() 26: length#(X) -> c_26() 27: nil#() -> c_27() 28: s#(X) -> c_28() 29: zeros#() -> c_29(cons#(0(),n__zeros()),0#()) 30: zeros#() -> c_30() * Step 7: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) and#(tt(),X) -> c_13(activate#(X)) isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_3() activate#(n__0()) -> c_4(0#()) activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) activate#(n__length(X)) -> c_9(length#(X)) activate#(n__nil()) -> c_10(nil#()) activate#(n__s(X)) -> c_11(s#(X)) activate#(n__zeros()) -> c_12(zeros#()) cons#(X1,X2) -> c_14() isNat#(X) -> c_15() isNat#(n__0()) -> c_16() isNatIList#(X) -> c_20() isNatIList#(n__zeros()) -> c_22() isNatList#(X) -> c_23() isNatList#(n__nil()) -> c_25() length#(X) -> c_26() nil#() -> c_27() s#(X) -> c_28() zeros#() -> c_29(cons#(0(),n__zeros()),0#()) zeros#() -> c_30() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0,0#/0,U11#/2 ,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1,zeros#/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/1,c_5/1,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/0,c_15/0,c_16/0,c_17/2,c_18/2 ,c_19/2,c_20/0,c_21/4,c_22/0,c_23/0,c_24/4,c_25/0,c_26/0,c_27/0,c_28/0,c_29/2,c_30/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,zeros#} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList ,n__length,n__nil,n__s,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_12(zeros#()):18 -->_3 activate#(n__s(X)) -> c_11(s#(X)):17 -->_3 activate#(n__nil()) -> c_10(nil#()):16 -->_3 activate#(n__length(X)) -> c_9(length#(X)):15 -->_3 activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)):14 -->_3 activate#(n__0()) -> c_4(0#()):13 -->_3 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_3 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 -->_1 s#(X) -> c_28():28 -->_2 length#(X) -> c_26():26 -->_3 activate#(X) -> c_3():12 2:S:activate#(n__isNat(X)) -> c_6(isNat#(X)) -->_1 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_1 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_1 isNat#(n__0()) -> c_16():21 -->_1 isNat#(X) -> c_15():20 3:S:activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) -->_1 isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)):8 -->_1 isNatIList#(n__zeros()) -> c_22():23 -->_1 isNatIList#(X) -> c_20():22 4:S:activate#(n__isNatList(X)) -> c_8(isNatList#(X)) -->_1 isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_1 isNatList#(n__nil()) -> c_25():25 -->_1 isNatList#(X) -> c_23():24 5:S:and#(tt(),X) -> c_13(activate#(X)) -->_1 activate#(n__zeros()) -> c_12(zeros#()):18 -->_1 activate#(n__s(X)) -> c_11(s#(X)):17 -->_1 activate#(n__nil()) -> c_10(nil#()):16 -->_1 activate#(n__length(X)) -> c_9(length#(X)):15 -->_1 activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)):14 -->_1 activate#(n__0()) -> c_4(0#()):13 -->_1 activate#(X) -> c_3():12 -->_1 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_1 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 6:S:isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) -->_2 activate#(n__zeros()) -> c_12(zeros#()):18 -->_2 activate#(n__s(X)) -> c_11(s#(X)):17 -->_2 activate#(n__nil()) -> c_10(nil#()):16 -->_2 activate#(n__length(X)) -> c_9(length#(X)):15 -->_2 activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)):14 -->_2 activate#(n__0()) -> c_4(0#()):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_1 isNatList#(n__nil()) -> c_25():25 -->_1 isNatList#(X) -> c_23():24 -->_2 activate#(X) -> c_3():12 -->_2 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_2 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 7:S:isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) -->_2 activate#(n__zeros()) -> c_12(zeros#()):18 -->_2 activate#(n__s(X)) -> c_11(s#(X)):17 -->_2 activate#(n__nil()) -> c_10(nil#()):16 -->_2 activate#(n__length(X)) -> c_9(length#(X)):15 -->_2 activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)):14 -->_2 activate#(n__0()) -> c_4(0#()):13 -->_1 isNat#(n__0()) -> c_16():21 -->_1 isNat#(X) -> c_15():20 -->_2 activate#(X) -> c_3():12 -->_1 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_1 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_2 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_2 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 8:S:isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) -->_2 activate#(n__zeros()) -> c_12(zeros#()):18 -->_2 activate#(n__s(X)) -> c_11(s#(X)):17 -->_2 activate#(n__nil()) -> c_10(nil#()):16 -->_2 activate#(n__length(X)) -> c_9(length#(X)):15 -->_2 activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)):14 -->_2 activate#(n__0()) -> c_4(0#()):13 -->_1 isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_1 isNatList#(n__nil()) -> c_25():25 -->_1 isNatList#(X) -> c_23():24 -->_2 activate#(X) -> c_3():12 -->_2 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_2 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 9:S:isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__zeros()) -> c_12(zeros#()):18 -->_3 activate#(n__zeros()) -> c_12(zeros#()):18 -->_4 activate#(n__s(X)) -> c_11(s#(X)):17 -->_3 activate#(n__s(X)) -> c_11(s#(X)):17 -->_4 activate#(n__nil()) -> c_10(nil#()):16 -->_3 activate#(n__nil()) -> c_10(nil#()):16 -->_4 activate#(n__length(X)) -> c_9(length#(X)):15 -->_3 activate#(n__length(X)) -> c_9(length#(X)):15 -->_4 activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)):14 -->_3 activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)):14 -->_4 activate#(n__0()) -> c_4(0#()):13 -->_3 activate#(n__0()) -> c_4(0#()):13 -->_2 isNat#(n__0()) -> c_16():21 -->_2 isNat#(X) -> c_15():20 -->_4 activate#(X) -> c_3():12 -->_3 activate#(X) -> c_3():12 -->_2 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_2 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_1 and#(tt(),X) -> c_13(activate#(X)):5 -->_4 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_3 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_4 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_3 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 10:S:isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_4 activate#(n__zeros()) -> c_12(zeros#()):18 -->_3 activate#(n__zeros()) -> c_12(zeros#()):18 -->_4 activate#(n__s(X)) -> c_11(s#(X)):17 -->_3 activate#(n__s(X)) -> c_11(s#(X)):17 -->_4 activate#(n__nil()) -> c_10(nil#()):16 -->_3 activate#(n__nil()) -> c_10(nil#()):16 -->_4 activate#(n__length(X)) -> c_9(length#(X)):15 -->_3 activate#(n__length(X)) -> c_9(length#(X)):15 -->_4 activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)):14 -->_3 activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)):14 -->_4 activate#(n__0()) -> c_4(0#()):13 -->_3 activate#(n__0()) -> c_4(0#()):13 -->_2 isNat#(n__0()) -> c_16():21 -->_2 isNat#(X) -> c_15():20 -->_4 activate#(X) -> c_3():12 -->_3 activate#(X) -> c_3():12 -->_2 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_2 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_1 and#(tt(),X) -> c_13(activate#(X)):5 -->_4 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_3 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_4 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_3 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 11:W:0#() -> c_1() 12:W:activate#(X) -> c_3() 13:W:activate#(n__0()) -> c_4(0#()) -->_1 0#() -> c_1():11 14:W:activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) -->_1 cons#(X1,X2) -> c_14():19 15:W:activate#(n__length(X)) -> c_9(length#(X)) -->_1 length#(X) -> c_26():26 16:W:activate#(n__nil()) -> c_10(nil#()) -->_1 nil#() -> c_27():27 17:W:activate#(n__s(X)) -> c_11(s#(X)) -->_1 s#(X) -> c_28():28 18:W:activate#(n__zeros()) -> c_12(zeros#()) -->_1 zeros#() -> c_29(cons#(0(),n__zeros()),0#()):29 -->_1 zeros#() -> c_30():30 19:W:cons#(X1,X2) -> c_14() 20:W:isNat#(X) -> c_15() 21:W:isNat#(n__0()) -> c_16() 22:W:isNatIList#(X) -> c_20() 23:W:isNatIList#(n__zeros()) -> c_22() 24:W:isNatList#(X) -> c_23() 25:W:isNatList#(n__nil()) -> c_25() 26:W:length#(X) -> c_26() 27:W:nil#() -> c_27() 28:W:s#(X) -> c_28() 29:W:zeros#() -> c_29(cons#(0(),n__zeros()),0#()) -->_1 cons#(X1,X2) -> c_14():19 -->_2 0#() -> c_1():11 30:W:zeros#() -> c_30() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 22: isNatIList#(X) -> c_20() 23: isNatIList#(n__zeros()) -> c_22() 24: isNatList#(X) -> c_23() 25: isNatList#(n__nil()) -> c_25() 12: activate#(X) -> c_3() 20: isNat#(X) -> c_15() 21: isNat#(n__0()) -> c_16() 13: activate#(n__0()) -> c_4(0#()) 14: activate#(n__cons(X1,X2)) -> c_5(cons#(X1,X2)) 15: activate#(n__length(X)) -> c_9(length#(X)) 26: length#(X) -> c_26() 16: activate#(n__nil()) -> c_10(nil#()) 27: nil#() -> c_27() 17: activate#(n__s(X)) -> c_11(s#(X)) 28: s#(X) -> c_28() 18: activate#(n__zeros()) -> c_12(zeros#()) 30: zeros#() -> c_30() 29: zeros#() -> c_29(cons#(0(),n__zeros()),0#()) 11: 0#() -> c_1() 19: cons#(X1,X2) -> c_14() * Step 8: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) and#(tt(),X) -> c_13(activate#(X)) isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0,0#/0,U11#/2 ,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1,zeros#/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0,c_1/0,c_2/3 ,c_3/0,c_4/1,c_5/1,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/0,c_15/0,c_16/0,c_17/2,c_18/2 ,c_19/2,c_20/0,c_21/4,c_22/0,c_23/0,c_24/4,c_25/0,c_26/0,c_27/0,c_28/0,c_29/2,c_30/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,zeros#} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList ,n__length,n__nil,n__s,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_8(isNatList#(X)):4 -->_3 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 2:S:activate#(n__isNat(X)) -> c_6(isNat#(X)) -->_1 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_1 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 3:S:activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) -->_1 isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)):8 4:S:activate#(n__isNatList(X)) -> c_8(isNatList#(X)) -->_1 isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 5:S:and#(tt(),X) -> c_13(activate#(X)) -->_1 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_1 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 6:S:isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) -->_1 isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_2 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 7:S:isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) -->_1 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_1 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_2 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_2 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 8:S:isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) -->_1 isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_2 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 9:S:isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_2 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_1 and#(tt(),X) -> c_13(activate#(X)):5 -->_4 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_3 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_4 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_3 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 10:S:isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_2 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_1 and#(tt(),X) -> c_13(activate#(X)):5 -->_4 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_3 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_4 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_3 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 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)) * Step 9: RemoveHeads MAYBE + Considered Problem: - Strict DPs: U11#(tt(),L) -> c_2(activate#(L)) activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) and#(tt(),X) -> c_13(activate#(X)) isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0,0#/0,U11#/2 ,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1,zeros#/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/1,c_5/1,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/0,c_15/0,c_16/0,c_17/2,c_18/2 ,c_19/2,c_20/0,c_21/4,c_22/0,c_23/0,c_24/4,c_25/0,c_26/0,c_27/0,c_28/0,c_29/2,c_30/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,zeros#} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList ,n__length,n__nil,n__s,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_8(isNatList#(X)):4 -->_1 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 2:S:activate#(n__isNat(X)) -> c_6(isNat#(X)) -->_1 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_1 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 3:S:activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) -->_1 isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):9 -->_1 isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)):8 4:S:activate#(n__isNatList(X)) -> c_8(isNatList#(X)) -->_1 isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 5:S:and#(tt(),X) -> c_13(activate#(X)) -->_1 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_1 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_1 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 6:S:isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) -->_1 isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_2 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 7:S:isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) -->_1 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_1 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_2 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_2 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 8:S:isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) -->_1 isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)):10 -->_2 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_2 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_2 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 9:S:isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_2 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_1 and#(tt(),X) -> c_13(activate#(X)):5 -->_4 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_3 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_4 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_3 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 10:S:isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) -->_2 isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)):7 -->_2 isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)):6 -->_1 and#(tt(),X) -> c_13(activate#(X)):5 -->_4 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_3 activate#(n__isNatList(X)) -> c_8(isNatList#(X)):4 -->_4 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_3 activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)):3 -->_4 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 -->_3 activate#(n__isNat(X)) -> c_6(isNat#(X)):2 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)))] * Step 10: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__isNat(X)) -> c_6(isNat#(X)) activate#(n__isNatIList(X)) -> c_7(isNatIList#(X)) activate#(n__isNatList(X)) -> c_8(isNatList#(X)) and#(tt(),X) -> c_13(activate#(X)) isNat#(n__length(V1)) -> c_17(isNatList#(activate(V1)),activate#(V1)) isNat#(n__s(V1)) -> c_18(isNat#(activate(V1)),activate#(V1)) isNatIList#(V) -> c_19(isNatList#(activate(V)),activate#(V)) isNatIList#(n__cons(V1,V2)) -> c_21(and#(isNat(activate(V1)),n__isNatIList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) isNatList#(n__cons(V1,V2)) -> c_24(and#(isNat(activate(V1)),n__isNatList(activate(V2))) ,isNat#(activate(V1)) ,activate#(V1) ,activate#(V2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() 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__zeros()) -> zeros() 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() length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,U11/2,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,zeros/0,0#/0,U11#/2 ,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1,zeros#/0} / {n__0/0 ,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1,n__zeros/0,tt/0,c_1/0,c_2/1 ,c_3/0,c_4/1,c_5/1,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/0,c_15/0,c_16/0,c_17/2,c_18/2 ,c_19/2,c_20/0,c_21/4,c_22/0,c_23/0,c_24/4,c_25/0,c_26/0,c_27/0,c_28/0,c_29/2,c_30/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,U11#,activate#,and#,cons#,isNat#,isNatIList# ,isNatList#,length#,nil#,s#,zeros#} and constructors {n__0,n__cons,n__isNat,n__isNatIList,n__isNatList ,n__length,n__nil,n__s,n__zeros,tt} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE