The rewrite relation of the following TRS is considered.
There are 200 ruless (increase limit for explicit display).
There are 263 ruless (increase limit for explicit display).
The dependency pairs are split into 1 component.
There are 239 ruless (increase limit for explicit display).
[a__U143(x1)] | = | x1 + 1 |
[a__isNaturalKind#(x1)] | = | x1 + 97705 |
[a__U151(x1, x2, x3)] | = | max(x1 + 19, x2 + 26986, x3 + 18, 0) |
[a__U131#(x1, x2, x3)] | = | max(x1 + 153925, x2 + 97707, x3 + 97709, 0) |
[U21(x1, x2)] | = | max(x1 + 40500, x2 + 40520, 0) |
[a__U102(x1, x2)] | = | max(x1 + 13486, x2 + 40493, 0) |
[a__U143#(x1)] | = | 0 |
[a__U82#(x1)] | = | 0 |
[a__U152(x1, x2)] | = | max(x1 + 19, x2 + 18, 0) |
[a__U72#(x1)] | = | 0 |
[U161(x1, x2)] | = | max(x1 + 4538, x2 + 40486, 0) |
[a__U71#(x1, x2)] | = | max(x2 + 97707, 0) |
[U11(x1, x2, x3)] | = | max(x1 + 2231, x2 + 29238, x3 + 2276, 0) |
[a__U171(x1, x2, x3)] | = | max(x1 + 42728, x2 + 42726, x3 + 42724, 0) |
[a__U92#(x1)] | = | 0 |
[a__U191(x1, x2)] | = | max(x1 + 9, x2 + 6, 0) |
[a__U153(x1)] | = | x1 + 12 |
[a__U112#(x1)] | = | 0 |
[s(x1)] | = | x1 + 0 |
[a__U133#(x1)] | = | 0 |
[a__U31#(x1, x2)] | = | max(x2 + 86449, 0) |
[a__U132(x1, x2)] | = | max(x1 + 13484, x2 + 13486, 0) |
[U143(x1)] | = | x1 + 1 |
[a__head#(x1)] | = | x1 + 97707 |
[a__natsFrom#(x1)] | = | x1 + 97707 |
[isPLNatKind(x1)] | = | x1 + 1 |
[U142(x1, x2)] | = | max(x1 + 1, x2 + 7, 0) |
[a__U142#(x1, x2)] | = | max(x2 + 84226, 0) |
[a__U191#(x1, x2)] | = | max(x1 + 84230, x2 + 84224, 0) |
[isPLNat(x1)] | = | x1 + 3 |
[a__snd#(x1)] | = | x1 + 84231 |
[a__afterNth(x1, x2)] | = | max(x1 + 29238, x2 + 13479, 0) |
[U42(x1, x2)] | = | max(x1 + 31, x2 + 28, 0) |
[U91(x1, x2)] | = | max(x1 + 15715, x2 + 29476, 0) |
[U221(x1, x2, x3)] | = | max(x1 + 40490, x2 + 67497, x3 + 40535, 0) |
[a__U82(x1)] | = | x1 + 254 |
[a__U152#(x1, x2)] | = | max(x2 + 84226, 0) |
[a__U153#(x1)] | = | 0 |
[take(x1, x2)] | = | max(x1 + 67497, x2 + 53979, 0) |
[U71(x1, x2)] | = | max(x1 + 13485, x2 + 40492, 0) |
[a__U62(x1)] | = | x1 + 18562 |
[and(x1, x2)] | = | max(x1 + 7, x2 + 0, 0) |
[U131(x1, x2, x3)] | = | max(x1 + 83187, x2 + 69700, x3 + 69701, 0) |
[a__U221(x1, x2, x3)] | = | max(x1 + 40490, x2 + 67497, x3 + 40535, 0) |
[U101(x1, x2, x3)] | = | max(x1 + 40495, x2 + 40494, x3 + 40493, 0) |
[a__U43#(x1)] | = | 0 |
[pair(x1, x2)] | = | max(x1 + 10, x2 + 6, 0) |
[fst(x1)] | = | x1 + 40513 |
[U111(x1, x2)] | = | max(x1 + 493, x2 + 40455, 0) |
[U132(x1, x2)] | = | max(x1 + 13484, x2 + 13486, 0) |
[U43(x1)] | = | x1 + 4 |
[a__U121(x1, x2)] | = | max(x1 + 13484, x2 + 26967, 0) |
[U152(x1, x2)] | = | max(x1 + 19, x2 + 18, 0) |
[U103(x1)] | = | x1 + 40487 |
[a__U111(x1, x2)] | = | max(x1 + 493, x2 + 40455, 0) |
[natsFrom(x1)] | = | x1 + 40486 |
[a__U103#(x1)] | = | 0 |
[a__snd(x1)] | = | x1 + 2254 |
[a__U181#(x1, x2)] | = | max(x2 + 84230, 0) |
[a__U51#(x1, x2, x3)] | = | max(x1 + 70734, x2 + 97707, x3 + 84225, 0) |
[isNaturalKind(x1)] | = | x1 + 13483 |
[splitAt(x1, x2)] | = | max(x1 + 26984, x2 + 22, 0) |
[U72(x1)] | = | x1 + 13525 |
[a__U11#(x1, x2, x3)] | = | max(x1 + 84210, x2 + 111216, x3 + 84254, 0) |
[a__U31(x1, x2)] | = | max(x1 + 2227, x2 + 13489, 0) |
[a__U51(x1, x2, x3)] | = | max(x1 + 1, x2 + 26968, x3 + 6, 0) |
[a__U81(x1, x2)] | = | max(x1 + 1, x2 + 257, 0) |
[a__U53#(x1)] | = | 0 |
[a__take#(x1, x2)] | = | max(x1 + 111217, x2 + 124715, 0) |
[a__U43(x1)] | = | x1 + 4 |
[a__isLNatKind#(x1)] | = | x1 + 84224 |
[a__U62#(x1)] | = | 0 |
[isNatural(x1)] | = | x1 + 26967 |
[a__U42#(x1, x2)] | = | max(x1 + 84252, x2 + 84226, 0) |
[a__U41(x1, x2, x3)] | = | max(x1 + 1, x2 + 26998, x3 + 13485, 0) |
[a__U122#(x1)] | = | 0 |
[U201(x1,...,x4)] | = | max(x1 + 3, x2 + 26984, x3 + 26979, x4 + 22, 0) |
[a__U122(x1)] | = | x1 + 0 |
[a__U21#(x1, x2)] | = | max(x1 + 57218, x2 + 84224, 0) |
[a__U81#(x1, x2)] | = | max(x2 + 84223, 0) |
[a__U161(x1, x2)] | = | max(x1 + 4538, x2 + 40486, 0) |
[a__U61#(x1, x2)] | = | max(x1 + 57215, x2 + 84223, 0) |
[U141(x1, x2, x3)] | = | max(x1 + 1, x2 + 9, x3 + 7, 0) |
[a__fst(x1)] | = | x1 + 40513 |
[tail(x1)] | = | x1 + 29470 |
[a__natsFrom(x1)] | = | x1 + 40486 |
[mark#(x1)] | = | x1 + 84223 |
[0] | = | 13523 |
[a__and#(x1, x2)] | = | max(x1 + 57218, x2 + 84223, 0) |
[a__U211#(x1, x2)] | = | max(x1 + 57216, x2 + 84224, 0) |
[a__isLNat(x1)] | = | x1 + 6 |
[U191(x1, x2)] | = | max(x1 + 9, x2 + 6, 0) |
[a__U21(x1, x2)] | = | max(x1 + 40500, x2 + 40520, 0) |
[U153(x1)] | = | x1 + 12 |
[U171(x1, x2, x3)] | = | max(x1 + 42728, x2 + 42726, x3 + 42724, 0) |
[a__U91(x1, x2)] | = | max(x1 + 15715, x2 + 29476, 0) |
[sel(x1, x2)] | = | max(x1 + 69710, x2 + 69712, 0) |
[U202(x1, x2)] | = | max(x1 + 0, x2 + 26979, 0) |
[afterNth(x1, x2)] | = | max(x1 + 29238, x2 + 13479, 0) |
[a__U151#(x1, x2, x3)] | = | max(x2 + 97707, x3 + 84227, 0) |
[a__U111#(x1, x2)] | = | max(x2 + 84715, 0) |
[a__U161#(x1, x2)] | = | max(x2 + 84224, 0) |
[a__U141#(x1, x2, x3)] | = | max(x2 + 84231, x3 + 84227, 0) |
[nil] | = | 27005 |
[a__splitAt(x1, x2)] | = | max(x1 + 26984, x2 + 22, 0) |
[isLNat(x1)] | = | x1 + 6 |
[a__U142(x1, x2)] | = | max(x1 + 1, x2 + 7, 0) |
[U62(x1)] | = | x1 + 18562 |
[a__U52#(x1, x2)] | = | max(x2 + 84225, 0) |
[a__U211(x1, x2)] | = | max(x1 + 2489, x2 + 2490, 0) |
[a__U102#(x1, x2)] | = | max(x1 + 0, x2 + 97708, 0) |
[a__sel#(x1, x2)] | = | max(x1 + 153932, x2 + 153934, 0) |
[mark(x1)] | = | x1 + 0 |
[U151(x1, x2, x3)] | = | max(x1 + 19, x2 + 26986, x3 + 18, 0) |
[a__isLNat#(x1)] | = | x1 + 84225 |
[U133(x1)] | = | x1 + 1059 |
[a__U72(x1)] | = | x1 + 13525 |
[a__U101#(x1, x2, x3)] | = | max(x1 + 124715, x2 + 97707, x3 + 97709, 0) |
[a__U11(x1, x2, x3)] | = | max(x1 + 2231, x2 + 29238, x3 + 2276, 0) |
[a__U53(x1)] | = | x1 + 0 |
[a__U141(x1, x2, x3)] | = | max(x1 + 1, x2 + 9, x3 + 7, 0) |
[a__sel(x1, x2)] | = | max(x1 + 69710, x2 + 69712, 0) |
[a__U42(x1, x2)] | = | max(x1 + 31, x2 + 28, 0) |
[a__U52(x1, x2)] | = | max(x1 + 1, x2 + 6, 0) |
[a__U181(x1, x2)] | = | max(x1 + 6, x2 + 8, 0) |
[isLNatKind(x1)] | = | x1 + 1 |
[U211(x1, x2)] | = | max(x1 + 2489, x2 + 2490, 0) |
[a__U202#(x1, x2)] | = | max(x1 + 84218, x2 + 84224, 0) |
[a__U201#(x1,...,x4)] | = | max(x2 + 111203, x3 + 84225, x4 + 84244, 0) |
[a__isPLNat(x1)] | = | x1 + 3 |
[a__isLNatKind(x1)] | = | x1 + 1 |
[a__U121#(x1, x2)] | = | max(x1 + 84223, x2 + 97706, 0) |
[U52(x1, x2)] | = | max(x1 + 1, x2 + 6, 0) |
[U61(x1, x2)] | = | max(x1 + 40518, x2 + 40518, 0) |
[U31(x1, x2)] | = | max(x1 + 2227, x2 + 13489, 0) |
[a__U171#(x1, x2, x3)] | = | max(x1 + 126950, x2 + 126948, x3 + 126946, 0) |
[a__U71(x1, x2)] | = | max(x1 + 13485, x2 + 40492, 0) |
[U92(x1)] | = | x1 + 16688 |
[a__isPLNat#(x1)] | = | x1 + 84222 |
[head(x1)] | = | x1 + 13488 |
[a__afterNth#(x1, x2)] | = | max(x1 + 111217, x2 + 97701, 0) |
[U112(x1)] | = | x1 + 40449 |
[a__splitAt#(x1, x2)] | = | max(x1 + 111203, x2 + 84244, 0) |
[a__isPLNatKind#(x1)] | = | x1 + 84219 |
[cons(x1, x2)] | = | max(x1 + 26962, x2 + 0, 0) |
[a__U92(x1)] | = | x1 + 16688 |
[a__U61(x1, x2)] | = | max(x1 + 40518, x2 + 40518, 0) |
[U102(x1, x2)] | = | max(x1 + 13486, x2 + 40493, 0) |
[snd(x1)] | = | x1 + 2254 |
[a__take(x1, x2)] | = | max(x1 + 67497, x2 + 53979, 0) |
[U81(x1, x2)] | = | max(x1 + 1, x2 + 257, 0) |
[a__U41#(x1, x2, x3)] | = | max(x2 + 111220, x3 + 97703, 0) |
[U82(x1)] | = | x1 + 254 |
[a__isNatural(x1)] | = | x1 + 26967 |
[tt] | = | 27006 |
[a__U131(x1, x2, x3)] | = | max(x1 + 83187, x2 + 69700, x3 + 69701, 0) |
[a__isNaturalKind(x1)] | = | x1 + 13483 |
[a__isNatural#(x1)] | = | x1 + 97706 |
[a__fst#(x1)] | = | x1 + 84231 |
[a__U133(x1)] | = | x1 + 1059 |
[a__U201(x1,...,x4)] | = | max(x1 + 3, x2 + 26984, x3 + 26979, x4 + 22, 0) |
[a__U202(x1, x2)] | = | max(x1 + 0, x2 + 26979, 0) |
[U51(x1, x2, x3)] | = | max(x1 + 1, x2 + 26968, x3 + 6, 0) |
[a__U132#(x1, x2)] | = | max(x2 + 97708, 0) |
[a__and(x1, x2)] | = | max(x1 + 7, x2 + 0, 0) |
[a__tail(x1)] | = | x1 + 29470 |
[a__U103(x1)] | = | x1 + 40487 |
[a__isPLNatKind(x1)] | = | x1 + 1 |
[U53(x1)] | = | x1 + 0 |
[a__U112(x1)] | = | x1 + 40449 |
[U41(x1, x2, x3)] | = | max(x1 + 1, x2 + 26998, x3 + 13485, 0) |
[a__tail#(x1)] | = | x1 + 97707 |
[a__U221#(x1, x2, x3)] | = | max(x1 + 84210, x2 + 111216, x3 + 124714, 0) |
[a__U101(x1, x2, x3)] | = | max(x1 + 40495, x2 + 40494, x3 + 40493, 0) |
[a__U91#(x1, x2)] | = | max(x2 + 84226, 0) |
[U121(x1, x2)] | = | max(x1 + 13484, x2 + 26967, 0) |
[a__head(x1)] | = | x1 + 13488 |
[U181(x1, x2)] | = | max(x1 + 6, x2 + 8, 0) |
[U122(x1)] | = | x1 + 0 |
There are 200 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair), the pairsThere are 223 ruless (increase limit for explicit display).
could be deleted.The dependency pairs are split into 5 components.
a__isNaturalKind#(s(V1)) | → | a__isNaturalKind#(V1) | (395) |
[a__U143(x1)] | = | x1 + 3 |
[a__isNaturalKind#(x1)] | = | x1 + 2 |
[a__U151(x1, x2, x3)] | = | x2 + 6 |
[a__U131#(x1, x2, x3)] | = | 2 |
[U21(x1, x2)] | = | x2 + 4 |
[a__U102(x1, x2)] | = | x2 + 11 |
[a__U143#(x1)] | = | 0 |
[a__U82#(x1)] | = | 0 |
[a__U152(x1, x2)] | = | x2 + 7 |
[a__U72#(x1)] | = | 0 |
[U161(x1, x2)] | = | x2 + 7 |
[a__U71#(x1, x2)] | = | 2 |
[U11(x1, x2, x3)] | = | 8 |
[a__U171(x1, x2, x3)] | = | x2 + x3 + 5 |
[a__U92#(x1)] | = | 0 |
[a__U191(x1, x2)] | = | x2 + 8 |
[a__U153(x1)] | = | 8 |
[a__U112#(x1)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[a__U133#(x1)] | = | 0 |
[a__U31#(x1, x2)] | = | 2 |
[a__U132(x1, x2)] | = | 11 |
[U143(x1)] | = | 4 |
[a__head#(x1)] | = | 0 |
[a__natsFrom#(x1)] | = | 2 |
[isPLNatKind(x1)] | = | 2 |
[U142(x1, x2)] | = | x1 + 8 |
[a__U142#(x1, x2)] | = | 2 |
[a__U191#(x1, x2)] | = | 2 |
[isPLNat(x1)] | = | 6 |
[a__snd#(x1)] | = | 1 |
[a__afterNth(x1, x2)] | = | 5 |
[U42(x1, x2)] | = | x1 + x2 + 12 |
[U91(x1, x2)] | = | x1 + 7 |
[U221(x1, x2, x3)] | = | x3 + 6 |
[a__U82(x1)] | = | 7 |
[a__U152#(x1, x2)] | = | 2 |
[a__U153#(x1)] | = | 0 |
[take(x1, x2)] | = | x2 + 2 |
[U71(x1, x2)] | = | 7 |
[a__U62(x1)] | = | 7 |
[and(x1, x2)] | = | 1 |
[U131(x1, x2, x3)] | = | 2 |
[a__U221(x1, x2, x3)] | = | x2 + 5 |
[U101(x1, x2, x3)] | = | 2 |
[a__U43#(x1)] | = | 0 |
[pair(x1, x2)] | = | x1 + 1 |
[fst(x1)] | = | x1 + 2 |
[U111(x1, x2)] | = | x1 + 6 |
[U132(x1, x2)] | = | x1 + 12 |
[U43(x1)] | = | 8 |
[a__U121(x1, x2)] | = | x1 + x2 + 1 |
[U152(x1, x2)] | = | 8 |
[U103(x1)] | = | 1 |
[a__U111(x1, x2)] | = | x2 + 5 |
[natsFrom(x1)] | = | x1 + 6 |
[a__U103#(x1)] | = | 0 |
[a__snd(x1)] | = | x1 + 1 |
[a__U181#(x1, x2)] | = | 0 |
[a__U51#(x1, x2, x3)] | = | 2 |
[isNaturalKind(x1)] | = | 6 |
[splitAt(x1, x2)] | = | x2 + 4 |
[U72(x1)] | = | 7 |
[a__U11#(x1, x2, x3)] | = | 2 |
[a__U31(x1, x2)] | = | x2 + 0 |
[a__U51(x1, x2, x3)] | = | x1 + x2 + 1 |
[a__U81(x1, x2)] | = | 6 |
[a__U53#(x1)] | = | 0 |
[a__take#(x1, x2)] | = | 2 |
[a__U43(x1)] | = | x1 + 7 |
[a__isLNatKind#(x1)] | = | 2 |
[a__U62#(x1)] | = | 0 |
[isNatural(x1)] | = | 0 |
[a__U42#(x1, x2)] | = | 0 |
[a__U41(x1, x2, x3)] | = | x1 + x3 + 1 |
[a__U122#(x1)] | = | 0 |
[U201(x1,...,x4)] | = | x1 + 6 |
[a__U122(x1)] | = | 0 |
[a__U21#(x1, x2)] | = | 2 |
[a__U81#(x1, x2)] | = | 0 |
[a__U161(x1, x2)] | = | 6 |
[a__U61#(x1, x2)] | = | 2 |
[U141(x1, x2, x3)] | = | x1 + 7 |
[a__fst(x1)] | = | x1 + 1 |
[tail(x1)] | = | 0 |
[a__natsFrom(x1)] | = | 5 |
[mark#(x1)] | = | 2 |
[0] | = | 4 |
[a__and#(x1, x2)] | = | 2 |
[a__U211#(x1, x2)] | = | 0 |
[a__isLNat(x1)] | = | 5 |
[U191(x1, x2)] | = | 9 |
[a__U21(x1, x2)] | = | x2 + 3 |
[U153(x1)] | = | x1 + 9 |
[U171(x1, x2, x3)] | = | x1 + 6 |
[a__U91(x1, x2)] | = | x1 + x2 + 6 |
[sel(x1, x2)] | = | 1 |
[U202(x1, x2)] | = | 10827 |
[afterNth(x1, x2)] | = | x2 + 6 |
[a__U151#(x1, x2, x3)] | = | 2 |
[a__U111#(x1, x2)] | = | 2 |
[a__U161#(x1, x2)] | = | 2 |
[a__U141#(x1, x2, x3)] | = | 2 |
[nil] | = | 8 |
[a__splitAt(x1, x2)] | = | x1 + 3 |
[isLNat(x1)] | = | x1 + 6 |
[a__U142(x1, x2)] | = | x2 + 7 |
[U62(x1)] | = | x1 + 8 |
[a__U52#(x1, x2)] | = | 2 |
[a__U211(x1, x2)] | = | 10828 |
[a__U102#(x1, x2)] | = | 2 |
[a__sel#(x1, x2)] | = | 2 |
[mark(x1)] | = | 4 |
[U151(x1, x2, x3)] | = | x3 + 7 |
[a__isLNat#(x1)] | = | 2 |
[U133(x1)] | = | x1 + 13 |
[a__U72(x1)] | = | x1 + 6 |
[a__U101#(x1, x2, x3)] | = | 2 |
[a__U11(x1, x2, x3)] | = | x2 + x3 + 7 |
[a__U53(x1)] | = | x1 + 7 |
[a__U141(x1, x2, x3)] | = | x2 + 6 |
[a__sel(x1, x2)] | = | x1 + x2 + 0 |
[a__U42(x1, x2)] | = | 11 |
[a__U52(x1, x2)] | = | x2 + 11 |
[a__U181(x1, x2)] | = | x2 + 3 |
[isLNatKind(x1)] | = | 7 |
[U211(x1, x2)] | = | x1 + 10829 |
[a__U202#(x1, x2)] | = | 0 |
[a__U201#(x1,...,x4)] | = | 2 |
[a__isPLNat(x1)] | = | 5 |
[a__isLNatKind(x1)] | = | 0 |
[a__U121#(x1, x2)] | = | 2 |
[U52(x1, x2)] | = | x1 + 12 |
[U61(x1, x2)] | = | 7 |
[U31(x1, x2)] | = | 1 |
[a__U171#(x1, x2, x3)] | = | 0 |
[a__U71(x1, x2)] | = | x2 + 6 |
[U92(x1)] | = | 1 |
[a__isPLNat#(x1)] | = | 2 |
[head(x1)] | = | x1 + 2 |
[a__afterNth#(x1, x2)] | = | 2 |
[U112(x1)] | = | 2 |
[a__splitAt#(x1, x2)] | = | 2 |
[a__isPLNatKind#(x1)] | = | 2 |
[cons(x1, x2)] | = | 10826 |
[a__U92(x1)] | = | 0 |
[a__U61(x1, x2)] | = | x2 + 6 |
[U102(x1, x2)] | = | x1 + 12 |
[snd(x1)] | = | x1 + 2 |
[a__take(x1, x2)] | = | x2 + 1 |
[U81(x1, x2)] | = | x2 + 7 |
[a__U41#(x1, x2, x3)] | = | 2 |
[U82(x1)] | = | 8 |
[a__isNatural(x1)] | = | 1 |
[tt] | = | 9 |
[a__U131(x1, x2, x3)] | = | x1 + 1 |
[a__isNaturalKind(x1)] | = | x1 + 5 |
[a__isNatural#(x1)] | = | 2 |
[a__fst#(x1)] | = | 2 |
[a__U133(x1)] | = | 12 |
[a__U201(x1,...,x4)] | = | x3 + x4 + 5 |
[a__U202(x1, x2)] | = | 10826 |
[U51(x1, x2, x3)] | = | 2 |
[a__U132#(x1, x2)] | = | 2 |
[a__and(x1, x2)] | = | x2 + 0 |
[a__tail(x1)] | = | x1 + 1 |
[a__U103(x1)] | = | 0 |
[a__isPLNatKind(x1)] | = | x1 + 1 |
[U53(x1)] | = | 8 |
[a__U112(x1)] | = | x1 + 1 |
[U41(x1, x2, x3)] | = | x2 + 2 |
[a__tail#(x1)] | = | 2 |
[a__U221#(x1, x2, x3)] | = | 2 |
[a__U101(x1, x2, x3)] | = | x1 + x2 + 1 |
[a__U91#(x1, x2)] | = | 2 |
[U121(x1, x2)] | = | 2 |
[a__head(x1)] | = | x1 + 1 |
[U181(x1, x2)] | = | x1 + 4 |
[U122(x1)] | = | x1 + 1 |
a__isNaturalKind#(s(V1)) | → | a__isNaturalKind#(V1) | (395) |
The dependency pairs are split into 0 components.
a__isNatural#(s(V1)) | → | a__U121#(a__isNaturalKind(V1),V1) | (291) |
a__U121#(tt,V1) | → | a__isNatural#(V1) | (260) |
[a__U143(x1)] | = | x1 + 3 |
[a__isNaturalKind#(x1)] | = | 2 |
[a__U151(x1, x2, x3)] | = | x2 + 6 |
[a__U131#(x1, x2, x3)] | = | 2 |
[U21(x1, x2)] | = | x2 + 4 |
[a__U102(x1, x2)] | = | x2 + 11 |
[a__U143#(x1)] | = | 0 |
[a__U82#(x1)] | = | 0 |
[a__U152(x1, x2)] | = | x2 + 7 |
[a__U72#(x1)] | = | 0 |
[U161(x1, x2)] | = | x2 + 7 |
[a__U71#(x1, x2)] | = | 2 |
[U11(x1, x2, x3)] | = | 7 |
[a__U171(x1, x2, x3)] | = | x2 + x3 + 5 |
[a__U92#(x1)] | = | 0 |
[a__U191(x1, x2)] | = | x2 + 7 |
[a__U153(x1)] | = | 8 |
[a__U112#(x1)] | = | 0 |
[s(x1)] | = | x1 + 2 |
[a__U133#(x1)] | = | 0 |
[a__U31#(x1, x2)] | = | 2 |
[a__U132(x1, x2)] | = | 11 |
[U143(x1)] | = | 4 |
[a__head#(x1)] | = | 0 |
[a__natsFrom#(x1)] | = | 2 |
[isPLNatKind(x1)] | = | 2 |
[U142(x1, x2)] | = | x1 + 8 |
[a__U142#(x1, x2)] | = | 2 |
[a__U191#(x1, x2)] | = | 2 |
[isPLNat(x1)] | = | 6 |
[a__snd#(x1)] | = | 1 |
[a__afterNth(x1, x2)] | = | 5 |
[U42(x1, x2)] | = | x1 + x2 + 12 |
[U91(x1, x2)] | = | x1 + 7 |
[U221(x1, x2, x3)] | = | x3 + 6 |
[a__U82(x1)] | = | 7 |
[a__U152#(x1, x2)] | = | 2 |
[a__U153#(x1)] | = | 0 |
[take(x1, x2)] | = | x2 + 2 |
[U71(x1, x2)] | = | 7 |
[a__U62(x1)] | = | 7 |
[and(x1, x2)] | = | 12112 |
[U131(x1, x2, x3)] | = | 2 |
[a__U221(x1, x2, x3)] | = | x2 + 5 |
[U101(x1, x2, x3)] | = | 2 |
[a__U43#(x1)] | = | 0 |
[pair(x1, x2)] | = | x1 + 1 |
[fst(x1)] | = | x1 + 2 |
[U111(x1, x2)] | = | x1 + 6 |
[U132(x1, x2)] | = | x1 + 12 |
[U43(x1)] | = | 8 |
[a__U121(x1, x2)] | = | x1 + x2 + 1 |
[U152(x1, x2)] | = | 8 |
[U103(x1)] | = | 1 |
[a__U111(x1, x2)] | = | x2 + 5 |
[natsFrom(x1)] | = | x1 + 6 |
[a__U103#(x1)] | = | 0 |
[a__snd(x1)] | = | x1 + 1 |
[a__U181#(x1, x2)] | = | 0 |
[a__U51#(x1, x2, x3)] | = | 2 |
[isNaturalKind(x1)] | = | 6 |
[splitAt(x1, x2)] | = | x2 + 3 |
[U72(x1)] | = | 7 |
[a__U11#(x1, x2, x3)] | = | 2 |
[a__U31(x1, x2)] | = | x2 + 0 |
[a__U51(x1, x2, x3)] | = | x1 + x2 + 1 |
[a__U81(x1, x2)] | = | 6 |
[a__U53#(x1)] | = | 0 |
[a__take#(x1, x2)] | = | 2 |
[a__U43(x1)] | = | x1 + 7 |
[a__isLNatKind#(x1)] | = | 2 |
[a__U62#(x1)] | = | 0 |
[isNatural(x1)] | = | 0 |
[a__U42#(x1, x2)] | = | 0 |
[a__U41(x1, x2, x3)] | = | x1 + x3 + 1 |
[a__U122#(x1)] | = | 0 |
[U201(x1,...,x4)] | = | x1 + 6 |
[a__U122(x1)] | = | 0 |
[a__U21#(x1, x2)] | = | 2 |
[a__U81#(x1, x2)] | = | 0 |
[a__U161(x1, x2)] | = | 6 |
[a__U61#(x1, x2)] | = | 2 |
[U141(x1, x2, x3)] | = | x1 + 7 |
[a__fst(x1)] | = | x1 + 1 |
[tail(x1)] | = | 0 |
[a__natsFrom(x1)] | = | 5 |
[mark#(x1)] | = | 2 |
[0] | = | 4 |
[a__and#(x1, x2)] | = | 2 |
[a__U211#(x1, x2)] | = | 0 |
[a__isLNat(x1)] | = | 5 |
[U191(x1, x2)] | = | 8 |
[a__U21(x1, x2)] | = | x2 + 3 |
[U153(x1)] | = | x1 + 9 |
[U171(x1, x2, x3)] | = | x1 + 6 |
[a__U91(x1, x2)] | = | x1 + x2 + 6 |
[sel(x1, x2)] | = | 17006 |
[U202(x1, x2)] | = | 10827 |
[afterNth(x1, x2)] | = | x2 + 6 |
[a__U151#(x1, x2, x3)] | = | 2 |
[a__U111#(x1, x2)] | = | 2 |
[a__U161#(x1, x2)] | = | 2 |
[a__U141#(x1, x2, x3)] | = | 2 |
[nil] | = | 8 |
[a__splitAt(x1, x2)] | = | x1 + 2 |
[isLNat(x1)] | = | x1 + 6 |
[a__U142(x1, x2)] | = | x2 + 7 |
[U62(x1)] | = | x1 + 8 |
[a__U52#(x1, x2)] | = | 2 |
[a__U211(x1, x2)] | = | x2 + 10828 |
[a__U102#(x1, x2)] | = | 2 |
[a__sel#(x1, x2)] | = | 2 |
[mark(x1)] | = | 4 |
[U151(x1, x2, x3)] | = | x3 + 7 |
[a__isLNat#(x1)] | = | 2 |
[U133(x1)] | = | x1 + 13 |
[a__U72(x1)] | = | x1 + 6 |
[a__U101#(x1, x2, x3)] | = | 2 |
[a__U11(x1, x2, x3)] | = | x2 + x3 + 6 |
[a__U53(x1)] | = | x1 + 7 |
[a__U141(x1, x2, x3)] | = | x2 + 6 |
[a__sel(x1, x2)] | = | x1 + x2 + 0 |
[a__U42(x1, x2)] | = | 11 |
[a__U52(x1, x2)] | = | x2 + 11 |
[a__U181(x1, x2)] | = | x2 + 3 |
[isLNatKind(x1)] | = | 17009 |
[U211(x1, x2)] | = | x1 + 10829 |
[a__U202#(x1, x2)] | = | 0 |
[a__U201#(x1,...,x4)] | = | 2 |
[a__isPLNat(x1)] | = | 5 |
[a__isLNatKind(x1)] | = | 0 |
[a__U121#(x1, x2)] | = | x2 + 3 |
[U52(x1, x2)] | = | x1 + 12 |
[U61(x1, x2)] | = | 7 |
[U31(x1, x2)] | = | 1 |
[a__U171#(x1, x2, x3)] | = | 0 |
[a__U71(x1, x2)] | = | x2 + 6 |
[U92(x1)] | = | 1 |
[a__isPLNat#(x1)] | = | 2 |
[head(x1)] | = | x1 + 2 |
[a__afterNth#(x1, x2)] | = | 2 |
[U112(x1)] | = | 2 |
[a__splitAt#(x1, x2)] | = | 2 |
[a__isPLNatKind#(x1)] | = | 2 |
[cons(x1, x2)] | = | 10826 |
[a__U92(x1)] | = | 0 |
[a__U61(x1, x2)] | = | x2 + 6 |
[U102(x1, x2)] | = | x1 + 12 |
[snd(x1)] | = | x1 + 2 |
[a__take(x1, x2)] | = | x2 + 1 |
[U81(x1, x2)] | = | x2 + 7 |
[a__U41#(x1, x2, x3)] | = | 2 |
[U82(x1)] | = | 8 |
[a__isNatural(x1)] | = | 1 |
[tt] | = | 9 |
[a__U131(x1, x2, x3)] | = | x1 + 1 |
[a__isNaturalKind(x1)] | = | x1 + 5 |
[a__isNatural#(x1)] | = | x1 + 2 |
[a__fst#(x1)] | = | 2 |
[a__U133(x1)] | = | 12 |
[a__U201(x1,...,x4)] | = | x3 + x4 + 5 |
[a__U202(x1, x2)] | = | 10826 |
[U51(x1, x2, x3)] | = | 2 |
[a__U132#(x1, x2)] | = | 2 |
[a__and(x1, x2)] | = | x2 + 3 |
[a__tail(x1)] | = | x1 + 1 |
[a__U103(x1)] | = | 0 |
[a__isPLNatKind(x1)] | = | x1 + 1 |
[U53(x1)] | = | 8 |
[a__U112(x1)] | = | x1 + 1 |
[U41(x1, x2, x3)] | = | x2 + 2 |
[a__tail#(x1)] | = | 2 |
[a__U221#(x1, x2, x3)] | = | 2 |
[a__U101(x1, x2, x3)] | = | x1 + x2 + 1 |
[a__U91#(x1, x2)] | = | 2 |
[U121(x1, x2)] | = | 2 |
[a__head(x1)] | = | x1 + 1 |
[U181(x1, x2)] | = | x1 + 4 |
[U122(x1)] | = | x1 + 1 |
a__isNatural#(s(V1)) | → | a__U121#(a__isNaturalKind(V1),V1) | (291) |
a__U121#(tt,V1) | → | a__isNatural#(V1) | (260) |
The dependency pairs are split into 0 components.
a__U201#(tt,N,X,XS) | → | a__splitAt#(mark(N),mark(XS)) | (324) |
a__splitAt#(s(N),cons(X,XS)) | → | a__U201#(a__and(a__and(a__isNatural(N),isNaturalKind(N)),and(and(isNatural(X),isNaturalKind(X)),and(isLNat(XS),isLNatKind(XS)))),N,X,XS) | (453) |
π(a__U131#) | = | 3 |
π(a__U133#) | = | 1 |
π(a__U31#) | = | 1 |
π(a__head#) | = | 1 |
π(isPLNat) | = | 1 |
π(a__U153#) | = | 1 |
π(and) | = | 2 |
π(a__U103#) | = | 1 |
π(a__U181#) | = | 1 |
π(a__U161#) | = | 2 |
π(a__U52#) | = | 2 |
π(mark) | = | 1 |
π(a__U201#) | = | 2 |
π(a__isPLNat) | = | 1 |
π(a__splitAt#) | = | 1 |
π(a__isPLNatKind#) | = | 1 |
π(a__isNatural#) | = | 1 |
π(a__fst#) | = | 1 |
π(a__and) | = | 2 |
π(a__U91#) | = | 2 |
prec(a__U143) | = | 0 | status(a__U143) | = | [] | list-extension(a__U143) | = | Lex | ||
prec(a__isNaturalKind#) | = | 0 | status(a__isNaturalKind#) | = | [] | list-extension(a__isNaturalKind#) | = | Lex | ||
prec(a__U151) | = | 10 | status(a__U151) | = | [] | list-extension(a__U151) | = | Lex | ||
prec(U21) | = | 1 | status(U21) | = | [2] | list-extension(U21) | = | Lex | ||
prec(a__U102) | = | 7 | status(a__U102) | = | [] | list-extension(a__U102) | = | Lex | ||
prec(a__U143#) | = | 0 | status(a__U143#) | = | [] | list-extension(a__U143#) | = | Lex | ||
prec(a__U82#) | = | 0 | status(a__U82#) | = | [] | list-extension(a__U82#) | = | Lex | ||
prec(a__U152) | = | 8 | status(a__U152) | = | [] | list-extension(a__U152) | = | Lex | ||
prec(a__U72#) | = | 0 | status(a__U72#) | = | [] | list-extension(a__U72#) | = | Lex | ||
prec(U161) | = | 8 | status(U161) | = | [] | list-extension(U161) | = | Lex | ||
prec(a__U71#) | = | 0 | status(a__U71#) | = | [1, 2] | list-extension(a__U71#) | = | Lex | ||
prec(U11) | = | 6 | status(U11) | = | [] | list-extension(U11) | = | Lex | ||
prec(a__U171) | = | 15 | status(a__U171) | = | [3, 2] | list-extension(a__U171) | = | Lex | ||
prec(a__U92#) | = | 0 | status(a__U92#) | = | [] | list-extension(a__U92#) | = | Lex | ||
prec(a__U191) | = | 0 | status(a__U191) | = | [] | list-extension(a__U191) | = | Lex | ||
prec(a__U153) | = | 7 | status(a__U153) | = | [] | list-extension(a__U153) | = | Lex | ||
prec(a__U112#) | = | 0 | status(a__U112#) | = | [] | list-extension(a__U112#) | = | Lex | ||
prec(s) | = | 10 | status(s) | = | [1] | list-extension(s) | = | Lex | ||
prec(a__U132) | = | 13 | status(a__U132) | = | [] | list-extension(a__U132) | = | Lex | ||
prec(U143) | = | 0 | status(U143) | = | [] | list-extension(U143) | = | Lex | ||
prec(a__natsFrom#) | = | 0 | status(a__natsFrom#) | = | [] | list-extension(a__natsFrom#) | = | Lex | ||
prec(isPLNatKind) | = | 3 | status(isPLNatKind) | = | [] | list-extension(isPLNatKind) | = | Lex | ||
prec(U142) | = | 0 | 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(a__snd#) | = | 0 | status(a__snd#) | = | [] | list-extension(a__snd#) | = | Lex | ||
prec(a__afterNth) | = | 15 | status(a__afterNth) | = | [] | list-extension(a__afterNth) | = | Lex | ||
prec(U42) | = | 7 | status(U42) | = | [] | list-extension(U42) | = | Lex | ||
prec(U91) | = | 9 | status(U91) | = | [] | list-extension(U91) | = | Lex | ||
prec(U221) | = | 11 | status(U221) | = | [3] | list-extension(U221) | = | Lex | ||
prec(a__U82) | = | 4 | status(a__U82) | = | [] | list-extension(a__U82) | = | Lex | ||
prec(a__U152#) | = | 0 | status(a__U152#) | = | [1, 2] | list-extension(a__U152#) | = | Lex | ||
prec(take) | = | 13 | status(take) | = | [] | list-extension(take) | = | Lex | ||
prec(U71) | = | 12 | status(U71) | = | [] | list-extension(U71) | = | Lex | ||
prec(a__U62) | = | 7 | status(a__U62) | = | [] | list-extension(a__U62) | = | Lex | ||
prec(U131) | = | 13 | status(U131) | = | [] | list-extension(U131) | = | Lex | ||
prec(a__U221) | = | 11 | status(a__U221) | = | [3] | list-extension(a__U221) | = | Lex | ||
prec(U101) | = | 7 | status(U101) | = | [3] | list-extension(U101) | = | Lex | ||
prec(a__U43#) | = | 0 | status(a__U43#) | = | [] | list-extension(a__U43#) | = | Lex | ||
prec(pair) | = | 2 | status(pair) | = | [] | list-extension(pair) | = | Lex | ||
prec(fst) | = | 0 | status(fst) | = | [1] | list-extension(fst) | = | Lex | ||
prec(U111) | = | 13 | status(U111) | = | [] | list-extension(U111) | = | Lex | ||
prec(U132) | = | 13 | status(U132) | = | [] | list-extension(U132) | = | Lex | ||
prec(U43) | = | 7 | status(U43) | = | [] | list-extension(U43) | = | Lex | ||
prec(a__U121) | = | 4 | status(a__U121) | = | [] | list-extension(a__U121) | = | Lex | ||
prec(U152) | = | 8 | status(U152) | = | [] | list-extension(U152) | = | Lex | ||
prec(U103) | = | 7 | status(U103) | = | [] | list-extension(U103) | = | Lex | ||
prec(a__U111) | = | 13 | status(a__U111) | = | [] | list-extension(a__U111) | = | Lex | ||
prec(natsFrom) | = | 8 | status(natsFrom) | = | [1] | list-extension(natsFrom) | = | Lex | ||
prec(a__snd) | = | 6 | status(a__snd) | = | [] | list-extension(a__snd) | = | Lex | ||
prec(a__U51#) | = | 0 | status(a__U51#) | = | [2, 1, 3] | list-extension(a__U51#) | = | Lex | ||
prec(isNaturalKind) | = | 3 | status(isNaturalKind) | = | [] | list-extension(isNaturalKind) | = | Lex | ||
prec(splitAt) | = | 10 | status(splitAt) | = | [2] | list-extension(splitAt) | = | Lex | ||
prec(U72) | = | 4 | status(U72) | = | [] | list-extension(U72) | = | Lex | ||
prec(a__U11#) | = | 0 | status(a__U11#) | = | [2, 1, 3] | list-extension(a__U11#) | = | Lex | ||
prec(a__U31) | = | 7 | status(a__U31) | = | [] | list-extension(a__U31) | = | Lex | ||
prec(a__U51) | = | 8 | status(a__U51) | = | [] | list-extension(a__U51) | = | Lex | ||
prec(a__U81) | = | 7 | status(a__U81) | = | [1, 2] | list-extension(a__U81) | = | Lex | ||
prec(a__U53#) | = | 0 | status(a__U53#) | = | [] | list-extension(a__U53#) | = | Lex | ||
prec(a__take#) | = | 0 | status(a__take#) | = | [2, 1] | list-extension(a__take#) | = | Lex | ||
prec(a__U43) | = | 7 | status(a__U43) | = | [] | list-extension(a__U43) | = | Lex | ||
prec(a__isLNatKind#) | = | 0 | status(a__isLNatKind#) | = | [] | list-extension(a__isLNatKind#) | = | Lex | ||
prec(a__U62#) | = | 0 | status(a__U62#) | = | [] | list-extension(a__U62#) | = | Lex | ||
prec(isNatural) | = | 5 | status(isNatural) | = | [] | list-extension(isNatural) | = | Lex | ||
prec(a__U42#) | = | 0 | status(a__U42#) | = | [1, 2] | list-extension(a__U42#) | = | Lex | ||
prec(a__U41) | = | 8 | status(a__U41) | = | [] | list-extension(a__U41) | = | Lex | ||
prec(a__U122#) | = | 0 | status(a__U122#) | = | [] | list-extension(a__U122#) | = | Lex | ||
prec(U201) | = | 9 | status(U201) | = | [4, 2, 1, 3] | list-extension(U201) | = | Lex | ||
prec(a__U122) | = | 4 | status(a__U122) | = | [] | list-extension(a__U122) | = | Lex | ||
prec(a__U21#) | = | 0 | status(a__U21#) | = | [] | list-extension(a__U21#) | = | Lex | ||
prec(a__U81#) | = | 0 | status(a__U81#) | = | [] | list-extension(a__U81#) | = | Lex | ||
prec(a__U161) | = | 8 | status(a__U161) | = | [] | list-extension(a__U161) | = | Lex | ||
prec(a__U61#) | = | 0 | status(a__U61#) | = | [2, 1] | list-extension(a__U61#) | = | Lex | ||
prec(U141) | = | 2 | status(U141) | = | [] | list-extension(U141) | = | Lex | ||
prec(a__fst) | = | 0 | status(a__fst) | = | [1] | list-extension(a__fst) | = | Lex | ||
prec(tail) | = | 8 | status(tail) | = | [] | list-extension(tail) | = | Lex | ||
prec(a__natsFrom) | = | 8 | status(a__natsFrom) | = | [1] | list-extension(a__natsFrom) | = | Lex | ||
prec(mark#) | = | 0 | status(mark#) | = | [] | list-extension(mark#) | = | Lex | ||
prec(0) | = | 7 | status(0) | = | [] | list-extension(0) | = | Lex | ||
prec(a__and#) | = | 0 | status(a__and#) | = | [1, 2] | list-extension(a__and#) | = | Lex | ||
prec(a__U211#) | = | 0 | status(a__U211#) | = | [2] | list-extension(a__U211#) | = | Lex | ||
prec(a__isLNat) | = | 12 | status(a__isLNat) | = | [] | list-extension(a__isLNat) | = | Lex | ||
prec(U191) | = | 0 | status(U191) | = | [] | list-extension(U191) | = | Lex | ||
prec(a__U21) | = | 1 | status(a__U21) | = | [2] | list-extension(a__U21) | = | Lex | ||
prec(U153) | = | 7 | status(U153) | = | [] | list-extension(U153) | = | Lex | ||
prec(U171) | = | 15 | status(U171) | = | [3, 2] | list-extension(U171) | = | Lex | ||
prec(a__U91) | = | 9 | status(a__U91) | = | [] | list-extension(a__U91) | = | Lex | ||
prec(sel) | = | 16 | status(sel) | = | [] | list-extension(sel) | = | Lex | ||
prec(U202) | = | 8 | status(U202) | = | [] | list-extension(U202) | = | Lex | ||
prec(afterNth) | = | 15 | status(afterNth) | = | [] | list-extension(afterNth) | = | Lex | ||
prec(a__U151#) | = | 0 | status(a__U151#) | = | [2, 3, 1] | list-extension(a__U151#) | = | Lex | ||
prec(a__U111#) | = | 0 | status(a__U111#) | = | [2, 1] | list-extension(a__U111#) | = | Lex | ||
prec(a__U141#) | = | 0 | status(a__U141#) | = | [2, 1, 3] | list-extension(a__U141#) | = | Lex | ||
prec(nil) | = | 7 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(a__splitAt) | = | 10 | status(a__splitAt) | = | [2] | list-extension(a__splitAt) | = | Lex | ||
prec(isLNat) | = | 12 | status(isLNat) | = | [] | list-extension(isLNat) | = | Lex | ||
prec(a__U142) | = | 0 | status(a__U142) | = | [] | list-extension(a__U142) | = | Lex | ||
prec(U62) | = | 7 | status(U62) | = | [] | list-extension(U62) | = | Lex | ||
prec(a__U211) | = | 8 | status(a__U211) | = | [] | list-extension(a__U211) | = | Lex | ||
prec(a__U102#) | = | 0 | status(a__U102#) | = | [1] | list-extension(a__U102#) | = | Lex | ||
prec(a__sel#) | = | 0 | status(a__sel#) | = | [1, 2] | list-extension(a__sel#) | = | Lex | ||
prec(U151) | = | 10 | status(U151) | = | [] | list-extension(U151) | = | Lex | ||
prec(a__isLNat#) | = | 0 | status(a__isLNat#) | = | [] | list-extension(a__isLNat#) | = | Lex | ||
prec(U133) | = | 13 | status(U133) | = | [] | list-extension(U133) | = | Lex | ||
prec(a__U72) | = | 4 | status(a__U72) | = | [] | list-extension(a__U72) | = | Lex | ||
prec(a__U101#) | = | 0 | status(a__U101#) | = | [1, 3, 2] | list-extension(a__U101#) | = | Lex | ||
prec(a__U11) | = | 6 | status(a__U11) | = | [] | list-extension(a__U11) | = | Lex | ||
prec(a__U53) | = | 7 | status(a__U53) | = | [] | list-extension(a__U53) | = | Lex | ||
prec(a__U141) | = | 2 | status(a__U141) | = | [] | list-extension(a__U141) | = | Lex | ||
prec(a__sel) | = | 16 | status(a__sel) | = | [] | list-extension(a__sel) | = | Lex | ||
prec(a__U42) | = | 7 | status(a__U42) | = | [] | list-extension(a__U42) | = | Lex | ||
prec(a__U52) | = | 7 | status(a__U52) | = | [] | list-extension(a__U52) | = | Lex | ||
prec(a__U181) | = | 3 | status(a__U181) | = | [] | list-extension(a__U181) | = | Lex | ||
prec(isLNatKind) | = | 3 | status(isLNatKind) | = | [] | list-extension(isLNatKind) | = | Lex | ||
prec(U211) | = | 8 | status(U211) | = | [] | list-extension(U211) | = | Lex | ||
prec(a__U202#) | = | 0 | status(a__U202#) | = | [2, 1] | list-extension(a__U202#) | = | Lex | ||
prec(a__isLNatKind) | = | 3 | status(a__isLNatKind) | = | [] | list-extension(a__isLNatKind) | = | Lex | ||
prec(a__U121#) | = | 0 | status(a__U121#) | = | [2, 1] | list-extension(a__U121#) | = | Lex | ||
prec(U52) | = | 7 | status(U52) | = | [] | list-extension(U52) | = | Lex | ||
prec(U61) | = | 12 | status(U61) | = | [] | list-extension(U61) | = | Lex | ||
prec(U31) | = | 7 | status(U31) | = | [] | list-extension(U31) | = | Lex | ||
prec(a__U171#) | = | 0 | status(a__U171#) | = | [2, 1, 3] | list-extension(a__U171#) | = | Lex | ||
prec(a__U71) | = | 12 | status(a__U71) | = | [] | list-extension(a__U71) | = | Lex | ||
prec(U92) | = | 7 | status(U92) | = | [] | list-extension(U92) | = | Lex | ||
prec(a__isPLNat#) | = | 0 | status(a__isPLNat#) | = | [] | list-extension(a__isPLNat#) | = | Lex | ||
prec(head) | = | 14 | status(head) | = | [1] | list-extension(head) | = | Lex | ||
prec(a__afterNth#) | = | 0 | status(a__afterNth#) | = | [2, 1] | list-extension(a__afterNth#) | = | Lex | ||
prec(U112) | = | 3 | status(U112) | = | [] | list-extension(U112) | = | Lex | ||
prec(cons) | = | 7 | status(cons) | = | [1] | list-extension(cons) | = | Lex | ||
prec(a__U92) | = | 7 | status(a__U92) | = | [] | list-extension(a__U92) | = | Lex | ||
prec(a__U61) | = | 12 | status(a__U61) | = | [] | list-extension(a__U61) | = | Lex | ||
prec(U102) | = | 7 | status(U102) | = | [] | list-extension(U102) | = | Lex | ||
prec(snd) | = | 6 | status(snd) | = | [] | list-extension(snd) | = | Lex | ||
prec(a__take) | = | 13 | status(a__take) | = | [] | list-extension(a__take) | = | Lex | ||
prec(U81) | = | 7 | status(U81) | = | [1, 2] | list-extension(U81) | = | Lex | ||
prec(a__U41#) | = | 0 | status(a__U41#) | = | [3, 2, 1] | list-extension(a__U41#) | = | Lex | ||
prec(U82) | = | 4 | status(U82) | = | [] | list-extension(U82) | = | Lex | ||
prec(a__isNatural) | = | 5 | status(a__isNatural) | = | [] | list-extension(a__isNatural) | = | Lex | ||
prec(tt) | = | 4 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(a__U131) | = | 13 | status(a__U131) | = | [] | list-extension(a__U131) | = | Lex | ||
prec(a__isNaturalKind) | = | 3 | status(a__isNaturalKind) | = | [] | list-extension(a__isNaturalKind) | = | Lex | ||
prec(a__U133) | = | 13 | status(a__U133) | = | [] | list-extension(a__U133) | = | Lex | ||
prec(a__U201) | = | 9 | status(a__U201) | = | [4, 2, 1, 3] | list-extension(a__U201) | = | Lex | ||
prec(a__U202) | = | 8 | status(a__U202) | = | [] | list-extension(a__U202) | = | Lex | ||
prec(U51) | = | 8 | status(U51) | = | [] | list-extension(U51) | = | Lex | ||
prec(a__U132#) | = | 0 | status(a__U132#) | = | [1, 2] | list-extension(a__U132#) | = | Lex | ||
prec(a__tail) | = | 8 | status(a__tail) | = | [] | list-extension(a__tail) | = | Lex | ||
prec(a__U103) | = | 7 | status(a__U103) | = | [] | list-extension(a__U103) | = | Lex | ||
prec(a__isPLNatKind) | = | 3 | status(a__isPLNatKind) | = | [] | list-extension(a__isPLNatKind) | = | Lex | ||
prec(U53) | = | 7 | status(U53) | = | [] | list-extension(U53) | = | Lex | ||
prec(a__U112) | = | 3 | status(a__U112) | = | [] | list-extension(a__U112) | = | Lex | ||
prec(U41) | = | 8 | status(U41) | = | [] | list-extension(U41) | = | Lex | ||
prec(a__tail#) | = | 0 | status(a__tail#) | = | [] | list-extension(a__tail#) | = | Lex | ||
prec(a__U221#) | = | 0 | status(a__U221#) | = | [1] | list-extension(a__U221#) | = | Lex | ||
prec(a__U101) | = | 7 | status(a__U101) | = | [3] | list-extension(a__U101) | = | Lex | ||
prec(U121) | = | 4 | status(U121) | = | [] | list-extension(U121) | = | Lex | ||
prec(a__head) | = | 14 | status(a__head) | = | [1] | list-extension(a__head) | = | Lex | ||
prec(U181) | = | 3 | status(U181) | = | [] | list-extension(U181) | = | Lex | ||
prec(U122) | = | 4 | status(U122) | = | [] | list-extension(U122) | = | Lex |
[a__U143(x1)] | = | 94131 |
[a__isNaturalKind#(x1)] | = | 1 |
[a__U151(x1, x2, x3)] | = | max(x2 + 62807, x3 + 156950, 0) |
[U21(x1, x2)] | = | max(x2 + 23934, 0) |
[a__U102(x1, x2)] | = | max(x2 + 345374, 0) |
[a__U143#(x1)] | = | 1 |
[a__U82#(x1)] | = | 1 |
[a__U152(x1, x2)] | = | max(x1 + 23710, 0) |
[a__U72#(x1)] | = | 1 |
[U161(x1, x2)] | = | max(x2 + 5, 0) |
[a__U71#(x1, x2)] | = | x1 + x2 + 1 |
[U11(x1, x2, x3)] | = | max(x1 + 219763, x2 + 219761, x3 + 282570, 0) |
[a__U171(x1, x2, x3)] | = | max(x1 + 321673, x2 + 321674, x3 + 321672, 0) |
[a__U92#(x1)] | = | 1 |
[a__U191(x1, x2)] | = | max(x2 + 219757, 0) |
[a__U153(x1)] | = | 86515 |
[a__U112#(x1)] | = | 1 |
[s(x1)] | = | x1 + 0 |
[a__U132(x1, x2)] | = | max(x2 + 62806, 0) |
[U143(x1)] | = | 94131 |
[a__natsFrom#(x1)] | = | 1 |
[isPLNatKind(x1)] | = | 62810 |
[U142(x1, x2)] | = | max(x2 + 94131, 0) |
[a__U142#(x1, x2)] | = | x2 + 1 |
[a__U191#(x1, x2)] | = | x1 + x2 + 1 |
[a__snd#(x1)] | = | 1 |
[a__afterNth(x1, x2)] | = | max(x1 + 219762, x2 + 282574, 0) |
[U42(x1, x2)] | = | max(x1 + 243468, 0) |
[U91(x1, x2)] | = | max(x1 + 0, 0) |
[U221(x1, x2, x3)] | = | max(x2 + 282568, x3 + 282569, 0) |
[a__U82(x1)] | = | x1 + 0 |
[a__U152#(x1, x2)] | = | x1 + x2 + 1 |
[take(x1, x2)] | = | x1 + x2 + 282570 |
[U71(x1, x2)] | = | max(x2 + 62808, 0) |
[a__U62(x1)] | = | 62805 |
[U131(x1, x2, x3)] | = | max(x1 + 0, x3 + 384485, 0) |
[a__U221(x1, x2, x3)] | = | max(x2 + 282568, x3 + 282569, 0) |
[U101(x1, x2, x3)] | = | max(x3 + 345374, 0) |
[a__U43#(x1)] | = | 1 |
[pair(x1, x2)] | = | max(x1 + 156944, x2 + 219756, 0) |
[fst(x1)] | = | x1 + 62810 |
[U111(x1, x2)] | = | max(x1 + 15382, x2 + 78189, 0) |
[U132(x1, x2)] | = | max(x2 + 62806, 0) |
[U43(x1)] | = | 62805 |
[a__U121(x1, x2)] | = | max(x2 + 39096, 0) |
[U152(x1, x2)] | = | max(x1 + 23710, 0) |
[U103(x1)] | = | 62805 |
[a__U111(x1, x2)] | = | max(x1 + 15382, x2 + 78189, 0) |
[natsFrom(x1)] | = | x1 + 5 |
[a__snd(x1)] | = | x1 + 62812 |
[a__U51#(x1, x2, x3)] | = | max(x1 + 1, x2 + 1, x3 + 1, 0) |
[isNaturalKind(x1)] | = | 62810 |
[splitAt(x1, x2)] | = | max(x1 + 156949, x2 + 219757, 0) |
[U72(x1)] | = | 62807 |
[a__U11#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U31(x1, x2)] | = | max(x2 + 39097, 0) |
[a__U51(x1, x2, x3)] | = | max(x2 + 62804, 0) |
[a__U81(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U53#(x1)] | = | 1 |
[a__take#(x1, x2)] | = | x1 + x2 + 1 |
[a__U43(x1)] | = | 62805 |
[a__isLNatKind#(x1)] | = | 1 |
[a__U62#(x1)] | = | 1 |
[isNatural(x1)] | = | x1 + 39096 |
[a__U42#(x1, x2)] | = | x1 + x2 + 1 |
[a__U41(x1, x2, x3)] | = | max(x1 + 0, x2 + 282565, 0) |
[a__U122#(x1)] | = | 1 |
[U201(x1,...,x4)] | = | max(x1 + 94138, x2 + 156949, x3 + 156950, x4 + 219757, 0) |
[a__U122(x1)] | = | x1 + 0 |
[a__U21#(x1, x2)] | = | x2 + 1 |
[a__U81#(x1, x2)] | = | x2 + 1 |
[a__U161(x1, x2)] | = | max(x2 + 5, 0) |
[a__U61#(x1, x2)] | = | x1 + x2 + 1 |
[U141(x1, x2, x3)] | = | max(x1 + 94133, x3 + 94132, 0) |
[a__fst(x1)] | = | x1 + 62810 |
[tail(x1)] | = | x1 + 6 |
[a__natsFrom(x1)] | = | x1 + 5 |
[mark#(x1)] | = | 1 |
[0] | = | 62809 |
[a__and#(x1, x2)] | = | max(x1 + 1, x2 + 1, 0) |
[a__U211#(x1, x2)] | = | x2 + 1 |
[a__isLNat(x1)] | = | x1 + 62804 |
[U191(x1, x2)] | = | max(x2 + 219757, 0) |
[a__U21(x1, x2)] | = | max(x2 + 23934, 0) |
[U153(x1)] | = | 86515 |
[U171(x1, x2, x3)] | = | max(x1 + 321673, x2 + 321674, x3 + 321672, 0) |
[a__U91(x1, x2)] | = | max(x1 + 0, 0) |
[sel(x1, x2)] | = | x1 + x2 + 384484 |
[U202(x1, x2)] | = | max(x1 + 0, x2 + 156945, 0) |
[afterNth(x1, x2)] | = | max(x1 + 219762, x2 + 282574, 0) |
[a__U151#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U111#(x1, x2)] | = | x1 + x2 + 1 |
[a__U141#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[nil] | = | 62806 |
[a__splitAt(x1, x2)] | = | max(x1 + 156949, x2 + 219757, 0) |
[isLNat(x1)] | = | x1 + 62804 |
[a__U142(x1, x2)] | = | max(x2 + 94131, 0) |
[U62(x1)] | = | 62805 |
[a__U211(x1, x2)] | = | max(x2 + 1, 0) |
[a__U102#(x1, x2)] | = | x1 + 1 |
[a__sel#(x1, x2)] | = | x1 + x2 + 1 |
[U151(x1, x2, x3)] | = | max(x2 + 62807, x3 + 156950, 0) |
[a__isLNat#(x1)] | = | 1 |
[U133(x1)] | = | 62805 |
[a__U72(x1)] | = | 62807 |
[a__U101#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U11(x1, x2, x3)] | = | max(x1 + 219763, x2 + 219761, x3 + 282570, 0) |
[a__U53(x1)] | = | 62805 |
[a__U141(x1, x2, x3)] | = | max(x1 + 94133, x3 + 94132, 0) |
[a__sel(x1, x2)] | = | x1 + x2 + 384484 |
[a__U42(x1, x2)] | = | max(x1 + 243468, 0) |
[a__U52(x1, x2)] | = | max(x1 + 0, 0) |
[a__U181(x1, x2)] | = | max(x1 + 219757, x2 + 219758, 0) |
[isLNatKind(x1)] | = | 62810 |
[U211(x1, x2)] | = | max(x2 + 1, 0) |
[a__U202#(x1, x2)] | = | x1 + x2 + 1 |
[a__isLNatKind(x1)] | = | 62810 |
[a__U121#(x1, x2)] | = | x1 + x2 + 1 |
[U52(x1, x2)] | = | max(x1 + 0, 0) |
[U61(x1, x2)] | = | max(x2 + 62806, 0) |
[U31(x1, x2)] | = | max(x2 + 39097, 0) |
[a__U171#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[a__U71(x1, x2)] | = | max(x2 + 62808, 0) |
[U92(x1)] | = | 62805 |
[a__isPLNat#(x1)] | = | 1 |
[head(x1)] | = | x1 + 39097 |
[a__afterNth#(x1, x2)] | = | x1 + x2 + 1 |
[U112(x1)] | = | 78188 |
[cons(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U92(x1)] | = | 62805 |
[a__U61(x1, x2)] | = | max(x2 + 62806, 0) |
[U102(x1, x2)] | = | max(x2 + 345374, 0) |
[snd(x1)] | = | x1 + 62812 |
[a__take(x1, x2)] | = | x1 + x2 + 282570 |
[U81(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[a__U41#(x1, x2, x3)] | = | x1 + x2 + x3 + 1 |
[U82(x1)] | = | x1 + 0 |
[a__isNatural(x1)] | = | x1 + 39096 |
[tt] | = | 62805 |
[a__U131(x1, x2, x3)] | = | max(x1 + 0, x3 + 384485, 0) |
[a__isNaturalKind(x1)] | = | 62810 |
[a__U133(x1)] | = | 62805 |
[a__U201(x1,...,x4)] | = | max(x1 + 94138, x2 + 156949, x3 + 156950, x4 + 219757, 0) |
[a__U202(x1, x2)] | = | max(x1 + 0, x2 + 156945, 0) |
[U51(x1, x2, x3)] | = | max(x2 + 62804, 0) |
[a__U132#(x1, x2)] | = | x1 + x2 + 1 |
[a__tail(x1)] | = | x1 + 6 |
[a__U103(x1)] | = | 62805 |
[a__isPLNatKind(x1)] | = | 62810 |
[U53(x1)] | = | 62805 |
[a__U112(x1)] | = | 78188 |
[U41(x1, x2, x3)] | = | max(x1 + 0, x2 + 282565, 0) |
[a__tail#(x1)] | = | 1 |
[a__U221#(x1, x2, x3)] | = | x1 + 1 |
[a__U101(x1, x2, x3)] | = | max(x3 + 345374, 0) |
[U121(x1, x2)] | = | max(x2 + 39096, 0) |
[a__head(x1)] | = | x1 + 39097 |
[U181(x1, x2)] | = | max(x1 + 219757, x2 + 219758, 0) |
[U122(x1)] | = | x1 + 0 |
There are 200 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__and(a__and(a__isNatural(N),isNaturalKind(N)),and(and(isNatural(X),isNaturalKind(X)),and(isLNat(XS),isLNatKind(XS)))),N,X,XS) | (453) |
The dependency pairs are split into 0 components.
a__U52#(tt,V2) | → | a__isLNat#(V2) | (438) |
a__U51#(tt,V1,V2) | → | a__U52#(a__isNatural(V1),V2) | (352) |
a__isLNat#(cons(V1,V2)) | → | a__U51#(a__and(a__isNaturalKind(V1),isLNatKind(V2)),V1,V2) | (223) |
[a__U143(x1)] | = | x1 + 20 |
[a__isNaturalKind#(x1)] | = | 2 |
[a__U151(x1, x2, x3)] | = | 9 |
[a__U131#(x1, x2, x3)] | = | 2 |
[U21(x1, x2)] | = | x1 + x2 + 20 |
[a__U102(x1, x2)] | = | 7 |
[a__U143#(x1)] | = | 0 |
[a__U82#(x1)] | = | 0 |
[a__U152(x1, x2)] | = | x2 + 10 |
[a__U72#(x1)] | = | 0 |
[U161(x1, x2)] | = | x1 + 9 |
[a__U71#(x1, x2)] | = | 2 |
[U11(x1, x2, x3)] | = | x2 + 3 |
[a__U171(x1, x2, x3)] | = | 7 |
[a__U92#(x1)] | = | 0 |
[a__U191(x1, x2)] | = | 10 |
[a__U153(x1)] | = | 11 |
[a__U112#(x1)] | = | 0 |
[s(x1)] | = | 7 |
[a__U133#(x1)] | = | 0 |
[a__U31#(x1, x2)] | = | 2 |
[a__U132(x1, x2)] | = | x2 + 9 |
[U143(x1)] | = | 21 |
[a__head#(x1)] | = | 0 |
[a__natsFrom#(x1)] | = | 2 |
[isPLNatKind(x1)] | = | 5 |
[U142(x1, x2)] | = | x1 + 27 |
[a__U142#(x1, x2)] | = | 2 |
[a__U191#(x1, x2)] | = | 2 |
[isPLNat(x1)] | = | 8 |
[a__snd#(x1)] | = | 1 |
[a__afterNth(x1, x2)] | = | x1 + 1 |
[U42(x1, x2)] | = | x1 + x2 + 10 |
[U91(x1, x2)] | = | x1 + 12 |
[U221(x1, x2, x3)] | = | x1 + x3 + 9 |
[a__U82(x1)] | = | 11 |
[a__U152#(x1, x2)] | = | 2 |
[a__U153#(x1)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 8 |
[U71(x1, x2)] | = | 2 |
[a__U62(x1)] | = | 9 |
[and(x1, x2)] | = | x1 + x2 + 6 |
[U131(x1, x2, x3)] | = | 9 |
[a__U221(x1, x2, x3)] | = | x2 + 8 |
[U101(x1, x2, x3)] | = | 4 |
[a__U43#(x1)] | = | 0 |
[pair(x1, x2)] | = | 17 |
[fst(x1)] | = | 2 |
[U111(x1, x2)] | = | x1 + 9 |
[U132(x1, x2)] | = | x1 + 10 |
[U43(x1)] | = | 16 |
[a__U121(x1, x2)] | = | x1 + x2 + 1 |
[U152(x1, x2)] | = | x1 + 11 |
[U103(x1)] | = | 12 |
[a__U111(x1, x2)] | = | x2 + 8 |
[natsFrom(x1)] | = | 8 |
[a__U103#(x1)] | = | 0 |
[a__snd(x1)] | = | 3 |
[a__U181#(x1, x2)] | = | 0 |
[a__U51#(x1, x2, x3)] | = | x3 + 2 |
[isNaturalKind(x1)] | = | 11 |
[splitAt(x1, x2)] | = | x2 + 1 |
[U72(x1)] | = | 12 |
[a__U11#(x1, x2, x3)] | = | 2 |
[a__U31(x1, x2)] | = | 0 |
[a__U51(x1, x2, x3)] | = | x1 + x2 + 3 |
[a__U81(x1, x2)] | = | 8 |
[a__U53#(x1)] | = | 0 |
[a__take#(x1, x2)] | = | 2 |
[a__U43(x1)] | = | x1 + 15 |
[a__isLNatKind#(x1)] | = | 2 |
[a__U62#(x1)] | = | 0 |
[isNatural(x1)] | = | x1 + 8 |
[a__U42#(x1, x2)] | = | 0 |
[a__U41(x1, x2, x3)] | = | x1 + x2 + 3 |
[a__U122#(x1)] | = | 0 |
[U201(x1,...,x4)] | = | x1 + x2 + x4 + 16 |
[a__U122(x1)] | = | 11 |
[a__U21#(x1, x2)] | = | 2 |
[a__U81#(x1, x2)] | = | 0 |
[a__U161(x1, x2)] | = | x2 + 8 |
[a__U61#(x1, x2)] | = | 2 |
[U141(x1, x2, x3)] | = | x1 + 26 |
[a__fst(x1)] | = | x1 + 1 |
[tail(x1)] | = | 2 |
[a__natsFrom(x1)] | = | 7 |
[mark#(x1)] | = | 2 |
[0] | = | 9 |
[a__and#(x1, x2)] | = | 2 |
[a__U211#(x1, x2)] | = | 0 |
[a__isLNat(x1)] | = | 7 |
[U191(x1, x2)] | = | x1 + x2 + 11 |
[a__U21(x1, x2)] | = | 19 |
[U153(x1)] | = | x1 + 12 |
[U171(x1, x2, x3)] | = | x1 + x3 + 8 |
[a__U91(x1, x2)] | = | x1 + 11 |
[sel(x1, x2)] | = | 1 |
[U202(x1, x2)] | = | x1 + 17 |
[afterNth(x1, x2)] | = | x1 + x2 + 2 |
[a__U151#(x1, x2, x3)] | = | 2 |
[a__U111#(x1, x2)] | = | 2 |
[a__U161#(x1, x2)] | = | 2 |
[a__U141#(x1, x2, x3)] | = | 2 |
[nil] | = | 7 |
[a__splitAt(x1, x2)] | = | x1 + x2 + 0 |
[isLNat(x1)] | = | x1 + 8 |
[a__U142(x1, x2)] | = | x2 + 26 |
[U62(x1)] | = | x1 + 10 |
[a__U52#(x1, x2)] | = | x2 + 1 |
[a__U211(x1, x2)] | = | 9 |
[a__U102#(x1, x2)] | = | 2 |
[a__sel#(x1, x2)] | = | 2 |
[mark(x1)] | = | 6 |
[U151(x1, x2, x3)] | = | 10 |
[a__isLNat#(x1)] | = | x1 + 0 |
[U133(x1)] | = | x1 + 12 |
[a__U72(x1)] | = | 11 |
[a__U101#(x1, x2, x3)] | = | 2 |
[a__U11(x1, x2, x3)] | = | x3 + 2 |
[a__U53(x1)] | = | 8 |
[a__U141(x1, x2, x3)] | = | x2 + x3 + 25 |
[a__sel(x1, x2)] | = | x1 + x2 + 0 |
[a__U42(x1, x2)] | = | x1 + 9 |
[a__U52(x1, x2)] | = | 7 |
[a__U181(x1, x2)] | = | 4 |
[isLNatKind(x1)] | = | x1 + 2 |
[U211(x1, x2)] | = | x1 + 10 |
[a__U202#(x1, x2)] | = | 0 |
[a__U201#(x1,...,x4)] | = | 3 |
[a__isPLNat(x1)] | = | x1 + 7 |
[a__isLNatKind(x1)] | = | x1 + 1 |
[a__U121#(x1, x2)] | = | 3 |
[U52(x1, x2)] | = | x1 + x2 + 8 |
[U61(x1, x2)] | = | x1 + 9 |
[U31(x1, x2)] | = | x2 + 1 |
[a__U171#(x1, x2, x3)] | = | 0 |
[a__U71(x1, x2)] | = | x1 + x2 + 1 |
[U92(x1)] | = | 18 |
[a__isPLNat#(x1)] | = | 2 |
[head(x1)] | = | 9 |
[a__afterNth#(x1, x2)] | = | 2 |
[U112(x1)] | = | 3 |
[a__splitAt#(x1, x2)] | = | 2 |
[a__isPLNatKind#(x1)] | = | 2 |
[cons(x1, x2)] | = | x2 + 7 |
[a__U92(x1)] | = | x1 + 17 |
[a__U61(x1, x2)] | = | x2 + 8 |
[U102(x1, x2)] | = | x1 + 8 |
[snd(x1)] | = | x1 + 0 |
[a__take(x1, x2)] | = | 7 |
[U81(x1, x2)] | = | x2 + 9 |
[a__U41#(x1, x2, x3)] | = | 2 |
[U82(x1)] | = | 12 |
[a__isNatural(x1)] | = | 7 |
[tt] | = | 12 |
[a__U131(x1, x2, x3)] | = | 8 |
[a__isNaturalKind(x1)] | = | 10 |
[a__isNatural#(x1)] | = | 2 |
[a__fst#(x1)] | = | 2 |
[a__U133(x1)] | = | 11 |
[a__U201(x1,...,x4)] | = | x3 + 15 |
[a__U202(x1, x2)] | = | 16 |
[U51(x1, x2, x3)] | = | 4 |
[a__U132#(x1, x2)] | = | 2 |
[a__and(x1, x2)] | = | 5 |
[a__tail(x1)] | = | x1 + 1 |
[a__U103(x1)] | = | 11 |
[a__isPLNatKind(x1)] | = | 4 |
[U53(x1)] | = | x1 + 9 |
[a__U112(x1)] | = | x1 + 2 |
[U41(x1, x2, x3)] | = | x3 + 4 |
[a__tail#(x1)] | = | 2 |
[a__U221#(x1, x2, x3)] | = | 2 |
[a__U101(x1, x2, x3)] | = | x1 + x2 + 3 |
[a__U91#(x1, x2)] | = | 2 |
[U121(x1, x2)] | = | 2 |
[a__head(x1)] | = | 8 |
[U181(x1, x2)] | = | x2 + 5 |
[U122(x1)] | = | 12 |
a__U52#(tt,V2) | → | a__isLNat#(V2) | (438) |
a__U51#(tt,V1,V2) | → | a__U52#(a__isNatural(V1),V2) | (352) |
a__isLNat#(cons(V1,V2)) | → | a__U51#(a__and(a__isNaturalKind(V1),isLNatKind(V2)),V1,V2) | (223) |
The dependency pairs are split into 0 components.
mark#(U53(X)) | → | mark#(X) | (388) |
mark#(s(X)) | → | mark#(X) | (463) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (399) |
mark#(U122(X)) | → | mark#(X) | (358) |
mark#(isLNatKind(X)) | → | a__isLNatKind#(X) | (335) |
a__isLNatKind#(cons(V1,V2)) | → | a__and#(a__isNaturalKind(V1),isLNatKind(V2)) | (403) |
mark#(U202(X1,X2)) | → | mark#(X1) | (325) |
a__and#(tt,X) | → | mark#(X) | (361) |
[a__U143(x1)] | = | x1 + 20 |
[a__isNaturalKind#(x1)] | = | 2 |
[a__U151(x1, x2, x3)] | = | 9 |
[a__U131#(x1, x2, x3)] | = | 2 |
[U21(x1, x2)] | = | x1 + x2 + 20 |
[a__U102(x1, x2)] | = | 7 |
[a__U143#(x1)] | = | 0 |
[a__U82#(x1)] | = | 0 |
[a__U152(x1, x2)] | = | x2 + 10 |
[a__U72#(x1)] | = | 0 |
[U161(x1, x2)] | = | x1 + 9 |
[a__U71#(x1, x2)] | = | 2 |
[U11(x1, x2, x3)] | = | x2 + 3 |
[a__U171(x1, x2, x3)] | = | 7 |
[a__U92#(x1)] | = | 0 |
[a__U191(x1, x2)] | = | 8 |
[a__U153(x1)] | = | 11 |
[a__U112#(x1)] | = | 0 |
[s(x1)] | = | x1 + 1 |
[a__U133#(x1)] | = | 0 |
[a__U31#(x1, x2)] | = | 2 |
[a__U132(x1, x2)] | = | x2 + 9 |
[U143(x1)] | = | 21 |
[a__head#(x1)] | = | 0 |
[a__natsFrom#(x1)] | = | 2 |
[isPLNatKind(x1)] | = | 5 |
[U142(x1, x2)] | = | x1 + 27 |
[a__U142#(x1, x2)] | = | 2 |
[a__U191#(x1, x2)] | = | 2 |
[isPLNat(x1)] | = | 8 |
[a__snd#(x1)] | = | 1 |
[a__afterNth(x1, x2)] | = | x1 + 1 |
[U42(x1, x2)] | = | x1 + x2 + 10 |
[U91(x1, x2)] | = | x1 + 12 |
[U221(x1, x2, x3)] | = | x1 + x3 + 9 |
[a__U82(x1)] | = | 9 |
[a__U152#(x1, x2)] | = | 2 |
[a__U153#(x1)] | = | 0 |
[take(x1, x2)] | = | x1 + x2 + 8 |
[U71(x1, x2)] | = | 2 |
[a__U62(x1)] | = | 9 |
[and(x1, x2)] | = | x1 + x2 + 6 |
[U131(x1, x2, x3)] | = | 9 |
[a__U221(x1, x2, x3)] | = | x2 + 8 |
[U101(x1, x2, x3)] | = | 4 |
[a__U43#(x1)] | = | 0 |
[pair(x1, x2)] | = | 17 |
[fst(x1)] | = | 2 |
[U111(x1, x2)] | = | x1 + 9 |
[U132(x1, x2)] | = | x1 + 10 |
[U43(x1)] | = | 16 |
[a__U121(x1, x2)] | = | x1 + x2 + 1 |
[U152(x1, x2)] | = | x1 + 11 |
[U103(x1)] | = | 9 |
[a__U111(x1, x2)] | = | x2 + 8 |
[natsFrom(x1)] | = | 8 |
[a__U103#(x1)] | = | 0 |
[a__snd(x1)] | = | 3 |
[a__U181#(x1, x2)] | = | 0 |
[a__U51#(x1, x2, x3)] | = | 2 |
[isNaturalKind(x1)] | = | 11 |
[splitAt(x1, x2)] | = | x2 + 1 |
[U72(x1)] | = | 8 |
[a__U11#(x1, x2, x3)] | = | 2 |
[a__U31(x1, x2)] | = | 0 |
[a__U51(x1, x2, x3)] | = | x1 + x2 + 3 |
[a__U81(x1, x2)] | = | 8 |
[a__U53#(x1)] | = | 0 |
[a__take#(x1, x2)] | = | 2 |
[a__U43(x1)] | = | x1 + 15 |
[a__isLNatKind#(x1)] | = | x1 + 31392 |
[a__U62#(x1)] | = | 0 |
[isNatural(x1)] | = | x1 + 8919 |
[a__U42#(x1, x2)] | = | 0 |
[a__U41(x1, x2, x3)] | = | x1 + x2 + 3 |
[a__U122#(x1)] | = | 0 |
[U201(x1,...,x4)] | = | x1 + x2 + x4 + 16 |
[a__U122(x1)] | = | 7 |
[a__U21#(x1, x2)] | = | 2 |
[a__U81#(x1, x2)] | = | 0 |
[a__U161(x1, x2)] | = | x2 + 8 |
[a__U61#(x1, x2)] | = | 2 |
[U141(x1, x2, x3)] | = | x1 + 26 |
[a__fst(x1)] | = | x1 + 1 |
[tail(x1)] | = | 2 |
[a__natsFrom(x1)] | = | 7 |
[mark#(x1)] | = | x1 + 2 |
[0] | = | 7 |
[a__and#(x1, x2)] | = | x2 + 3 |
[a__U211#(x1, x2)] | = | 0 |
[a__isLNat(x1)] | = | 7 |
[U191(x1, x2)] | = | x1 + x2 + 9 |
[a__U21(x1, x2)] | = | 19 |
[U153(x1)] | = | x1 + 12 |
[U171(x1, x2, x3)] | = | x1 + x3 + 8 |
[a__U91(x1, x2)] | = | x1 + 11 |
[sel(x1, x2)] | = | 1 |
[U202(x1, x2)] | = | x1 + 17 |
[afterNth(x1, x2)] | = | x1 + x2 + 2 |
[a__U151#(x1, x2, x3)] | = | 2 |
[a__U111#(x1, x2)] | = | 2 |
[a__U161#(x1, x2)] | = | 2 |
[a__U141#(x1, x2, x3)] | = | 2 |
[nil] | = | 7 |
[a__splitAt(x1, x2)] | = | x1 + x2 + 0 |
[isLNat(x1)] | = | x1 + 30367 |
[a__U142(x1, x2)] | = | x2 + 26 |
[U62(x1)] | = | x1 + 10 |
[a__U52#(x1, x2)] | = | 1 |
[a__U211(x1, x2)] | = | 9 |
[a__U102#(x1, x2)] | = | 2 |
[a__sel#(x1, x2)] | = | 2 |
[mark(x1)] | = | 6 |
[U151(x1, x2, x3)] | = | 10 |
[a__isLNat#(x1)] | = | 0 |
[U133(x1)] | = | x1 + 11 |
[a__U72(x1)] | = | 7 |
[a__U101#(x1, x2, x3)] | = | 2 |
[a__U11(x1, x2, x3)] | = | x3 + 2 |
[a__U53(x1)] | = | 8 |
[a__U141(x1, x2, x3)] | = | x2 + x3 + 25 |
[a__sel(x1, x2)] | = | x1 + x2 + 0 |
[a__U42(x1, x2)] | = | x1 + 9 |
[a__U52(x1, x2)] | = | 7 |
[a__U181(x1, x2)] | = | 4 |
[isLNatKind(x1)] | = | x1 + 31391 |
[U211(x1, x2)] | = | x1 + 10 |
[a__U202#(x1, x2)] | = | 0 |
[a__U201#(x1,...,x4)] | = | 3 |
[a__isPLNat(x1)] | = | x1 + 7 |
[a__isLNatKind(x1)] | = | x1 + 1 |
[a__U121#(x1, x2)] | = | 3 |
[U52(x1, x2)] | = | x1 + x2 + 8 |
[U61(x1, x2)] | = | x1 + 9 |
[U31(x1, x2)] | = | x2 + 1 |
[a__U171#(x1, x2, x3)] | = | 0 |
[a__U71(x1, x2)] | = | x1 + x2 + 1 |
[U92(x1)] | = | 18 |
[a__isPLNat#(x1)] | = | 2 |
[head(x1)] | = | 9 |
[a__afterNth#(x1, x2)] | = | 2 |
[U112(x1)] | = | 3 |
[a__splitAt#(x1, x2)] | = | 2 |
[a__isPLNatKind#(x1)] | = | 2 |
[cons(x1, x2)] | = | x2 + 7 |
[a__U92(x1)] | = | x1 + 17 |
[a__U61(x1, x2)] | = | x2 + 8 |
[U102(x1, x2)] | = | x1 + 8 |
[snd(x1)] | = | x1 + 0 |
[a__take(x1, x2)] | = | 7 |
[U81(x1, x2)] | = | x2 + 9 |
[a__U41#(x1, x2, x3)] | = | 2 |
[U82(x1)] | = | 10 |
[a__isNatural(x1)] | = | 7 |
[tt] | = | 12 |
[a__U131(x1, x2, x3)] | = | 8 |
[a__isNaturalKind(x1)] | = | 10 |
[a__isNatural#(x1)] | = | 2 |
[a__fst#(x1)] | = | 2 |
[a__U133(x1)] | = | 10 |
[a__U201(x1,...,x4)] | = | x3 + 15 |
[a__U202(x1, x2)] | = | 16 |
[U51(x1, x2, x3)] | = | 4 |
[a__U132#(x1, x2)] | = | 2 |
[a__and(x1, x2)] | = | 5 |
[a__tail(x1)] | = | x1 + 1 |
[a__U103(x1)] | = | 8 |
[a__isPLNatKind(x1)] | = | 4 |
[U53(x1)] | = | x1 + 9 |
[a__U112(x1)] | = | x1 + 2 |
[U41(x1, x2, x3)] | = | x3 + 4 |
[a__tail#(x1)] | = | 2 |
[a__U221#(x1, x2, x3)] | = | 2 |
[a__U101(x1, x2, x3)] | = | x1 + x2 + 3 |
[a__U91#(x1, x2)] | = | 2 |
[U121(x1, x2)] | = | 2 |
[a__head(x1)] | = | 8 |
[U181(x1, x2)] | = | x2 + 5 |
[U122(x1)] | = | x1 + 8 |
mark#(U53(X)) | → | mark#(X) | (388) |
mark#(s(X)) | → | mark#(X) | (463) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (399) |
mark#(U122(X)) | → | mark#(X) | (358) |
mark#(isLNatKind(X)) | → | a__isLNatKind#(X) | (335) |
a__isLNatKind#(cons(V1,V2)) | → | a__and#(a__isNaturalKind(V1),isLNatKind(V2)) | (403) |
mark#(U202(X1,X2)) | → | mark#(X1) | (325) |
a__and#(tt,X) | → | mark#(X) | (361) |
The dependency pairs are split into 0 components.