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() , U101(tt(), V1, V2) -> U102(isNatKind(activate(V1)), activate(V1), activate(V2)) , U102(tt(), V1, V2) -> U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) , 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__nil()) -> nil() , U103(tt(), V1, V2) -> U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__cons(V1, V2)) -> U51(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__nil()) -> tt() , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) , U105(tt(), V2) -> U106(isNatIList(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U106(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) , U12(tt(), V1) -> U13(isNatList(activate(V1))) , U111(tt(), L, N) -> U112(isNatIListKind(activate(L)), activate(L), activate(N)) , U112(tt(), L, N) -> U113(isNat(activate(N)), activate(L), activate(N)) , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) , U114(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U111(isNatList(activate(L)), activate(L), N) , length(nil()) -> 0() , U13(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U101(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U91(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) , U122(tt()) -> nil() , nil() -> n__nil() , U131(tt(), IL, M, N) -> U132(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N)) , U132(tt(), IL, M, N) -> U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) , U133(tt(), IL, M, N) -> U134(isNatKind(activate(M)), activate(IL), activate(M), activate(N)) , U134(tt(), IL, M, N) -> U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) , U135(tt(), IL, M, N) -> U136(isNatKind(activate(N)), activate(IL), activate(M), activate(N)) , U136(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isNatList(activate(V))) , U33(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNatKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNatIList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) , U52(tt()) -> tt() , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) , U62(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt(), V1, V2) -> U92(isNatKind(activate(V1)), activate(V1), activate(V2)) , U92(tt(), V1, V2) -> U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U93(tt(), V1, V2) -> U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) , U95(tt(), V2) -> U96(isNatList(activate(V2))) , U96(tt()) -> tt() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U121(isNatIList(IL), IL) , take(s(M), cons(N, IL)) -> U131(isNatIList(activate(IL)), 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) '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) '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) '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() , U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , isNatKind^#(n__0()) -> c_7() , isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , U71^#(tt()) -> c_71() , U81^#(tt()) -> c_72() , 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__nil()) -> c_17(nil^#()) , take^#(X1, X2) -> c_79(X1, X2) , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , length^#(X) -> c_39(X) , length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , length^#(nil()) -> c_41(0^#()) , s^#(X) -> c_38(X) , nil^#() -> c_48() , U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , isNatIListKind^#(n__zeros()) -> c_19() , isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__nil()) -> c_22() , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , U106^#(tt()) -> c_28() , isNat^#(n__0()) -> c_25() , isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_30() , isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , U13^#(tt()) -> c_42() , U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__nil()) -> c_45() , U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , U122^#(tt()) -> c_47(nil^#()) , U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , U23^#(tt()) -> c_57() , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , U33^#(tt()) -> c_60() , U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , U46^#(tt()) -> c_66() , U52^#(tt()) -> c_68() , U62^#(tt()) -> c_70() , U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , U96^#(tt()) -> c_78() } 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() , U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , isNatKind^#(n__0()) -> c_7() , isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , U71^#(tt()) -> c_71() , U81^#(tt()) -> c_72() , 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__nil()) -> c_17(nil^#()) , take^#(X1, X2) -> c_79(X1, X2) , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , length^#(X) -> c_39(X) , length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , length^#(nil()) -> c_41(0^#()) , s^#(X) -> c_38(X) , nil^#() -> c_48() , U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , isNatIListKind^#(n__zeros()) -> c_19() , isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__nil()) -> c_22() , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , U106^#(tt()) -> c_28() , isNat^#(n__0()) -> c_25() , isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_30() , isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , U13^#(tt()) -> c_42() , U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__nil()) -> c_45() , U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , U122^#(tt()) -> c_47(nil^#()) , U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , U23^#(tt()) -> c_57() , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , U33^#(tt()) -> c_60() , U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , U46^#(tt()) -> c_66() , U52^#(tt()) -> c_68() , U62^#(tt()) -> c_70() , U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , U96^#(tt()) -> c_78() } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U101(tt(), V1, V2) -> U102(isNatKind(activate(V1)), activate(V1), activate(V2)) , U102(tt(), V1, V2) -> U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) , 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__nil()) -> nil() , U103(tt(), V1, V2) -> U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__cons(V1, V2)) -> U51(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__nil()) -> tt() , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) , U105(tt(), V2) -> U106(isNatIList(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U106(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) , U12(tt(), V1) -> U13(isNatList(activate(V1))) , U111(tt(), L, N) -> U112(isNatIListKind(activate(L)), activate(L), activate(N)) , U112(tt(), L, N) -> U113(isNat(activate(N)), activate(L), activate(N)) , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) , U114(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U111(isNatList(activate(L)), activate(L), N) , length(nil()) -> 0() , U13(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U101(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U91(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) , U122(tt()) -> nil() , nil() -> n__nil() , U131(tt(), IL, M, N) -> U132(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N)) , U132(tt(), IL, M, N) -> U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) , U133(tt(), IL, M, N) -> U134(isNatKind(activate(M)), activate(IL), activate(M), activate(N)) , U134(tt(), IL, M, N) -> U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) , U135(tt(), IL, M, N) -> U136(isNatKind(activate(N)), activate(IL), activate(M), activate(N)) , U136(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isNatList(activate(V))) , U33(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNatKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNatIList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) , U52(tt()) -> tt() , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) , U62(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt(), V1, V2) -> U92(isNatKind(activate(V1)), activate(V1), activate(V2)) , U92(tt(), V1, V2) -> U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U93(tt(), V1, V2) -> U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) , U95(tt(), V2) -> U96(isNatList(activate(V2))) , U96(tt()) -> tt() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U121(isNatIList(IL), IL) , take(s(M), cons(N, IL)) -> U131(isNatIList(activate(IL)), activate(IL), M, N) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,4,8,11,12,28,30,33,37,38,44,49,56,67,69,74,75,76,81} by applications of Pre({2,4,8,11,12,28,30,33,37,38,44,49,56,67,69,74,75,76,81}) = {3,9,10,13,14,16,20,21,24,26,27,34,35,36,48,59,66,68,73,80}. 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: U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 6: U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 7: U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 8: isNatKind^#(n__0()) -> c_7() , 9: isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , 10: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , 11: U71^#(tt()) -> c_71() , 12: U81^#(tt()) -> c_72() , 13: activate^#(X) -> c_10(X) , 14: activate^#(n__zeros()) -> c_11(zeros^#()) , 15: activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , 16: activate^#(n__0()) -> c_13(0^#()) , 17: activate^#(n__length(X)) -> c_14(length^#(X)) , 18: activate^#(n__s(X)) -> c_15(s^#(X)) , 19: activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , 20: activate^#(n__nil()) -> c_17(nil^#()) , 21: take^#(X1, X2) -> c_79(X1, X2) , 22: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , 23: take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , 24: length^#(X) -> c_39(X) , 25: length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , 26: length^#(nil()) -> c_41(0^#()) , 27: s^#(X) -> c_38(X) , 28: nil^#() -> c_48() , 29: U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , 30: isNatIListKind^#(n__zeros()) -> c_19() , 31: isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , 32: isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , 33: isNatIListKind^#(n__nil()) -> c_22() , 34: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , 35: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , 36: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , 37: U106^#(tt()) -> c_28() , 38: isNat^#(n__0()) -> c_25() , 39: isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 40: isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , 41: U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , 42: U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , 43: isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , 44: isNatIList^#(n__zeros()) -> c_30() , 45: isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 46: U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , 47: U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 48: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , 49: U13^#(tt()) -> c_42() , 50: U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , 51: U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , 52: U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , 53: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , 54: isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 55: isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 56: isNatList^#(n__nil()) -> c_45() , 57: U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 58: U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , 59: U122^#(tt()) -> c_47(nil^#()) , 60: U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , 61: U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , 62: U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , 63: U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , 64: U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , 65: U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 66: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , 67: U23^#(tt()) -> c_57() , 68: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , 69: U33^#(tt()) -> c_60() , 70: U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 71: U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 72: U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , 73: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , 74: U46^#(tt()) -> c_66() , 75: U52^#(tt()) -> c_68() , 76: U62^#(tt()) -> c_70() , 77: U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 78: U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 79: U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , 81: U96^#(tt()) -> c_78() } 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) , U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , 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__nil()) -> c_17(nil^#()) , take^#(X1, X2) -> c_79(X1, X2) , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , length^#(X) -> c_39(X) , length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , length^#(nil()) -> c_41(0^#()) , s^#(X) -> c_38(X) , U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , U122^#(tt()) -> c_47(nil^#()) , U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U101(tt(), V1, V2) -> U102(isNatKind(activate(V1)), activate(V1), activate(V2)) , U102(tt(), V1, V2) -> U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) , 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__nil()) -> nil() , U103(tt(), V1, V2) -> U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__cons(V1, V2)) -> U51(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__nil()) -> tt() , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) , U105(tt(), V2) -> U106(isNatIList(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U106(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) , U12(tt(), V1) -> U13(isNatList(activate(V1))) , U111(tt(), L, N) -> U112(isNatIListKind(activate(L)), activate(L), activate(N)) , U112(tt(), L, N) -> U113(isNat(activate(N)), activate(L), activate(N)) , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) , U114(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U111(isNatList(activate(L)), activate(L), N) , length(nil()) -> 0() , U13(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U101(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U91(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) , U122(tt()) -> nil() , nil() -> n__nil() , U131(tt(), IL, M, N) -> U132(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N)) , U132(tt(), IL, M, N) -> U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) , U133(tt(), IL, M, N) -> U134(isNatKind(activate(M)), activate(IL), activate(M), activate(N)) , U134(tt(), IL, M, N) -> U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) , U135(tt(), IL, M, N) -> U136(isNatKind(activate(N)), activate(IL), activate(M), activate(N)) , U136(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isNatList(activate(V))) , U33(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNatKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNatIList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) , U52(tt()) -> tt() , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) , U62(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt(), V1, V2) -> U92(isNatKind(activate(V1)), activate(V1), activate(V2)) , U92(tt(), V1, V2) -> U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U93(tt(), V1, V2) -> U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) , U95(tt(), V2) -> U96(isNatList(activate(V2))) , U96(tt()) -> tt() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U121(isNatIList(IL), IL) , take(s(M), cons(N, IL)) -> U131(isNatIList(activate(IL)), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , isNatKind^#(n__0()) -> c_7() , U71^#(tt()) -> c_71() , U81^#(tt()) -> c_72() , nil^#() -> c_48() , isNatIListKind^#(n__zeros()) -> c_19() , isNatIListKind^#(n__nil()) -> c_22() , U106^#(tt()) -> c_28() , isNat^#(n__0()) -> c_25() , isNatIList^#(n__zeros()) -> c_30() , U13^#(tt()) -> c_42() , isNatList^#(n__nil()) -> c_45() , U23^#(tt()) -> c_57() , U33^#(tt()) -> c_60() , U46^#(tt()) -> c_66() , U52^#(tt()) -> c_68() , U62^#(tt()) -> c_70() , U96^#(tt()) -> c_78() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {6,7,11,15,21,26,27,28,37,46,53,54,58,62} by applications of Pre({6,7,11,15,21,26,27,28,37,46,53,54,58,62}) = {2,8,12,16,19,22,23,24,25,31,32,35,45,57,61}. Here rules are labeled as follows: DPs: { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) , 2: cons^#(X1, X2) -> c_3(X1, X2) , 3: U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 4: U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 5: U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 6: isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , 7: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , 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__nil()) -> c_17(nil^#()) , 16: take^#(X1, X2) -> c_79(X1, X2) , 17: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , 18: take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , 19: length^#(X) -> c_39(X) , 20: length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , 21: length^#(nil()) -> c_41(0^#()) , 22: s^#(X) -> c_38(X) , 23: U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , 24: isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , 25: isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , 26: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , 27: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , 28: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , 29: isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 30: isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , 31: U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , 32: U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , 33: isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , 34: isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 35: U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , 36: U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 37: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , 38: U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , 39: U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , 40: U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , 41: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , 42: isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 43: isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 44: U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 45: U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , 46: U122^#(tt()) -> c_47(nil^#()) , 47: U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , 48: U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , 49: U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , 50: U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , 51: U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , 52: U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 53: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , 54: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , 55: U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 56: U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 57: U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , 58: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , 59: U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 60: U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 61: U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , 62: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , 63: zeros^#() -> c_2() , 64: 0^#() -> c_4() , 65: isNatKind^#(n__0()) -> c_7() , 66: U71^#(tt()) -> c_71() , 67: U81^#(tt()) -> c_72() , 68: nil^#() -> c_48() , 69: isNatIListKind^#(n__zeros()) -> c_19() , 70: isNatIListKind^#(n__nil()) -> c_22() , 71: U106^#(tt()) -> c_28() , 72: isNat^#(n__0()) -> c_25() , 73: isNatIList^#(n__zeros()) -> c_30() , 74: U13^#(tt()) -> c_42() , 75: isNatList^#(n__nil()) -> c_45() , 76: U23^#(tt()) -> c_57() , 77: U33^#(tt()) -> c_60() , 78: U46^#(tt()) -> c_66() , 79: U52^#(tt()) -> c_68() , 80: U62^#(tt()) -> c_70() , 81: U96^#(tt()) -> c_78() } 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) , U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U103^#(tt(), V1, V2) -> c_18(U104^#(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)) , take^#(X1, X2) -> c_79(X1, X2) , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , length^#(X) -> c_39(X) , length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , s^#(X) -> c_38(X) , U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U101(tt(), V1, V2) -> U102(isNatKind(activate(V1)), activate(V1), activate(V2)) , U102(tt(), V1, V2) -> U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) , 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__nil()) -> nil() , U103(tt(), V1, V2) -> U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__cons(V1, V2)) -> U51(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__nil()) -> tt() , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) , U105(tt(), V2) -> U106(isNatIList(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U106(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) , U12(tt(), V1) -> U13(isNatList(activate(V1))) , U111(tt(), L, N) -> U112(isNatIListKind(activate(L)), activate(L), activate(N)) , U112(tt(), L, N) -> U113(isNat(activate(N)), activate(L), activate(N)) , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) , U114(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U111(isNatList(activate(L)), activate(L), N) , length(nil()) -> 0() , U13(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U101(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U91(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) , U122(tt()) -> nil() , nil() -> n__nil() , U131(tt(), IL, M, N) -> U132(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N)) , U132(tt(), IL, M, N) -> U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) , U133(tt(), IL, M, N) -> U134(isNatKind(activate(M)), activate(IL), activate(M), activate(N)) , U134(tt(), IL, M, N) -> U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) , U135(tt(), IL, M, N) -> U136(isNatKind(activate(N)), activate(IL), activate(M), activate(N)) , U136(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isNatList(activate(V))) , U33(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNatKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNatIList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) , U52(tt()) -> tt() , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) , U62(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt(), V1, V2) -> U92(isNatKind(activate(V1)), activate(V1), activate(V2)) , U92(tt(), V1, V2) -> U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U93(tt(), V1, V2) -> U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) , U95(tt(), V2) -> U96(isNatList(activate(V2))) , U96(tt()) -> tt() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U121(isNatIList(IL), IL) , take(s(M), cons(N, IL)) -> U131(isNatIList(activate(IL)), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , isNatKind^#(n__0()) -> c_7() , isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , U71^#(tt()) -> c_71() , U81^#(tt()) -> c_72() , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__nil()) -> c_17(nil^#()) , length^#(nil()) -> c_41(0^#()) , nil^#() -> c_48() , isNatIListKind^#(n__zeros()) -> c_19() , isNatIListKind^#(n__nil()) -> c_22() , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , U106^#(tt()) -> c_28() , isNat^#(n__0()) -> c_25() , isNatIList^#(n__zeros()) -> c_30() , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , U13^#(tt()) -> c_42() , isNatList^#(n__nil()) -> c_45() , U122^#(tt()) -> c_47(nil^#()) , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , U23^#(tt()) -> c_57() , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , U33^#(tt()) -> c_60() , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , U46^#(tt()) -> c_66() , U52^#(tt()) -> c_68() , U62^#(tt()) -> c_70() , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , U96^#(tt()) -> c_78() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {18,19,20,23,24,27,36,45,48} by applications of Pre({18,19,20,23,24,27,36,45,48}) = {2,5,6,12,13,15,17,21,22,25,44,47}. Here rules are labeled as follows: DPs: { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) , 2: cons^#(X1, X2) -> c_3(X1, X2) , 3: U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 4: U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 5: U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 6: activate^#(X) -> c_10(X) , 7: activate^#(n__zeros()) -> c_11(zeros^#()) , 8: activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , 9: activate^#(n__length(X)) -> c_14(length^#(X)) , 10: activate^#(n__s(X)) -> c_15(s^#(X)) , 11: activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , 12: take^#(X1, X2) -> c_79(X1, X2) , 13: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , 14: take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , 15: length^#(X) -> c_39(X) , 16: length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , 17: s^#(X) -> c_38(X) , 18: U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , 19: isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , 20: isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , 21: isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 22: isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , 23: U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , 24: U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , 25: isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , 26: isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 27: U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , 28: U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 29: U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , 30: U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , 31: U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , 32: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , 33: isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 34: isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 35: U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 36: U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , 37: U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , 38: U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , 39: U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , 40: U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , 41: U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , 42: U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 43: U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 44: U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 45: U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , 46: U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 47: U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 48: U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , 49: zeros^#() -> c_2() , 50: 0^#() -> c_4() , 51: isNatKind^#(n__0()) -> c_7() , 52: isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , 53: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , 54: U71^#(tt()) -> c_71() , 55: U81^#(tt()) -> c_72() , 56: activate^#(n__0()) -> c_13(0^#()) , 57: activate^#(n__nil()) -> c_17(nil^#()) , 58: length^#(nil()) -> c_41(0^#()) , 59: nil^#() -> c_48() , 60: isNatIListKind^#(n__zeros()) -> c_19() , 61: isNatIListKind^#(n__nil()) -> c_22() , 62: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , 63: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , 64: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , 65: U106^#(tt()) -> c_28() , 66: isNat^#(n__0()) -> c_25() , 67: isNatIList^#(n__zeros()) -> c_30() , 68: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , 69: U13^#(tt()) -> c_42() , 70: isNatList^#(n__nil()) -> c_45() , 71: U122^#(tt()) -> c_47(nil^#()) , 72: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , 73: U23^#(tt()) -> c_57() , 74: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , 75: U33^#(tt()) -> c_60() , 76: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , 77: U46^#(tt()) -> c_66() , 78: U52^#(tt()) -> c_68() , 79: U62^#(tt()) -> c_70() , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , 81: U96^#(tt()) -> c_78() } 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) , U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U103^#(tt(), V1, V2) -> c_18(U104^#(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)) , take^#(X1, X2) -> c_79(X1, X2) , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , length^#(X) -> c_39(X) , length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , s^#(X) -> c_38(X) , isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U101(tt(), V1, V2) -> U102(isNatKind(activate(V1)), activate(V1), activate(V2)) , U102(tt(), V1, V2) -> U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) , 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__nil()) -> nil() , U103(tt(), V1, V2) -> U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__cons(V1, V2)) -> U51(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__nil()) -> tt() , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) , U105(tt(), V2) -> U106(isNatIList(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U106(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) , U12(tt(), V1) -> U13(isNatList(activate(V1))) , U111(tt(), L, N) -> U112(isNatIListKind(activate(L)), activate(L), activate(N)) , U112(tt(), L, N) -> U113(isNat(activate(N)), activate(L), activate(N)) , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) , U114(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U111(isNatList(activate(L)), activate(L), N) , length(nil()) -> 0() , U13(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U101(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U91(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) , U122(tt()) -> nil() , nil() -> n__nil() , U131(tt(), IL, M, N) -> U132(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N)) , U132(tt(), IL, M, N) -> U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) , U133(tt(), IL, M, N) -> U134(isNatKind(activate(M)), activate(IL), activate(M), activate(N)) , U134(tt(), IL, M, N) -> U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) , U135(tt(), IL, M, N) -> U136(isNatKind(activate(N)), activate(IL), activate(M), activate(N)) , U136(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isNatList(activate(V))) , U33(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNatKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNatIList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) , U52(tt()) -> tt() , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) , U62(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt(), V1, V2) -> U92(isNatKind(activate(V1)), activate(V1), activate(V2)) , U92(tt(), V1, V2) -> U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U93(tt(), V1, V2) -> U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) , U95(tt(), V2) -> U96(isNatList(activate(V2))) , U96(tt()) -> tt() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U121(isNatIList(IL), IL) , take(s(M), cons(N, IL)) -> U131(isNatIList(activate(IL)), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , isNatKind^#(n__0()) -> c_7() , isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , U71^#(tt()) -> c_71() , U81^#(tt()) -> c_72() , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__nil()) -> c_17(nil^#()) , length^#(nil()) -> c_41(0^#()) , nil^#() -> c_48() , U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , isNatIListKind^#(n__zeros()) -> c_19() , isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__nil()) -> c_22() , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , U106^#(tt()) -> c_28() , isNat^#(n__0()) -> c_25() , U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(n__zeros()) -> c_30() , U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , U13^#(tt()) -> c_42() , isNatList^#(n__nil()) -> c_45() , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , U122^#(tt()) -> c_47(nil^#()) , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , U23^#(tt()) -> c_57() , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , U33^#(tt()) -> c_60() , U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , U46^#(tt()) -> c_66() , U52^#(tt()) -> c_68() , U62^#(tt()) -> c_70() , U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , U96^#(tt()) -> c_78() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {5,13,18,19,20,37,39} by applications of Pre({5,13,18,19,20,37,39}) = {2,4,6,8,12,15,17,36,38}. Here rules are labeled as follows: DPs: { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) , 2: cons^#(X1, X2) -> c_3(X1, X2) , 3: U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 4: U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 5: U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 6: activate^#(X) -> c_10(X) , 7: activate^#(n__zeros()) -> c_11(zeros^#()) , 8: activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , 9: activate^#(n__length(X)) -> c_14(length^#(X)) , 10: activate^#(n__s(X)) -> c_15(s^#(X)) , 11: activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , 12: take^#(X1, X2) -> c_79(X1, X2) , 13: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , 14: take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , 15: length^#(X) -> c_39(X) , 16: length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , 17: s^#(X) -> c_38(X) , 18: isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 19: isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , 20: isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , 21: isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 22: U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 23: U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , 24: U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , 25: U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , 26: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , 27: isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 28: isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 29: U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 30: U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , 31: U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , 32: U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , 33: U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , 34: U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , 35: U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 36: U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 37: U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 38: U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 39: U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 40: zeros^#() -> c_2() , 41: 0^#() -> c_4() , 42: isNatKind^#(n__0()) -> c_7() , 43: isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , 44: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , 45: U71^#(tt()) -> c_71() , 46: U81^#(tt()) -> c_72() , 47: activate^#(n__0()) -> c_13(0^#()) , 48: activate^#(n__nil()) -> c_17(nil^#()) , 49: length^#(nil()) -> c_41(0^#()) , 50: nil^#() -> c_48() , 51: U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , 52: isNatIListKind^#(n__zeros()) -> c_19() , 53: isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , 54: isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , 55: isNatIListKind^#(n__nil()) -> c_22() , 56: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , 57: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , 58: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , 59: U106^#(tt()) -> c_28() , 60: isNat^#(n__0()) -> c_25() , 61: U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , 62: U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , 63: isNatIList^#(n__zeros()) -> c_30() , 64: U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , 65: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , 66: U13^#(tt()) -> c_42() , 67: isNatList^#(n__nil()) -> c_45() , 68: U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , 69: U122^#(tt()) -> c_47(nil^#()) , 70: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , 71: U23^#(tt()) -> c_57() , 72: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , 73: U33^#(tt()) -> c_60() , 74: U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , 75: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , 76: U46^#(tt()) -> c_66() , 77: U52^#(tt()) -> c_68() , 78: U62^#(tt()) -> c_70() , 79: U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , 81: U96^#(tt()) -> c_78() } 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) , U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U102^#(tt(), V1, V2) -> c_6(U103^#(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)) , take^#(X1, X2) -> c_79(X1, X2) , take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , length^#(X) -> c_39(X) , length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , s^#(X) -> c_38(X) , isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) } Strict Trs: { zeros() -> cons(0(), n__zeros()) , zeros() -> n__zeros() , cons(X1, X2) -> n__cons(X1, X2) , 0() -> n__0() , U101(tt(), V1, V2) -> U102(isNatKind(activate(V1)), activate(V1), activate(V2)) , U102(tt(), V1, V2) -> U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) , 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__nil()) -> nil() , U103(tt(), V1, V2) -> U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__cons(V1, V2)) -> U51(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__nil()) -> tt() , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) , U105(tt(), V2) -> U106(isNatIList(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U106(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) , U12(tt(), V1) -> U13(isNatList(activate(V1))) , U111(tt(), L, N) -> U112(isNatIListKind(activate(L)), activate(L), activate(N)) , U112(tt(), L, N) -> U113(isNat(activate(N)), activate(L), activate(N)) , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) , U114(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U111(isNatList(activate(L)), activate(L), N) , length(nil()) -> 0() , U13(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U101(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U91(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) , U122(tt()) -> nil() , nil() -> n__nil() , U131(tt(), IL, M, N) -> U132(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N)) , U132(tt(), IL, M, N) -> U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) , U133(tt(), IL, M, N) -> U134(isNatKind(activate(M)), activate(IL), activate(M), activate(N)) , U134(tt(), IL, M, N) -> U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) , U135(tt(), IL, M, N) -> U136(isNatKind(activate(N)), activate(IL), activate(M), activate(N)) , U136(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isNatList(activate(V))) , U33(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNatKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNatIList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) , U52(tt()) -> tt() , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) , U62(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt(), V1, V2) -> U92(isNatKind(activate(V1)), activate(V1), activate(V2)) , U92(tt(), V1, V2) -> U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U93(tt(), V1, V2) -> U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) , U95(tt(), V2) -> U96(isNatList(activate(V2))) , U96(tt()) -> tt() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U121(isNatIList(IL), IL) , take(s(M), cons(N, IL)) -> U131(isNatIList(activate(IL)), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , isNatKind^#(n__0()) -> c_7() , isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , U71^#(tt()) -> c_71() , U81^#(tt()) -> c_72() , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__nil()) -> c_17(nil^#()) , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , length^#(nil()) -> c_41(0^#()) , nil^#() -> c_48() , U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , isNatIListKind^#(n__zeros()) -> c_19() , isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__nil()) -> c_22() , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , U106^#(tt()) -> c_28() , isNat^#(n__0()) -> c_25() , isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_30() , U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , U13^#(tt()) -> c_42() , isNatList^#(n__nil()) -> c_45() , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , U122^#(tt()) -> c_47(nil^#()) , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , U23^#(tt()) -> c_57() , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , U33^#(tt()) -> c_60() , U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , U46^#(tt()) -> c_66() , U52^#(tt()) -> c_68() , U62^#(tt()) -> c_70() , U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , U96^#(tt()) -> c_78() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {4,31,32} by applications of Pre({4,31,32}) = {2,3,5,11,13,15,17,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: U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 4: U102^#(tt(), V1, V2) -> c_6(U103^#(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: take^#(X1, X2) -> c_79(X1, X2) , 12: take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , 13: length^#(X) -> c_39(X) , 14: length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , 15: s^#(X) -> c_38(X) , 16: isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 17: U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 18: U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , 19: U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , 20: U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , 21: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , 22: isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 23: isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 24: U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 25: U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , 26: U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , 27: U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , 28: U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , 29: U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , 30: U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 31: U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 32: U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 33: zeros^#() -> c_2() , 34: 0^#() -> c_4() , 35: U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 36: isNatKind^#(n__0()) -> c_7() , 37: isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , 38: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , 39: U71^#(tt()) -> c_71() , 40: U81^#(tt()) -> c_72() , 41: activate^#(n__0()) -> c_13(0^#()) , 42: activate^#(n__nil()) -> c_17(nil^#()) , 43: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , 44: length^#(nil()) -> c_41(0^#()) , 45: nil^#() -> c_48() , 46: U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , 47: isNatIListKind^#(n__zeros()) -> c_19() , 48: isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , 49: isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , 50: isNatIListKind^#(n__nil()) -> c_22() , 51: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , 52: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , 53: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , 54: U106^#(tt()) -> c_28() , 55: isNat^#(n__0()) -> c_25() , 56: isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 57: isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , 58: U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , 59: U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , 60: isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , 61: isNatIList^#(n__zeros()) -> c_30() , 62: U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , 63: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , 64: U13^#(tt()) -> c_42() , 65: isNatList^#(n__nil()) -> c_45() , 66: U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , 67: U122^#(tt()) -> c_47(nil^#()) , 68: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , 69: U23^#(tt()) -> c_57() , 70: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , 71: U33^#(tt()) -> c_60() , 72: U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 73: U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , 74: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , 75: U46^#(tt()) -> c_66() , 76: U52^#(tt()) -> c_68() , 77: U62^#(tt()) -> c_70() , 78: U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 79: U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , 81: U96^#(tt()) -> c_78() } 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) , U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), 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)) , take^#(X1, X2) -> c_79(X1, X2) , take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , length^#(X) -> c_39(X) , length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , s^#(X) -> c_38(X) , isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , U136^#(tt(), IL, M, N) -> c_54(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() , U101(tt(), V1, V2) -> U102(isNatKind(activate(V1)), activate(V1), activate(V2)) , U102(tt(), V1, V2) -> U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) , 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__nil()) -> nil() , U103(tt(), V1, V2) -> U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__cons(V1, V2)) -> U51(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__nil()) -> tt() , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) , U105(tt(), V2) -> U106(isNatIList(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U106(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) , U12(tt(), V1) -> U13(isNatList(activate(V1))) , U111(tt(), L, N) -> U112(isNatIListKind(activate(L)), activate(L), activate(N)) , U112(tt(), L, N) -> U113(isNat(activate(N)), activate(L), activate(N)) , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) , U114(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U111(isNatList(activate(L)), activate(L), N) , length(nil()) -> 0() , U13(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U101(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U91(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) , U122(tt()) -> nil() , nil() -> n__nil() , U131(tt(), IL, M, N) -> U132(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N)) , U132(tt(), IL, M, N) -> U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) , U133(tt(), IL, M, N) -> U134(isNatKind(activate(M)), activate(IL), activate(M), activate(N)) , U134(tt(), IL, M, N) -> U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) , U135(tt(), IL, M, N) -> U136(isNatKind(activate(N)), activate(IL), activate(M), activate(N)) , U136(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isNatList(activate(V))) , U33(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNatKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNatIList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) , U52(tt()) -> tt() , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) , U62(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt(), V1, V2) -> U92(isNatKind(activate(V1)), activate(V1), activate(V2)) , U92(tt(), V1, V2) -> U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U93(tt(), V1, V2) -> U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) , U95(tt(), V2) -> U96(isNatList(activate(V2))) , U96(tt()) -> tt() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U121(isNatIList(IL), IL) , take(s(M), cons(N, IL)) -> U131(isNatIList(activate(IL)), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , isNatKind^#(n__0()) -> c_7() , isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , U71^#(tt()) -> c_71() , U81^#(tt()) -> c_72() , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__nil()) -> c_17(nil^#()) , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , length^#(nil()) -> c_41(0^#()) , nil^#() -> c_48() , U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , isNatIListKind^#(n__zeros()) -> c_19() , isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__nil()) -> c_22() , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , U106^#(tt()) -> c_28() , isNat^#(n__0()) -> c_25() , isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_30() , U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , U13^#(tt()) -> c_42() , isNatList^#(n__nil()) -> c_45() , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , U122^#(tt()) -> c_47(nil^#()) , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , U23^#(tt()) -> c_57() , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , U33^#(tt()) -> c_60() , U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , U46^#(tt()) -> c_66() , U52^#(tt()) -> c_68() , U62^#(tt()) -> c_70() , U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , U96^#(tt()) -> c_78() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {3,16,23} by applications of Pre({3,16,23}) = {2,4,10,12,14,15,21,22}. Here rules are labeled as follows: DPs: { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) , 2: cons^#(X1, X2) -> c_3(X1, X2) , 3: U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 4: activate^#(X) -> c_10(X) , 5: activate^#(n__zeros()) -> c_11(zeros^#()) , 6: activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , 7: activate^#(n__length(X)) -> c_14(length^#(X)) , 8: activate^#(n__s(X)) -> c_15(s^#(X)) , 9: activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , 10: take^#(X1, X2) -> c_79(X1, X2) , 11: take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , 12: length^#(X) -> c_39(X) , 13: length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , 14: s^#(X) -> c_38(X) , 15: isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 16: U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 17: U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , 18: U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , 19: U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , 20: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , 21: isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 22: isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 23: U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 24: U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , 25: U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , 26: U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , 27: U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , 28: U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , 29: U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 30: zeros^#() -> c_2() , 31: 0^#() -> c_4() , 32: U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 33: U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 34: isNatKind^#(n__0()) -> c_7() , 35: isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , 36: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , 37: U71^#(tt()) -> c_71() , 38: U81^#(tt()) -> c_72() , 39: activate^#(n__0()) -> c_13(0^#()) , 40: activate^#(n__nil()) -> c_17(nil^#()) , 41: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , 42: length^#(nil()) -> c_41(0^#()) , 43: nil^#() -> c_48() , 44: U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , 45: isNatIListKind^#(n__zeros()) -> c_19() , 46: isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , 47: isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , 48: isNatIListKind^#(n__nil()) -> c_22() , 49: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , 50: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , 51: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , 52: U106^#(tt()) -> c_28() , 53: isNat^#(n__0()) -> c_25() , 54: isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 55: isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , 56: U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , 57: U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , 58: isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , 59: isNatIList^#(n__zeros()) -> c_30() , 60: U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , 61: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , 62: U13^#(tt()) -> c_42() , 63: isNatList^#(n__nil()) -> c_45() , 64: U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , 65: U122^#(tt()) -> c_47(nil^#()) , 66: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , 67: U23^#(tt()) -> c_57() , 68: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , 69: U33^#(tt()) -> c_60() , 70: U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 71: U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 72: U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , 73: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , 74: U46^#(tt()) -> c_66() , 75: U52^#(tt()) -> c_68() , 76: U62^#(tt()) -> c_70() , 77: U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 78: U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 79: U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , 81: U96^#(tt()) -> c_78() } 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)) , take^#(X1, X2) -> c_79(X1, X2) , take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , length^#(X) -> c_39(X) , length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , s^#(X) -> c_38(X) , isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , U136^#(tt(), IL, M, N) -> c_54(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() , U101(tt(), V1, V2) -> U102(isNatKind(activate(V1)), activate(V1), activate(V2)) , U102(tt(), V1, V2) -> U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) , 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__nil()) -> nil() , U103(tt(), V1, V2) -> U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__cons(V1, V2)) -> U51(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__nil()) -> tt() , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) , U105(tt(), V2) -> U106(isNatIList(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U106(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) , U12(tt(), V1) -> U13(isNatList(activate(V1))) , U111(tt(), L, N) -> U112(isNatIListKind(activate(L)), activate(L), activate(N)) , U112(tt(), L, N) -> U113(isNat(activate(N)), activate(L), activate(N)) , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) , U114(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U111(isNatList(activate(L)), activate(L), N) , length(nil()) -> 0() , U13(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U101(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U91(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) , U122(tt()) -> nil() , nil() -> n__nil() , U131(tt(), IL, M, N) -> U132(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N)) , U132(tt(), IL, M, N) -> U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) , U133(tt(), IL, M, N) -> U134(isNatKind(activate(M)), activate(IL), activate(M), activate(N)) , U134(tt(), IL, M, N) -> U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) , U135(tt(), IL, M, N) -> U136(isNatKind(activate(N)), activate(IL), activate(M), activate(N)) , U136(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isNatList(activate(V))) , U33(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNatKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNatIList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) , U52(tt()) -> tt() , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) , U62(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt(), V1, V2) -> U92(isNatKind(activate(V1)), activate(V1), activate(V2)) , U92(tt(), V1, V2) -> U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U93(tt(), V1, V2) -> U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) , U95(tt(), V2) -> U96(isNatList(activate(V2))) , U96(tt()) -> tt() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U121(isNatIList(IL), IL) , take(s(M), cons(N, IL)) -> U131(isNatIList(activate(IL)), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , isNatKind^#(n__0()) -> c_7() , isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , U71^#(tt()) -> c_71() , U81^#(tt()) -> c_72() , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__nil()) -> c_17(nil^#()) , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , length^#(nil()) -> c_41(0^#()) , nil^#() -> c_48() , U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , isNatIListKind^#(n__zeros()) -> c_19() , isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__nil()) -> c_22() , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , U106^#(tt()) -> c_28() , isNat^#(n__0()) -> c_25() , isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_30() , U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , U13^#(tt()) -> c_42() , isNatList^#(n__nil()) -> c_45() , U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , U122^#(tt()) -> c_47(nil^#()) , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , U23^#(tt()) -> c_57() , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , U33^#(tt()) -> c_60() , U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , U46^#(tt()) -> c_66() , U52^#(tt()) -> c_68() , U62^#(tt()) -> c_70() , U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , U96^#(tt()) -> c_78() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {14,19,20} by applications of Pre({14,19,20}) = {2,3,9,11,13}. Here rules are labeled as follows: DPs: { 1: zeros^#() -> c_1(cons^#(0(), n__zeros())) , 2: cons^#(X1, X2) -> c_3(X1, X2) , 3: activate^#(X) -> c_10(X) , 4: activate^#(n__zeros()) -> c_11(zeros^#()) , 5: activate^#(n__take(X1, X2)) -> c_12(take^#(X1, X2)) , 6: activate^#(n__length(X)) -> c_14(length^#(X)) , 7: activate^#(n__s(X)) -> c_15(s^#(X)) , 8: activate^#(n__cons(X1, X2)) -> c_16(cons^#(X1, X2)) , 9: take^#(X1, X2) -> c_79(X1, X2) , 10: take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , 11: length^#(X) -> c_39(X) , 12: length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , 13: s^#(X) -> c_38(X) , 14: isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 15: U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , 16: U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , 17: U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , 18: U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , 19: isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 20: isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 21: U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , 22: U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , 23: U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , 24: U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , 25: U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , 26: U136^#(tt(), IL, M, N) -> c_54(cons^#(activate(N), n__take(activate(M), activate(IL)))) , 27: zeros^#() -> c_2() , 28: 0^#() -> c_4() , 29: U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 30: U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 31: U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 32: isNatKind^#(n__0()) -> c_7() , 33: isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , 34: isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , 35: U71^#(tt()) -> c_71() , 36: U81^#(tt()) -> c_72() , 37: activate^#(n__0()) -> c_13(0^#()) , 38: activate^#(n__nil()) -> c_17(nil^#()) , 39: take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , 40: length^#(nil()) -> c_41(0^#()) , 41: nil^#() -> c_48() , 42: U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , 43: isNatIListKind^#(n__zeros()) -> c_19() , 44: isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , 45: isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , 46: isNatIListKind^#(n__nil()) -> c_22() , 47: U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , 48: U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , 49: U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , 50: U106^#(tt()) -> c_28() , 51: isNat^#(n__0()) -> c_25() , 52: isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , 53: isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , 54: U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , 55: U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , 56: isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , 57: isNatIList^#(n__zeros()) -> c_30() , 58: U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , 59: U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 60: U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , 61: U13^#(tt()) -> c_42() , 62: isNatList^#(n__nil()) -> c_45() , 63: U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , 64: U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , 65: U122^#(tt()) -> c_47(nil^#()) , 66: U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , 67: U23^#(tt()) -> c_57() , 68: U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , 69: U33^#(tt()) -> c_60() , 70: U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 71: U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 72: U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , 73: U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , 74: U46^#(tt()) -> c_66() , 75: U52^#(tt()) -> c_68() , 76: U62^#(tt()) -> c_70() , 77: U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 78: U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , 79: U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , 80: U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , 81: U96^#(tt()) -> c_78() } 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)) , take^#(X1, X2) -> c_79(X1, X2) , take^#(s(M), cons(N, IL)) -> c_81(U131^#(isNatIList(activate(IL)), activate(IL), M, N)) , length^#(X) -> c_39(X) , length^#(cons(N, L)) -> c_40(U111^#(isNatList(activate(L)), activate(L), N)) , s^#(X) -> c_38(X) , U111^#(tt(), L, N) -> c_34(U112^#(isNatIListKind(activate(L)), activate(L), activate(N))) , U112^#(tt(), L, N) -> c_35(U113^#(isNat(activate(N)), activate(L), activate(N))) , U113^#(tt(), L, N) -> c_36(U114^#(isNatKind(activate(N)), activate(L))) , U114^#(tt(), L) -> c_37(s^#(length(activate(L)))) , U131^#(tt(), IL, M, N) -> c_49(U132^#(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N))) , U132^#(tt(), IL, M, N) -> c_50(U133^#(isNat(activate(M)), activate(IL), activate(M), activate(N))) , U133^#(tt(), IL, M, N) -> c_51(U134^#(isNatKind(activate(M)), activate(IL), activate(M), activate(N))) , U134^#(tt(), IL, M, N) -> c_52(U135^#(isNat(activate(N)), activate(IL), activate(M), activate(N))) , U135^#(tt(), IL, M, N) -> c_53(U136^#(isNatKind(activate(N)), activate(IL), activate(M), activate(N))) , U136^#(tt(), IL, M, N) -> c_54(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() , U101(tt(), V1, V2) -> U102(isNatKind(activate(V1)), activate(V1), activate(V2)) , U102(tt(), V1, V2) -> U103(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatKind(n__0()) -> tt() , isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) , isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) , 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__nil()) -> nil() , U103(tt(), V1, V2) -> U104(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , isNatIListKind(n__zeros()) -> tt() , isNatIListKind(n__take(V1, V2)) -> U61(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__cons(V1, V2)) -> U51(isNatKind(activate(V1)), activate(V2)) , isNatIListKind(n__nil()) -> tt() , U104(tt(), V1, V2) -> U105(isNat(activate(V1)), activate(V2)) , U105(tt(), V2) -> U106(isNatIList(activate(V2))) , isNat(n__0()) -> tt() , isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)), activate(V1)) , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)) , U106(tt()) -> tt() , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V)) , isNatIList(n__zeros()) -> tt() , isNatIList(n__cons(V1, V2)) -> U41(isNatKind(activate(V1)), activate(V1), activate(V2)) , U11(tt(), V1) -> U12(isNatIListKind(activate(V1)), activate(V1)) , U12(tt(), V1) -> U13(isNatList(activate(V1))) , U111(tt(), L, N) -> U112(isNatIListKind(activate(L)), activate(L), activate(N)) , U112(tt(), L, N) -> U113(isNat(activate(N)), activate(L), activate(N)) , U113(tt(), L, N) -> U114(isNatKind(activate(N)), activate(L)) , U114(tt(), L) -> s(length(activate(L))) , s(X) -> n__s(X) , length(X) -> n__length(X) , length(cons(N, L)) -> U111(isNatList(activate(L)), activate(L), N) , length(nil()) -> 0() , U13(tt()) -> tt() , isNatList(n__take(V1, V2)) -> U101(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__cons(V1, V2)) -> U91(isNatKind(activate(V1)), activate(V1), activate(V2)) , isNatList(n__nil()) -> tt() , U121(tt(), IL) -> U122(isNatIListKind(activate(IL))) , U122(tt()) -> nil() , nil() -> n__nil() , U131(tt(), IL, M, N) -> U132(isNatIListKind(activate(IL)), activate(IL), activate(M), activate(N)) , U132(tt(), IL, M, N) -> U133(isNat(activate(M)), activate(IL), activate(M), activate(N)) , U133(tt(), IL, M, N) -> U134(isNatKind(activate(M)), activate(IL), activate(M), activate(N)) , U134(tt(), IL, M, N) -> U135(isNat(activate(N)), activate(IL), activate(M), activate(N)) , U135(tt(), IL, M, N) -> U136(isNatKind(activate(N)), activate(IL), activate(M), activate(N)) , U136(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))) , U21(tt(), V1) -> U22(isNatKind(activate(V1)), activate(V1)) , U22(tt(), V1) -> U23(isNat(activate(V1))) , U23(tt()) -> tt() , U31(tt(), V) -> U32(isNatIListKind(activate(V)), activate(V)) , U32(tt(), V) -> U33(isNatList(activate(V))) , U33(tt()) -> tt() , U41(tt(), V1, V2) -> U42(isNatKind(activate(V1)), activate(V1), activate(V2)) , U42(tt(), V1, V2) -> U43(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U43(tt(), V1, V2) -> U44(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U44(tt(), V1, V2) -> U45(isNat(activate(V1)), activate(V2)) , U45(tt(), V2) -> U46(isNatIList(activate(V2))) , U46(tt()) -> tt() , U51(tt(), V2) -> U52(isNatIListKind(activate(V2))) , U52(tt()) -> tt() , U61(tt(), V2) -> U62(isNatIListKind(activate(V2))) , U62(tt()) -> tt() , U71(tt()) -> tt() , U81(tt()) -> tt() , U91(tt(), V1, V2) -> U92(isNatKind(activate(V1)), activate(V1), activate(V2)) , U92(tt(), V1, V2) -> U93(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U93(tt(), V1, V2) -> U94(isNatIListKind(activate(V2)), activate(V1), activate(V2)) , U94(tt(), V1, V2) -> U95(isNat(activate(V1)), activate(V2)) , U95(tt(), V2) -> U96(isNatList(activate(V2))) , U96(tt()) -> tt() , take(X1, X2) -> n__take(X1, X2) , take(0(), IL) -> U121(isNatIList(IL), IL) , take(s(M), cons(N, IL)) -> U131(isNatIList(activate(IL)), activate(IL), M, N) } Weak DPs: { zeros^#() -> c_2() , 0^#() -> c_4() , U101^#(tt(), V1, V2) -> c_5(U102^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U102^#(tt(), V1, V2) -> c_6(U103^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U103^#(tt(), V1, V2) -> c_18(U104^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , isNatKind^#(n__0()) -> c_7() , isNatKind^#(n__length(V1)) -> c_8(U71^#(isNatIListKind(activate(V1)))) , isNatKind^#(n__s(V1)) -> c_9(U81^#(isNatKind(activate(V1)))) , U71^#(tt()) -> c_71() , U81^#(tt()) -> c_72() , activate^#(n__0()) -> c_13(0^#()) , activate^#(n__nil()) -> c_17(nil^#()) , take^#(0(), IL) -> c_80(U121^#(isNatIList(IL), IL)) , length^#(nil()) -> c_41(0^#()) , nil^#() -> c_48() , U104^#(tt(), V1, V2) -> c_23(U105^#(isNat(activate(V1)), activate(V2))) , isNatIListKind^#(n__zeros()) -> c_19() , isNatIListKind^#(n__take(V1, V2)) -> c_20(U61^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__cons(V1, V2)) -> c_21(U51^#(isNatKind(activate(V1)), activate(V2))) , isNatIListKind^#(n__nil()) -> c_22() , U61^#(tt(), V2) -> c_69(U62^#(isNatIListKind(activate(V2)))) , U51^#(tt(), V2) -> c_67(U52^#(isNatIListKind(activate(V2)))) , U105^#(tt(), V2) -> c_24(U106^#(isNatIList(activate(V2)))) , U106^#(tt()) -> c_28() , isNat^#(n__0()) -> c_25() , isNat^#(n__length(V1)) -> c_26(U11^#(isNatIListKind(activate(V1)), activate(V1))) , isNat^#(n__s(V1)) -> c_27(U21^#(isNatKind(activate(V1)), activate(V1))) , U11^#(tt(), V1) -> c_32(U12^#(isNatIListKind(activate(V1)), activate(V1))) , U21^#(tt(), V1) -> c_55(U22^#(isNatKind(activate(V1)), activate(V1))) , isNatIList^#(V) -> c_29(U31^#(isNatIListKind(activate(V)), activate(V))) , isNatIList^#(n__zeros()) -> c_30() , isNatIList^#(n__cons(V1, V2)) -> c_31(U41^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U31^#(tt(), V) -> c_58(U32^#(isNatIListKind(activate(V)), activate(V))) , U41^#(tt(), V1, V2) -> c_61(U42^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U12^#(tt(), V1) -> c_33(U13^#(isNatList(activate(V1)))) , U13^#(tt()) -> c_42() , isNatList^#(n__take(V1, V2)) -> c_43(U101^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__cons(V1, V2)) -> c_44(U91^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , isNatList^#(n__nil()) -> c_45() , U91^#(tt(), V1, V2) -> c_73(U92^#(isNatKind(activate(V1)), activate(V1), activate(V2))) , U121^#(tt(), IL) -> c_46(U122^#(isNatIListKind(activate(IL)))) , U122^#(tt()) -> c_47(nil^#()) , U22^#(tt(), V1) -> c_56(U23^#(isNat(activate(V1)))) , U23^#(tt()) -> c_57() , U32^#(tt(), V) -> c_59(U33^#(isNatList(activate(V)))) , U33^#(tt()) -> c_60() , U42^#(tt(), V1, V2) -> c_62(U43^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U43^#(tt(), V1, V2) -> c_63(U44^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U44^#(tt(), V1, V2) -> c_64(U45^#(isNat(activate(V1)), activate(V2))) , U45^#(tt(), V2) -> c_65(U46^#(isNatIList(activate(V2)))) , U46^#(tt()) -> c_66() , U52^#(tt()) -> c_68() , U62^#(tt()) -> c_70() , U92^#(tt(), V1, V2) -> c_74(U93^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U93^#(tt(), V1, V2) -> c_75(U94^#(isNatIListKind(activate(V2)), activate(V1), activate(V2))) , U94^#(tt(), V1, V2) -> c_76(U95^#(isNat(activate(V1)), activate(V2))) , U95^#(tt(), V2) -> c_77(U96^#(isNatList(activate(V2)))) , U96^#(tt()) -> c_78() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..