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