The rewrite relation of the following TRS is considered.
There are 142 ruless (increase limit for explicit display).
There are 206 ruless (increase limit for explicit display).
The dependency pairs are split into 28
components.
-
The
1st
component contains the
pair
top#(mark(X)) |
→ |
top#(proper(X)) |
(213) |
top#(ok(X)) |
→ |
top#(active(X)) |
(208) |
1.1.1 Reduction Pair Processor with Usable Rules
Using the argument filter
π(U72#) |
= |
1 |
π(U32#) |
= |
1 |
π(top) |
= |
1 |
π(isNeList#) |
= |
1 |
π(U53#) |
= |
1 |
π(top#) |
= |
1 |
π(isPal#) |
= |
1 |
π(U52#) |
= |
1 |
π(proper) |
= |
1 |
π(ok) |
= |
1 |
π(isNePal#) |
= |
1 |
π(U11#) |
= |
1 |
π(active) |
= |
1 |
π(U21#) |
= |
1 |
π(isPalListKind) |
= |
1 |
in combination with the following Weighted Path Order with the following precedence and status
prec(a) |
= |
4 |
|
status(a) |
= |
[] |
|
list-extension(a) |
= |
Lex |
prec(U21) |
= |
12 |
|
status(U21) |
= |
[3, 2, 1] |
|
list-extension(U21) |
= |
Lex |
prec(isPalListKind#) |
= |
0 |
|
status(isPalListKind#) |
= |
[] |
|
list-extension(isPalListKind#) |
= |
Lex |
prec(U11) |
= |
8 |
|
status(U11) |
= |
[1, 2] |
|
list-extension(U11) |
= |
Lex |
prec(isNeList) |
= |
7 |
|
status(isNeList) |
= |
[1] |
|
list-extension(isNeList) |
= |
Lex |
prec(isPal) |
= |
13 |
|
status(isPal) |
= |
[1] |
|
list-extension(isPal) |
= |
Lex |
prec(U42) |
= |
11 |
|
status(U42) |
= |
[1, 2] |
|
list-extension(U42) |
= |
Lex |
prec(u) |
= |
6 |
|
status(u) |
= |
[] |
|
list-extension(u) |
= |
Lex |
prec(U71) |
= |
10 |
|
status(U71) |
= |
[2, 1] |
|
list-extension(U71) |
= |
Lex |
prec(and) |
= |
9 |
|
status(and) |
= |
[1, 2] |
|
list-extension(and) |
= |
Lex |
prec(U43) |
= |
5 |
|
status(U43) |
= |
[1] |
|
list-extension(U43) |
= |
Lex |
prec(U23#) |
= |
0 |
|
status(U23#) |
= |
[] |
|
list-extension(U23#) |
= |
Lex |
prec(__#) |
= |
0 |
|
status(__#) |
= |
[] |
|
list-extension(__#) |
= |
Lex |
prec(U43#) |
= |
0 |
|
status(U43#) |
= |
[] |
|
list-extension(U43#) |
= |
Lex |
prec(U23) |
= |
1 |
|
status(U23) |
= |
[1] |
|
list-extension(U23) |
= |
Lex |
prec(isNePal) |
= |
10 |
|
status(isNePal) |
= |
[1] |
|
list-extension(isNePal) |
= |
Lex |
prec(U72) |
= |
9 |
|
status(U72) |
= |
[1] |
|
list-extension(U72) |
= |
Lex |
prec(isQid#) |
= |
0 |
|
status(isQid#) |
= |
[] |
|
list-extension(isQid#) |
= |
Lex |
prec(U12) |
= |
3 |
|
status(U12) |
= |
[1] |
|
list-extension(U12) |
= |
Lex |
prec(isQid) |
= |
6 |
|
status(isQid) |
= |
[] |
|
list-extension(isQid) |
= |
Lex |
prec(o) |
= |
6 |
|
status(o) |
= |
[] |
|
list-extension(o) |
= |
Lex |
prec(U42#) |
= |
0 |
|
status(U42#) |
= |
[] |
|
list-extension(U42#) |
= |
Lex |
prec(U12#) |
= |
0 |
|
status(U12#) |
= |
[] |
|
list-extension(U12#) |
= |
Lex |
prec(U62#) |
= |
0 |
|
status(U62#) |
= |
[] |
|
list-extension(U62#) |
= |
Lex |
prec(isList) |
= |
9 |
|
status(isList) |
= |
[1] |
|
list-extension(isList) |
= |
Lex |
prec(nil) |
= |
6 |
|
status(nil) |
= |
[] |
|
list-extension(nil) |
= |
Lex |
prec(U62) |
= |
1 |
|
status(U62) |
= |
[1] |
|
list-extension(U62) |
= |
Lex |
prec(mark) |
= |
1 |
|
status(mark) |
= |
[1] |
|
list-extension(mark) |
= |
Lex |
prec(isList#) |
= |
0 |
|
status(isList#) |
= |
[] |
|
list-extension(isList#) |
= |
Lex |
prec(U32) |
= |
5 |
|
status(U32) |
= |
[1] |
|
list-extension(U32) |
= |
Lex |
prec(proper#) |
= |
0 |
|
status(proper#) |
= |
[] |
|
list-extension(proper#) |
= |
Lex |
prec(i) |
= |
6 |
|
status(i) |
= |
[] |
|
list-extension(i) |
= |
Lex |
prec(U52) |
= |
11 |
|
status(U52) |
= |
[1, 2] |
|
list-extension(U52) |
= |
Lex |
prec(U61) |
= |
7 |
|
status(U61) |
= |
[1] |
|
list-extension(U61) |
= |
Lex |
prec(U51#) |
= |
0 |
|
status(U51#) |
= |
[2, 1, 3] |
|
list-extension(U51#) |
= |
Lex |
prec(e) |
= |
6 |
|
status(e) |
= |
[] |
|
list-extension(e) |
= |
Lex |
prec(U31) |
= |
6 |
|
status(U31) |
= |
[2, 1] |
|
list-extension(U31) |
= |
Lex |
prec(U41#) |
= |
0 |
|
status(U41#) |
= |
[3, 1] |
|
list-extension(U41#) |
= |
Lex |
prec(active#) |
= |
0 |
|
status(active#) |
= |
[] |
|
list-extension(active#) |
= |
Lex |
prec(U22#) |
= |
0 |
|
status(U22#) |
= |
[2, 1] |
|
list-extension(U22#) |
= |
Lex |
prec(tt) |
= |
3 |
|
status(tt) |
= |
[] |
|
list-extension(tt) |
= |
Lex |
prec(U71#) |
= |
0 |
|
status(U71#) |
= |
[2, 1] |
|
list-extension(U71#) |
= |
Lex |
prec(U22) |
= |
9 |
|
status(U22) |
= |
[2, 1] |
|
list-extension(U22) |
= |
Lex |
prec(U51) |
= |
12 |
|
status(U51) |
= |
[2, 3, 1] |
|
list-extension(U51) |
= |
Lex |
prec(U53) |
= |
2 |
|
status(U53) |
= |
[1] |
|
list-extension(U53) |
= |
Lex |
prec(U41) |
= |
12 |
|
status(U41) |
= |
[3, 2, 1] |
|
list-extension(U41) |
= |
Lex |
prec(U31#) |
= |
0 |
|
status(U31#) |
= |
[2, 1] |
|
list-extension(U31#) |
= |
Lex |
prec(and#) |
= |
0 |
|
status(and#) |
= |
[1, 2] |
|
list-extension(and#) |
= |
Lex |
prec(__) |
= |
13 |
|
status(__) |
= |
[1, 2] |
|
list-extension(__) |
= |
Lex |
prec(U61#) |
= |
0 |
|
status(U61#) |
= |
[1, 2] |
|
list-extension(U61#) |
= |
Lex |
and the following
Max-polynomial interpretation
[a] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
max(x1 + 0, x2 + 0, x3 + 0, 0) |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[isNeList(x1)] |
=
|
x1 + 0 |
[isPal(x1)] |
=
|
x1 + 0 |
[U42(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[u] |
=
|
0 |
[U71(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[and(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[U43(x1)] |
=
|
x1 + 0 |
[U23#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
max(0) |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 0 |
[isNePal(x1)] |
=
|
x1 + 0 |
[U72(x1)] |
=
|
x1 + 0 |
[isQid#(x1)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 0 |
[isQid(x1)] |
=
|
0 |
[o] |
=
|
0 |
[U42#(x1, x2)] |
=
|
max(0) |
[U12#(x1)] |
=
|
0 |
[U62#(x1)] |
=
|
0 |
[isList(x1)] |
=
|
x1 + 0 |
[nil] |
=
|
0 |
[U62(x1)] |
=
|
x1 + 0 |
[mark(x1)] |
=
|
x1 + 0 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
x1 + 0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
0 |
[U52(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[U61(x1, x2)] |
=
|
max(x1 + 0, 0) |
[U51#(x1, x2, x3)] |
=
|
max(x1 + 0, x2 + 0, x3 + 0, 0) |
[e] |
=
|
0 |
[U31(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[U41#(x1, x2, x3)] |
=
|
max(x1 + 0, x3 + 0, 0) |
[active#(x1)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[tt] |
=
|
0 |
[U71#(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[U22(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[U51(x1, x2, x3)] |
=
|
max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U53(x1)] |
=
|
x1 + 0 |
[U41(x1, x2, x3)] |
=
|
max(x1 + 0, x2 + 0, x3 + 0, 0) |
[U31#(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[and#(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[__(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[U61#(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
together with the usable
rulesThere are 140 ruless (increase limit for explicit display).
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
top#(mark(X)) |
→ |
top#(proper(X)) |
(213) |
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#(U61(X1,X2)) |
→ |
active#(X1) |
(343) |
active#(U41(X1,X2,X3)) |
→ |
active#(X1) |
(244) |
active#(U42(X1,X2)) |
→ |
active#(X1) |
(337) |
active#(U23(X)) |
→ |
active#(X) |
(240) |
active#(U51(X1,X2,X3)) |
→ |
active#(X1) |
(336) |
active#(U11(X1,X2)) |
→ |
active#(X1) |
(239) |
active#(__(X1,X2)) |
→ |
active#(X1) |
(331) |
active#(U22(X1,X2)) |
→ |
active#(X1) |
(222) |
active#(U62(X)) |
→ |
active#(X) |
(319) |
active#(and(X1,X2)) |
→ |
active#(X1) |
(212) |
active#(U43(X)) |
→ |
active#(X) |
(196) |
active#(U32(X)) |
→ |
active#(X) |
(187) |
active#(U72(X)) |
→ |
active#(X) |
(176) |
active#(U21(X1,X2,X3)) |
→ |
active#(X1) |
(279) |
active#(U12(X)) |
→ |
active#(X) |
(275) |
active#(U52(X1,X2)) |
→ |
active#(X1) |
(164) |
active#(__(X1,X2)) |
→ |
active#(X2) |
(163) |
active#(U31(X1,X2)) |
→ |
active#(X1) |
(265) |
active#(U71(X1,X2)) |
→ |
active#(X1) |
(152) |
active#(U53(X)) |
→ |
active#(X) |
(259) |
1.1.2 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
x1 + x3 + 1 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
x1 + x2 + 1 |
[isNeList(x1)] |
=
|
x1 + 0 |
[isPal(x1)] |
=
|
x1 + 1 |
[U42(x1, x2)] |
=
|
x1 + x2 + 5 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + 3289 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + 2 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
x1 + 9 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 9 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
x1 + 3292 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 21544 |
[isQid(x1)] |
=
|
x1 + 0 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
x1 + 1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 2 |
[isList(x1)] |
=
|
x1 + 0 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
x1 + 38687 |
[mark(x1)] |
=
|
x1 + 0 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
x1 + 5 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1, x2)] |
=
|
x1 + x2 + 13024 |
[U61(x1, x2)] |
=
|
x1 + x2 + 4037 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 0 |
[U31(x1, x2)] |
=
|
x1 + 1 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
x1 + 0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
3 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 5 |
[U51(x1, x2, x3)] |
=
|
x1 + x3 + 1 |
[isPalListKind(x1)] |
=
|
x1 + 0 |
[U53(x1)] |
=
|
x1 + 13028 |
[U41(x1, x2, x3)] |
=
|
x1 + x3 + 1 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rules
isList(ok(X)) |
→ |
ok(isList(X)) |
(122) |
U53(mark(X)) |
→ |
mark(U53(X)) |
(78) |
U42(ok(X1),ok(X2)) |
→ |
ok(U42(X1,X2)) |
(128) |
U23(mark(X)) |
→ |
mark(U23(X)) |
(70) |
U53(ok(X)) |
→ |
ok(U53(X)) |
(132) |
U42(mark(X1),X2) |
→ |
mark(U42(X1,X2)) |
(74) |
U23(ok(X)) |
→ |
ok(U23(X)) |
(123) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
active#(U61(X1,X2)) |
→ |
active#(X1) |
(343) |
active#(U41(X1,X2,X3)) |
→ |
active#(X1) |
(244) |
active#(U42(X1,X2)) |
→ |
active#(X1) |
(337) |
active#(U23(X)) |
→ |
active#(X) |
(240) |
active#(U51(X1,X2,X3)) |
→ |
active#(X1) |
(336) |
active#(U11(X1,X2)) |
→ |
active#(X1) |
(239) |
active#(__(X1,X2)) |
→ |
active#(X1) |
(331) |
active#(U22(X1,X2)) |
→ |
active#(X1) |
(222) |
active#(U62(X)) |
→ |
active#(X) |
(319) |
active#(and(X1,X2)) |
→ |
active#(X1) |
(212) |
active#(U43(X)) |
→ |
active#(X) |
(196) |
active#(U32(X)) |
→ |
active#(X) |
(187) |
active#(U72(X)) |
→ |
active#(X) |
(176) |
active#(U21(X1,X2,X3)) |
→ |
active#(X1) |
(279) |
active#(U12(X)) |
→ |
active#(X) |
(275) |
active#(U52(X1,X2)) |
→ |
active#(X1) |
(164) |
active#(__(X1,X2)) |
→ |
active#(X2) |
(163) |
active#(U31(X1,X2)) |
→ |
active#(X1) |
(265) |
active#(U71(X1,X2)) |
→ |
active#(X1) |
(152) |
active#(U53(X)) |
→ |
active#(X) |
(259) |
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#(U43(X)) |
→ |
proper#(X) |
(344) |
proper#(isNeList(X)) |
→ |
proper#(X) |
(341) |
proper#(U22(X1,X2)) |
→ |
proper#(X2) |
(248) |
proper#(isPal(X)) |
→ |
proper#(X) |
(246) |
proper#(isNePal(X)) |
→ |
proper#(X) |
(243) |
proper#(isList(X)) |
→ |
proper#(X) |
(236) |
proper#(U31(X1,X2)) |
→ |
proper#(X2) |
(233) |
proper#(U62(X)) |
→ |
proper#(X) |
(226) |
proper#(U52(X1,X2)) |
→ |
proper#(X1) |
(225) |
proper#(U31(X1,X2)) |
→ |
proper#(X1) |
(223) |
proper#(and(X1,X2)) |
→ |
proper#(X2) |
(323) |
proper#(U12(X)) |
→ |
proper#(X) |
(220) |
proper#(U42(X1,X2)) |
→ |
proper#(X1) |
(218) |
proper#(U11(X1,X2)) |
→ |
proper#(X2) |
(318) |
proper#(U22(X1,X2)) |
→ |
proper#(X1) |
(216) |
proper#(U32(X)) |
→ |
proper#(X) |
(317) |
proper#(U41(X1,X2,X3)) |
→ |
proper#(X2) |
(316) |
proper#(isPalListKind(X)) |
→ |
proper#(X) |
(211) |
proper#(U61(X1,X2)) |
→ |
proper#(X2) |
(295) |
proper#(U72(X)) |
→ |
proper#(X) |
(194) |
proper#(__(X1,X2)) |
→ |
proper#(X2) |
(292) |
proper#(U21(X1,X2,X3)) |
→ |
proper#(X3) |
(293) |
proper#(U21(X1,X2,X3)) |
→ |
proper#(X2) |
(192) |
proper#(U53(X)) |
→ |
proper#(X) |
(190) |
proper#(U71(X1,X2)) |
→ |
proper#(X1) |
(178) |
proper#(U21(X1,X2,X3)) |
→ |
proper#(X1) |
(179) |
proper#(U71(X1,X2)) |
→ |
proper#(X2) |
(280) |
proper#(U51(X1,X2,X3)) |
→ |
proper#(X2) |
(175) |
proper#(and(X1,X2)) |
→ |
proper#(X1) |
(173) |
proper#(U42(X1,X2)) |
→ |
proper#(X2) |
(169) |
proper#(U41(X1,X2,X3)) |
→ |
proper#(X3) |
(276) |
proper#(U52(X1,X2)) |
→ |
proper#(X2) |
(162) |
proper#(isQid(X)) |
→ |
proper#(X) |
(264) |
proper#(U61(X1,X2)) |
→ |
proper#(X1) |
(154) |
proper#(__(X1,X2)) |
→ |
proper#(X1) |
(155) |
proper#(U23(X)) |
→ |
proper#(X) |
(260) |
proper#(U51(X1,X2,X3)) |
→ |
proper#(X1) |
(150) |
proper#(U51(X1,X2,X3)) |
→ |
proper#(X3) |
(254) |
proper#(U11(X1,X2)) |
→ |
proper#(X1) |
(143) |
proper#(U41(X1,X2,X3)) |
→ |
proper#(X1) |
(253) |
1.1.3 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
x1 + x2 + x3 + 1 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
x1 + x2 + 1 |
[isNeList(x1)] |
=
|
x1 + 11123 |
[isPal(x1)] |
=
|
x1 + 1 |
[U42(x1, x2)] |
=
|
x1 + x2 + 4 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 1 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 17374 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
x1 + 11199 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 24637 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
x1 + 4 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 1 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
x1 + 0 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
x1 + 12160 |
[mark(x1)] |
=
|
x1 + 0 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
x1 + 49419 |
[proper#(x1)] |
=
|
x1 + 0 |
[i] |
=
|
1 |
[U52(x1, x2)] |
=
|
x1 + x2 + 2765 |
[U61(x1, x2)] |
=
|
x1 + x2 + 1 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 0 |
[U31(x1, x2)] |
=
|
x1 + x2 + 23904 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
3 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 24634 |
[U51(x1, x2, x3)] |
=
|
x1 + x2 + x3 + 9555 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
x1 + 13028 |
[U41(x1, x2, x3)] |
=
|
x1 + x2 + x3 + 1 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rules
isPal(ok(X)) |
→ |
ok(isPal(X)) |
(140) |
isList(ok(X)) |
→ |
ok(isList(X)) |
(122) |
U53(mark(X)) |
→ |
mark(U53(X)) |
(78) |
U42(ok(X1),ok(X2)) |
→ |
ok(U42(X1,X2)) |
(128) |
U23(mark(X)) |
→ |
mark(U23(X)) |
(70) |
U53(ok(X)) |
→ |
ok(U53(X)) |
(132) |
U42(mark(X1),X2) |
→ |
mark(U42(X1,X2)) |
(74) |
U23(ok(X)) |
→ |
ok(U23(X)) |
(123) |
isPalListKind(ok(X)) |
→ |
ok(isPalListKind(X)) |
(139) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
proper#(U43(X)) |
→ |
proper#(X) |
(344) |
proper#(isNeList(X)) |
→ |
proper#(X) |
(341) |
proper#(U22(X1,X2)) |
→ |
proper#(X2) |
(248) |
proper#(isPal(X)) |
→ |
proper#(X) |
(246) |
proper#(isNePal(X)) |
→ |
proper#(X) |
(243) |
proper#(isList(X)) |
→ |
proper#(X) |
(236) |
proper#(U31(X1,X2)) |
→ |
proper#(X2) |
(233) |
proper#(U62(X)) |
→ |
proper#(X) |
(226) |
proper#(U52(X1,X2)) |
→ |
proper#(X1) |
(225) |
proper#(U31(X1,X2)) |
→ |
proper#(X1) |
(223) |
proper#(and(X1,X2)) |
→ |
proper#(X2) |
(323) |
proper#(U12(X)) |
→ |
proper#(X) |
(220) |
proper#(U42(X1,X2)) |
→ |
proper#(X1) |
(218) |
proper#(U11(X1,X2)) |
→ |
proper#(X2) |
(318) |
proper#(U22(X1,X2)) |
→ |
proper#(X1) |
(216) |
proper#(U32(X)) |
→ |
proper#(X) |
(317) |
proper#(U41(X1,X2,X3)) |
→ |
proper#(X2) |
(316) |
proper#(isPalListKind(X)) |
→ |
proper#(X) |
(211) |
proper#(U61(X1,X2)) |
→ |
proper#(X2) |
(295) |
proper#(U72(X)) |
→ |
proper#(X) |
(194) |
proper#(__(X1,X2)) |
→ |
proper#(X2) |
(292) |
proper#(U21(X1,X2,X3)) |
→ |
proper#(X3) |
(293) |
proper#(U21(X1,X2,X3)) |
→ |
proper#(X2) |
(192) |
proper#(U53(X)) |
→ |
proper#(X) |
(190) |
proper#(U71(X1,X2)) |
→ |
proper#(X1) |
(178) |
proper#(U21(X1,X2,X3)) |
→ |
proper#(X1) |
(179) |
proper#(U71(X1,X2)) |
→ |
proper#(X2) |
(280) |
proper#(U51(X1,X2,X3)) |
→ |
proper#(X2) |
(175) |
proper#(and(X1,X2)) |
→ |
proper#(X1) |
(173) |
proper#(U42(X1,X2)) |
→ |
proper#(X2) |
(169) |
proper#(U41(X1,X2,X3)) |
→ |
proper#(X3) |
(276) |
proper#(U52(X1,X2)) |
→ |
proper#(X2) |
(162) |
proper#(isQid(X)) |
→ |
proper#(X) |
(264) |
proper#(U61(X1,X2)) |
→ |
proper#(X1) |
(154) |
proper#(__(X1,X2)) |
→ |
proper#(X1) |
(155) |
proper#(U23(X)) |
→ |
proper#(X) |
(260) |
proper#(U51(X1,X2,X3)) |
→ |
proper#(X1) |
(150) |
proper#(U51(X1,X2,X3)) |
→ |
proper#(X3) |
(254) |
proper#(U11(X1,X2)) |
→ |
proper#(X1) |
(143) |
proper#(U41(X1,X2,X3)) |
→ |
proper#(X1) |
(253) |
could be deleted.
1.1.3.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
4th
component contains the
pair
U11#(mark(X1),X2) |
→ |
U11#(X1,X2) |
(230) |
U11#(ok(X1),ok(X2)) |
→ |
U11#(X1,X2) |
(327) |
1.1.4 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
5051 |
[isNeList(x1)] |
=
|
11129 |
[isPal(x1)] |
=
|
18048 |
[U42(x1, x2)] |
=
|
x2 + 1701 |
[u] |
=
|
20758 |
[U71(x1, x2)] |
=
|
1236 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
2 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
1522 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
2973 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 18683 |
[isQid(x1)] |
=
|
10610 |
[o] |
=
|
2021 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
3637 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
29362 |
[U62(x1)] |
=
|
2473 |
[mark(x1)] |
=
|
5052 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
x1 + 14182 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
2 |
[U52(x1, x2)] |
=
|
5051 |
[U61(x1, x2)] |
=
|
1935 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
16348 |
[U11#(x1, x2)] |
=
|
x2 + 0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
2453 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
1603 |
[U51(x1, x2, x3)] |
=
|
x1 + x2 + 30144 |
[isPalListKind(x1)] |
=
|
23480 |
[U53(x1)] |
=
|
5051 |
[U41(x1, x2, x3)] |
=
|
3202 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
3039 |
[U61#(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)) |
→ |
U11#(X1,X2) |
(327) |
could be deleted.
1.1.4.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
5th
component contains the
pair
U32#(ok(X)) |
→ |
U32#(X) |
(191) |
U32#(mark(X)) |
→ |
U32#(X) |
(180) |
1.1.5 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
x1 + 0 |
[U21(x1, x2, x3)] |
=
|
55994 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
10088 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
7531 |
[U42(x1, x2)] |
=
|
x2 + 13882 |
[u] |
=
|
4426 |
[U71(x1, x2)] |
=
|
16387 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
21560 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
41137 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
14429 |
[isNePal(x1)] |
=
|
x1 + 18769 |
[U72(x1)] |
=
|
30534 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 1 |
[isQid(x1)] |
=
|
10610 |
[o] |
=
|
32488 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 4563 |
[isList(x1)] |
=
|
3637 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
11620 |
[U62(x1)] |
=
|
27498 |
[mark(x1)] |
=
|
x1 + 27366 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
103 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
10966 |
[U52(x1, x2)] |
=
|
3870 |
[U61(x1, x2)] |
=
|
11776 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
41304 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
19143 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
5022 |
[U51(x1, x2, x3)] |
=
|
x1 + x2 + 61402 |
[isPalListKind(x1)] |
=
|
23480 |
[U53(x1)] |
=
|
0 |
[U41(x1, x2, x3)] |
=
|
28348 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U32#(ok(X)) |
→ |
U32#(X) |
(191) |
U32#(mark(X)) |
→ |
U32#(X) |
(180) |
could be deleted.
1.1.5.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
6th
component contains the
pair
U43#(mark(X)) |
→ |
U43#(X) |
(315) |
U43#(ok(X)) |
→ |
U43#(X) |
(301) |
1.1.6 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
84532 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
29062 |
[isNeList(x1)] |
=
|
8234 |
[isPal(x1)] |
=
|
7531 |
[U42(x1, x2)] |
=
|
x2 + 15745 |
[u] |
=
|
4426 |
[U71(x1, x2)] |
=
|
9543 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 10182 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
11765 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
x1 + 0 |
[U23(x1)] |
=
|
26837 |
[isNePal(x1)] |
=
|
x1 + 11414 |
[U72(x1)] |
=
|
11804 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 1 |
[isQid(x1)] |
=
|
10610 |
[o] |
=
|
32488 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 2658 |
[isList(x1)] |
=
|
3637 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
11620 |
[U62(x1)] |
=
|
1375 |
[mark(x1)] |
=
|
x1 + 2 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
26006 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
23611 |
[U52(x1, x2)] |
=
|
17267 |
[U61(x1, x2)] |
=
|
32354 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
7276 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
17842 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
534 |
[U51(x1, x2, x3)] |
=
|
x1 + x2 + 61402 |
[isPalListKind(x1)] |
=
|
23480 |
[U53(x1)] |
=
|
0 |
[U41(x1, x2, x3)] |
=
|
54426 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U43#(mark(X)) |
→ |
U43#(X) |
(315) |
U43#(ok(X)) |
→ |
U43#(X) |
(301) |
could be deleted.
1.1.6.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
7th
component contains the
pair
U41#(mark(X1),X2,X3) |
→ |
U41#(X1,X2,X3) |
(308) |
U41#(ok(X1),ok(X2),ok(X3)) |
→ |
U41#(X1,X2,X3) |
(170) |
1.1.7 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
84532 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
9395 |
[isPal(x1)] |
=
|
7531 |
[U42(x1, x2)] |
=
|
x2 + 2 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 2 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
2 |
[isNePal(x1)] |
=
|
x1 + 31389 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 21512 |
[isQid(x1)] |
=
|
10610 |
[o] |
=
|
22543 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
3637 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
12478 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 2 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
29329 |
[U52(x1, x2)] |
=
|
2 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
28072 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
2 |
[U41#(x1, x2, x3)] |
=
|
x3 + 0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
2 |
[U51(x1, x2, x3)] |
=
|
x1 + x2 + 33617 |
[isPalListKind(x1)] |
=
|
53807 |
[U53(x1)] |
=
|
0 |
[U41(x1, x2, x3)] |
=
|
2939 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
U41#(ok(X1),ok(X2),ok(X3)) |
→ |
U41#(X1,X2,X3) |
(170) |
could be deleted.
1.1.7.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
8th
component contains the
pair
U22#(mark(X1),X2) |
→ |
U22#(X1,X2) |
(215) |
U22#(ok(X1),ok(X2)) |
→ |
U22#(X1,X2) |
(302) |
1.1.8 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
1589 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
7397 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
7531 |
[U42(x1, x2)] |
=
|
x2 + 2 |
[u] |
=
|
54118 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 2 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
2 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 1 |
[isQid(x1)] |
=
|
10610 |
[o] |
=
|
41322 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 26933 |
[isList(x1)] |
=
|
3637 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
46556 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 8299 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
35394 |
[U52(x1, x2)] |
=
|
2 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
20045 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
2 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
x2 + 0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
2 |
[U51(x1, x2, x3)] |
=
|
x1 + x2 + 44534 |
[isPalListKind(x1)] |
=
|
29969 |
[U53(x1)] |
=
|
0 |
[U41(x1, x2, x3)] |
=
|
24601 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
U22#(ok(X1),ok(X2)) |
→ |
U22#(X1,X2) |
(302) |
could be deleted.
1.1.8.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
9th
component contains the
pair
isPal#(ok(X)) |
→ |
isPal#(X) |
(303) |
1.1.9 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
29976 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2215 |
[isNeList(x1)] |
=
|
16493 |
[isPal(x1)] |
=
|
7531 |
[U42(x1, x2)] |
=
|
x2 + 2 |
[u] |
=
|
4880 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 2 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
586 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
2 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
x1 + 0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 1 |
[isQid(x1)] |
=
|
15820 |
[o] |
=
|
8645 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 21782 |
[isList(x1)] |
=
|
3637 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
43393 |
[U62(x1)] |
=
|
26412 |
[mark(x1)] |
=
|
x1 + 8299 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
2079 |
[U52(x1, x2)] |
=
|
2 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
28869 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
2 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
2 |
[U51(x1, x2, x3)] |
=
|
x1 + x2 + 1 |
[isPalListKind(x1)] |
=
|
2 |
[U53(x1)] |
=
|
0 |
[U41(x1, x2, x3)] |
=
|
12147 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
isPal#(ok(X)) |
→ |
isPal#(X) |
(303) |
could be deleted.
1.1.9.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
10th
component contains the
pair
U21#(mark(X1),X2,X3) |
→ |
U21#(X1,X2,X3) |
(311) |
U21#(ok(X1),ok(X2),ok(X3)) |
→ |
U21#(X1,X2,X3) |
(171) |
1.1.10 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
23205 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
14318 |
[isNeList(x1)] |
=
|
9780 |
[isPal(x1)] |
=
|
7531 |
[U42(x1, x2)] |
=
|
x2 + 2 |
[u] |
=
|
55725 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 2 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
2 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
x1 + 1 |
[isQid(x1)] |
=
|
15820 |
[o] |
=
|
12039 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 7230 |
[isList(x1)] |
=
|
3637 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
24698 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 8299 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
19034 |
[U52(x1, x2)] |
=
|
2 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
6142 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
2 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
x2 + x3 + 0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
2 |
[U51(x1, x2, x3)] |
=
|
x1 + x2 + 1 |
[isPalListKind(x1)] |
=
|
2 |
[U53(x1)] |
=
|
0 |
[U41(x1, x2, x3)] |
=
|
2 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
U21#(ok(X1),ok(X2),ok(X3)) |
→ |
U21#(X1,X2,X3) |
(171) |
could be deleted.
1.1.10.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
11th
component contains the
pair
isNePal#(ok(X)) |
→ |
isNePal#(X) |
(188) |
1.1.11 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
x1 + 10249 |
[isPal(x1)] |
=
|
1 |
[U42(x1, x2)] |
=
|
2 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + 1 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 1 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
1 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 5 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
x1 + 0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
3 |
[mark(x1)] |
=
|
x1 + 2 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1, x2)] |
=
|
x2 + 2 |
[U61(x1, x2)] |
=
|
3 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
3 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 1 |
[U51(x1, x2, x3)] |
=
|
0 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
3 |
[U41(x1, x2, x3)] |
=
|
x2 + 2 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rule
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(119) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
isNePal#(ok(X)) |
→ |
isNePal#(X) |
(188) |
could be deleted.
1.1.11.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
12th
component contains the
pair
U42#(mark(X1),X2) |
→ |
U42#(X1,X2) |
(158) |
U42#(ok(X1),ok(X2)) |
→ |
U42#(X1,X2) |
(144) |
1.1.12 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
2 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
1 |
[U42(x1, x2)] |
=
|
2 |
[u] |
=
|
16277 |
[U71(x1, x2)] |
=
|
x1 + 1 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 18239 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
1 |
[o] |
=
|
11480 |
[U42#(x1, x2)] |
=
|
x1 + x2 + 0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
2 |
[U62(x1)] |
=
|
2930 |
[mark(x1)] |
=
|
x1 + 26121 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
2 |
[U52(x1, x2)] |
=
|
x2 + 31875 |
[U61(x1, x2)] |
=
|
3 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
2 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
3 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
2 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 1 |
[U51(x1, x2, x3)] |
=
|
0 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
3 |
[U41(x1, x2, x3)] |
=
|
x2 + 20034 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rule
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(119) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U42#(mark(X1),X2) |
→ |
U42#(X1,X2) |
(158) |
U42#(ok(X1),ok(X2)) |
→ |
U42#(X1,X2) |
(144) |
could be deleted.
1.1.12.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
13th
component contains the
pair
isPalListKind#(ok(X)) |
→ |
isPalListKind#(X) |
(298) |
1.1.13 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
x1 + 0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
x1 + 2436 |
[isPal(x1)] |
=
|
1 |
[U42(x1, x2)] |
=
|
2 |
[u] |
=
|
52347 |
[U71(x1, x2)] |
=
|
x1 + 9259 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 51837 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 1 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
1 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 4 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
3 |
[mark(x1)] |
=
|
x1 + 18177 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
59903 |
[U52(x1, x2)] |
=
|
x2 + 26864 |
[U61(x1, x2)] |
=
|
3 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
3 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
48992 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 26623 |
[U51(x1, x2, x3)] |
=
|
0 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
3 |
[U41(x1, x2, x3)] |
=
|
x2 + 17735 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 42040 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rule
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(119) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
isPalListKind#(ok(X)) |
→ |
isPalListKind#(X) |
(298) |
could be deleted.
1.1.13.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
14th
component contains the
pair
U31#(mark(X1),X2) |
→ |
U31#(X1,X2) |
(231) |
U31#(ok(X1),ok(X2)) |
→ |
U31#(X1,X2) |
(291) |
1.1.14 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
2 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
1 |
[U42(x1, x2)] |
=
|
2 |
[u] |
=
|
1191 |
[U71(x1, x2)] |
=
|
x1 + 1 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 1 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
1 |
[o] |
=
|
2 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
2 |
[U62(x1)] |
=
|
24574 |
[mark(x1)] |
=
|
x1 + 18177 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
2 |
[U52(x1, x2)] |
=
|
x2 + 8868 |
[U61(x1, x2)] |
=
|
3 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
2 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
3 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
4 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 26811 |
[U51(x1, x2, x3)] |
=
|
0 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
12607 |
[U41(x1, x2, x3)] |
=
|
x2 + 30857 |
[U31#(x1, x2)] |
=
|
x1 + x2 + 0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rule
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(119) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U31#(mark(X1),X2) |
→ |
U31#(X1,X2) |
(231) |
U31#(ok(X1),ok(X2)) |
→ |
U31#(X1,X2) |
(291) |
could be deleted.
1.1.14.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
15th
component contains the
pair
isQid#(ok(X)) |
→ |
isQid#(X) |
(255) |
1.1.15 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
1 |
[U42(x1, x2)] |
=
|
2 |
[u] |
=
|
2581 |
[U71(x1, x2)] |
=
|
x1 + 20562 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 18789 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 1 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
x1 + 15132 |
[isQid#(x1)] |
=
|
x1 + 0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
1 |
[o] |
=
|
2 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 3159 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
21968 |
[U62(x1)] |
=
|
26617 |
[mark(x1)] |
=
|
x1 + 28008 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
4540 |
[U52(x1, x2)] |
=
|
x2 + 8868 |
[U61(x1, x2)] |
=
|
3 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
2749 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
3 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
49240 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 8341 |
[U51(x1, x2, x3)] |
=
|
0 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
12607 |
[U41(x1, x2, x3)] |
=
|
x2 + 4268 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rule
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(119) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
isQid#(ok(X)) |
→ |
isQid#(X) |
(255) |
could be deleted.
1.1.15.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
16th
component contains the
pair
U52#(ok(X1),ok(X2)) |
→ |
U52#(X1,X2) |
(345) |
U52#(mark(X1),X2) |
→ |
U52#(X1,X2) |
(281) |
1.1.16 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
2 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
1 |
[U42(x1, x2)] |
=
|
2 |
[u] |
=
|
10759 |
[U71(x1, x2)] |
=
|
x1 + 30098 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 1 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
x1 + 10079 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
x1 + 0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
2 |
[o] |
=
|
2 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
2 |
[U62(x1)] |
=
|
22425 |
[mark(x1)] |
=
|
x1 + 19907 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
4540 |
[U52(x1, x2)] |
=
|
x2 + 989 |
[U61(x1, x2)] |
=
|
3 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
21359 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
7183 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
13667 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 1083 |
[U51(x1, x2, x3)] |
=
|
0 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
10710 |
[U41(x1, x2, x3)] |
=
|
x2 + 4268 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rule
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(119) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U52#(ok(X1),ok(X2)) |
→ |
U52#(X1,X2) |
(345) |
U52#(mark(X1),X2) |
→ |
U52#(X1,X2) |
(281) |
could be deleted.
1.1.16.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
17th
component contains the
pair
isNeList#(ok(X)) |
→ |
isNeList#(X) |
(217) |
1.1.17 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
2 |
[U42(x1, x2)] |
=
|
2 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + 30098 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 17594 |
[isNeList#(x1)] |
=
|
x1 + 0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 1 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
2 |
[o] |
=
|
27960 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 2 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
3 |
[mark(x1)] |
=
|
x1 + 4429 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
4540 |
[U52(x1, x2)] |
=
|
x2 + 4675 |
[U61(x1, x2)] |
=
|
3 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
38718 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
3 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
13667 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 13751 |
[U51(x1, x2, x3)] |
=
|
0 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
10710 |
[U41(x1, x2, x3)] |
=
|
x2 + 4268 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rule
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(119) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
isNeList#(ok(X)) |
→ |
isNeList#(X) |
(217) |
could be deleted.
1.1.17.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
18th
component contains the
pair
U72#(mark(X)) |
→ |
U72#(X) |
(241) |
U72#(ok(X)) |
→ |
U72#(X) |
(314) |
1.1.18 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
x1 + 0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
1 |
[U42(x1, x2)] |
=
|
2 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + 30098 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + x2 + 1837 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 18767 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
1 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 38 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
9513 |
[mark(x1)] |
=
|
x1 + 20414 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1, x2)] |
=
|
x2 + 24752 |
[U61(x1, x2)] |
=
|
11372 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
89 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
11749 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
x1 + x2 + 21861 |
[U51(x1, x2, x3)] |
=
|
0 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
2576 |
[U41(x1, x2, x3)] |
=
|
x2 + 33830 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rule
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(119) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U72#(mark(X)) |
→ |
U72#(X) |
(241) |
U72#(ok(X)) |
→ |
U72#(X) |
(314) |
could be deleted.
1.1.18.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
19th
component contains the
pair
and#(mark(X1),X2) |
→ |
and#(X1,X2) |
(206) |
and#(ok(X1),ok(X2)) |
→ |
and#(X1,X2) |
(198) |
1.1.19 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
x1 + 4461 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
1921 |
[isNeList(x1)] |
=
|
4 |
[isPal(x1)] |
=
|
2 |
[U42(x1, x2)] |
=
|
x1 + x2 + 5804 |
[u] |
=
|
2 |
[U71(x1, x2)] |
=
|
4 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
x1 + 2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 1301 |
[isNePal(x1)] |
=
|
4 |
[U72(x1)] |
=
|
3 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
3 |
[o] |
=
|
5383 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 44478 |
[isList(x1)] |
=
|
x1 + 52 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
2 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 9426 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
x1 + 1141 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
2485 |
[U52(x1, x2)] |
=
|
x1 + 9247 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
8783 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 1 |
[U31(x1, x2)] |
=
|
x1 + 1 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
10777 |
[U51(x1, x2, x3)] |
=
|
5 |
[isPalListKind(x1)] |
=
|
x1 + 642 |
[U53(x1)] |
=
|
3 |
[U41(x1, x2, x3)] |
=
|
x1 + 2065 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
x1 + x2 + 0 |
[__(x1, x2)] |
=
|
9424 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rules
isList(ok(X)) |
→ |
ok(isList(X)) |
(122) |
U23(mark(X)) |
→ |
mark(U23(X)) |
(70) |
U23(ok(X)) |
→ |
ok(U23(X)) |
(123) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
and#(mark(X1),X2) |
→ |
and#(X1,X2) |
(206) |
and#(ok(X1),ok(X2)) |
→ |
and#(X1,X2) |
(198) |
could be deleted.
1.1.19.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
20th
component contains the
pair
U12#(mark(X)) |
→ |
U12#(X) |
(234) |
U12#(ok(X)) |
→ |
U12#(X) |
(257) |
1.1.20 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
x1 + 1 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
2 |
[U42(x1, x2)] |
=
|
x1 + x2 + 1 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
x1 + 1 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 1 |
[isNePal(x1)] |
=
|
4 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
2 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
x1 + 0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 29398 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
x1 + 1 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
2 |
[U52(x1, x2)] |
=
|
x1 + 1 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 29395 |
[U31(x1, x2)] |
=
|
x1 + 1 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
2 |
[U51(x1, x2, x3)] |
=
|
5 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
2 |
[U41(x1, x2, x3)] |
=
|
x1 + 1 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rules
isList(ok(X)) |
→ |
ok(isList(X)) |
(122) |
U23(mark(X)) |
→ |
mark(U23(X)) |
(70) |
U23(ok(X)) |
→ |
ok(U23(X)) |
(123) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U12#(mark(X)) |
→ |
U12#(X) |
(234) |
U12#(ok(X)) |
→ |
U12#(X) |
(257) |
could be deleted.
1.1.20.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
21th
component contains the
pair
isList#(ok(X)) |
→ |
isList#(X) |
(333) |
1.1.21 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
x1 + 1 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
2 |
[U42(x1, x2)] |
=
|
x1 + x2 + 1 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
x1 + 1 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 1 |
[isNePal(x1)] |
=
|
4 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
2 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 18901 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 29398 |
[isList#(x1)] |
=
|
x1 + 0 |
[U32(x1)] |
=
|
x1 + 1 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1, x2)] |
=
|
x1 + 1 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 1 |
[U31(x1, x2)] |
=
|
x1 + 1 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
2 |
[U51(x1, x2, x3)] |
=
|
2 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
2 |
[U41(x1, x2, x3)] |
=
|
x1 + 1 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rules
isList(ok(X)) |
→ |
ok(isList(X)) |
(122) |
U23(mark(X)) |
→ |
mark(U23(X)) |
(70) |
U23(ok(X)) |
→ |
ok(U23(X)) |
(123) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
isList#(ok(X)) |
→ |
isList#(X) |
(333) |
could be deleted.
1.1.21.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
22th
component contains the
pair
U23#(mark(X)) |
→ |
U23#(X) |
(310) |
U23#(ok(X)) |
→ |
U23#(X) |
(147) |
1.1.22 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
8857 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
x1 + 1 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
2 |
[U42(x1, x2)] |
=
|
x1 + x2 + 20982 |
[u] |
=
|
3772 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
x1 + 1 |
[U23#(x1)] |
=
|
x1 + 0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 2809 |
[isNePal(x1)] |
=
|
4 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
2 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 6436 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 29398 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
x1 + 15483 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1, x2)] |
=
|
x1 + 1 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 1 |
[U31(x1, x2)] |
=
|
x1 + 1 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
2 |
[U51(x1, x2, x3)] |
=
|
2 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
2 |
[U41(x1, x2, x3)] |
=
|
x1 + 1 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rules
isList(ok(X)) |
→ |
ok(isList(X)) |
(122) |
U23(mark(X)) |
→ |
mark(U23(X)) |
(70) |
U23(ok(X)) |
→ |
ok(U23(X)) |
(123) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U23#(mark(X)) |
→ |
U23#(X) |
(310) |
U23#(ok(X)) |
→ |
U23#(X) |
(147) |
could be deleted.
1.1.22.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
23th
component contains the
pair
__#(X1,mark(X2)) |
→ |
__#(X1,X2) |
(289) |
__#(mark(X1),X2) |
→ |
__#(X1,X2) |
(287) |
__#(ok(X1),ok(X2)) |
→ |
__#(X1,X2) |
(151) |
1.1.23 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
x1 + 1 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
2 |
[U42(x1, x2)] |
=
|
x1 + x2 + 1 |
[u] |
=
|
2 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x2 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
x1 + 1 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
x2 + 0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
x1 + 2 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
2 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
x1 + 2 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 4 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
x1 + 1 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1, x2)] |
=
|
x1 + 1 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 1 |
[U31(x1, x2)] |
=
|
x1 + 1 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
2 |
[U51(x1, x2, x3)] |
=
|
2 |
[isPalListKind(x1)] |
=
|
x1 + 1 |
[U53(x1)] |
=
|
2 |
[U41(x1, x2, x3)] |
=
|
x1 + 4 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rules
isList(ok(X)) |
→ |
ok(isList(X)) |
(122) |
U23(mark(X)) |
→ |
mark(U23(X)) |
(70) |
U23(ok(X)) |
→ |
ok(U23(X)) |
(123) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
__#(X1,mark(X2)) |
→ |
__#(X1,X2) |
(289) |
__#(ok(X1),ok(X2)) |
→ |
__#(X1,X2) |
(151) |
could be deleted.
1.1.23.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
24th
component contains the
pair
U71#(ok(X1),ok(X2)) |
→ |
U71#(X1,X2) |
(330) |
U71#(mark(X1),X2) |
→ |
U71#(X1,X2) |
(283) |
1.1.24 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
11779 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
4 |
[isNeList(x1)] |
=
|
4 |
[isPal(x1)] |
=
|
2 |
[U42(x1, x2)] |
=
|
4 |
[u] |
=
|
2 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + 3349 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
2 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
2 |
[isNePal(x1)] |
=
|
2 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
3 |
[isQid(x1)] |
=
|
x1 + 11480 |
[o] |
=
|
1 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 31067 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
12715 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 17321 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1, x2)] |
=
|
4 |
[U61(x1, x2)] |
=
|
4 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 1 |
[U31(x1, x2)] |
=
|
3 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
x2 + 0 |
[U22(x1, x2)] |
=
|
3 |
[U51(x1, x2, x3)] |
=
|
4 |
[isPalListKind(x1)] |
=
|
2 |
[U53(x1)] |
=
|
x1 + 2 |
[U41(x1, x2, x3)] |
=
|
5 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
17319 |
[U61#(x1, x2)] |
=
|
0 |
together with the usable
rules
isQid(ok(X)) |
→ |
ok(isQid(X)) |
(126) |
and(ok(X1),ok(X2)) |
→ |
ok(and(X1,X2)) |
(138) |
and(mark(X1),X2) |
→ |
mark(and(X1,X2)) |
(83) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
U71#(ok(X1),ok(X2)) |
→ |
U71#(X1,X2) |
(330) |
could be deleted.
1.1.24.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
25th
component contains the
pair
U51#(ok(X1),ok(X2),ok(X3)) |
→ |
U51#(X1,X2,X3) |
(332) |
U51#(mark(X1),X2,X3) |
→ |
U51#(X1,X2,X3) |
(177) |
1.1.25 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
14805 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
11466 |
[isNeList(x1)] |
=
|
15782 |
[isPal(x1)] |
=
|
5232 |
[U42(x1, x2)] |
=
|
30471 |
[u] |
=
|
20882 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
13077 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
22370 |
[isNePal(x1)] |
=
|
x1 + 41884 |
[U72(x1)] |
=
|
4509 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
5503 |
[isQid(x1)] |
=
|
2517 |
[o] |
=
|
19719 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 509 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
13268 |
[mark(x1)] |
=
|
x1 + 20176 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
800 |
[U52(x1, x2)] |
=
|
15933 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
x3 + 0 |
[e] |
=
|
26283 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
3 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
12791 |
[U51(x1, x2, x3)] |
=
|
6265 |
[isPalListKind(x1)] |
=
|
2 |
[U53(x1)] |
=
|
x1 + 31382 |
[U41(x1, x2, x3)] |
=
|
28534 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
28386 |
[U61#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
U51#(ok(X1),ok(X2),ok(X3)) |
→ |
U51#(X1,X2,X3) |
(332) |
could be deleted.
1.1.25.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
26th
component contains the
pair
U53#(mark(X)) |
→ |
U53#(X) |
(235) |
U53#(ok(X)) |
→ |
U53#(X) |
(167) |
1.1.26 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
22711 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
20347 |
[isNeList(x1)] |
=
|
19912 |
[isPal(x1)] |
=
|
5232 |
[U42(x1, x2)] |
=
|
42897 |
[u] |
=
|
20882 |
[U71(x1, x2)] |
=
|
13848 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
25045 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
x1 + 0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
36521 |
[isNePal(x1)] |
=
|
x1 + 29015 |
[U72(x1)] |
=
|
10589 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2391 |
[isQid(x1)] |
=
|
2 |
[o] |
=
|
28154 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 574 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[U62(x1)] |
=
|
29610 |
[mark(x1)] |
=
|
x1 + 30325 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
19746 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
42881 |
[U52(x1, x2)] |
=
|
2952 |
[U61(x1, x2)] |
=
|
28001 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
11143 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
2 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
32216 |
[U51(x1, x2, x3)] |
=
|
14272 |
[isPalListKind(x1)] |
=
|
12815 |
[U53(x1)] |
=
|
x1 + 32060 |
[U41(x1, x2, x3)] |
=
|
35811 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
5840 |
[U61#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U53#(mark(X)) |
→ |
U53#(X) |
(235) |
U53#(ok(X)) |
→ |
U53#(X) |
(167) |
could be deleted.
1.1.26.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
27th
component contains the
pair
U61#(mark(X1),X2) |
→ |
U61#(X1,X2) |
(309) |
U61#(ok(X1),ok(X2)) |
→ |
U61#(X1,X2) |
(307) |
1.1.27 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
2 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
2 |
[isNeList(x1)] |
=
|
31878 |
[isPal(x1)] |
=
|
5232 |
[U42(x1, x2)] |
=
|
42897 |
[u] |
=
|
19048 |
[U71(x1, x2)] |
=
|
7949 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + 18847 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
25045 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
26530 |
[isNePal(x1)] |
=
|
x1 + 49527 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
2 |
[isQid(x1)] |
=
|
32280 |
[o] |
=
|
9430 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
0 |
[ok(x1)] |
=
|
x1 + 2408 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
27977 |
[U62(x1)] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 30325 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
21837 |
[U52(x1, x2)] |
=
|
31469 |
[U61(x1, x2)] |
=
|
2 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
37300 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
2 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
24855 |
[U51(x1, x2, x3)] |
=
|
2 |
[isPalListKind(x1)] |
=
|
18015 |
[U53(x1)] |
=
|
x1 + 1 |
[U41(x1, x2, x3)] |
=
|
12396 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
x1 + 0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U61#(mark(X1),X2) |
→ |
U61#(X1,X2) |
(309) |
U61#(ok(X1),ok(X2)) |
→ |
U61#(X1,X2) |
(307) |
could be deleted.
1.1.27.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
28th
component contains the
pair
U62#(mark(X)) |
→ |
U62#(X) |
(326) |
U62#(ok(X)) |
→ |
U62#(X) |
(282) |
1.1.28 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U32#(x1)] |
=
|
0 |
[U21(x1, x2, x3)] |
=
|
8809 |
[isPalListKind#(x1)] |
=
|
0 |
[U11(x1, x2)] |
=
|
3918 |
[isNeList(x1)] |
=
|
31878 |
[isPal(x1)] |
=
|
5232 |
[U42(x1, x2)] |
=
|
66638 |
[u] |
=
|
19048 |
[U71(x1, x2)] |
=
|
19207 |
[top(x1)] |
=
|
0 |
[and(x1, x2)] |
=
|
x1 + 1 |
[isNeList#(x1)] |
=
|
0 |
[U43(x1)] |
=
|
10033 |
[U23#(x1)] |
=
|
0 |
[U53#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[U43#(x1)] |
=
|
0 |
[U23(x1)] |
=
|
16167 |
[isNePal(x1)] |
=
|
x1 + 49527 |
[U72(x1)] |
=
|
8854 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1, x2)] |
=
|
0 |
[U12(x1)] |
=
|
9283 |
[isQid(x1)] |
=
|
2 |
[o] |
=
|
9430 |
[U42#(x1, x2)] |
=
|
0 |
[U12#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[U62#(x1)] |
=
|
x1 + 0 |
[ok(x1)] |
=
|
x1 + 20490 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
33763 |
[U62(x1)] |
=
|
10183 |
[mark(x1)] |
=
|
x1 + 30325 |
[isList#(x1)] |
=
|
0 |
[U32(x1)] |
=
|
2 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
377 |
[U52(x1, x2)] |
=
|
6093 |
[U61(x1, x2)] |
=
|
13199 |
[U51#(x1, x2, x3)] |
=
|
0 |
[e] |
=
|
37300 |
[U11#(x1, x2)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1, x2)] |
=
|
10541 |
[U41#(x1, x2, x3)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2, x3)] |
=
|
0 |
[U22#(x1, x2)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1, x2)] |
=
|
16790 |
[U51(x1, x2, x3)] |
=
|
20672 |
[isPalListKind(x1)] |
=
|
3455 |
[U53(x1)] |
=
|
x1 + 32312 |
[U41(x1, x2, x3)] |
=
|
17942 |
[U31#(x1, x2)] |
=
|
0 |
[and#(x1, x2)] |
=
|
0 |
[__(x1, x2)] |
=
|
2 |
[U61#(x1, x2)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U62#(mark(X)) |
→ |
U62#(X) |
(326) |
U62#(ok(X)) |
→ |
U62#(X) |
(282) |
could be deleted.
1.1.28.1 Dependency Graph Processor
The dependency pairs are split into 0
components.