MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U71(isLNat(XS), XS) , splitAt(s(N), cons(X, XS)) -> U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__fst(X)) -> fst(activate(X)) , activate(n__snd(X)) -> snd(activate(X)) , activate(n__tail(X)) -> tail(activate(X)) , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(activate(X)) , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) , activate(n__splitAt(X1, X2)) -> splitAt(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNatural(X)) -> isNatural(X) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y) , U21(tt(), X) -> activate(X) , U31(tt(), N) -> activate(N) , U41(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U51(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(isNatural(N), n__isLNat(activate(XS))), N) , afterNth(N, XS) -> U11(and(isNatural(N), n__isLNat(XS)), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U61(tt(), Y) -> activate(Y) , U71(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U81(tt(), N, X, XS) -> U82(splitAt(activate(N), activate(XS)), activate(X)) , U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U91(tt(), XS) -> activate(XS) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> isNatural(activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> isLNat(activate(V1)) , isNatural(n__sel(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(n__cons(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(n__fst(V1)) -> isPLNat(activate(V1)) , isLNat(n__snd(V1)) -> isPLNat(activate(V1)) , isLNat(n__tail(V1)) -> isLNat(activate(V1)) , isLNat(n__take(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isPLNat(n__pair(V1, V2)) -> and(isLNat(activate(V1)), n__isLNat(activate(V2))) , isPLNat(n__splitAt(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , natsFrom(N) -> U41(isNatural(N), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U51(and(isNatural(N), n__isLNat(XS)), N, XS) , sel(X1, X2) -> n__sel(X1, X2) , 0() -> n__0() , s(X) -> n__s(X) , tail(X) -> n__tail(X) , tail(cons(N, XS)) -> U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) , take(N, XS) -> U101(and(isNatural(N), n__isLNat(XS)), N, XS) , take(X1, X2) -> n__take(X1, X2) } 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) '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 2) '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 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 perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-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: { U101^#(tt(), N, XS) -> c_1(fst^#(splitAt(activate(N), activate(XS)))) , fst^#(X) -> c_2(X) , fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X)) , U21^#(tt(), X) -> c_28(activate^#(X)) , splitAt^#(X1, X2) -> c_4(X1, X2) , splitAt^#(0(), XS) -> c_5(U71^#(isLNat(XS), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U81^#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))) , U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS))) , U81^#(tt(), N, X, XS) -> c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X))) , activate^#(X) -> c_7(X) , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_9(s^#(activate(X))) , activate^#(n__isLNat(X)) -> c_10(isLNat^#(X)) , activate^#(n__nil()) -> c_11(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_12(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_13(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_14(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_15(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_16(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_17(take^#(activate(X1), activate(X2))) , activate^#(n__0()) -> c_18(0^#()) , activate^#(n__head(X)) -> c_19(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_20(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_21(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_23(and^#(activate(X1), X2)) , activate^#(n__isNatural(X)) -> c_24(isNatural^#(X)) , natsFrom^#(N) -> c_62(U41^#(isNatural(N), N)) , natsFrom^#(X) -> c_63(X) , s^#(X) -> c_67(X) , isLNat^#(X) -> c_51(X) , isLNat^#(n__natsFrom(V1)) -> c_52(isNatural^#(activate(V1))) , isLNat^#(n__nil()) -> c_53() , isLNat^#(n__afterNth(V1, V2)) -> c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , isLNat^#(n__cons(V1, V2)) -> c_55(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , isLNat^#(n__fst(V1)) -> c_56(isPLNat^#(activate(V1))) , isLNat^#(n__snd(V1)) -> c_57(isPLNat^#(activate(V1))) , isLNat^#(n__tail(V1)) -> c_58(isLNat^#(activate(V1))) , isLNat^#(n__take(V1, V2)) -> c_59(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , nil^#() -> c_40() , afterNth^#(N, XS) -> c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , afterNth^#(X1, X2) -> c_36(X1, X2) , cons^#(X1, X2) -> c_31(X1, X2) , snd^#(X) -> c_26(X) , snd^#(pair(X, Y)) -> c_27(U61^#(and(isLNat(X), n__isLNat(Y)), Y)) , tail^#(X) -> c_68(X) , tail^#(cons(N, XS)) -> c_69(U91^#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))) , take^#(N, XS) -> c_70(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , take^#(X1, X2) -> c_71(X1, X2) , 0^#() -> c_66() , head^#(X) -> c_33(X) , head^#(cons(N, XS)) -> c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N)) , sel^#(N, XS) -> c_64(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , sel^#(X1, X2) -> c_65(X1, X2) , pair^#(X1, X2) -> c_39(X1, X2) , and^#(X1, X2) -> c_44(X1, X2) , and^#(tt(), X) -> c_45(activate^#(X)) , isNatural^#(X) -> c_46(X) , isNatural^#(n__s(V1)) -> c_47(isNatural^#(activate(V1))) , isNatural^#(n__0()) -> c_48() , isNatural^#(n__head(V1)) -> c_49(isLNat^#(activate(V1))) , isNatural^#(n__sel(V1, V2)) -> c_50(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , U11^#(tt(), N, XS) -> c_25(snd^#(splitAt(activate(N), activate(XS)))) , U61^#(tt(), Y) -> c_37(activate^#(Y)) , U31^#(tt(), N) -> c_29(activate^#(N)) , U41^#(tt(), N) -> c_30(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U51^#(tt(), N, XS) -> c_32(head^#(afterNth(activate(N), activate(XS)))) , U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS)) , U91^#(tt(), XS) -> c_43(activate^#(XS)) , isPLNat^#(n__pair(V1, V2)) -> c_60(and^#(isLNat(activate(V1)), n__isLNat(activate(V2)))) , isPLNat^#(n__splitAt(V1, V2)) -> c_61(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U101^#(tt(), N, XS) -> c_1(fst^#(splitAt(activate(N), activate(XS)))) , fst^#(X) -> c_2(X) , fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X)) , U21^#(tt(), X) -> c_28(activate^#(X)) , splitAt^#(X1, X2) -> c_4(X1, X2) , splitAt^#(0(), XS) -> c_5(U71^#(isLNat(XS), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U81^#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))) , U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS))) , U81^#(tt(), N, X, XS) -> c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X))) , activate^#(X) -> c_7(X) , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_9(s^#(activate(X))) , activate^#(n__isLNat(X)) -> c_10(isLNat^#(X)) , activate^#(n__nil()) -> c_11(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_12(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_13(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_14(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_15(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_16(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_17(take^#(activate(X1), activate(X2))) , activate^#(n__0()) -> c_18(0^#()) , activate^#(n__head(X)) -> c_19(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_20(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_21(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_23(and^#(activate(X1), X2)) , activate^#(n__isNatural(X)) -> c_24(isNatural^#(X)) , natsFrom^#(N) -> c_62(U41^#(isNatural(N), N)) , natsFrom^#(X) -> c_63(X) , s^#(X) -> c_67(X) , isLNat^#(X) -> c_51(X) , isLNat^#(n__natsFrom(V1)) -> c_52(isNatural^#(activate(V1))) , isLNat^#(n__nil()) -> c_53() , isLNat^#(n__afterNth(V1, V2)) -> c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , isLNat^#(n__cons(V1, V2)) -> c_55(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , isLNat^#(n__fst(V1)) -> c_56(isPLNat^#(activate(V1))) , isLNat^#(n__snd(V1)) -> c_57(isPLNat^#(activate(V1))) , isLNat^#(n__tail(V1)) -> c_58(isLNat^#(activate(V1))) , isLNat^#(n__take(V1, V2)) -> c_59(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , nil^#() -> c_40() , afterNth^#(N, XS) -> c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , afterNth^#(X1, X2) -> c_36(X1, X2) , cons^#(X1, X2) -> c_31(X1, X2) , snd^#(X) -> c_26(X) , snd^#(pair(X, Y)) -> c_27(U61^#(and(isLNat(X), n__isLNat(Y)), Y)) , tail^#(X) -> c_68(X) , tail^#(cons(N, XS)) -> c_69(U91^#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))) , take^#(N, XS) -> c_70(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , take^#(X1, X2) -> c_71(X1, X2) , 0^#() -> c_66() , head^#(X) -> c_33(X) , head^#(cons(N, XS)) -> c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N)) , sel^#(N, XS) -> c_64(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , sel^#(X1, X2) -> c_65(X1, X2) , pair^#(X1, X2) -> c_39(X1, X2) , and^#(X1, X2) -> c_44(X1, X2) , and^#(tt(), X) -> c_45(activate^#(X)) , isNatural^#(X) -> c_46(X) , isNatural^#(n__s(V1)) -> c_47(isNatural^#(activate(V1))) , isNatural^#(n__0()) -> c_48() , isNatural^#(n__head(V1)) -> c_49(isLNat^#(activate(V1))) , isNatural^#(n__sel(V1, V2)) -> c_50(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , U11^#(tt(), N, XS) -> c_25(snd^#(splitAt(activate(N), activate(XS)))) , U61^#(tt(), Y) -> c_37(activate^#(Y)) , U31^#(tt(), N) -> c_29(activate^#(N)) , U41^#(tt(), N) -> c_30(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U51^#(tt(), N, XS) -> c_32(head^#(afterNth(activate(N), activate(XS)))) , U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS)) , U91^#(tt(), XS) -> c_43(activate^#(XS)) , isPLNat^#(n__pair(V1, V2)) -> c_60(and^#(isLNat(activate(V1)), n__isLNat(activate(V2)))) , isPLNat^#(n__splitAt(V1, V2)) -> c_61(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) } Strict Trs: { U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U71(isLNat(XS), XS) , splitAt(s(N), cons(X, XS)) -> U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__fst(X)) -> fst(activate(X)) , activate(n__snd(X)) -> snd(activate(X)) , activate(n__tail(X)) -> tail(activate(X)) , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(activate(X)) , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) , activate(n__splitAt(X1, X2)) -> splitAt(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNatural(X)) -> isNatural(X) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y) , U21(tt(), X) -> activate(X) , U31(tt(), N) -> activate(N) , U41(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U51(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(isNatural(N), n__isLNat(activate(XS))), N) , afterNth(N, XS) -> U11(and(isNatural(N), n__isLNat(XS)), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U61(tt(), Y) -> activate(Y) , U71(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U81(tt(), N, X, XS) -> U82(splitAt(activate(N), activate(XS)), activate(X)) , U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U91(tt(), XS) -> activate(XS) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> isNatural(activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> isLNat(activate(V1)) , isNatural(n__sel(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(n__cons(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(n__fst(V1)) -> isPLNat(activate(V1)) , isLNat(n__snd(V1)) -> isPLNat(activate(V1)) , isLNat(n__tail(V1)) -> isLNat(activate(V1)) , isLNat(n__take(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isPLNat(n__pair(V1, V2)) -> and(isLNat(activate(V1)), n__isLNat(activate(V2))) , isPLNat(n__splitAt(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , natsFrom(N) -> U41(isNatural(N), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U51(and(isNatural(N), n__isLNat(XS)), N, XS) , sel(X1, X2) -> n__sel(X1, X2) , 0() -> n__0() , s(X) -> n__s(X) , tail(X) -> n__tail(X) , tail(cons(N, XS)) -> U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) , take(N, XS) -> U101(and(isNatural(N), n__isLNat(XS)), N, XS) , take(X1, X2) -> n__take(X1, X2) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {33,40,50,60} by applications of Pre({33,40,50,60}) = {2,5,10,13,14,21,27,29,30,31,32,38,42,43,44,46,49,51,54,55,56,58,59,61}. Here rules are labeled as follows: DPs: { 1: U101^#(tt(), N, XS) -> c_1(fst^#(splitAt(activate(N), activate(XS)))) , 2: fst^#(X) -> c_2(X) , 3: fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X)) , 4: U21^#(tt(), X) -> c_28(activate^#(X)) , 5: splitAt^#(X1, X2) -> c_4(X1, X2) , 6: splitAt^#(0(), XS) -> c_5(U71^#(isLNat(XS), XS)) , 7: splitAt^#(s(N), cons(X, XS)) -> c_6(U81^#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))) , 8: U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS))) , 9: U81^#(tt(), N, X, XS) -> c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X))) , 10: activate^#(X) -> c_7(X) , 11: activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(activate(X))) , 12: activate^#(n__s(X)) -> c_9(s^#(activate(X))) , 13: activate^#(n__isLNat(X)) -> c_10(isLNat^#(X)) , 14: activate^#(n__nil()) -> c_11(nil^#()) , 15: activate^#(n__afterNth(X1, X2)) -> c_12(afterNth^#(activate(X1), activate(X2))) , 16: activate^#(n__cons(X1, X2)) -> c_13(cons^#(activate(X1), X2)) , 17: activate^#(n__fst(X)) -> c_14(fst^#(activate(X))) , 18: activate^#(n__snd(X)) -> c_15(snd^#(activate(X))) , 19: activate^#(n__tail(X)) -> c_16(tail^#(activate(X))) , 20: activate^#(n__take(X1, X2)) -> c_17(take^#(activate(X1), activate(X2))) , 21: activate^#(n__0()) -> c_18(0^#()) , 22: activate^#(n__head(X)) -> c_19(head^#(activate(X))) , 23: activate^#(n__sel(X1, X2)) -> c_20(sel^#(activate(X1), activate(X2))) , 24: activate^#(n__pair(X1, X2)) -> c_21(pair^#(activate(X1), activate(X2))) , 25: activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(activate(X1), activate(X2))) , 26: activate^#(n__and(X1, X2)) -> c_23(and^#(activate(X1), X2)) , 27: activate^#(n__isNatural(X)) -> c_24(isNatural^#(X)) , 28: natsFrom^#(N) -> c_62(U41^#(isNatural(N), N)) , 29: natsFrom^#(X) -> c_63(X) , 30: s^#(X) -> c_67(X) , 31: isLNat^#(X) -> c_51(X) , 32: isLNat^#(n__natsFrom(V1)) -> c_52(isNatural^#(activate(V1))) , 33: isLNat^#(n__nil()) -> c_53() , 34: isLNat^#(n__afterNth(V1, V2)) -> c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , 35: isLNat^#(n__cons(V1, V2)) -> c_55(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , 36: isLNat^#(n__fst(V1)) -> c_56(isPLNat^#(activate(V1))) , 37: isLNat^#(n__snd(V1)) -> c_57(isPLNat^#(activate(V1))) , 38: isLNat^#(n__tail(V1)) -> c_58(isLNat^#(activate(V1))) , 39: isLNat^#(n__take(V1, V2)) -> c_59(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , 40: nil^#() -> c_40() , 41: afterNth^#(N, XS) -> c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , 42: afterNth^#(X1, X2) -> c_36(X1, X2) , 43: cons^#(X1, X2) -> c_31(X1, X2) , 44: snd^#(X) -> c_26(X) , 45: snd^#(pair(X, Y)) -> c_27(U61^#(and(isLNat(X), n__isLNat(Y)), Y)) , 46: tail^#(X) -> c_68(X) , 47: tail^#(cons(N, XS)) -> c_69(U91^#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))) , 48: take^#(N, XS) -> c_70(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , 49: take^#(X1, X2) -> c_71(X1, X2) , 50: 0^#() -> c_66() , 51: head^#(X) -> c_33(X) , 52: head^#(cons(N, XS)) -> c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N)) , 53: sel^#(N, XS) -> c_64(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , 54: sel^#(X1, X2) -> c_65(X1, X2) , 55: pair^#(X1, X2) -> c_39(X1, X2) , 56: and^#(X1, X2) -> c_44(X1, X2) , 57: and^#(tt(), X) -> c_45(activate^#(X)) , 58: isNatural^#(X) -> c_46(X) , 59: isNatural^#(n__s(V1)) -> c_47(isNatural^#(activate(V1))) , 60: isNatural^#(n__0()) -> c_48() , 61: isNatural^#(n__head(V1)) -> c_49(isLNat^#(activate(V1))) , 62: isNatural^#(n__sel(V1, V2)) -> c_50(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , 63: U11^#(tt(), N, XS) -> c_25(snd^#(splitAt(activate(N), activate(XS)))) , 64: U61^#(tt(), Y) -> c_37(activate^#(Y)) , 65: U31^#(tt(), N) -> c_29(activate^#(N)) , 66: U41^#(tt(), N) -> c_30(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , 67: U51^#(tt(), N, XS) -> c_32(head^#(afterNth(activate(N), activate(XS)))) , 68: U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS)) , 69: U91^#(tt(), XS) -> c_43(activate^#(XS)) , 70: isPLNat^#(n__pair(V1, V2)) -> c_60(and^#(isLNat(activate(V1)), n__isLNat(activate(V2)))) , 71: isPLNat^#(n__splitAt(V1, V2)) -> c_61(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U101^#(tt(), N, XS) -> c_1(fst^#(splitAt(activate(N), activate(XS)))) , fst^#(X) -> c_2(X) , fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X)) , U21^#(tt(), X) -> c_28(activate^#(X)) , splitAt^#(X1, X2) -> c_4(X1, X2) , splitAt^#(0(), XS) -> c_5(U71^#(isLNat(XS), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U81^#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))) , U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS))) , U81^#(tt(), N, X, XS) -> c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X))) , activate^#(X) -> c_7(X) , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_9(s^#(activate(X))) , activate^#(n__isLNat(X)) -> c_10(isLNat^#(X)) , activate^#(n__nil()) -> c_11(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_12(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_13(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_14(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_15(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_16(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_17(take^#(activate(X1), activate(X2))) , activate^#(n__0()) -> c_18(0^#()) , activate^#(n__head(X)) -> c_19(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_20(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_21(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_23(and^#(activate(X1), X2)) , activate^#(n__isNatural(X)) -> c_24(isNatural^#(X)) , natsFrom^#(N) -> c_62(U41^#(isNatural(N), N)) , natsFrom^#(X) -> c_63(X) , s^#(X) -> c_67(X) , isLNat^#(X) -> c_51(X) , isLNat^#(n__natsFrom(V1)) -> c_52(isNatural^#(activate(V1))) , isLNat^#(n__afterNth(V1, V2)) -> c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , isLNat^#(n__cons(V1, V2)) -> c_55(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , isLNat^#(n__fst(V1)) -> c_56(isPLNat^#(activate(V1))) , isLNat^#(n__snd(V1)) -> c_57(isPLNat^#(activate(V1))) , isLNat^#(n__tail(V1)) -> c_58(isLNat^#(activate(V1))) , isLNat^#(n__take(V1, V2)) -> c_59(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , afterNth^#(N, XS) -> c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , afterNth^#(X1, X2) -> c_36(X1, X2) , cons^#(X1, X2) -> c_31(X1, X2) , snd^#(X) -> c_26(X) , snd^#(pair(X, Y)) -> c_27(U61^#(and(isLNat(X), n__isLNat(Y)), Y)) , tail^#(X) -> c_68(X) , tail^#(cons(N, XS)) -> c_69(U91^#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))) , take^#(N, XS) -> c_70(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , take^#(X1, X2) -> c_71(X1, X2) , head^#(X) -> c_33(X) , head^#(cons(N, XS)) -> c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N)) , sel^#(N, XS) -> c_64(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , sel^#(X1, X2) -> c_65(X1, X2) , pair^#(X1, X2) -> c_39(X1, X2) , and^#(X1, X2) -> c_44(X1, X2) , and^#(tt(), X) -> c_45(activate^#(X)) , isNatural^#(X) -> c_46(X) , isNatural^#(n__s(V1)) -> c_47(isNatural^#(activate(V1))) , isNatural^#(n__head(V1)) -> c_49(isLNat^#(activate(V1))) , isNatural^#(n__sel(V1, V2)) -> c_50(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , U11^#(tt(), N, XS) -> c_25(snd^#(splitAt(activate(N), activate(XS)))) , U61^#(tt(), Y) -> c_37(activate^#(Y)) , U31^#(tt(), N) -> c_29(activate^#(N)) , U41^#(tt(), N) -> c_30(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U51^#(tt(), N, XS) -> c_32(head^#(afterNth(activate(N), activate(XS)))) , U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS)) , U91^#(tt(), XS) -> c_43(activate^#(XS)) , isPLNat^#(n__pair(V1, V2)) -> c_60(and^#(isLNat(activate(V1)), n__isLNat(activate(V2)))) , isPLNat^#(n__splitAt(V1, V2)) -> c_61(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) } Strict Trs: { U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U71(isLNat(XS), XS) , splitAt(s(N), cons(X, XS)) -> U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__fst(X)) -> fst(activate(X)) , activate(n__snd(X)) -> snd(activate(X)) , activate(n__tail(X)) -> tail(activate(X)) , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(activate(X)) , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) , activate(n__splitAt(X1, X2)) -> splitAt(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNatural(X)) -> isNatural(X) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y) , U21(tt(), X) -> activate(X) , U31(tt(), N) -> activate(N) , U41(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U51(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(isNatural(N), n__isLNat(activate(XS))), N) , afterNth(N, XS) -> U11(and(isNatural(N), n__isLNat(XS)), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U61(tt(), Y) -> activate(Y) , U71(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U81(tt(), N, X, XS) -> U82(splitAt(activate(N), activate(XS)), activate(X)) , U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U91(tt(), XS) -> activate(XS) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> isNatural(activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> isLNat(activate(V1)) , isNatural(n__sel(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(n__cons(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(n__fst(V1)) -> isPLNat(activate(V1)) , isLNat(n__snd(V1)) -> isPLNat(activate(V1)) , isLNat(n__tail(V1)) -> isLNat(activate(V1)) , isLNat(n__take(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isPLNat(n__pair(V1, V2)) -> and(isLNat(activate(V1)), n__isLNat(activate(V2))) , isPLNat(n__splitAt(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , natsFrom(N) -> U41(isNatural(N), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U51(and(isNatural(N), n__isLNat(XS)), N, XS) , sel(X1, X2) -> n__sel(X1, X2) , 0() -> n__0() , s(X) -> n__s(X) , tail(X) -> n__tail(X) , tail(cons(N, XS)) -> U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) , take(N, XS) -> U101(and(isNatural(N), n__isLNat(XS)), N, XS) , take(X1, X2) -> n__take(X1, X2) } Weak DPs: { isLNat^#(n__nil()) -> c_53() , nil^#() -> c_40() , 0^#() -> c_66() , isNatural^#(n__0()) -> c_48() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {14,21} by applications of Pre({14,21}) = {2,4,5,10,29,30,31,40,41,42,44,47,48,51,52,53,54,55,60,61,65}. Here rules are labeled as follows: DPs: { 1: U101^#(tt(), N, XS) -> c_1(fst^#(splitAt(activate(N), activate(XS)))) , 2: fst^#(X) -> c_2(X) , 3: fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X)) , 4: U21^#(tt(), X) -> c_28(activate^#(X)) , 5: splitAt^#(X1, X2) -> c_4(X1, X2) , 6: splitAt^#(0(), XS) -> c_5(U71^#(isLNat(XS), XS)) , 7: splitAt^#(s(N), cons(X, XS)) -> c_6(U81^#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))) , 8: U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS))) , 9: U81^#(tt(), N, X, XS) -> c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X))) , 10: activate^#(X) -> c_7(X) , 11: activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(activate(X))) , 12: activate^#(n__s(X)) -> c_9(s^#(activate(X))) , 13: activate^#(n__isLNat(X)) -> c_10(isLNat^#(X)) , 14: activate^#(n__nil()) -> c_11(nil^#()) , 15: activate^#(n__afterNth(X1, X2)) -> c_12(afterNth^#(activate(X1), activate(X2))) , 16: activate^#(n__cons(X1, X2)) -> c_13(cons^#(activate(X1), X2)) , 17: activate^#(n__fst(X)) -> c_14(fst^#(activate(X))) , 18: activate^#(n__snd(X)) -> c_15(snd^#(activate(X))) , 19: activate^#(n__tail(X)) -> c_16(tail^#(activate(X))) , 20: activate^#(n__take(X1, X2)) -> c_17(take^#(activate(X1), activate(X2))) , 21: activate^#(n__0()) -> c_18(0^#()) , 22: activate^#(n__head(X)) -> c_19(head^#(activate(X))) , 23: activate^#(n__sel(X1, X2)) -> c_20(sel^#(activate(X1), activate(X2))) , 24: activate^#(n__pair(X1, X2)) -> c_21(pair^#(activate(X1), activate(X2))) , 25: activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(activate(X1), activate(X2))) , 26: activate^#(n__and(X1, X2)) -> c_23(and^#(activate(X1), X2)) , 27: activate^#(n__isNatural(X)) -> c_24(isNatural^#(X)) , 28: natsFrom^#(N) -> c_62(U41^#(isNatural(N), N)) , 29: natsFrom^#(X) -> c_63(X) , 30: s^#(X) -> c_67(X) , 31: isLNat^#(X) -> c_51(X) , 32: isLNat^#(n__natsFrom(V1)) -> c_52(isNatural^#(activate(V1))) , 33: isLNat^#(n__afterNth(V1, V2)) -> c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , 34: isLNat^#(n__cons(V1, V2)) -> c_55(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , 35: isLNat^#(n__fst(V1)) -> c_56(isPLNat^#(activate(V1))) , 36: isLNat^#(n__snd(V1)) -> c_57(isPLNat^#(activate(V1))) , 37: isLNat^#(n__tail(V1)) -> c_58(isLNat^#(activate(V1))) , 38: isLNat^#(n__take(V1, V2)) -> c_59(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , 39: afterNth^#(N, XS) -> c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , 40: afterNth^#(X1, X2) -> c_36(X1, X2) , 41: cons^#(X1, X2) -> c_31(X1, X2) , 42: snd^#(X) -> c_26(X) , 43: snd^#(pair(X, Y)) -> c_27(U61^#(and(isLNat(X), n__isLNat(Y)), Y)) , 44: tail^#(X) -> c_68(X) , 45: tail^#(cons(N, XS)) -> c_69(U91^#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))) , 46: take^#(N, XS) -> c_70(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , 47: take^#(X1, X2) -> c_71(X1, X2) , 48: head^#(X) -> c_33(X) , 49: head^#(cons(N, XS)) -> c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N)) , 50: sel^#(N, XS) -> c_64(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , 51: sel^#(X1, X2) -> c_65(X1, X2) , 52: pair^#(X1, X2) -> c_39(X1, X2) , 53: and^#(X1, X2) -> c_44(X1, X2) , 54: and^#(tt(), X) -> c_45(activate^#(X)) , 55: isNatural^#(X) -> c_46(X) , 56: isNatural^#(n__s(V1)) -> c_47(isNatural^#(activate(V1))) , 57: isNatural^#(n__head(V1)) -> c_49(isLNat^#(activate(V1))) , 58: isNatural^#(n__sel(V1, V2)) -> c_50(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , 59: U11^#(tt(), N, XS) -> c_25(snd^#(splitAt(activate(N), activate(XS)))) , 60: U61^#(tt(), Y) -> c_37(activate^#(Y)) , 61: U31^#(tt(), N) -> c_29(activate^#(N)) , 62: U41^#(tt(), N) -> c_30(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , 63: U51^#(tt(), N, XS) -> c_32(head^#(afterNth(activate(N), activate(XS)))) , 64: U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS)) , 65: U91^#(tt(), XS) -> c_43(activate^#(XS)) , 66: isPLNat^#(n__pair(V1, V2)) -> c_60(and^#(isLNat(activate(V1)), n__isLNat(activate(V2)))) , 67: isPLNat^#(n__splitAt(V1, V2)) -> c_61(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , 68: isLNat^#(n__nil()) -> c_53() , 69: nil^#() -> c_40() , 70: 0^#() -> c_66() , 71: isNatural^#(n__0()) -> c_48() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U101^#(tt(), N, XS) -> c_1(fst^#(splitAt(activate(N), activate(XS)))) , fst^#(X) -> c_2(X) , fst^#(pair(X, Y)) -> c_3(U21^#(and(isLNat(X), n__isLNat(Y)), X)) , U21^#(tt(), X) -> c_28(activate^#(X)) , splitAt^#(X1, X2) -> c_4(X1, X2) , splitAt^#(0(), XS) -> c_5(U71^#(isLNat(XS), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_6(U81^#(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS))) , U71^#(tt(), XS) -> c_38(pair^#(nil(), activate(XS))) , U81^#(tt(), N, X, XS) -> c_41(U82^#(splitAt(activate(N), activate(XS)), activate(X))) , activate^#(X) -> c_7(X) , activate^#(n__natsFrom(X)) -> c_8(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_9(s^#(activate(X))) , activate^#(n__isLNat(X)) -> c_10(isLNat^#(X)) , activate^#(n__afterNth(X1, X2)) -> c_12(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_13(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_14(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_15(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_16(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_17(take^#(activate(X1), activate(X2))) , activate^#(n__head(X)) -> c_19(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_20(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_21(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_22(splitAt^#(activate(X1), activate(X2))) , activate^#(n__and(X1, X2)) -> c_23(and^#(activate(X1), X2)) , activate^#(n__isNatural(X)) -> c_24(isNatural^#(X)) , natsFrom^#(N) -> c_62(U41^#(isNatural(N), N)) , natsFrom^#(X) -> c_63(X) , s^#(X) -> c_67(X) , isLNat^#(X) -> c_51(X) , isLNat^#(n__natsFrom(V1)) -> c_52(isNatural^#(activate(V1))) , isLNat^#(n__afterNth(V1, V2)) -> c_54(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , isLNat^#(n__cons(V1, V2)) -> c_55(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , isLNat^#(n__fst(V1)) -> c_56(isPLNat^#(activate(V1))) , isLNat^#(n__snd(V1)) -> c_57(isPLNat^#(activate(V1))) , isLNat^#(n__tail(V1)) -> c_58(isLNat^#(activate(V1))) , isLNat^#(n__take(V1, V2)) -> c_59(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , afterNth^#(N, XS) -> c_35(U11^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , afterNth^#(X1, X2) -> c_36(X1, X2) , cons^#(X1, X2) -> c_31(X1, X2) , snd^#(X) -> c_26(X) , snd^#(pair(X, Y)) -> c_27(U61^#(and(isLNat(X), n__isLNat(Y)), Y)) , tail^#(X) -> c_68(X) , tail^#(cons(N, XS)) -> c_69(U91^#(and(isNatural(N), n__isLNat(activate(XS))), activate(XS))) , take^#(N, XS) -> c_70(U101^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , take^#(X1, X2) -> c_71(X1, X2) , head^#(X) -> c_33(X) , head^#(cons(N, XS)) -> c_34(U31^#(and(isNatural(N), n__isLNat(activate(XS))), N)) , sel^#(N, XS) -> c_64(U51^#(and(isNatural(N), n__isLNat(XS)), N, XS)) , sel^#(X1, X2) -> c_65(X1, X2) , pair^#(X1, X2) -> c_39(X1, X2) , and^#(X1, X2) -> c_44(X1, X2) , and^#(tt(), X) -> c_45(activate^#(X)) , isNatural^#(X) -> c_46(X) , isNatural^#(n__s(V1)) -> c_47(isNatural^#(activate(V1))) , isNatural^#(n__head(V1)) -> c_49(isLNat^#(activate(V1))) , isNatural^#(n__sel(V1, V2)) -> c_50(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) , U11^#(tt(), N, XS) -> c_25(snd^#(splitAt(activate(N), activate(XS)))) , U61^#(tt(), Y) -> c_37(activate^#(Y)) , U31^#(tt(), N) -> c_29(activate^#(N)) , U41^#(tt(), N) -> c_30(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U51^#(tt(), N, XS) -> c_32(head^#(afterNth(activate(N), activate(XS)))) , U82^#(pair(YS, ZS), X) -> c_42(pair^#(cons(activate(X), YS), ZS)) , U91^#(tt(), XS) -> c_43(activate^#(XS)) , isPLNat^#(n__pair(V1, V2)) -> c_60(and^#(isLNat(activate(V1)), n__isLNat(activate(V2)))) , isPLNat^#(n__splitAt(V1, V2)) -> c_61(and^#(isNatural(activate(V1)), n__isLNat(activate(V2)))) } Strict Trs: { U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U71(isLNat(XS), XS) , splitAt(s(N), cons(X, XS)) -> U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N, X, activate(XS)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__nil()) -> nil() , activate(n__afterNth(X1, X2)) -> afterNth(activate(X1), activate(X2)) , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) , activate(n__fst(X)) -> fst(activate(X)) , activate(n__snd(X)) -> snd(activate(X)) , activate(n__tail(X)) -> tail(activate(X)) , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) , activate(n__0()) -> 0() , activate(n__head(X)) -> head(activate(X)) , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) , activate(n__splitAt(X1, X2)) -> splitAt(activate(X1), activate(X2)) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isNatural(X)) -> isNatural(X) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y) , U21(tt(), X) -> activate(X) , U31(tt(), N) -> activate(N) , U41(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U51(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(isNatural(N), n__isLNat(activate(XS))), N) , afterNth(N, XS) -> U11(and(isNatural(N), n__isLNat(XS)), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U61(tt(), Y) -> activate(Y) , U71(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U81(tt(), N, X, XS) -> U82(splitAt(activate(N), activate(XS)), activate(X)) , U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U91(tt(), XS) -> activate(XS) , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> isNatural(activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> isLNat(activate(V1)) , isNatural(n__sel(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(n__cons(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isLNat(n__fst(V1)) -> isPLNat(activate(V1)) , isLNat(n__snd(V1)) -> isPLNat(activate(V1)) , isLNat(n__tail(V1)) -> isLNat(activate(V1)) , isLNat(n__take(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , isPLNat(n__pair(V1, V2)) -> and(isLNat(activate(V1)), n__isLNat(activate(V2))) , isPLNat(n__splitAt(V1, V2)) -> and(isNatural(activate(V1)), n__isLNat(activate(V2))) , natsFrom(N) -> U41(isNatural(N), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U51(and(isNatural(N), n__isLNat(XS)), N, XS) , sel(X1, X2) -> n__sel(X1, X2) , 0() -> n__0() , s(X) -> n__s(X) , tail(X) -> n__tail(X) , tail(cons(N, XS)) -> U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)) , take(N, XS) -> U101(and(isNatural(N), n__isLNat(XS)), N, XS) , take(X1, X2) -> n__take(X1, X2) } Weak DPs: { activate^#(n__nil()) -> c_11(nil^#()) , activate^#(n__0()) -> c_18(0^#()) , isLNat^#(n__nil()) -> c_53() , nil^#() -> c_40() , 0^#() -> c_66() , isNatural^#(n__0()) -> c_48() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..