MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2)) , U102(tt(), V2) -> U103(isLNat(activate(V2))) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)), activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)), activate(V1)) , isNatural(n__sel(V1, V2)) -> U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isNaturalKind(X)) -> isNaturalKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__isLNatKind(X)) -> isLNatKind(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__isNatural(X)) -> isNatural(X) , U103(tt()) -> tt() , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)), activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)), activate(V1)) , isLNat(n__take(V1, V2)) -> U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS) , splitAt(s(N), cons(X, XS)) -> U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS)) , U111(tt(), V1) -> U112(isLNat(activate(V1))) , U112(tt()) -> tt() , U121(tt(), V1) -> U122(isNatural(activate(V1))) , U122(tt()) -> tt() , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2)) , U132(tt(), V2) -> U133(isLNat(activate(V2))) , U133(tt()) -> tt() , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2)) , U142(tt(), V2) -> U143(isLNat(activate(V2))) , U143(tt()) -> tt() , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2)) , U152(tt(), V2) -> U153(isLNat(activate(V2))) , U153(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) , afterNth(N, XS) -> U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(splitAt(activate(N), activate(XS)), activate(X)) , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X) -> activate(X) , U211(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X) , U31(tt(), N) -> activate(N) , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isLNat(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isLNat(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1) -> U62(isPLNat(activate(V1))) , U62(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U71(tt(), V1) -> U72(isNatural(activate(V1))) , U72(tt()) -> tt() , U81(tt(), V1) -> U82(isPLNat(activate(V1))) , U82(tt()) -> tt() , U91(tt(), V1) -> U92(isLNat(activate(V1))) , U92(tt()) -> tt() , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNaturalKind(X) -> n__isNaturalKind(X) , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) , isNaturalKind(n__0()) -> tt() , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) , isNaturalKind(n__sel(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__pair(V1, V2)) -> and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__splitAt(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(X) -> n__isLNatKind(X) , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) , isLNatKind(n__nil()) -> tt() , isLNatKind(n__afterNth(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__cons(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) , isLNatKind(n__take(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(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)) -> U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) , take(N, XS) -> U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(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) '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(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , U103^#(tt()) -> c_28() , isNatural^#(X) -> c_3(X) , isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , isNatural^#(n__0()) -> c_5() , isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_10(s^#(activate(X))) , activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , activate^#(n__nil()) -> c_15(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , activate^#(n__0()) -> c_22(0^#()) , activate^#(n__head(X)) -> c_23(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , natsFrom^#(X) -> c_111(X) , s^#(X) -> c_115(X) , isNaturalKind^#(X) -> c_94(X) , isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , isNaturalKind^#(n__0()) -> c_96() , isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , and^#(X1, X2) -> c_92(X1, X2) , and^#(tt(), X) -> c_93(activate^#(X)) , isLNat^#(X) -> c_29(X) , isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , isLNat^#(n__nil()) -> c_31() , isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNatKind^#(X) -> c_101(X) , isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , isLNatKind^#(n__nil()) -> c_103() , isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , nil^#() -> c_67() , afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , afterNth^#(X1, X2) -> c_63(X1, X2) , cons^#(X1, X2) -> c_58(X1, X2) , fst^#(X) -> c_73(X) , fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , snd^#(X) -> c_39(X) , snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , tail^#(X) -> c_116(X) , tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , take^#(X1, X2) -> c_119(X1, X2) , 0^#() -> c_114() , head^#(X) -> c_60(X) , head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , sel^#(X1, X2) -> c_113(X1, X2) , pair^#(X1, X2) -> c_66(X1, X2) , splitAt^#(X1, X2) -> c_41(X1, X2) , splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , U181^#(tt(), Y) -> c_64(activate^#(Y)) , U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , U112^#(tt()) -> c_45() , U122^#(tt()) -> c_47() , U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , U133^#(tt()) -> c_50() , U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , U143^#(tt()) -> c_53() , U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , U153^#(tt()) -> c_56() , U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N) -> c_75(activate^#(N)) , U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X) -> c_70(activate^#(X)) , U211^#(tt(), XS) -> c_71(activate^#(XS)) , U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , U43^#(tt()) -> c_78() , U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , U53^#(tt()) -> c_81() , U62^#(tt()) -> c_83() , isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , U72^#(tt()) -> c_87() , U82^#(tt()) -> c_89() , U92^#(tt()) -> c_91() , isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(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(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , U103^#(tt()) -> c_28() , isNatural^#(X) -> c_3(X) , isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , isNatural^#(n__0()) -> c_5() , isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_10(s^#(activate(X))) , activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , activate^#(n__nil()) -> c_15(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , activate^#(n__0()) -> c_22(0^#()) , activate^#(n__head(X)) -> c_23(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , natsFrom^#(X) -> c_111(X) , s^#(X) -> c_115(X) , isNaturalKind^#(X) -> c_94(X) , isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , isNaturalKind^#(n__0()) -> c_96() , isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , and^#(X1, X2) -> c_92(X1, X2) , and^#(tt(), X) -> c_93(activate^#(X)) , isLNat^#(X) -> c_29(X) , isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , isLNat^#(n__nil()) -> c_31() , isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNatKind^#(X) -> c_101(X) , isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , isLNatKind^#(n__nil()) -> c_103() , isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , nil^#() -> c_67() , afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , afterNth^#(X1, X2) -> c_63(X1, X2) , cons^#(X1, X2) -> c_58(X1, X2) , fst^#(X) -> c_73(X) , fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , snd^#(X) -> c_39(X) , snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , tail^#(X) -> c_116(X) , tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , take^#(X1, X2) -> c_119(X1, X2) , 0^#() -> c_114() , head^#(X) -> c_60(X) , head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , sel^#(X1, X2) -> c_113(X1, X2) , pair^#(X1, X2) -> c_66(X1, X2) , splitAt^#(X1, X2) -> c_41(X1, X2) , splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , U181^#(tt(), Y) -> c_64(activate^#(Y)) , U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , U112^#(tt()) -> c_45() , U122^#(tt()) -> c_47() , U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , U133^#(tt()) -> c_50() , U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , U143^#(tt()) -> c_53() , U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , U153^#(tt()) -> c_56() , U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N) -> c_75(activate^#(N)) , U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X) -> c_70(activate^#(X)) , U211^#(tt(), XS) -> c_71(activate^#(XS)) , U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , U43^#(tt()) -> c_78() , U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , U53^#(tt()) -> c_81() , U62^#(tt()) -> c_83() , isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , U72^#(tt()) -> c_87() , U82^#(tt()) -> c_89() , U92^#(tt()) -> c_91() , isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) } Strict Trs: { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2)) , U102(tt(), V2) -> U103(isLNat(activate(V2))) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)), activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)), activate(V1)) , isNatural(n__sel(V1, V2)) -> U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isNaturalKind(X)) -> isNaturalKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__isLNatKind(X)) -> isLNatKind(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__isNatural(X)) -> isNatural(X) , U103(tt()) -> tt() , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)), activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)), activate(V1)) , isLNat(n__take(V1, V2)) -> U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS) , splitAt(s(N), cons(X, XS)) -> U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS)) , U111(tt(), V1) -> U112(isLNat(activate(V1))) , U112(tt()) -> tt() , U121(tt(), V1) -> U122(isNatural(activate(V1))) , U122(tt()) -> tt() , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2)) , U132(tt(), V2) -> U133(isLNat(activate(V2))) , U133(tt()) -> tt() , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2)) , U142(tt(), V2) -> U143(isLNat(activate(V2))) , U143(tt()) -> tt() , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2)) , U152(tt(), V2) -> U153(isLNat(activate(V2))) , U153(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) , afterNth(N, XS) -> U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(splitAt(activate(N), activate(XS)), activate(X)) , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X) -> activate(X) , U211(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X) , U31(tt(), N) -> activate(N) , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isLNat(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isLNat(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1) -> U62(isPLNat(activate(V1))) , U62(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U71(tt(), V1) -> U72(isNatural(activate(V1))) , U72(tt()) -> tt() , U81(tt(), V1) -> U82(isPLNat(activate(V1))) , U82(tt()) -> tt() , U91(tt(), V1) -> U92(isLNat(activate(V1))) , U92(tt()) -> tt() , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNaturalKind(X) -> n__isNaturalKind(X) , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) , isNaturalKind(n__0()) -> tt() , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) , isNaturalKind(n__sel(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__pair(V1, V2)) -> and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__splitAt(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(X) -> n__isLNatKind(X) , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) , isLNatKind(n__nil()) -> tt() , isLNatKind(n__afterNth(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__cons(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) , isLNatKind(n__take(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(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)) -> U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) , take(N, XS) -> U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , take(X1, X2) -> n__take(X1, X2) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {3,6,37,44,53,60,72,91,92,94,97,100,109,111,112,115,116,117} by applications of Pre({3,6,37,44,53,60,72,91,92,94,97,100,109,111,112,115,116,117}) = {2,4,9,10,12,15,17,18,19,26,31,33,34,35,36,38,40,42,51,52,58,62,63,64,66,68,71,73,76,77,78,81,84,85,86,93,96,99,108,110}. Here rules are labeled as follows: DPs: { 1: U101^#(tt(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , 2: U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , 3: U103^#(tt()) -> c_28() , 4: isNatural^#(X) -> c_3(X) , 5: isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , 6: isNatural^#(n__0()) -> c_5() , 7: isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , 8: isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 9: U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , 10: U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , 11: U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , 12: activate^#(X) -> c_8(X) , 13: activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , 14: activate^#(n__s(X)) -> c_10(s^#(activate(X))) , 15: activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , 16: activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , 17: activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , 18: activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , 19: activate^#(n__nil()) -> c_15(nil^#()) , 20: activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , 21: activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , 22: activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , 23: activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , 24: activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , 25: activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , 26: activate^#(n__0()) -> c_22(0^#()) , 27: activate^#(n__head(X)) -> c_23(head^#(activate(X))) , 28: activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , 29: activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , 30: activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , 31: activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , 32: natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , 33: natsFrom^#(X) -> c_111(X) , 34: s^#(X) -> c_115(X) , 35: isNaturalKind^#(X) -> c_94(X) , 36: isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , 37: isNaturalKind^#(n__0()) -> c_96() , 38: isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , 39: isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 40: and^#(X1, X2) -> c_92(X1, X2) , 41: and^#(tt(), X) -> c_93(activate^#(X)) , 42: isLNat^#(X) -> c_29(X) , 43: isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , 44: isLNat^#(n__nil()) -> c_31() , 45: isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 46: isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 47: isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , 48: isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , 49: isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , 50: isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 51: isLNatKind^#(X) -> c_101(X) , 52: isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , 53: isLNatKind^#(n__nil()) -> c_103() , 54: isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 55: isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 56: isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , 57: isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , 58: isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , 59: isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 60: nil^#() -> c_67() , 61: afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 62: afterNth^#(X1, X2) -> c_63(X1, X2) , 63: cons^#(X1, X2) -> c_58(X1, X2) , 64: fst^#(X) -> c_73(X) , 65: fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , 66: snd^#(X) -> c_39(X) , 67: snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , 68: tail^#(X) -> c_116(X) , 69: tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , 70: take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 71: take^#(X1, X2) -> c_119(X1, X2) , 72: 0^#() -> c_114() , 73: head^#(X) -> c_60(X) , 74: head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , 75: sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 76: sel^#(X1, X2) -> c_113(X1, X2) , 77: pair^#(X1, X2) -> c_66(X1, X2) , 78: splitAt^#(X1, X2) -> c_41(X1, X2) , 79: splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , 80: splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , 81: U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , 82: U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , 83: U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , 84: U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , 85: U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , 86: U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , 87: U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , 88: U181^#(tt(), Y) -> c_64(activate^#(Y)) , 89: U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , 90: U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , 91: U112^#(tt()) -> c_45() , 92: U122^#(tt()) -> c_47() , 93: U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , 94: U133^#(tt()) -> c_50() , 95: U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , 96: U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , 97: U143^#(tt()) -> c_53() , 98: U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , 99: U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , 100: U153^#(tt()) -> c_56() , 101: U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , 102: U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , 103: U31^#(tt(), N) -> c_75(activate^#(N)) , 104: U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , 105: U21^#(tt(), X) -> c_70(activate^#(X)) , 106: U211^#(tt(), XS) -> c_71(activate^#(XS)) , 107: U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , 108: U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , 109: U43^#(tt()) -> c_78() , 110: U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , 111: U53^#(tt()) -> c_81() , 112: U62^#(tt()) -> c_83() , 113: isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 114: isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 115: U72^#(tt()) -> c_87() , 116: U82^#(tt()) -> c_89() , 117: U92^#(tt()) -> c_91() , 118: isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , 119: isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U101^#(tt(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , isNatural^#(X) -> c_3(X) , isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_10(s^#(activate(X))) , activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , activate^#(n__nil()) -> c_15(nil^#()) , activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , activate^#(n__0()) -> c_22(0^#()) , activate^#(n__head(X)) -> c_23(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , natsFrom^#(X) -> c_111(X) , s^#(X) -> c_115(X) , isNaturalKind^#(X) -> c_94(X) , isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , and^#(X1, X2) -> c_92(X1, X2) , and^#(tt(), X) -> c_93(activate^#(X)) , isLNat^#(X) -> c_29(X) , isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNatKind^#(X) -> c_101(X) , isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , afterNth^#(X1, X2) -> c_63(X1, X2) , cons^#(X1, X2) -> c_58(X1, X2) , fst^#(X) -> c_73(X) , fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , snd^#(X) -> c_39(X) , snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , tail^#(X) -> c_116(X) , tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , take^#(X1, X2) -> c_119(X1, X2) , head^#(X) -> c_60(X) , head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , sel^#(X1, X2) -> c_113(X1, X2) , pair^#(X1, X2) -> c_66(X1, X2) , splitAt^#(X1, X2) -> c_41(X1, X2) , splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , U181^#(tt(), Y) -> c_64(activate^#(Y)) , U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N) -> c_75(activate^#(N)) , U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X) -> c_70(activate^#(X)) , U211^#(tt(), XS) -> c_71(activate^#(XS)) , U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) } Strict Trs: { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2)) , U102(tt(), V2) -> U103(isLNat(activate(V2))) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)), activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)), activate(V1)) , isNatural(n__sel(V1, V2)) -> U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isNaturalKind(X)) -> isNaturalKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__isLNatKind(X)) -> isLNatKind(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__isNatural(X)) -> isNatural(X) , U103(tt()) -> tt() , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)), activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)), activate(V1)) , isLNat(n__take(V1, V2)) -> U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS) , splitAt(s(N), cons(X, XS)) -> U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS)) , U111(tt(), V1) -> U112(isLNat(activate(V1))) , U112(tt()) -> tt() , U121(tt(), V1) -> U122(isNatural(activate(V1))) , U122(tt()) -> tt() , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2)) , U132(tt(), V2) -> U133(isLNat(activate(V2))) , U133(tt()) -> tt() , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2)) , U142(tt(), V2) -> U143(isLNat(activate(V2))) , U143(tt()) -> tt() , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2)) , U152(tt(), V2) -> U153(isLNat(activate(V2))) , U153(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) , afterNth(N, XS) -> U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(splitAt(activate(N), activate(XS)), activate(X)) , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X) -> activate(X) , U211(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X) , U31(tt(), N) -> activate(N) , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isLNat(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isLNat(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1) -> U62(isPLNat(activate(V1))) , U62(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U71(tt(), V1) -> U72(isNatural(activate(V1))) , U72(tt()) -> tt() , U81(tt(), V1) -> U82(isPLNat(activate(V1))) , U82(tt()) -> tt() , U91(tt(), V1) -> U92(isLNat(activate(V1))) , U92(tt()) -> tt() , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNaturalKind(X) -> n__isNaturalKind(X) , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) , isNaturalKind(n__0()) -> tt() , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) , isNaturalKind(n__sel(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__pair(V1, V2)) -> and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__splitAt(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(X) -> n__isLNatKind(X) , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) , isLNatKind(n__nil()) -> tt() , isLNatKind(n__afterNth(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__cons(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) , isLNatKind(n__take(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(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)) -> U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) , take(N, XS) -> U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , take(X1, X2) -> n__take(X1, X2) } Weak DPs: { U103^#(tt()) -> c_28() , isNatural^#(n__0()) -> c_5() , isNaturalKind^#(n__0()) -> c_96() , isLNat^#(n__nil()) -> c_31() , isLNatKind^#(n__nil()) -> c_103() , nil^#() -> c_67() , 0^#() -> c_114() , U112^#(tt()) -> c_45() , U122^#(tt()) -> c_47() , U133^#(tt()) -> c_50() , U143^#(tt()) -> c_53() , U153^#(tt()) -> c_56() , U43^#(tt()) -> c_78() , U53^#(tt()) -> c_81() , U62^#(tt()) -> c_83() , U72^#(tt()) -> c_87() , U82^#(tt()) -> c_89() , U92^#(tt()) -> c_91() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,7,8,17,24,74,77,78,79,84,86,88,96,97} by applications of Pre({2,7,8,17,24,74,77,78,79,84,86,88,96,97}) = {1,3,4,5,9,10,31,32,33,37,38,39,40,43,44,45,47,56,57,58,60,62,65,66,69,70,71,75,76,81,85,87,91,93,94}. Here rules are labeled as follows: DPs: { 1: U101^#(tt(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , 2: U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , 3: isNatural^#(X) -> c_3(X) , 4: isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , 5: isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , 6: isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 7: U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , 8: U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , 9: U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , 10: activate^#(X) -> c_8(X) , 11: activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , 12: activate^#(n__s(X)) -> c_10(s^#(activate(X))) , 13: activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , 14: activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , 15: activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , 16: activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , 17: activate^#(n__nil()) -> c_15(nil^#()) , 18: activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , 19: activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , 20: activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , 21: activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , 22: activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , 23: activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , 24: activate^#(n__0()) -> c_22(0^#()) , 25: activate^#(n__head(X)) -> c_23(head^#(activate(X))) , 26: activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , 27: activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , 28: activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , 29: activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , 30: natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , 31: natsFrom^#(X) -> c_111(X) , 32: s^#(X) -> c_115(X) , 33: isNaturalKind^#(X) -> c_94(X) , 34: isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , 35: isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , 36: isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 37: and^#(X1, X2) -> c_92(X1, X2) , 38: and^#(tt(), X) -> c_93(activate^#(X)) , 39: isLNat^#(X) -> c_29(X) , 40: isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , 41: isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 42: isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 43: isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , 44: isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , 45: isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , 46: isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 47: isLNatKind^#(X) -> c_101(X) , 48: isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , 49: isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 50: isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 51: isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , 52: isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , 53: isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , 54: isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 55: afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 56: afterNth^#(X1, X2) -> c_63(X1, X2) , 57: cons^#(X1, X2) -> c_58(X1, X2) , 58: fst^#(X) -> c_73(X) , 59: fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , 60: snd^#(X) -> c_39(X) , 61: snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , 62: tail^#(X) -> c_116(X) , 63: tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , 64: take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 65: take^#(X1, X2) -> c_119(X1, X2) , 66: head^#(X) -> c_60(X) , 67: head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , 68: sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 69: sel^#(X1, X2) -> c_113(X1, X2) , 70: pair^#(X1, X2) -> c_66(X1, X2) , 71: splitAt^#(X1, X2) -> c_41(X1, X2) , 72: splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , 73: splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , 74: U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , 75: U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , 76: U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , 77: U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , 78: U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , 79: U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , 80: U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , 81: U181^#(tt(), Y) -> c_64(activate^#(Y)) , 82: U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , 83: U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , 84: U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , 85: U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , 86: U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , 87: U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , 88: U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , 89: U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , 90: U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , 91: U31^#(tt(), N) -> c_75(activate^#(N)) , 92: U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , 93: U21^#(tt(), X) -> c_70(activate^#(X)) , 94: U211^#(tt(), XS) -> c_71(activate^#(XS)) , 95: U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , 96: U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , 97: U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , 98: isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 99: isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 100: isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , 101: isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 102: U103^#(tt()) -> c_28() , 103: isNatural^#(n__0()) -> c_5() , 104: isNaturalKind^#(n__0()) -> c_96() , 105: isLNat^#(n__nil()) -> c_31() , 106: isLNatKind^#(n__nil()) -> c_103() , 107: nil^#() -> c_67() , 108: 0^#() -> c_114() , 109: U112^#(tt()) -> c_45() , 110: U122^#(tt()) -> c_47() , 111: U133^#(tt()) -> c_50() , 112: U143^#(tt()) -> c_53() , 113: U153^#(tt()) -> c_56() , 114: U43^#(tt()) -> c_78() , 115: U53^#(tt()) -> c_81() , 116: U62^#(tt()) -> c_83() , 117: U72^#(tt()) -> c_87() , 118: U82^#(tt()) -> c_89() , 119: U92^#(tt()) -> c_91() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U101^#(tt(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , isNatural^#(X) -> c_3(X) , isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_10(s^#(activate(X))) , activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , activate^#(n__head(X)) -> c_23(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , natsFrom^#(X) -> c_111(X) , s^#(X) -> c_115(X) , isNaturalKind^#(X) -> c_94(X) , isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , and^#(X1, X2) -> c_92(X1, X2) , and^#(tt(), X) -> c_93(activate^#(X)) , isLNat^#(X) -> c_29(X) , isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNatKind^#(X) -> c_101(X) , isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , afterNth^#(X1, X2) -> c_63(X1, X2) , cons^#(X1, X2) -> c_58(X1, X2) , fst^#(X) -> c_73(X) , fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , snd^#(X) -> c_39(X) , snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , tail^#(X) -> c_116(X) , tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , take^#(X1, X2) -> c_119(X1, X2) , head^#(X) -> c_60(X) , head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , sel^#(X1, X2) -> c_113(X1, X2) , pair^#(X1, X2) -> c_66(X1, X2) , splitAt^#(X1, X2) -> c_41(X1, X2) , splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , U181^#(tt(), Y) -> c_64(activate^#(Y)) , U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N) -> c_75(activate^#(N)) , U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X) -> c_70(activate^#(X)) , U211^#(tt(), XS) -> c_71(activate^#(XS)) , U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) } Strict Trs: { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2)) , U102(tt(), V2) -> U103(isLNat(activate(V2))) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)), activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)), activate(V1)) , isNatural(n__sel(V1, V2)) -> U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isNaturalKind(X)) -> isNaturalKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__isLNatKind(X)) -> isLNatKind(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__isNatural(X)) -> isNatural(X) , U103(tt()) -> tt() , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)), activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)), activate(V1)) , isLNat(n__take(V1, V2)) -> U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS) , splitAt(s(N), cons(X, XS)) -> U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS)) , U111(tt(), V1) -> U112(isLNat(activate(V1))) , U112(tt()) -> tt() , U121(tt(), V1) -> U122(isNatural(activate(V1))) , U122(tt()) -> tt() , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2)) , U132(tt(), V2) -> U133(isLNat(activate(V2))) , U133(tt()) -> tt() , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2)) , U142(tt(), V2) -> U143(isLNat(activate(V2))) , U143(tt()) -> tt() , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2)) , U152(tt(), V2) -> U153(isLNat(activate(V2))) , U153(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) , afterNth(N, XS) -> U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(splitAt(activate(N), activate(XS)), activate(X)) , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X) -> activate(X) , U211(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X) , U31(tt(), N) -> activate(N) , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isLNat(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isLNat(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1) -> U62(isPLNat(activate(V1))) , U62(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U71(tt(), V1) -> U72(isNatural(activate(V1))) , U72(tt()) -> tt() , U81(tt(), V1) -> U82(isPLNat(activate(V1))) , U82(tt()) -> tt() , U91(tt(), V1) -> U92(isLNat(activate(V1))) , U92(tt()) -> tt() , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNaturalKind(X) -> n__isNaturalKind(X) , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) , isNaturalKind(n__0()) -> tt() , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) , isNaturalKind(n__sel(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__pair(V1, V2)) -> and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__splitAt(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(X) -> n__isLNatKind(X) , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) , isLNatKind(n__nil()) -> tt() , isLNatKind(n__afterNth(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__cons(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) , isLNatKind(n__take(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(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)) -> U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) , take(N, XS) -> U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , take(X1, X2) -> n__take(X1, X2) } Weak DPs: { U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , U103^#(tt()) -> c_28() , isNatural^#(n__0()) -> c_5() , U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , activate^#(n__nil()) -> c_15(nil^#()) , activate^#(n__0()) -> c_22(0^#()) , isNaturalKind^#(n__0()) -> c_96() , isLNat^#(n__nil()) -> c_31() , isLNatKind^#(n__nil()) -> c_103() , nil^#() -> c_67() , 0^#() -> c_114() , U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , U112^#(tt()) -> c_45() , U122^#(tt()) -> c_47() , U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , U133^#(tt()) -> c_50() , U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , U143^#(tt()) -> c_53() , U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , U153^#(tt()) -> c_56() , U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , U43^#(tt()) -> c_78() , U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , U53^#(tt()) -> c_81() , U62^#(tt()) -> c_83() , U72^#(tt()) -> c_87() , U82^#(tt()) -> c_89() , U92^#(tt()) -> c_91() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,3,4,6,35,38,39,40,69,70,75,76} by applications of Pre({1,3,4,6,35,38,39,40,69,70,75,76}) = {2,5,7,12,24,26,27,28,32,34,36,37,41,42,51,52,53,55,57,60,61,64,65,66,84,85}. Here rules are labeled as follows: DPs: { 1: U101^#(tt(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , 2: isNatural^#(X) -> c_3(X) , 3: isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , 4: isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , 5: isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 6: U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , 7: activate^#(X) -> c_8(X) , 8: activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , 9: activate^#(n__s(X)) -> c_10(s^#(activate(X))) , 10: activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , 11: activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , 12: activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , 13: activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , 14: activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , 15: activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , 16: activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , 17: activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , 18: activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , 19: activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , 20: activate^#(n__head(X)) -> c_23(head^#(activate(X))) , 21: activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , 22: activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , 23: activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , 24: activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , 25: natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , 26: natsFrom^#(X) -> c_111(X) , 27: s^#(X) -> c_115(X) , 28: isNaturalKind^#(X) -> c_94(X) , 29: isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , 30: isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , 31: isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 32: and^#(X1, X2) -> c_92(X1, X2) , 33: and^#(tt(), X) -> c_93(activate^#(X)) , 34: isLNat^#(X) -> c_29(X) , 35: isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , 36: isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 37: isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 38: isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , 39: isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , 40: isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , 41: isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 42: isLNatKind^#(X) -> c_101(X) , 43: isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , 44: isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 45: isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 46: isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , 47: isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , 48: isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , 49: isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 50: afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 51: afterNth^#(X1, X2) -> c_63(X1, X2) , 52: cons^#(X1, X2) -> c_58(X1, X2) , 53: fst^#(X) -> c_73(X) , 54: fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , 55: snd^#(X) -> c_39(X) , 56: snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , 57: tail^#(X) -> c_116(X) , 58: tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , 59: take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 60: take^#(X1, X2) -> c_119(X1, X2) , 61: head^#(X) -> c_60(X) , 62: head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , 63: sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 64: sel^#(X1, X2) -> c_113(X1, X2) , 65: pair^#(X1, X2) -> c_66(X1, X2) , 66: splitAt^#(X1, X2) -> c_41(X1, X2) , 67: splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , 68: splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , 69: U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , 70: U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , 71: U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , 72: U181^#(tt(), Y) -> c_64(activate^#(Y)) , 73: U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , 74: U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , 75: U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , 76: U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , 77: U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , 78: U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , 79: U31^#(tt(), N) -> c_75(activate^#(N)) , 80: U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , 81: U21^#(tt(), X) -> c_70(activate^#(X)) , 82: U211^#(tt(), XS) -> c_71(activate^#(XS)) , 83: U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , 84: isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 85: isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 86: isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , 87: isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 88: U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , 89: U103^#(tt()) -> c_28() , 90: isNatural^#(n__0()) -> c_5() , 91: U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , 92: U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , 93: activate^#(n__nil()) -> c_15(nil^#()) , 94: activate^#(n__0()) -> c_22(0^#()) , 95: isNaturalKind^#(n__0()) -> c_96() , 96: isLNat^#(n__nil()) -> c_31() , 97: isLNatKind^#(n__nil()) -> c_103() , 98: nil^#() -> c_67() , 99: 0^#() -> c_114() , 100: U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , 101: U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , 102: U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , 103: U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , 104: U112^#(tt()) -> c_45() , 105: U122^#(tt()) -> c_47() , 106: U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , 107: U133^#(tt()) -> c_50() , 108: U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , 109: U143^#(tt()) -> c_53() , 110: U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , 111: U153^#(tt()) -> c_56() , 112: U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , 113: U43^#(tt()) -> c_78() , 114: U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , 115: U53^#(tt()) -> c_81() , 116: U62^#(tt()) -> c_83() , 117: U72^#(tt()) -> c_87() , 118: U82^#(tt()) -> c_89() , 119: U92^#(tt()) -> c_91() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isNatural^#(X) -> c_3(X) , isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , activate^#(X) -> c_8(X) , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_10(s^#(activate(X))) , activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , activate^#(n__head(X)) -> c_23(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , natsFrom^#(X) -> c_111(X) , s^#(X) -> c_115(X) , isNaturalKind^#(X) -> c_94(X) , isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , and^#(X1, X2) -> c_92(X1, X2) , and^#(tt(), X) -> c_93(activate^#(X)) , isLNat^#(X) -> c_29(X) , isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNatKind^#(X) -> c_101(X) , isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , afterNth^#(X1, X2) -> c_63(X1, X2) , cons^#(X1, X2) -> c_58(X1, X2) , fst^#(X) -> c_73(X) , fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , snd^#(X) -> c_39(X) , snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , tail^#(X) -> c_116(X) , tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , take^#(X1, X2) -> c_119(X1, X2) , head^#(X) -> c_60(X) , head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , sel^#(X1, X2) -> c_113(X1, X2) , pair^#(X1, X2) -> c_66(X1, X2) , splitAt^#(X1, X2) -> c_41(X1, X2) , splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , U181^#(tt(), Y) -> c_64(activate^#(Y)) , U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N) -> c_75(activate^#(N)) , U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X) -> c_70(activate^#(X)) , U211^#(tt(), XS) -> c_71(activate^#(XS)) , U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) } Strict Trs: { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2)) , U102(tt(), V2) -> U103(isLNat(activate(V2))) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)), activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)), activate(V1)) , isNatural(n__sel(V1, V2)) -> U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isNaturalKind(X)) -> isNaturalKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__isLNatKind(X)) -> isLNatKind(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__isNatural(X)) -> isNatural(X) , U103(tt()) -> tt() , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)), activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)), activate(V1)) , isLNat(n__take(V1, V2)) -> U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS) , splitAt(s(N), cons(X, XS)) -> U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS)) , U111(tt(), V1) -> U112(isLNat(activate(V1))) , U112(tt()) -> tt() , U121(tt(), V1) -> U122(isNatural(activate(V1))) , U122(tt()) -> tt() , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2)) , U132(tt(), V2) -> U133(isLNat(activate(V2))) , U133(tt()) -> tt() , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2)) , U142(tt(), V2) -> U143(isLNat(activate(V2))) , U143(tt()) -> tt() , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2)) , U152(tt(), V2) -> U153(isLNat(activate(V2))) , U153(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) , afterNth(N, XS) -> U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(splitAt(activate(N), activate(XS)), activate(X)) , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X) -> activate(X) , U211(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X) , U31(tt(), N) -> activate(N) , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isLNat(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isLNat(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1) -> U62(isPLNat(activate(V1))) , U62(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U71(tt(), V1) -> U72(isNatural(activate(V1))) , U72(tt()) -> tt() , U81(tt(), V1) -> U82(isPLNat(activate(V1))) , U82(tt()) -> tt() , U91(tt(), V1) -> U92(isLNat(activate(V1))) , U92(tt()) -> tt() , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNaturalKind(X) -> n__isNaturalKind(X) , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) , isNaturalKind(n__0()) -> tt() , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) , isNaturalKind(n__sel(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__pair(V1, V2)) -> and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__splitAt(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(X) -> n__isLNatKind(X) , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) , isLNatKind(n__nil()) -> tt() , isLNatKind(n__afterNth(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__cons(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) , isLNatKind(n__take(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(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)) -> U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) , take(N, XS) -> U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , take(X1, X2) -> n__take(X1, X2) } Weak DPs: { U101^#(tt(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , U103^#(tt()) -> c_28() , isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , isNatural^#(n__0()) -> c_5() , isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , activate^#(n__nil()) -> c_15(nil^#()) , activate^#(n__0()) -> c_22(0^#()) , isNaturalKind^#(n__0()) -> c_96() , isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , isLNat^#(n__nil()) -> c_31() , isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , isLNatKind^#(n__nil()) -> c_103() , nil^#() -> c_67() , 0^#() -> c_114() , U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , U112^#(tt()) -> c_45() , U122^#(tt()) -> c_47() , U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , U133^#(tt()) -> c_50() , U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , U143^#(tt()) -> c_53() , U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , U153^#(tt()) -> c_56() , U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , U43^#(tt()) -> c_78() , U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , U53^#(tt()) -> c_81() , U62^#(tt()) -> c_83() , U72^#(tt()) -> c_87() , U82^#(tt()) -> c_89() , U92^#(tt()) -> c_91() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {2,31,32,33,72,73} by applications of Pre({2,31,32,33,72,73}) = {1,3,8,20,22,23,24,28,30,34,43,44,45,47,49,52,53,56,57,58}. Here rules are labeled as follows: DPs: { 1: isNatural^#(X) -> c_3(X) , 2: isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 3: activate^#(X) -> c_8(X) , 4: activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , 5: activate^#(n__s(X)) -> c_10(s^#(activate(X))) , 6: activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , 7: activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , 8: activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , 9: activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , 10: activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , 11: activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , 12: activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , 13: activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , 14: activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , 15: activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , 16: activate^#(n__head(X)) -> c_23(head^#(activate(X))) , 17: activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , 18: activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , 19: activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , 20: activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , 21: natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , 22: natsFrom^#(X) -> c_111(X) , 23: s^#(X) -> c_115(X) , 24: isNaturalKind^#(X) -> c_94(X) , 25: isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , 26: isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , 27: isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 28: and^#(X1, X2) -> c_92(X1, X2) , 29: and^#(tt(), X) -> c_93(activate^#(X)) , 30: isLNat^#(X) -> c_29(X) , 31: isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 32: isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 33: isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 34: isLNatKind^#(X) -> c_101(X) , 35: isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , 36: isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 37: isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 38: isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , 39: isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , 40: isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , 41: isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 42: afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 43: afterNth^#(X1, X2) -> c_63(X1, X2) , 44: cons^#(X1, X2) -> c_58(X1, X2) , 45: fst^#(X) -> c_73(X) , 46: fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , 47: snd^#(X) -> c_39(X) , 48: snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , 49: tail^#(X) -> c_116(X) , 50: tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , 51: take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 52: take^#(X1, X2) -> c_119(X1, X2) , 53: head^#(X) -> c_60(X) , 54: head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , 55: sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , 56: sel^#(X1, X2) -> c_113(X1, X2) , 57: pair^#(X1, X2) -> c_66(X1, X2) , 58: splitAt^#(X1, X2) -> c_41(X1, X2) , 59: splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , 60: splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , 61: U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , 62: U181^#(tt(), Y) -> c_64(activate^#(Y)) , 63: U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , 64: U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , 65: U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , 66: U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , 67: U31^#(tt(), N) -> c_75(activate^#(N)) , 68: U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , 69: U21^#(tt(), X) -> c_70(activate^#(X)) , 70: U211^#(tt(), XS) -> c_71(activate^#(XS)) , 71: U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , 72: isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 73: isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , 74: isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , 75: isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , 76: U101^#(tt(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , 77: U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , 78: U103^#(tt()) -> c_28() , 79: isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , 80: isNatural^#(n__0()) -> c_5() , 81: isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , 82: U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , 83: U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , 84: U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , 85: activate^#(n__nil()) -> c_15(nil^#()) , 86: activate^#(n__0()) -> c_22(0^#()) , 87: isNaturalKind^#(n__0()) -> c_96() , 88: isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , 89: isLNat^#(n__nil()) -> c_31() , 90: isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , 91: isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , 92: isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , 93: isLNatKind^#(n__nil()) -> c_103() , 94: nil^#() -> c_67() , 95: 0^#() -> c_114() , 96: U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , 97: U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , 98: U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , 99: U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , 100: U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , 101: U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , 102: U112^#(tt()) -> c_45() , 103: U122^#(tt()) -> c_47() , 104: U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , 105: U133^#(tt()) -> c_50() , 106: U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , 107: U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , 108: U143^#(tt()) -> c_53() , 109: U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , 110: U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , 111: U153^#(tt()) -> c_56() , 112: U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , 113: U43^#(tt()) -> c_78() , 114: U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , 115: U53^#(tt()) -> c_81() , 116: U62^#(tt()) -> c_83() , 117: U72^#(tt()) -> c_87() , 118: U82^#(tt()) -> c_89() , 119: U92^#(tt()) -> c_91() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isNatural^#(X) -> c_3(X) , activate^#(X) -> c_8(X) , activate^#(n__natsFrom(X)) -> c_9(natsFrom^#(activate(X))) , activate^#(n__s(X)) -> c_10(s^#(activate(X))) , activate^#(n__isNaturalKind(X)) -> c_11(isNaturalKind^#(X)) , activate^#(n__and(X1, X2)) -> c_12(and^#(activate(X1), X2)) , activate^#(n__isLNat(X)) -> c_13(isLNat^#(X)) , activate^#(n__isLNatKind(X)) -> c_14(isLNatKind^#(X)) , activate^#(n__afterNth(X1, X2)) -> c_16(afterNth^#(activate(X1), activate(X2))) , activate^#(n__cons(X1, X2)) -> c_17(cons^#(activate(X1), X2)) , activate^#(n__fst(X)) -> c_18(fst^#(activate(X))) , activate^#(n__snd(X)) -> c_19(snd^#(activate(X))) , activate^#(n__tail(X)) -> c_20(tail^#(activate(X))) , activate^#(n__take(X1, X2)) -> c_21(take^#(activate(X1), activate(X2))) , activate^#(n__head(X)) -> c_23(head^#(activate(X))) , activate^#(n__sel(X1, X2)) -> c_24(sel^#(activate(X1), activate(X2))) , activate^#(n__pair(X1, X2)) -> c_25(pair^#(activate(X1), activate(X2))) , activate^#(n__splitAt(X1, X2)) -> c_26(splitAt^#(activate(X1), activate(X2))) , activate^#(n__isNatural(X)) -> c_27(isNatural^#(X)) , natsFrom^#(N) -> c_110(U161^#(and(isNatural(N), n__isNaturalKind(N)), N)) , natsFrom^#(X) -> c_111(X) , s^#(X) -> c_115(X) , isNaturalKind^#(X) -> c_94(X) , isNaturalKind^#(n__s(V1)) -> c_95(isNaturalKind^#(activate(V1))) , isNaturalKind^#(n__head(V1)) -> c_97(isLNatKind^#(activate(V1))) , isNaturalKind^#(n__sel(V1, V2)) -> c_98(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , and^#(X1, X2) -> c_92(X1, X2) , and^#(tt(), X) -> c_93(activate^#(X)) , isLNat^#(X) -> c_29(X) , isLNatKind^#(X) -> c_101(X) , isLNatKind^#(n__natsFrom(V1)) -> c_102(isNaturalKind^#(activate(V1))) , isLNatKind^#(n__afterNth(V1, V2)) -> c_104(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__cons(V1, V2)) -> c_105(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , isLNatKind^#(n__fst(V1)) -> c_106(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__snd(V1)) -> c_107(isPLNatKind^#(activate(V1))) , isLNatKind^#(n__tail(V1)) -> c_108(isLNatKind^#(activate(V1))) , isLNatKind^#(n__take(V1, V2)) -> c_109(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) , afterNth^#(N, XS) -> c_62(U11^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , afterNth^#(X1, X2) -> c_63(X1, X2) , cons^#(X1, X2) -> c_58(X1, X2) , fst^#(X) -> c_73(X) , fst^#(pair(X, Y)) -> c_74(U21^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X)) , snd^#(X) -> c_39(X) , snd^#(pair(X, Y)) -> c_40(U181^#(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y)) , tail^#(X) -> c_116(X) , tail^#(cons(N, XS)) -> c_117(U211^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS))) , take^#(N, XS) -> c_118(U221^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , take^#(X1, X2) -> c_119(X1, X2) , head^#(X) -> c_60(X) , head^#(cons(N, XS)) -> c_61(U31^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N)) , sel^#(N, XS) -> c_112(U171^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS)) , sel^#(X1, X2) -> c_113(X1, X2) , pair^#(X1, X2) -> c_66(X1, X2) , splitAt^#(X1, X2) -> c_41(X1, X2) , splitAt^#(0(), XS) -> c_42(U191^#(and(isLNat(XS), n__isLNatKind(XS)), XS)) , splitAt^#(s(N), cons(X, XS)) -> c_43(U201^#(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS))) , U11^#(tt(), N, XS) -> c_38(snd^#(splitAt(activate(N), activate(XS)))) , U181^#(tt(), Y) -> c_64(activate^#(Y)) , U191^#(tt(), XS) -> c_65(pair^#(nil(), activate(XS))) , U201^#(tt(), N, X, XS) -> c_68(U202^#(splitAt(activate(N), activate(XS)), activate(X))) , U161^#(tt(), N) -> c_57(cons^#(activate(N), n__natsFrom(n__s(activate(N))))) , U171^#(tt(), N, XS) -> c_59(head^#(afterNth(activate(N), activate(XS)))) , U31^#(tt(), N) -> c_75(activate^#(N)) , U202^#(pair(YS, ZS), X) -> c_69(pair^#(cons(activate(X), YS), ZS)) , U21^#(tt(), X) -> c_70(activate^#(X)) , U211^#(tt(), XS) -> c_71(activate^#(XS)) , U221^#(tt(), N, XS) -> c_72(fst^#(splitAt(activate(N), activate(XS)))) , isPLNatKind^#(n__pair(V1, V2)) -> c_99(and^#(isLNatKind(activate(V1)), n__isLNatKind(activate(V2)))) , isPLNatKind^#(n__splitAt(V1, V2)) -> c_100(and^#(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2)))) } Strict Trs: { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2)) , U102(tt(), V2) -> U103(isLNat(activate(V2))) , isNatural(X) -> n__isNatural(X) , isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)), activate(V1)) , isNatural(n__0()) -> tt() , isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)), activate(V1)) , isNatural(n__sel(V1, V2)) -> U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , activate(X) -> X , activate(n__natsFrom(X)) -> natsFrom(activate(X)) , activate(n__s(X)) -> s(activate(X)) , activate(n__isNaturalKind(X)) -> isNaturalKind(X) , activate(n__and(X1, X2)) -> and(activate(X1), X2) , activate(n__isLNat(X)) -> isLNat(X) , activate(n__isLNatKind(X)) -> isLNatKind(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__isNatural(X)) -> isNatural(X) , U103(tt()) -> tt() , isLNat(X) -> n__isLNat(X) , isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)), activate(V1)) , isLNat(n__nil()) -> tt() , isLNat(n__afterNth(V1, V2)) -> U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__cons(V1, V2)) -> U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)), activate(V1)) , isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)), activate(V1)) , isLNat(n__take(V1, V2)) -> U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) , snd(X) -> n__snd(X) , snd(pair(X, Y)) -> U181(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), Y) , splitAt(X1, X2) -> n__splitAt(X1, X2) , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS) , splitAt(s(N), cons(X, XS)) -> U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N, X, activate(XS)) , U111(tt(), V1) -> U112(isLNat(activate(V1))) , U112(tt()) -> tt() , U121(tt(), V1) -> U122(isNatural(activate(V1))) , U122(tt()) -> tt() , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2)) , U132(tt(), V2) -> U133(isLNat(activate(V2))) , U133(tt()) -> tt() , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2)) , U142(tt(), V2) -> U143(isLNat(activate(V2))) , U143(tt()) -> tt() , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2)) , U152(tt(), V2) -> U153(isLNat(activate(V2))) , U153(tt()) -> tt() , U161(tt(), N) -> cons(activate(N), n__natsFrom(n__s(activate(N)))) , cons(X1, X2) -> n__cons(X1, X2) , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) , head(X) -> n__head(X) , head(cons(N, XS)) -> U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) , afterNth(N, XS) -> U11(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , afterNth(X1, X2) -> n__afterNth(X1, X2) , U181(tt(), Y) -> activate(Y) , U191(tt(), XS) -> pair(nil(), activate(XS)) , pair(X1, X2) -> n__pair(X1, X2) , nil() -> n__nil() , U201(tt(), N, X, XS) -> U202(splitAt(activate(N), activate(XS)), activate(X)) , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) , U21(tt(), X) -> activate(X) , U211(tt(), XS) -> activate(XS) , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) , fst(X) -> n__fst(X) , fst(pair(X, Y)) -> U21(and(and(isLNat(X), n__isLNatKind(X)), n__and(n__isLNat(Y), n__isLNatKind(Y))), X) , U31(tt(), N) -> activate(N) , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2)) , U42(tt(), V2) -> U43(isLNat(activate(V2))) , U43(tt()) -> tt() , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2)) , U52(tt(), V2) -> U53(isLNat(activate(V2))) , U53(tt()) -> tt() , U61(tt(), V1) -> U62(isPLNat(activate(V1))) , U62(tt()) -> tt() , isPLNat(n__pair(V1, V2)) -> U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , isPLNat(n__splitAt(V1, V2)) -> U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2)) , U71(tt(), V1) -> U72(isNatural(activate(V1))) , U72(tt()) -> tt() , U81(tt(), V1) -> U82(isPLNat(activate(V1))) , U82(tt()) -> tt() , U91(tt(), V1) -> U92(isLNat(activate(V1))) , U92(tt()) -> tt() , and(X1, X2) -> n__and(X1, X2) , and(tt(), X) -> activate(X) , isNaturalKind(X) -> n__isNaturalKind(X) , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) , isNaturalKind(n__0()) -> tt() , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) , isNaturalKind(n__sel(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__pair(V1, V2)) -> and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) , isPLNatKind(n__splitAt(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(X) -> n__isLNatKind(X) , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) , isLNatKind(n__nil()) -> tt() , isLNatKind(n__afterNth(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__cons(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) , isLNatKind(n__take(V1, V2)) -> and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N) , natsFrom(X) -> n__natsFrom(X) , sel(N, XS) -> U171(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(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)) -> U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) , take(N, XS) -> U221(and(and(isNatural(N), n__isNaturalKind(N)), n__and(n__isLNat(XS), n__isLNatKind(XS))), N, XS) , take(X1, X2) -> n__take(X1, X2) } Weak DPs: { U101^#(tt(), V1, V2) -> c_1(U102^#(isNatural(activate(V1)), activate(V2))) , U102^#(tt(), V2) -> c_2(U103^#(isLNat(activate(V2)))) , U103^#(tt()) -> c_28() , isNatural^#(n__s(V1)) -> c_4(U121^#(isNaturalKind(activate(V1)), activate(V1))) , isNatural^#(n__0()) -> c_5() , isNatural^#(n__head(V1)) -> c_6(U111^#(isLNatKind(activate(V1)), activate(V1))) , isNatural^#(n__sel(V1, V2)) -> c_7(U131^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , U121^#(tt(), V1) -> c_46(U122^#(isNatural(activate(V1)))) , U111^#(tt(), V1) -> c_44(U112^#(isLNat(activate(V1)))) , U131^#(tt(), V1, V2) -> c_48(U132^#(isNatural(activate(V1)), activate(V2))) , activate^#(n__nil()) -> c_15(nil^#()) , activate^#(n__0()) -> c_22(0^#()) , isNaturalKind^#(n__0()) -> c_96() , isLNat^#(n__natsFrom(V1)) -> c_30(U71^#(isNaturalKind(activate(V1)), activate(V1))) , isLNat^#(n__nil()) -> c_31() , isLNat^#(n__afterNth(V1, V2)) -> c_32(U41^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__cons(V1, V2)) -> c_33(U51^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNat^#(n__fst(V1)) -> c_34(U61^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__snd(V1)) -> c_35(U81^#(isPLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__tail(V1)) -> c_36(U91^#(isLNatKind(activate(V1)), activate(V1))) , isLNat^#(n__take(V1, V2)) -> c_37(U101^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isLNatKind^#(n__nil()) -> c_103() , nil^#() -> c_67() , 0^#() -> c_114() , U71^#(tt(), V1) -> c_86(U72^#(isNatural(activate(V1)))) , U41^#(tt(), V1, V2) -> c_76(U42^#(isNatural(activate(V1)), activate(V2))) , U51^#(tt(), V1, V2) -> c_79(U52^#(isNatural(activate(V1)), activate(V2))) , U61^#(tt(), V1) -> c_82(U62^#(isPLNat(activate(V1)))) , U81^#(tt(), V1) -> c_88(U82^#(isPLNat(activate(V1)))) , U91^#(tt(), V1) -> c_90(U92^#(isLNat(activate(V1)))) , U112^#(tt()) -> c_45() , U122^#(tt()) -> c_47() , U132^#(tt(), V2) -> c_49(U133^#(isLNat(activate(V2)))) , U133^#(tt()) -> c_50() , U141^#(tt(), V1, V2) -> c_51(U142^#(isLNat(activate(V1)), activate(V2))) , U142^#(tt(), V2) -> c_52(U143^#(isLNat(activate(V2)))) , U143^#(tt()) -> c_53() , U151^#(tt(), V1, V2) -> c_54(U152^#(isNatural(activate(V1)), activate(V2))) , U152^#(tt(), V2) -> c_55(U153^#(isLNat(activate(V2)))) , U153^#(tt()) -> c_56() , U42^#(tt(), V2) -> c_77(U43^#(isLNat(activate(V2)))) , U43^#(tt()) -> c_78() , U52^#(tt(), V2) -> c_80(U53^#(isLNat(activate(V2)))) , U53^#(tt()) -> c_81() , U62^#(tt()) -> c_83() , isPLNat^#(n__pair(V1, V2)) -> c_84(U141^#(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , isPLNat^#(n__splitAt(V1, V2)) -> c_85(U151^#(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1), activate(V2))) , U72^#(tt()) -> c_87() , U82^#(tt()) -> c_89() , U92^#(tt()) -> c_91() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) '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 Arrrr..