The rewrite relation of the following TRS is considered.
There are 168 ruless (increase limit for explicit display).
There are 203 ruless (increase limit for explicit display).
The dependency pairs are split into 2 components.
There are 127 ruless (increase limit for explicit display).
[U204(x1, x2)] | = | max(x1 + 0, x2 + 42, 0) |
[a__U151(x1, x2)] | = | max(x1 + 4, x2 + 13, 0) |
[a__U131#(x1, x2)] | = | max(0) |
[U21(x1, x2, x3)] | = | max(x1 + 26, x2 + 26, x3 + 24, 0) |
[a__U102(x1)] | = | x1 + 4 |
[a__U152(x1)] | = | x1 + 3 |
[U161(x1, x2)] | = | max(x1 + 9, x2 + 22, 0) |
[a__U71#(x1)] | = | 0 |
[U182(x1, x2)] | = | max(x1 + 3, x2 + 2, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 19532, x2 + 19531, x3 + 19529, 0) |
[a__U171(x1, x2, x3)] | = | max(x1 + 46110, x2 + 46110, x3 + 46110, 0) |
[a__U182(x1, x2)] | = | max(x1 + 3, x2 + 2, 0) |
[a__U191(x1, x2)] | = | max(x1 + 49, x2 + 59, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2, x3)] | = | max(x2 + 69023, x3 + 1, 0) |
[a__U132(x1)] | = | x1 + 46114 |
[a__head#(x1)] | = | x1 + 69022 |
[a__natsFrom#(x1)] | = | x1 + 42491 |
[U142(x1)] | = | x1 + 4 |
[a__U142#(x1)] | = | 0 |
[a__U191#(x1, x2)] | = | max(x1 + 42482, x2 + 42490, 0) |
[isPLNat(x1)] | = | x1 + 0 |
[a__snd#(x1)] | = | x1 + 42473 |
[a__afterNth(x1, x2)] | = | max(x1 + 19547, x2 + 19545, 0) |
[U42(x1)] | = | x1 + 19545 |
[U91(x1)] | = | x1 + 28593 |
[U221(x1, x2, x3)] | = | max(x1 + 75, x2 + 76, x3 + 75, 0) |
[a__U182#(x1, x2)] | = | max(x1 + 2, x2 + 42490, 0) |
[a__U152#(x1)] | = | 0 |
[take(x1, x2)] | = | max(x1 + 90, x2 + 88, 0) |
[U71(x1)] | = | x1 + 7 |
[U131(x1, x2)] | = | max(x1 + 46125, x2 + 46124, 0) |
[a__U221(x1, x2, x3)] | = | max(x1 + 75, x2 + 76, x3 + 75, 0) |
[U101(x1, x2)] | = | max(x1 + 86, x2 + 87, 0) |
[pair(x1, x2)] | = | max(x1 + 25, x2 + 23, 0) |
[fst(x1)] | = | x1 + 14 |
[U111(x1)] | = | x1 + 6 |
[U132(x1)] | = | x1 + 46114 |
[a__U121(x1)] | = | x1 + 0 |
[U152(x1)] | = | x1 + 3 |
[a__U204#(x1, x2)] | = | max(x1 + 42467, x2 + 42529, 0) |
[a__U111(x1)] | = | x1 + 6 |
[natsFrom(x1)] | = | x1 + 22 |
[a__snd(x1)] | = | x1 + 19454 |
[a__U181#(x1, x2)] | = | max(x2 + 42495, 0) |
[a__U51#(x1, x2)] | = | max(0) |
[a__U172(x1, x2, x3)] | = | max(x1 + 46099, x2 + 46095, x3 + 46097, 0) |
[a__U22(x1, x2)] | = | max(x1 + 7, x2 + 6, 0) |
[U172(x1, x2, x3)] | = | max(x1 + 46099, x2 + 46095, x3 + 46097, 0) |
[splitAt(x1, x2)] | = | max(x1 + 61, x2 + 59, 0) |
[a__U222(x1, x2, x3)] | = | max(x1 + 64, x2 + 75, x3 + 75, 0) |
[a__U11#(x1, x2, x3)] | = | max(x1 + 62006, x2 + 62019, x3 + 62017, 0) |
[a__U31(x1, x2, x3)] | = | max(x1 + 26535, x2 + 26544, x3 + 26545, 0) |
[a__U51(x1, x2)] | = | max(x1 + 1, x2 + 10, 0) |
[a__U81(x1)] | = | x1 + 4730 |
[a__take#(x1, x2)] | = | max(x1 + 42578, x2 + 42565, 0) |
[a__U172#(x1, x2, x3)] | = | max(x1 + 88587, x2 + 88583, x3 + 88585, 0) |
[U12(x1, x2, x3)] | = | max(x1 + 19518, x2 + 19515, x3 + 19516, 0) |
[isNatural(x1)] | = | x1 + 13 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | max(x1 + 19544, x2 + 19555, 0) |
[U222(x1, x2, x3)] | = | max(x1 + 64, x2 + 75, x3 + 75, 0) |
[a__U12#(x1, x2, x3)] | = | max(x1 + 62006, x2 + 42550, x3 + 42548, 0) |
[U201(x1,...,x4)] | = | max(x1 + 39, x2 + 61, x3 + 58, x4 + 59, 0) |
[a__U21#(x1, x2, x3)] | = | max(x2 + 42514, x3 + 42512, 0) |
[a__U81#(x1)] | = | 0 |
[a__U161(x1, x2)] | = | max(x1 + 9, x2 + 22, 0) |
[a__U61#(x1)] | = | 0 |
[U141(x1, x2)] | = | max(x1 + 14, x2 + 14, 0) |
[a__fst(x1)] | = | x1 + 14 |
[tail(x1)] | = | x1 + 28593 |
[a__natsFrom(x1)] | = | x1 + 22 |
[mark#(x1)] | = | x1 + 42489 |
[a__U204(x1, x2)] | = | max(x1 + 0, x2 + 42, 0) |
[0] | = | 44495 |
[a__U211#(x1, x2)] | = | max(x2 + 42491, 0) |
[a__isLNat(x1)] | = | x1 + 10 |
[U191(x1, x2)] | = | max(x1 + 49, x2 + 59, 0) |
[a__U21(x1, x2, x3)] | = | max(x1 + 26, x2 + 26, x3 + 24, 0) |
[U171(x1, x2, x3)] | = | max(x1 + 46110, x2 + 46110, x3 + 46110, 0) |
[a__U32(x1, x2)] | = | max(x1 + 26535, x2 + 26544, 0) |
[a__U91(x1)] | = | x1 + 28593 |
[sel(x1, x2)] | = | max(x1 + 46125, x2 + 46123, 0) |
[U202(x1,...,x4)] | = | max(x1 + 45, x2 + 61, x3 + 42, x4 + 59, 0) |
[afterNth(x1, x2)] | = | max(x1 + 19547, x2 + 19545, 0) |
[a__U151#(x1, x2)] | = | max(0) |
[a__U111#(x1)] | = | 0 |
[a__U161#(x1, x2)] | = | max(x2 + 42490, 0) |
[a__U141#(x1, x2)] | = | max(0) |
[nil] | = | 1 |
[a__splitAt(x1, x2)] | = | max(x1 + 61, x2 + 59, 0) |
[isLNat(x1)] | = | x1 + 10 |
[a__U142(x1)] | = | x1 + 4 |
[a__U52#(x1)] | = | 0 |
[a__U211(x1, x2)] | = | max(x1 + 28580, x2 + 28579, 0) |
[a__U102#(x1)] | = | 0 |
[a__sel#(x1, x2)] | = | max(x1 + 88613, x2 + 88599, 0) |
[mark(x1)] | = | x1 + 0 |
[U151(x1, x2)] | = | max(x1 + 4, x2 + 13, 0) |
[a__isLNat#(x1)] | = | 0 |
[a__U101#(x1, x2)] | = | max(0) |
[a__U11(x1, x2, x3)] | = | max(x1 + 19532, x2 + 19531, x3 + 19529, 0) |
[a__U222#(x1, x2, x3)] | = | max(x2 + 42552, x3 + 42550, 0) |
[U32(x1, x2)] | = | max(x1 + 26535, x2 + 26544, 0) |
[a__U141(x1, x2)] | = | max(x1 + 14, x2 + 14, 0) |
[a__sel(x1, x2)] | = | max(x1 + 46125, x2 + 46123, 0) |
[a__U42(x1)] | = | x1 + 19545 |
[a__U52(x1)] | = | x1 + 0 |
[a__U181(x1, x2)] | = | max(x1 + 5, x2 + 13, 0) |
[U211(x1, x2)] | = | max(x1 + 28580, x2 + 28579, 0) |
[U203(x1,...,x4)] | = | max(x1 + 43, x2 + 61, x3 + 42, x4 + 59, 0) |
[a__U202#(x1,...,x4)] | = | max(x1 + 42532, x2 + 42549, x3 + 42530, x4 + 42529, 0) |
[a__U12(x1, x2, x3)] | = | max(x1 + 19518, x2 + 19515, x3 + 19516, 0) |
[a__U201#(x1,...,x4)] | = | max(x2 + 42549, x3 + 42546, x4 + 42529, 0) |
[a__isPLNat(x1)] | = | x1 + 0 |
[a__U121#(x1)] | = | 0 |
[U52(x1)] | = | x1 + 0 |
[U61(x1)] | = | x1 + 24 |
[a__U22#(x1, x2)] | = | max(x2 + 42494, 0) |
[U31(x1, x2, x3)] | = | max(x1 + 26535, x2 + 26544, x3 + 26545, 0) |
[a__U171#(x1, x2, x3)] | = | max(x1 + 88588, x2 + 88584, x3 + 88598, 0) |
[a__U71(x1)] | = | x1 + 7 |
[a__U203#(x1,...,x4)] | = | max(x2 + 42549, x3 + 42530, x4 + 42529, 0) |
[a__isPLNat#(x1)] | = | 0 |
[head(x1)] | = | x1 + 26548 |
[a__afterNth#(x1, x2)] | = | max(x1 + 62035, x2 + 62020, 0) |
[a__splitAt#(x1, x2)] | = | max(x1 + 42549, x2 + 42529, 0) |
[cons(x1, x2)] | = | max(x1 + 17, x2 + 0, 0) |
[a__U61(x1)] | = | x1 + 24 |
[U102(x1)] | = | x1 + 4 |
[snd(x1)] | = | x1 + 19454 |
[a__take(x1, x2)] | = | max(x1 + 90, x2 + 88, 0) |
[U81(x1)] | = | x1 + 4730 |
[a__U41#(x1, x2)] | = | max(0) |
[tt] | = | 8 |
[a__isNatural(x1)] | = | x1 + 13 |
[a__U131(x1, x2)] | = | max(x1 + 46125, x2 + 46124, 0) |
[a__isNatural#(x1)] | = | 0 |
[a__fst#(x1)] | = | x1 + 42490 |
[a__U212#(x1, x2)] | = | max(x2 + 42490, 0) |
[a__U201(x1,...,x4)] | = | max(x1 + 39, x2 + 61, x3 + 58, x4 + 59, 0) |
[a__U202(x1,...,x4)] | = | max(x1 + 45, x2 + 61, x3 + 42, x4 + 59, 0) |
[U22(x1, x2)] | = | max(x1 + 7, x2 + 6, 0) |
[U51(x1, x2)] | = | max(x1 + 1, x2 + 10, 0) |
[a__U132#(x1)] | = | 0 |
[a__tail(x1)] | = | x1 + 28593 |
[U212(x1, x2)] | = | max(x1 + 28569, x2 + 2090, 0) |
[U41(x1, x2)] | = | max(x1 + 19544, x2 + 19555, 0) |
[a__tail#(x1)] | = | x1 + 42492 |
[a__U203(x1,...,x4)] | = | max(x1 + 43, x2 + 61, x3 + 42, x4 + 59, 0) |
[a__U32#(x1, x2)] | = | max(x2 + 69022, 0) |
[a__U221#(x1, x2, x3)] | = | max(x2 + 42564, x3 + 42552, 0) |
[a__U101(x1, x2)] | = | max(x1 + 86, x2 + 87, 0) |
[a__U91#(x1)] | = | 0 |
[U121(x1)] | = | x1 + 0 |
[a__head(x1)] | = | x1 + 26548 |
[U181(x1, x2)] | = | max(x1 + 5, x2 + 13, 0) |
[a__U212(x1, x2)] | = | max(x1 + 28569, x2 + 2090, 0) |
There are 168 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsThere are 119 ruless (increase limit for explicit display).
could be deleted.The dependency pairs are split into 2 components.
a__U203#(tt,N,X,XS) | → | a__splitAt#(mark(N),mark(XS)) | (201) |
a__U201#(tt,N,X,XS) | → | a__U202#(a__isNatural(X),N,X,XS) | (258) |
a__splitAt#(s(N),cons(X,XS)) | → | a__U201#(a__isNatural(N),N,X,XS) | (317) |
a__U202#(tt,N,X,XS) | → | a__U203#(a__isLNat(XS),N,X,XS) | (350) |
π(a__snd#) | = | 1 |
π(U42) | = | 1 |
π(U91) | = | 1 |
π(a__U11#) | = | 1 |
π(a__U61#) | = | 1 |
π(a__U211#) | = | 1 |
π(a__U91) | = | 1 |
π(a__U161#) | = | 1 |
π(a__U102#) | = | 1 |
π(mark) | = | 1 |
π(a__isLNat#) | = | 1 |
π(a__U222#) | = | 1 |
π(a__U42) | = | 1 |
π(a__U202#) | = | 2 |
π(a__U201#) | = | 2 |
π(a__U203#) | = | 2 |
π(a__splitAt#) | = | 1 |
π(a__fst#) | = | 1 |
π(a__U212#) | = | 2 |
prec(U204) | = | 3 | status(U204) | = | [] | list-extension(U204) | = | Lex | ||
prec(a__U151) | = | 11 | status(a__U151) | = | [] | list-extension(a__U151) | = | Lex | ||
prec(a__U131#) | = | 0 | status(a__U131#) | = | [2, 1] | list-extension(a__U131#) | = | Lex | ||
prec(U21) | = | 14 | status(U21) | = | [2] | list-extension(U21) | = | Lex | ||
prec(a__U102) | = | 18 | status(a__U102) | = | [] | list-extension(a__U102) | = | Lex | ||
prec(a__U152) | = | 11 | status(a__U152) | = | [] | list-extension(a__U152) | = | Lex | ||
prec(U161) | = | 2 | status(U161) | = | [2] | list-extension(U161) | = | Lex | ||
prec(a__U71#) | = | 0 | status(a__U71#) | = | [] | list-extension(a__U71#) | = | Lex | ||
prec(U182) | = | 0 | status(U182) | = | [] | list-extension(U182) | = | Lex | ||
prec(U11) | = | 0 | status(U11) | = | [] | list-extension(U11) | = | Lex | ||
prec(a__U171) | = | 0 | status(a__U171) | = | [2, 1, 3] | list-extension(a__U171) | = | Lex | ||
prec(a__U182) | = | 0 | status(a__U182) | = | [] | list-extension(a__U182) | = | Lex | ||
prec(a__U191) | = | 1 | status(a__U191) | = | [] | list-extension(a__U191) | = | Lex | ||
prec(s) | = | 6 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(a__U31#) | = | 0 | status(a__U31#) | = | [1, 2, 3] | list-extension(a__U31#) | = | Lex | ||
prec(a__U132) | = | 11 | status(a__U132) | = | [] | list-extension(a__U132) | = | Lex | ||
prec(a__head#) | = | 0 | status(a__head#) | = | [] | list-extension(a__head#) | = | Lex | ||
prec(a__natsFrom#) | = | 0 | status(a__natsFrom#) | = | [] | list-extension(a__natsFrom#) | = | Lex | ||
prec(U142) | = | 14 | status(U142) | = | [] | list-extension(U142) | = | Lex | ||
prec(a__U142#) | = | 0 | status(a__U142#) | = | [] | list-extension(a__U142#) | = | Lex | ||
prec(a__U191#) | = | 0 | status(a__U191#) | = | [2, 1] | list-extension(a__U191#) | = | Lex | ||
prec(isPLNat) | = | 16 | status(isPLNat) | = | [] | list-extension(isPLNat) | = | Lex | ||
prec(a__afterNth) | = | 14 | status(a__afterNth) | = | [2] | list-extension(a__afterNth) | = | Lex | ||
prec(U221) | = | 17 | status(U221) | = | [] | list-extension(U221) | = | Lex | ||
prec(a__U182#) | = | 0 | status(a__U182#) | = | [2, 1] | list-extension(a__U182#) | = | Lex | ||
prec(a__U152#) | = | 0 | status(a__U152#) | = | [] | list-extension(a__U152#) | = | Lex | ||
prec(take) | = | 17 | status(take) | = | [1] | list-extension(take) | = | Lex | ||
prec(U71) | = | 8 | status(U71) | = | [] | list-extension(U71) | = | Lex | ||
prec(U131) | = | 11 | status(U131) | = | [] | list-extension(U131) | = | Lex | ||
prec(a__U221) | = | 17 | status(a__U221) | = | [] | list-extension(a__U221) | = | Lex | ||
prec(U101) | = | 18 | status(U101) | = | [1] | list-extension(U101) | = | Lex | ||
prec(pair) | = | 1 | status(pair) | = | [1] | list-extension(pair) | = | Lex | ||
prec(fst) | = | 15 | status(fst) | = | [1] | list-extension(fst) | = | Lex | ||
prec(U111) | = | 6 | status(U111) | = | [] | list-extension(U111) | = | Lex | ||
prec(U132) | = | 11 | status(U132) | = | [] | list-extension(U132) | = | Lex | ||
prec(a__U121) | = | 6 | status(a__U121) | = | [] | list-extension(a__U121) | = | Lex | ||
prec(U152) | = | 11 | status(U152) | = | [] | list-extension(U152) | = | Lex | ||
prec(a__U204#) | = | 0 | status(a__U204#) | = | [2, 1] | list-extension(a__U204#) | = | Lex | ||
prec(a__U111) | = | 6 | status(a__U111) | = | [] | list-extension(a__U111) | = | Lex | ||
prec(natsFrom) | = | 13 | status(natsFrom) | = | [] | list-extension(natsFrom) | = | Lex | ||
prec(a__snd) | = | 14 | status(a__snd) | = | [] | list-extension(a__snd) | = | Lex | ||
prec(a__U181#) | = | 0 | status(a__U181#) | = | [1, 2] | list-extension(a__U181#) | = | Lex | ||
prec(a__U51#) | = | 0 | status(a__U51#) | = | [] | list-extension(a__U51#) | = | Lex | ||
prec(a__U172) | = | 15 | status(a__U172) | = | [] | list-extension(a__U172) | = | Lex | ||
prec(a__U22) | = | 14 | status(a__U22) | = | [2] | list-extension(a__U22) | = | Lex | ||
prec(U172) | = | 15 | status(U172) | = | [] | list-extension(U172) | = | Lex | ||
prec(splitAt) | = | 6 | status(splitAt) | = | [] | list-extension(splitAt) | = | Lex | ||
prec(a__U222) | = | 16 | status(a__U222) | = | [2] | list-extension(a__U222) | = | Lex | ||
prec(a__U31) | = | 15 | status(a__U31) | = | [] | list-extension(a__U31) | = | Lex | ||
prec(a__U51) | = | 9 | status(a__U51) | = | [] | list-extension(a__U51) | = | Lex | ||
prec(a__U81) | = | 8 | status(a__U81) | = | [] | list-extension(a__U81) | = | Lex | ||
prec(a__take#) | = | 0 | status(a__take#) | = | [2] | list-extension(a__take#) | = | Lex | ||
prec(a__U172#) | = | 0 | status(a__U172#) | = | [3, 1] | list-extension(a__U172#) | = | Lex | ||
prec(U12) | = | 14 | status(U12) | = | [] | list-extension(U12) | = | Lex | ||
prec(isNatural) | = | 6 | status(isNatural) | = | [] | list-extension(isNatural) | = | Lex | ||
prec(a__U42#) | = | 0 | status(a__U42#) | = | [] | list-extension(a__U42#) | = | Lex | ||
prec(a__U41) | = | 8 | status(a__U41) | = | [] | list-extension(a__U41) | = | Lex | ||
prec(U222) | = | 16 | status(U222) | = | [2] | list-extension(U222) | = | Lex | ||
prec(a__U12#) | = | 0 | status(a__U12#) | = | [3, 1, 2] | list-extension(a__U12#) | = | Lex | ||
prec(U201) | = | 6 | status(U201) | = | [] | list-extension(U201) | = | Lex | ||
prec(a__U21#) | = | 0 | status(a__U21#) | = | [2, 3, 1] | list-extension(a__U21#) | = | Lex | ||
prec(a__U81#) | = | 0 | status(a__U81#) | = | [] | list-extension(a__U81#) | = | Lex | ||
prec(a__U161) | = | 2 | status(a__U161) | = | [2] | list-extension(a__U161) | = | Lex | ||
prec(U141) | = | 15 | status(U141) | = | [] | list-extension(U141) | = | Lex | ||
prec(a__fst) | = | 15 | status(a__fst) | = | [1] | list-extension(a__fst) | = | Lex | ||
prec(tail) | = | 1 | status(tail) | = | [] | list-extension(tail) | = | Lex | ||
prec(a__natsFrom) | = | 13 | status(a__natsFrom) | = | [] | list-extension(a__natsFrom) | = | Lex | ||
prec(mark#) | = | 0 | status(mark#) | = | [] | list-extension(mark#) | = | Lex | ||
prec(a__U204) | = | 3 | status(a__U204) | = | [] | list-extension(a__U204) | = | Lex | ||
prec(0) | = | 14 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(a__isLNat) | = | 9 | status(a__isLNat) | = | [] | list-extension(a__isLNat) | = | Lex | ||
prec(U191) | = | 1 | status(U191) | = | [] | list-extension(U191) | = | Lex | ||
prec(a__U21) | = | 14 | status(a__U21) | = | [2] | list-extension(a__U21) | = | Lex | ||
prec(U171) | = | 0 | status(U171) | = | [2, 1, 3] | list-extension(U171) | = | Lex | ||
prec(a__U32) | = | 12 | status(a__U32) | = | [] | list-extension(a__U32) | = | Lex | ||
prec(sel) | = | 5 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(U202) | = | 5 | status(U202) | = | [4] | list-extension(U202) | = | Lex | ||
prec(afterNth) | = | 14 | status(afterNth) | = | [2] | list-extension(afterNth) | = | Lex | ||
prec(a__U151#) | = | 0 | status(a__U151#) | = | [1] | list-extension(a__U151#) | = | Lex | ||
prec(a__U111#) | = | 0 | status(a__U111#) | = | [] | list-extension(a__U111#) | = | Lex | ||
prec(a__U141#) | = | 0 | status(a__U141#) | = | [2] | list-extension(a__U141#) | = | Lex | ||
prec(nil) | = | 0 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(a__splitAt) | = | 6 | status(a__splitAt) | = | [] | list-extension(a__splitAt) | = | Lex | ||
prec(isLNat) | = | 9 | status(isLNat) | = | [] | list-extension(isLNat) | = | Lex | ||
prec(a__U142) | = | 14 | status(a__U142) | = | [] | list-extension(a__U142) | = | Lex | ||
prec(a__U52#) | = | 0 | status(a__U52#) | = | [] | list-extension(a__U52#) | = | Lex | ||
prec(a__U211) | = | 1 | status(a__U211) | = | [1] | list-extension(a__U211) | = | Lex | ||
prec(a__sel#) | = | 0 | status(a__sel#) | = | [] | list-extension(a__sel#) | = | Lex | ||
prec(U151) | = | 11 | status(U151) | = | [] | list-extension(U151) | = | Lex | ||
prec(a__U101#) | = | 0 | status(a__U101#) | = | [1, 2] | list-extension(a__U101#) | = | Lex | ||
prec(a__U11) | = | 0 | status(a__U11) | = | [] | list-extension(a__U11) | = | Lex | ||
prec(U32) | = | 12 | status(U32) | = | [] | list-extension(U32) | = | Lex | ||
prec(a__U141) | = | 15 | status(a__U141) | = | [] | list-extension(a__U141) | = | Lex | ||
prec(a__sel) | = | 5 | status(a__sel) | = | [] | list-extension(a__sel) | = | Lex | ||
prec(a__U52) | = | 10 | status(a__U52) | = | [] | list-extension(a__U52) | = | Lex | ||
prec(a__U181) | = | 14 | status(a__U181) | = | [] | list-extension(a__U181) | = | Lex | ||
prec(U211) | = | 1 | status(U211) | = | [1] | list-extension(U211) | = | Lex | ||
prec(U203) | = | 4 | status(U203) | = | [4] | list-extension(U203) | = | Lex | ||
prec(a__U12) | = | 14 | status(a__U12) | = | [] | list-extension(a__U12) | = | Lex | ||
prec(a__isPLNat) | = | 16 | status(a__isPLNat) | = | [] | list-extension(a__isPLNat) | = | Lex | ||
prec(a__U121#) | = | 0 | status(a__U121#) | = | [] | list-extension(a__U121#) | = | Lex | ||
prec(U52) | = | 10 | status(U52) | = | [] | list-extension(U52) | = | Lex | ||
prec(U61) | = | 9 | status(U61) | = | [] | list-extension(U61) | = | Lex | ||
prec(a__U22#) | = | 0 | status(a__U22#) | = | [1, 2] | list-extension(a__U22#) | = | Lex | ||
prec(U31) | = | 15 | status(U31) | = | [] | list-extension(U31) | = | Lex | ||
prec(a__U171#) | = | 0 | status(a__U171#) | = | [3, 2] | list-extension(a__U171#) | = | Lex | ||
prec(a__U71) | = | 8 | status(a__U71) | = | [] | list-extension(a__U71) | = | Lex | ||
prec(a__isPLNat#) | = | 0 | status(a__isPLNat#) | = | [] | list-extension(a__isPLNat#) | = | Lex | ||
prec(head) | = | 15 | status(head) | = | [] | list-extension(head) | = | Lex | ||
prec(a__afterNth#) | = | 0 | status(a__afterNth#) | = | [2, 1] | list-extension(a__afterNth#) | = | Lex | ||
prec(cons) | = | 2 | status(cons) | = | [] | list-extension(cons) | = | Lex | ||
prec(a__U61) | = | 9 | status(a__U61) | = | [] | list-extension(a__U61) | = | Lex | ||
prec(U102) | = | 18 | status(U102) | = | [] | list-extension(U102) | = | Lex | ||
prec(snd) | = | 14 | status(snd) | = | [] | list-extension(snd) | = | Lex | ||
prec(a__take) | = | 17 | status(a__take) | = | [1] | list-extension(a__take) | = | Lex | ||
prec(U81) | = | 8 | status(U81) | = | [] | list-extension(U81) | = | Lex | ||
prec(a__U41#) | = | 0 | status(a__U41#) | = | [1, 2] | list-extension(a__U41#) | = | Lex | ||
prec(tt) | = | 11 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(a__isNatural) | = | 6 | status(a__isNatural) | = | [] | list-extension(a__isNatural) | = | Lex | ||
prec(a__U131) | = | 11 | status(a__U131) | = | [] | list-extension(a__U131) | = | Lex | ||
prec(a__isNatural#) | = | 0 | status(a__isNatural#) | = | [] | list-extension(a__isNatural#) | = | Lex | ||
prec(a__U201) | = | 6 | status(a__U201) | = | [] | list-extension(a__U201) | = | Lex | ||
prec(a__U202) | = | 5 | status(a__U202) | = | [4] | list-extension(a__U202) | = | Lex | ||
prec(U22) | = | 14 | status(U22) | = | [2] | list-extension(U22) | = | Lex | ||
prec(U51) | = | 9 | status(U51) | = | [] | list-extension(U51) | = | Lex | ||
prec(a__U132#) | = | 0 | status(a__U132#) | = | [] | list-extension(a__U132#) | = | Lex | ||
prec(a__tail) | = | 1 | status(a__tail) | = | [] | list-extension(a__tail) | = | Lex | ||
prec(U212) | = | 14 | status(U212) | = | [2] | list-extension(U212) | = | Lex | ||
prec(U41) | = | 8 | status(U41) | = | [] | list-extension(U41) | = | Lex | ||
prec(a__tail#) | = | 0 | status(a__tail#) | = | [] | list-extension(a__tail#) | = | Lex | ||
prec(a__U203) | = | 4 | status(a__U203) | = | [4] | list-extension(a__U203) | = | Lex | ||
prec(a__U32#) | = | 0 | status(a__U32#) | = | [] | list-extension(a__U32#) | = | Lex | ||
prec(a__U221#) | = | 0 | status(a__U221#) | = | [] | list-extension(a__U221#) | = | Lex | ||
prec(a__U101) | = | 18 | status(a__U101) | = | [1] | list-extension(a__U101) | = | Lex | ||
prec(a__U91#) | = | 0 | status(a__U91#) | = | [] | list-extension(a__U91#) | = | Lex | ||
prec(U121) | = | 6 | status(U121) | = | [] | list-extension(U121) | = | Lex | ||
prec(a__head) | = | 15 | status(a__head) | = | [] | list-extension(a__head) | = | Lex | ||
prec(U181) | = | 14 | status(U181) | = | [] | list-extension(U181) | = | Lex | ||
prec(a__U212) | = | 14 | status(a__U212) | = | [2] | list-extension(a__U212) | = | Lex |
[U204(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U151(x1, x2)] | = | max(0) |
[a__U131#(x1, x2)] | = | x1 + x2 + 1 |
[U21(x1, x2, x3)] | = | max(x2 + 0, 0) |
[a__U102(x1)] | = | x1 + 39915 |
[a__U152(x1)] | = | 0 |
[U161(x1, x2)] | = | max(x1 + 6309, x2 + 6314, 0) |
[a__U71#(x1)] | = | 1 |
[U182(x1, x2)] | = | max(x2 + 23699, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 63607, x3 + 63611, 0) |
[a__U171(x1, x2, x3)] | = | max(x1 + 87313, x2 + 87311, x3 + 87312, 0) |
[a__U182(x1, x2)] | = | max(x2 + 23699, 0) |
[a__U191(x1, x2)] | = | max(x2 + 39911, 0) |
[s(x1)] | = | x1 + 0 |
[a__U31#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U132(x1)] | = | 0 |
[a__head#(x1)] | = | 1 |
[a__natsFrom#(x1)] | = | 1 |
[U142(x1)] | = | 0 |
[a__U142#(x1)] | = | 1 |
[a__U191#(x1, x2)] | = | x1 + x2 + 1 |
[isPLNat(x1)] | = | 0 |
[a__afterNth(x1, x2)] | = | max(x2 + 63612, 0) |
[U221(x1, x2, x3)] | = | max(x1 + 39915, x2 + 39914, x3 + 39913, 0) |
[a__U182#(x1, x2)] | = | x1 + x2 + 1 |
[a__U152#(x1)] | = | 1 |
[take(x1, x2)] | = | x1 + x2 + 39921 |
[U71(x1)] | = | 3 |
[U131(x1, x2)] | = | 4 |
[a__U221(x1, x2, x3)] | = | max(x1 + 39915, x2 + 39914, x3 + 39913, 0) |
[U101(x1, x2)] | = | x1 + x2 + 63614 |
[pair(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[fst(x1)] | = | x1 + 0 |
[U111(x1)] | = | 1 |
[U132(x1)] | = | 0 |
[a__U121(x1)] | = | 5 |
[U152(x1)] | = | 0 |
[a__U204#(x1, x2)] | = | x1 + x2 + 1 |
[a__U111(x1)] | = | 1 |
[natsFrom(x1)] | = | x1 + 6314 |
[a__snd(x1)] | = | x1 + 23699 |
[a__U181#(x1, x2)] | = | x1 + x2 + 1 |
[a__U51#(x1, x2)] | = | max(x2 + 1, 0) |
[a__U172(x1, x2, x3)] | = | max(x3 + 87310, 0) |
[a__U22(x1, x2)] | = | max(x2 + 0, 0) |
[U172(x1, x2, x3)] | = | max(x3 + 87310, 0) |
[splitAt(x1, x2)] | = | max(x2 + 39911, 0) |
[a__U222(x1, x2, x3)] | = | max(x2 + 39910, x3 + 39912, 0) |
[a__U31(x1, x2, x3)] | = | max(x1 + 23692, x2 + 23693, 0) |
[a__U51(x1, x2)] | = | max(x1 + 19805, 0) |
[a__U81(x1)] | = | 47398 |
[a__take#(x1, x2)] | = | x2 + 1 |
[a__U172#(x1, x2, x3)] | = | x1 + x3 + 1 |
[U12(x1, x2, x3)] | = | max(x3 + 63610, 0) |
[isNatural(x1)] | = | 5 |
[a__U42#(x1)] | = | 1 |
[a__U41(x1, x2)] | = | max(x2 + 63613, 0) |
[U222(x1, x2, x3)] | = | max(x2 + 39910, x3 + 39912, 0) |
[a__U12#(x1, x2, x3)] | = | x1 + x2 + x3 + 0 |
[U201(x1,...,x4)] | = | max(x1 + 16213, x3 + 39911, x4 + 39911, 0) |
[a__U21#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U81#(x1)] | = | 1 |
[a__U161(x1, x2)] | = | max(x1 + 6309, x2 + 6314, 0) |
[U141(x1, x2)] | = | max(0) |
[a__fst(x1)] | = | x1 + 0 |
[tail(x1)] | = | x1 + 74900 |
[a__natsFrom(x1)] | = | x1 + 6314 |
[mark#(x1)] | = | 1 |
[a__U204(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[0] | = | 23700 |
[a__isLNat(x1)] | = | x1 + 23699 |
[U191(x1, x2)] | = | max(x2 + 39911, 0) |
[a__U21(x1, x2, x3)] | = | max(x2 + 0, 0) |
[U171(x1, x2, x3)] | = | max(x1 + 87313, x2 + 87311, x3 + 87312, 0) |
[a__U32(x1, x2)] | = | max(x2 + 1, 0) |
[sel(x1, x2)] | = | x1 + x2 + 87319 |
[U202(x1,...,x4)] | = | max(x1 + 16208, x3 + 39910, x4 + 39911, 0) |
[afterNth(x1, x2)] | = | max(x2 + 63612, 0) |
[a__U151#(x1, x2)] | = | max(x1 + 1, 0) |
[a__U111#(x1)] | = | 1 |
[a__U141#(x1, x2)] | = | max(x2 + 1, 0) |
[nil] | = | 4900 |
[a__splitAt(x1, x2)] | = | max(x2 + 39911, 0) |
[isLNat(x1)] | = | x1 + 23699 |
[a__U142(x1)] | = | 0 |
[a__U52#(x1)] | = | 1 |
[a__U211(x1, x2)] | = | max(x1 + 0, x2 + 74899, 0) |
[a__sel#(x1, x2)] | = | x2 + 1 |
[U151(x1, x2)] | = | max(0) |
[a__U101#(x1, x2)] | = | x1 + x2 + 1 |
[a__U11(x1, x2, x3)] | = | max(x1 + 63607, x3 + 63611, 0) |
[U32(x1, x2)] | = | max(x2 + 1, 0) |
[a__U141(x1, x2)] | = | max(0) |
[a__sel(x1, x2)] | = | x1 + x2 + 87319 |
[a__U52(x1)] | = | 19803 |
[a__U181(x1, x2)] | = | max(x2 + 23699, 0) |
[U211(x1, x2)] | = | max(x1 + 0, x2 + 74899, 0) |
[U203(x1,...,x4)] | = | max(x1 + 16210, x3 + 16209, x4 + 39911, 0) |
[a__U12(x1, x2, x3)] | = | max(x3 + 63610, 0) |
[a__isPLNat(x1)] | = | 0 |
[a__U121#(x1)] | = | 1 |
[U52(x1)] | = | 19803 |
[U61(x1)] | = | 23699 |
[a__U22#(x1, x2)] | = | x1 + x2 + 1 |
[U31(x1, x2, x3)] | = | max(x1 + 23692, x2 + 23693, 0) |
[a__U171#(x1, x2, x3)] | = | x2 + x3 + 1 |
[a__U71(x1)] | = | 3 |
[a__isPLNat#(x1)] | = | 1 |
[head(x1)] | = | x1 + 23698 |
[a__afterNth#(x1, x2)] | = | x1 + x2 + 1 |
[cons(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U61(x1)] | = | 23699 |
[U102(x1)] | = | x1 + 39915 |
[snd(x1)] | = | x1 + 23699 |
[a__take(x1, x2)] | = | x1 + x2 + 39921 |
[U81(x1)] | = | 47398 |
[a__U41#(x1, x2)] | = | max(x1 + 1, x2 + 1, 0) |
[tt] | = | 0 |
[a__isNatural(x1)] | = | 5 |
[a__U131(x1, x2)] | = | 4 |
[a__isNatural#(x1)] | = | 1 |
[a__U201(x1,...,x4)] | = | max(x1 + 16213, x3 + 39911, x4 + 39911, 0) |
[a__U202(x1,...,x4)] | = | max(x1 + 16208, x3 + 39910, x4 + 39911, 0) |
[U22(x1, x2)] | = | max(x2 + 0, 0) |
[U51(x1, x2)] | = | max(x1 + 19805, 0) |
[a__U132#(x1)] | = | 1 |
[a__tail(x1)] | = | x1 + 74900 |
[U212(x1, x2)] | = | max(x1 + 51199, x2 + 51199, 0) |
[U41(x1, x2)] | = | max(x2 + 63613, 0) |
[a__tail#(x1)] | = | 1 |
[a__U203(x1,...,x4)] | = | max(x1 + 16210, x3 + 16209, x4 + 39911, 0) |
[a__U32#(x1, x2)] | = | x2 + 1 |
[a__U221#(x1, x2, x3)] | = | x1 + 1 |
[a__U101(x1, x2)] | = | x1 + x2 + 63614 |
[a__U91#(x1)] | = | 1 |
[U121(x1)] | = | 5 |
[a__head(x1)] | = | x1 + 23698 |
[U181(x1, x2)] | = | max(x2 + 23699, 0) |
[a__U212(x1, x2)] | = | max(x1 + 51199, x2 + 51199, 0) |
There are 168 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the paira__splitAt#(s(N),cons(X,XS)) | → | a__U201#(a__isNatural(N),N,X,XS) | (317) |
The dependency pairs are split into 0 components.
mark#(U52(X)) | → | mark#(X) | (270) |
mark#(U121(X)) | → | mark#(X) | (293) |
mark#(U204(X1,X2)) | → | mark#(X1) | (273) |
mark#(s(X)) | → | mark#(X) | (265) |
[U204(x1, x2)] | = | x1 + 32036 |
[a__U151(x1, x2)] | = | 2 |
[a__U131#(x1, x2)] | = | 0 |
[U21(x1, x2, x3)] | = | x2 + 32026 |
[a__U102(x1)] | = | 6 |
[a__U152(x1)] | = | 3 |
[U161(x1, x2)] | = | 2 |
[a__U71#(x1)] | = | 0 |
[U182(x1, x2)] | = | 5 |
[U11(x1, x2, x3)] | = | 3 |
[a__U171(x1, x2, x3)] | = | 3 |
[a__U182(x1, x2)] | = | x1 + x2 + 4 |
[a__U191(x1, x2)] | = | x1 + 1 |
[s(x1)] | = | x1 + 1 |
[a__U31#(x1, x2, x3)] | = | 0 |
[a__U132(x1)] | = | 32030 |
[a__head#(x1)] | = | 0 |
[a__natsFrom#(x1)] | = | 0 |
[U142(x1)] | = | x1 + 32031 |
[a__U142#(x1)] | = | 0 |
[a__U191#(x1, x2)] | = | 0 |
[isPLNat(x1)] | = | x1 + 1 |
[a__snd#(x1)] | = | 0 |
[a__afterNth(x1, x2)] | = | x2 + 1 |
[U42(x1)] | = | x1 + 32031 |
[U91(x1)] | = | x1 + 5 |
[U221(x1, x2, x3)] | = | 2 |
[a__U182#(x1, x2)] | = | 0 |
[a__U152#(x1)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 2 |
[U71(x1)] | = | 10 |
[U131(x1, x2)] | = | 32030 |
[a__U221(x1, x2, x3)] | = | x1 + x3 + 1 |
[U101(x1, x2)] | = | x1 + 6 |
[pair(x1, x2)] | = | 32036 |
[fst(x1)] | = | 32027 |
[U111(x1)] | = | 32031 |
[U132(x1)] | = | x1 + 32031 |
[a__U121(x1)] | = | 4 |
[U152(x1)] | = | 4 |
[a__U204#(x1, x2)] | = | 0 |
[a__U111(x1)] | = | 32030 |
[natsFrom(x1)] | = | x1 + 8 |
[a__snd(x1)] | = | 4 |
[a__U181#(x1, x2)] | = | 0 |
[a__U51#(x1, x2)] | = | 0 |
[a__U172(x1, x2, x3)] | = | x2 + 4 |
[a__U22(x1, x2)] | = | x2 + 0 |
[U172(x1, x2, x3)] | = | x1 + 5 |
[splitAt(x1, x2)] | = | 3 |
[a__U222(x1, x2, x3)] | = | x2 + x3 + 32033 |
[a__U11#(x1, x2, x3)] | = | 0 |
[a__U31(x1, x2, x3)] | = | x1 + x3 + 4 |
[a__U51(x1, x2)] | = | x2 + 32027 |
[a__U81(x1)] | = | x1 + 8 |
[a__take#(x1, x2)] | = | 0 |
[a__U172#(x1, x2, x3)] | = | 0 |
[U12(x1, x2, x3)] | = | x1 + 4 |
[isNatural(x1)] | = | 3 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | 32029 |
[U222(x1, x2, x3)] | = | x1 + 32034 |
[a__U12#(x1, x2, x3)] | = | 0 |
[U201(x1,...,x4)] | = | x2 + x3 + x4 + 4 |
[a__U21#(x1, x2, x3)] | = | 0 |
[a__U81#(x1)] | = | 0 |
[a__U161(x1, x2)] | = | x1 + 1 |
[a__U61#(x1)] | = | 0 |
[U141(x1, x2)] | = | 2 |
[a__fst(x1)] | = | 32026 |
[tail(x1)] | = | 3 |
[a__natsFrom(x1)] | = | 2 |
[mark#(x1)] | = | x1 + 0 |
[a__U204(x1, x2)] | = | x2 + 32035 |
[0] | = | 2 |
[a__U211#(x1, x2)] | = | 0 |
[a__isLNat(x1)] | = | x1 + 2 |
[U191(x1, x2)] | = | 2 |
[a__U21(x1, x2, x3)] | = | x1 + x3 + 32025 |
[U171(x1, x2, x3)] | = | x1 + 4 |
[a__U32(x1, x2)] | = | x2 + 32036 |
[a__U91(x1)] | = | x1 + 4 |
[sel(x1, x2)] | = | x1 + 3 |
[U202(x1,...,x4)] | = | 5 |
[afterNth(x1, x2)] | = | x1 + 4 |
[a__U151#(x1, x2)] | = | 0 |
[a__U111#(x1)] | = | 0 |
[a__U161#(x1, x2)] | = | 0 |
[a__U141#(x1, x2)] | = | 0 |
[nil] | = | 5 |
[a__splitAt(x1, x2)] | = | 2 |
[isLNat(x1)] | = | x1 + 3 |
[a__U142(x1)] | = | 32030 |
[a__U52#(x1)] | = | 0 |
[a__U211(x1, x2)] | = | x2 + 3 |
[a__U102#(x1)] | = | 0 |
[a__sel#(x1, x2)] | = | 1 |
[mark(x1)] | = | 1 |
[U151(x1, x2)] | = | x1 + 3 |
[a__isLNat#(x1)] | = | 0 |
[a__U101#(x1, x2)] | = | 0 |
[a__U11(x1, x2, x3)] | = | x2 + x3 + 2 |
[a__U222#(x1, x2, x3)] | = | 0 |
[U32(x1, x2)] | = | 32037 |
[a__U141(x1, x2)] | = | x1 + x2 + 1 |
[a__sel(x1, x2)] | = | 2 |
[a__U42(x1)] | = | 32030 |
[a__U52(x1)] | = | 32030 |
[a__U181(x1, x2)] | = | x2 + 5 |
[U211(x1, x2)] | = | x1 + 4 |
[U203(x1,...,x4)] | = | 4 |
[a__U202#(x1,...,x4)] | = | 0 |
[a__U12(x1, x2, x3)] | = | 3 |
[a__U201#(x1,...,x4)] | = | 0 |
[a__isPLNat(x1)] | = | 0 |
[a__U121#(x1)] | = | 0 |
[U52(x1)] | = | x1 + 32031 |
[U61(x1)] | = | x1 + 32031 |
[a__U22#(x1, x2)] | = | 0 |
[U31(x1, x2, x3)] | = | x2 + 5 |
[a__U171#(x1, x2, x3)] | = | 1 |
[a__U71(x1)] | = | x1 + 9 |
[a__U203#(x1,...,x4)] | = | 0 |
[a__isPLNat#(x1)] | = | 0 |
[head(x1)] | = | x1 + 32027 |
[a__afterNth#(x1, x2)] | = | 0 |
[a__splitAt#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x2 + 32024 |
[a__U61(x1)] | = | 32030 |
[U102(x1)] | = | 7 |
[snd(x1)] | = | 5 |
[a__take(x1, x2)] | = | x1 + 1 |
[U81(x1)] | = | x1 + 9 |
[a__U41#(x1, x2)] | = | 0 |
[tt] | = | 32031 |
[a__isNatural(x1)] | = | x1 + 2 |
[a__U131(x1, x2)] | = | x2 + 32029 |
[a__isNatural#(x1)] | = | 0 |
[a__fst#(x1)] | = | 0 |
[a__U212#(x1, x2)] | = | 0 |
[a__U201(x1,...,x4)] | = | 3 |
[a__U202(x1,...,x4)] | = | x4 + 4 |
[U22(x1, x2)] | = | 1 |
[U51(x1, x2)] | = | 32028 |
[a__U132#(x1)] | = | 0 |
[a__tail(x1)] | = | 2 |
[U212(x1, x2)] | = | x1 + 1 |
[U41(x1, x2)] | = | x1 + x2 + 32030 |
[a__tail#(x1)] | = | 0 |
[a__U203(x1,...,x4)] | = | x1 + x4 + 3 |
[a__U32#(x1, x2)] | = | 0 |
[a__U221#(x1, x2, x3)] | = | 0 |
[a__U101(x1, x2)] | = | 5 |
[a__U91#(x1)] | = | 0 |
[U121(x1)] | = | x1 + 5 |
[a__head(x1)] | = | 5 |
[U181(x1, x2)] | = | 6 |
[a__U212(x1, x2)] | = | x2 + 0 |
mark#(U52(X)) | → | mark#(X) | (270) |
mark#(U121(X)) | → | mark#(X) | (293) |
mark#(U204(X1,X2)) | → | mark#(X1) | (273) |
mark#(s(X)) | → | mark#(X) | (265) |
The dependency pairs are split into 0 components.
a__U131#(tt,V2) | → | a__isLNat#(V2) | (277) |
a__U101#(tt,V2) | → | a__isLNat#(V2) | (366) |
a__isLNat#(afterNth(V1,V2)) | → | a__isNatural#(V1) | (365) |
a__isNatural#(sel(V1,V2)) | → | a__U131#(a__isNatural(V1),V2) | (269) |
a__isPLNat#(pair(V1,V2)) | → | a__U141#(a__isLNat(V1),V2) | (363) |
a__isNatural#(sel(V1,V2)) | → | a__isNatural#(V1) | (257) |
a__U151#(tt,V2) | → | a__isLNat#(V2) | (254) |
a__isPLNat#(splitAt(V1,V2)) | → | a__isNatural#(V1) | (351) |
a__isNatural#(s(V1)) | → | a__isNatural#(V1) | (248) |
a__isLNat#(afterNth(V1,V2)) | → | a__U41#(a__isNatural(V1),V2) | (345) |
a__isPLNat#(pair(V1,V2)) | → | a__isLNat#(V1) | (239) |
a__isLNat#(natsFrom(V1)) | → | a__isNatural#(V1) | (229) |
a__isLNat#(cons(V1,V2)) | → | a__U51#(a__isNatural(V1),V2) | (226) |
a__U141#(tt,V2) | → | a__isLNat#(V2) | (223) |
a__isLNat#(cons(V1,V2)) | → | a__isNatural#(V1) | (196) |
a__U51#(tt,V2) | → | a__isLNat#(V2) | (197) |
a__isPLNat#(splitAt(V1,V2)) | → | a__U151#(a__isNatural(V1),V2) | (193) |
a__isLNat#(fst(V1)) | → | a__isPLNat#(V1) | (189) |
a__isLNat#(take(V1,V2)) | → | a__isNatural#(V1) | (297) |
a__U41#(tt,V2) | → | a__isLNat#(V2) | (186) |
a__isNatural#(head(V1)) | → | a__isLNat#(V1) | (292) |
a__isLNat#(take(V1,V2)) | → | a__U101#(a__isNatural(V1),V2) | (290) |
a__isLNat#(tail(V1)) | → | a__isLNat#(V1) | (173) |
a__isLNat#(snd(V1)) | → | a__isPLNat#(V1) | (172) |
[U204(x1, x2)] | = | x1 + 15 |
[a__U151(x1, x2)] | = | 2 |
[a__U131#(x1, x2)] | = | x2 + 1 |
[U21(x1, x2, x3)] | = | x2 + 64047 |
[a__U102(x1)] | = | 6 |
[a__U152(x1)] | = | 3 |
[U161(x1, x2)] | = | 2 |
[a__U71#(x1)] | = | 0 |
[U182(x1, x2)] | = | 5 |
[U11(x1, x2, x3)] | = | 3 |
[a__U171(x1, x2, x3)] | = | 3 |
[a__U182(x1, x2)] | = | x1 + x2 + 4 |
[a__U191(x1, x2)] | = | x1 + 1 |
[s(x1)] | = | x1 + 1 |
[a__U31#(x1, x2, x3)] | = | 0 |
[a__U132(x1)] | = | 7 |
[a__head#(x1)] | = | 0 |
[a__natsFrom#(x1)] | = | 0 |
[U142(x1)] | = | x1 + 10 |
[a__U142#(x1)] | = | 0 |
[a__U191#(x1, x2)] | = | 0 |
[isPLNat(x1)] | = | x1 + 1 |
[a__snd#(x1)] | = | 0 |
[a__afterNth(x1, x2)] | = | x2 + 1 |
[U42(x1)] | = | x1 + 7 |
[U91(x1)] | = | x1 + 5 |
[U221(x1, x2, x3)] | = | 2 |
[a__U182#(x1, x2)] | = | 0 |
[a__U152#(x1)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 2 |
[U71(x1)] | = | 12 |
[U131(x1, x2)] | = | 7 |
[a__U221(x1, x2, x3)] | = | x1 + x3 + 1 |
[U101(x1, x2)] | = | x1 + 6 |
[pair(x1, x2)] | = | x1 + x2 + 8 |
[fst(x1)] | = | x1 + 5 |
[U111(x1)] | = | 10 |
[U132(x1)] | = | x1 + 8 |
[a__U121(x1)] | = | 4 |
[U152(x1)] | = | 4 |
[a__U204#(x1, x2)] | = | 0 |
[a__U111(x1)] | = | 9 |
[natsFrom(x1)] | = | x1 + 8 |
[a__snd(x1)] | = | 4 |
[a__U181#(x1, x2)] | = | 0 |
[a__U51#(x1, x2)] | = | x2 + 1 |
[a__U172(x1, x2, x3)] | = | x2 + 4 |
[a__U22(x1, x2)] | = | x2 + 0 |
[U172(x1, x2, x3)] | = | x1 + 5 |
[splitAt(x1, x2)] | = | x1 + x2 + 3 |
[a__U222(x1, x2, x3)] | = | x2 + x3 + 12 |
[a__U11#(x1, x2, x3)] | = | 0 |
[a__U31(x1, x2, x3)] | = | x1 + x3 + 4 |
[a__U51(x1, x2)] | = | x2 + 8 |
[a__U81(x1)] | = | x1 + 8 |
[a__take#(x1, x2)] | = | 0 |
[a__U172#(x1, x2, x3)] | = | 0 |
[U12(x1, x2, x3)] | = | x1 + 4 |
[isNatural(x1)] | = | 3 |
[a__U42#(x1)] | = | 0 |
[a__U41(x1, x2)] | = | 5 |
[U222(x1, x2, x3)] | = | x1 + 13 |
[a__U12#(x1, x2, x3)] | = | 0 |
[U201(x1,...,x4)] | = | x2 + x3 + x4 + 4 |
[a__U21#(x1, x2, x3)] | = | 0 |
[a__U81#(x1)] | = | 0 |
[a__U161(x1, x2)] | = | x1 + 1 |
[a__U61#(x1)] | = | 0 |
[U141(x1, x2)] | = | 2 |
[a__fst(x1)] | = | 2 |
[tail(x1)] | = | x1 + 3 |
[a__natsFrom(x1)] | = | 2 |
[mark#(x1)] | = | 0 |
[a__U204(x1, x2)] | = | x2 + 14 |
[0] | = | 2 |
[a__U211#(x1, x2)] | = | 0 |
[a__isLNat(x1)] | = | x1 + 2 |
[U191(x1, x2)] | = | 2 |
[a__U21(x1, x2, x3)] | = | x1 + x3 + 64046 |
[U171(x1, x2, x3)] | = | x1 + 4 |
[a__U32(x1, x2)] | = | x2 + 15 |
[a__U91(x1)] | = | x1 + 4 |
[sel(x1, x2)] | = | x1 + x2 + 3 |
[U202(x1,...,x4)] | = | 5 |
[afterNth(x1, x2)] | = | x1 + x2 + 2 |
[a__U151#(x1, x2)] | = | x2 + 1 |
[a__U111#(x1)] | = | 0 |
[a__U161#(x1, x2)] | = | 0 |
[a__U141#(x1, x2)] | = | x2 + 1 |
[nil] | = | 7 |
[a__splitAt(x1, x2)] | = | 2 |
[isLNat(x1)] | = | x1 + 3 |
[a__U142(x1)] | = | 9 |
[a__U52#(x1)] | = | 0 |
[a__U211(x1, x2)] | = | x2 + 3 |
[a__U102#(x1)] | = | 0 |
[a__sel#(x1, x2)] | = | 1 |
[mark(x1)] | = | 1 |
[U151(x1, x2)] | = | x1 + 3 |
[a__isLNat#(x1)] | = | x1 + 0 |
[a__U101#(x1, x2)] | = | x2 + 1 |
[a__U11(x1, x2, x3)] | = | x2 + x3 + 2 |
[a__U222#(x1, x2, x3)] | = | 0 |
[U32(x1, x2)] | = | 16 |
[a__U141(x1, x2)] | = | x1 + x2 + 1 |
[a__sel(x1, x2)] | = | 2 |
[a__U42(x1)] | = | 6 |
[a__U52(x1)] | = | 9 |
[a__U181(x1, x2)] | = | x2 + 5 |
[U211(x1, x2)] | = | x1 + 4 |
[U203(x1,...,x4)] | = | 4 |
[a__U202#(x1,...,x4)] | = | 0 |
[a__U12(x1, x2, x3)] | = | 3 |
[a__U201#(x1,...,x4)] | = | 0 |
[a__isPLNat(x1)] | = | 0 |
[a__U121#(x1)] | = | 0 |
[U52(x1)] | = | x1 + 10 |
[U61(x1)] | = | x1 + 9 |
[a__U22#(x1, x2)] | = | 0 |
[U31(x1, x2, x3)] | = | x2 + 5 |
[a__U171#(x1, x2, x3)] | = | 1 |
[a__U71(x1)] | = | x1 + 11 |
[a__U203#(x1,...,x4)] | = | 0 |
[a__isPLNat#(x1)] | = | x1 + 4 |
[head(x1)] | = | x1 + 6 |
[a__afterNth#(x1, x2)] | = | 0 |
[a__splitAt#(x1, x2)] | = | 0 |
[cons(x1, x2)] | = | x1 + x2 + 5 |
[a__U61(x1)] | = | 8 |
[U102(x1)] | = | 7 |
[snd(x1)] | = | x1 + 5 |
[a__take(x1, x2)] | = | x1 + 1 |
[U81(x1)] | = | x1 + 9 |
[a__U41#(x1, x2)] | = | x2 + 1 |
[tt] | = | 10 |
[a__isNatural(x1)] | = | x1 + 2 |
[a__U131(x1, x2)] | = | x2 + 6 |
[a__isNatural#(x1)] | = | x1 + 0 |
[a__fst#(x1)] | = | 0 |
[a__U212#(x1, x2)] | = | 0 |
[a__U201(x1,...,x4)] | = | 3 |
[a__U202(x1,...,x4)] | = | x4 + 4 |
[U22(x1, x2)] | = | 1 |
[U51(x1, x2)] | = | 9 |
[a__U132#(x1)] | = | 0 |
[a__tail(x1)] | = | 2 |
[U212(x1, x2)] | = | x1 + 1 |
[U41(x1, x2)] | = | x1 + x2 + 6 |
[a__tail#(x1)] | = | 0 |
[a__U203(x1,...,x4)] | = | x1 + x4 + 3 |
[a__U32#(x1, x2)] | = | 0 |
[a__U221#(x1, x2, x3)] | = | 0 |
[a__U101(x1, x2)] | = | 5 |
[a__U91#(x1)] | = | 0 |
[U121(x1)] | = | x1 + 5 |
[a__head(x1)] | = | 5 |
[U181(x1, x2)] | = | 6 |
[a__U212(x1, x2)] | = | x2 + 0 |
a__U131#(tt,V2) | → | a__isLNat#(V2) | (277) |
a__U101#(tt,V2) | → | a__isLNat#(V2) | (366) |
a__isLNat#(afterNth(V1,V2)) | → | a__isNatural#(V1) | (365) |
a__isNatural#(sel(V1,V2)) | → | a__U131#(a__isNatural(V1),V2) | (269) |
a__isPLNat#(pair(V1,V2)) | → | a__U141#(a__isLNat(V1),V2) | (363) |
a__isNatural#(sel(V1,V2)) | → | a__isNatural#(V1) | (257) |
a__U151#(tt,V2) | → | a__isLNat#(V2) | (254) |
a__isPLNat#(splitAt(V1,V2)) | → | a__isNatural#(V1) | (351) |
a__isNatural#(s(V1)) | → | a__isNatural#(V1) | (248) |
a__isLNat#(afterNth(V1,V2)) | → | a__U41#(a__isNatural(V1),V2) | (345) |
a__isPLNat#(pair(V1,V2)) | → | a__isLNat#(V1) | (239) |
a__isLNat#(natsFrom(V1)) | → | a__isNatural#(V1) | (229) |
a__isLNat#(cons(V1,V2)) | → | a__U51#(a__isNatural(V1),V2) | (226) |
a__U141#(tt,V2) | → | a__isLNat#(V2) | (223) |
a__isLNat#(cons(V1,V2)) | → | a__isNatural#(V1) | (196) |
a__U51#(tt,V2) | → | a__isLNat#(V2) | (197) |
a__isPLNat#(splitAt(V1,V2)) | → | a__U151#(a__isNatural(V1),V2) | (193) |
a__isLNat#(fst(V1)) | → | a__isPLNat#(V1) | (189) |
a__isLNat#(take(V1,V2)) | → | a__isNatural#(V1) | (297) |
a__U41#(tt,V2) | → | a__isLNat#(V2) | (186) |
a__isNatural#(head(V1)) | → | a__isLNat#(V1) | (292) |
a__isLNat#(take(V1,V2)) | → | a__U101#(a__isNatural(V1),V2) | (290) |
a__isLNat#(tail(V1)) | → | a__isLNat#(V1) | (173) |
a__isLNat#(snd(V1)) | → | a__isPLNat#(V1) | (172) |
The dependency pairs are split into 0 components.