The rewrite relation of the following TRS is considered.
There are 101 ruless (increase limit for explicit display).
There are 154 ruless (increase limit for explicit display).
The dependency pairs are split into 19
components.
-
The
1st
component contains the
pair
mark#(U22(X)) |
→ |
active#(U22(mark(X))) |
(185) |
active#(U21(tt,V2)) |
→ |
mark#(U22(isList(V2))) |
(252) |
mark#(isPal(X)) |
→ |
active#(isPal(X)) |
(184) |
mark#(U81(X)) |
→ |
mark#(X) |
(181) |
mark#(U11(X)) |
→ |
mark#(X) |
(249) |
mark#(U72(X)) |
→ |
mark#(X) |
(178) |
active#(U41(tt,V2)) |
→ |
mark#(U42(isNeList(V2))) |
(248) |
mark#(U51(X1,X2)) |
→ |
active#(U51(mark(X1),X2)) |
(247) |
active#(isNeList(__(V1,V2))) |
→ |
mark#(U51(isNeList(V1),V2)) |
(175) |
active#(isPal(V)) |
→ |
mark#(U81(isNePal(V))) |
(173) |
mark#(U72(X)) |
→ |
active#(U72(mark(X))) |
(170) |
active#(__(__(X,Y),Z)) |
→ |
mark#(__(X,__(Y,Z))) |
(245) |
active#(isList(__(V1,V2))) |
→ |
mark#(U21(isList(V1),V2)) |
(244) |
active#(__(X,nil)) |
→ |
mark#(X) |
(239) |
mark#(U52(X)) |
→ |
active#(U52(mark(X))) |
(237) |
mark#(U61(X)) |
→ |
mark#(X) |
(156) |
active#(U51(tt,V2)) |
→ |
mark#(U52(isList(V2))) |
(157) |
active#(isNeList(V)) |
→ |
mark#(U31(isQid(V))) |
(231) |
mark#(U11(X)) |
→ |
active#(U11(mark(X))) |
(229) |
mark#(U21(X1,X2)) |
→ |
mark#(X1) |
(151) |
mark#(U61(X)) |
→ |
active#(U61(mark(X))) |
(148) |
mark#(isNeList(X)) |
→ |
active#(isNeList(X)) |
(222) |
mark#(U51(X1,X2)) |
→ |
mark#(X1) |
(220) |
mark#(U71(X1,X2)) |
→ |
mark#(X1) |
(144) |
mark#(U22(X)) |
→ |
mark#(X) |
(142) |
active#(isNePal(__(I,__(P,I)))) |
→ |
mark#(U71(isQid(I),P)) |
(218) |
mark#(isNePal(X)) |
→ |
active#(isNePal(X)) |
(136) |
mark#(isQid(X)) |
→ |
active#(isQid(X)) |
(211) |
active#(isNePal(V)) |
→ |
mark#(U61(isQid(V))) |
(129) |
mark#(__(X1,X2)) |
→ |
mark#(X1) |
(130) |
mark#(__(X1,X2)) |
→ |
mark#(X2) |
(128) |
active#(__(nil,X)) |
→ |
mark#(X) |
(125) |
mark#(U81(X)) |
→ |
active#(U81(mark(X))) |
(207) |
mark#(U71(X1,X2)) |
→ |
active#(U71(mark(X1),X2)) |
(205) |
active#(U71(tt,P)) |
→ |
mark#(U72(isPal(P))) |
(121) |
mark#(U42(X)) |
→ |
mark#(X) |
(204) |
mark#(U41(X1,X2)) |
→ |
active#(U41(mark(X1),X2)) |
(119) |
mark#(U52(X)) |
→ |
mark#(X) |
(203) |
mark#(__(X1,X2)) |
→ |
active#(__(mark(X1),mark(X2))) |
(201) |
mark#(U31(X)) |
→ |
mark#(X) |
(115) |
mark#(U41(X1,X2)) |
→ |
mark#(X1) |
(198) |
mark#(U42(X)) |
→ |
active#(U42(mark(X))) |
(110) |
active#(isList(V)) |
→ |
mark#(U11(isNeList(V))) |
(194) |
mark#(U21(X1,X2)) |
→ |
active#(U21(mark(X1),X2)) |
(191) |
mark#(U31(X)) |
→ |
active#(U31(mark(X))) |
(106) |
active#(isNeList(__(V1,V2))) |
→ |
mark#(U41(isList(V1),V2)) |
(103) |
mark#(isList(X)) |
→ |
active#(isList(X)) |
(188) |
1.1.1 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
283 |
[U11(x1)] |
=
|
118 |
[isNeList(x1)] |
=
|
283 |
[isPal(x1)] |
=
|
283 |
[U42(x1)] |
=
|
245 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
283 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
283 |
[U72(x1)] |
=
|
138 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
282 |
[o] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
283 |
[isList(x1)] |
=
|
283 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
267 |
[U61(x1)] |
=
|
196 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
0 |
[U31(x1)] |
=
|
224 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
x1 + 0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
128 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
131 |
[U51(x1, x2)] |
=
|
283 |
[U41(x1, x2)] |
=
|
283 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
283 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
U51(mark(X1),X2) |
→ |
U51(X1,X2) |
(80) |
U42(active(X)) |
→ |
U42(X) |
(77) |
isList(mark(X)) |
→ |
isList(X) |
(68) |
U52(active(X)) |
→ |
U52(X) |
(85) |
isNePal(mark(X)) |
→ |
isNePal(X) |
(100) |
U21(X1,mark(X2)) |
→ |
U21(X1,X2) |
(63) |
U11(mark(X)) |
→ |
U11(X) |
(60) |
U61(active(X)) |
→ |
U61(X) |
(87) |
U52(mark(X)) |
→ |
U52(X) |
(84) |
U21(X1,active(X2)) |
→ |
U21(X1,X2) |
(65) |
U41(mark(X1),X2) |
→ |
U41(X1,X2) |
(72) |
U21(active(X1),X2) |
→ |
U21(X1,X2) |
(64) |
U72(active(X)) |
→ |
U72(X) |
(93) |
U72(mark(X)) |
→ |
U72(X) |
(92) |
U71(mark(X1),X2) |
→ |
U71(X1,X2) |
(88) |
U21(mark(X1),X2) |
→ |
U21(X1,X2) |
(62) |
U51(active(X1),X2) |
→ |
U51(X1,X2) |
(82) |
U71(X1,mark(X2)) |
→ |
U71(X1,X2) |
(89) |
__(mark(X1),X2) |
→ |
__(X1,X2) |
(56) |
isNeList(active(X)) |
→ |
isNeList(X) |
(79) |
isNePal(active(X)) |
→ |
isNePal(X) |
(101) |
isList(active(X)) |
→ |
isList(X) |
(69) |
U81(mark(X)) |
→ |
U81(X) |
(96) |
isNeList(mark(X)) |
→ |
isNeList(X) |
(78) |
U51(X1,mark(X2)) |
→ |
U51(X1,X2) |
(81) |
U31(mark(X)) |
→ |
U31(X) |
(70) |
isPal(mark(X)) |
→ |
isPal(X) |
(94) |
U42(mark(X)) |
→ |
U42(X) |
(76) |
__(X1,mark(X2)) |
→ |
__(X1,X2) |
(57) |
isQid(mark(X)) |
→ |
isQid(X) |
(98) |
U71(active(X1),X2) |
→ |
U71(X1,X2) |
(90) |
U22(active(X)) |
→ |
U22(X) |
(67) |
__(X1,active(X2)) |
→ |
__(X1,X2) |
(59) |
U11(active(X)) |
→ |
U11(X) |
(61) |
__(active(X1),X2) |
→ |
__(X1,X2) |
(58) |
U41(active(X1),X2) |
→ |
U41(X1,X2) |
(74) |
U41(X1,active(X2)) |
→ |
U41(X1,X2) |
(75) |
U31(active(X)) |
→ |
U31(X) |
(71) |
U41(X1,mark(X2)) |
→ |
U41(X1,X2) |
(73) |
U71(X1,active(X2)) |
→ |
U71(X1,X2) |
(91) |
U81(active(X)) |
→ |
U81(X) |
(97) |
isQid(active(X)) |
→ |
isQid(X) |
(99) |
isPal(active(X)) |
→ |
isPal(X) |
(95) |
U22(mark(X)) |
→ |
U22(X) |
(66) |
U51(X1,active(X2)) |
→ |
U51(X1,X2) |
(83) |
U61(mark(X)) |
→ |
U61(X) |
(86) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
mark#(U22(X)) |
→ |
active#(U22(mark(X))) |
(185) |
mark#(U72(X)) |
→ |
active#(U72(mark(X))) |
(170) |
mark#(U52(X)) |
→ |
active#(U52(mark(X))) |
(237) |
mark#(U11(X)) |
→ |
active#(U11(mark(X))) |
(229) |
mark#(U61(X)) |
→ |
active#(U61(mark(X))) |
(148) |
mark#(isQid(X)) |
→ |
active#(isQid(X)) |
(211) |
mark#(U81(X)) |
→ |
active#(U81(mark(X))) |
(207) |
mark#(U42(X)) |
→ |
active#(U42(mark(X))) |
(110) |
mark#(U31(X)) |
→ |
active#(U31(mark(X))) |
(106) |
could be deleted.
1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
2nd
component contains the
pair
U72#(active(X)) |
→ |
U72#(X) |
(153) |
U72#(mark(X)) |
→ |
U72#(X) |
(118) |
1.1.2 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
900 |
[U72#(x1)] |
=
|
x1 + 0 |
[U21(x1, x2)] |
=
|
x1 + 19505 |
[U11(x1)] |
=
|
x1 + 3590 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
3012 |
[U42(x1)] |
=
|
3708 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 6 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 4 |
[U72(x1)] |
=
|
463 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
0 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
x1 + 3589 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
936 |
[U52(x1)] |
=
|
x1 + 11 |
[U61(x1)] |
=
|
x1 + 5 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
x1 + 13705 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 3010 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
3593 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 19511 |
[U51(x1, x2)] |
=
|
x1 + x2 + 5 |
[U41(x1, x2)] |
=
|
x1 + x2 + 113 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isPal(mark(X)) |
→ |
isPal(X) |
(94) |
isPal(active(X)) |
→ |
isPal(X) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U72#(active(X)) |
→ |
U72#(X) |
(153) |
U72#(mark(X)) |
→ |
U72#(X) |
(118) |
could be deleted.
1.1.2.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
3rd
component contains the
pair
isPal#(active(X)) |
→ |
isPal#(X) |
(255) |
isPal#(mark(X)) |
→ |
isPal#(X) |
(143) |
1.1.3 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + 11251 |
[U11(x1)] |
=
|
x1 + 7362 |
[isNeList(x1)] |
=
|
x1 + 2 |
[isPal(x1)] |
=
|
1 |
[U42(x1)] |
=
|
10 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 3 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
x1 + 0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
0 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
x1 + 17580 |
[U61(x1)] |
=
|
x1 + 2 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
x1 + 3 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 2 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
4 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 19511 |
[U51(x1, x2)] |
=
|
x1 + x2 + 17575 |
[U41(x1, x2)] |
=
|
x1 + x2 + 4 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isPal(mark(X)) |
→ |
isPal(X) |
(94) |
isPal(active(X)) |
→ |
isPal(X) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
isPal#(active(X)) |
→ |
isPal#(X) |
(255) |
isPal#(mark(X)) |
→ |
isPal#(X) |
(143) |
could be deleted.
1.1.3.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
4th
component contains the
pair
isNePal#(active(X)) |
→ |
isNePal#(X) |
(160) |
isNePal#(mark(X)) |
→ |
isNePal#(X) |
(209) |
1.1.4 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + 925 |
[U11(x1)] |
=
|
x1 + 405 |
[isNeList(x1)] |
=
|
x1 + 732 |
[isPal(x1)] |
=
|
1185 |
[U42(x1)] |
=
|
4779 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 1353 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 1914 |
[U72(x1)] |
=
|
655 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1486 |
[o] |
=
|
0 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
x1 + 213 |
[isNePal#(x1)] |
=
|
x1 + 0 |
[nil] |
=
|
1274 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
x1 + 4047 |
[U61(x1)] |
=
|
x1 + 1352 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 924 |
[U31(x1)] |
=
|
x1 + 170 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 195 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
2411 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 11257 |
[U51(x1, x2)] |
=
|
x1 + x2 + 925 |
[U41(x1, x2)] |
=
|
x1 + x2 + 1444 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isPal(mark(X)) |
→ |
isPal(X) |
(94) |
isPal(active(X)) |
→ |
isPal(X) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
isNePal#(active(X)) |
→ |
isNePal#(X) |
(160) |
isNePal#(mark(X)) |
→ |
isNePal#(X) |
(209) |
could be deleted.
1.1.4.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
5th
component contains the
pair
U81#(mark(X)) |
→ |
U81#(X) |
(232) |
U81#(active(X)) |
→ |
U81#(X) |
(208) |
1.1.5 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + 21953 |
[U11(x1)] |
=
|
x1 + 967 |
[isNeList(x1)] |
=
|
x1 + 1629 |
[isPal(x1)] |
=
|
2 |
[U42(x1)] |
=
|
23365 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 5753 |
[U81#(x1)] |
=
|
x1 + 0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 5751 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
0 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
x1 + 8 |
[U61(x1)] |
=
|
x1 + 5752 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
x1 + 1630 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 21541 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
4 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 21958 |
[U51(x1, x2)] |
=
|
x1 + x2 + 3 |
[U41(x1, x2)] |
=
|
x1 + x2 + 1631 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isPal(mark(X)) |
→ |
isPal(X) |
(94) |
isPal(active(X)) |
→ |
isPal(X) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U81#(mark(X)) |
→ |
U81#(X) |
(232) |
U81#(active(X)) |
→ |
U81#(X) |
(208) |
could be deleted.
1.1.5.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
6th
component contains the
pair
U52#(active(X)) |
→ |
U52#(X) |
(162) |
U52#(mark(X)) |
→ |
U52#(X) |
(138) |
1.1.6 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
37351 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + 24636 |
[U11(x1)] |
=
|
x1 + 20178 |
[isNeList(x1)] |
=
|
x1 + 29993 |
[isPal(x1)] |
=
|
17065 |
[U42(x1)] |
=
|
60933 |
[u] |
=
|
13963 |
[U71(x1, x2)] |
=
|
x1 + x2 + 14432 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 2 |
[U72(x1)] |
=
|
30383 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
x1 + 0 |
[isQid(x1)] |
=
|
x1 + 1304 |
[o] |
=
|
0 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
x1 + 7722 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
30933 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
12063 |
[U52(x1)] |
=
|
x1 + 46958 |
[U61(x1)] |
=
|
x1 + 9501 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
37351 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
x1 + 28691 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 17065 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
38657 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 55573 |
[U51(x1, x2)] |
=
|
x1 + x2 + 16021 |
[U41(x1, x2)] |
=
|
x1 + x2 + 22274 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isPal(mark(X)) |
→ |
isPal(X) |
(94) |
isPal(active(X)) |
→ |
isPal(X) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U52#(active(X)) |
→ |
U52#(X) |
(162) |
U52#(mark(X)) |
→ |
U52#(X) |
(138) |
could be deleted.
1.1.6.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
7th
component contains the
pair
U71#(mark(X1),X2) |
→ |
U71#(X1,X2) |
(174) |
U71#(active(X1),X2) |
→ |
U71#(X1,X2) |
(166) |
U71#(X1,mark(X2)) |
→ |
U71#(X1,X2) |
(165) |
U71#(X1,active(X2)) |
→ |
U71#(X1,X2) |
(161) |
1.1.7 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + 23810 |
[U11(x1)] |
=
|
x1 + 9299 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
1 |
[U42(x1)] |
=
|
24368 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 28474 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
0 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
x1 + 8 |
[U61(x1)] |
=
|
x1 + 9501 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
x1 + 23033 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 2 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
4 |
[U71#(x1, x2)] |
=
|
x1 + 0 |
[U22(x1)] |
=
|
x1 + 42512 |
[U51(x1, x2)] |
=
|
x1 + x2 + 3 |
[U41(x1, x2)] |
=
|
x1 + x2 + 24362 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isPal(mark(X)) |
→ |
isPal(X) |
(94) |
isPal(active(X)) |
→ |
isPal(X) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U71#(mark(X1),X2) |
→ |
U71#(X1,X2) |
(174) |
U71#(active(X1),X2) |
→ |
U71#(X1,X2) |
(166) |
could be deleted.
1.1.7.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
8th
component contains the
pair
U31#(mark(X)) |
→ |
U31#(X) |
(140) |
U31#(active(X)) |
→ |
U31#(X) |
(213) |
1.1.8 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + 19073 |
[U11(x1)] |
=
|
x1 + 16546 |
[isNeList(x1)] |
=
|
x1 + 1682 |
[isPal(x1)] |
=
|
1 |
[U42(x1)] |
=
|
1691 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 5969 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
0 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
x1 + 0 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
x1 + 21661 |
[U61(x1)] |
=
|
x1 + 2 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
x1 + 15808 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 31223 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
4 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
50686 |
[U51(x1, x2)] |
=
|
x1 + x2 + 8197 |
[U41(x1, x2)] |
=
|
x1 + x2 + 1685 |
[U31#(x1)] |
=
|
x1 + 0 |
[__(x1, x2)] |
=
|
1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isPal(mark(X)) |
→ |
isPal(X) |
(94) |
isPal(active(X)) |
→ |
isPal(X) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U31#(mark(X)) |
→ |
U31#(X) |
(140) |
U31#(active(X)) |
→ |
U31#(X) |
(213) |
could be deleted.
1.1.8.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
9th
component contains the
pair
isQid#(mark(X)) |
→ |
isQid#(X) |
(182) |
isQid#(active(X)) |
→ |
isQid#(X) |
(235) |
1.1.9 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x2 + 18311 |
[U11(x1)] |
=
|
x1 + 18308 |
[isNeList(x1)] |
=
|
x1 + 2 |
[isPal(x1)] |
=
|
16844 |
[U42(x1)] |
=
|
25751 |
[u] |
=
|
31594 |
[U71(x1, x2)] |
=
|
x1 + 19208 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 6338 |
[U72(x1)] |
=
|
17271 |
[isQid#(x1)] |
=
|
x1 + 0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
6 |
[o] |
=
|
8924 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
x1 + 5436 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
25751 |
[U61(x1)] |
=
|
x1 + 19206 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
54370 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 12874 |
[U31(x1)] |
=
|
12876 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 23380 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
38625 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 25749 |
[U51(x1, x2)] |
=
|
12877 |
[U41(x1, x2)] |
=
|
12877 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
U31(mark(X)) |
→ |
U31(X) |
(70) |
U31(active(X)) |
→ |
U31(X) |
(71) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
isQid#(mark(X)) |
→ |
isQid#(X) |
(182) |
isQid#(active(X)) |
→ |
isQid#(X) |
(235) |
could be deleted.
1.1.9.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
10th
component contains the
pair
U51#(active(X1),X2) |
→ |
U51#(X1,X2) |
(172) |
U51#(X1,mark(X2)) |
→ |
U51#(X1,X2) |
(225) |
U51#(mark(X1),X2) |
→ |
U51#(X1,X2) |
(217) |
U51#(X1,active(X2)) |
→ |
U51#(X1,X2) |
(195) |
1.1.10 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
72857 |
[U11(x1)] |
=
|
x1 + 20350 |
[isNeList(x1)] |
=
|
52507 |
[isPal(x1)] |
=
|
x1 + 10470 |
[U42(x1)] |
=
|
x1 + 61310 |
[u] |
=
|
30545 |
[U71(x1, x2)] |
=
|
x1 + x2 + 4025 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 4581 |
[U72(x1)] |
=
|
x1 + 100502 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
14167 |
[o] |
=
|
29345 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
59247 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
34832 |
[U52(x1)] |
=
|
79727 |
[U61(x1)] |
=
|
x1 + 30998 |
[U51#(x1, x2)] |
=
|
x1 + x2 + 0 |
[e] |
=
|
34638 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 13610 |
[U31(x1)] |
=
|
66117 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 19499 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
93337 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 27220 |
[U51(x1, x2)] |
=
|
x2 + 66117 |
[U41(x1, x2)] |
=
|
x1 + x2 + 6870 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isNeList(active(X)) |
→ |
isNeList(X) |
(79) |
isNeList(mark(X)) |
→ |
isNeList(X) |
(78) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U51#(active(X1),X2) |
→ |
U51#(X1,X2) |
(172) |
U51#(X1,mark(X2)) |
→ |
U51#(X1,X2) |
(225) |
U51#(mark(X1),X2) |
→ |
U51#(X1,X2) |
(217) |
U51#(X1,active(X2)) |
→ |
U51#(X1,X2) |
(195) |
could be deleted.
1.1.10.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
11th
component contains the
pair
U41#(mark(X1),X2) |
→ |
U41#(X1,X2) |
(250) |
U41#(X1,active(X2)) |
→ |
U41#(X1,X2) |
(171) |
U41#(X1,mark(X2)) |
→ |
U41#(X1,X2) |
(158) |
U41#(active(X1),X2) |
→ |
U41#(X1,X2) |
(221) |
1.1.11 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
5530 |
[U11(x1)] |
=
|
x1 + 5529 |
[isNeList(x1)] |
=
|
1 |
[isPal(x1)] |
=
|
x1 + 6245 |
[U42(x1)] |
=
|
x1 + 106948 |
[u] |
=
|
30545 |
[U71(x1, x2)] |
=
|
x1 + x2 + 39899 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 36199 |
[U72(x1)] |
=
|
x1 + 54739 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
1572 |
[o] |
=
|
29345 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
259 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
934 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
10543 |
[U61(x1)] |
=
|
x1 + 39898 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
56444 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 5271 |
[U31(x1)] |
=
|
5272 |
[U41#(x1, x2)] |
=
|
x1 + 0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 77524 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
15814 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 10542 |
[U51(x1, x2)] |
=
|
x2 + 5272 |
[U41(x1, x2)] |
=
|
x1 + x2 + 5013 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isNeList(active(X)) |
→ |
isNeList(X) |
(79) |
isNeList(mark(X)) |
→ |
isNeList(X) |
(78) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U41#(mark(X1),X2) |
→ |
U41#(X1,X2) |
(250) |
U41#(active(X1),X2) |
→ |
U41#(X1,X2) |
(221) |
could be deleted.
1.1.11.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
12th
component contains the
pair
U11#(active(X)) |
→ |
U11#(X) |
(210) |
U11#(mark(X)) |
→ |
U11#(X) |
(197) |
1.1.12 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
52788 |
[U11(x1)] |
=
|
x1 + 1 |
[isNeList(x1)] |
=
|
21894 |
[isPal(x1)] |
=
|
x1 + 17468 |
[U42(x1)] |
=
|
x1 + 11 |
[u] |
=
|
7758 |
[U71(x1, x2)] |
=
|
x1 + x2 + 53 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 476 |
[U72(x1)] |
=
|
x1 + 4487 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
426 |
[o] |
=
|
6753 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
21893 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
50450 |
[U52(x1)] |
=
|
21898 |
[U61(x1)] |
=
|
x1 + 18324 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
29324 |
[U11#(x1)] |
=
|
x1 + 0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
21896 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 16994 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
21900 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 30897 |
[U51(x1, x2)] |
=
|
x2 + 21896 |
[U41(x1, x2)] |
=
|
x1 + x2 + 3 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isNeList(active(X)) |
→ |
isNeList(X) |
(79) |
isNeList(mark(X)) |
→ |
isNeList(X) |
(78) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U11#(active(X)) |
→ |
U11#(X) |
(210) |
U11#(mark(X)) |
→ |
U11#(X) |
(197) |
could be deleted.
1.1.12.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
13th
component contains the
pair
U61#(active(X)) |
→ |
U61#(X) |
(219) |
U61#(mark(X)) |
→ |
U61#(X) |
(102) |
1.1.13 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
8910 |
[U11(x1)] |
=
|
x1 + 8296 |
[isNeList(x1)] |
=
|
3736 |
[isPal(x1)] |
=
|
x1 + 3739 |
[U42(x1)] |
=
|
x1 + 3745 |
[u] |
=
|
17957 |
[U71(x1, x2)] |
=
|
x1 + x2 + 2 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
x1 + 7 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
2 |
[o] |
=
|
29267 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
38208 |
[U52(x1)] |
=
|
3740 |
[U61(x1)] |
=
|
x1 + 21955 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
33272 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
3738 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 3740 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
3742 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 8911 |
[U51(x1, x2)] |
=
|
x2 + 3738 |
[U41(x1, x2)] |
=
|
x1 + x2 + 3737 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 1 |
[U61#(x1)] |
=
|
x1 + 0 |
together with the usable
rules
isNeList(active(X)) |
→ |
isNeList(X) |
(79) |
isNeList(mark(X)) |
→ |
isNeList(X) |
(78) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U61#(active(X)) |
→ |
U61#(X) |
(219) |
U61#(mark(X)) |
→ |
U61#(X) |
(102) |
could be deleted.
1.1.13.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
14th
component contains the
pair
__#(mark(X1),X2) |
→ |
__#(X1,X2) |
(238) |
__#(X1,mark(X2)) |
→ |
__#(X1,X2) |
(122) |
__#(active(X1),X2) |
→ |
__#(X1,X2) |
(200) |
__#(X1,active(X2)) |
→ |
__#(X1,X2) |
(192) |
1.1.14 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
2653 |
[U11(x1)] |
=
|
x1 + 2 |
[isNeList(x1)] |
=
|
1 |
[isPal(x1)] |
=
|
x1 + 1 |
[U42(x1)] |
=
|
x1 + 10 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 7164 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
x2 + 0 |
[isNePal(x1)] |
=
|
x1 + 2 |
[U72(x1)] |
=
|
x1 + 7172 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
1 |
[o] |
=
|
21587 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
5 |
[U61(x1)] |
=
|
x1 + 3 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
3 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 3740 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
7 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 2654 |
[U51(x1, x2)] |
=
|
x2 + 3 |
[U41(x1, x2)] |
=
|
x1 + x2 + 2 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isNeList(active(X)) |
→ |
isNeList(X) |
(79) |
isNeList(mark(X)) |
→ |
isNeList(X) |
(78) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
__#(X1,mark(X2)) |
→ |
__#(X1,X2) |
(122) |
__#(X1,active(X2)) |
→ |
__#(X1,X2) |
(192) |
could be deleted.
1.1.14.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
15th
component contains the
pair
U22#(mark(X)) |
→ |
U22#(X) |
(152) |
U22#(active(X)) |
→ |
U22#(X) |
(114) |
1.1.15 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
32783 |
[U11(x1)] |
=
|
x1 + 2 |
[isNeList(x1)] |
=
|
32781 |
[isPal(x1)] |
=
|
x1 + 7506 |
[U42(x1)] |
=
|
x1 + 10 |
[u] |
=
|
15500 |
[U71(x1, x2)] |
=
|
x1 + x2 + 1 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 5319 |
[U72(x1)] |
=
|
x1 + 25284 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
5321 |
[o] |
=
|
23986 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
32781 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
18888 |
[U52(x1)] |
=
|
32785 |
[U61(x1)] |
=
|
x1 + 24066 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
12394 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
32783 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 2189 |
[U22#(x1)] |
=
|
x1 + 0 |
[tt] |
=
|
32787 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 21290 |
[U51(x1, x2)] |
=
|
x2 + 32783 |
[U41(x1, x2)] |
=
|
x1 + x2 + 2 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isNeList(active(X)) |
→ |
isNeList(X) |
(79) |
isNeList(mark(X)) |
→ |
isNeList(X) |
(78) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U22#(mark(X)) |
→ |
U22#(X) |
(152) |
U22#(active(X)) |
→ |
U22#(X) |
(114) |
could be deleted.
1.1.15.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
16th
component contains the
pair
U42#(mark(X)) |
→ |
U42#(X) |
(242) |
U42#(active(X)) |
→ |
U42#(X) |
(240) |
1.1.16 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
5 |
[U11(x1)] |
=
|
x1 + 4 |
[isNeList(x1)] |
=
|
1 |
[isPal(x1)] |
=
|
x1 + 2 |
[U42(x1)] |
=
|
x1 + 9 |
[u] |
=
|
44156 |
[U71(x1, x2)] |
=
|
x1 + x2 + 1 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 3 |
[U72(x1)] |
=
|
x1 + 8 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
5 |
[o] |
=
|
15190 |
[U42#(x1)] |
=
|
x1 + 0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
3 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
56385 |
[U52(x1)] |
=
|
5 |
[U61(x1)] |
=
|
x1 + 21992 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
9232 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
3 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 1 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
7 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 12015 |
[U51(x1, x2)] |
=
|
x2 + 3 |
[U41(x1, x2)] |
=
|
x1 + x2 + 1 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isNeList(active(X)) |
→ |
isNeList(X) |
(79) |
isNeList(mark(X)) |
→ |
isNeList(X) |
(78) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U42#(mark(X)) |
→ |
U42#(X) |
(242) |
U42#(active(X)) |
→ |
U42#(X) |
(240) |
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#(active(X)) |
→ |
isNeList#(X) |
(155) |
isNeList#(mark(X)) |
→ |
isNeList#(X) |
(199) |
1.1.17 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + x2 + 659 |
[U11(x1)] |
=
|
8076 |
[isNeList(x1)] |
=
|
x1 + 10430 |
[isPal(x1)] |
=
|
12512 |
[U42(x1)] |
=
|
x1 + 28171 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x2 + 19023 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
x1 + 0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
1 |
[U72(x1)] |
=
|
19025 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
10658 |
[o] |
=
|
25514 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
8074 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
41775 |
[U52(x1)] |
=
|
21964 |
[U61(x1)] |
=
|
3 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
23708 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
10432 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 12513 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
19027 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 11614 |
[U51(x1, x2)] |
=
|
x1 + x2 + 2935 |
[U41(x1, x2)] |
=
|
38599 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
U42(active(X)) |
→ |
U42(X) |
(77) |
U52(active(X)) |
→ |
U52(X) |
(85) |
isNePal(mark(X)) |
→ |
isNePal(X) |
(100) |
U11(mark(X)) |
→ |
U11(X) |
(60) |
U61(active(X)) |
→ |
U61(X) |
(87) |
U52(mark(X)) |
→ |
U52(X) |
(84) |
isNeList(active(X)) |
→ |
isNeList(X) |
(79) |
isNePal(active(X)) |
→ |
isNePal(X) |
(101) |
isNeList(mark(X)) |
→ |
isNeList(X) |
(78) |
U31(mark(X)) |
→ |
U31(X) |
(70) |
U42(mark(X)) |
→ |
U42(X) |
(76) |
U11(active(X)) |
→ |
U11(X) |
(61) |
U31(active(X)) |
→ |
U31(X) |
(71) |
U61(mark(X)) |
→ |
U61(X) |
(86) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
isNeList#(active(X)) |
→ |
isNeList#(X) |
(155) |
isNeList#(mark(X)) |
→ |
isNeList#(X) |
(199) |
could be deleted.
1.1.17.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
18th
component contains the
pair
U21#(mark(X1),X2) |
→ |
U21#(X1,X2) |
(163) |
U21#(X1,mark(X2)) |
→ |
U21#(X1,X2) |
(224) |
U21#(X1,active(X2)) |
→ |
U21#(X1,X2) |
(141) |
U21#(active(X1),X2) |
→ |
U21#(X1,X2) |
(117) |
1.1.18 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x2 + 5083 |
[U11(x1)] |
=
|
3 |
[isNeList(x1)] |
=
|
51923 |
[isPal(x1)] |
=
|
16531 |
[U42(x1)] |
=
|
51927 |
[u] |
=
|
423 |
[U71(x1, x2)] |
=
|
x2 + 13620 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
1 |
[U72(x1)] |
=
|
13622 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 31188 |
[o] |
=
|
19455 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
41865 |
[mark(x1)] |
=
|
x1 + 1 |
[isList#(x1)] |
=
|
0 |
[i] |
=
|
1431 |
[U52(x1)] |
=
|
51927 |
[U61(x1)] |
=
|
3 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1907 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 2 |
[U31(x1)] |
=
|
x1 + 20737 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
x1 + 0 |
[U81(x1)] |
=
|
16533 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
51929 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
5085 |
[U51(x1, x2)] |
=
|
x2 + 51925 |
[U41(x1, x2)] |
=
|
x2 + 51925 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
7382 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
U52(active(X)) |
→ |
U52(X) |
(85) |
U52(mark(X)) |
→ |
U52(X) |
(84) |
U81(mark(X)) |
→ |
U81(X) |
(96) |
U31(mark(X)) |
→ |
U31(X) |
(70) |
isQid(mark(X)) |
→ |
isQid(X) |
(98) |
U22(active(X)) |
→ |
U22(X) |
(67) |
U31(active(X)) |
→ |
U31(X) |
(71) |
U81(active(X)) |
→ |
U81(X) |
(97) |
isQid(active(X)) |
→ |
isQid(X) |
(99) |
U22(mark(X)) |
→ |
U22(X) |
(66) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U21#(mark(X1),X2) |
→ |
U21#(X1,X2) |
(163) |
U21#(active(X1),X2) |
→ |
U21#(X1,X2) |
(117) |
could be deleted.
1.1.18.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
19th
component contains the
pair
isList#(mark(X)) |
→ |
isList#(X) |
(187) |
isList#(active(X)) |
→ |
isList#(X) |
(168) |
1.1.19 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x2 + 1612 |
[U11(x1)] |
=
|
1612 |
[isNeList(x1)] |
=
|
4116 |
[isPal(x1)] |
=
|
1 |
[U42(x1)] |
=
|
4120 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x2 + 9036 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
9034 |
[U72(x1)] |
=
|
9038 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1918 |
[o] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[mark#(x1)] |
=
|
1 |
[isList(x1)] |
=
|
1610 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
38565 |
[mark(x1)] |
=
|
x1 + 33781 |
[isList#(x1)] |
=
|
x1 + 0 |
[i] |
=
|
4875 |
[U52(x1)] |
=
|
4120 |
[U61(x1)] |
=
|
9036 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 33782 |
[U31(x1)] |
=
|
x1 + 2200 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
1 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
3693 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
12273 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
1614 |
[U51(x1, x2)] |
=
|
x2 + 4118 |
[U41(x1, x2)] |
=
|
x2 + 4118 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
5372 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
U52(active(X)) |
→ |
U52(X) |
(85) |
U52(mark(X)) |
→ |
U52(X) |
(84) |
U81(mark(X)) |
→ |
U81(X) |
(96) |
U31(mark(X)) |
→ |
U31(X) |
(70) |
isQid(mark(X)) |
→ |
isQid(X) |
(98) |
U22(active(X)) |
→ |
U22(X) |
(67) |
U31(active(X)) |
→ |
U31(X) |
(71) |
U81(active(X)) |
→ |
U81(X) |
(97) |
isQid(active(X)) |
→ |
isQid(X) |
(99) |
U22(mark(X)) |
→ |
U22(X) |
(66) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
isList#(mark(X)) |
→ |
isList#(X) |
(187) |
isList#(active(X)) |
→ |
isList#(X) |
(168) |
could be deleted.
1.1.19.1 Dependency Graph Processor
The dependency pairs are split into 0
components.