MAYBE * Step 1: InnermostRuleRemoval MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) length(cons(N,L)) -> uLength(and(isNat(N),isNatList(activate(L))),activate(L)) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) take(0(),IL) -> uTake1(isNatIList(IL)) take(s(M),cons(N,IL)) -> uTake2(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,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,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,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)) -> uLength(and(isNat(N),isNatList(activate(L))),activate(L)) take(0(),IL) -> uTake1(isNatIList(IL)) take(s(M),cons(N,IL)) -> uTake2(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) All above mentioned rules can be savely removed. * Step 2: DependencyPairs MAYBE + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0} / {n__0/0,n__cons/2,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,activate,and,cons,isNat,isNatIList,isNatList,length,nil ,s,take,uLength,uTake1,uTake2,zeros} and constructors {n__0,n__cons,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() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__nil()) -> c_6(nil#()) activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zeros()) -> c_9(zeros#()) and#(tt(),T) -> c_10() cons#(X1,X2) -> c_11() isNat#(n__0()) -> c_12() isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatIList#(n__zeros()) -> c_17() isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) isNatList#(n__nil()) -> c_19() isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) length#(X) -> c_21() nil#() -> c_22() s#(X) -> c_23() take#(X1,X2) -> c_24() uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) uTake1#(tt()) -> c_26(nil#()) uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) zeros#() -> c_28(cons#(0(),n__zeros()),0#()) zeros#() -> c_29() Weak DPs and mark the set of starting terms. * Step 3: UsableRules MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__nil()) -> c_6(nil#()) activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zeros()) -> c_9(zeros#()) and#(tt(),T) -> c_10() cons#(X1,X2) -> c_11() isNat#(n__0()) -> c_12() isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatIList#(n__zeros()) -> c_17() isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) isNatList#(n__nil()) -> c_19() isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) length#(X) -> c_21() nil#() -> c_22() s#(X) -> c_23() take#(X1,X2) -> c_24() uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) uTake1#(tt()) -> c_26(nil#()) uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) zeros#() -> c_28(cons#(0(),n__zeros()),0#()) zeros#() -> c_29() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) length(X) -> n__length(X) nil() -> n__nil() s(X) -> n__s(X) take(X1,X2) -> n__take(X1,X2) uLength(tt(),L) -> s(length(activate(L))) uTake1(tt()) -> nil() uTake2(tt(),M,N,IL) -> cons(activate(N),n__take(activate(M),activate(IL))) zeros() -> cons(0(),n__zeros()) zeros() -> n__zeros() - Signature: {0/0,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/2,c_6/1,c_7/2,c_8/3,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/5,c_17/0,c_18/5,c_19/0,c_20/5,c_21/0,c_22/0,c_23/0,c_24/0,c_25/3,c_26/1,c_27/4,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,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__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) 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() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__nil()) -> c_6(nil#()) activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zeros()) -> c_9(zeros#()) and#(tt(),T) -> c_10() cons#(X1,X2) -> c_11() isNat#(n__0()) -> c_12() isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatIList#(n__zeros()) -> c_17() isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) isNatList#(n__nil()) -> c_19() isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) length#(X) -> c_21() nil#() -> c_22() s#(X) -> c_23() take#(X1,X2) -> c_24() uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) uTake1#(tt()) -> c_26(nil#()) uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) zeros#() -> c_28(cons#(0(),n__zeros()),0#()) zeros#() -> c_29() * Step 4: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__nil()) -> c_6(nil#()) activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zeros()) -> c_9(zeros#()) and#(tt(),T) -> c_10() cons#(X1,X2) -> c_11() isNat#(n__0()) -> c_12() isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatIList#(n__zeros()) -> c_17() isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) isNatList#(n__nil()) -> c_19() isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) length#(X) -> c_21() nil#() -> c_22() s#(X) -> c_23() take#(X1,X2) -> c_24() uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) uTake1#(tt()) -> c_26(nil#()) uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) zeros#() -> c_28(cons#(0(),n__zeros()),0#()) zeros#() -> c_29() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/2,c_6/1,c_7/2,c_8/3,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/5,c_17/0,c_18/5,c_19/0,c_20/5,c_21/0,c_22/0,c_23/0,c_24/0,c_25/3,c_26/1,c_27/4,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,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,2,10,11,12,17,19,21,22,23,24,29} by application of Pre({1,2,10,11,12,17,19,21,22,23,24,29}) = {3,4,5,6,7,8,9,13,14,15,16,18,20,25,26,27,28}. Here rules are labelled as follows: 1: 0#() -> c_1() 2: activate#(X) -> c_2() 3: activate#(n__0()) -> c_3(0#()) 4: activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) 5: activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) 6: activate#(n__nil()) -> c_6(nil#()) 7: activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) 8: activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 9: activate#(n__zeros()) -> c_9(zeros#()) 10: and#(tt(),T) -> c_10() 11: cons#(X1,X2) -> c_11() 12: isNat#(n__0()) -> c_12() 13: isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) 14: isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) 15: isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) 16: isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) 17: isNatIList#(n__zeros()) -> c_17() 18: isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) 19: isNatList#(n__nil()) -> c_19() 20: isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) 21: length#(X) -> c_21() 22: nil#() -> c_22() 23: s#(X) -> c_23() 24: take#(X1,X2) -> c_24() 25: uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) 26: uTake1#(tt()) -> c_26(nil#()) 27: uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) 28: zeros#() -> c_28(cons#(0(),n__zeros()),0#()) 29: zeros#() -> c_29() * Step 5: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__0()) -> c_3(0#()) activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__nil()) -> c_6(nil#()) activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zeros()) -> c_9(zeros#()) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) uTake1#(tt()) -> c_26(nil#()) uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) zeros#() -> c_28(cons#(0(),n__zeros()),0#()) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() and#(tt(),T) -> c_10() cons#(X1,X2) -> c_11() isNat#(n__0()) -> c_12() isNatIList#(n__zeros()) -> c_17() isNatList#(n__nil()) -> c_19() length#(X) -> c_21() nil#() -> c_22() s#(X) -> c_23() take#(X1,X2) -> c_24() zeros#() -> c_29() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/2,c_6/1,c_7/2,c_8/3,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/5,c_17/0,c_18/5,c_19/0,c_20/5,c_21/0,c_22/0,c_23/0,c_24/0,c_25/3,c_26/1,c_27/4,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,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,4,15,17} by application of Pre({1,4,15,17}) = {2,3,5,6,7,8,9,10,11,12,13,14,16}. Here rules are labelled as follows: 1: activate#(n__0()) -> c_3(0#()) 2: activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) 3: activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) 4: activate#(n__nil()) -> c_6(nil#()) 5: activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) 6: activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 7: activate#(n__zeros()) -> c_9(zeros#()) 8: isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) 9: isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) 10: isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) 11: isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) 12: isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) 13: isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) 14: uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) 15: uTake1#(tt()) -> c_26(nil#()) 16: uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) 17: zeros#() -> c_28(cons#(0(),n__zeros()),0#()) 18: 0#() -> c_1() 19: activate#(X) -> c_2() 20: and#(tt(),T) -> c_10() 21: cons#(X1,X2) -> c_11() 22: isNat#(n__0()) -> c_12() 23: isNatIList#(n__zeros()) -> c_17() 24: isNatList#(n__nil()) -> c_19() 25: length#(X) -> c_21() 26: nil#() -> c_22() 27: s#(X) -> c_23() 28: take#(X1,X2) -> c_24() 29: zeros#() -> c_29() * Step 6: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) activate#(n__zeros()) -> c_9(zeros#()) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__nil()) -> c_6(nil#()) and#(tt(),T) -> c_10() cons#(X1,X2) -> c_11() isNat#(n__0()) -> c_12() isNatIList#(n__zeros()) -> c_17() isNatList#(n__nil()) -> c_19() length#(X) -> c_21() nil#() -> c_22() s#(X) -> c_23() take#(X1,X2) -> c_24() uTake1#(tt()) -> c_26(nil#()) zeros#() -> c_28(cons#(0(),n__zeros()),0#()) zeros#() -> c_29() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/2,c_6/1,c_7/2,c_8/3,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/5,c_17/0,c_18/5,c_19/0,c_20/5,c_21/0,c_22/0,c_23/0,c_24/0,c_25/3,c_26/1,c_27/4,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,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 {5} by application of Pre({5}) = {1,2,3,4,6,7,8,9,10,11,12,13}. Here rules are labelled as follows: 1: activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) 2: activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) 3: activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) 4: activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) 5: activate#(n__zeros()) -> c_9(zeros#()) 6: isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) 7: isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) 8: isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) 9: isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) 10: isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) 11: isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) 12: uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) 13: uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) 14: 0#() -> c_1() 15: activate#(X) -> c_2() 16: activate#(n__0()) -> c_3(0#()) 17: activate#(n__nil()) -> c_6(nil#()) 18: and#(tt(),T) -> c_10() 19: cons#(X1,X2) -> c_11() 20: isNat#(n__0()) -> c_12() 21: isNatIList#(n__zeros()) -> c_17() 22: isNatList#(n__nil()) -> c_19() 23: length#(X) -> c_21() 24: nil#() -> c_22() 25: s#(X) -> c_23() 26: take#(X1,X2) -> c_24() 27: uTake1#(tt()) -> c_26(nil#()) 28: zeros#() -> c_28(cons#(0(),n__zeros()),0#()) 29: zeros#() -> c_29() * Step 7: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) - Weak DPs: 0#() -> c_1() activate#(X) -> c_2() activate#(n__0()) -> c_3(0#()) activate#(n__nil()) -> c_6(nil#()) activate#(n__zeros()) -> c_9(zeros#()) and#(tt(),T) -> c_10() cons#(X1,X2) -> c_11() isNat#(n__0()) -> c_12() isNatIList#(n__zeros()) -> c_17() isNatList#(n__nil()) -> c_19() length#(X) -> c_21() nil#() -> c_22() s#(X) -> c_23() take#(X1,X2) -> c_24() uTake1#(tt()) -> c_26(nil#()) zeros#() -> c_28(cons#(0(),n__zeros()),0#()) zeros#() -> c_29() - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/2,c_6/1,c_7/2,c_8/3,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/5,c_17/0,c_18/5,c_19/0,c_20/5,c_21/0,c_22/0,c_23/0,c_24/0,c_25/3,c_26/1,c_27/4,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) -->_2 activate#(n__zeros()) -> c_9(zeros#()):17 -->_2 activate#(n__nil()) -> c_6(nil#()):16 -->_2 activate#(n__0()) -> c_3(0#()):15 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_1 cons#(X1,X2) -> c_11():19 -->_2 activate#(X) -> c_2():14 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 2:S:activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) -->_2 activate#(n__zeros()) -> c_9(zeros#()):17 -->_2 activate#(n__nil()) -> c_6(nil#()):16 -->_2 activate#(n__0()) -> c_3(0#()):15 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_1 length#(X) -> c_21():23 -->_2 activate#(X) -> c_2():14 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 3:S:activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) -->_2 activate#(n__zeros()) -> c_9(zeros#()):17 -->_2 activate#(n__nil()) -> c_6(nil#()):16 -->_2 activate#(n__0()) -> c_3(0#()):15 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_1 s#(X) -> c_23():25 -->_2 activate#(X) -> c_2():14 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 4:S:activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__zeros()) -> c_9(zeros#()):17 -->_2 activate#(n__zeros()) -> c_9(zeros#()):17 -->_3 activate#(n__nil()) -> c_6(nil#()):16 -->_2 activate#(n__nil()) -> c_6(nil#()):16 -->_3 activate#(n__0()) -> c_3(0#()):15 -->_2 activate#(n__0()) -> c_3(0#()):15 -->_1 take#(X1,X2) -> c_24():26 -->_3 activate#(X) -> c_2():14 -->_2 activate#(X) -> c_2():14 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 5:S:isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) -->_2 activate#(n__zeros()) -> c_9(zeros#()):17 -->_2 activate#(n__nil()) -> c_6(nil#()):16 -->_2 activate#(n__0()) -> c_3(0#()):15 -->_1 isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):10 -->_1 isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):9 -->_1 isNatList#(n__nil()) -> c_19():22 -->_2 activate#(X) -> c_2():14 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 6:S:isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) -->_2 activate#(n__zeros()) -> c_9(zeros#()):17 -->_2 activate#(n__nil()) -> c_6(nil#()):16 -->_2 activate#(n__0()) -> c_3(0#()):15 -->_1 isNat#(n__0()) -> c_12():20 -->_2 activate#(X) -> c_2():14 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 7:S:isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) -->_2 activate#(n__zeros()) -> c_9(zeros#()):17 -->_2 activate#(n__nil()) -> c_6(nil#()):16 -->_2 activate#(n__0()) -> c_3(0#()):15 -->_1 isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):10 -->_1 isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):9 -->_1 isNatList#(n__nil()) -> c_19():22 -->_2 activate#(X) -> c_2():14 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 8:S:isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_5 activate#(n__zeros()) -> c_9(zeros#()):17 -->_3 activate#(n__zeros()) -> c_9(zeros#()):17 -->_5 activate#(n__nil()) -> c_6(nil#()):16 -->_3 activate#(n__nil()) -> c_6(nil#()):16 -->_5 activate#(n__0()) -> c_3(0#()):15 -->_3 activate#(n__0()) -> c_3(0#()):15 -->_4 isNatIList#(n__zeros()) -> c_17():21 -->_2 isNat#(n__0()) -> c_12():20 -->_1 and#(tt(),T) -> c_10():18 -->_5 activate#(X) -> c_2():14 -->_3 activate#(X) -> c_2():14 -->_4 isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):8 -->_4 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):7 -->_2 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_2 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_5 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_5 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_5 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_5 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 9:S:isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) -->_5 activate#(n__zeros()) -> c_9(zeros#()):17 -->_3 activate#(n__zeros()) -> c_9(zeros#()):17 -->_5 activate#(n__nil()) -> c_6(nil#()):16 -->_3 activate#(n__nil()) -> c_6(nil#()):16 -->_5 activate#(n__0()) -> c_3(0#()):15 -->_3 activate#(n__0()) -> c_3(0#()):15 -->_4 isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):10 -->_4 isNatList#(n__nil()) -> c_19():22 -->_2 isNat#(n__0()) -> c_12():20 -->_1 and#(tt(),T) -> c_10():18 -->_5 activate#(X) -> c_2():14 -->_3 activate#(X) -> c_2():14 -->_4 isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):9 -->_2 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_2 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_5 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_5 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_5 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_5 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 10:S:isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_5 activate#(n__zeros()) -> c_9(zeros#()):17 -->_3 activate#(n__zeros()) -> c_9(zeros#()):17 -->_5 activate#(n__nil()) -> c_6(nil#()):16 -->_3 activate#(n__nil()) -> c_6(nil#()):16 -->_5 activate#(n__0()) -> c_3(0#()):15 -->_3 activate#(n__0()) -> c_3(0#()):15 -->_4 isNatIList#(n__zeros()) -> c_17():21 -->_2 isNat#(n__0()) -> c_12():20 -->_1 and#(tt(),T) -> c_10():18 -->_5 activate#(X) -> c_2():14 -->_3 activate#(X) -> c_2():14 -->_4 isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):8 -->_4 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):7 -->_2 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_2 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_5 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_5 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_5 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_5 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 11:S:uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) -->_3 activate#(n__zeros()) -> c_9(zeros#()):17 -->_3 activate#(n__nil()) -> c_6(nil#()):16 -->_3 activate#(n__0()) -> c_3(0#()):15 -->_1 s#(X) -> c_23():25 -->_2 length#(X) -> c_21():23 -->_3 activate#(X) -> c_2():14 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 12:S:uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) -->_4 activate#(n__zeros()) -> c_9(zeros#()):17 -->_3 activate#(n__zeros()) -> c_9(zeros#()):17 -->_2 activate#(n__zeros()) -> c_9(zeros#()):17 -->_4 activate#(n__nil()) -> c_6(nil#()):16 -->_3 activate#(n__nil()) -> c_6(nil#()):16 -->_2 activate#(n__nil()) -> c_6(nil#()):16 -->_4 activate#(n__0()) -> c_3(0#()):15 -->_3 activate#(n__0()) -> c_3(0#()):15 -->_2 activate#(n__0()) -> c_3(0#()):15 -->_1 cons#(X1,X2) -> c_11():19 -->_4 activate#(X) -> c_2():14 -->_3 activate#(X) -> c_2():14 -->_2 activate#(X) -> c_2():14 -->_4 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_4 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_4 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_4 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 13:W:0#() -> c_1() 14:W:activate#(X) -> c_2() 15:W:activate#(n__0()) -> c_3(0#()) -->_1 0#() -> c_1():13 16:W:activate#(n__nil()) -> c_6(nil#()) -->_1 nil#() -> c_22():24 17:W:activate#(n__zeros()) -> c_9(zeros#()) -->_1 zeros#() -> c_28(cons#(0(),n__zeros()),0#()):28 -->_1 zeros#() -> c_29():29 18:W:and#(tt(),T) -> c_10() 19:W:cons#(X1,X2) -> c_11() 20:W:isNat#(n__0()) -> c_12() 21:W:isNatIList#(n__zeros()) -> c_17() 22:W:isNatList#(n__nil()) -> c_19() 23:W:length#(X) -> c_21() 24:W:nil#() -> c_22() 25:W:s#(X) -> c_23() 26:W:take#(X1,X2) -> c_24() 27:W:uTake1#(tt()) -> c_26(nil#()) -->_1 nil#() -> c_22():24 28:W:zeros#() -> c_28(cons#(0(),n__zeros()),0#()) -->_1 cons#(X1,X2) -> c_11():19 -->_2 0#() -> c_1():13 29:W:zeros#() -> c_29() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 27: uTake1#(tt()) -> c_26(nil#()) 22: isNatList#(n__nil()) -> c_19() 18: and#(tt(),T) -> c_10() 20: isNat#(n__0()) -> c_12() 21: isNatIList#(n__zeros()) -> c_17() 23: length#(X) -> c_21() 25: s#(X) -> c_23() 14: activate#(X) -> c_2() 26: take#(X1,X2) -> c_24() 15: activate#(n__0()) -> c_3(0#()) 16: activate#(n__nil()) -> c_6(nil#()) 24: nil#() -> c_22() 17: activate#(n__zeros()) -> c_9(zeros#()) 29: zeros#() -> c_29() 28: zeros#() -> c_28(cons#(0(),n__zeros()),0#()) 13: 0#() -> c_1() 19: cons#(X1,X2) -> c_11() * Step 8: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/2,c_5/2,c_6/1,c_7/2,c_8/3,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/5,c_17/0,c_18/5,c_19/0,c_20/5,c_21/0,c_22/0,c_23/0,c_24/0,c_25/3,c_26/1,c_27/4,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)) -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 2:S:activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)) -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 3:S:activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)) -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 4:S:activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)) -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 5:S:isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) -->_1 isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):10 -->_1 isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):9 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 6:S:isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 7:S:isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) -->_1 isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):10 -->_1 isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):9 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 8:S:isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_4 isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):8 -->_4 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):7 -->_2 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_2 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_5 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_5 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_5 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_5 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 9:S:isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)) -->_4 isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):10 -->_4 isNatList#(n__cons(N,L)) -> c_18(and#(isNat(activate(N)),isNatList(activate(L))) ,isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):9 -->_2 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_2 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_5 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_5 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_5 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_5 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 10:S:isNatList#(n__take(N,IL)) -> c_20(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_4 isNatIList#(n__cons(N,IL)) -> c_16(and#(isNat(activate(N)),isNatIList(activate(IL))) ,isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):8 -->_4 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):7 -->_2 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_2 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_5 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_5 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_5 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_5 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 11:S:uLength#(tt(),L) -> c_25(s#(length(activate(L))),length#(activate(L)),activate#(L)) -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 12:S:uTake2#(tt(),M,N,IL) -> c_27(cons#(activate(N),n__take(activate(M),activate(IL))) ,activate#(N) ,activate#(M) ,activate#(IL)) -->_4 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_3 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_8(take#(activate(X1),activate(X2)),activate#(X1),activate#(X2)):4 -->_4 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_3 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_2 activate#(n__s(X)) -> c_7(s#(activate(X)),activate#(X)):3 -->_4 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_3 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(length#(activate(X)),activate#(X)):2 -->_4 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_3 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(cons#(activate(X1),X2),activate#(X1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) uLength#(tt(),L) -> c_25(activate#(L)) uTake2#(tt(),M,N,IL) -> c_27(activate#(N),activate#(M),activate#(IL)) * Step 9: UsableRules MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) uLength#(tt(),L) -> c_25(activate#(L)) uTake2#(tt(),M,N,IL) -> c_27(activate#(N),activate#(M),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() and(tt(),T) -> T cons(X1,X2) -> n__cons(X1,X2) isNat(n__0()) -> tt() isNat(n__length(L)) -> isNatList(activate(L)) isNat(n__s(N)) -> isNat(activate(N)) isNatIList(IL) -> isNatList(activate(IL)) isNatIList(n__cons(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) isNatIList(n__zeros()) -> tt() isNatList(n__cons(N,L)) -> and(isNat(activate(N)),isNatList(activate(L))) isNatList(n__nil()) -> tt() isNatList(n__take(N,IL)) -> and(isNat(activate(N)),isNatIList(activate(IL))) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,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__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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() activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) uLength#(tt(),L) -> c_25(activate#(L)) uTake2#(tt(),M,N,IL) -> c_27(activate#(N),activate#(M),activate#(IL)) * Step 10: RemoveHeads MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) uLength#(tt(),L) -> c_25(activate#(L)) uTake2#(tt(),M,N,IL) -> c_27(activate#(N),activate#(M),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 2:S:activate#(n__length(X)) -> c_5(activate#(X)) -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 3:S:activate#(n__s(X)) -> c_7(activate#(X)) -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 4:S:activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 5:S:isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) -->_1 isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):10 -->_1 isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):9 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 6:S:isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 7:S:isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) -->_1 isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):10 -->_1 isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):9 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 8:S:isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_3 isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):8 -->_3 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):7 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_4 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_4 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_4 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_4 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 9:S:isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) -->_3 isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):10 -->_3 isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):9 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_4 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_4 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_4 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_4 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 10:S:isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_3 isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):8 -->_3 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):7 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):6 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):5 -->_4 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_4 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_4 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_4 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 11:S:uLength#(tt(),L) -> c_25(activate#(L)) -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 12:S:uTake2#(tt(),M,N,IL) -> c_27(activate#(N),activate#(M),activate#(IL)) -->_3 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):4 -->_3 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):3 -->_3 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):2 -->_3 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):1 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). [(11,uLength#(tt(),L) -> c_25(activate#(L))) ,(12,uTake2#(tt(),M,N,IL) -> c_27(activate#(N),activate#(M),activate#(IL)))] * Step 11: Decompose MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) - Weak DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0 ,s#/1,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1 ,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0 ,c_13/2,c_14/2,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3 ,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil ,n__s,n__take,n__zeros,tt} Problem (S) - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) - Weak DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0 ,s#/1,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1 ,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0 ,c_13/2,c_14/2,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3 ,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil ,n__s,n__take,n__zeros,tt} ** Step 11.a:1: PredecessorEstimationCP MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) - Weak DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 4: activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) The strictly oriented rules are moved into the weak component. *** Step 11.a:1.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) - Weak DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1,2}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2,3,4}, uargs(c_18) = {1,2,3,4}, uargs(c_20) = {1,2,3,4} Following symbols are considered usable: {0,activate,cons,length,nil,s,take,zeros,0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList#,length# ,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} TcT has computed the following interpretation: p(0) = [0] [0] p(activate) = [1 0] x1 + [0] [0 1] [0] p(and) = [0 0] x1 + [0] [0 1] [1] p(cons) = [1 1] x1 + [1 1] x2 + [0] [0 1] [0 1] [0] p(isNat) = [2 1] x1 + [0] [0 0] [0] p(isNatIList) = [0] [0] p(isNatList) = [0 0] x1 + [2] [2 2] [0] p(length) = [1 3] x1 + [2] [0 1] [1] p(n__0) = [0] [0] p(n__cons) = [1 1] x1 + [1 1] x2 + [0] [0 1] [0 1] [0] p(n__length) = [1 3] x1 + [2] [0 1] [1] p(n__nil) = [2] [1] p(n__s) = [1 3] x1 + [3] [0 1] [0] p(n__take) = [1 1] x1 + [1 2] x2 + [2] [0 1] [0 1] [1] p(n__zeros) = [3] [0] p(nil) = [2] [1] p(s) = [1 3] x1 + [3] [0 1] [0] p(take) = [1 1] x1 + [1 2] x2 + [2] [0 1] [0 1] [1] p(tt) = [0] [1] p(uLength) = [0 0] x2 + [0] [2 1] [0] p(uTake1) = [0] [0] p(uTake2) = [0 1] x1 + [0 0] x2 + [0 0] x3 + [0] [0 0] [1 2] [0 1] [0] p(zeros) = [3] [0] p(0#) = [0] [2] p(activate#) = [0 1] x1 + [0] [0 2] [0] p(and#) = [0] [0] p(cons#) = [2 0] x1 + [2] [1 0] [0] p(isNat#) = [1 0] x1 + [0] [0 1] [1] p(isNatIList#) = [1 1] x1 + [2] [0 1] [0] p(isNatList#) = [1 0] x1 + [0] [0 1] [1] p(length#) = [2 0] x1 + [0] [0 0] [2] p(nil#) = [2] [2] p(s#) = [0 0] x1 + [1] [2 0] [0] p(take#) = [0 0] x1 + [2 1] x2 + [0] [0 1] [0 0] [0] p(uLength#) = [0 1] x2 + [0] [0 0] [0] p(uTake1#) = [0] [0] p(uTake2#) = [2 0] x1 + [0 2] x3 + [2 2] x4 + [2] [0 0] [2 1] [0 2] [0] p(zeros#) = [0] [2] p(c_1) = [0] [2] p(c_2) = [2] [0] p(c_3) = [0 0] x1 + [0] [0 1] [0] p(c_4) = [1 0] x1 + [0] [2 0] [0] p(c_5) = [1 0] x1 + [1] [2 0] [2] p(c_6) = [2 1] x1 + [0] [0 2] [2] p(c_7) = [1 0] x1 + [0] [2 0] [0] p(c_8) = [1 0] x1 + [1 0] x2 + [0] [1 0] [0 1] [2] p(c_9) = [2] [2] p(c_10) = [2] [0] p(c_11) = [0] [0] p(c_12) = [0] [0] p(c_13) = [1 0] x1 + [1 1] x2 + [1] [0 1] [0 0] [1] p(c_14) = [1 2] x1 + [1 0] x2 + [1] [0 1] [0 0] [0] p(c_15) = [1 0] x1 + [1 0] x2 + [1] [0 0] [1 0] [0] p(c_16) = [1 0] x1 + [2 0] x2 + [1 0] x3 + [1 0] x4 + [0] [0 0] [0 0] [0 0] [0 0] [0] p(c_17) = [0] [0] p(c_18) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [0] [0 0] [1 0] [0 0] [1 0] [0] p(c_19) = [0] [0] p(c_20) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [1 0] x4 + [0] [0 0] [0 0] [0 0] [0 0] [2] p(c_21) = [0] [1] p(c_22) = [0] [0] p(c_23) = [0] [1] p(c_24) = [1] [1] p(c_25) = [0] [2] p(c_26) = [1] [2] p(c_27) = [0 0] x1 + [0 2] x3 + [0] [2 2] [0 0] [0] p(c_28) = [0] [2] p(c_29) = [1] [0] Following rules are strictly oriented: activate#(n__take(X1,X2)) = [0 1] X1 + [0 1] X2 + [1] [0 2] [0 2] [2] > [0 1] X1 + [0 1] X2 + [0] [0 1] [0 2] [2] = c_8(activate#(X1),activate#(X2)) Following rules are (at-least) weakly oriented: activate#(n__cons(X1,X2)) = [0 1] X1 + [0 1] X2 + [0] [0 2] [0 2] [0] >= [0 1] X1 + [0] [0 2] [0] = c_4(activate#(X1)) activate#(n__length(X)) = [0 1] X + [1] [0 2] [2] >= [0 1] X + [1] [0 2] [2] = c_5(activate#(X)) activate#(n__s(X)) = [0 1] X + [0] [0 2] [0] >= [0 1] X + [0] [0 2] [0] = c_7(activate#(X)) isNat#(n__length(L)) = [1 3] L + [2] [0 1] [2] >= [1 3] L + [1] [0 1] [2] = c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) = [1 3] N + [3] [0 1] [1] >= [1 3] N + [3] [0 1] [1] = c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) = [1 1] IL + [2] [0 1] [0] >= [1 1] IL + [1] [0 1] [0] = c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) = [1 2] IL + [1 2] N + [2] [0 1] [0 1] [0] >= [1 2] IL + [1 2] N + [2] [0 0] [0 0] [0] = c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) = [1 1] L + [1 1] N + [0] [0 1] [0 1] [1] >= [1 1] L + [1 1] N + [0] [0 1] [0 1] [0] = c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) = [1 2] IL + [1 1] N + [2] [0 1] [0 1] [2] >= [1 2] IL + [1 1] N + [2] [0 0] [0 0] [2] = c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) 0() = [0] [0] >= [0] [0] = n__0() activate(X) = [1 0] X + [0] [0 1] [0] >= [1 0] X + [0] [0 1] [0] = X activate(n__0()) = [0] [0] >= [0] [0] = 0() activate(n__cons(X1,X2)) = [1 1] X1 + [1 1] X2 + [0] [0 1] [0 1] [0] >= [1 1] X1 + [1 1] X2 + [0] [0 1] [0 1] [0] = cons(activate(X1),X2) activate(n__length(X)) = [1 3] X + [2] [0 1] [1] >= [1 3] X + [2] [0 1] [1] = length(activate(X)) activate(n__nil()) = [2] [1] >= [2] [1] = nil() activate(n__s(X)) = [1 3] X + [3] [0 1] [0] >= [1 3] X + [3] [0 1] [0] = s(activate(X)) activate(n__take(X1,X2)) = [1 1] X1 + [1 2] X2 + [2] [0 1] [0 1] [1] >= [1 1] X1 + [1 2] X2 + [2] [0 1] [0 1] [1] = take(activate(X1),activate(X2)) activate(n__zeros()) = [3] [0] >= [3] [0] = zeros() cons(X1,X2) = [1 1] X1 + [1 1] X2 + [0] [0 1] [0 1] [0] >= [1 1] X1 + [1 1] X2 + [0] [0 1] [0 1] [0] = n__cons(X1,X2) length(X) = [1 3] X + [2] [0 1] [1] >= [1 3] X + [2] [0 1] [1] = n__length(X) nil() = [2] [1] >= [2] [1] = n__nil() s(X) = [1 3] X + [3] [0 1] [0] >= [1 3] X + [3] [0 1] [0] = n__s(X) take(X1,X2) = [1 1] X1 + [1 2] X2 + [2] [0 1] [0 1] [1] >= [1 1] X1 + [1 2] X2 + [2] [0 1] [0 1] [1] = n__take(X1,X2) zeros() = [3] [0] >= [3] [0] = cons(0(),n__zeros()) zeros() = [3] [0] >= [3] [0] = n__zeros() *** Step 11.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) - Weak DPs: activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 11.a:1.b:1: PredecessorEstimationCP MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) - Weak DPs: activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 3: activate#(n__s(X)) -> c_7(activate#(X)) The strictly oriented rules are moved into the weak component. **** Step 11.a:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) - Weak DPs: activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1,2}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2,3,4}, uargs(c_18) = {1,2,3,4}, uargs(c_20) = {1,2,3,4} Following symbols are considered usable: {0,activate,cons,length,nil,s,take,zeros,0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList#,length# ,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(activate) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(and) = [0] [0] [0] p(cons) = [1 1 1] [1 1 1] [0] [0 0 1] x1 + [0 0 1] x2 + [0] [0 0 1] [0 0 0] [0] p(isNat) = [0] [0] [0] p(isNatIList) = [0] [0] [0] p(isNatList) = [0] [0] [0] p(length) = [1 1 1] [1] [0 0 0] x1 + [1] [0 0 1] [0] p(n__0) = [0] [0] [0] p(n__cons) = [1 1 1] [1 1 1] [0] [0 0 1] x1 + [0 0 1] x2 + [0] [0 0 1] [0 0 0] [0] p(n__length) = [1 1 1] [1] [0 0 0] x1 + [1] [0 0 1] [0] p(n__nil) = [0] [1] [1] p(n__s) = [1 1 1] [0] [0 0 1] x1 + [1] [0 0 1] [1] p(n__take) = [1 1 1] [1 1 1] [0] [0 0 1] x1 + [0 0 1] x2 + [0] [0 0 1] [0 0 1] [1] p(n__zeros) = [0] [0] [0] p(nil) = [0] [1] [1] p(s) = [1 1 1] [0] [0 0 1] x1 + [1] [0 0 1] [1] p(take) = [1 1 1] [1 1 1] [0] [0 0 1] x1 + [0 0 1] x2 + [0] [0 0 1] [0 0 1] [1] p(tt) = [0] [0] [0] p(uLength) = [0] [0] [0] p(uTake1) = [0] [0] [0] p(uTake2) = [0] [0] [0] p(zeros) = [0] [0] [0] p(0#) = [0] [0] [0] p(activate#) = [0 0 1] [0] [0 0 1] x1 + [0] [0 0 1] [1] p(and#) = [0] [0] [0] p(cons#) = [0] [0] [0] p(isNat#) = [1 0 0] [0] [1 1 0] x1 + [1] [0 1 1] [0] p(isNatIList#) = [1 1 1] [1] [1 0 1] x1 + [0] [1 1 0] [1] p(isNatList#) = [1 1 0] [1] [1 0 0] x1 + [0] [1 1 0] [1] p(length#) = [0] [0] [0] p(nil#) = [0] [0] [0] p(s#) = [0] [0] [0] p(take#) = [0] [0] [0] p(uLength#) = [0] [0] [0] p(uTake1#) = [0] [0] [0] p(uTake2#) = [0] [0] [0] p(zeros#) = [0] [0] [0] p(c_1) = [0] [0] [0] p(c_2) = [0] [0] [0] p(c_3) = [0] [0] [0] p(c_4) = [1 0 0] [0] [0 0 0] x1 + [0] [0 0 0] [1] p(c_5) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 0] [0] p(c_6) = [0] [0] [0] p(c_7) = [1 0 0] [0] [0 0 0] x1 + [1] [0 0 1] [1] p(c_8) = [1 0 0] [1 0 0] [0] [0 0 1] x1 + [0 0 0] x2 + [0] [0 1 0] [0 1 0] [0] p(c_9) = [0] [0] [0] p(c_10) = [0] [0] [0] p(c_11) = [0] [0] [0] p(c_12) = [0] [0] [0] p(c_13) = [1 0 0] [1 0 0] [0] [1 0 0] x1 + [0 0 0] x2 + [1] [0 0 0] [0 1 0] [0] p(c_14) = [1 0 0] [1 0 0] [0] [0 1 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 0 1] [0] p(c_15) = [1 0 0] [1 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0] [0 0 0] [0 0 0] [1] p(c_16) = [1 0 0] [1 0 0] [1 0 0] [1 0 0] [0] [1 0 1] x1 + [0 0 0] x2 + [0 0 0] x3 + [0 0 0] x4 + [0] [0 0 1] [0 1 0] [0 1 0] [0 0 0] [0] p(c_17) = [0] [0] [0] p(c_18) = [1 0 0] [1 1 0] [1 0 0] [1 1 0] [0] [1 0 0] x1 + [1 0 0] x2 + [0 1 0] x3 + [0 0 0] x4 + [0] [0 0 1] [1 0 0] [1 0 0] [1 1 0] [0] p(c_19) = [0] [0] [0] p(c_20) = [1 0 1] [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 1 0] x2 + [0 1 0] x3 + [0 0 0] x4 + [0] [0 0 1] [1 0 0] [1 0 0] [0 0 0] [0] p(c_21) = [0] [0] [0] p(c_22) = [0] [0] [0] p(c_23) = [0] [0] [0] p(c_24) = [0] [0] [0] p(c_25) = [0] [0] [0] p(c_26) = [0] [0] [0] p(c_27) = [0] [0] [0] p(c_28) = [0] [0] [0] p(c_29) = [0] [0] [0] Following rules are strictly oriented: activate#(n__s(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 1] [2] > [0 0 1] [0] [0 0 0] X + [1] [0 0 1] [2] = c_7(activate#(X)) Following rules are (at-least) weakly oriented: activate#(n__cons(X1,X2)) = [0 0 1] [0] [0 0 1] X1 + [0] [0 0 1] [1] >= [0 0 1] [0] [0 0 0] X1 + [0] [0 0 0] [1] = c_4(activate#(X1)) activate#(n__length(X)) = [0 0 1] [0] [0 0 1] X + [0] [0 0 1] [1] >= [0 0 1] [0] [0 0 1] X + [0] [0 0 0] [0] = c_5(activate#(X)) activate#(n__take(X1,X2)) = [0 0 1] [0 0 1] [1] [0 0 1] X1 + [0 0 1] X2 + [1] [0 0 1] [0 0 1] [2] >= [0 0 1] [0 0 1] [0] [0 0 1] X1 + [0 0 0] X2 + [1] [0 0 1] [0 0 1] [0] = c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) = [1 1 1] [1] [1 1 1] L + [3] [0 0 1] [1] >= [1 1 1] [1] [1 1 0] L + [2] [0 0 1] [0] = c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) = [1 1 1] [0] [1 1 2] N + [2] [0 0 2] [2] >= [1 0 1] [0] [1 1 0] N + [1] [0 0 1] [1] = c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) = [1 1 1] [1] [1 0 1] IL + [0] [1 1 0] [1] >= [1 1 1] [1] [1 0 1] IL + [0] [0 0 0] [1] = c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) = [1 1 2] [1 1 3] [1] [1 1 1] IL + [1 1 2] N + [0] [1 1 2] [1 1 2] [1] >= [1 1 2] [1 0 1] [1] [0 0 0] IL + [1 1 1] N + [0] [1 0 1] [0 1 2] [0] = c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) = [1 1 2] [1 1 2] [1] [1 1 1] L + [1 1 1] N + [0] [1 1 2] [1 1 2] [1] >= [1 1 2] [1 0 2] [1] [1 0 0] L + [1 0 1] N + [0] [1 1 2] [0 1 2] [1] = c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) = [1 1 2] [1 1 2] [1] [1 1 1] IL + [1 1 1] N + [0] [1 1 2] [1 1 2] [1] >= [1 1 2] [1 1 2] [1] [1 0 1] IL + [0 0 1] N + [0] [1 1 1] [0 1 2] [1] = c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) 0() = [0] [0] [0] >= [0] [0] [0] = n__0() activate(X) = [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] = X activate(n__0()) = [0] [0] [0] >= [0] [0] [0] = 0() activate(n__cons(X1,X2)) = [1 1 1] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 0] [0] >= [1 1 1] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 0] [0] = cons(activate(X1),X2) activate(n__length(X)) = [1 1 1] [1] [0 0 0] X + [1] [0 0 1] [0] >= [1 1 1] [1] [0 0 0] X + [1] [0 0 1] [0] = length(activate(X)) activate(n__nil()) = [0] [1] [1] >= [0] [1] [1] = nil() activate(n__s(X)) = [1 1 1] [0] [0 0 1] X + [1] [0 0 1] [1] >= [1 1 1] [0] [0 0 1] X + [1] [0 0 1] [1] = s(activate(X)) activate(n__take(X1,X2)) = [1 1 1] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 1] [1] >= [1 1 1] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 1] [1] = take(activate(X1),activate(X2)) activate(n__zeros()) = [0] [0] [0] >= [0] [0] [0] = zeros() cons(X1,X2) = [1 1 1] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 0] [0] >= [1 1 1] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 0] [0] = n__cons(X1,X2) length(X) = [1 1 1] [1] [0 0 0] X + [1] [0 0 1] [0] >= [1 1 1] [1] [0 0 0] X + [1] [0 0 1] [0] = n__length(X) nil() = [0] [1] [1] >= [0] [1] [1] = n__nil() s(X) = [1 1 1] [0] [0 0 1] X + [1] [0 0 1] [1] >= [1 1 1] [0] [0 0 1] X + [1] [0 0 1] [1] = n__s(X) take(X1,X2) = [1 1 1] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 1] [1] >= [1 1 1] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 1] [1] = n__take(X1,X2) zeros() = [0] [0] [0] >= [0] [0] [0] = cons(0(),n__zeros()) zeros() = [0] [0] [0] >= [0] [0] [0] = n__zeros() **** Step 11.a:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) - Weak DPs: activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 11.a:1.b:1.b:1: PredecessorEstimationCP MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) - Weak DPs: activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: activate#(n__length(X)) -> c_5(activate#(X)) The strictly oriented rules are moved into the weak component. ***** Step 11.a:1.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) - Weak DPs: activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1}, uargs(c_7) = {1}, uargs(c_8) = {1,2}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2,3,4}, uargs(c_18) = {1,2,3,4}, uargs(c_20) = {1,2,3,4} Following symbols are considered usable: {0,activate,cons,length,nil,s,take,zeros,0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList#,length# ,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} TcT has computed the following interpretation: p(0) = [0] [0] [0] p(activate) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(and) = [0] [0] [0] p(cons) = [1 1 0] [1 1 1] [0] [0 0 1] x1 + [0 0 1] x2 + [0] [0 0 1] [0 0 0] [0] p(isNat) = [0] [0] [0] p(isNatIList) = [0] [0] [0] p(isNatList) = [0] [0] [0] p(length) = [1 1 0] [0] [0 0 1] x1 + [1] [0 0 1] [1] p(n__0) = [0] [0] [0] p(n__cons) = [1 1 0] [1 1 1] [0] [0 0 1] x1 + [0 0 1] x2 + [0] [0 0 1] [0 0 0] [0] p(n__length) = [1 1 0] [0] [0 0 1] x1 + [1] [0 0 1] [1] p(n__nil) = [0] [0] [0] p(n__s) = [1 1 1] [1] [0 0 1] x1 + [1] [0 0 1] [1] p(n__take) = [1 1 1] [1 1 1] [1] [0 0 0] x1 + [0 0 1] x2 + [1] [0 0 1] [0 0 1] [1] p(n__zeros) = [0] [0] [0] p(nil) = [0] [0] [0] p(s) = [1 1 1] [1] [0 0 1] x1 + [1] [0 0 1] [1] p(take) = [1 1 1] [1 1 1] [1] [0 0 0] x1 + [0 0 1] x2 + [1] [0 0 1] [0 0 1] [1] p(tt) = [0] [0] [0] p(uLength) = [0] [0] [0] p(uTake1) = [0] [0] [0] p(uTake2) = [0] [0] [0] p(zeros) = [0] [0] [0] p(0#) = [0] [0] [0] p(activate#) = [0 0 1] [0] [0 0 0] x1 + [1] [0 0 0] [1] p(and#) = [0] [0] [0] p(cons#) = [0] [0] [0] p(isNat#) = [1 1 0] [0] [1 1 1] x1 + [0] [0 1 0] [1] p(isNatIList#) = [1 1 1] [0] [0 1 1] x1 + [0] [1 0 0] [1] p(isNatList#) = [1 1 0] [0] [0 0 0] x1 + [1] [1 1 0] [1] p(length#) = [0] [0] [0] p(nil#) = [0] [0] [0] p(s#) = [0] [0] [0] p(take#) = [0] [0] [0] p(uLength#) = [0] [0] [0] p(uTake1#) = [0] [0] [0] p(uTake2#) = [0] [0] [0] p(zeros#) = [0] [0] [0] p(c_1) = [0] [0] [0] p(c_2) = [0] [0] [0] p(c_3) = [0] [0] [0] p(c_4) = [1 0 0] [0] [0 0 0] x1 + [0] [0 0 0] [0] p(c_5) = [1 0 0] [0] [0 0 0] x1 + [1] [0 1 0] [0] p(c_6) = [0] [0] [0] p(c_7) = [1 1 0] [0] [0 1 0] x1 + [0] [0 0 0] [1] p(c_8) = [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [0 1 0] [0] p(c_9) = [0] [0] [0] p(c_10) = [0] [0] [0] p(c_11) = [0] [0] [0] p(c_12) = [0] [0] [0] p(c_13) = [1 0 0] [1 0 0] [0] [0 0 1] x1 + [1 0 0] x2 + [1] [0 0 0] [0 0 0] [1] p(c_14) = [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 0 0] x2 + [0] [0 0 0] [1 0 1] [1] p(c_15) = [1 0 0] [1 0 0] [0] [0 0 0] x1 + [1 0 0] x2 + [0] [0 1 0] [0 0 0] [0] p(c_16) = [1 0 0] [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0] [0 0 0] [0 1 0] [0 1 0] [0 0 0] [0] p(c_17) = [0] [0] [0] p(c_18) = [1 0 0] [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [0 0 0] x4 + [0] [0 0 0] [1 0 1] [0 0 0] [1 0 0] [0] p(c_19) = [0] [0] [0] p(c_20) = [1 0 0] [1 1 0] [1 0 0] [1 0 0] [1] [0 0 0] x1 + [0 0 1] x2 + [0 0 0] x3 + [0 0 0] x4 + [0] [0 0 0] [0 0 0] [0 1 0] [0 0 0] [1] p(c_21) = [0] [0] [0] p(c_22) = [0] [0] [0] p(c_23) = [0] [0] [0] p(c_24) = [0] [0] [0] p(c_25) = [0] [0] [0] p(c_26) = [0] [0] [0] p(c_27) = [0] [0] [0] p(c_28) = [0] [0] [0] p(c_29) = [0] [0] [0] Following rules are strictly oriented: activate#(n__length(X)) = [0 0 1] [1] [0 0 0] X + [1] [0 0 0] [1] > [0 0 1] [0] [0 0 0] X + [1] [0 0 0] [1] = c_5(activate#(X)) Following rules are (at-least) weakly oriented: activate#(n__cons(X1,X2)) = [0 0 1] [0] [0 0 0] X1 + [1] [0 0 0] [1] >= [0 0 1] [0] [0 0 0] X1 + [0] [0 0 0] [0] = c_4(activate#(X1)) activate#(n__s(X)) = [0 0 1] [1] [0 0 0] X + [1] [0 0 0] [1] >= [0 0 1] [1] [0 0 0] X + [1] [0 0 0] [1] = c_7(activate#(X)) activate#(n__take(X1,X2)) = [0 0 1] [0 0 1] [1] [0 0 0] X1 + [0 0 0] X2 + [1] [0 0 0] [0 0 0] [1] >= [0 0 1] [0 0 1] [0] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 0] [0 0 0] [1] = c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) = [1 1 1] [1] [1 1 2] L + [2] [0 0 1] [2] >= [1 1 1] [0] [1 1 1] L + [2] [0 0 0] [1] = c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) = [1 1 2] [2] [1 1 3] N + [3] [0 0 1] [2] >= [1 1 1] [0] [0 0 0] N + [0] [0 0 1] [2] = c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) = [1 1 1] [0] [0 1 1] IL + [0] [1 0 0] [1] >= [1 1 1] [0] [0 0 1] IL + [0] [0 0 0] [1] = c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) = [1 1 2] [1 1 2] [0] [0 0 1] IL + [0 0 2] N + [0] [1 1 1] [1 1 0] [1] >= [1 1 2] [1 1 1] [0] [0 0 1] IL + [0 0 1] N + [0] [0 1 1] [0 0 0] [1] = c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) = [1 1 2] [1 1 1] [0] [0 0 0] L + [0 0 0] N + [1] [1 1 2] [1 1 1] [1] >= [1 1 1] [1 1 1] [0] [0 0 0] L + [0 0 0] N + [0] [0 0 1] [0 0 1] [1] = c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) = [1 1 2] [1 1 1] [2] [0 0 0] IL + [0 0 0] N + [1] [1 1 2] [1 1 1] [3] >= [1 1 2] [1 1 1] [2] [0 0 0] IL + [0 0 0] N + [1] [0 1 1] [0 0 0] [1] = c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) 0() = [0] [0] [0] >= [0] [0] [0] = n__0() activate(X) = [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] = X activate(n__0()) = [0] [0] [0] >= [0] [0] [0] = 0() activate(n__cons(X1,X2)) = [1 1 0] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 0] [0] >= [1 1 0] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 0] [0] = cons(activate(X1),X2) activate(n__length(X)) = [1 1 0] [0] [0 0 1] X + [1] [0 0 1] [1] >= [1 1 0] [0] [0 0 1] X + [1] [0 0 1] [1] = length(activate(X)) activate(n__nil()) = [0] [0] [0] >= [0] [0] [0] = nil() activate(n__s(X)) = [1 1 1] [1] [0 0 1] X + [1] [0 0 1] [1] >= [1 1 1] [1] [0 0 1] X + [1] [0 0 1] [1] = s(activate(X)) activate(n__take(X1,X2)) = [1 1 1] [1 1 1] [1] [0 0 0] X1 + [0 0 1] X2 + [1] [0 0 1] [0 0 1] [1] >= [1 1 1] [1 1 1] [1] [0 0 0] X1 + [0 0 1] X2 + [1] [0 0 1] [0 0 1] [1] = take(activate(X1),activate(X2)) activate(n__zeros()) = [0] [0] [0] >= [0] [0] [0] = zeros() cons(X1,X2) = [1 1 0] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 0] [0] >= [1 1 0] [1 1 1] [0] [0 0 1] X1 + [0 0 1] X2 + [0] [0 0 1] [0 0 0] [0] = n__cons(X1,X2) length(X) = [1 1 0] [0] [0 0 1] X + [1] [0 0 1] [1] >= [1 1 0] [0] [0 0 1] X + [1] [0 0 1] [1] = n__length(X) nil() = [0] [0] [0] >= [0] [0] [0] = n__nil() s(X) = [1 1 1] [1] [0 0 1] X + [1] [0 0 1] [1] >= [1 1 1] [1] [0 0 1] X + [1] [0 0 1] [1] = n__s(X) take(X1,X2) = [1 1 1] [1 1 1] [1] [0 0 0] X1 + [0 0 1] X2 + [1] [0 0 1] [0 0 1] [1] >= [1 1 1] [1 1 1] [1] [0 0 0] X1 + [0 0 1] X2 + [1] [0 0 1] [0 0 1] [1] = n__take(X1,X2) zeros() = [0] [0] [0] >= [0] [0] [0] = cons(0(),n__zeros()) zeros() = [0] [0] [0] >= [0] [0] [0] = n__zeros() ***** Step 11.a:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) - Weak DPs: activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 11.a:1.b:1.b:1.b:1: Failure MAYBE + Considered Problem: - Strict DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) - Weak DPs: activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: EmptyProcessor + Details: The problem is still open. ** Step 11.b:1: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak DPs: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) activate#(n__length(X)) -> c_5(activate#(X)) activate#(n__s(X)) -> c_7(activate#(X)) activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_1 isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):6 -->_1 isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):5 2:S:isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):2 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):1 3:S:isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_1 isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):6 -->_1 isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):5 4:S:isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_4 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_4 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_4 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_4 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_3 isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):4 -->_3 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):3 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):2 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):1 5:S:isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) -->_4 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_4 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_4 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_4 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_3 isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):6 -->_3 isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):5 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):2 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):1 6:S:isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_4 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_4 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_4 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_4 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_3 isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):4 -->_3 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):3 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):2 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):1 7:W:activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 8:W:activate#(n__length(X)) -> c_5(activate#(X)) -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 9:W:activate#(n__s(X)) -> c_7(activate#(X)) -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 10:W:activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) -->_2 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_1 activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)):10 -->_2 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_1 activate#(n__s(X)) -> c_7(activate#(X)):9 -->_2 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_1 activate#(n__length(X)) -> c_5(activate#(X)):8 -->_2 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 -->_1 activate#(n__cons(X1,X2)) -> c_4(activate#(X1)):7 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: activate#(n__take(X1,X2)) -> c_8(activate#(X1),activate#(X2)) 9: activate#(n__s(X)) -> c_7(activate#(X)) 8: activate#(n__length(X)) -> c_5(activate#(X)) 7: activate#(n__cons(X1,X2)) -> c_4(activate#(X1)) ** Step 11.b:2: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),activate#(N),isNatIList#(activate(IL)),activate#(IL)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/2,c_14/2 ,c_15/2,c_16/4,c_17/0,c_18/4,c_19/0,c_20/4,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)) -->_1 isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):6 -->_1 isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):5 2:S:isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)) -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):2 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):1 3:S:isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)) -->_1 isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):6 -->_1 isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):5 4:S:isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_3 isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):4 -->_3 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):3 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):2 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):1 5:S:isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),activate#(N),isNatList#(activate(L)),activate#(L)) -->_3 isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):6 -->_3 isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)) ,activate#(N) ,isNatList#(activate(L)) ,activate#(L)):5 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):2 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):1 6:S:isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)) -->_3 isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)) ,activate#(N) ,isNatIList#(activate(IL)) ,activate#(IL)):4 -->_3 isNatIList#(IL) -> c_15(isNatList#(activate(IL)),activate#(IL)):3 -->_1 isNat#(n__s(N)) -> c_14(isNat#(activate(N)),activate#(N)):2 -->_1 isNat#(n__length(L)) -> c_13(isNatList#(activate(L)),activate#(L)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNat#(n__s(N)) -> c_14(isNat#(activate(N))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) ** Step 11.b:3: PredecessorEstimationCP MAYBE + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNat#(n__s(N)) -> c_14(isNat#(activate(N))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: isNat#(n__s(N)) -> c_14(isNat#(activate(N))) The strictly oriented rules are moved into the weak component. *** Step 11.b:3.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNat#(n__s(N)) -> c_14(isNat#(activate(N))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1,2}, uargs(c_18) = {1,2}, uargs(c_20) = {1,2} Following symbols are considered usable: {0,activate,cons,length,nil,s,take,zeros,0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList#,length# ,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [2] x2 + [1] p(cons) = [1] x1 + [1] x2 + [0] p(isNat) = [1] x1 + [0] p(isNatIList) = [1] x1 + [1] p(isNatList) = [2] x1 + [1] p(length) = [1] x1 + [2] p(n__0) = [0] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__length) = [1] x1 + [2] p(n__nil) = [8] p(n__s) = [1] x1 + [5] p(n__take) = [1] x1 + [1] x2 + [0] p(n__zeros) = [0] p(nil) = [8] p(s) = [1] x1 + [5] p(take) = [1] x1 + [1] x2 + [0] p(tt) = [1] p(uLength) = [1] x1 + [1] x2 + [1] p(uTake1) = [2] p(uTake2) = [4] x1 + [1] p(zeros) = [0] p(0#) = [1] p(activate#) = [2] p(and#) = [1] x2 + [1] p(cons#) = [0] p(isNat#) = [4] x1 + [0] p(isNatIList#) = [4] x1 + [0] p(isNatList#) = [4] x1 + [0] p(length#) = [1] p(nil#) = [0] p(s#) = [1] p(take#) = [1] x1 + [1] p(uLength#) = [2] x1 + [1] p(uTake1#) = [1] x1 + [1] p(uTake2#) = [1] x4 + [8] p(zeros#) = [0] p(c_1) = [1] p(c_2) = [4] p(c_3) = [0] p(c_4) = [1] p(c_5) = [1] p(c_6) = [1] x1 + [1] p(c_7) = [1] p(c_8) = [0] p(c_9) = [4] x1 + [0] p(c_10) = [1] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [8] p(c_14) = [1] x1 + [7] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [0] p(c_18) = [1] x1 + [1] x2 + [0] p(c_19) = [1] p(c_20) = [1] x1 + [1] x2 + [0] p(c_21) = [0] p(c_22) = [1] p(c_23) = [8] p(c_24) = [8] p(c_25) = [4] x1 + [0] p(c_26) = [0] p(c_27) = [1] x1 + [2] x2 + [1] x3 + [0] p(c_28) = [8] x1 + [8] x2 + [0] p(c_29) = [2] Following rules are strictly oriented: isNat#(n__s(N)) = [4] N + [20] > [4] N + [7] = c_14(isNat#(activate(N))) Following rules are (at-least) weakly oriented: isNat#(n__length(L)) = [4] L + [8] >= [4] L + [8] = c_13(isNatList#(activate(L))) isNatIList#(IL) = [4] IL + [0] >= [4] IL + [0] = c_15(isNatList#(activate(IL))) isNatIList#(n__cons(N,IL)) = [4] IL + [4] N + [0] >= [4] IL + [4] N + [0] = c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) = [4] L + [4] N + [0] >= [4] L + [4] N + [0] = c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) = [4] IL + [4] N + [0] >= [4] IL + [4] N + [0] = c_20(isNat#(activate(N)),isNatIList#(activate(IL))) 0() = [0] >= [0] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [0] >= [0] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = cons(activate(X1),X2) activate(n__length(X)) = [1] X + [2] >= [1] X + [2] = length(activate(X)) activate(n__nil()) = [8] >= [8] = nil() activate(n__s(X)) = [1] X + [5] >= [1] X + [5] = s(activate(X)) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = take(activate(X1),activate(X2)) activate(n__zeros()) = [0] >= [0] = zeros() cons(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__cons(X1,X2) length(X) = [1] X + [2] >= [1] X + [2] = n__length(X) nil() = [8] >= [8] = n__nil() s(X) = [1] X + [5] >= [1] X + [5] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__take(X1,X2) zeros() = [0] >= [0] = cons(0(),n__zeros()) zeros() = [0] >= [0] = n__zeros() *** Step 11.b:3.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak DPs: isNat#(n__s(N)) -> c_14(isNat#(activate(N))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 11.b:3.b:1: PredecessorEstimationCP MAYBE + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak DPs: isNat#(n__s(N)) -> c_14(isNat#(activate(N))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: isNatIList#(IL) -> c_15(isNatList#(activate(IL))) The strictly oriented rules are moved into the weak component. **** Step 11.b:3.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak DPs: isNat#(n__s(N)) -> c_14(isNat#(activate(N))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1,2}, uargs(c_18) = {1,2}, uargs(c_20) = {1,2} Following symbols are considered usable: {0,activate,cons,length,nil,s,take,zeros,0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList#,length# ,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(and) = [0] p(cons) = [1] x1 + [1] x2 + [0] p(isNat) = [0] p(isNatIList) = [4] p(isNatList) = [2] p(length) = [1] x1 + [8] p(n__0) = [0] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__length) = [1] x1 + [8] p(n__nil) = [0] p(n__s) = [1] x1 + [2] p(n__take) = [1] x1 + [1] x2 + [4] p(n__zeros) = [0] p(nil) = [0] p(s) = [1] x1 + [2] p(take) = [1] x1 + [1] x2 + [4] p(tt) = [1] p(uLength) = [2] p(uTake1) = [2] x1 + [0] p(uTake2) = [4] x1 + [2] x3 + [1] p(zeros) = [0] p(0#) = [1] p(activate#) = [1] x1 + [4] p(and#) = [1] x1 + [1] x2 + [1] p(cons#) = [1] p(isNat#) = [1] x1 + [0] p(isNatIList#) = [1] x1 + [11] p(isNatList#) = [1] x1 + [8] p(length#) = [1] x1 + [0] p(nil#) = [1] p(s#) = [2] x1 + [0] p(take#) = [1] x1 + [4] p(uLength#) = [1] x1 + [4] x2 + [0] p(uTake1#) = [1] x1 + [8] p(uTake2#) = [2] x1 + [1] x2 + [1] p(zeros#) = [2] p(c_1) = [1] p(c_2) = [1] p(c_3) = [1] p(c_4) = [8] p(c_5) = [0] p(c_6) = [1] x1 + [1] p(c_7) = [1] x1 + [1] p(c_8) = [1] x2 + [1] p(c_9) = [2] p(c_10) = [0] p(c_11) = [1] p(c_12) = [1] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [2] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [0] p(c_18) = [1] x1 + [1] x2 + [0] p(c_19) = [2] p(c_20) = [1] x1 + [1] x2 + [1] p(c_21) = [0] p(c_22) = [1] p(c_23) = [2] p(c_24) = [4] p(c_25) = [1] x1 + [0] p(c_26) = [1] p(c_27) = [2] x2 + [0] p(c_28) = [1] x2 + [2] p(c_29) = [2] Following rules are strictly oriented: isNatIList#(IL) = [1] IL + [11] > [1] IL + [8] = c_15(isNatList#(activate(IL))) Following rules are (at-least) weakly oriented: isNat#(n__length(L)) = [1] L + [8] >= [1] L + [8] = c_13(isNatList#(activate(L))) isNat#(n__s(N)) = [1] N + [2] >= [1] N + [2] = c_14(isNat#(activate(N))) isNatIList#(n__cons(N,IL)) = [1] IL + [1] N + [11] >= [1] IL + [1] N + [11] = c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) = [1] L + [1] N + [8] >= [1] L + [1] N + [8] = c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) = [1] IL + [1] N + [12] >= [1] IL + [1] N + [12] = c_20(isNat#(activate(N)),isNatIList#(activate(IL))) 0() = [0] >= [0] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [0] >= [0] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = cons(activate(X1),X2) activate(n__length(X)) = [1] X + [8] >= [1] X + [8] = length(activate(X)) activate(n__nil()) = [0] >= [0] = nil() activate(n__s(X)) = [1] X + [2] >= [1] X + [2] = s(activate(X)) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = take(activate(X1),activate(X2)) activate(n__zeros()) = [0] >= [0] = zeros() cons(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__cons(X1,X2) length(X) = [1] X + [8] >= [1] X + [8] = n__length(X) nil() = [0] >= [0] = n__nil() s(X) = [1] X + [2] >= [1] X + [2] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [4] >= [1] X1 + [1] X2 + [4] = n__take(X1,X2) zeros() = [0] >= [0] = cons(0(),n__zeros()) zeros() = [0] >= [0] = n__zeros() **** Step 11.b:3.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak DPs: isNat#(n__s(N)) -> c_14(isNat#(activate(N))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 11.b:3.b:1.b:1: PredecessorEstimationCP MAYBE + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak DPs: isNat#(n__s(N)) -> c_14(isNat#(activate(N))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) 4: isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) The strictly oriented rules are moved into the weak component. ***** Step 11.b:3.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak DPs: isNat#(n__s(N)) -> c_14(isNat#(activate(N))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_13) = {1}, uargs(c_14) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1,2}, uargs(c_18) = {1,2}, uargs(c_20) = {1,2} Following symbols are considered usable: {0,activate,cons,length,nil,s,take,zeros,0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList#,length# ,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(and) = [1] x1 + [2] p(cons) = [1] x1 + [1] x2 + [0] p(isNat) = [1] p(isNatIList) = [8] x1 + [1] p(isNatList) = [0] p(length) = [1] x1 + [2] p(n__0) = [0] p(n__cons) = [1] x1 + [1] x2 + [0] p(n__length) = [1] x1 + [2] p(n__nil) = [0] p(n__s) = [1] x1 + [0] p(n__take) = [1] x1 + [1] x2 + [2] p(n__zeros) = [0] p(nil) = [0] p(s) = [1] x1 + [0] p(take) = [1] x1 + [1] x2 + [2] p(tt) = [1] p(uLength) = [2] p(uTake1) = [4] x1 + [1] p(uTake2) = [8] x2 + [2] x3 + [1] x4 + [2] p(zeros) = [0] p(0#) = [1] p(activate#) = [4] x1 + [2] p(and#) = [8] x1 + [1] x2 + [2] p(cons#) = [1] x1 + [0] p(isNat#) = [8] x1 + [0] p(isNatIList#) = [8] x1 + [4] p(isNatList#) = [8] x1 + [0] p(length#) = [2] x1 + [1] p(nil#) = [0] p(s#) = [1] x1 + [1] p(take#) = [1] p(uLength#) = [4] x2 + [0] p(uTake1#) = [1] x1 + [8] p(uTake2#) = [1] x2 + [2] x4 + [0] p(zeros#) = [4] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] x1 + [0] p(c_4) = [2] x1 + [1] p(c_5) = [2] p(c_6) = [1] p(c_7) = [2] x1 + [0] p(c_8) = [1] x2 + [0] p(c_9) = [1] p(c_10) = [1] p(c_11) = [0] p(c_12) = [1] p(c_13) = [1] x1 + [9] p(c_14) = [1] x1 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [1] x2 + [0] p(c_17) = [2] p(c_18) = [1] x1 + [1] x2 + [0] p(c_19) = [0] p(c_20) = [1] x1 + [1] x2 + [10] p(c_21) = [1] p(c_22) = [2] p(c_23) = [2] p(c_24) = [1] p(c_25) = [2] x1 + [1] p(c_26) = [1] x1 + [8] p(c_27) = [1] x1 + [2] x2 + [0] p(c_28) = [2] x1 + [0] p(c_29) = [0] Following rules are strictly oriented: isNat#(n__length(L)) = [8] L + [16] > [8] L + [9] = c_13(isNatList#(activate(L))) isNatList#(n__take(N,IL)) = [8] IL + [8] N + [16] > [8] IL + [8] N + [14] = c_20(isNat#(activate(N)),isNatIList#(activate(IL))) Following rules are (at-least) weakly oriented: isNat#(n__s(N)) = [8] N + [0] >= [8] N + [0] = c_14(isNat#(activate(N))) isNatIList#(IL) = [8] IL + [4] >= [8] IL + [0] = c_15(isNatList#(activate(IL))) isNatIList#(n__cons(N,IL)) = [8] IL + [8] N + [4] >= [8] IL + [8] N + [4] = c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) = [8] L + [8] N + [0] >= [8] L + [8] N + [0] = c_18(isNat#(activate(N)),isNatList#(activate(L))) 0() = [0] >= [0] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [0] >= [0] = 0() activate(n__cons(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = cons(activate(X1),X2) activate(n__length(X)) = [1] X + [2] >= [1] X + [2] = length(activate(X)) activate(n__nil()) = [0] >= [0] = nil() activate(n__s(X)) = [1] X + [0] >= [1] X + [0] = s(activate(X)) activate(n__take(X1,X2)) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = take(activate(X1),activate(X2)) activate(n__zeros()) = [0] >= [0] = zeros() cons(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__cons(X1,X2) length(X) = [1] X + [2] >= [1] X + [2] = n__length(X) nil() = [0] >= [0] = n__nil() s(X) = [1] X + [0] >= [1] X + [0] = n__s(X) take(X1,X2) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = n__take(X1,X2) zeros() = [0] >= [0] = cons(0(),n__zeros()) zeros() = [0] >= [0] = n__zeros() ***** Step 11.b:3.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) - Weak DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNat#(n__s(N)) -> c_14(isNat#(activate(N))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () ***** Step 11.b:3.b:1.b:1.b:1: Failure MAYBE + Considered Problem: - Strict DPs: isNatIList#(n__cons(N,IL)) -> c_16(isNat#(activate(N)),isNatIList#(activate(IL))) isNatList#(n__cons(N,L)) -> c_18(isNat#(activate(N)),isNatList#(activate(L))) - Weak DPs: isNat#(n__length(L)) -> c_13(isNatList#(activate(L))) isNat#(n__s(N)) -> c_14(isNat#(activate(N))) isNatIList#(IL) -> c_15(isNatList#(activate(IL))) isNatList#(n__take(N,IL)) -> c_20(isNat#(activate(N)),isNatIList#(activate(IL))) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__cons(X1,X2)) -> cons(activate(X1),X2) activate(n__length(X)) -> length(activate(X)) activate(n__nil()) -> nil() activate(n__s(X)) -> s(activate(X)) activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) activate(n__zeros()) -> zeros() cons(X1,X2) -> n__cons(X1,X2) 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,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,uLength/2,uTake1/1 ,uTake2/4,zeros/0,0#/0,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,nil#/0,s#/1 ,take#/2,uLength#/2,uTake1#/1,uTake2#/4,zeros#/0} / {n__0/0,n__cons/2,n__length/1,n__nil/0,n__s/1,n__take/2 ,n__zeros/0,tt/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/2,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/1 ,c_15/1,c_16/2,c_17/0,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0,c_23/0,c_24/0,c_25/1,c_26/1,c_27/3,c_28/2,c_29/0} - Obligation: innermost runtime complexity wrt. defined symbols {0#,activate#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,nil#,s#,take#,uLength#,uTake1#,uTake2#,zeros#} and constructors {n__0,n__cons,n__length,n__nil,n__s ,n__take,n__zeros,tt} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE