MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U11(tt(), V1) -> U12(isNatList(activate(V1))) , U12(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__length(X)) -> length(X) , activate(n__s(X)) -> s(X) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__isNatIListKind(X)) -> isNatIListKind(X) , activate(n__nil()) -> nil() , activate(n__and(X1, X2)) -> and(X1, X2) , activate(n__isNatKind(X)) -> isNatKind(X) , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U31(tt(), V) -> U32(isNatList(activate(V))) , U32(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNatIList(activate(V2))) , U43(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isNatList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) , U62(tt(), V2) -> U63(isNatIList(activate(V2))) , U63(tt()) -> tt() , U71(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L)) , length(nil()) -> 0() , U81(tt()) -> nil() , nil() -> n__nil() , U91(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatIListKind(X) -> n__isNatIListKind(X) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__cons(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__nil()) -> tt() , isNatKind(X) -> n__isNatKind(X) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) , take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { zeros^#() -> c_1(cons^#(0(), n__zeros())) , zeros^#() -> c_2() , cons^#(X1, X2) -> c_3(X1, X2) , 0^#() -> c_4() , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , U12^#(tt()) -> c_6() , isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , isNatList^#(n__nil()) -> c_9() , U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , activate^#(X) -> c_10(X) , activate^#(n__zeros()) -> c_11(zeros^#()) , activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__length(X)) -> c_14(length^#(X)) , activate^#(n__s(X)) -> c_15(s^#(X)) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , activate^#(n__nil()) -> c_18(nil^#()) , activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , take^#(X1, X2) -> c_59(X1, X2) , take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , length^#(X) -> c_42(X) , length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , length^#(nil()) -> c_44(0^#()) , s^#(X) -> c_41(X) , isNatIListKind^#(X) -> c_50(X) , isNatIListKind^#(n__zeros()) -> c_51() , isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , isNatIListKind^#(n__nil()) -> c_54() , nil^#() -> c_46() , and^#(X1, X2) -> c_48(X1, X2) , and^#(tt(), X) -> c_49(activate^#(X)) , isNatKind^#(X) -> c_55(X) , isNatKind^#(n__0()) -> c_56() , isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , U22^#(tt()) -> c_22() , isNat^#(n__0()) -> c_23() , isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , U32^#(tt()) -> c_27() , U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , U43^#(tt()) -> c_30() , isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_32() , isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , U53^#(tt()) -> c_36() , U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , U63^#(tt()) -> c_39() , U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , U81^#(tt()) -> c_45(nil^#()) , U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { zeros^#() -> c_1(cons^#(0(), n__zeros())) , zeros^#() -> c_2() , cons^#(X1, X2) -> c_3(X1, X2) , 0^#() -> c_4() , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , U12^#(tt()) -> c_6() , isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , isNatList^#(n__nil()) -> c_9() , U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , activate^#(X) -> c_10(X) , activate^#(n__zeros()) -> c_11(zeros^#()) , activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__length(X)) -> c_14(length^#(X)) , activate^#(n__s(X)) -> c_15(s^#(X)) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , activate^#(n__nil()) -> c_18(nil^#()) , activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , take^#(X1, X2) -> c_59(X1, X2) , take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , length^#(X) -> c_42(X) , length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , length^#(nil()) -> c_44(0^#()) , s^#(X) -> c_41(X) , isNatIListKind^#(X) -> c_50(X) , isNatIListKind^#(n__zeros()) -> c_51() , isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , isNatIListKind^#(n__nil()) -> c_54() , nil^#() -> c_46() , and^#(X1, X2) -> c_48(X1, X2) , and^#(tt(), X) -> c_49(activate^#(X)) , isNatKind^#(X) -> c_55(X) , isNatKind^#(n__0()) -> c_56() , isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , U22^#(tt()) -> c_22() , isNat^#(n__0()) -> c_23() , isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , U32^#(tt()) -> c_27() , U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , U43^#(tt()) -> c_30() , isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_32() , isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , U53^#(tt()) -> c_36() , U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , U63^#(tt()) -> c_39() , U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , U81^#(tt()) -> c_45(nil^#()) , U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U11(tt(), V1) -> U12(isNatList(activate(V1))) , U12(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__length(X)) -> length(X) , activate(n__s(X)) -> s(X) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__isNatIListKind(X)) -> isNatIListKind(X) , activate(n__nil()) -> nil() , activate(n__and(X1, X2)) -> and(X1, X2) , activate(n__isNatKind(X)) -> isNatKind(X) , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U31(tt(), V) -> U32(isNatList(activate(V))) , U32(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNatIList(activate(V2))) , U43(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isNatList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) , U62(tt(), V2) -> U63(isNatIList(activate(V2))) , U63(tt()) -> tt() , U71(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L)) , length(nil()) -> 0() , U81(tt()) -> nil() , nil() -> n__nil() , U91(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatIListKind(X) -> n__isNatIListKind(X) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__cons(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__nil()) -> tt() , isNatKind(X) -> n__isNatKind(X) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) , take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,4,6,9,31,34,35,39,43,44,48,51,53,56,58} by applications of Pre({2,4,6,9,31,34,35,39,43,44,48,51,53,56,58}) = {3,5,12,13,15,19,20,22,23,26,28,29,30,36,38,40,41,42,47,50,55,57,60}. Here rules are labeled as follows: DPs: { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) , 2: zeros^#() -> c_2() , 3: cons^#(X1, X2) -> c_3(X1, X2) , 4: 0^#() -> c_4() , 5: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , 6: U12^#(tt()) -> c_6() , 7: isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 8: isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 9: isNatList^#(n__nil()) -> c_9() , 10: U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , 11: U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , 12: activate^#(X) -> c_10(X) , 13: activate^#(n__zeros()) -> c_11(zeros^#()) , 14: activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , 15: activate^#(n__0()) -> c_13(0^#()) , 16: activate^#(n__length(X)) -> c_14(length^#(X)) , 17: activate^#(n__s(X)) -> c_15(s^#(X)) , 18: activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , 19: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , 20: activate^#(n__nil()) -> c_18(nil^#()) , 21: activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , 22: activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , 23: take^#(X1, X2) -> c_59(X1, X2) , 24: take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , 25: take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , 26: length^#(X) -> c_42(X) , 27: length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , 28: length^#(nil()) -> c_44(0^#()) , 29: s^#(X) -> c_41(X) , 30: isNatIListKind^#(X) -> c_50(X) , 31: isNatIListKind^#(n__zeros()) -> c_51() , 32: isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , 33: isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , 34: isNatIListKind^#(n__nil()) -> c_54() , 35: nil^#() -> c_46() , 36: and^#(X1, X2) -> c_48(X1, X2) , 37: and^#(tt(), X) -> c_49(activate^#(X)) , 38: isNatKind^#(X) -> c_55(X) , 39: isNatKind^#(n__0()) -> c_56() , 40: isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , 41: isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , 42: U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , 43: U22^#(tt()) -> c_22() , 44: isNat^#(n__0()) -> c_23() , 45: isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 46: isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , 47: U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , 48: U32^#(tt()) -> c_27() , 49: U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , 50: U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , 51: U43^#(tt()) -> c_30() , 52: isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , 53: isNatIList^#(n__zeros()) -> c_32() , 54: isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 55: U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , 56: U53^#(tt()) -> c_36() , 57: U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , 58: U63^#(tt()) -> c_39() , 59: U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , 60: U81^#(tt()) -> c_45(nil^#()) , 61: U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { zeros^#() -> c_1(cons^#(0(), n__zeros())) , cons^#(X1, X2) -> c_3(X1, X2) , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , activate^#(X) -> c_10(X) , activate^#(n__zeros()) -> c_11(zeros^#()) , activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__length(X)) -> c_14(length^#(X)) , activate^#(n__s(X)) -> c_15(s^#(X)) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , activate^#(n__nil()) -> c_18(nil^#()) , activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , take^#(X1, X2) -> c_59(X1, X2) , take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , length^#(X) -> c_42(X) , length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , length^#(nil()) -> c_44(0^#()) , s^#(X) -> c_41(X) , isNatIListKind^#(X) -> c_50(X) , isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , and^#(X1, X2) -> c_48(X1, X2) , and^#(tt(), X) -> c_49(activate^#(X)) , isNatKind^#(X) -> c_55(X) , isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , U81^#(tt()) -> c_45(nil^#()) , U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U11(tt(), V1) -> U12(isNatList(activate(V1))) , U12(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__length(X)) -> length(X) , activate(n__s(X)) -> s(X) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__isNatIListKind(X)) -> isNatIListKind(X) , activate(n__nil()) -> nil() , activate(n__and(X1, X2)) -> and(X1, X2) , activate(n__isNatKind(X)) -> isNatKind(X) , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U31(tt(), V) -> U32(isNatList(activate(V))) , U32(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNatIList(activate(V2))) , U43(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isNatList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) , U62(tt(), V2) -> U63(isNatIList(activate(V2))) , U63(tt()) -> tt() , U71(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L)) , length(nil()) -> 0() , U81(tt()) -> nil() , nil() -> n__nil() , U91(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatIListKind(X) -> n__isNatIListKind(X) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__cons(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__nil()) -> tt() , isNatKind(X) -> n__isNatKind(X) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) , take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , U12^#(tt()) -> c_6() , isNatList^#(n__nil()) -> c_9() , isNatIListKind^#(n__zeros()) -> c_51() , isNatIListKind^#(n__nil()) -> c_54() , nil^#() -> c_46() , isNatKind^#(n__0()) -> c_56() , U22^#(tt()) -> c_22() , isNat^#(n__0()) -> c_23() , U32^#(tt()) -> c_27() , U43^#(tt()) -> c_30() , isNatIList^#(n__zeros()) -> c_32() , U53^#(tt()) -> c_36() , U63^#(tt()) -> c_39() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {3,11,16,24,34,37,39,42,43,45} by applications of Pre({3,11,16,24,34,37,39,42,43,45}) = {2,6,7,8,12,19,20,22,25,26,29,30,31,35,36,38,40}. Here rules are labeled as follows: DPs: { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) , 2: cons^#(X1, X2) -> c_3(X1, X2) , 3: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , 4: isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 5: isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 6: U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , 7: U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , 8: activate^#(X) -> c_10(X) , 9: activate^#(n__zeros()) -> c_11(zeros^#()) , 10: activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , 11: activate^#(n__0()) -> c_13(0^#()) , 12: activate^#(n__length(X)) -> c_14(length^#(X)) , 13: activate^#(n__s(X)) -> c_15(s^#(X)) , 14: activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , 15: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , 16: activate^#(n__nil()) -> c_18(nil^#()) , 17: activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , 18: activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , 19: take^#(X1, X2) -> c_59(X1, X2) , 20: take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , 21: take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , 22: length^#(X) -> c_42(X) , 23: length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , 24: length^#(nil()) -> c_44(0^#()) , 25: s^#(X) -> c_41(X) , 26: isNatIListKind^#(X) -> c_50(X) , 27: isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , 28: isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , 29: and^#(X1, X2) -> c_48(X1, X2) , 30: and^#(tt(), X) -> c_49(activate^#(X)) , 31: isNatKind^#(X) -> c_55(X) , 32: isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , 33: isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , 34: U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , 35: isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 36: isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , 37: U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , 38: U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , 39: U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , 40: isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , 41: isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 42: U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , 43: U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , 44: U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , 45: U81^#(tt()) -> c_45(nil^#()) , 46: U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 47: zeros^#() -> c_2() , 48: 0^#() -> c_4() , 49: U12^#(tt()) -> c_6() , 50: isNatList^#(n__nil()) -> c_9() , 51: isNatIListKind^#(n__zeros()) -> c_51() , 52: isNatIListKind^#(n__nil()) -> c_54() , 53: nil^#() -> c_46() , 54: isNatKind^#(n__0()) -> c_56() , 55: U22^#(tt()) -> c_22() , 56: isNat^#(n__0()) -> c_23() , 57: U32^#(tt()) -> c_27() , 58: U43^#(tt()) -> c_30() , 59: isNatIList^#(n__zeros()) -> c_32() , 60: U53^#(tt()) -> c_36() , 61: U63^#(tt()) -> c_39() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { zeros^#() -> c_1(cons^#(0(), n__zeros())) , cons^#(X1, X2) -> c_3(X1, X2) , isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , activate^#(X) -> c_10(X) , activate^#(n__zeros()) -> c_11(zeros^#()) , activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , activate^#(n__length(X)) -> c_14(length^#(X)) , activate^#(n__s(X)) -> c_15(s^#(X)) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , take^#(X1, X2) -> c_59(X1, X2) , take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , length^#(X) -> c_42(X) , length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , s^#(X) -> c_41(X) , isNatIListKind^#(X) -> c_50(X) , isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , and^#(X1, X2) -> c_48(X1, X2) , and^#(tt(), X) -> c_49(activate^#(X)) , isNatKind^#(X) -> c_55(X) , isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U11(tt(), V1) -> U12(isNatList(activate(V1))) , U12(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__length(X)) -> length(X) , activate(n__s(X)) -> s(X) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__isNatIListKind(X)) -> isNatIListKind(X) , activate(n__nil()) -> nil() , activate(n__and(X1, X2)) -> and(X1, X2) , activate(n__isNatKind(X)) -> isNatKind(X) , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U31(tt(), V) -> U32(isNatList(activate(V))) , U32(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNatIList(activate(V2))) , U43(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isNatList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) , U62(tt(), V2) -> U63(isNatIList(activate(V2))) , U63(tt()) -> tt() , U71(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L)) , length(nil()) -> 0() , U81(tt()) -> nil() , nil() -> n__nil() , U91(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatIListKind(X) -> n__isNatIListKind(X) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__cons(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__nil()) -> tt() , isNatKind(X) -> n__isNatKind(X) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) , take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , U12^#(tt()) -> c_6() , isNatList^#(n__nil()) -> c_9() , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__nil()) -> c_18(nil^#()) , length^#(nil()) -> c_44(0^#()) , isNatIListKind^#(n__zeros()) -> c_51() , isNatIListKind^#(n__nil()) -> c_54() , nil^#() -> c_46() , isNatKind^#(n__0()) -> c_56() , U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , U22^#(tt()) -> c_22() , isNat^#(n__0()) -> c_23() , U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , U32^#(tt()) -> c_27() , U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , U43^#(tt()) -> c_30() , isNatIList^#(n__zeros()) -> c_32() , U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , U53^#(tt()) -> c_36() , U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , U63^#(tt()) -> c_39() , U81^#(tt()) -> c_45(nil^#()) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,6,17,30,31,32,33} by applications of Pre({5,6,17,30,31,32,33}) = {2,3,4,7,9,16,19,21,22,25,27,34}. Here rules are labeled as follows: DPs: { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) , 2: cons^#(X1, X2) -> c_3(X1, X2) , 3: isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 4: isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 5: U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , 6: U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , 7: activate^#(X) -> c_10(X) , 8: activate^#(n__zeros()) -> c_11(zeros^#()) , 9: activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , 10: activate^#(n__length(X)) -> c_14(length^#(X)) , 11: activate^#(n__s(X)) -> c_15(s^#(X)) , 12: activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , 13: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , 14: activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , 15: activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , 16: take^#(X1, X2) -> c_59(X1, X2) , 17: take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , 18: take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , 19: length^#(X) -> c_42(X) , 20: length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , 21: s^#(X) -> c_41(X) , 22: isNatIListKind^#(X) -> c_50(X) , 23: isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , 24: isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , 25: and^#(X1, X2) -> c_48(X1, X2) , 26: and^#(tt(), X) -> c_49(activate^#(X)) , 27: isNatKind^#(X) -> c_55(X) , 28: isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , 29: isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , 30: isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 31: isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , 32: U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , 33: isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , 34: isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 35: U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , 36: U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 37: zeros^#() -> c_2() , 38: 0^#() -> c_4() , 39: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , 40: U12^#(tt()) -> c_6() , 41: isNatList^#(n__nil()) -> c_9() , 42: activate^#(n__0()) -> c_13(0^#()) , 43: activate^#(n__nil()) -> c_18(nil^#()) , 44: length^#(nil()) -> c_44(0^#()) , 45: isNatIListKind^#(n__zeros()) -> c_51() , 46: isNatIListKind^#(n__nil()) -> c_54() , 47: nil^#() -> c_46() , 48: isNatKind^#(n__0()) -> c_56() , 49: U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , 50: U22^#(tt()) -> c_22() , 51: isNat^#(n__0()) -> c_23() , 52: U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , 53: U32^#(tt()) -> c_27() , 54: U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , 55: U43^#(tt()) -> c_30() , 56: isNatIList^#(n__zeros()) -> c_32() , 57: U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , 58: U53^#(tt()) -> c_36() , 59: U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , 60: U63^#(tt()) -> c_39() , 61: U81^#(tt()) -> c_45(nil^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { zeros^#() -> c_1(cons^#(0(), n__zeros())) , cons^#(X1, X2) -> c_3(X1, X2) , isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , activate^#(X) -> c_10(X) , activate^#(n__zeros()) -> c_11(zeros^#()) , activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , activate^#(n__length(X)) -> c_14(length^#(X)) , activate^#(n__s(X)) -> c_15(s^#(X)) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , take^#(X1, X2) -> c_59(X1, X2) , take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , length^#(X) -> c_42(X) , length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , s^#(X) -> c_41(X) , isNatIListKind^#(X) -> c_50(X) , isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , and^#(X1, X2) -> c_48(X1, X2) , and^#(tt(), X) -> c_49(activate^#(X)) , isNatKind^#(X) -> c_55(X) , isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U11(tt(), V1) -> U12(isNatList(activate(V1))) , U12(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__length(X)) -> length(X) , activate(n__s(X)) -> s(X) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__isNatIListKind(X)) -> isNatIListKind(X) , activate(n__nil()) -> nil() , activate(n__and(X1, X2)) -> and(X1, X2) , activate(n__isNatKind(X)) -> isNatKind(X) , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U31(tt(), V) -> U32(isNatList(activate(V))) , U32(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNatIList(activate(V2))) , U43(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isNatList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) , U62(tt(), V2) -> U63(isNatIList(activate(V2))) , U63(tt()) -> tt() , U71(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L)) , length(nil()) -> 0() , U81(tt()) -> nil() , nil() -> n__nil() , U91(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatIListKind(X) -> n__isNatIListKind(X) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__cons(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__nil()) -> tt() , isNatKind(X) -> n__isNatKind(X) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) , take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , U12^#(tt()) -> c_6() , isNatList^#(n__nil()) -> c_9() , U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__nil()) -> c_18(nil^#()) , take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , length^#(nil()) -> c_44(0^#()) , isNatIListKind^#(n__zeros()) -> c_51() , isNatIListKind^#(n__nil()) -> c_54() , nil^#() -> c_46() , isNatKind^#(n__0()) -> c_56() , U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , U22^#(tt()) -> c_22() , isNat^#(n__0()) -> c_23() , isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , U32^#(tt()) -> c_27() , U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , U43^#(tt()) -> c_30() , isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_32() , U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , U53^#(tt()) -> c_36() , U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , U63^#(tt()) -> c_39() , U81^#(tt()) -> c_45(nil^#()) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {3,4,27} by applications of Pre({3,4,27}) = {2,5,14,16,18,19,22,24}. Here rules are labeled as follows: DPs: { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) , 2: cons^#(X1, X2) -> c_3(X1, X2) , 3: isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 4: isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 5: activate^#(X) -> c_10(X) , 6: activate^#(n__zeros()) -> c_11(zeros^#()) , 7: activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , 8: activate^#(n__length(X)) -> c_14(length^#(X)) , 9: activate^#(n__s(X)) -> c_15(s^#(X)) , 10: activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , 11: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , 12: activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , 13: activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , 14: take^#(X1, X2) -> c_59(X1, X2) , 15: take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , 16: length^#(X) -> c_42(X) , 17: length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , 18: s^#(X) -> c_41(X) , 19: isNatIListKind^#(X) -> c_50(X) , 20: isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , 21: isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , 22: and^#(X1, X2) -> c_48(X1, X2) , 23: and^#(tt(), X) -> c_49(activate^#(X)) , 24: isNatKind^#(X) -> c_55(X) , 25: isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , 26: isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , 27: isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , 28: U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , 29: U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 30: zeros^#() -> c_2() , 31: 0^#() -> c_4() , 32: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , 33: U12^#(tt()) -> c_6() , 34: isNatList^#(n__nil()) -> c_9() , 35: U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , 36: U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , 37: activate^#(n__0()) -> c_13(0^#()) , 38: activate^#(n__nil()) -> c_18(nil^#()) , 39: take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , 40: length^#(nil()) -> c_44(0^#()) , 41: isNatIListKind^#(n__zeros()) -> c_51() , 42: isNatIListKind^#(n__nil()) -> c_54() , 43: nil^#() -> c_46() , 44: isNatKind^#(n__0()) -> c_56() , 45: U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , 46: U22^#(tt()) -> c_22() , 47: isNat^#(n__0()) -> c_23() , 48: isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 49: isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , 50: U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , 51: U32^#(tt()) -> c_27() , 52: U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , 53: U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , 54: U43^#(tt()) -> c_30() , 55: isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , 56: isNatIList^#(n__zeros()) -> c_32() , 57: U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , 58: U53^#(tt()) -> c_36() , 59: U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , 60: U63^#(tt()) -> c_39() , 61: U81^#(tt()) -> c_45(nil^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { zeros^#() -> c_1(cons^#(0(), n__zeros())) , cons^#(X1, X2) -> c_3(X1, X2) , activate^#(X) -> c_10(X) , activate^#(n__zeros()) -> c_11(zeros^#()) , activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , activate^#(n__length(X)) -> c_14(length^#(X)) , activate^#(n__s(X)) -> c_15(s^#(X)) , activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X)) , activate^#(n__and(X1, X2)) -> c_19(and^#(X1, X2)) , activate^#(n__isNatKind(X)) -> c_20(isNatKind^#(X)) , take^#(X1, X2) -> c_59(X1, X2) , take^#(s(M), cons(N, IL)) -> c_61(U91^#(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N)) , length^#(X) -> c_42(X) , length^#(cons(N, L)) -> c_43(U71^#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L))) , s^#(X) -> c_41(X) , isNatIListKind^#(X) -> c_50(X) , isNatIListKind^#(n__take(V1, V2)) -> c_52(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , isNatIListKind^#(n__cons(V1, V2)) -> c_53(and^#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))) , and^#(X1, X2) -> c_48(X1, X2) , and^#(tt(), X) -> c_49(activate^#(X)) , isNatKind^#(X) -> c_55(X) , isNatKind^#(n__length(V1)) -> c_57(isNatIListKind^#(activate(V1))) , isNatKind^#(n__s(V1)) -> c_58(isNatKind^#(activate(V1))) , U71^#(tt(), L) -> c_40(s^#(length(activate(L)))) , U91^#(tt(), IL, M, N) -> c_47(cons^#(activate(N), n__take(activate(M), activate(IL)))) } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U11(tt(), V1) -> U12(isNatList(activate(V1))) , U12(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , activate(X) -> X , activate(n__zeros()) -> zeros() , activate(n__take(X1, X2)) -> take(X1, X2) , activate(n__0()) -> 0() , activate(n__length(X)) -> length(X) , activate(n__s(X)) -> s(X) , activate(n__cons(X1, X2)) -> cons(X1, X2) , activate(n__isNatIListKind(X)) -> isNatIListKind(X) , activate(n__nil()) -> nil() , activate(n__and(X1, X2)) -> and(X1, X2) , activate(n__isNatKind(X)) -> isNatKind(X) , U21(tt(), V1) -> U22(isNat(activate(V1))) , U22(tt()) -> tt() , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U31(tt(), V) -> U32(isNatList(activate(V))) , U32(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isNatIList(activate(V2))) , U43(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isNatList(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2)) , U62(tt(), V2) -> U63(isNatIList(activate(V2))) , U63(tt()) -> tt() , U71(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L)) , length(nil()) -> 0() , U81(tt()) -> nil() , nil() -> n__nil() , U91(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatIListKind(X) -> n__isNatIListKind(X) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__cons(V1, V2)) -> and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) , isNatIListKind(n__nil()) -> tt() , isNatKind(X) -> n__isNatKind(X) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) , isNatKind(n__s(V1)) -> isNatKind(activate(V1)) , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL))) , take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1)))) , U12^#(tt()) -> c_6() , isNatList^#(n__take(V1, V2)) -> c_7(U61^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_8(U51^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , isNatList^#(n__nil()) -> c_9() , U61^#(tt(), V1, V2) -> c_37(U62^#(isNat(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_34(U52^#(isNat(activate(V1)), activate(V2))) , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__nil()) -> c_18(nil^#()) , take^#(0(), IL) -> c_60(U81^#(and(isNatIList(IL), n__isNatIListKind(IL)))) , length^#(nil()) -> c_44(0^#()) , isNatIListKind^#(n__zeros()) -> c_51() , isNatIListKind^#(n__nil()) -> c_54() , nil^#() -> c_46() , isNatKind^#(n__0()) -> c_56() , U21^#(tt(), V1) -> c_21(U22^#(isNat(activate(V1)))) , U22^#(tt()) -> c_22() , isNat^#(n__0()) -> c_23() , isNat^#(n__length(V1)) -> c_24(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_25(U21^#(isNatKind(activate(V1)), activate(V1))) , U31^#(tt(), V) -> c_26(U32^#(isNatList(activate(V)))) , U32^#(tt()) -> c_27() , U41^#(tt(), V1, V2) -> c_28(U42^#(isNat(activate(V1)), activate(V2))) , U42^#(tt(), V2) -> c_29(U43^#(isNatIList(activate(V2)))) , U43^#(tt()) -> c_30() , isNatIList^#(V) -> c_31(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_32() , isNatIList^#(n__cons(V1, V2)) -> c_33(U41^#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2))) , U52^#(tt(), V2) -> c_35(U53^#(isNatList(activate(V2)))) , U53^#(tt()) -> c_36() , U62^#(tt(), V2) -> c_38(U63^#(isNatIList(activate(V2)))) , U63^#(tt()) -> c_39() , U81^#(tt()) -> c_45(nil^#()) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..