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