Runtime Complexity TRS:
The TRS R consists of the following rules:

a__U101(tt, V1, V2) → a__U102(a__isNaturalKind(V1), V1, V2)
a__U102(tt, V1, V2) → a__U103(a__isLNatKind(V2), V1, V2)
a__U103(tt, V1, V2) → a__U104(a__isLNatKind(V2), V1, V2)
a__U104(tt, V1, V2) → a__U105(a__isNatural(V1), V2)
a__U105(tt, V2) → a__U106(a__isLNat(V2))
a__U106(tt) → tt
a__U11(tt, N, XS) → a__U12(a__isNaturalKind(N), N, XS)
a__U111(tt, V2) → a__U112(a__isLNatKind(V2))
a__U112(tt) → tt
a__U12(tt, N, XS) → a__U13(a__isLNat(XS), N, XS)
a__U121(tt, V2) → a__U122(a__isLNatKind(V2))
a__U122(tt) → tt
a__U13(tt, N, XS) → a__U14(a__isLNatKind(XS), N, XS)
a__U131(tt) → tt
a__U14(tt, N, XS) → a__snd(a__splitAt(mark(N), mark(XS)))
a__U141(tt) → tt
a__U151(tt) → tt
a__U161(tt) → tt
a__U171(tt, V2) → a__U172(a__isLNatKind(V2))
a__U172(tt) → tt
a__U181(tt, V1) → a__U182(a__isLNatKind(V1), V1)
a__U182(tt, V1) → a__U183(a__isLNat(V1))
a__U183(tt) → tt
a__U191(tt, V1) → a__U192(a__isNaturalKind(V1), V1)
a__U192(tt, V1) → a__U193(a__isNatural(V1))
a__U193(tt) → tt
a__U201(tt, V1, V2) → a__U202(a__isNaturalKind(V1), V1, V2)
a__U202(tt, V1, V2) → a__U203(a__isLNatKind(V2), V1, V2)
a__U203(tt, V1, V2) → a__U204(a__isLNatKind(V2), V1, V2)
a__U204(tt, V1, V2) → a__U205(a__isNatural(V1), V2)
a__U205(tt, V2) → a__U206(a__isLNat(V2))
a__U206(tt) → tt
a__U21(tt, X, Y) → a__U22(a__isLNatKind(X), X, Y)
a__U211(tt) → tt
a__U22(tt, X, Y) → a__U23(a__isLNat(Y), X, Y)
a__U221(tt) → tt
a__U23(tt, X, Y) → a__U24(a__isLNatKind(Y), X)
a__U231(tt, V2) → a__U232(a__isLNatKind(V2))
a__U232(tt) → tt
a__U24(tt, X) → mark(X)
a__U241(tt, V1, V2) → a__U242(a__isLNatKind(V1), V1, V2)
a__U242(tt, V1, V2) → a__U243(a__isLNatKind(V2), V1, V2)
a__U243(tt, V1, V2) → a__U244(a__isLNatKind(V2), V1, V2)
a__U244(tt, V1, V2) → a__U245(a__isLNat(V1), V2)
a__U245(tt, V2) → a__U246(a__isLNat(V2))
a__U246(tt) → tt
a__U251(tt, V1, V2) → a__U252(a__isNaturalKind(V1), V1, V2)
a__U252(tt, V1, V2) → a__U253(a__isLNatKind(V2), V1, V2)
a__U253(tt, V1, V2) → a__U254(a__isLNatKind(V2), V1, V2)
a__U254(tt, V1, V2) → a__U255(a__isNatural(V1), V2)
a__U255(tt, V2) → a__U256(a__isLNat(V2))
a__U256(tt) → tt
a__U261(tt, V2) → a__U262(a__isLNatKind(V2))
a__U262(tt) → tt
a__U271(tt, V2) → a__U272(a__isLNatKind(V2))
a__U272(tt) → tt
a__U281(tt, N) → a__U282(a__isNaturalKind(N), N)
a__U282(tt, N) → cons(mark(N), natsFrom(s(N)))
a__U291(tt, N, XS) → a__U292(a__isNaturalKind(N), N, XS)
a__U292(tt, N, XS) → a__U293(a__isLNat(XS), N, XS)
a__U293(tt, N, XS) → a__U294(a__isLNatKind(XS), N, XS)
a__U294(tt, N, XS) → a__head(a__afterNth(mark(N), mark(XS)))
a__U301(tt, X, Y) → a__U302(a__isLNatKind(X), Y)
a__U302(tt, Y) → a__U303(a__isLNat(Y), Y)
a__U303(tt, Y) → a__U304(a__isLNatKind(Y), Y)
a__U304(tt, Y) → mark(Y)
a__U31(tt, N, XS) → a__U32(a__isNaturalKind(N), N, XS)
a__U311(tt, XS) → a__U312(a__isLNatKind(XS), XS)
a__U312(tt, XS) → pair(nil, mark(XS))
a__U32(tt, N, XS) → a__U33(a__isLNat(XS), N, XS)
a__U321(tt, N, X, XS) → a__U322(a__isNaturalKind(N), N, X, XS)
a__U322(tt, N, X, XS) → a__U323(a__isNatural(X), N, X, XS)
a__U323(tt, N, X, XS) → a__U324(a__isNaturalKind(X), N, X, XS)
a__U324(tt, N, X, XS) → a__U325(a__isLNat(XS), N, X, XS)
a__U325(tt, N, X, XS) → a__U326(a__isLNatKind(XS), N, X, XS)
a__U326(tt, N, X, XS) → a__U327(a__splitAt(mark(N), mark(XS)), X)
a__U327(pair(YS, ZS), X) → pair(cons(mark(X), YS), mark(ZS))
a__U33(tt, N, XS) → a__U34(a__isLNatKind(XS), N)
a__U331(tt, N, XS) → a__U332(a__isNaturalKind(N), XS)
a__U332(tt, XS) → a__U333(a__isLNat(XS), XS)
a__U333(tt, XS) → a__U334(a__isLNatKind(XS), XS)
a__U334(tt, XS) → mark(XS)
a__U34(tt, N) → mark(N)
a__U341(tt, N, XS) → a__U342(a__isNaturalKind(N), N, XS)
a__U342(tt, N, XS) → a__U343(a__isLNat(XS), N, XS)
a__U343(tt, N, XS) → a__U344(a__isLNatKind(XS), N, XS)
a__U344(tt, N, XS) → a__fst(a__splitAt(mark(N), mark(XS)))
a__U41(tt, V1, V2) → a__U42(a__isNaturalKind(V1), V1, V2)
a__U42(tt, V1, V2) → a__U43(a__isLNatKind(V2), V1, V2)
a__U43(tt, V1, V2) → a__U44(a__isLNatKind(V2), V1, V2)
a__U44(tt, V1, V2) → a__U45(a__isNatural(V1), V2)
a__U45(tt, V2) → a__U46(a__isLNat(V2))
a__U46(tt) → tt
a__U51(tt, V1, V2) → a__U52(a__isNaturalKind(V1), V1, V2)
a__U52(tt, V1, V2) → a__U53(a__isLNatKind(V2), V1, V2)
a__U53(tt, V1, V2) → a__U54(a__isLNatKind(V2), V1, V2)
a__U54(tt, V1, V2) → a__U55(a__isNatural(V1), V2)
a__U55(tt, V2) → a__U56(a__isLNat(V2))
a__U56(tt) → tt
a__U61(tt, V1) → a__U62(a__isPLNatKind(V1), V1)
a__U62(tt, V1) → a__U63(a__isPLNat(V1))
a__U63(tt) → tt
a__U71(tt, V1) → a__U72(a__isNaturalKind(V1), V1)
a__U72(tt, V1) → a__U73(a__isNatural(V1))
a__U73(tt) → tt
a__U81(tt, V1) → a__U82(a__isPLNatKind(V1), V1)
a__U82(tt, V1) → a__U83(a__isPLNat(V1))
a__U83(tt) → tt
a__U91(tt, V1) → a__U92(a__isLNatKind(V1), V1)
a__U92(tt, V1) → a__U93(a__isLNat(V1))
a__U93(tt) → tt
a__afterNth(N, XS) → a__U11(a__isNatural(N), N, XS)
a__fst(pair(X, Y)) → a__U21(a__isLNat(X), X, Y)
a__head(cons(N, XS)) → a__U31(a__isNatural(N), N, XS)
a__isLNat(nil) → tt
a__isLNat(afterNth(V1, V2)) → a__U41(a__isNaturalKind(V1), V1, V2)
a__isLNat(cons(V1, V2)) → a__U51(a__isNaturalKind(V1), V1, V2)
a__isLNat(fst(V1)) → a__U61(a__isPLNatKind(V1), V1)
a__isLNat(natsFrom(V1)) → a__U71(a__isNaturalKind(V1), V1)
a__isLNat(snd(V1)) → a__U81(a__isPLNatKind(V1), V1)
a__isLNat(tail(V1)) → a__U91(a__isLNatKind(V1), V1)
a__isLNat(take(V1, V2)) → a__U101(a__isNaturalKind(V1), V1, V2)
a__isLNatKind(nil) → tt
a__isLNatKind(afterNth(V1, V2)) → a__U111(a__isNaturalKind(V1), V2)
a__isLNatKind(cons(V1, V2)) → a__U121(a__isNaturalKind(V1), V2)
a__isLNatKind(fst(V1)) → a__U131(a__isPLNatKind(V1))
a__isLNatKind(natsFrom(V1)) → a__U141(a__isNaturalKind(V1))
a__isLNatKind(snd(V1)) → a__U151(a__isPLNatKind(V1))
a__isLNatKind(tail(V1)) → a__U161(a__isLNatKind(V1))
a__isLNatKind(take(V1, V2)) → a__U171(a__isNaturalKind(V1), V2)
a__isNatural(0) → tt
a__isNatural(head(V1)) → a__U181(a__isLNatKind(V1), V1)
a__isNatural(s(V1)) → a__U191(a__isNaturalKind(V1), V1)
a__isNatural(sel(V1, V2)) → a__U201(a__isNaturalKind(V1), V1, V2)
a__isNaturalKind(0) → tt
a__isNaturalKind(head(V1)) → a__U211(a__isLNatKind(V1))
a__isNaturalKind(s(V1)) → a__U221(a__isNaturalKind(V1))
a__isNaturalKind(sel(V1, V2)) → a__U231(a__isNaturalKind(V1), V2)
a__isPLNat(pair(V1, V2)) → a__U241(a__isLNatKind(V1), V1, V2)
a__isPLNat(splitAt(V1, V2)) → a__U251(a__isNaturalKind(V1), V1, V2)
a__isPLNatKind(pair(V1, V2)) → a__U261(a__isLNatKind(V1), V2)
a__isPLNatKind(splitAt(V1, V2)) → a__U271(a__isNaturalKind(V1), V2)
a__natsFrom(N) → a__U281(a__isNatural(N), N)
a__sel(N, XS) → a__U291(a__isNatural(N), N, XS)
a__snd(pair(X, Y)) → a__U301(a__isLNat(X), X, Y)
a__splitAt(0, XS) → a__U311(a__isLNat(XS), XS)
a__splitAt(s(N), cons(X, XS)) → a__U321(a__isNatural(N), N, X, XS)
a__tail(cons(N, XS)) → a__U331(a__isNatural(N), N, XS)
a__take(N, XS) → a__U341(a__isNatural(N), N, XS)
mark(U101(X1, X2, X3)) → a__U101(mark(X1), X2, X3)
mark(U102(X1, X2, X3)) → a__U102(mark(X1), X2, X3)
mark(isNaturalKind(X)) → a__isNaturalKind(X)
mark(U103(X1, X2, X3)) → a__U103(mark(X1), X2, X3)
mark(isLNatKind(X)) → a__isLNatKind(X)
mark(U104(X1, X2, X3)) → a__U104(mark(X1), X2, X3)
mark(U105(X1, X2)) → a__U105(mark(X1), X2)
mark(isNatural(X)) → a__isNatural(X)
mark(U106(X)) → a__U106(mark(X))
mark(isLNat(X)) → a__isLNat(X)
mark(U11(X1, X2, X3)) → a__U11(mark(X1), X2, X3)
mark(U12(X1, X2, X3)) → a__U12(mark(X1), X2, X3)
mark(U111(X1, X2)) → a__U111(mark(X1), X2)
mark(U112(X)) → a__U112(mark(X))
mark(U13(X1, X2, X3)) → a__U13(mark(X1), X2, X3)
mark(U121(X1, X2)) → a__U121(mark(X1), X2)
mark(U122(X)) → a__U122(mark(X))
mark(U14(X1, X2, X3)) → a__U14(mark(X1), X2, X3)
mark(U131(X)) → a__U131(mark(X))
mark(snd(X)) → a__snd(mark(X))
mark(splitAt(X1, X2)) → a__splitAt(mark(X1), mark(X2))
mark(U141(X)) → a__U141(mark(X))
mark(U151(X)) → a__U151(mark(X))
mark(U161(X)) → a__U161(mark(X))
mark(U171(X1, X2)) → a__U171(mark(X1), X2)
mark(U172(X)) → a__U172(mark(X))
mark(U181(X1, X2)) → a__U181(mark(X1), X2)
mark(U182(X1, X2)) → a__U182(mark(X1), X2)
mark(U183(X)) → a__U183(mark(X))
mark(U191(X1, X2)) → a__U191(mark(X1), X2)
mark(U192(X1, X2)) → a__U192(mark(X1), X2)
mark(U193(X)) → a__U193(mark(X))
mark(U201(X1, X2, X3)) → a__U201(mark(X1), X2, X3)
mark(U202(X1, X2, X3)) → a__U202(mark(X1), X2, X3)
mark(U203(X1, X2, X3)) → a__U203(mark(X1), X2, X3)
mark(U204(X1, X2, X3)) → a__U204(mark(X1), X2, X3)
mark(U205(X1, X2)) → a__U205(mark(X1), X2)
mark(U206(X)) → a__U206(mark(X))
mark(U21(X1, X2, X3)) → a__U21(mark(X1), X2, X3)
mark(U22(X1, X2, X3)) → a__U22(mark(X1), X2, X3)
mark(U211(X)) → a__U211(mark(X))
mark(U23(X1, X2, X3)) → a__U23(mark(X1), X2, X3)
mark(U221(X)) → a__U221(mark(X))
mark(U24(X1, X2)) → a__U24(mark(X1), X2)
mark(U231(X1, X2)) → a__U231(mark(X1), X2)
mark(U232(X)) → a__U232(mark(X))
mark(U241(X1, X2, X3)) → a__U241(mark(X1), X2, X3)
mark(U242(X1, X2, X3)) → a__U242(mark(X1), X2, X3)
mark(U243(X1, X2, X3)) → a__U243(mark(X1), X2, X3)
mark(U244(X1, X2, X3)) → a__U244(mark(X1), X2, X3)
mark(U245(X1, X2)) → a__U245(mark(X1), X2)
mark(U246(X)) → a__U246(mark(X))
mark(U251(X1, X2, X3)) → a__U251(mark(X1), X2, X3)
mark(U252(X1, X2, X3)) → a__U252(mark(X1), X2, X3)
mark(U253(X1, X2, X3)) → a__U253(mark(X1), X2, X3)
mark(U254(X1, X2, X3)) → a__U254(mark(X1), X2, X3)
mark(U255(X1, X2)) → a__U255(mark(X1), X2)
mark(U256(X)) → a__U256(mark(X))
mark(U261(X1, X2)) → a__U261(mark(X1), X2)
mark(U262(X)) → a__U262(mark(X))
mark(U271(X1, X2)) → a__U271(mark(X1), X2)
mark(U272(X)) → a__U272(mark(X))
mark(U281(X1, X2)) → a__U281(mark(X1), X2)
mark(U282(X1, X2)) → a__U282(mark(X1), X2)
mark(natsFrom(X)) → a__natsFrom(mark(X))
mark(U291(X1, X2, X3)) → a__U291(mark(X1), X2, X3)
mark(U292(X1, X2, X3)) → a__U292(mark(X1), X2, X3)
mark(U293(X1, X2, X3)) → a__U293(mark(X1), X2, X3)
mark(U294(X1, X2, X3)) → a__U294(mark(X1), X2, X3)
mark(head(X)) → a__head(mark(X))
mark(afterNth(X1, X2)) → a__afterNth(mark(X1), mark(X2))
mark(U301(X1, X2, X3)) → a__U301(mark(X1), X2, X3)
mark(U302(X1, X2)) → a__U302(mark(X1), X2)
mark(U303(X1, X2)) → a__U303(mark(X1), X2)
mark(U304(X1, X2)) → a__U304(mark(X1), X2)
mark(U31(X1, X2, X3)) → a__U31(mark(X1), X2, X3)
mark(U32(X1, X2, X3)) → a__U32(mark(X1), X2, X3)
mark(U311(X1, X2)) → a__U311(mark(X1), X2)
mark(U312(X1, X2)) → a__U312(mark(X1), X2)
mark(U33(X1, X2, X3)) → a__U33(mark(X1), X2, X3)
mark(U321(X1, X2, X3, X4)) → a__U321(mark(X1), X2, X3, X4)
mark(U322(X1, X2, X3, X4)) → a__U322(mark(X1), X2, X3, X4)
mark(U323(X1, X2, X3, X4)) → a__U323(mark(X1), X2, X3, X4)
mark(U324(X1, X2, X3, X4)) → a__U324(mark(X1), X2, X3, X4)
mark(U325(X1, X2, X3, X4)) → a__U325(mark(X1), X2, X3, X4)
mark(U326(X1, X2, X3, X4)) → a__U326(mark(X1), X2, X3, X4)
mark(U327(X1, X2)) → a__U327(mark(X1), X2)
mark(U34(X1, X2)) → a__U34(mark(X1), X2)
mark(U331(X1, X2, X3)) → a__U331(mark(X1), X2, X3)
mark(U332(X1, X2)) → a__U332(mark(X1), X2)
mark(U333(X1, X2)) → a__U333(mark(X1), X2)
mark(U334(X1, X2)) → a__U334(mark(X1), X2)
mark(U341(X1, X2, X3)) → a__U341(mark(X1), X2, X3)
mark(U342(X1, X2, X3)) → a__U342(mark(X1), X2, X3)
mark(U343(X1, X2, X3)) → a__U343(mark(X1), X2, X3)
mark(U344(X1, X2, X3)) → a__U344(mark(X1), X2, X3)
mark(fst(X)) → a__fst(mark(X))
mark(U41(X1, X2, X3)) → a__U41(mark(X1), X2, X3)
mark(U42(X1, X2, X3)) → a__U42(mark(X1), X2, X3)
mark(U43(X1, X2, X3)) → a__U43(mark(X1), X2, X3)
mark(U44(X1, X2, X3)) → a__U44(mark(X1), X2, X3)
mark(U45(X1, X2)) → a__U45(mark(X1), X2)
mark(U46(X)) → a__U46(mark(X))
mark(U51(X1, X2, X3)) → a__U51(mark(X1), X2, X3)
mark(U52(X1, X2, X3)) → a__U52(mark(X1), X2, X3)
mark(U53(X1, X2, X3)) → a__U53(mark(X1), X2, X3)
mark(U54(X1, X2, X3)) → a__U54(mark(X1), X2, X3)
mark(U55(X1, X2)) → a__U55(mark(X1), X2)
mark(U56(X)) → a__U56(mark(X))
mark(U61(X1, X2)) → a__U61(mark(X1), X2)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(isPLNatKind(X)) → a__isPLNatKind(X)
mark(U63(X)) → a__U63(mark(X))
mark(isPLNat(X)) → a__isPLNat(X)
mark(U71(X1, X2)) → a__U71(mark(X1), X2)
mark(U72(X1, X2)) → a__U72(mark(X1), X2)
mark(U73(X)) → a__U73(mark(X))
mark(U81(X1, X2)) → a__U81(mark(X1), X2)
mark(U82(X1, X2)) → a__U82(mark(X1), X2)
mark(U83(X)) → a__U83(mark(X))
mark(U91(X1, X2)) → a__U91(mark(X1), X2)
mark(U92(X1, X2)) → a__U92(mark(X1), X2)
mark(U93(X)) → a__U93(mark(X))
mark(tail(X)) → a__tail(mark(X))
mark(take(X1, X2)) → a__take(mark(X1), mark(X2))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(tt) → tt
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
mark(pair(X1, X2)) → pair(mark(X1), mark(X2))
mark(nil) → nil
mark(0) → 0
a__U101(X1, X2, X3) → U101(X1, X2, X3)
a__U102(X1, X2, X3) → U102(X1, X2, X3)
a__isNaturalKind(X) → isNaturalKind(X)
a__U103(X1, X2, X3) → U103(X1, X2, X3)
a__isLNatKind(X) → isLNatKind(X)
a__U104(X1, X2, X3) → U104(X1, X2, X3)
a__U105(X1, X2) → U105(X1, X2)
a__isNatural(X) → isNatural(X)
a__U106(X) → U106(X)
a__isLNat(X) → isLNat(X)
a__U11(X1, X2, X3) → U11(X1, X2, X3)
a__U12(X1, X2, X3) → U12(X1, X2, X3)
a__U111(X1, X2) → U111(X1, X2)
a__U112(X) → U112(X)
a__U13(X1, X2, X3) → U13(X1, X2, X3)
a__U121(X1, X2) → U121(X1, X2)
a__U122(X) → U122(X)
a__U14(X1, X2, X3) → U14(X1, X2, X3)
a__U131(X) → U131(X)
a__snd(X) → snd(X)
a__splitAt(X1, X2) → splitAt(X1, X2)
a__U141(X) → U141(X)
a__U151(X) → U151(X)
a__U161(X) → U161(X)
a__U171(X1, X2) → U171(X1, X2)
a__U172(X) → U172(X)
a__U181(X1, X2) → U181(X1, X2)
a__U182(X1, X2) → U182(X1, X2)
a__U183(X) → U183(X)
a__U191(X1, X2) → U191(X1, X2)
a__U192(X1, X2) → U192(X1, X2)
a__U193(X) → U193(X)
a__U201(X1, X2, X3) → U201(X1, X2, X3)
a__U202(X1, X2, X3) → U202(X1, X2, X3)
a__U203(X1, X2, X3) → U203(X1, X2, X3)
a__U204(X1, X2, X3) → U204(X1, X2, X3)
a__U205(X1, X2) → U205(X1, X2)
a__U206(X) → U206(X)
a__U21(X1, X2, X3) → U21(X1, X2, X3)
a__U22(X1, X2, X3) → U22(X1, X2, X3)
a__U211(X) → U211(X)
a__U23(X1, X2, X3) → U23(X1, X2, X3)
a__U221(X) → U221(X)
a__U24(X1, X2) → U24(X1, X2)
a__U231(X1, X2) → U231(X1, X2)
a__U232(X) → U232(X)
a__U241(X1, X2, X3) → U241(X1, X2, X3)
a__U242(X1, X2, X3) → U242(X1, X2, X3)
a__U243(X1, X2, X3) → U243(X1, X2, X3)
a__U244(X1, X2, X3) → U244(X1, X2, X3)
a__U245(X1, X2) → U245(X1, X2)
a__U246(X) → U246(X)
a__U251(X1, X2, X3) → U251(X1, X2, X3)
a__U252(X1, X2, X3) → U252(X1, X2, X3)
a__U253(X1, X2, X3) → U253(X1, X2, X3)
a__U254(X1, X2, X3) → U254(X1, X2, X3)
a__U255(X1, X2) → U255(X1, X2)
a__U256(X) → U256(X)
a__U261(X1, X2) → U261(X1, X2)
a__U262(X) → U262(X)
a__U271(X1, X2) → U271(X1, X2)
a__U272(X) → U272(X)
a__U281(X1, X2) → U281(X1, X2)
a__U282(X1, X2) → U282(X1, X2)
a__natsFrom(X) → natsFrom(X)
a__U291(X1, X2, X3) → U291(X1, X2, X3)
a__U292(X1, X2, X3) → U292(X1, X2, X3)
a__U293(X1, X2, X3) → U293(X1, X2, X3)
a__U294(X1, X2, X3) → U294(X1, X2, X3)
a__head(X) → head(X)
a__afterNth(X1, X2) → afterNth(X1, X2)
a__U301(X1, X2, X3) → U301(X1, X2, X3)
a__U302(X1, X2) → U302(X1, X2)
a__U303(X1, X2) → U303(X1, X2)
a__U304(X1, X2) → U304(X1, X2)
a__U31(X1, X2, X3) → U31(X1, X2, X3)
a__U32(X1, X2, X3) → U32(X1, X2, X3)
a__U311(X1, X2) → U311(X1, X2)
a__U312(X1, X2) → U312(X1, X2)
a__U33(X1, X2, X3) → U33(X1, X2, X3)
a__U321(X1, X2, X3, X4) → U321(X1, X2, X3, X4)
a__U322(X1, X2, X3, X4) → U322(X1, X2, X3, X4)
a__U323(X1, X2, X3, X4) → U323(X1, X2, X3, X4)
a__U324(X1, X2, X3, X4) → U324(X1, X2, X3, X4)
a__U325(X1, X2, X3, X4) → U325(X1, X2, X3, X4)
a__U326(X1, X2, X3, X4) → U326(X1, X2, X3, X4)
a__U327(X1, X2) → U327(X1, X2)
a__U34(X1, X2) → U34(X1, X2)
a__U331(X1, X2, X3) → U331(X1, X2, X3)
a__U332(X1, X2) → U332(X1, X2)
a__U333(X1, X2) → U333(X1, X2)
a__U334(X1, X2) → U334(X1, X2)
a__U341(X1, X2, X3) → U341(X1, X2, X3)
a__U342(X1, X2, X3) → U342(X1, X2, X3)
a__U343(X1, X2, X3) → U343(X1, X2, X3)
a__U344(X1, X2, X3) → U344(X1, X2, X3)
a__fst(X) → fst(X)
a__U41(X1, X2, X3) → U41(X1, X2, X3)
a__U42(X1, X2, X3) → U42(X1, X2, X3)
a__U43(X1, X2, X3) → U43(X1, X2, X3)
a__U44(X1, X2, X3) → U44(X1, X2, X3)
a__U45(X1, X2) → U45(X1, X2)
a__U46(X) → U46(X)
a__U51(X1, X2, X3) → U51(X1, X2, X3)
a__U52(X1, X2, X3) → U52(X1, X2, X3)
a__U53(X1, X2, X3) → U53(X1, X2, X3)
a__U54(X1, X2, X3) → U54(X1, X2, X3)
a__U55(X1, X2) → U55(X1, X2)
a__U56(X) → U56(X)
a__U61(X1, X2) → U61(X1, X2)
a__U62(X1, X2) → U62(X1, X2)
a__isPLNatKind(X) → isPLNatKind(X)
a__U63(X) → U63(X)
a__isPLNat(X) → isPLNat(X)
a__U71(X1, X2) → U71(X1, X2)
a__U72(X1, X2) → U72(X1, X2)
a__U73(X) → U73(X)
a__U81(X1, X2) → U81(X1, X2)
a__U82(X1, X2) → U82(X1, X2)
a__U83(X) → U83(X)
a__U91(X1, X2) → U91(X1, X2)
a__U92(X1, X2) → U92(X1, X2)
a__U93(X) → U93(X)
a__tail(X) → tail(X)
a__take(X1, X2) → take(X1, X2)
a__sel(X1, X2) → sel(X1, X2)

Rewrite Strategy: INNERMOST


Renamed function symbols to avoid clashes with predefined symbol.


Runtime Complexity TRS:
The TRS R consists of the following rules:


a__U101'(tt', V1, V2) → a__U102'(a__isNaturalKind'(V1), V1, V2)
a__U102'(tt', V1, V2) → a__U103'(a__isLNatKind'(V2), V1, V2)
a__U103'(tt', V1, V2) → a__U104'(a__isLNatKind'(V2), V1, V2)
a__U104'(tt', V1, V2) → a__U105'(a__isNatural'(V1), V2)
a__U105'(tt', V2) → a__U106'(a__isLNat'(V2))
a__U106'(tt') → tt'
a__U11'(tt', N, XS) → a__U12'(a__isNaturalKind'(N), N, XS)
a__U111'(tt', V2) → a__U112'(a__isLNatKind'(V2))
a__U112'(tt') → tt'
a__U12'(tt', N, XS) → a__U13'(a__isLNat'(XS), N, XS)
a__U121'(tt', V2) → a__U122'(a__isLNatKind'(V2))
a__U122'(tt') → tt'
a__U13'(tt', N, XS) → a__U14'(a__isLNatKind'(XS), N, XS)
a__U131'(tt') → tt'
a__U14'(tt', N, XS) → a__snd'(a__splitAt'(mark'(N), mark'(XS)))
a__U141'(tt') → tt'
a__U151'(tt') → tt'
a__U161'(tt') → tt'
a__U171'(tt', V2) → a__U172'(a__isLNatKind'(V2))
a__U172'(tt') → tt'
a__U181'(tt', V1) → a__U182'(a__isLNatKind'(V1), V1)
a__U182'(tt', V1) → a__U183'(a__isLNat'(V1))
a__U183'(tt') → tt'
a__U191'(tt', V1) → a__U192'(a__isNaturalKind'(V1), V1)
a__U192'(tt', V1) → a__U193'(a__isNatural'(V1))
a__U193'(tt') → tt'
a__U201'(tt', V1, V2) → a__U202'(a__isNaturalKind'(V1), V1, V2)
a__U202'(tt', V1, V2) → a__U203'(a__isLNatKind'(V2), V1, V2)
a__U203'(tt', V1, V2) → a__U204'(a__isLNatKind'(V2), V1, V2)
a__U204'(tt', V1, V2) → a__U205'(a__isNatural'(V1), V2)
a__U205'(tt', V2) → a__U206'(a__isLNat'(V2))
a__U206'(tt') → tt'
a__U21'(tt', X, Y) → a__U22'(a__isLNatKind'(X), X, Y)
a__U211'(tt') → tt'
a__U22'(tt', X, Y) → a__U23'(a__isLNat'(Y), X, Y)
a__U221'(tt') → tt'
a__U23'(tt', X, Y) → a__U24'(a__isLNatKind'(Y), X)
a__U231'(tt', V2) → a__U232'(a__isLNatKind'(V2))
a__U232'(tt') → tt'
a__U24'(tt', X) → mark'(X)
a__U241'(tt', V1, V2) → a__U242'(a__isLNatKind'(V1), V1, V2)
a__U242'(tt', V1, V2) → a__U243'(a__isLNatKind'(V2), V1, V2)
a__U243'(tt', V1, V2) → a__U244'(a__isLNatKind'(V2), V1, V2)
a__U244'(tt', V1, V2) → a__U245'(a__isLNat'(V1), V2)
a__U245'(tt', V2) → a__U246'(a__isLNat'(V2))
a__U246'(tt') → tt'
a__U251'(tt', V1, V2) → a__U252'(a__isNaturalKind'(V1), V1, V2)
a__U252'(tt', V1, V2) → a__U253'(a__isLNatKind'(V2), V1, V2)
a__U253'(tt', V1, V2) → a__U254'(a__isLNatKind'(V2), V1, V2)
a__U254'(tt', V1, V2) → a__U255'(a__isNatural'(V1), V2)
a__U255'(tt', V2) → a__U256'(a__isLNat'(V2))
a__U256'(tt') → tt'
a__U261'(tt', V2) → a__U262'(a__isLNatKind'(V2))
a__U262'(tt') → tt'
a__U271'(tt', V2) → a__U272'(a__isLNatKind'(V2))
a__U272'(tt') → tt'
a__U281'(tt', N) → a__U282'(a__isNaturalKind'(N), N)
a__U282'(tt', N) → cons'(mark'(N), natsFrom'(s'(N)))
a__U291'(tt', N, XS) → a__U292'(a__isNaturalKind'(N), N, XS)
a__U292'(tt', N, XS) → a__U293'(a__isLNat'(XS), N, XS)
a__U293'(tt', N, XS) → a__U294'(a__isLNatKind'(XS), N, XS)
a__U294'(tt', N, XS) → a__head'(a__afterNth'(mark'(N), mark'(XS)))
a__U301'(tt', X, Y) → a__U302'(a__isLNatKind'(X), Y)
a__U302'(tt', Y) → a__U303'(a__isLNat'(Y), Y)
a__U303'(tt', Y) → a__U304'(a__isLNatKind'(Y), Y)
a__U304'(tt', Y) → mark'(Y)
a__U31'(tt', N, XS) → a__U32'(a__isNaturalKind'(N), N, XS)
a__U311'(tt', XS) → a__U312'(a__isLNatKind'(XS), XS)
a__U312'(tt', XS) → pair'(nil', mark'(XS))
a__U32'(tt', N, XS) → a__U33'(a__isLNat'(XS), N, XS)
a__U321'(tt', N, X, XS) → a__U322'(a__isNaturalKind'(N), N, X, XS)
a__U322'(tt', N, X, XS) → a__U323'(a__isNatural'(X), N, X, XS)
a__U323'(tt', N, X, XS) → a__U324'(a__isNaturalKind'(X), N, X, XS)
a__U324'(tt', N, X, XS) → a__U325'(a__isLNat'(XS), N, X, XS)
a__U325'(tt', N, X, XS) → a__U326'(a__isLNatKind'(XS), N, X, XS)
a__U326'(tt', N, X, XS) → a__U327'(a__splitAt'(mark'(N), mark'(XS)), X)
a__U327'(pair'(YS, ZS), X) → pair'(cons'(mark'(X), YS), mark'(ZS))
a__U33'(tt', N, XS) → a__U34'(a__isLNatKind'(XS), N)
a__U331'(tt', N, XS) → a__U332'(a__isNaturalKind'(N), XS)
a__U332'(tt', XS) → a__U333'(a__isLNat'(XS), XS)
a__U333'(tt', XS) → a__U334'(a__isLNatKind'(XS), XS)
a__U334'(tt', XS) → mark'(XS)
a__U34'(tt', N) → mark'(N)
a__U341'(tt', N, XS) → a__U342'(a__isNaturalKind'(N), N, XS)
a__U342'(tt', N, XS) → a__U343'(a__isLNat'(XS), N, XS)
a__U343'(tt', N, XS) → a__U344'(a__isLNatKind'(XS), N, XS)
a__U344'(tt', N, XS) → a__fst'(a__splitAt'(mark'(N), mark'(XS)))
a__U41'(tt', V1, V2) → a__U42'(a__isNaturalKind'(V1), V1, V2)
a__U42'(tt', V1, V2) → a__U43'(a__isLNatKind'(V2), V1, V2)
a__U43'(tt', V1, V2) → a__U44'(a__isLNatKind'(V2), V1, V2)
a__U44'(tt', V1, V2) → a__U45'(a__isNatural'(V1), V2)
a__U45'(tt', V2) → a__U46'(a__isLNat'(V2))
a__U46'(tt') → tt'
a__U51'(tt', V1, V2) → a__U52'(a__isNaturalKind'(V1), V1, V2)
a__U52'(tt', V1, V2) → a__U53'(a__isLNatKind'(V2), V1, V2)
a__U53'(tt', V1, V2) → a__U54'(a__isLNatKind'(V2), V1, V2)
a__U54'(tt', V1, V2) → a__U55'(a__isNatural'(V1), V2)
a__U55'(tt', V2) → a__U56'(a__isLNat'(V2))
a__U56'(tt') → tt'
a__U61'(tt', V1) → a__U62'(a__isPLNatKind'(V1), V1)
a__U62'(tt', V1) → a__U63'(a__isPLNat'(V1))
a__U63'(tt') → tt'
a__U71'(tt', V1) → a__U72'(a__isNaturalKind'(V1), V1)
a__U72'(tt', V1) → a__U73'(a__isNatural'(V1))
a__U73'(tt') → tt'
a__U81'(tt', V1) → a__U82'(a__isPLNatKind'(V1), V1)
a__U82'(tt', V1) → a__U83'(a__isPLNat'(V1))
a__U83'(tt') → tt'
a__U91'(tt', V1) → a__U92'(a__isLNatKind'(V1), V1)
a__U92'(tt', V1) → a__U93'(a__isLNat'(V1))
a__U93'(tt') → tt'
a__afterNth'(N, XS) → a__U11'(a__isNatural'(N), N, XS)
a__fst'(pair'(X, Y)) → a__U21'(a__isLNat'(X), X, Y)
a__head'(cons'(N, XS)) → a__U31'(a__isNatural'(N), N, XS)
a__isLNat'(nil') → tt'
a__isLNat'(afterNth'(V1, V2)) → a__U41'(a__isNaturalKind'(V1), V1, V2)
a__isLNat'(cons'(V1, V2)) → a__U51'(a__isNaturalKind'(V1), V1, V2)
a__isLNat'(fst'(V1)) → a__U61'(a__isPLNatKind'(V1), V1)
a__isLNat'(natsFrom'(V1)) → a__U71'(a__isNaturalKind'(V1), V1)
a__isLNat'(snd'(V1)) → a__U81'(a__isPLNatKind'(V1), V1)
a__isLNat'(tail'(V1)) → a__U91'(a__isLNatKind'(V1), V1)
a__isLNat'(take'(V1, V2)) → a__U101'(a__isNaturalKind'(V1), V1, V2)
a__isLNatKind'(nil') → tt'
a__isLNatKind'(afterNth'(V1, V2)) → a__U111'(a__isNaturalKind'(V1), V2)
a__isLNatKind'(cons'(V1, V2)) → a__U121'(a__isNaturalKind'(V1), V2)
a__isLNatKind'(fst'(V1)) → a__U131'(a__isPLNatKind'(V1))
a__isLNatKind'(natsFrom'(V1)) → a__U141'(a__isNaturalKind'(V1))
a__isLNatKind'(snd'(V1)) → a__U151'(a__isPLNatKind'(V1))
a__isLNatKind'(tail'(V1)) → a__U161'(a__isLNatKind'(V1))
a__isLNatKind'(take'(V1, V2)) → a__U171'(a__isNaturalKind'(V1), V2)
a__isNatural'(0') → tt'
a__isNatural'(head'(V1)) → a__U181'(a__isLNatKind'(V1), V1)
a__isNatural'(s'(V1)) → a__U191'(a__isNaturalKind'(V1), V1)
a__isNatural'(sel'(V1, V2)) → a__U201'(a__isNaturalKind'(V1), V1, V2)
a__isNaturalKind'(0') → tt'
a__isNaturalKind'(head'(V1)) → a__U211'(a__isLNatKind'(V1))
a__isNaturalKind'(s'(V1)) → a__U221'(a__isNaturalKind'(V1))
a__isNaturalKind'(sel'(V1, V2)) → a__U231'(a__isNaturalKind'(V1), V2)
a__isPLNat'(pair'(V1, V2)) → a__U241'(a__isLNatKind'(V1), V1, V2)
a__isPLNat'(splitAt'(V1, V2)) → a__U251'(a__isNaturalKind'(V1), V1, V2)
a__isPLNatKind'(pair'(V1, V2)) → a__U261'(a__isLNatKind'(V1), V2)
a__isPLNatKind'(splitAt'(V1, V2)) → a__U271'(a__isNaturalKind'(V1), V2)
a__natsFrom'(N) → a__U281'(a__isNatural'(N), N)
a__sel'(N, XS) → a__U291'(a__isNatural'(N), N, XS)
a__snd'(pair'(X, Y)) → a__U301'(a__isLNat'(X), X, Y)
a__splitAt'(0', XS) → a__U311'(a__isLNat'(XS), XS)
a__splitAt'(s'(N), cons'(X, XS)) → a__U321'(a__isNatural'(N), N, X, XS)
a__tail'(cons'(N, XS)) → a__U331'(a__isNatural'(N), N, XS)
a__take'(N, XS) → a__U341'(a__isNatural'(N), N, XS)
mark'(U101'(X1, X2, X3)) → a__U101'(mark'(X1), X2, X3)
mark'(U102'(X1, X2, X3)) → a__U102'(mark'(X1), X2, X3)
mark'(isNaturalKind'(X)) → a__isNaturalKind'(X)
mark'(U103'(X1, X2, X3)) → a__U103'(mark'(X1), X2, X3)
mark'(isLNatKind'(X)) → a__isLNatKind'(X)
mark'(U104'(X1, X2, X3)) → a__U104'(mark'(X1), X2, X3)
mark'(U105'(X1, X2)) → a__U105'(mark'(X1), X2)
mark'(isNatural'(X)) → a__isNatural'(X)
mark'(U106'(X)) → a__U106'(mark'(X))
mark'(isLNat'(X)) → a__isLNat'(X)
mark'(U11'(X1, X2, X3)) → a__U11'(mark'(X1), X2, X3)
mark'(U12'(X1, X2, X3)) → a__U12'(mark'(X1), X2, X3)
mark'(U111'(X1, X2)) → a__U111'(mark'(X1), X2)
mark'(U112'(X)) → a__U112'(mark'(X))
mark'(U13'(X1, X2, X3)) → a__U13'(mark'(X1), X2, X3)
mark'(U121'(X1, X2)) → a__U121'(mark'(X1), X2)
mark'(U122'(X)) → a__U122'(mark'(X))
mark'(U14'(X1, X2, X3)) → a__U14'(mark'(X1), X2, X3)
mark'(U131'(X)) → a__U131'(mark'(X))
mark'(snd'(X)) → a__snd'(mark'(X))
mark'(splitAt'(X1, X2)) → a__splitAt'(mark'(X1), mark'(X2))
mark'(U141'(X)) → a__U141'(mark'(X))
mark'(U151'(X)) → a__U151'(mark'(X))
mark'(U161'(X)) → a__U161'(mark'(X))
mark'(U171'(X1, X2)) → a__U171'(mark'(X1), X2)
mark'(U172'(X)) → a__U172'(mark'(X))
mark'(U181'(X1, X2)) → a__U181'(mark'(X1), X2)
mark'(U182'(X1, X2)) → a__U182'(mark'(X1), X2)
mark'(U183'(X)) → a__U183'(mark'(X))
mark'(U191'(X1, X2)) → a__U191'(mark'(X1), X2)
mark'(U192'(X1, X2)) → a__U192'(mark'(X1), X2)
mark'(U193'(X)) → a__U193'(mark'(X))
mark'(U201'(X1, X2, X3)) → a__U201'(mark'(X1), X2, X3)
mark'(U202'(X1, X2, X3)) → a__U202'(mark'(X1), X2, X3)
mark'(U203'(X1, X2, X3)) → a__U203'(mark'(X1), X2, X3)
mark'(U204'(X1, X2, X3)) → a__U204'(mark'(X1), X2, X3)
mark'(U205'(X1, X2)) → a__U205'(mark'(X1), X2)
mark'(U206'(X)) → a__U206'(mark'(X))
mark'(U21'(X1, X2, X3)) → a__U21'(mark'(X1), X2, X3)
mark'(U22'(X1, X2, X3)) → a__U22'(mark'(X1), X2, X3)
mark'(U211'(X)) → a__U211'(mark'(X))
mark'(U23'(X1, X2, X3)) → a__U23'(mark'(X1), X2, X3)
mark'(U221'(X)) → a__U221'(mark'(X))
mark'(U24'(X1, X2)) → a__U24'(mark'(X1), X2)
mark'(U231'(X1, X2)) → a__U231'(mark'(X1), X2)
mark'(U232'(X)) → a__U232'(mark'(X))
mark'(U241'(X1, X2, X3)) → a__U241'(mark'(X1), X2, X3)
mark'(U242'(X1, X2, X3)) → a__U242'(mark'(X1), X2, X3)
mark'(U243'(X1, X2, X3)) → a__U243'(mark'(X1), X2, X3)
mark'(U244'(X1, X2, X3)) → a__U244'(mark'(X1), X2, X3)
mark'(U245'(X1, X2)) → a__U245'(mark'(X1), X2)
mark'(U246'(X)) → a__U246'(mark'(X))
mark'(U251'(X1, X2, X3)) → a__U251'(mark'(X1), X2, X3)
mark'(U252'(X1, X2, X3)) → a__U252'(mark'(X1), X2, X3)
mark'(U253'(X1, X2, X3)) → a__U253'(mark'(X1), X2, X3)
mark'(U254'(X1, X2, X3)) → a__U254'(mark'(X1), X2, X3)
mark'(U255'(X1, X2)) → a__U255'(mark'(X1), X2)
mark'(U256'(X)) → a__U256'(mark'(X))
mark'(U261'(X1, X2)) → a__U261'(mark'(X1), X2)
mark'(U262'(X)) → a__U262'(mark'(X))
mark'(U271'(X1, X2)) → a__U271'(mark'(X1), X2)
mark'(U272'(X)) → a__U272'(mark'(X))
mark'(U281'(X1, X2)) → a__U281'(mark'(X1), X2)
mark'(U282'(X1, X2)) → a__U282'(mark'(X1), X2)
mark'(natsFrom'(X)) → a__natsFrom'(mark'(X))
mark'(U291'(X1, X2, X3)) → a__U291'(mark'(X1), X2, X3)
mark'(U292'(X1, X2, X3)) → a__U292'(mark'(X1), X2, X3)
mark'(U293'(X1, X2, X3)) → a__U293'(mark'(X1), X2, X3)
mark'(U294'(X1, X2, X3)) → a__U294'(mark'(X1), X2, X3)
mark'(head'(X)) → a__head'(mark'(X))
mark'(afterNth'(X1, X2)) → a__afterNth'(mark'(X1), mark'(X2))
mark'(U301'(X1, X2, X3)) → a__U301'(mark'(X1), X2, X3)
mark'(U302'(X1, X2)) → a__U302'(mark'(X1), X2)
mark'(U303'(X1, X2)) → a__U303'(mark'(X1), X2)
mark'(U304'(X1, X2)) → a__U304'(mark'(X1), X2)
mark'(U31'(X1, X2, X3)) → a__U31'(mark'(X1), X2, X3)
mark'(U32'(X1, X2, X3)) → a__U32'(mark'(X1), X2, X3)
mark'(U311'(X1, X2)) → a__U311'(mark'(X1), X2)
mark'(U312'(X1, X2)) → a__U312'(mark'(X1), X2)
mark'(U33'(X1, X2, X3)) → a__U33'(mark'(X1), X2, X3)
mark'(U321'(X1, X2, X3, X4)) → a__U321'(mark'(X1), X2, X3, X4)
mark'(U322'(X1, X2, X3, X4)) → a__U322'(mark'(X1), X2, X3, X4)
mark'(U323'(X1, X2, X3, X4)) → a__U323'(mark'(X1), X2, X3, X4)
mark'(U324'(X1, X2, X3, X4)) → a__U324'(mark'(X1), X2, X3, X4)
mark'(U325'(X1, X2, X3, X4)) → a__U325'(mark'(X1), X2, X3, X4)
mark'(U326'(X1, X2, X3, X4)) → a__U326'(mark'(X1), X2, X3, X4)
mark'(U327'(X1, X2)) → a__U327'(mark'(X1), X2)
mark'(U34'(X1, X2)) → a__U34'(mark'(X1), X2)
mark'(U331'(X1, X2, X3)) → a__U331'(mark'(X1), X2, X3)
mark'(U332'(X1, X2)) → a__U332'(mark'(X1), X2)
mark'(U333'(X1, X2)) → a__U333'(mark'(X1), X2)
mark'(U334'(X1, X2)) → a__U334'(mark'(X1), X2)
mark'(U341'(X1, X2, X3)) → a__U341'(mark'(X1), X2, X3)
mark'(U342'(X1, X2, X3)) → a__U342'(mark'(X1), X2, X3)
mark'(U343'(X1, X2, X3)) → a__U343'(mark'(X1), X2, X3)
mark'(U344'(X1, X2, X3)) → a__U344'(mark'(X1), X2, X3)
mark'(fst'(X)) → a__fst'(mark'(X))
mark'(U41'(X1, X2, X3)) → a__U41'(mark'(X1), X2, X3)
mark'(U42'(X1, X2, X3)) → a__U42'(mark'(X1), X2, X3)
mark'(U43'(X1, X2, X3)) → a__U43'(mark'(X1), X2, X3)
mark'(U44'(X1, X2, X3)) → a__U44'(mark'(X1), X2, X3)
mark'(U45'(X1, X2)) → a__U45'(mark'(X1), X2)
mark'(U46'(X)) → a__U46'(mark'(X))
mark'(U51'(X1, X2, X3)) → a__U51'(mark'(X1), X2, X3)
mark'(U52'(X1, X2, X3)) → a__U52'(mark'(X1), X2, X3)
mark'(U53'(X1, X2, X3)) → a__U53'(mark'(X1), X2, X3)
mark'(U54'(X1, X2, X3)) → a__U54'(mark'(X1), X2, X3)
mark'(U55'(X1, X2)) → a__U55'(mark'(X1), X2)
mark'(U56'(X)) → a__U56'(mark'(X))
mark'(U61'(X1, X2)) → a__U61'(mark'(X1), X2)
mark'(U62'(X1, X2)) → a__U62'(mark'(X1), X2)
mark'(isPLNatKind'(X)) → a__isPLNatKind'(X)
mark'(U63'(X)) → a__U63'(mark'(X))
mark'(isPLNat'(X)) → a__isPLNat'(X)
mark'(U71'(X1, X2)) → a__U71'(mark'(X1), X2)
mark'(U72'(X1, X2)) → a__U72'(mark'(X1), X2)
mark'(U73'(X)) → a__U73'(mark'(X))
mark'(U81'(X1, X2)) → a__U81'(mark'(X1), X2)
mark'(U82'(X1, X2)) → a__U82'(mark'(X1), X2)
mark'(U83'(X)) → a__U83'(mark'(X))
mark'(U91'(X1, X2)) → a__U91'(mark'(X1), X2)
mark'(U92'(X1, X2)) → a__U92'(mark'(X1), X2)
mark'(U93'(X)) → a__U93'(mark'(X))
mark'(tail'(X)) → a__tail'(mark'(X))
mark'(take'(X1, X2)) → a__take'(mark'(X1), mark'(X2))
mark'(sel'(X1, X2)) → a__sel'(mark'(X1), mark'(X2))
mark'(tt') → tt'
mark'(cons'(X1, X2)) → cons'(mark'(X1), X2)
mark'(s'(X)) → s'(mark'(X))
mark'(pair'(X1, X2)) → pair'(mark'(X1), mark'(X2))
mark'(nil') → nil'
mark'(0') → 0'
a__U101'(X1, X2, X3) → U101'(X1, X2, X3)
a__U102'(X1, X2, X3) → U102'(X1, X2, X3)
a__isNaturalKind'(X) → isNaturalKind'(X)
a__U103'(X1, X2, X3) → U103'(X1, X2, X3)
a__isLNatKind'(X) → isLNatKind'(X)
a__U104'(X1, X2, X3) → U104'(X1, X2, X3)
a__U105'(X1, X2) → U105'(X1, X2)
a__isNatural'(X) → isNatural'(X)
a__U106'(X) → U106'(X)
a__isLNat'(X) → isLNat'(X)
a__U11'(X1, X2, X3) → U11'(X1, X2, X3)
a__U12'(X1, X2, X3) → U12'(X1, X2, X3)
a__U111'(X1, X2) → U111'(X1, X2)
a__U112'(X) → U112'(X)
a__U13'(X1, X2, X3) → U13'(X1, X2, X3)
a__U121'(X1, X2) → U121'(X1, X2)
a__U122'(X) → U122'(X)
a__U14'(X1, X2, X3) → U14'(X1, X2, X3)
a__U131'(X) → U131'(X)
a__snd'(X) → snd'(X)
a__splitAt'(X1, X2) → splitAt'(X1, X2)
a__U141'(X) → U141'(X)
a__U151'(X) → U151'(X)
a__U161'(X) → U161'(X)
a__U171'(X1, X2) → U171'(X1, X2)
a__U172'(X) → U172'(X)
a__U181'(X1, X2) → U181'(X1, X2)
a__U182'(X1, X2) → U182'(X1, X2)
a__U183'(X) → U183'(X)
a__U191'(X1, X2) → U191'(X1, X2)
a__U192'(X1, X2) → U192'(X1, X2)
a__U193'(X) → U193'(X)
a__U201'(X1, X2, X3) → U201'(X1, X2, X3)
a__U202'(X1, X2, X3) → U202'(X1, X2, X3)
a__U203'(X1, X2, X3) → U203'(X1, X2, X3)
a__U204'(X1, X2, X3) → U204'(X1, X2, X3)
a__U205'(X1, X2) → U205'(X1, X2)
a__U206'(X) → U206'(X)
a__U21'(X1, X2, X3) → U21'(X1, X2, X3)
a__U22'(X1, X2, X3) → U22'(X1, X2, X3)
a__U211'(X) → U211'(X)
a__U23'(X1, X2, X3) → U23'(X1, X2, X3)
a__U221'(X) → U221'(X)
a__U24'(X1, X2) → U24'(X1, X2)
a__U231'(X1, X2) → U231'(X1, X2)
a__U232'(X) → U232'(X)
a__U241'(X1, X2, X3) → U241'(X1, X2, X3)
a__U242'(X1, X2, X3) → U242'(X1, X2, X3)
a__U243'(X1, X2, X3) → U243'(X1, X2, X3)
a__U244'(X1, X2, X3) → U244'(X1, X2, X3)
a__U245'(X1, X2) → U245'(X1, X2)
a__U246'(X) → U246'(X)
a__U251'(X1, X2, X3) → U251'(X1, X2, X3)
a__U252'(X1, X2, X3) → U252'(X1, X2, X3)
a__U253'(X1, X2, X3) → U253'(X1, X2, X3)
a__U254'(X1, X2, X3) → U254'(X1, X2, X3)
a__U255'(X1, X2) → U255'(X1, X2)
a__U256'(X) → U256'(X)
a__U261'(X1, X2) → U261'(X1, X2)
a__U262'(X) → U262'(X)
a__U271'(X1, X2) → U271'(X1, X2)
a__U272'(X) → U272'(X)
a__U281'(X1, X2) → U281'(X1, X2)
a__U282'(X1, X2) → U282'(X1, X2)
a__natsFrom'(X) → natsFrom'(X)
a__U291'(X1, X2, X3) → U291'(X1, X2, X3)
a__U292'(X1, X2, X3) → U292'(X1, X2, X3)
a__U293'(X1, X2, X3) → U293'(X1, X2, X3)
a__U294'(X1, X2, X3) → U294'(X1, X2, X3)
a__head'(X) → head'(X)
a__afterNth'(X1, X2) → afterNth'(X1, X2)
a__U301'(X1, X2, X3) → U301'(X1, X2, X3)
a__U302'(X1, X2) → U302'(X1, X2)
a__U303'(X1, X2) → U303'(X1, X2)
a__U304'(X1, X2) → U304'(X1, X2)
a__U31'(X1, X2, X3) → U31'(X1, X2, X3)
a__U32'(X1, X2, X3) → U32'(X1, X2, X3)
a__U311'(X1, X2) → U311'(X1, X2)
a__U312'(X1, X2) → U312'(X1, X2)
a__U33'(X1, X2, X3) → U33'(X1, X2, X3)
a__U321'(X1, X2, X3, X4) → U321'(X1, X2, X3, X4)
a__U322'(X1, X2, X3, X4) → U322'(X1, X2, X3, X4)
a__U323'(X1, X2, X3, X4) → U323'(X1, X2, X3, X4)
a__U324'(X1, X2, X3, X4) → U324'(X1, X2, X3, X4)
a__U325'(X1, X2, X3, X4) → U325'(X1, X2, X3, X4)
a__U326'(X1, X2, X3, X4) → U326'(X1, X2, X3, X4)
a__U327'(X1, X2) → U327'(X1, X2)
a__U34'(X1, X2) → U34'(X1, X2)
a__U331'(X1, X2, X3) → U331'(X1, X2, X3)
a__U332'(X1, X2) → U332'(X1, X2)
a__U333'(X1, X2) → U333'(X1, X2)
a__U334'(X1, X2) → U334'(X1, X2)
a__U341'(X1, X2, X3) → U341'(X1, X2, X3)
a__U342'(X1, X2, X3) → U342'(X1, X2, X3)
a__U343'(X1, X2, X3) → U343'(X1, X2, X3)
a__U344'(X1, X2, X3) → U344'(X1, X2, X3)
a__fst'(X) → fst'(X)
a__U41'(X1, X2, X3) → U41'(X1, X2, X3)
a__U42'(X1, X2, X3) → U42'(X1, X2, X3)
a__U43'(X1, X2, X3) → U43'(X1, X2, X3)
a__U44'(X1, X2, X3) → U44'(X1, X2, X3)
a__U45'(X1, X2) → U45'(X1, X2)
a__U46'(X) → U46'(X)
a__U51'(X1, X2, X3) → U51'(X1, X2, X3)
a__U52'(X1, X2, X3) → U52'(X1, X2, X3)
a__U53'(X1, X2, X3) → U53'(X1, X2, X3)
a__U54'(X1, X2, X3) → U54'(X1, X2, X3)
a__U55'(X1, X2) → U55'(X1, X2)
a__U56'(X) → U56'(X)
a__U61'(X1, X2) → U61'(X1, X2)
a__U62'(X1, X2) → U62'(X1, X2)
a__isPLNatKind'(X) → isPLNatKind'(X)
a__U63'(X) → U63'(X)
a__isPLNat'(X) → isPLNat'(X)
a__U71'(X1, X2) → U71'(X1, X2)
a__U72'(X1, X2) → U72'(X1, X2)
a__U73'(X) → U73'(X)
a__U81'(X1, X2) → U81'(X1, X2)
a__U82'(X1, X2) → U82'(X1, X2)
a__U83'(X) → U83'(X)
a__U91'(X1, X2) → U91'(X1, X2)
a__U92'(X1, X2) → U92'(X1, X2)
a__U93'(X) → U93'(X)
a__tail'(X) → tail'(X)
a__take'(X1, X2) → take'(X1, X2)
a__sel'(X1, X2) → sel'(X1, X2)

Rewrite Strategy: INNERMOST


Infered types.