The rewrite relation of the following TRS is considered.
active(U11(tt,N,X,XS)) |
→ |
mark(U12(splitAt(N,XS),X)) |
(1) |
active(U12(pair(YS,ZS),X)) |
→ |
mark(pair(cons(X,YS),ZS)) |
(2) |
active(afterNth(N,XS)) |
→ |
mark(snd(splitAt(N,XS))) |
(3) |
active(and(tt,X)) |
→ |
mark(X) |
(4) |
active(fst(pair(X,Y))) |
→ |
mark(X) |
(5) |
active(head(cons(N,XS))) |
→ |
mark(N) |
(6) |
active(natsFrom(N)) |
→ |
mark(cons(N,natsFrom(s(N)))) |
(7) |
active(sel(N,XS)) |
→ |
mark(head(afterNth(N,XS))) |
(8) |
active(snd(pair(X,Y))) |
→ |
mark(Y) |
(9) |
active(splitAt(0,XS)) |
→ |
mark(pair(nil,XS)) |
(10) |
active(splitAt(s(N),cons(X,XS))) |
→ |
mark(U11(tt,N,X,XS)) |
(11) |
active(tail(cons(N,XS))) |
→ |
mark(XS) |
(12) |
active(take(N,XS)) |
→ |
mark(fst(splitAt(N,XS))) |
(13) |
active(U11(X1,X2,X3,X4)) |
→ |
U11(active(X1),X2,X3,X4) |
(14) |
active(U12(X1,X2)) |
→ |
U12(active(X1),X2) |
(15) |
active(splitAt(X1,X2)) |
→ |
splitAt(active(X1),X2) |
(16) |
active(splitAt(X1,X2)) |
→ |
splitAt(X1,active(X2)) |
(17) |
active(pair(X1,X2)) |
→ |
pair(active(X1),X2) |
(18) |
active(pair(X1,X2)) |
→ |
pair(X1,active(X2)) |
(19) |
active(cons(X1,X2)) |
→ |
cons(active(X1),X2) |
(20) |
active(afterNth(X1,X2)) |
→ |
afterNth(active(X1),X2) |
(21) |
active(afterNth(X1,X2)) |
→ |
afterNth(X1,active(X2)) |
(22) |
active(snd(X)) |
→ |
snd(active(X)) |
(23) |
active(and(X1,X2)) |
→ |
and(active(X1),X2) |
(24) |
active(fst(X)) |
→ |
fst(active(X)) |
(25) |
active(head(X)) |
→ |
head(active(X)) |
(26) |
active(natsFrom(X)) |
→ |
natsFrom(active(X)) |
(27) |
active(s(X)) |
→ |
s(active(X)) |
(28) |
active(sel(X1,X2)) |
→ |
sel(active(X1),X2) |
(29) |
active(sel(X1,X2)) |
→ |
sel(X1,active(X2)) |
(30) |
active(tail(X)) |
→ |
tail(active(X)) |
(31) |
active(take(X1,X2)) |
→ |
take(active(X1),X2) |
(32) |
active(take(X1,X2)) |
→ |
take(X1,active(X2)) |
(33) |
U11(mark(X1),X2,X3,X4) |
→ |
mark(U11(X1,X2,X3,X4)) |
(34) |
U12(mark(X1),X2) |
→ |
mark(U12(X1,X2)) |
(35) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(36) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(37) |
pair(mark(X1),X2) |
→ |
mark(pair(X1,X2)) |
(38) |
pair(X1,mark(X2)) |
→ |
mark(pair(X1,X2)) |
(39) |
cons(mark(X1),X2) |
→ |
mark(cons(X1,X2)) |
(40) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(41) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(42) |
snd(mark(X)) |
→ |
mark(snd(X)) |
(43) |
and(mark(X1),X2) |
→ |
mark(and(X1,X2)) |
(44) |
fst(mark(X)) |
→ |
mark(fst(X)) |
(45) |
head(mark(X)) |
→ |
mark(head(X)) |
(46) |
natsFrom(mark(X)) |
→ |
mark(natsFrom(X)) |
(47) |
s(mark(X)) |
→ |
mark(s(X)) |
(48) |
sel(mark(X1),X2) |
→ |
mark(sel(X1,X2)) |
(49) |
sel(X1,mark(X2)) |
→ |
mark(sel(X1,X2)) |
(50) |
tail(mark(X)) |
→ |
mark(tail(X)) |
(51) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(52) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(53) |
proper(U11(X1,X2,X3,X4)) |
→ |
U11(proper(X1),proper(X2),proper(X3),proper(X4)) |
(54) |
proper(tt) |
→ |
ok(tt) |
(55) |
proper(U12(X1,X2)) |
→ |
U12(proper(X1),proper(X2)) |
(56) |
proper(splitAt(X1,X2)) |
→ |
splitAt(proper(X1),proper(X2)) |
(57) |
proper(pair(X1,X2)) |
→ |
pair(proper(X1),proper(X2)) |
(58) |
proper(cons(X1,X2)) |
→ |
cons(proper(X1),proper(X2)) |
(59) |
proper(afterNth(X1,X2)) |
→ |
afterNth(proper(X1),proper(X2)) |
(60) |
proper(snd(X)) |
→ |
snd(proper(X)) |
(61) |
proper(and(X1,X2)) |
→ |
and(proper(X1),proper(X2)) |
(62) |
proper(fst(X)) |
→ |
fst(proper(X)) |
(63) |
proper(head(X)) |
→ |
head(proper(X)) |
(64) |
proper(natsFrom(X)) |
→ |
natsFrom(proper(X)) |
(65) |
proper(s(X)) |
→ |
s(proper(X)) |
(66) |
proper(sel(X1,X2)) |
→ |
sel(proper(X1),proper(X2)) |
(67) |
proper(0) |
→ |
ok(0) |
(68) |
proper(nil) |
→ |
ok(nil) |
(69) |
proper(tail(X)) |
→ |
tail(proper(X)) |
(70) |
proper(take(X1,X2)) |
→ |
take(proper(X1),proper(X2)) |
(71) |
U11(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(U11(X1,X2,X3,X4)) |
(72) |
U12(ok(X1),ok(X2)) |
→ |
ok(U12(X1,X2)) |
(73) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(74) |
pair(ok(X1),ok(X2)) |
→ |
ok(pair(X1,X2)) |
(75) |
cons(ok(X1),ok(X2)) |
→ |
ok(cons(X1,X2)) |
(76) |
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(77) |
snd(ok(X)) |
→ |
ok(snd(X)) |
(78) |
and(ok(X1),ok(X2)) |
→ |
ok(and(X1,X2)) |
(79) |
fst(ok(X)) |
→ |
ok(fst(X)) |
(80) |
head(ok(X)) |
→ |
ok(head(X)) |
(81) |
natsFrom(ok(X)) |
→ |
ok(natsFrom(X)) |
(82) |
s(ok(X)) |
→ |
ok(s(X)) |
(83) |
sel(ok(X1),ok(X2)) |
→ |
ok(sel(X1,X2)) |
(84) |
tail(ok(X)) |
→ |
ok(tail(X)) |
(85) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(86) |
top(mark(X)) |
→ |
top(proper(X)) |
(87) |
top(ok(X)) |
→ |
top(active(X)) |
(88) |
There are 135 ruless (increase limit for explicit display).
The dependency pairs are split into 18
components.
-
The
1st
component contains the
pair
top#(ok(X)) |
→ |
top#(active(X)) |
(114) |
top#(mark(X)) |
→ |
top#(proper(X)) |
(99) |
1.1.1 Reduction Pair Processor with Usable Rules
Using the argument filter
π(fst) |
= |
1 |
π(top#) |
= |
1 |
π(proper) |
= |
1 |
π(ok) |
= |
1 |
π(tail#) |
= |
1 |
π(splitAt#) |
= |
1 |
π(proper#) |
= |
1 |
π(active) |
= |
1 |
π(head) |
= |
1 |
in combination with the following Weighted Path Order with the following precedence and status
prec(U11) |
= |
5 |
|
status(U11) |
= |
[2, 4, 3, 1] |
|
list-extension(U11) |
= |
Lex |
prec(cons#) |
= |
0 |
|
status(cons#) |
= |
[] |
|
list-extension(cons#) |
= |
Lex |
prec(s) |
= |
7 |
|
status(s) |
= |
[1] |
|
list-extension(s) |
= |
Lex |
prec(take#) |
= |
0 |
|
status(take#) |
= |
[1, 2] |
|
list-extension(take#) |
= |
Lex |
prec(take) |
= |
3 |
|
status(take) |
= |
[2, 1] |
|
list-extension(take) |
= |
Lex |
prec(top) |
= |
0 |
|
status(top) |
= |
[] |
|
list-extension(top) |
= |
Lex |
prec(and) |
= |
3 |
|
status(and) |
= |
[2, 1] |
|
list-extension(and) |
= |
Lex |
prec(pair) |
= |
2 |
|
status(pair) |
= |
[1, 2] |
|
list-extension(pair) |
= |
Lex |
prec(natsFrom) |
= |
7 |
|
status(natsFrom) |
= |
[1] |
|
list-extension(natsFrom) |
= |
Lex |
prec(head#) |
= |
0 |
|
status(head#) |
= |
[] |
|
list-extension(head#) |
= |
Lex |
prec(splitAt) |
= |
5 |
|
status(splitAt) |
= |
[1, 2] |
|
list-extension(splitAt) |
= |
Lex |
prec(fst#) |
= |
0 |
|
status(fst#) |
= |
[] |
|
list-extension(fst#) |
= |
Lex |
prec(U12) |
= |
4 |
|
status(U12) |
= |
[1] |
|
list-extension(U12) |
= |
Lex |
prec(U12#) |
= |
0 |
|
status(U12#) |
= |
[2, 1] |
|
list-extension(U12#) |
= |
Lex |
prec(tail) |
= |
7 |
|
status(tail) |
= |
[1] |
|
list-extension(tail) |
= |
Lex |
prec(0) |
= |
0 |
|
status(0) |
= |
[] |
|
list-extension(0) |
= |
Lex |
prec(sel#) |
= |
0 |
|
status(sel#) |
= |
[1, 2] |
|
list-extension(sel#) |
= |
Lex |
prec(sel) |
= |
8 |
|
status(sel) |
= |
[2, 1] |
|
list-extension(sel) |
= |
Lex |
prec(s#) |
= |
0 |
|
status(s#) |
= |
[] |
|
list-extension(s#) |
= |
Lex |
prec(afterNth) |
= |
5 |
|
status(afterNth) |
= |
[2, 1] |
|
list-extension(afterNth) |
= |
Lex |
prec(nil) |
= |
6 |
|
status(nil) |
= |
[] |
|
list-extension(nil) |
= |
Lex |
prec(mark) |
= |
1 |
|
status(mark) |
= |
[1] |
|
list-extension(mark) |
= |
Lex |
prec(afterNth#) |
= |
0 |
|
status(afterNth#) |
= |
[2, 1] |
|
list-extension(afterNth#) |
= |
Lex |
prec(U11#) |
= |
0 |
|
status(U11#) |
= |
[4, 3, 2, 1] |
|
list-extension(U11#) |
= |
Lex |
prec(snd#) |
= |
0 |
|
status(snd#) |
= |
[] |
|
list-extension(snd#) |
= |
Lex |
prec(cons) |
= |
3 |
|
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) |
= |
3 |
|
status(snd) |
= |
[1] |
|
list-extension(snd) |
= |
Lex |
prec(tt) |
= |
8 |
|
status(tt) |
= |
[] |
|
list-extension(tt) |
= |
Lex |
prec(pair#) |
= |
0 |
|
status(pair#) |
= |
[2, 1] |
|
list-extension(pair#) |
= |
Lex |
prec(and#) |
= |
0 |
|
status(and#) |
= |
[1, 2] |
|
list-extension(and#) |
= |
Lex |
and the following
Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
max(x1 + 58818, x2 + 29411, x3 + 29410, x4 + 58817, 0) |
[cons#(x1, x2)] |
=
|
max(x2 + 1, 0) |
[s(x1)] |
=
|
x1 + 0 |
[take#(x1, x2)] |
=
|
x1 + x2 + 1 |
[take(x1, x2)] |
=
|
x1 + x2 + 66447 |
[top(x1)] |
=
|
1 |
[and(x1, x2)] |
=
|
x1 + x2 + 11650 |
[pair(x1, x2)] |
=
|
max(x1 + 29407, x2 + 29407, 0) |
[natsFrom(x1)] |
=
|
x1 + 12282 |
[head#(x1)] |
=
|
1 |
[splitAt(x1, x2)] |
=
|
max(x1 + 29411, x2 + 58817, 0) |
[fst#(x1)] |
=
|
1 |
[U12(x1, x2)] |
=
|
max(x1 + 0, x2 + 29410, 0) |
[U12#(x1, x2)] |
=
|
max(x1 + 1, x2 + 1, 0) |
[tail(x1)] |
=
|
x1 + 13506 |
[0] |
=
|
29408 |
[sel#(x1, x2)] |
=
|
x1 + x2 + 1 |
[sel(x1, x2)] |
=
|
x1 + x2 + 83208 |
[s#(x1)] |
=
|
1 |
[afterNth(x1, x2)] |
=
|
x1 + x2 + 83207 |
[nil] |
=
|
29409 |
[mark(x1)] |
=
|
x1 + 0 |
[afterNth#(x1, x2)] |
=
|
x1 + x2 + 1 |
[U11#(x1,...,x4)] |
=
|
max(x1 + 1, x2 + 1, x3 + 1, x4 + 1, 0) |
[snd#(x1)] |
=
|
1 |
[cons(x1, x2)] |
=
|
max(x1 + 2, x2 + 0, 0) |
[natsFrom#(x1)] |
=
|
1 |
[active#(x1)] |
=
|
1 |
[snd(x1)] |
=
|
x1 + 24389 |
[tt] |
=
|
1 |
[pair#(x1, x2)] |
=
|
max(x1 + 1, x2 + 1, 0) |
[and#(x1, x2)] |
=
|
x1 + x2 + 1 |
together with the usable
rules
active(pair(X1,X2)) |
→ |
pair(active(X1),X2) |
(18) |
sel(X1,mark(X2)) |
→ |
mark(sel(X1,X2)) |
(50) |
fst(ok(X)) |
→ |
ok(fst(X)) |
(80) |
active(and(tt,X)) |
→ |
mark(X) |
(4) |
active(U12(X1,X2)) |
→ |
U12(active(X1),X2) |
(15) |
active(sel(N,XS)) |
→ |
mark(head(afterNth(N,XS))) |
(8) |
proper(U11(X1,X2,X3,X4)) |
→ |
U11(proper(X1),proper(X2),proper(X3),proper(X4)) |
(54) |
active(U11(tt,N,X,XS)) |
→ |
mark(U12(splitAt(N,XS),X)) |
(1) |
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(77) |
active(afterNth(N,XS)) |
→ |
mark(snd(splitAt(N,XS))) |
(3) |
active(splitAt(X1,X2)) |
→ |
splitAt(active(X1),X2) |
(16) |
active(afterNth(X1,X2)) |
→ |
afterNth(active(X1),X2) |
(21) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(36) |
proper(0) |
→ |
ok(0) |
(68) |
tail(ok(X)) |
→ |
ok(tail(X)) |
(85) |
active(head(X)) |
→ |
head(active(X)) |
(26) |
proper(fst(X)) |
→ |
fst(proper(X)) |
(63) |
active(pair(X1,X2)) |
→ |
pair(X1,active(X2)) |
(19) |
active(take(X1,X2)) |
→ |
take(active(X1),X2) |
(32) |
active(splitAt(X1,X2)) |
→ |
splitAt(X1,active(X2)) |
(17) |
proper(afterNth(X1,X2)) |
→ |
afterNth(proper(X1),proper(X2)) |
(60) |
active(natsFrom(X)) |
→ |
natsFrom(active(X)) |
(27) |
sel(ok(X1),ok(X2)) |
→ |
ok(sel(X1,X2)) |
(84) |
U11(mark(X1),X2,X3,X4) |
→ |
mark(U11(X1,X2,X3,X4)) |
(34) |
active(afterNth(X1,X2)) |
→ |
afterNth(X1,active(X2)) |
(22) |
active(s(X)) |
→ |
s(active(X)) |
(28) |
proper(natsFrom(X)) |
→ |
natsFrom(proper(X)) |
(65) |
and(mark(X1),X2) |
→ |
mark(and(X1,X2)) |
(44) |
active(fst(pair(X,Y))) |
→ |
mark(X) |
(5) |
U11(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(U11(X1,X2,X3,X4)) |
(72) |
active(take(X1,X2)) |
→ |
take(X1,active(X2)) |
(33) |
proper(head(X)) |
→ |
head(proper(X)) |
(64) |
active(splitAt(0,XS)) |
→ |
mark(pair(nil,XS)) |
(10) |
pair(X1,mark(X2)) |
→ |
mark(pair(X1,X2)) |
(39) |
active(natsFrom(N)) |
→ |
mark(cons(N,natsFrom(s(N)))) |
(7) |
active(cons(X1,X2)) |
→ |
cons(active(X1),X2) |
(20) |
active(fst(X)) |
→ |
fst(active(X)) |
(25) |
sel(mark(X1),X2) |
→ |
mark(sel(X1,X2)) |
(49) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(52) |
active(sel(X1,X2)) |
→ |
sel(X1,active(X2)) |
(30) |
proper(and(X1,X2)) |
→ |
and(proper(X1),proper(X2)) |
(62) |
active(U11(X1,X2,X3,X4)) |
→ |
U11(active(X1),X2,X3,X4) |
(14) |
natsFrom(ok(X)) |
→ |
ok(natsFrom(X)) |
(82) |
proper(U12(X1,X2)) |
→ |
U12(proper(X1),proper(X2)) |
(56) |
and(ok(X1),ok(X2)) |
→ |
ok(and(X1,X2)) |
(79) |
active(tail(X)) |
→ |
tail(active(X)) |
(31) |
active(tail(cons(N,XS))) |
→ |
mark(XS) |
(12) |
proper(nil) |
→ |
ok(nil) |
(69) |
fst(mark(X)) |
→ |
mark(fst(X)) |
(45) |
snd(ok(X)) |
→ |
ok(snd(X)) |
(78) |
head(ok(X)) |
→ |
ok(head(X)) |
(81) |
active(snd(X)) |
→ |
snd(active(X)) |
(23) |
proper(tail(X)) |
→ |
tail(proper(X)) |
(70) |
active(and(X1,X2)) |
→ |
and(active(X1),X2) |
(24) |
cons(ok(X1),ok(X2)) |
→ |
ok(cons(X1,X2)) |
(76) |
proper(splitAt(X1,X2)) |
→ |
splitAt(proper(X1),proper(X2)) |
(57) |
active(splitAt(s(N),cons(X,XS))) |
→ |
mark(U11(tt,N,X,XS)) |
(11) |
active(snd(pair(X,Y))) |
→ |
mark(Y) |
(9) |
active(take(N,XS)) |
→ |
mark(fst(splitAt(N,XS))) |
(13) |
tail(mark(X)) |
→ |
mark(tail(X)) |
(51) |
cons(mark(X1),X2) |
→ |
mark(cons(X1,X2)) |
(40) |
proper(sel(X1,X2)) |
→ |
sel(proper(X1),proper(X2)) |
(67) |
proper(tt) |
→ |
ok(tt) |
(55) |
proper(cons(X1,X2)) |
→ |
cons(proper(X1),proper(X2)) |
(59) |
active(head(cons(N,XS))) |
→ |
mark(N) |
(6) |
pair(mark(X1),X2) |
→ |
mark(pair(X1,X2)) |
(38) |
proper(snd(X)) |
→ |
snd(proper(X)) |
(61) |
proper(pair(X1,X2)) |
→ |
pair(proper(X1),proper(X2)) |
(58) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(74) |
pair(ok(X1),ok(X2)) |
→ |
ok(pair(X1,X2)) |
(75) |
s(mark(X)) |
→ |
mark(s(X)) |
(48) |
proper(take(X1,X2)) |
→ |
take(proper(X1),proper(X2)) |
(71) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(53) |
natsFrom(mark(X)) |
→ |
mark(natsFrom(X)) |
(47) |
U12(ok(X1),ok(X2)) |
→ |
ok(U12(X1,X2)) |
(73) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(37) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(41) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(42) |
head(mark(X)) |
→ |
mark(head(X)) |
(46) |
proper(s(X)) |
→ |
s(proper(X)) |
(66) |
s(ok(X)) |
→ |
ok(s(X)) |
(83) |
U12(mark(X1),X2) |
→ |
mark(U12(X1,X2)) |
(35) |
active(sel(X1,X2)) |
→ |
sel(active(X1),X2) |
(29) |
snd(mark(X)) |
→ |
mark(snd(X)) |
(43) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(86) |
active(U12(pair(YS,ZS),X)) |
→ |
mark(pair(cons(X,YS),ZS)) |
(2) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
top#(mark(X)) |
→ |
top#(proper(X)) |
(99) |
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#(snd(X)) |
→ |
active#(X) |
(222) |
active#(U11(X1,X2,X3,X4)) |
→ |
active#(X1) |
(160) |
active#(splitAt(X1,X2)) |
→ |
active#(X2) |
(218) |
active#(head(X)) |
→ |
active#(X) |
(157) |
active#(U12(X1,X2)) |
→ |
active#(X1) |
(205) |
active#(natsFrom(X)) |
→ |
active#(X) |
(133) |
active#(take(X1,X2)) |
→ |
active#(X1) |
(199) |
active#(pair(X1,X2)) |
→ |
active#(X1) |
(198) |
active#(pair(X1,X2)) |
→ |
active#(X2) |
(128) |
active#(s(X)) |
→ |
active#(X) |
(127) |
active#(sel(X1,X2)) |
→ |
active#(X2) |
(125) |
active#(tail(X)) |
→ |
active#(X) |
(124) |
active#(splitAt(X1,X2)) |
→ |
active#(X1) |
(192) |
active#(sel(X1,X2)) |
→ |
active#(X1) |
(120) |
active#(take(X1,X2)) |
→ |
active#(X2) |
(188) |
active#(fst(X)) |
→ |
active#(X) |
(109) |
active#(cons(X1,X2)) |
→ |
active#(X1) |
(106) |
active#(afterNth(X1,X2)) |
→ |
active#(X1) |
(98) |
active#(afterNth(X1,X2)) |
→ |
active#(X2) |
(174) |
active#(and(X1,X2)) |
→ |
active#(X1) |
(96) |
1.1.2 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
x1 + x3 + 1 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x1 + x2 + 1 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 1 |
[pair(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst(x1)] |
=
|
x1 + 1 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 5082 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x1 + 1 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
x1 + 24897 |
[proper(x1)] |
=
|
x1 + 1 |
[ok(x1)] |
=
|
3 |
[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)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
0 |
[head(x1)] |
=
|
x1 + 1 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
x1 + 0 |
[snd(x1)] |
=
|
x1 + 1 |
[tt] |
=
|
1 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
together with the usable
rules
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(77) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(36) |
U11(mark(X1),X2,X3,X4) |
→ |
mark(U11(X1,X2,X3,X4)) |
(34) |
U11(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(U11(X1,X2,X3,X4)) |
(72) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(52) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(74) |
s(mark(X)) |
→ |
mark(s(X)) |
(48) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(53) |
U12(ok(X1),ok(X2)) |
→ |
ok(U12(X1,X2)) |
(73) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(37) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(41) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(42) |
s(ok(X)) |
→ |
ok(s(X)) |
(83) |
U12(mark(X1),X2) |
→ |
mark(U12(X1,X2)) |
(35) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(86) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
active#(snd(X)) |
→ |
active#(X) |
(222) |
active#(U11(X1,X2,X3,X4)) |
→ |
active#(X1) |
(160) |
active#(splitAt(X1,X2)) |
→ |
active#(X2) |
(218) |
active#(head(X)) |
→ |
active#(X) |
(157) |
active#(U12(X1,X2)) |
→ |
active#(X1) |
(205) |
active#(natsFrom(X)) |
→ |
active#(X) |
(133) |
active#(take(X1,X2)) |
→ |
active#(X1) |
(199) |
active#(pair(X1,X2)) |
→ |
active#(X1) |
(198) |
active#(pair(X1,X2)) |
→ |
active#(X2) |
(128) |
active#(s(X)) |
→ |
active#(X) |
(127) |
active#(sel(X1,X2)) |
→ |
active#(X2) |
(125) |
active#(tail(X)) |
→ |
active#(X) |
(124) |
active#(splitAt(X1,X2)) |
→ |
active#(X1) |
(192) |
active#(sel(X1,X2)) |
→ |
active#(X1) |
(120) |
active#(take(X1,X2)) |
→ |
active#(X2) |
(188) |
active#(fst(X)) |
→ |
active#(X) |
(109) |
active#(cons(X1,X2)) |
→ |
active#(X1) |
(106) |
active#(afterNth(X1,X2)) |
→ |
active#(X1) |
(98) |
active#(afterNth(X1,X2)) |
→ |
active#(X2) |
(174) |
active#(and(X1,X2)) |
→ |
active#(X1) |
(96) |
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#(pair(X1,X2)) |
→ |
proper#(X1) |
(164) |
proper#(head(X)) |
→ |
proper#(X) |
(156) |
proper#(cons(X1,X2)) |
→ |
proper#(X1) |
(151) |
proper#(afterNth(X1,X2)) |
→ |
proper#(X2) |
(149) |
proper#(U11(X1,X2,X3,X4)) |
→ |
proper#(X1) |
(212) |
proper#(fst(X)) |
→ |
proper#(X) |
(136) |
proper#(afterNth(X1,X2)) |
→ |
proper#(X1) |
(201) |
proper#(pair(X1,X2)) |
→ |
proper#(X2) |
(200) |
proper#(U11(X1,X2,X3,X4)) |
→ |
proper#(X2) |
(196) |
proper#(cons(X1,X2)) |
→ |
proper#(X2) |
(194) |
proper#(take(X1,X2)) |
→ |
proper#(X1) |
(195) |
proper#(U12(X1,X2)) |
→ |
proper#(X2) |
(121) |
proper#(U12(X1,X2)) |
→ |
proper#(X1) |
(115) |
proper#(sel(X1,X2)) |
→ |
proper#(X1) |
(187) |
proper#(tail(X)) |
→ |
proper#(X) |
(110) |
proper#(U11(X1,X2,X3,X4)) |
→ |
proper#(X4) |
(186) |
proper#(snd(X)) |
→ |
proper#(X) |
(184) |
proper#(and(X1,X2)) |
→ |
proper#(X2) |
(183) |
proper#(and(X1,X2)) |
→ |
proper#(X1) |
(177) |
proper#(splitAt(X1,X2)) |
→ |
proper#(X1) |
(97) |
proper#(s(X)) |
→ |
proper#(X) |
(173) |
proper#(natsFrom(X)) |
→ |
proper#(X) |
(170) |
proper#(sel(X1,X2)) |
→ |
proper#(X2) |
(93) |
proper#(U11(X1,X2,X3,X4)) |
→ |
proper#(X3) |
(169) |
proper#(splitAt(X1,X2)) |
→ |
proper#(X2) |
(91) |
proper#(take(X1,X2)) |
→ |
proper#(X2) |
(168) |
1.1.3 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
x1 + x2 + x3 + x4 + 1 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x1 + x2 + 1 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 1 |
[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 |
[U12(x1, x2)] |
=
|
x1 + x2 + 1 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
x1 + 24897 |
[proper(x1)] |
=
|
x1 + 0 |
[ok(x1)] |
=
|
2 |
[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 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
0 |
[head(x1)] |
=
|
x1 + 1 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
x1 + 1 |
[tt] |
=
|
1 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
together with the usable
rules
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(77) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(36) |
U11(mark(X1),X2,X3,X4) |
→ |
mark(U11(X1,X2,X3,X4)) |
(34) |
U11(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(U11(X1,X2,X3,X4)) |
(72) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(52) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(74) |
s(mark(X)) |
→ |
mark(s(X)) |
(48) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(53) |
U12(ok(X1),ok(X2)) |
→ |
ok(U12(X1,X2)) |
(73) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(37) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(41) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(42) |
s(ok(X)) |
→ |
ok(s(X)) |
(83) |
U12(mark(X1),X2) |
→ |
mark(U12(X1,X2)) |
(35) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(86) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
proper#(pair(X1,X2)) |
→ |
proper#(X1) |
(164) |
proper#(head(X)) |
→ |
proper#(X) |
(156) |
proper#(cons(X1,X2)) |
→ |
proper#(X1) |
(151) |
proper#(afterNth(X1,X2)) |
→ |
proper#(X2) |
(149) |
proper#(U11(X1,X2,X3,X4)) |
→ |
proper#(X1) |
(212) |
proper#(fst(X)) |
→ |
proper#(X) |
(136) |
proper#(afterNth(X1,X2)) |
→ |
proper#(X1) |
(201) |
proper#(pair(X1,X2)) |
→ |
proper#(X2) |
(200) |
proper#(U11(X1,X2,X3,X4)) |
→ |
proper#(X2) |
(196) |
proper#(cons(X1,X2)) |
→ |
proper#(X2) |
(194) |
proper#(take(X1,X2)) |
→ |
proper#(X1) |
(195) |
proper#(U12(X1,X2)) |
→ |
proper#(X2) |
(121) |
proper#(U12(X1,X2)) |
→ |
proper#(X1) |
(115) |
proper#(sel(X1,X2)) |
→ |
proper#(X1) |
(187) |
proper#(tail(X)) |
→ |
proper#(X) |
(110) |
proper#(U11(X1,X2,X3,X4)) |
→ |
proper#(X4) |
(186) |
proper#(snd(X)) |
→ |
proper#(X) |
(184) |
proper#(and(X1,X2)) |
→ |
proper#(X2) |
(183) |
proper#(and(X1,X2)) |
→ |
proper#(X1) |
(177) |
proper#(splitAt(X1,X2)) |
→ |
proper#(X1) |
(97) |
proper#(s(X)) |
→ |
proper#(X) |
(173) |
proper#(natsFrom(X)) |
→ |
proper#(X) |
(170) |
proper#(sel(X1,X2)) |
→ |
proper#(X2) |
(93) |
proper#(U11(X1,X2,X3,X4)) |
→ |
proper#(X3) |
(169) |
proper#(splitAt(X1,X2)) |
→ |
proper#(X2) |
(91) |
proper#(take(X1,X2)) |
→ |
proper#(X2) |
(168) |
could be deleted.
1.1.3.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
4th
component contains the
pair
s#(ok(X)) |
→ |
s#(X) |
(214) |
s#(mark(X)) |
→ |
s#(X) |
(207) |
1.1.4 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
x1 + x2 + x3 + x4 + 0 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x1 + x2 + 0 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 1 |
[pair(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst(x1)] |
=
|
x1 + 1 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 0 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x1 + x2 + 1 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
x1 + 1 |
[proper(x1)] |
=
|
x1 + 0 |
[ok(x1)] |
=
|
x1 + 2 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
x1 + x2 + 1 |
[s#(x1)] |
=
|
x1 + 0 |
[afterNth(x1, x2)] |
=
|
x1 + x2 + 0 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 0 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
0 |
[head(x1)] |
=
|
x1 + 1 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
x1 + 1 |
[tt] |
=
|
1 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
together with the usable
rules
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(77) |
splitAt(mark(X1),X2) |
→ |
mark(splitAt(X1,X2)) |
(36) |
U11(mark(X1),X2,X3,X4) |
→ |
mark(U11(X1,X2,X3,X4)) |
(34) |
U11(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(U11(X1,X2,X3,X4)) |
(72) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(52) |
splitAt(ok(X1),ok(X2)) |
→ |
ok(splitAt(X1,X2)) |
(74) |
s(mark(X)) |
→ |
mark(s(X)) |
(48) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(53) |
U12(ok(X1),ok(X2)) |
→ |
ok(U12(X1,X2)) |
(73) |
splitAt(X1,mark(X2)) |
→ |
mark(splitAt(X1,X2)) |
(37) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(41) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(42) |
s(ok(X)) |
→ |
ok(s(X)) |
(83) |
U12(mark(X1),X2) |
→ |
mark(U12(X1,X2)) |
(35) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(86) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
could be deleted.
1.1.4.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
5th
component contains the
pair
take#(ok(X1),ok(X2)) |
→ |
take#(X1,X2) |
(209) |
take#(mark(X1),X2) |
→ |
take#(X1,X2) |
(204) |
take#(X1,mark(X2)) |
→ |
take#(X1,X2) |
(193) |
1.1.5 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
x1 + x2 + x3 + x4 + 0 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
x2 + 0 |
[take(x1, x2)] |
=
|
x1 + x2 + 0 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 22305 |
[pair(x1, x2)] |
=
|
x1 + x2 + 1 |
[fst(x1)] |
=
|
28224 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 0 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
x2 + 2 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x1 + x2 + 1 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
x1 + 34320 |
[proper(x1)] |
=
|
x1 + 0 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
x1 + x2 + 1 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
x1 + x2 + 0 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 1 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
x1 + 1 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
x1 + 1 |
[tt] |
=
|
1 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
together with the usable
rules
afterNth(ok(X1),ok(X2)) |
→ |
ok(afterNth(X1,X2)) |
(77) |
U11(mark(X1),X2,X3,X4) |
→ |
mark(U11(X1,X2,X3,X4)) |
(34) |
U11(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
ok(U11(X1,X2,X3,X4)) |
(72) |
take(mark(X1),X2) |
→ |
mark(take(X1,X2)) |
(52) |
s(mark(X)) |
→ |
mark(s(X)) |
(48) |
take(X1,mark(X2)) |
→ |
mark(take(X1,X2)) |
(53) |
U12(ok(X1),ok(X2)) |
→ |
ok(U12(X1,X2)) |
(73) |
afterNth(mark(X1),X2) |
→ |
mark(afterNth(X1,X2)) |
(41) |
afterNth(X1,mark(X2)) |
→ |
mark(afterNth(X1,X2)) |
(42) |
s(ok(X)) |
→ |
ok(s(X)) |
(83) |
U12(mark(X1),X2) |
→ |
mark(U12(X1,X2)) |
(35) |
take(ok(X1),ok(X2)) |
→ |
ok(take(X1,X2)) |
(86) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
take#(ok(X1),ok(X2)) |
→ |
take#(X1,X2) |
(209) |
take#(X1,mark(X2)) |
→ |
take#(X1,X2) |
(193) |
could be deleted.
1.1.5.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
6th
component contains the
pair
pair#(X1,mark(X2)) |
→ |
pair#(X1,X2) |
(152) |
pair#(ok(X1),ok(X2)) |
→ |
pair#(X1,X2) |
(185) |
pair#(mark(X1),X2) |
→ |
pair#(X1,X2) |
(92) |
1.1.6 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
x1 + x3 + 18698 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
616 |
[pair(x1, x2)] |
=
|
x2 + 24124 |
[fst(x1)] |
=
|
31048 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 37157 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
27127 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
23724 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
12771 |
[proper(x1)] |
=
|
x1 + 1 |
[ok(x1)] |
=
|
x1 + 29351 |
[0] |
=
|
21965 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
18419 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
15079 |
[nil] |
=
|
52813 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 7675 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
28473 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x2 + 24813 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
23033 |
[tt] |
=
|
1 |
[pair#(x1, x2)] |
=
|
x1 + x2 + 0 |
[and#(x1, x2)] |
=
|
0 |
together with the usable
rules
s(mark(X)) |
→ |
mark(s(X)) |
(48) |
s(ok(X)) |
→ |
ok(s(X)) |
(83) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
pair#(X1,mark(X2)) |
→ |
pair#(X1,X2) |
(152) |
pair#(ok(X1),ok(X2)) |
→ |
pair#(X1,X2) |
(185) |
pair#(mark(X1),X2) |
→ |
pair#(X1,X2) |
(92) |
could be deleted.
1.1.6.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
7th
component contains the
pair
snd#(ok(X)) |
→ |
snd#(X) |
(162) |
snd#(mark(X)) |
→ |
snd#(X) |
(219) |
1.1.7 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
25853 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
15786 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
31849 |
[pair(x1, x2)] |
=
|
x1 + 8927 |
[fst(x1)] |
=
|
19784 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
25324 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 22742 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
12876 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 764 |
[0] |
=
|
56785 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
17272 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
16847 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 4 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
3 |
[head(x1)] |
=
|
12450 |
[snd#(x1)] |
=
|
x1 + 0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 8930 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
23381 |
[tt] |
=
|
4673 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
snd#(ok(X)) |
→ |
snd#(X) |
(162) |
snd#(mark(X)) |
→ |
snd#(X) |
(219) |
could be deleted.
1.1.7.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
8th
component contains the
pair
cons#(mark(X1),X2) |
→ |
cons#(X1,X2) |
(206) |
cons#(ok(X1),ok(X2)) |
→ |
cons#(X1,X2) |
(182) |
1.1.8 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
25853 |
[cons#(x1, x2)] |
=
|
x1 + 0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
12333 |
[pair(x1, x2)] |
=
|
x1 + 2 |
[fst(x1)] |
=
|
35596 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
16038 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 27469 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
12874 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
2 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 5 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
34659 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 39590 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
17083 |
[tt] |
=
|
4673 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
cons#(mark(X1),X2) |
→ |
cons#(X1,X2) |
(206) |
cons#(ok(X1),ok(X2)) |
→ |
cons#(X1,X2) |
(182) |
could be deleted.
1.1.8.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
9th
component contains the
pair
sel#(X1,mark(X2)) |
→ |
sel#(X1,X2) |
(155) |
sel#(mark(X1),X2) |
→ |
sel#(X1,X2) |
(148) |
sel#(ok(X1),ok(X2)) |
→ |
sel#(X1,X2) |
(137) |
1.1.9 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
10310 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 9623 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
32023 |
[pair(x1, x2)] |
=
|
x1 + 2 |
[fst(x1)] |
=
|
27135 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
2 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 17535 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
12874 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
x2 + 0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
2 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 5 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
7943 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
2 |
[tt] |
=
|
1 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
sel#(X1,mark(X2)) |
→ |
sel#(X1,X2) |
(155) |
sel#(ok(X1),ok(X2)) |
→ |
sel#(X1,X2) |
(137) |
could be deleted.
1.1.9.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
10th
component contains the
pair
splitAt#(X1,mark(X2)) |
→ |
splitAt#(X1,X2) |
(158) |
splitAt#(ok(X1),ok(X2)) |
→ |
splitAt#(X1,X2) |
(141) |
splitAt#(mark(X1),X2) |
→ |
splitAt#(X1,X2) |
(116) |
1.1.10 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
24036 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 22135 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
16349 |
[pair(x1, x2)] |
=
|
x1 + 2 |
[fst(x1)] |
=
|
12700 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 3449 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
2 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 2 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
12874 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
30145 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
2 |
[nil] |
=
|
52051 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
x2 + 0 |
[mark(x1)] |
=
|
x1 + 5 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
22051 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
2 |
[tt] |
=
|
18072 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
splitAt#(X1,mark(X2)) |
→ |
splitAt#(X1,X2) |
(158) |
splitAt#(ok(X1),ok(X2)) |
→ |
splitAt#(X1,X2) |
(141) |
could be deleted.
1.1.10.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
11th
component contains the
pair
tail#(ok(X)) |
→ |
tail#(X) |
(113) |
tail#(mark(X)) |
→ |
tail#(X) |
(101) |
1.1.11 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
5152 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 19734 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 25342 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
30435 |
[pair(x1, x2)] |
=
|
x1 + 3190 |
[fst(x1)] |
=
|
22295 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
5576 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 25320 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
27345 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 27869 |
[0] |
=
|
1090 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
1751 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
29044 |
[nil] |
=
|
19891 |
[tail#(x1)] |
=
|
x1 + 0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 10741 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 18407 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
4811 |
[tt] |
=
|
10509 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
tail#(ok(X)) |
→ |
tail#(X) |
(113) |
tail#(mark(X)) |
→ |
tail#(X) |
(101) |
could be deleted.
1.1.11.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
12th
component contains the
pair
U12#(ok(X1),ok(X2)) |
→ |
U12#(X1,X2) |
(216) |
U12#(mark(X1),X2) |
→ |
U12#(X1,X2) |
(171) |
1.1.12 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
5152 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
30435 |
[pair(x1, x2)] |
=
|
x1 + 26107 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
2 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 30352 |
[U12#(x1, x2)] |
=
|
x2 + 0 |
[tail(x1)] |
=
|
27345 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 4004 |
[0] |
=
|
9311 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
22786 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
2 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 10741 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
4811 |
[tt] |
=
|
1 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
U12#(ok(X1),ok(X2)) |
→ |
U12#(X1,X2) |
(216) |
could be deleted.
1.1.12.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
13th
component contains the
pair
and#(ok(X1),ok(X2)) |
→ |
and#(X1,X2) |
(153) |
and#(mark(X1),X2) |
→ |
and#(X1,X2) |
(90) |
1.1.13 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
2 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 11875 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
7531 |
[pair(x1, x2)] |
=
|
x1 + 2 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 13881 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
2 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 16387 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
27345 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 21559 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
2 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 10741 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
2 |
[tt] |
=
|
1 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
x1 + 0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
and#(ok(X1),ok(X2)) |
→ |
and#(X1,X2) |
(153) |
and#(mark(X1),X2) |
→ |
and#(X1,X2) |
(90) |
could be deleted.
1.1.13.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
14th
component contains the
pair
head#(mark(X)) |
→ |
head#(X) |
(132) |
head#(ok(X)) |
→ |
head#(X) |
(129) |
1.1.14 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
17267 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 32353 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 11875 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
8234 |
[pair(x1, x2)] |
=
|
x1 + 9543 |
[fst(x1)] |
=
|
10182 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
x1 + 0 |
[splitAt(x1, x2)] |
=
|
11765 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 42654 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
27345 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 21559 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
26837 |
[nil] |
=
|
11414 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 10741 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
11804 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 19214 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
2 |
[tt] |
=
|
26537 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
head#(mark(X)) |
→ |
head#(X) |
(132) |
head#(ok(X)) |
→ |
head#(X) |
(129) |
could be deleted.
1.1.14.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
15th
component contains the
pair
natsFrom#(mark(X)) |
→ |
natsFrom#(X) |
(208) |
natsFrom#(ok(X)) |
→ |
natsFrom#(X) |
(191) |
1.1.15 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
22101 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 32353 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 30530 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
8234 |
[pair(x1, x2)] |
=
|
x1 + 9607 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
11765 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 64240 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
27345 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 4418 |
[0] |
=
|
196 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
13579 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
26837 |
[nil] |
=
|
57134 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 10741 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
25054 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 32537 |
[natsFrom#(x1)] |
=
|
x1 + 0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
2 |
[tt] |
=
|
32207 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
natsFrom#(mark(X)) |
→ |
natsFrom#(X) |
(208) |
natsFrom#(ok(X)) |
→ |
natsFrom#(X) |
(191) |
could be deleted.
1.1.15.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
16th
component contains the
pair
afterNth#(X1,mark(X2)) |
→ |
afterNth#(X1,X2) |
(150) |
afterNth#(mark(X1),X2) |
→ |
afterNth#(X1,X2) |
(130) |
afterNth#(ok(X1),ok(X2)) |
→ |
afterNth#(X1,X2) |
(180) |
1.1.16 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
23655 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
2939 |
[pair(x1, x2)] |
=
|
x1 + 8742 |
[fst(x1)] |
=
|
2 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
2 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 64240 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
27345 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 12881 |
[0] |
=
|
1 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
13579 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
2 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 20987 |
[afterNth#(x1, x2)] |
=
|
x1 + 0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
2 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 1 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
2 |
[tt] |
=
|
32207 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
afterNth#(mark(X1),X2) |
→ |
afterNth#(X1,X2) |
(130) |
afterNth#(ok(X1),ok(X2)) |
→ |
afterNth#(X1,X2) |
(180) |
could be deleted.
1.1.16.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
17th
component contains the
pair
fst#(ok(X)) |
→ |
fst#(X) |
(123) |
fst#(mark(X)) |
→ |
fst#(X) |
(108) |
1.1.17 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
15214 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 15343 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
20023 |
[pair(x1, x2)] |
=
|
x1 + 15062 |
[fst(x1)] |
=
|
17221 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
21762 |
[fst#(x1)] |
=
|
x1 + 0 |
[U12(x1, x2)] |
=
|
x2 + 117584 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
27345 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 4390 |
[0] |
=
|
20099 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
2 |
[nil] |
=
|
2998 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 31992 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
13135 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 32435 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
2 |
[tt] |
=
|
46716 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
fst#(ok(X)) |
→ |
fst#(X) |
(123) |
fst#(mark(X)) |
→ |
fst#(X) |
(108) |
could be deleted.
1.1.17.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
18th
component contains the
pair
U11#(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
U11#(X1,X2,X3,X4) |
(202) |
U11#(mark(X1),X2,X3,X4) |
→ |
U11#(X1,X2,X3,X4) |
(176) |
1.1.18 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[U11(x1,...,x4)] |
=
|
2 |
[cons#(x1, x2)] |
=
|
0 |
[s(x1)] |
=
|
x1 + 1 |
[take#(x1, x2)] |
=
|
0 |
[take(x1, x2)] |
=
|
x2 + 23861 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
12572 |
[pair(x1, x2)] |
=
|
x1 + 2 |
[fst(x1)] |
=
|
47115 |
[top#(x1)] |
=
|
0 |
[natsFrom(x1)] |
=
|
x1 + 1 |
[head#(x1)] |
=
|
0 |
[splitAt(x1, x2)] |
=
|
26412 |
[fst#(x1)] |
=
|
0 |
[U12(x1, x2)] |
=
|
x2 + 2 |
[U12#(x1, x2)] |
=
|
0 |
[tail(x1)] |
=
|
27345 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 834 |
[0] |
=
|
94 |
[sel#(x1, x2)] |
=
|
0 |
[sel(x1, x2)] |
=
|
2 |
[s#(x1)] |
=
|
0 |
[afterNth(x1, x2)] |
=
|
30824 |
[nil] |
=
|
1 |
[tail#(x1)] |
=
|
0 |
[splitAt#(x1, x2)] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 2215 |
[afterNth#(x1, x2)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[U11#(x1,...,x4)] |
=
|
x2 + 0 |
[active(x1)] |
=
|
1 |
[head(x1)] |
=
|
25940 |
[snd#(x1)] |
=
|
0 |
[cons(x1, x2)] |
=
|
x1 + x2 + 15781 |
[natsFrom#(x1)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[snd(x1)] |
=
|
295 |
[tt] |
=
|
16686 |
[pair#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
U11#(ok(X1),ok(X2),ok(X3),ok(X4)) |
→ |
U11#(X1,X2,X3,X4) |
(202) |
could be deleted.
1.1.18.1 Dependency Graph Processor
The dependency pairs are split into 1
component.