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