The rewrite relation of the following TRS is considered.
active(natsFrom(N)) |
→ |
mark(cons(N,natsFrom(s(N)))) |
(1) |
active(fst(pair(XS,YS))) |
→ |
mark(XS) |
(2) |
active(snd(pair(XS,YS))) |
→ |
mark(YS) |
(3) |
active(splitAt(0,XS)) |
→ |
mark(pair(nil,XS)) |
(4) |
active(splitAt(s(N),cons(X,XS))) |
→ |
mark(u(splitAt(N,XS),N,X,XS)) |
(5) |
active(u(pair(YS,ZS),N,X,XS)) |
→ |
mark(pair(cons(X,YS),ZS)) |
(6) |
active(head(cons(N,XS))) |
→ |
mark(N) |
(7) |
active(tail(cons(N,XS))) |
→ |
mark(XS) |
(8) |
active(sel(N,XS)) |
→ |
mark(head(afterNth(N,XS))) |
(9) |
active(take(N,XS)) |
→ |
mark(fst(splitAt(N,XS))) |
(10) |
active(afterNth(N,XS)) |
→ |
mark(snd(splitAt(N,XS))) |
(11) |
active(natsFrom(X)) |
→ |
natsFrom(active(X)) |
(12) |
active(cons(X1,X2)) |
→ |
cons(active(X1),X2) |
(13) |
active(s(X)) |
→ |
s(active(X)) |
(14) |
active(fst(X)) |
→ |
fst(active(X)) |
(15) |
active(pair(X1,X2)) |
→ |
pair(active(X1),X2) |
(16) |
active(pair(X1,X2)) |
→ |
pair(X1,active(X2)) |
(17) |
active(snd(X)) |
→ |
snd(active(X)) |
(18) |
active(splitAt(X1,X2)) |
→ |
splitAt(active(X1),X2) |
(19) |
active(splitAt(X1,X2)) |
→ |
splitAt(X1,active(X2)) |
(20) |
active(u(X1,X2,X3,X4)) |
→ |
u(active(X1),X2,X3,X4) |
(21) |
active(head(X)) |
→ |
head(active(X)) |
(22) |
active(tail(X)) |
→ |
tail(active(X)) |
(23) |
active(sel(X1,X2)) |
→ |
sel(active(X1),X2) |
(24) |
active(sel(X1,X2)) |
→ |
sel(X1,active(X2)) |
(25) |
active(afterNth(X1,X2)) |
→ |
afterNth(active(X1),X2) |
(26) |
active(afterNth(X1,X2)) |
→ |
afterNth(X1,active(X2)) |
(27) |
active(take(X1,X2)) |
→ |
take(active(X1),X2) |
(28) |
active(take(X1,X2)) |
→ |
take(X1,active(X2)) |
(29) |
natsFrom(mark(X)) |
→ |
mark(natsFrom(X)) |
(30) |
cons(mark(X1),X2) |
→ |
mark(cons(X1,X2)) |
(31) |
s(mark(X)) |
→ |
mark(s(X)) |
(32) |
fst(mark(X)) |
→ |
mark(fst(X)) |
(33) |
pair(mark(X1),X2) |
→ |
mark(pair(X1,X2)) |
(34) |
pair(X1,mark(X2)) |
→ |
mark(pair(X1,X2)) |
(35) |
snd(mark(X)) |
→ |
mark(snd(X)) |
(36) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(37) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(38) |
u(mark(X1),X2,X3,X4) |
→ |
mark(u(X1,X2,X3,X4)) |
(39) |
head(mark(X)) |
→ |
mark(head(X)) |
(40) |
tail(mark(X)) |
→ |
mark(tail(X)) |
(41) |
sel(mark(X1),X2) |
→ |
mark(sel(X1,X2)) |
(42) |
sel(X1,mark(X2)) |
→ |
mark(sel(X1,X2)) |
(43) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(44) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(45) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(46) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(47) |
proper(natsFrom(X)) |
→ |
natsFrom(proper(X)) |
(48) |
proper(cons(X1,X2)) |
→ |
cons(proper(X1),proper(X2)) |
(49) |
proper(s(X)) |
→ |
s(proper(X)) |
(50) |
proper(fst(X)) |
→ |
fst(proper(X)) |
(51) |
proper(pair(X1,X2)) |
→ |
pair(proper(X1),proper(X2)) |
(52) |
proper(snd(X)) |
→ |
snd(proper(X)) |
(53) |
proper(splitAt(X1,X2)) |
→ |
splitAt(proper(X1),proper(X2)) |
(54) |
proper(0) |
→ |
ok(0) |
(55) |
proper(nil) |
→ |
ok(nil) |
(56) |
proper(u(X1,X2,X3,X4)) |
→ |
u(proper(X1),proper(X2),proper(X3),proper(X4)) |
(57) |
proper(head(X)) |
→ |
head(proper(X)) |
(58) |
proper(tail(X)) |
→ |
tail(proper(X)) |
(59) |
proper(sel(X1,X2)) |
→ |
sel(proper(X1),proper(X2)) |
(60) |
proper(afterNth(X1,X2)) |
→ |
afterNth(proper(X1),proper(X2)) |
(61) |
proper(take(X1,X2)) |
→ |
take(proper(X1),proper(X2)) |
(62) |
natsFrom(ok(X)) |
→ |
ok(natsFrom(X)) |
(63) |
cons(ok(X1),ok(X2)) |
→ |
ok(cons(X1,X2)) |
(64) |
s(ok(X)) |
→ |
ok(s(X)) |
(65) |
fst(ok(X)) |
→ |
ok(fst(X)) |
(66) |
pair(ok(X1),ok(X2)) |
→ |
ok(pair(X1,X2)) |
(67) |
snd(ok(X)) |
→ |
ok(snd(X)) |
(68) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(69) |
u(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(u(X1,X2,X3,X4)) |
(70) |
head(ok(X)) |
→ |
ok(head(X)) |
(71) |
tail(ok(X)) |
→ |
ok(tail(X)) |
(72) |
sel(ok(X1),ok(X2)) |
→ |
ok(sel(X1,X2)) |
(73) |
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(74) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(75) |
top(mark(X)) |
→ |
top(proper(X)) |
(76) |
top(ok(X)) |
→ |
top(active(X)) |
(77) |
There are 120 ruless (increase limit for explicit display).
The dependency pairs are split into 16
components.
-
The
1st
component contains the
pair
top#(ok(X)) |
→ |
top#(active(X)) |
(143) |
top#(mark(X)) |
→ |
top#(proper(X)) |
(163) |
1.1.1 Reduction Pair Processor with Usable Rules
Using the argument filter
π(cons#) |
= |
2 |
π(proper) |
= |
1 |
π(ok) |
= |
1 |
π(sel#) |
= |
2 |
π(afterNth#) |
= |
2 |
π(proper#) |
= |
1 |
π(active) |
= |
1 |
π(head) |
= |
1 |
π(snd#) |
= |
1 |
in combination with the following Weighted Path Order with the following precedence and status
prec(s) |
= |
4 |
|
status(s) |
= |
[1] |
|
list-extension(s) |
= |
Lex |
prec(take#) |
= |
0 |
|
status(take#) |
= |
[] |
|
list-extension(take#) |
= |
Lex |
prec(u) |
= |
6 |
|
status(u) |
= |
[3, 2, 4, 1] |
|
list-extension(u) |
= |
Lex |
prec(take) |
= |
3 |
|
status(take) |
= |
[1, 2] |
|
list-extension(take) |
= |
Lex |
prec(top) |
= |
0 |
|
status(top) |
= |
[] |
|
list-extension(top) |
= |
Lex |
prec(u#) |
= |
0 |
|
status(u#) |
= |
[4, 1] |
|
list-extension(u#) |
= |
Lex |
prec(pair) |
= |
4 |
|
status(pair) |
= |
[1, 2] |
|
list-extension(pair) |
= |
Lex |
prec(fst) |
= |
6 |
|
status(fst) |
= |
[1] |
|
list-extension(fst) |
= |
Lex |
prec(top#) |
= |
0 |
|
status(top#) |
= |
[1] |
|
list-extension(top#) |
= |
Lex |
prec(natsFrom) |
= |
4 |
|
status(natsFrom) |
= |
[1] |
|
list-extension(natsFrom) |
= |
Lex |
prec(head#) |
= |
0 |
|
status(head#) |
= |
[] |
|
list-extension(head#) |
= |
Lex |
prec(splitAt) |
= |
7 |
|
status(splitAt) |
= |
[1, 2] |
|
list-extension(splitAt) |
= |
Lex |
prec(fst#) |
= |
0 |
|
status(fst#) |
= |
[] |
|
list-extension(fst#) |
= |
Lex |
prec(tail) |
= |
2 |
|
status(tail) |
= |
[1] |
|
list-extension(tail) |
= |
Lex |
prec(0) |
= |
3 |
|
status(0) |
= |
[] |
|
list-extension(0) |
= |
Lex |
prec(sel) |
= |
1 |
|
status(sel) |
= |
[2, 1] |
|
list-extension(sel) |
= |
Lex |
prec(s#) |
= |
0 |
|
status(s#) |
= |
[] |
|
list-extension(s#) |
= |
Lex |
prec(afterNth) |
= |
3 |
|
status(afterNth) |
= |
[1, 2] |
|
list-extension(afterNth) |
= |
Lex |
prec(nil) |
= |
3 |
|
status(nil) |
= |
[] |
|
list-extension(nil) |
= |
Lex |
prec(tail#) |
= |
0 |
|
status(tail#) |
= |
[] |
|
list-extension(tail#) |
= |
Lex |
prec(splitAt#) |
= |
0 |
|
status(splitAt#) |
= |
[] |
|
list-extension(splitAt#) |
= |
Lex |
prec(mark) |
= |
0 |
|
status(mark) |
= |
[1] |
|
list-extension(mark) |
= |
Lex |
prec(cons) |
= |
2 |
|
status(cons) |
= |
[1] |
|
list-extension(cons) |
= |
Lex |
prec(natsFrom#) |
= |
0 |
|
status(natsFrom#) |
= |
[] |
|
list-extension(natsFrom#) |
= |
Lex |
prec(active#) |
= |
0 |
|
status(active#) |
= |
[] |
|
list-extension(active#) |
= |
Lex |
prec(snd) |
= |
4 |
|
status(snd) |
= |
[1] |
|
list-extension(snd) |
= |
Lex |
prec(pair#) |
= |
0 |
|
status(pair#) |
= |
[1, 2] |
|
list-extension(pair#) |
= |
Lex |
and the following
Max-polynomial interpretation
[s(x1)] |
=
|
x1 + 0 |
[take#(x1, x2)] |
=
|
x2 + 1 |
[u(x1,...,x4)] |
=
|
max(x1 + 0, x2 + 16674, x3 + 33354, x4 + 0, 0) |
[take(x1, x2)] |
=
|
x1 + x2 + 36534 |
[top(x1)] |
=
|
1 |
[u#(x1,...,x4)] |
=
|
max(x1 + 1, x2 + 1, x4 + 1, 0) |
[pair(x1, x2)] |
=
|
max(x1 + 16675, x2 + 16676, 0) |
[fst(x1)] |
=
|
x1 + 19856 |
[top#(x1)] |
=
|
x1 + 1 |
[natsFrom(x1)] |
=
|
x1 + 31939 |
[head#(x1)] |
=
|
1 |
[splitAt(x1, x2)] |
=
|
x1 + x2 + 16677 |
[fst#(x1)] |
=
|
1 |
[tail(x1)] |
=
|
x1 + 15943 |
[0] |
=
|
1 |
[sel(x1, x2)] |
=
|
x1 + x2 + 72926 |
[s#(x1)] |
=
|
1 |
[afterNth(x1, x2)] |
=
|
x1 + x2 + 72925 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
1 |
[splitAt#(x1, x2)] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 0 |
[cons(x1, x2)] |
=
|
max(x1 + 16678, x2 + 0, 0) |
[natsFrom#(x1)] |
=
|
1 |
[active#(x1)] |
=
|
1 |
[snd(x1)] |
=
|
x1 + 28872 |
[pair#(x1, x2)] |
=
|
max(x1 + 1, x2 + 1, 0) |
together with the usable
rules
active(snd(X)) |
→ |
snd(active(X)) |
(18) |
proper(s(X)) |
→ |
s(proper(X)) |
(50) |
active(splitAt(0,XS)) |
→ |
mark(pair(nil,XS)) |
(4) |
active(fst(X)) |
→ |
fst(active(X)) |
(15) |
active(tail(cons(N,XS))) |
→ |
mark(XS) |
(8) |
proper(splitAt(X1,X2)) |
→ |
splitAt(proper(X1),proper(X2)) |
(54) |
active(natsFrom(N)) |
→ |
mark(cons(N,natsFrom(s(N)))) |
(1) |
active(snd(pair(XS,YS))) |
→ |
mark(YS) |
(3) |
active(pair(X1,X2)) |
→ |
pair(active(X1),X2) |
(16) |
active(u(X1,X2,X3,X4)) |
→ |
u(active(X1),X2,X3,X4) |
(21) |
snd(mark(X)) |
→ |
mark(snd(X)) |
(36) |
snd(ok(X)) |
→ |
ok(snd(X)) |
(68) |
active(afterNth(X1,X2)) |
→ |
afterNth(active(X1),X2) |
(26) |
natsFrom(ok(X)) |
→ |
ok(natsFrom(X)) |
(63) |
active(splitAt(X1,X2)) |
→ |
splitAt(active(X1),X2) |
(19) |
s(mark(X)) |
→ |
mark(s(X)) |
(32) |
active(pair(X1,X2)) |
→ |
pair(X1,active(X2)) |
(17) |
proper(sel(X1,X2)) |
→ |
sel(proper(X1),proper(X2)) |
(60) |
active(afterNth(X1,X2)) |
→ |
afterNth(X1,active(X2)) |
(27) |
pair(mark(X1),X2) |
→ |
mark(pair(X1,X2)) |
(34) |
active(head(X)) |
→ |
head(active(X)) |
(22) |
active(take(X1,X2)) |
→ |
take(active(X1),X2) |
(28) |
s(ok(X)) |
→ |
ok(s(X)) |
(65) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(44) |
active(splitAt(s(N),cons(X,XS))) |
→ |
mark(u(splitAt(N,XS),N,X,XS)) |
(5) |
tail(ok(X)) |
→ |
ok(tail(X)) |
(72) |
fst(mark(X)) |
→ |
mark(fst(X)) |
(33) |
cons(ok(X1),ok(X2)) |
→ |
ok(cons(X1,X2)) |
(64) |
active(take(N,XS)) |
→ |
mark(fst(splitAt(N,XS))) |
(10) |
u(mark(X1),X2,X3,X4) |
→ |
mark(u(X1,X2,X3,X4)) |
(39) |
active(head(cons(N,XS))) |
→ |
mark(N) |
(7) |
active(splitAt(X1,X2)) |
→ |
splitAt(X1,active(X2)) |
(20) |
active(sel(X1,X2)) |
→ |
sel(X1,active(X2)) |
(25) |
proper(cons(X1,X2)) |
→ |
cons(proper(X1),proper(X2)) |
(49) |
proper(pair(X1,X2)) |
→ |
pair(proper(X1),proper(X2)) |
(52) |
natsFrom(mark(X)) |
→ |
mark(natsFrom(X)) |
(30) |
proper(take(X1,X2)) |
→ |
take(proper(X1),proper(X2)) |
(62) |
active(s(X)) |
→ |
s(active(X)) |
(14) |
proper(nil) |
→ |
ok(nil) |
(56) |
cons(mark(X1),X2) |
→ |
mark(cons(X1,X2)) |
(31) |
active(natsFrom(X)) |
→ |
natsFrom(active(X)) |
(12) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(69) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(45) |
active(tail(X)) |
→ |
tail(active(X)) |
(23) |
u(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(u(X1,X2,X3,X4)) |
(70) |
active(sel(X1,X2)) |
→ |
sel(active(X1),X2) |
(24) |
proper(u(X1,X2,X3,X4)) |
→ |
u(proper(X1),proper(X2),proper(X3),proper(X4)) |
(57) |
active(afterNth(N,XS)) |
→ |
mark(snd(splitAt(N,XS))) |
(11) |
active(sel(N,XS)) |
→ |
mark(head(afterNth(N,XS))) |
(9) |
active(cons(X1,X2)) |
→ |
cons(active(X1),X2) |
(13) |
proper(fst(X)) |
→ |
fst(proper(X)) |
(51) |
head(mark(X)) |
→ |
mark(head(X)) |
(40) |
pair(ok(X1),ok(X2)) |
→ |
ok(pair(X1,X2)) |
(67) |
proper(0) |
→ |
ok(0) |
(55) |
proper(tail(X)) |
→ |
tail(proper(X)) |
(59) |
active(u(pair(YS,ZS),N,X,XS)) |
→ |
mark(pair(cons(X,YS),ZS)) |
(6) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(38) |
proper(afterNth(X1,X2)) |
→ |
afterNth(proper(X1),proper(X2)) |
(61) |
proper(head(X)) |
→ |
head(proper(X)) |
(58) |
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(74) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(75) |
proper(natsFrom(X)) |
→ |
natsFrom(proper(X)) |
(48) |
head(ok(X)) |
→ |
ok(head(X)) |
(71) |
proper(snd(X)) |
→ |
snd(proper(X)) |
(53) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(47) |
sel(ok(X1),ok(X2)) |
→ |
ok(sel(X1,X2)) |
(73) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(37) |
tail(mark(X)) |
→ |
mark(tail(X)) |
(41) |
sel(mark(X1),X2) |
→ |
mark(sel(X1,X2)) |
(42) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(46) |
fst(ok(X)) |
→ |
ok(fst(X)) |
(66) |
pair(X1,mark(X2)) |
→ |
mark(pair(X1,X2)) |
(35) |
active(take(X1,X2)) |
→ |
take(X1,active(X2)) |
(29) |
sel(X1,mark(X2)) |
→ |
mark(sel(X1,X2)) |
(43) |
active(fst(pair(XS,YS))) |
→ |
mark(XS) |
(2) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
top#(mark(X)) |
→ |
top#(proper(X)) |
(163) |
could be deleted.
1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
2nd
component contains the
pair
active#(tail(X)) |
→ |
active#(X) |
(196) |
active#(u(X1,X2,X3,X4)) |
→ |
active#(X1) |
(192) |
active#(sel(X1,X2)) |
→ |
active#(X2) |
(133) |
active#(splitAt(X1,X2)) |
→ |
active#(X1) |
(132) |
active#(natsFrom(X)) |
→ |
active#(X) |
(188) |
active#(take(X1,X2)) |
→ |
active#(X2) |
(185) |
active#(s(X)) |
→ |
active#(X) |
(121) |
active#(head(X)) |
→ |
active#(X) |
(180) |
active#(pair(X1,X2)) |
→ |
active#(X1) |
(177) |
active#(cons(X1,X2)) |
→ |
active#(X1) |
(167) |
active#(splitAt(X1,X2)) |
→ |
active#(X2) |
(98) |
active#(sel(X1,X2)) |
→ |
active#(X1) |
(96) |
active#(snd(X)) |
→ |
active#(X) |
(161) |
active#(afterNth(X1,X2)) |
→ |
active#(X1) |
(92) |
active#(pair(X1,X2)) |
→ |
active#(X2) |
(157) |
active#(fst(X)) |
→ |
active#(X) |
(87) |
active#(take(X1,X2)) |
→ |
active#(X1) |
(83) |
active#(afterNth(X1,X2)) |
→ |
active#(X2) |
(151) |
1.1.2 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
x1 + x3 + 1 |
[take(x1, x2)] |
=
|
x1 + x2 + 1 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst(x1)] |
=
|
x1 + 1 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
x1 + 32002 |
[proper(x1)] |
=
|
x1 + 5928 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
x1 + x2 + 30215 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
x1 + x2 + 1 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 0 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
3 |
[head(x1)] |
=
|
x1 + 1 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
x1 + 0 |
[snd(x1)] |
=
|
x1 + 1 |
[pair#(x1, x2)] |
=
|
0 |
together with the usable
rules
snd(mark(X)) |
→ |
mark(snd(X)) |
(36) |
snd(ok(X)) |
→ |
ok(snd(X)) |
(68) |
natsFrom(ok(X)) |
→ |
ok(natsFrom(X)) |
(63) |
s(mark(X)) |
→ |
mark(s(X)) |
(32) |
pair(mark(X1),X2) |
→ |
mark(pair(X1,X2)) |
(34) |
s(ok(X)) |
→ |
ok(s(X)) |
(65) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(44) |
tail(ok(X)) |
→ |
ok(tail(X)) |
(72) |
fst(mark(X)) |
→ |
mark(fst(X)) |
(33) |
cons(ok(X1),ok(X2)) |
→ |
ok(cons(X1,X2)) |
(64) |
u(mark(X1),X2,X3,X4) |
→ |
mark(u(X1,X2,X3,X4)) |
(39) |
natsFrom(mark(X)) |
→ |
mark(natsFrom(X)) |
(30) |
proper(nil) |
→ |
ok(nil) |
(56) |
cons(mark(X1),X2) |
→ |
mark(cons(X1,X2)) |
(31) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(69) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(45) |
u(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(u(X1,X2,X3,X4)) |
(70) |
head(mark(X)) |
→ |
mark(head(X)) |
(40) |
pair(ok(X1),ok(X2)) |
→ |
ok(pair(X1,X2)) |
(67) |
proper(0) |
→ |
ok(0) |
(55) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(38) |
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(74) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(75) |
head(ok(X)) |
→ |
ok(head(X)) |
(71) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(47) |
sel(ok(X1),ok(X2)) |
→ |
ok(sel(X1,X2)) |
(73) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(37) |
tail(mark(X)) |
→ |
mark(tail(X)) |
(41) |
sel(mark(X1),X2) |
→ |
mark(sel(X1,X2)) |
(42) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(46) |
fst(ok(X)) |
→ |
ok(fst(X)) |
(66) |
pair(X1,mark(X2)) |
→ |
mark(pair(X1,X2)) |
(35) |
sel(X1,mark(X2)) |
→ |
mark(sel(X1,X2)) |
(43) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
active#(tail(X)) |
→ |
active#(X) |
(196) |
active#(u(X1,X2,X3,X4)) |
→ |
active#(X1) |
(192) |
active#(sel(X1,X2)) |
→ |
active#(X2) |
(133) |
active#(splitAt(X1,X2)) |
→ |
active#(X1) |
(132) |
active#(natsFrom(X)) |
→ |
active#(X) |
(188) |
active#(take(X1,X2)) |
→ |
active#(X2) |
(185) |
active#(s(X)) |
→ |
active#(X) |
(121) |
active#(head(X)) |
→ |
active#(X) |
(180) |
active#(pair(X1,X2)) |
→ |
active#(X1) |
(177) |
active#(cons(X1,X2)) |
→ |
active#(X1) |
(167) |
active#(splitAt(X1,X2)) |
→ |
active#(X2) |
(98) |
active#(sel(X1,X2)) |
→ |
active#(X1) |
(96) |
active#(snd(X)) |
→ |
active#(X) |
(161) |
active#(afterNth(X1,X2)) |
→ |
active#(X1) |
(92) |
active#(pair(X1,X2)) |
→ |
active#(X2) |
(157) |
active#(fst(X)) |
→ |
active#(X) |
(87) |
active#(take(X1,X2)) |
→ |
active#(X1) |
(83) |
active#(afterNth(X1,X2)) |
→ |
active#(X2) |
(151) |
could be deleted.
1.1.2.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
3rd
component contains the
pair
proper#(s(X)) |
→ |
proper#(X) |
(129) |
proper#(afterNth(X1,X2)) |
→ |
proper#(X2) |
(127) |
proper#(natsFrom(X)) |
→ |
proper#(X) |
(184) |
proper#(snd(X)) |
→ |
proper#(X) |
(117) |
proper#(pair(X1,X2)) |
→ |
proper#(X1) |
(176) |
proper#(fst(X)) |
→ |
proper#(X) |
(174) |
proper#(sel(X1,X2)) |
→ |
proper#(X1) |
(114) |
proper#(u(X1,X2,X3,X4)) |
→ |
proper#(X1) |
(113) |
proper#(cons(X1,X2)) |
→ |
proper#(X2) |
(112) |
proper#(take(X1,X2)) |
→ |
proper#(X2) |
(171) |
proper#(take(X1,X2)) |
→ |
proper#(X1) |
(109) |
proper#(splitAt(X1,X2)) |
→ |
proper#(X2) |
(104) |
proper#(splitAt(X1,X2)) |
→ |
proper#(X1) |
(101) |
proper#(afterNth(X1,X2)) |
→ |
proper#(X1) |
(166) |
proper#(tail(X)) |
→ |
proper#(X) |
(165) |
proper#(sel(X1,X2)) |
→ |
proper#(X2) |
(94) |
proper#(pair(X1,X2)) |
→ |
proper#(X2) |
(158) |
proper#(u(X1,X2,X3,X4)) |
→ |
proper#(X2) |
(89) |
proper#(u(X1,X2,X3,X4)) |
→ |
proper#(X3) |
(86) |
proper#(cons(X1,X2)) |
→ |
proper#(X1) |
(84) |
proper#(u(X1,X2,X3,X4)) |
→ |
proper#(X4) |
(80) |
proper#(head(X)) |
→ |
proper#(X) |
(150) |
1.1.3 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
x1 + x2 + x3 + x4 + 1 |
[take(x1, x2)] |
=
|
x1 + x2 + 1 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst(x1)] |
=
|
x1 + 1 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
x1 + 1 |
[proper(x1)] |
=
|
x1 + 1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
x1 + x2 + 1 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
x1 + x2 + 1 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 0 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
x1 + 0 |
[active(x1)] |
=
|
3 |
[head(x1)] |
=
|
x1 + 1 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
x1 + 1 |
[pair#(x1, x2)] |
=
|
0 |
together with the usable
rules
snd(mark(X)) |
→ |
mark(snd(X)) |
(36) |
snd(ok(X)) |
→ |
ok(snd(X)) |
(68) |
natsFrom(ok(X)) |
→ |
ok(natsFrom(X)) |
(63) |
s(mark(X)) |
→ |
mark(s(X)) |
(32) |
pair(mark(X1),X2) |
→ |
mark(pair(X1,X2)) |
(34) |
s(ok(X)) |
→ |
ok(s(X)) |
(65) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(44) |
tail(ok(X)) |
→ |
ok(tail(X)) |
(72) |
fst(mark(X)) |
→ |
mark(fst(X)) |
(33) |
cons(ok(X1),ok(X2)) |
→ |
ok(cons(X1,X2)) |
(64) |
u(mark(X1),X2,X3,X4) |
→ |
mark(u(X1,X2,X3,X4)) |
(39) |
natsFrom(mark(X)) |
→ |
mark(natsFrom(X)) |
(30) |
proper(nil) |
→ |
ok(nil) |
(56) |
cons(mark(X1),X2) |
→ |
mark(cons(X1,X2)) |
(31) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(69) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(45) |
u(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(u(X1,X2,X3,X4)) |
(70) |
head(mark(X)) |
→ |
mark(head(X)) |
(40) |
pair(ok(X1),ok(X2)) |
→ |
ok(pair(X1,X2)) |
(67) |
proper(0) |
→ |
ok(0) |
(55) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(38) |
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(74) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(75) |
head(ok(X)) |
→ |
ok(head(X)) |
(71) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(47) |
sel(ok(X1),ok(X2)) |
→ |
ok(sel(X1,X2)) |
(73) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(37) |
tail(mark(X)) |
→ |
mark(tail(X)) |
(41) |
sel(mark(X1),X2) |
→ |
mark(sel(X1,X2)) |
(42) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(46) |
fst(ok(X)) |
→ |
ok(fst(X)) |
(66) |
pair(X1,mark(X2)) |
→ |
mark(pair(X1,X2)) |
(35) |
sel(X1,mark(X2)) |
→ |
mark(sel(X1,X2)) |
(43) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
proper#(s(X)) |
→ |
proper#(X) |
(129) |
proper#(afterNth(X1,X2)) |
→ |
proper#(X2) |
(127) |
proper#(natsFrom(X)) |
→ |
proper#(X) |
(184) |
proper#(snd(X)) |
→ |
proper#(X) |
(117) |
proper#(pair(X1,X2)) |
→ |
proper#(X1) |
(176) |
proper#(fst(X)) |
→ |
proper#(X) |
(174) |
proper#(sel(X1,X2)) |
→ |
proper#(X1) |
(114) |
proper#(u(X1,X2,X3,X4)) |
→ |
proper#(X1) |
(113) |
proper#(cons(X1,X2)) |
→ |
proper#(X2) |
(112) |
proper#(take(X1,X2)) |
→ |
proper#(X2) |
(171) |
proper#(take(X1,X2)) |
→ |
proper#(X1) |
(109) |
proper#(splitAt(X1,X2)) |
→ |
proper#(X2) |
(104) |
proper#(splitAt(X1,X2)) |
→ |
proper#(X1) |
(101) |
proper#(afterNth(X1,X2)) |
→ |
proper#(X1) |
(166) |
proper#(tail(X)) |
→ |
proper#(X) |
(165) |
proper#(sel(X1,X2)) |
→ |
proper#(X2) |
(94) |
proper#(pair(X1,X2)) |
→ |
proper#(X2) |
(158) |
proper#(u(X1,X2,X3,X4)) |
→ |
proper#(X2) |
(89) |
proper#(u(X1,X2,X3,X4)) |
→ |
proper#(X3) |
(86) |
proper#(cons(X1,X2)) |
→ |
proper#(X1) |
(84) |
proper#(u(X1,X2,X3,X4)) |
→ |
proper#(X4) |
(80) |
proper#(head(X)) |
→ |
proper#(X) |
(150) |
could be deleted.
1.1.3.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
4th
component contains the
pair
snd#(mark(X)) |
→ |
snd#(X) |
(134) |
snd#(ok(X)) |
→ |
snd#(X) |
(179) |
1.1.4 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
x1 + x2 + x3 + x4 + 1 |
[take(x1, x2)] |
=
|
x1 + x2 + 1 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst(x1)] |
=
|
x1 + 2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
x1 + 32613 |
[proper(x1)] |
=
|
x1 + 1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
x1 + x2 + 10392 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
x1 + x2 + 1 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 0 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
3 |
[head(x1)] |
=
|
x1 + 2 |
[snd#(x1)] |
=
|
x1 + 0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
x1 + 1 |
[pair#(x1, x2)] |
=
|
0 |
together with the usable
rules
snd(mark(X)) |
→ |
mark(snd(X)) |
(36) |
snd(ok(X)) |
→ |
ok(snd(X)) |
(68) |
natsFrom(ok(X)) |
→ |
ok(natsFrom(X)) |
(63) |
s(mark(X)) |
→ |
mark(s(X)) |
(32) |
pair(mark(X1),X2) |
→ |
mark(pair(X1,X2)) |
(34) |
s(ok(X)) |
→ |
ok(s(X)) |
(65) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(44) |
tail(ok(X)) |
→ |
ok(tail(X)) |
(72) |
fst(mark(X)) |
→ |
mark(fst(X)) |
(33) |
cons(ok(X1),ok(X2)) |
→ |
ok(cons(X1,X2)) |
(64) |
u(mark(X1),X2,X3,X4) |
→ |
mark(u(X1,X2,X3,X4)) |
(39) |
natsFrom(mark(X)) |
→ |
mark(natsFrom(X)) |
(30) |
proper(nil) |
→ |
ok(nil) |
(56) |
cons(mark(X1),X2) |
→ |
mark(cons(X1,X2)) |
(31) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(69) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(45) |
u(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(u(X1,X2,X3,X4)) |
(70) |
head(mark(X)) |
→ |
mark(head(X)) |
(40) |
pair(ok(X1),ok(X2)) |
→ |
ok(pair(X1,X2)) |
(67) |
proper(0) |
→ |
ok(0) |
(55) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(38) |
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(74) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(75) |
head(ok(X)) |
→ |
ok(head(X)) |
(71) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(47) |
sel(ok(X1),ok(X2)) |
→ |
ok(sel(X1,X2)) |
(73) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(37) |
tail(mark(X)) |
→ |
mark(tail(X)) |
(41) |
sel(mark(X1),X2) |
→ |
mark(sel(X1,X2)) |
(42) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(46) |
fst(ok(X)) |
→ |
ok(fst(X)) |
(66) |
pair(X1,mark(X2)) |
→ |
mark(pair(X1,X2)) |
(35) |
sel(X1,mark(X2)) |
→ |
mark(sel(X1,X2)) |
(43) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
snd#(ok(X)) |
→ |
snd#(X) |
(179) |
could be deleted.
1.1.4.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
5th
component contains the
pair
natsFrom#(mark(X)) |
→ |
natsFrom#(X) |
(105) |
natsFrom#(ok(X)) |
→ |
natsFrom#(X) |
(93) |
1.1.5 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
x1 + x2 + x3 + x4 + 1 |
[take(x1, x2)] |
=
|
x1 + x2 + 28312 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst(x1)] |
=
|
x1 + 1 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
x1 + 31682 |
[proper(x1)] |
=
|
x1 + 1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
x1 + x2 + 1 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
x1 + x2 + 1 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 1 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
4 |
[head(x1)] |
=
|
x1 + 1 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
x1 + 0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
x1 + 1 |
[pair#(x1, x2)] |
=
|
0 |
together with the usable
rules
snd(mark(X)) |
→ |
mark(snd(X)) |
(36) |
snd(ok(X)) |
→ |
ok(snd(X)) |
(68) |
natsFrom(ok(X)) |
→ |
ok(natsFrom(X)) |
(63) |
s(mark(X)) |
→ |
mark(s(X)) |
(32) |
pair(mark(X1),X2) |
→ |
mark(pair(X1,X2)) |
(34) |
s(ok(X)) |
→ |
ok(s(X)) |
(65) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(44) |
tail(ok(X)) |
→ |
ok(tail(X)) |
(72) |
fst(mark(X)) |
→ |
mark(fst(X)) |
(33) |
cons(ok(X1),ok(X2)) |
→ |
ok(cons(X1,X2)) |
(64) |
u(mark(X1),X2,X3,X4) |
→ |
mark(u(X1,X2,X3,X4)) |
(39) |
natsFrom(mark(X)) |
→ |
mark(natsFrom(X)) |
(30) |
proper(nil) |
→ |
ok(nil) |
(56) |
cons(mark(X1),X2) |
→ |
mark(cons(X1,X2)) |
(31) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(69) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(45) |
u(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(u(X1,X2,X3,X4)) |
(70) |
head(mark(X)) |
→ |
mark(head(X)) |
(40) |
pair(ok(X1),ok(X2)) |
→ |
ok(pair(X1,X2)) |
(67) |
proper(0) |
→ |
ok(0) |
(55) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(38) |
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(74) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(75) |
head(ok(X)) |
→ |
ok(head(X)) |
(71) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(47) |
sel(ok(X1),ok(X2)) |
→ |
ok(sel(X1,X2)) |
(73) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(37) |
tail(mark(X)) |
→ |
mark(tail(X)) |
(41) |
sel(mark(X1),X2) |
→ |
mark(sel(X1,X2)) |
(42) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(46) |
fst(ok(X)) |
→ |
ok(fst(X)) |
(66) |
pair(X1,mark(X2)) |
→ |
mark(pair(X1,X2)) |
(35) |
sel(X1,mark(X2)) |
→ |
mark(sel(X1,X2)) |
(43) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
natsFrom#(mark(X)) |
→ |
natsFrom#(X) |
(105) |
natsFrom#(ok(X)) |
→ |
natsFrom#(X) |
(93) |
could be deleted.
1.1.5.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
6th
component contains the
pair
head#(mark(X)) |
→ |
head#(X) |
(145) |
head#(ok(X)) |
→ |
head#(X) |
(142) |
1.1.6 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
x1 + x2 + x3 + x4 + 2 |
[take(x1, x2)] |
=
|
x1 + x2 + 1 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
x1 + x2 + 2 |
[fst(x1)] |
=
|
x1 + 1 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
x1 + 0 |
[splitAt(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
x1 + 32299 |
[proper(x1)] |
=
|
x1 + 1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
29764 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
x1 + x2 + 1 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
x1 + x2 + 1 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 1 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
4 |
[head(x1)] |
=
|
x1 + 1 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
x1 + 1 |
[pair#(x1, x2)] |
=
|
0 |
together with the usable
rules
snd(mark(X)) |
→ |
mark(snd(X)) |
(36) |
snd(ok(X)) |
→ |
ok(snd(X)) |
(68) |
natsFrom(ok(X)) |
→ |
ok(natsFrom(X)) |
(63) |
s(mark(X)) |
→ |
mark(s(X)) |
(32) |
pair(mark(X1),X2) |
→ |
mark(pair(X1,X2)) |
(34) |
s(ok(X)) |
→ |
ok(s(X)) |
(65) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(44) |
tail(ok(X)) |
→ |
ok(tail(X)) |
(72) |
fst(mark(X)) |
→ |
mark(fst(X)) |
(33) |
cons(ok(X1),ok(X2)) |
→ |
ok(cons(X1,X2)) |
(64) |
u(mark(X1),X2,X3,X4) |
→ |
mark(u(X1,X2,X3,X4)) |
(39) |
natsFrom(mark(X)) |
→ |
mark(natsFrom(X)) |
(30) |
proper(nil) |
→ |
ok(nil) |
(56) |
cons(mark(X1),X2) |
→ |
mark(cons(X1,X2)) |
(31) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(69) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(45) |
u(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(u(X1,X2,X3,X4)) |
(70) |
head(mark(X)) |
→ |
mark(head(X)) |
(40) |
pair(ok(X1),ok(X2)) |
→ |
ok(pair(X1,X2)) |
(67) |
proper(0) |
→ |
ok(0) |
(55) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(38) |
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(74) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(75) |
head(ok(X)) |
→ |
ok(head(X)) |
(71) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(47) |
sel(ok(X1),ok(X2)) |
→ |
ok(sel(X1,X2)) |
(73) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(37) |
tail(mark(X)) |
→ |
mark(tail(X)) |
(41) |
sel(mark(X1),X2) |
→ |
mark(sel(X1,X2)) |
(42) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(46) |
fst(ok(X)) |
→ |
ok(fst(X)) |
(66) |
pair(X1,mark(X2)) |
→ |
mark(pair(X1,X2)) |
(35) |
sel(X1,mark(X2)) |
→ |
mark(sel(X1,X2)) |
(43) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
head#(mark(X)) |
→ |
head#(X) |
(145) |
head#(ok(X)) |
→ |
head#(X) |
(142) |
could be deleted.
1.1.6.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
7th
component contains the
pair
afterNth#(ok(X1),ok(X2)) |
→ |
afterNth#(X1,X2) |
(197) |
afterNth#(mark(X1),X2) |
→ |
afterNth#(X1,X2) |
(195) |
afterNth#(X1,mark(X2)) |
→ |
afterNth#(X1,X2) |
(116) |
1.1.7 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
26389 |
[take(x1, x2)] |
=
|
x2 + 5553 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
8094 |
[fst(x1)] |
=
|
8518 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
23540 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
x1 + 21293 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
1316 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 3 |
[0] |
=
|
16393 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
5610 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
21952 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
x1 + x2 + 0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
26405 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 3342 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
8753 |
[pair#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
afterNth#(ok(X1),ok(X2)) |
→ |
afterNth#(X1,X2) |
(197) |
afterNth#(mark(X1),X2) |
→ |
afterNth#(X1,X2) |
(195) |
afterNth#(X1,mark(X2)) |
→ |
afterNth#(X1,X2) |
(116) |
could be deleted.
1.1.7.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
8th
component contains the
pair
tail#(mark(X)) |
→ |
tail#(X) |
(189) |
tail#(ok(X)) |
→ |
tail#(X) |
(186) |
1.1.8 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
14044 |
[take(x1, x2)] |
=
|
593 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
22297 |
[fst(x1)] |
=
|
3902 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
28550 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
21294 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
28661 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
6275 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
21952 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
x1 + 0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
14397 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
2062 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
23049 |
[pair#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
tail#(mark(X)) |
→ |
tail#(X) |
(189) |
tail#(ok(X)) |
→ |
tail#(X) |
(186) |
could be deleted.
1.1.8.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
9th
component contains the
pair
fst#(mark(X)) |
→ |
fst#(X) |
(122) |
fst#(ok(X)) |
→ |
fst#(X) |
(162) |
1.1.9 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
12064 |
[take(x1, x2)] |
=
|
593 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
3751 |
[fst(x1)] |
=
|
19213 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
32601 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
30384 |
[fst#(x1)] |
=
|
x1 + 0 |
[tail(x1)] |
=
|
8683 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
17066 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
21952 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
13964 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
24635 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
31772 |
[pair#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
fst#(mark(X)) |
→ |
fst#(X) |
(122) |
fst#(ok(X)) |
→ |
fst#(X) |
(162) |
could be deleted.
1.1.9.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
10th
component contains the
pair
u#(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
u#(X1,X2,X3,X4) |
(99) |
u#(mark(X1),X2,X3,X4) |
→ |
u#(X1,X2,X3,X4) |
(160) |
1.1.10 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
8922 |
[take(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
x1 + x2 + 0 |
[pair(x1, x2)] |
=
|
2 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
12268 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
29572 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
2 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
23622 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
21952 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
27531 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
29829 |
[pair#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
u#(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
u#(X1,X2,X3,X4) |
(99) |
u#(mark(X1),X2,X3,X4) |
→ |
u#(X1,X2,X3,X4) |
(160) |
could be deleted.
1.1.10.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
11th
component contains the
pair
take#(X1,mark(X2)) |
→ |
take#(X1,X2) |
(119) |
take#(ok(X1),ok(X2)) |
→ |
take#(X1,X2) |
(173) |
take#(mark(X1),X2) |
→ |
take#(X1,X2) |
(108) |
1.1.11 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
x1 + 0 |
[u(x1,...,x4)] |
=
|
3289 |
[take(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
2 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
21541 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
13021 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
2 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
12820 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
21952 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
27531 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
29899 |
[pair#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
take#(ok(X1),ok(X2)) |
→ |
take#(X1,X2) |
(173) |
take#(mark(X1),X2) |
→ |
take#(X1,X2) |
(108) |
could be deleted.
1.1.11.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
12th
component contains the
pair
pair#(X1,mark(X2)) |
→ |
pair#(X1,X2) |
(193) |
pair#(ok(X1),ok(X2)) |
→ |
pair#(X1,X2) |
(81) |
pair#(mark(X1),X2) |
→ |
pair#(X1,X2) |
(79) |
1.1.12 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
2 |
[take(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
2 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
23724 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
2 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
2 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
12770 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
21952 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
2 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
29351 |
[pair#(x1, x2)] |
=
|
x1 + x2 + 0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
pair#(X1,mark(X2)) |
→ |
pair#(X1,X2) |
(193) |
pair#(ok(X1),ok(X2)) |
→ |
pair#(X1,X2) |
(81) |
pair#(mark(X1),X2) |
→ |
pair#(X1,X2) |
(79) |
could be deleted.
1.1.12.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
13th
component contains the
pair
cons#(mark(X1),X2) |
→ |
cons#(X1,X2) |
(111) |
cons#(ok(X1),ok(X2)) |
→ |
cons#(X1,X2) |
(100) |
1.1.13 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
x2 + 0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
879 |
[take(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
13421 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
6754 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
21796 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
2 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
29999 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
1464 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
2 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
7915 |
[pair#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
cons#(ok(X1),ok(X2)) |
→ |
cons#(X1,X2) |
(100) |
could be deleted.
1.1.13.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
14th
component contains the
pair
sel#(X1,mark(X2)) |
→ |
sel#(X1,X2) |
(187) |
sel#(ok(X1),ok(X2)) |
→ |
sel#(X1,X2) |
(154) |
sel#(mark(X1),X2) |
→ |
sel#(X1,X2) |
(152) |
1.1.14 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
2 |
[take(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
2 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
27668 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
21796 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
2 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
3 |
[sel#(x1, x2)] |
=
|
x1 + 0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
2 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
2 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
2 |
[pair#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
sel#(ok(X1),ok(X2)) |
→ |
sel#(X1,X2) |
(154) |
sel#(mark(X1),X2) |
→ |
sel#(X1,X2) |
(152) |
could be deleted.
1.1.14.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
15th
component contains the
pair
splitAt#(ok(X1),ok(X2)) |
→ |
splitAt#(X1,X2) |
(146) |
splitAt#(X1,mark(X2)) |
→ |
splitAt#(X1,X2) |
(125) |
splitAt#(mark(X1),X2) |
→ |
splitAt#(X1,X2) |
(118) |
1.1.15 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
2 |
[take(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
2 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
24328 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
21796 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
2 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
2953 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
2 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
x1 + 0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
2 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
2 |
[pair#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
splitAt#(ok(X1),ok(X2)) |
→ |
splitAt#(X1,X2) |
(146) |
splitAt#(mark(X1),X2) |
→ |
splitAt#(X1,X2) |
(118) |
could be deleted.
1.1.15.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
16th
component contains the
pair
s#(ok(X)) |
→ |
s#(X) |
(128) |
s#(mark(X)) |
→ |
s#(X) |
(124) |
1.1.16 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
2 |
[take#(x1, x2)] |
=
|
0 |
[u(x1,...,x4)] |
=
|
16517 |
[take(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[u#(x1,...,x4)] |
=
|
0 |
[pair(x1, x2)] |
=
|
14259 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
21654 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
x2 + 32662 |
[fst#(x1)] |
=
|
0 |
[tail(x1)] |
=
|
2 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 5328 |
[0] |
=
|
26694 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
31223 |
[s#(x1)] |
=
|
x1 + 0 |
[afterNth(x1, x2)] |
=
|
29849 |
[nil] |
=
|
2558 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4686 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
31061 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
2 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
18839 |
[pair#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
s#(ok(X)) |
→ |
s#(X) |
(128) |
s#(mark(X)) |
→ |
s#(X) |
(124) |
could be deleted.
1.1.16.1 Dependency Graph Processor
The dependency pairs are split into 0
components.