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__U202#(tt, N, X, XS) | → | a__U203#(a__isLNat(XS), N, X, XS) | mark#(U151(X1, X2)) | → | mark#(X1) | |
| mark#(U142(X)) | → | a__U142#(mark(X)) | mark#(U102(X)) | → | mark#(X) | |
| a__isNatural#(head(V1)) | → | a__isLNat#(V1) | mark#(U132(X)) | → | mark#(X) | |
| mark#(U131(X1, X2)) | → | a__U131#(mark(X1), X2) | mark#(U91(X)) | → | a__U91#(mark(X)) | |
| mark#(U12(X1, X2, X3)) | → | a__U12#(mark(X1), X2, X3) | mark#(U121(X)) | → | mark#(X) | |
| mark#(s(X)) | → | mark#(X) | mark#(sel(X1, X2)) | → | mark#(X1) | |
| a__U31#(tt, N, XS) | → | a__isLNat#(XS) | mark#(U203(X1, X2, X3, X4)) | → | mark#(X1) | |
| mark#(U132(X)) | → | a__U132#(mark(X)) | mark#(U204(X1, X2)) | → | mark#(X1) | |
| mark#(U171(X1, X2, X3)) | → | mark#(X1) | mark#(afterNth(X1, X2)) | → | mark#(X1) | |
| mark#(U52(X)) | → | mark#(X) | a__tail#(cons(N, XS)) | → | a__U211#(a__isNatural(N), XS) | |
| a__U141#(tt, V2) | → | a__isLNat#(V2) | a__U21#(tt, X, Y) | → | a__U22#(a__isLNat(Y), X) | |
| mark#(U11(X1, X2, X3)) | → | mark#(X1) | a__U22#(tt, X) | → | mark#(X) | |
| a__U181#(tt, Y) | → | a__U182#(a__isLNat(Y), Y) | a__U12#(tt, N, XS) | → | mark#(XS) | |
| a__U203#(tt, N, X, XS) | → | a__splitAt#(mark(N), mark(XS)) | mark#(U211(X1, X2)) | → | a__U211#(mark(X1), X2) | |
| a__U172#(tt, N, XS) | → | a__head#(a__afterNth(mark(N), mark(XS))) | a__U151#(tt, V2) | → | a__isLNat#(V2) | |
| mark#(U111(X)) | → | mark#(X) | a__U211#(tt, XS) | → | a__isLNat#(XS) | |
| mark#(head(X)) | → | mark#(X) | mark#(U22(X1, X2)) | → | mark#(X1) | |
| mark#(splitAt(X1, X2)) | → | mark#(X1) | mark#(isPLNat(X)) | → | a__isPLNat#(X) | |
| mark#(isNatural(X)) | → | a__isNatural#(X) | mark#(fst(X)) | → | a__fst#(mark(X)) | |
| a__U12#(tt, N, XS) | → | mark#(N) | mark#(U41(X1, X2)) | → | mark#(X1) | |
| mark#(U61(X)) | → | mark#(X) | mark#(fst(X)) | → | mark#(X) | |
| a__U141#(tt, V2) | → | a__U142#(a__isLNat(V2)) | mark#(U51(X1, X2)) | → | a__U51#(mark(X1), X2) | |
| mark#(U221(X1, X2, X3)) | → | mark#(X1) | a__splitAt#(s(N), cons(X, XS)) | → | a__isNatural#(N) | |
| mark#(snd(X)) | → | mark#(X) | mark#(U21(X1, X2, X3)) | → | a__U21#(mark(X1), X2, X3) | |
| mark#(natsFrom(X)) | → | mark#(X) | a__U191#(tt, XS) | → | mark#(XS) | |
| mark#(U201(X1, X2, X3, X4)) | → | mark#(X1) | a__isNatural#(head(V1)) | → | a__U111#(a__isLNat(V1)) | |
| mark#(U111(X)) | → | a__U111#(mark(X)) | a__U222#(tt, N, XS) | → | mark#(XS) | |
| mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) | a__U221#(tt, N, XS) | → | a__U222#(a__isLNat(XS), N, XS) | |
| mark#(splitAt(X1, X2)) | → | a__splitAt#(mark(X1), mark(X2)) | mark#(U172(X1, X2, X3)) | → | mark#(X1) | |
| mark#(U191(X1, X2)) | → | mark#(X1) | mark#(U101(X1, X2)) | → | mark#(X1) | |
| a__isLNat#(tail(V1)) | → | a__U91#(a__isLNat(V1)) | a__isLNat#(fst(V1)) | → | a__isPLNat#(V1) | |
| mark#(take(X1, X2)) | → | mark#(X1) | a__sel#(N, XS) | → | a__isNatural#(N) | |
| a__U101#(tt, V2) | → | a__isLNat#(V2) | a__isLNat#(afterNth(V1, V2)) | → | a__U41#(a__isNatural(V1), V2) | |
| a__U101#(tt, V2) | → | a__U102#(a__isLNat(V2)) | a__U222#(tt, N, XS) | → | a__fst#(a__splitAt(mark(N), mark(XS))) | |
| mark#(U203(X1, X2, X3, X4)) | → | a__U203#(mark(X1), X2, X3, X4) | mark#(U41(X1, X2)) | → | a__U41#(mark(X1), X2) | |
| a__isLNat#(fst(V1)) | → | a__U61#(a__isPLNat(V1)) | a__U222#(tt, N, XS) | → | mark#(N) | |
| mark#(U204(X1, X2)) | → | a__U204#(mark(X1), X2) | mark#(U131(X1, X2)) | → | mark#(X1) | |
| mark#(U32(X1, X2)) | → | a__U32#(mark(X1), X2) | a__fst#(pair(X, Y)) | → | a__isLNat#(X) | |
| a__U171#(tt, N, XS) | → | a__U172#(a__isLNat(XS), N, XS) | mark#(U31(X1, X2, X3)) | → | mark#(X1) | |
| a__U172#(tt, N, XS) | → | a__afterNth#(mark(N), mark(XS)) | a__isLNat#(snd(V1)) | → | a__U81#(a__isPLNat(V1)) | |
| mark#(U42(X)) | → | a__U42#(mark(X)) | mark#(U211(X1, X2)) | → | mark#(X1) | |
| mark#(U11(X1, X2, X3)) | → | a__U11#(mark(X1), X2, X3) | a__U51#(tt, V2) | → | a__U52#(a__isLNat(V2)) | |
| a__U21#(tt, X, Y) | → | a__isLNat#(Y) | a__U31#(tt, N, XS) | → | a__U32#(a__isLNat(XS), N) | |
| a__U222#(tt, N, XS) | → | a__splitAt#(mark(N), mark(XS)) | mark#(U181(X1, X2)) | → | mark#(X1) | |
| mark#(U42(X)) | → | mark#(X) | mark#(U221(X1, X2, X3)) | → | a__U221#(mark(X1), X2, X3) | |
| a__U182#(tt, Y) | → | mark#(Y) | mark#(U172(X1, X2, X3)) | → | a__U172#(mark(X1), X2, X3) | |
| mark#(sel(X1, X2)) | → | mark#(X2) | a__isLNat#(afterNth(V1, V2)) | → | a__isNatural#(V1) | |
| a__U221#(tt, N, XS) | → | a__isLNat#(XS) | mark#(tail(X)) | → | a__tail#(mark(X)) | |
| mark#(U12(X1, X2, X3)) | → | mark#(X1) | a__U201#(tt, N, X, XS) | → | a__U202#(a__isNatural(X), N, X, XS) | |
| a__U172#(tt, N, XS) | → | mark#(N) | mark#(splitAt(X1, X2)) | → | mark#(X2) | |
| a__isLNat#(cons(V1, V2)) | → | a__U51#(a__isNatural(V1), V2) | a__U41#(tt, V2) | → | a__isLNat#(V2) | |
| a__isNatural#(sel(V1, V2)) | → | a__U131#(a__isNatural(V1), V2) | mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | |
| mark#(natsFrom(X)) | → | a__natsFrom#(mark(X)) | mark#(U142(X)) | → | mark#(X) | |
| mark#(pair(X1, X2)) | → | mark#(X2) | a__natsFrom#(N) | → | a__U161#(a__isNatural(N), N) | |
| a__head#(cons(N, XS)) | → | a__U31#(a__isNatural(N), N, XS) | a__U12#(tt, N, XS) | → | a__splitAt#(mark(N), mark(XS)) | |
| a__isLNat#(tail(V1)) | → | a__isLNat#(V1) | a__snd#(pair(X, Y)) | → | a__isLNat#(X) | |
| a__snd#(pair(X, Y)) | → | a__U181#(a__isLNat(X), Y) | a__U203#(tt, N, X, XS) | → | mark#(N) | |
| a__U11#(tt, N, XS) | → | a__isLNat#(XS) | mark#(cons(X1, X2)) | → | mark#(X1) | |
| a__splitAt#(0, XS) | → | a__isLNat#(XS) | a__splitAt#(s(N), cons(X, XS)) | → | a__U201#(a__isNatural(N), N, X, XS) | |
| mark#(pair(X1, X2)) | → | mark#(X1) | a__isLNat#(take(V1, V2)) | → | a__U101#(a__isNatural(V1), V2) | |
| mark#(U161(X1, X2)) | → | a__U161#(mark(X1), X2) | mark#(tail(X)) | → | mark#(X) | |
| a__sel#(N, XS) | → | a__U171#(a__isNatural(N), N, XS) | a__head#(cons(N, XS)) | → | a__isNatural#(N) | |
| mark#(U32(X1, X2)) | → | mark#(X1) | mark#(afterNth(X1, X2)) | → | mark#(X2) | |
| a__isPLNat#(pair(V1, V2)) | → | a__U141#(a__isLNat(V1), V2) | a__isPLNat#(splitAt(V1, V2)) | → | a__U151#(a__isNatural(V1), V2) | |
| a__U171#(tt, N, XS) | → | a__isLNat#(XS) | mark#(U181(X1, X2)) | → | a__U181#(mark(X1), X2) | |
| a__afterNth#(N, XS) | → | a__isNatural#(N) | mark#(U152(X)) | → | a__U152#(mark(X)) | |
| mark#(head(X)) | → | a__head#(mark(X)) | a__U11#(tt, N, XS) | → | a__U12#(a__isLNat(XS), N, XS) | |
| mark#(U61(X)) | → | a__U61#(mark(X)) | a__tail#(cons(N, XS)) | → | a__isNatural#(N) | |
| a__U151#(tt, V2) | → | a__U152#(a__isLNat(V2)) | mark#(U31(X1, X2, X3)) | → | a__U31#(mark(X1), X2, X3) | |
| a__isLNat#(cons(V1, V2)) | → | a__isNatural#(V1) | a__U32#(tt, N) | → | mark#(N) | |
| a__isLNat#(take(V1, V2)) | → | a__isNatural#(V1) | a__U172#(tt, N, XS) | → | mark#(XS) | |
| mark#(U52(X)) | → | a__U52#(mark(X)) | mark#(U71(X)) | → | a__U71#(mark(X)) | |
| mark#(U71(X)) | → | mark#(X) | a__U212#(tt, XS) | → | mark#(XS) | |
| a__U12#(tt, N, XS) | → | a__snd#(a__splitAt(mark(N), mark(XS))) | mark#(afterNth(X1, X2)) | → | a__afterNth#(mark(X1), mark(X2)) | |
| mark#(U212(X1, X2)) | → | a__U212#(mark(X1), X2) | a__take#(N, XS) | → | a__isNatural#(N) | |
| mark#(U22(X1, X2)) | → | a__U22#(mark(X1), X2) | mark#(U141(X1, X2)) | → | a__U141#(mark(X1), X2) | |
| a__U181#(tt, Y) | → | a__isLNat#(Y) | mark#(U102(X)) | → | a__U102#(mark(X)) | |
| mark#(U121(X)) | → | a__U121#(mark(X)) | mark#(U81(X)) | → | mark#(X) | |
| mark#(U191(X1, X2)) | → | a__U191#(mark(X1), X2) | a__isLNat#(snd(V1)) | → | a__isPLNat#(V1) | |
| a__U201#(tt, N, X, XS) | → | a__isNatural#(X) | mark#(U202(X1, X2, X3, X4)) | → | a__U202#(mark(X1), X2, X3, X4) | |
| mark#(U212(X1, X2)) | → | mark#(X1) | a__isNatural#(s(V1)) | → | a__isNatural#(V1) | |
| a__isPLNat#(splitAt(V1, V2)) | → | a__isNatural#(V1) | a__U202#(tt, N, X, XS) | → | a__isLNat#(XS) | |
| mark#(U101(X1, X2)) | → | a__U101#(mark(X1), X2) | a__isNatural#(s(V1)) | → | a__U121#(a__isNatural(V1)) | |
| a__U204#(pair(YS, ZS), X) | → | mark#(ZS) | a__isLNat#(natsFrom(V1)) | → | a__isNatural#(V1) | |
| mark#(isLNat(X)) | → | a__isLNat#(X) | a__U211#(tt, XS) | → | a__U212#(a__isLNat(XS), XS) | |
| mark#(U161(X1, X2)) | → | mark#(X1) | mark#(U182(X1, X2)) | → | mark#(X1) | |
| mark#(snd(X)) | → | a__snd#(mark(X)) | mark#(U21(X1, X2, X3)) | → | mark#(X1) | |
| a__U51#(tt, V2) | → | a__isLNat#(V2) | a__U204#(pair(YS, ZS), X) | → | mark#(X) | |
| mark#(U171(X1, X2, X3)) | → | a__U171#(mark(X1), X2, X3) | mark#(U202(X1, X2, X3, X4)) | → | mark#(X1) | |
| mark#(U51(X1, X2)) | → | mark#(X1) | a__isNatural#(sel(V1, V2)) | → | a__isNatural#(V1) | |
| a__splitAt#(0, XS) | → | a__U191#(a__isLNat(XS), XS) | mark#(U222(X1, X2, X3)) | → | a__U222#(mark(X1), X2, X3) | |
| a__U131#(tt, V2) | → | a__isLNat#(V2) | a__U41#(tt, V2) | → | a__U42#(a__isLNat(V2)) | |
| mark#(U152(X)) | → | mark#(X) | mark#(U151(X1, X2)) | → | a__U151#(mark(X1), X2) | |
| a__U161#(tt, N) | → | mark#(N) | a__isLNat#(natsFrom(V1)) | → | a__U71#(a__isNatural(V1)) | |
| a__afterNth#(N, XS) | → | a__U11#(a__isNatural(N), N, XS) | a__U131#(tt, V2) | → | a__U132#(a__isLNat(V2)) | |
| mark#(U222(X1, X2, X3)) | → | mark#(X1) | a__take#(N, XS) | → | a__U221#(a__isNatural(N), N, XS) | |
| mark#(U141(X1, X2)) | → | mark#(X1) | a__fst#(pair(X, Y)) | → | a__U21#(a__isLNat(X), X, Y) | |
| mark#(U201(X1, X2, X3, X4)) | → | a__U201#(mark(X1), X2, X3, X4) | a__U203#(tt, N, X, XS) | → | mark#(XS) | |
| a__natsFrom#(N) | → | a__isNatural#(N) | mark#(U182(X1, X2)) | → | a__U182#(mark(X1), X2) | |
| mark#(take(X1, X2)) | → | mark#(X2) | a__isPLNat#(pair(V1, V2)) | → | a__isLNat#(V1) | |
| mark#(U81(X)) | → | a__U81#(mark(X)) | mark#(U91(X)) | → | mark#(X) | |
| a__U203#(tt, N, X, XS) | → | a__U204#(a__splitAt(mark(N), mark(XS)), X) |
| a__U101(tt, V2) | → | a__U102(a__isLNat(V2)) | a__U102(tt) | → | tt | |
| a__U11(tt, N, XS) | → | a__U12(a__isLNat(XS), N, XS) | a__U111(tt) | → | tt | |
| a__U12(tt, N, XS) | → | a__snd(a__splitAt(mark(N), mark(XS))) | a__U121(tt) | → | tt | |
| a__U131(tt, V2) | → | a__U132(a__isLNat(V2)) | a__U132(tt) | → | tt | |
| a__U141(tt, V2) | → | a__U142(a__isLNat(V2)) | a__U142(tt) | → | tt | |
| a__U151(tt, V2) | → | a__U152(a__isLNat(V2)) | a__U152(tt) | → | tt | |
| a__U161(tt, N) | → | cons(mark(N), natsFrom(s(N))) | a__U171(tt, N, XS) | → | a__U172(a__isLNat(XS), N, XS) | |
| a__U172(tt, N, XS) | → | a__head(a__afterNth(mark(N), mark(XS))) | a__U181(tt, Y) | → | a__U182(a__isLNat(Y), Y) | |
| a__U182(tt, Y) | → | mark(Y) | a__U191(tt, XS) | → | pair(nil, mark(XS)) | |
| a__U201(tt, N, X, XS) | → | a__U202(a__isNatural(X), N, X, XS) | a__U202(tt, N, X, XS) | → | a__U203(a__isLNat(XS), N, X, XS) | |
| a__U203(tt, N, X, XS) | → | a__U204(a__splitAt(mark(N), mark(XS)), X) | a__U204(pair(YS, ZS), X) | → | pair(cons(mark(X), YS), mark(ZS)) | |
| a__U21(tt, X, Y) | → | a__U22(a__isLNat(Y), X) | a__U211(tt, XS) | → | a__U212(a__isLNat(XS), XS) | |
| a__U212(tt, XS) | → | mark(XS) | a__U22(tt, X) | → | mark(X) | |
| a__U221(tt, N, XS) | → | a__U222(a__isLNat(XS), N, XS) | a__U222(tt, N, XS) | → | a__fst(a__splitAt(mark(N), mark(XS))) | |
| a__U31(tt, N, XS) | → | a__U32(a__isLNat(XS), N) | a__U32(tt, N) | → | mark(N) | |
| a__U41(tt, V2) | → | a__U42(a__isLNat(V2)) | a__U42(tt) | → | tt | |
| a__U51(tt, V2) | → | a__U52(a__isLNat(V2)) | a__U52(tt) | → | tt | |
| a__U61(tt) | → | tt | a__U71(tt) | → | tt | |
| a__U81(tt) | → | tt | a__U91(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__isNatural(V1), V2) | a__isLNat(cons(V1, V2)) | → | a__U51(a__isNatural(V1), V2) | |
| a__isLNat(fst(V1)) | → | a__U61(a__isPLNat(V1)) | a__isLNat(natsFrom(V1)) | → | a__U71(a__isNatural(V1)) | |
| a__isLNat(snd(V1)) | → | a__U81(a__isPLNat(V1)) | a__isLNat(tail(V1)) | → | a__U91(a__isLNat(V1)) | |
| a__isLNat(take(V1, V2)) | → | a__U101(a__isNatural(V1), V2) | a__isNatural(0) | → | tt | |
| a__isNatural(head(V1)) | → | a__U111(a__isLNat(V1)) | a__isNatural(s(V1)) | → | a__U121(a__isNatural(V1)) | |
| a__isNatural(sel(V1, V2)) | → | a__U131(a__isNatural(V1), V2) | a__isPLNat(pair(V1, V2)) | → | a__U141(a__isLNat(V1), V2) | |
| a__isPLNat(splitAt(V1, V2)) | → | a__U151(a__isNatural(V1), V2) | a__natsFrom(N) | → | a__U161(a__isNatural(N), N) | |
| a__sel(N, XS) | → | a__U171(a__isNatural(N), N, XS) | a__snd(pair(X, Y)) | → | a__U181(a__isLNat(X), Y) | |
| a__splitAt(0, XS) | → | a__U191(a__isLNat(XS), XS) | a__splitAt(s(N), cons(X, XS)) | → | a__U201(a__isNatural(N), N, X, XS) | |
| a__tail(cons(N, XS)) | → | a__U211(a__isNatural(N), XS) | a__take(N, XS) | → | a__U221(a__isNatural(N), N, XS) | |
| mark(U101(X1, X2)) | → | a__U101(mark(X1), X2) | mark(U102(X)) | → | a__U102(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(X)) | → | a__U111(mark(X)) | |
| mark(snd(X)) | → | a__snd(mark(X)) | mark(splitAt(X1, X2)) | → | a__splitAt(mark(X1), mark(X2)) | |
| mark(U121(X)) | → | a__U121(mark(X)) | mark(U131(X1, X2)) | → | a__U131(mark(X1), X2) | |
| mark(U132(X)) | → | a__U132(mark(X)) | mark(U141(X1, X2)) | → | a__U141(mark(X1), X2) | |
| mark(U142(X)) | → | a__U142(mark(X)) | mark(U151(X1, X2)) | → | a__U151(mark(X1), X2) | |
| mark(U152(X)) | → | a__U152(mark(X)) | mark(U161(X1, X2)) | → | a__U161(mark(X1), X2) | |
| mark(natsFrom(X)) | → | a__natsFrom(mark(X)) | mark(U171(X1, X2, X3)) | → | a__U171(mark(X1), X2, X3) | |
| mark(U172(X1, X2, X3)) | → | a__U172(mark(X1), X2, X3) | mark(head(X)) | → | a__head(mark(X)) | |
| mark(afterNth(X1, X2)) | → | a__afterNth(mark(X1), mark(X2)) | mark(U181(X1, X2)) | → | a__U181(mark(X1), X2) | |
| mark(U182(X1, X2)) | → | a__U182(mark(X1), X2) | mark(U191(X1, X2)) | → | a__U191(mark(X1), X2) | |
| mark(U201(X1, X2, X3, X4)) | → | a__U201(mark(X1), X2, X3, X4) | mark(U202(X1, X2, X3, X4)) | → | a__U202(mark(X1), X2, X3, X4) | |
| mark(isNatural(X)) | → | a__isNatural(X) | mark(U203(X1, X2, X3, X4)) | → | a__U203(mark(X1), X2, X3, X4) | |
| mark(U204(X1, X2)) | → | a__U204(mark(X1), X2) | mark(U21(X1, X2, X3)) | → | a__U21(mark(X1), X2, X3) | |
| mark(U22(X1, X2)) | → | a__U22(mark(X1), X2) | mark(U211(X1, X2)) | → | a__U211(mark(X1), X2) | |
| mark(U212(X1, X2)) | → | a__U212(mark(X1), X2) | mark(U221(X1, X2, X3)) | → | a__U221(mark(X1), X2, X3) | |
| mark(U222(X1, X2, X3)) | → | a__U222(mark(X1), X2, X3) | mark(fst(X)) | → | a__fst(mark(X)) | |
| mark(U31(X1, X2, X3)) | → | a__U31(mark(X1), X2, X3) | mark(U32(X1, X2)) | → | a__U32(mark(X1), X2) | |
| mark(U41(X1, X2)) | → | a__U41(mark(X1), X2) | mark(U42(X)) | → | a__U42(mark(X)) | |
| mark(U51(X1, X2)) | → | a__U51(mark(X1), X2) | mark(U52(X)) | → | a__U52(mark(X)) | |
| mark(U61(X)) | → | a__U61(mark(X)) | mark(U71(X)) | → | a__U71(mark(X)) | |
| mark(U81(X)) | → | a__U81(mark(X)) | mark(U91(X)) | → | a__U91(mark(X)) | |
| mark(isPLNat(X)) | → | a__isPLNat(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) | → | U101(X1, X2) | a__U102(X) | → | U102(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(X) | → | U111(X) | |
| a__snd(X) | → | snd(X) | a__splitAt(X1, X2) | → | splitAt(X1, X2) | |
| a__U121(X) | → | U121(X) | a__U131(X1, X2) | → | U131(X1, X2) | |
| a__U132(X) | → | U132(X) | a__U141(X1, X2) | → | U141(X1, X2) | |
| a__U142(X) | → | U142(X) | a__U151(X1, X2) | → | U151(X1, X2) | |
| a__U152(X) | → | U152(X) | a__U161(X1, X2) | → | U161(X1, X2) | |
| a__natsFrom(X) | → | natsFrom(X) | a__U171(X1, X2, X3) | → | U171(X1, X2, X3) | |
| a__U172(X1, X2, X3) | → | U172(X1, X2, X3) | a__head(X) | → | head(X) | |
| a__afterNth(X1, X2) | → | afterNth(X1, X2) | a__U181(X1, X2) | → | U181(X1, X2) | |
| a__U182(X1, X2) | → | U182(X1, X2) | a__U191(X1, X2) | → | U191(X1, X2) | |
| a__U201(X1, X2, X3, X4) | → | U201(X1, X2, X3, X4) | a__U202(X1, X2, X3, X4) | → | U202(X1, X2, X3, X4) | |
| a__isNatural(X) | → | isNatural(X) | a__U203(X1, X2, X3, X4) | → | U203(X1, X2, X3, X4) | |
| a__U204(X1, X2) | → | U204(X1, X2) | a__U21(X1, X2, X3) | → | U21(X1, X2, X3) | |
| a__U22(X1, X2) | → | U22(X1, X2) | a__U211(X1, X2) | → | U211(X1, X2) | |
| a__U212(X1, X2) | → | U212(X1, X2) | a__U221(X1, X2, X3) | → | U221(X1, X2, X3) | |
| a__U222(X1, X2, X3) | → | U222(X1, X2, X3) | a__fst(X) | → | fst(X) | |
| a__U31(X1, X2, X3) | → | U31(X1, X2, X3) | a__U32(X1, X2) | → | U32(X1, X2) | |
| a__U41(X1, X2) | → | U41(X1, X2) | a__U42(X) | → | U42(X) | |
| a__U51(X1, X2) | → | U51(X1, X2) | a__U52(X) | → | U52(X) | |
| a__U61(X) | → | U61(X) | a__U71(X) | → | U71(X) | |
| a__U81(X) | → | U81(X) | a__U91(X) | → | U91(X) | |
| a__isPLNat(X) | → | isPLNat(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__U121, U111, U61, a__isPLNat, a__U41, a__U42, a__isNatural, a__U191, a__U111, isPLNat, tail, U71, U191, 0, U121, a__U32, a__U31, a__sel, a__U141, a__U142, a__take, pair, U132, U131, U42, a__U91, U41, a__fst, a__U22, a__head, a__snd, a__U21, cons, a__afterNth, a__U131, a__U132, splitAt, U142, U141, U51, s, tt, U52, a__U12, a__U11, afterNth, natsFrom, a__natsFrom, U161, U204, U203, a__U161, fst, a__U222, U211, a__U221, U212, a__U71, head, U21, U22, a__U202, a__U203, a__U204, mark, U151, U152, a__U152, a__U151, a__U212, U221, a__U211, isLNat, U222, a__U81, U31, U32, a__U51, a__U52, U181, U182, a__U182, isNatural, a__U181, a__U201, U91, a__isLNat, a__U102, a__U101, snd, U171, U172, a__U171, a__U172, a__tail, U201, U202, a__splitAt, take, U81, U11, U12, a__U61, U102, sel, nil, U101