The rewrite relation of the following TRS is considered.
There are 103 ruless (increase limit for explicit display).
There are 131 ruless (increase limit for explicit display).
The dependency pairs are split into 21
components.
-
The
1st
component contains the
pair
top#(mark(X)) |
→ |
top#(proper(X)) |
(208) |
top#(ok(X)) |
→ |
top#(active(X)) |
(198) |
1.1.1 Reduction Pair Processor with Usable Rules
Using the argument filter
π(top#) |
= |
1 |
π(U52#) |
= |
1 |
π(proper) |
= |
1 |
π(ok) |
= |
1 |
π(U51#) |
= |
1 |
π(active) |
= |
1 |
π(U71#) |
= |
2 |
π(U31#) |
= |
1 |
π(U61#) |
= |
1 |
in combination with the following Weighted Path Order with the following precedence and status
prec(a) |
= |
11 |
|
status(a) |
= |
[] |
|
list-extension(a) |
= |
Lex |
prec(U72#) |
= |
0 |
|
status(U72#) |
= |
[] |
|
list-extension(U72#) |
= |
Lex |
prec(U21) |
= |
5 |
|
status(U21) |
= |
[1, 2] |
|
list-extension(U21) |
= |
Lex |
prec(U11) |
= |
2 |
|
status(U11) |
= |
[1] |
|
list-extension(U11) |
= |
Lex |
prec(isNeList) |
= |
2 |
|
status(isNeList) |
= |
[1] |
|
list-extension(isNeList) |
= |
Lex |
prec(isPal) |
= |
6 |
|
status(isPal) |
= |
[1] |
|
list-extension(isPal) |
= |
Lex |
prec(U42) |
= |
0 |
|
status(U42) |
= |
[1] |
|
list-extension(U42) |
= |
Lex |
prec(u) |
= |
11 |
|
status(u) |
= |
[] |
|
list-extension(u) |
= |
Lex |
prec(U71) |
= |
6 |
|
status(U71) |
= |
[2, 1] |
|
list-extension(U71) |
= |
Lex |
prec(top) |
= |
0 |
|
status(top) |
= |
[] |
|
list-extension(top) |
= |
Lex |
prec(U81#) |
= |
0 |
|
status(U81#) |
= |
[] |
|
list-extension(U81#) |
= |
Lex |
prec(isNeList#) |
= |
0 |
|
status(isNeList#) |
= |
[] |
|
list-extension(isNeList#) |
= |
Lex |
prec(__#) |
= |
0 |
|
status(__#) |
= |
[2, 1] |
|
list-extension(__#) |
= |
Lex |
prec(isNePal) |
= |
5 |
|
status(isNePal) |
= |
[1] |
|
list-extension(isNePal) |
= |
Lex |
prec(U72) |
= |
5 |
|
status(U72) |
= |
[1] |
|
list-extension(U72) |
= |
Lex |
prec(isQid#) |
= |
0 |
|
status(isQid#) |
= |
[] |
|
list-extension(isQid#) |
= |
Lex |
prec(isPal#) |
= |
0 |
|
status(isPal#) |
= |
[] |
|
list-extension(isPal#) |
= |
Lex |
prec(isQid) |
= |
0 |
|
status(isQid) |
= |
[1] |
|
list-extension(isQid) |
= |
Lex |
prec(o) |
= |
4 |
|
status(o) |
= |
[] |
|
list-extension(o) |
= |
Lex |
prec(U42#) |
= |
0 |
|
status(U42#) |
= |
[] |
|
list-extension(U42#) |
= |
Lex |
prec(isList) |
= |
3 |
|
status(isList) |
= |
[1] |
|
list-extension(isList) |
= |
Lex |
prec(isNePal#) |
= |
0 |
|
status(isNePal#) |
= |
[] |
|
list-extension(isNePal#) |
= |
Lex |
prec(nil) |
= |
11 |
|
status(nil) |
= |
[] |
|
list-extension(nil) |
= |
Lex |
prec(mark) |
= |
0 |
|
status(mark) |
= |
[1] |
|
list-extension(mark) |
= |
Lex |
prec(isList#) |
= |
0 |
|
status(isList#) |
= |
[] |
|
list-extension(isList#) |
= |
Lex |
prec(proper#) |
= |
0 |
|
status(proper#) |
= |
[] |
|
list-extension(proper#) |
= |
Lex |
prec(i) |
= |
11 |
|
status(i) |
= |
[] |
|
list-extension(i) |
= |
Lex |
prec(U52) |
= |
4 |
|
status(U52) |
= |
[1] |
|
list-extension(U52) |
= |
Lex |
prec(U61) |
= |
0 |
|
status(U61) |
= |
[1] |
|
list-extension(U61) |
= |
Lex |
prec(e) |
= |
10 |
|
status(e) |
= |
[] |
|
list-extension(e) |
= |
Lex |
prec(U11#) |
= |
0 |
|
status(U11#) |
= |
[] |
|
list-extension(U11#) |
= |
Lex |
prec(U31) |
= |
1 |
|
status(U31) |
= |
[1] |
|
list-extension(U31) |
= |
Lex |
prec(U41#) |
= |
0 |
|
status(U41#) |
= |
[] |
|
list-extension(U41#) |
= |
Lex |
prec(active#) |
= |
0 |
|
status(active#) |
= |
[] |
|
list-extension(active#) |
= |
Lex |
prec(U21#) |
= |
0 |
|
status(U21#) |
= |
[1, 2] |
|
list-extension(U21#) |
= |
Lex |
prec(U81) |
= |
0 |
|
status(U81) |
= |
[1] |
|
list-extension(U81) |
= |
Lex |
prec(U22#) |
= |
0 |
|
status(U22#) |
= |
[] |
|
list-extension(U22#) |
= |
Lex |
prec(tt) |
= |
4 |
|
status(tt) |
= |
[] |
|
list-extension(tt) |
= |
Lex |
prec(U22) |
= |
4 |
|
status(U22) |
= |
[1] |
|
list-extension(U22) |
= |
Lex |
prec(U51) |
= |
6 |
|
status(U51) |
= |
[1, 2] |
|
list-extension(U51) |
= |
Lex |
prec(U41) |
= |
2 |
|
status(U41) |
= |
[2, 1] |
|
list-extension(U41) |
= |
Lex |
prec(__) |
= |
7 |
|
status(__) |
= |
[1, 2] |
|
list-extension(__) |
= |
Lex |
and the following
Max-polynomial interpretation
[a] |
=
|
0 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[U11(x1)] |
=
|
x1 + 0 |
[isNeList(x1)] |
=
|
x1 + 0 |
[isPal(x1)] |
=
|
x1 + 0 |
[U42(x1)] |
=
|
x1 + 0 |
[u] |
=
|
0 |
[U71(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[isNePal(x1)] |
=
|
x1 + 0 |
[U72(x1)] |
=
|
x1 + 0 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 0 |
[o] |
=
|
0 |
[U42#(x1)] |
=
|
0 |
[isList(x1)] |
=
|
x1 + 0 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
0 |
[mark(x1)] |
=
|
x1 + 0 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
0 |
[U52(x1)] |
=
|
x1 + 0 |
[U61(x1)] |
=
|
x1 + 0 |
[e] |
=
|
0 |
[U11#(x1)] |
=
|
0 |
[U31(x1)] |
=
|
x1 + 0 |
[U41#(x1, x2)] |
=
|
max(0) |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[U81(x1)] |
=
|
x1 + 0 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 0 |
[U51(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[U41(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
[__(x1, x2)] |
=
|
max(x1 + 0, x2 + 0, 0) |
together with the usable
rulesThere are 101 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)) |
(208) |
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#(__(X1,X2)) |
→ |
active#(X2) |
(228) |
active#(U41(X1,X2)) |
→ |
active#(X1) |
(227) |
active#(__(X1,X2)) |
→ |
active#(X1) |
(161) |
active#(U51(X1,X2)) |
→ |
active#(X1) |
(158) |
active#(U72(X)) |
→ |
active#(X) |
(220) |
active#(U21(X1,X2)) |
→ |
active#(X1) |
(147) |
active#(U61(X)) |
→ |
active#(X) |
(144) |
active#(U31(X)) |
→ |
active#(X) |
(131) |
active#(U52(X)) |
→ |
active#(X) |
(194) |
active#(U22(X)) |
→ |
active#(X) |
(193) |
active#(U81(X)) |
→ |
active#(X) |
(186) |
active#(U71(X1,X2)) |
→ |
active#(X1) |
(185) |
active#(U42(X)) |
→ |
active#(X) |
(108) |
active#(U11(X)) |
→ |
active#(X) |
(105) |
1.1.2 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + 2655 |
[U11(x1)] |
=
|
x1 + 1 |
[isNeList(x1)] |
=
|
x1 + 41274 |
[isPal(x1)] |
=
|
x1 + 27695 |
[U42(x1)] |
=
|
x1 + 41745 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + 12578 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 0 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
x1 + 45189 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
0 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
0 |
[mark(x1)] |
=
|
0 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
x1 + 1 |
[U61(x1)] |
=
|
x1 + 1 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
59483 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
x1 + 1 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
x1 + 0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 1 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 0 |
[U51(x1, x2)] |
=
|
x1 + x2 + 1 |
[U41(x1, x2)] |
=
|
x1 + 0 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
active(isList(__(V1,V2))) |
→ |
mark(U21(isList(V1),V2)) |
(18) |
U31(mark(X)) |
→ |
mark(U31(X)) |
(50) |
proper(e) |
→ |
ok(e) |
(80) |
active(U11(tt)) |
→ |
mark(tt) |
(4) |
active(U81(tt)) |
→ |
mark(tt) |
(15) |
active(U41(tt,V2)) |
→ |
mark(U42(isNeList(V2))) |
(8) |
U52(mark(X)) |
→ |
mark(U52(X)) |
(54) |
active(__(__(X,Y),Z)) |
→ |
mark(__(X,__(Y,Z))) |
(1) |
active(__(nil,X)) |
→ |
mark(X) |
(3) |
active(isList(V)) |
→ |
mark(U11(isNeList(V))) |
(16) |
active(isNeList(__(V1,V2))) |
→ |
mark(U51(isNeList(V1),V2)) |
(21) |
U11(ok(X)) |
→ |
ok(U11(X)) |
(85) |
isQid(ok(X)) |
→ |
ok(isQid(X)) |
(100) |
active(isQid(a)) |
→ |
mark(tt) |
(26) |
active(isNeList(V)) |
→ |
mark(U31(isQid(V))) |
(19) |
active(isList(nil)) |
→ |
mark(tt) |
(17) |
proper(nil) |
→ |
ok(nil) |
(60) |
active(isQid(e)) |
→ |
mark(tt) |
(27) |
U22(ok(X)) |
→ |
ok(U22(X)) |
(87) |
__(ok(X1),ok(X2)) |
→ |
ok(__(X1,X2)) |
(84) |
active(isNePal(V)) |
→ |
mark(U61(isQid(V))) |
(22) |
active(isQid(i)) |
→ |
mark(tt) |
(28) |
active(U21(tt,V2)) |
→ |
mark(U22(isList(V2))) |
(5) |
U51(ok(X1),ok(X2)) |
→ |
ok(U51(X1,X2)) |
(93) |
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(92) |
active(U51(tt,V2)) |
→ |
mark(U52(isList(V2))) |
(10) |
active(U31(tt)) |
→ |
mark(tt) |
(7) |
active(isNeList(__(V1,V2))) |
→ |
mark(U41(isList(V1),V2)) |
(20) |
active(isPal(nil)) |
→ |
mark(tt) |
(25) |
U22(mark(X)) |
→ |
mark(U22(X)) |
(49) |
U42(mark(X)) |
→ |
mark(U42(X)) |
(52) |
active(isQid(u)) |
→ |
mark(tt) |
(30) |
proper(tt) |
→ |
ok(tt) |
(62) |
active(U72(tt)) |
→ |
mark(tt) |
(14) |
proper(o) |
→ |
ok(o) |
(82) |
U31(ok(X)) |
→ |
ok(U31(X)) |
(89) |
U71(mark(X1),X2) |
→ |
mark(U71(X1,X2)) |
(56) |
proper(a) |
→ |
ok(a) |
(79) |
active(U61(tt)) |
→ |
mark(tt) |
(12) |
isNePal(ok(X)) |
→ |
ok(isNePal(X)) |
(101) |
U71(ok(X1),ok(X2)) |
→ |
ok(U71(X1,X2)) |
(96) |
__(mark(X1),X2) |
→ |
mark(__(X1,X2)) |
(45) |
proper(i) |
→ |
ok(i) |
(81) |
active(isNePal(__(I,__(P,I)))) |
→ |
mark(U71(isQid(I),P)) |
(23) |
active(isPal(V)) |
→ |
mark(U81(isNePal(V))) |
(24) |
U52(ok(X)) |
→ |
ok(U52(X)) |
(94) |
U72(mark(X)) |
→ |
mark(U72(X)) |
(57) |
isPal(ok(X)) |
→ |
ok(isPal(X)) |
(98) |
active(U52(tt)) |
→ |
mark(tt) |
(11) |
active(U42(tt)) |
→ |
mark(tt) |
(9) |
active(U71(tt,P)) |
→ |
mark(U72(isPal(P))) |
(13) |
U41(mark(X1),X2) |
→ |
mark(U41(X1,X2)) |
(51) |
U41(ok(X1),ok(X2)) |
→ |
ok(U41(X1,X2)) |
(90) |
U61(mark(X)) |
→ |
mark(U61(X)) |
(55) |
active(U22(tt)) |
→ |
mark(tt) |
(6) |
U81(mark(X)) |
→ |
mark(U81(X)) |
(58) |
U21(mark(X1),X2) |
→ |
mark(U21(X1,X2)) |
(48) |
U51(mark(X1),X2) |
→ |
mark(U51(X1,X2)) |
(53) |
U11(mark(X)) |
→ |
mark(U11(X)) |
(47) |
U42(ok(X)) |
→ |
ok(U42(X)) |
(91) |
U72(ok(X)) |
→ |
ok(U72(X)) |
(97) |
U81(ok(X)) |
→ |
ok(U81(X)) |
(99) |
U61(ok(X)) |
→ |
ok(U61(X)) |
(95) |
__(X1,mark(X2)) |
→ |
mark(__(X1,X2)) |
(46) |
proper(u) |
→ |
ok(u) |
(83) |
active(isQid(o)) |
→ |
mark(tt) |
(29) |
U21(ok(X1),ok(X2)) |
→ |
ok(U21(X1,X2)) |
(86) |
active(__(X,nil)) |
→ |
mark(X) |
(2) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
active#(__(X1,X2)) |
→ |
active#(X2) |
(228) |
active#(__(X1,X2)) |
→ |
active#(X1) |
(161) |
active#(U51(X1,X2)) |
→ |
active#(X1) |
(158) |
active#(U72(X)) |
→ |
active#(X) |
(220) |
active#(U21(X1,X2)) |
→ |
active#(X1) |
(147) |
active#(U61(X)) |
→ |
active#(X) |
(144) |
active#(U31(X)) |
→ |
active#(X) |
(131) |
active#(U52(X)) |
→ |
active#(X) |
(194) |
active#(U81(X)) |
→ |
active#(X) |
(186) |
active#(U71(X1,X2)) |
→ |
active#(X1) |
(185) |
active#(U42(X)) |
→ |
active#(X) |
(108) |
active#(U11(X)) |
→ |
active#(X) |
(105) |
could be deleted.
1.1.2.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
3rd
component contains the
pair
proper#(U52(X)) |
→ |
proper#(X) |
(176) |
proper#(U81(X)) |
→ |
proper#(X) |
(174) |
proper#(isNePal(X)) |
→ |
proper#(X) |
(172) |
proper#(U72(X)) |
→ |
proper#(X) |
(173) |
proper#(U21(X1,X2)) |
→ |
proper#(X1) |
(171) |
proper#(U42(X)) |
→ |
proper#(X) |
(169) |
proper#(isList(X)) |
→ |
proper#(X) |
(151) |
proper#(U71(X1,X2)) |
→ |
proper#(X2) |
(218) |
proper#(U51(X1,X2)) |
→ |
proper#(X1) |
(148) |
proper#(U21(X1,X2)) |
→ |
proper#(X2) |
(142) |
proper#(__(X1,X2)) |
→ |
proper#(X2) |
(133) |
proper#(U51(X1,X2)) |
→ |
proper#(X2) |
(130) |
proper#(U22(X)) |
→ |
proper#(X) |
(200) |
proper#(isPal(X)) |
→ |
proper#(X) |
(196) |
proper#(__(X1,X2)) |
→ |
proper#(X1) |
(116) |
proper#(U11(X)) |
→ |
proper#(X) |
(190) |
proper#(isQid(X)) |
→ |
proper#(X) |
(187) |
proper#(U41(X1,X2)) |
→ |
proper#(X1) |
(115) |
proper#(U41(X1,X2)) |
→ |
proper#(X2) |
(112) |
proper#(isNeList(X)) |
→ |
proper#(X) |
(110) |
proper#(U61(X)) |
→ |
proper#(X) |
(182) |
proper#(U31(X)) |
→ |
proper#(X) |
(183) |
proper#(U71(X1,X2)) |
→ |
proper#(X1) |
(180) |
1.1.3 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + x2 + 1 |
[U11(x1)] |
=
|
x1 + 1 |
[isNeList(x1)] |
=
|
x1 + 9999 |
[isPal(x1)] |
=
|
x1 + 1 |
[U42(x1)] |
=
|
x1 + 23802 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 23235 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
x1 + 1 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
x1 + 17686 |
[ok(x1)] |
=
|
x1 + 17686 |
[isList(x1)] |
=
|
x1 + 14078 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
0 |
[mark(x1)] |
=
|
0 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
x1 + 0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
x1 + 1 |
[U61(x1)] |
=
|
x1 + 14622 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
22305 |
[U31(x1)] |
=
|
x1 + 1 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 1 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 1 |
[U51(x1, x2)] |
=
|
x1 + x2 + 1 |
[U41(x1, x2)] |
=
|
x1 + x2 + 18871 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + x2 + 1 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
U31(mark(X)) |
→ |
mark(U31(X)) |
(50) |
proper(e) |
→ |
ok(e) |
(80) |
active(U11(tt)) |
→ |
mark(tt) |
(4) |
active(U81(tt)) |
→ |
mark(tt) |
(15) |
U52(mark(X)) |
→ |
mark(U52(X)) |
(54) |
U11(ok(X)) |
→ |
ok(U11(X)) |
(85) |
isQid(ok(X)) |
→ |
ok(isQid(X)) |
(100) |
active(isQid(a)) |
→ |
mark(tt) |
(26) |
active(isList(nil)) |
→ |
mark(tt) |
(17) |
proper(nil) |
→ |
ok(nil) |
(60) |
active(isQid(e)) |
→ |
mark(tt) |
(27) |
__(ok(X1),ok(X2)) |
→ |
ok(__(X1,X2)) |
(84) |
active(isQid(i)) |
→ |
mark(tt) |
(28) |
U51(ok(X1),ok(X2)) |
→ |
ok(U51(X1,X2)) |
(93) |
isNeList(ok(X)) |
→ |
ok(isNeList(X)) |
(92) |
active(U31(tt)) |
→ |
mark(tt) |
(7) |
isList(ok(X)) |
→ |
ok(isList(X)) |
(88) |
active(isPal(nil)) |
→ |
mark(tt) |
(25) |
U22(mark(X)) |
→ |
mark(U22(X)) |
(49) |
U42(mark(X)) |
→ |
mark(U42(X)) |
(52) |
active(isQid(u)) |
→ |
mark(tt) |
(30) |
proper(tt) |
→ |
ok(tt) |
(62) |
active(U72(tt)) |
→ |
mark(tt) |
(14) |
proper(o) |
→ |
ok(o) |
(82) |
U71(mark(X1),X2) |
→ |
mark(U71(X1,X2)) |
(56) |
proper(a) |
→ |
ok(a) |
(79) |
active(U61(tt)) |
→ |
mark(tt) |
(12) |
isNePal(ok(X)) |
→ |
ok(isNePal(X)) |
(101) |
U71(ok(X1),ok(X2)) |
→ |
ok(U71(X1,X2)) |
(96) |
__(mark(X1),X2) |
→ |
mark(__(X1,X2)) |
(45) |
proper(i) |
→ |
ok(i) |
(81) |
U72(mark(X)) |
→ |
mark(U72(X)) |
(57) |
isPal(ok(X)) |
→ |
ok(isPal(X)) |
(98) |
active(U52(tt)) |
→ |
mark(tt) |
(11) |
active(U42(tt)) |
→ |
mark(tt) |
(9) |
U41(mark(X1),X2) |
→ |
mark(U41(X1,X2)) |
(51) |
U41(ok(X1),ok(X2)) |
→ |
ok(U41(X1,X2)) |
(90) |
U61(mark(X)) |
→ |
mark(U61(X)) |
(55) |
active(U22(tt)) |
→ |
mark(tt) |
(6) |
U81(mark(X)) |
→ |
mark(U81(X)) |
(58) |
U21(mark(X1),X2) |
→ |
mark(U21(X1,X2)) |
(48) |
U51(mark(X1),X2) |
→ |
mark(U51(X1,X2)) |
(53) |
U11(mark(X)) |
→ |
mark(U11(X)) |
(47) |
U42(ok(X)) |
→ |
ok(U42(X)) |
(91) |
U72(ok(X)) |
→ |
ok(U72(X)) |
(97) |
U81(ok(X)) |
→ |
ok(U81(X)) |
(99) |
U61(ok(X)) |
→ |
ok(U61(X)) |
(95) |
__(X1,mark(X2)) |
→ |
mark(__(X1,X2)) |
(46) |
proper(u) |
→ |
ok(u) |
(83) |
active(isQid(o)) |
→ |
mark(tt) |
(29) |
U21(ok(X1),ok(X2)) |
→ |
ok(U21(X1,X2)) |
(86) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
proper#(U52(X)) |
→ |
proper#(X) |
(176) |
proper#(U81(X)) |
→ |
proper#(X) |
(174) |
proper#(isNePal(X)) |
→ |
proper#(X) |
(172) |
proper#(U72(X)) |
→ |
proper#(X) |
(173) |
proper#(U21(X1,X2)) |
→ |
proper#(X1) |
(171) |
proper#(U42(X)) |
→ |
proper#(X) |
(169) |
proper#(isList(X)) |
→ |
proper#(X) |
(151) |
proper#(U71(X1,X2)) |
→ |
proper#(X2) |
(218) |
proper#(U51(X1,X2)) |
→ |
proper#(X1) |
(148) |
proper#(U21(X1,X2)) |
→ |
proper#(X2) |
(142) |
proper#(__(X1,X2)) |
→ |
proper#(X2) |
(133) |
proper#(U51(X1,X2)) |
→ |
proper#(X2) |
(130) |
proper#(U22(X)) |
→ |
proper#(X) |
(200) |
proper#(isPal(X)) |
→ |
proper#(X) |
(196) |
proper#(__(X1,X2)) |
→ |
proper#(X1) |
(116) |
proper#(U11(X)) |
→ |
proper#(X) |
(190) |
proper#(isQid(X)) |
→ |
proper#(X) |
(187) |
proper#(U41(X1,X2)) |
→ |
proper#(X1) |
(115) |
proper#(U41(X1,X2)) |
→ |
proper#(X2) |
(112) |
proper#(isNeList(X)) |
→ |
proper#(X) |
(110) |
proper#(U61(X)) |
→ |
proper#(X) |
(182) |
proper#(U31(X)) |
→ |
proper#(X) |
(183) |
proper#(U71(X1,X2)) |
→ |
proper#(X1) |
(180) |
could be deleted.
1.1.3.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
4th
component contains the
pair
U31#(mark(X)) |
→ |
U31#(X) |
(179) |
U31#(ok(X)) |
→ |
U31#(X) |
(124) |
1.1.4 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + x2 + 1 |
[U11(x1)] |
=
|
8786 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
x1 + 1 |
[U42(x1)] |
=
|
x1 + 1 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 1 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
3 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
5017 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 3905 |
[isList(x1)] |
=
|
3 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
33606 |
[mark(x1)] |
=
|
x1 + 55148 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
20845 |
[U52(x1)] |
=
|
x1 + 33730 |
[U61(x1)] |
=
|
x1 + 1 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
256 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
x1 + 1 |
[U31(x1)] |
=
|
x1 + 13020 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
270 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
x1 + 26834 |
[U51(x1, x2)] |
=
|
54947 |
[U41(x1, x2)] |
=
|
x1 + 26287 |
[U31#(x1)] |
=
|
x1 + 0 |
[__(x1, x2)] |
=
|
x1 + 21540 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
U31(mark(X)) |
→ |
mark(U31(X)) |
(50) |
isQid(ok(X)) |
→ |
ok(isQid(X)) |
(100) |
U31(ok(X)) |
→ |
ok(U31(X)) |
(89) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
U31#(mark(X)) |
→ |
U31#(X) |
(179) |
U31#(ok(X)) |
→ |
U31#(X) |
(124) |
could be deleted.
1.1.4.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
5th
component contains the
pair
U71#(mark(X1),X2) |
→ |
U71#(X1,X2) |
(153) |
U71#(ok(X1),ok(X2)) |
→ |
U71#(X1,X2) |
(189) |
1.1.5 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
3 |
[U11(x1)] |
=
|
32009 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
24328 |
[U42(x1)] |
=
|
x1 + 16872 |
[u] |
=
|
31216 |
[U71(x1, x2)] |
=
|
x2 + 14990 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
2954 |
[U72(x1)] |
=
|
3 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
14652 |
[o] |
=
|
16160 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 10263 |
[isList(x1)] |
=
|
3 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 6559 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
17822 |
[U52(x1)] |
=
|
x1 + 40351 |
[U61(x1)] |
=
|
31302 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
41499 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
356 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
7523 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
x1 + 0 |
[U22(x1)] |
=
|
8511 |
[U51(x1, x2)] |
=
|
15505 |
[U41(x1, x2)] |
=
|
10906 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U71#(mark(X1),X2) |
→ |
U71#(X1,X2) |
(153) |
U71#(ok(X1),ok(X2)) |
→ |
U71#(X1,X2) |
(189) |
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#(mark(X)) |
→ |
U52#(X) |
(214) |
U52#(ok(X)) |
→ |
U52#(X) |
(123) |
1.1.6 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
31410 |
[U11(x1)] |
=
|
12354 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
24328 |
[U42(x1)] |
=
|
x1 + 16872 |
[u] |
=
|
18418 |
[U71(x1, x2)] |
=
|
x2 + 40762 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
2954 |
[U72(x1)] |
=
|
12524 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
x1 + 0 |
[isQid(x1)] |
=
|
14652 |
[o] |
=
|
16160 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 28976 |
[isList(x1)] |
=
|
2 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 29849 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
17822 |
[U52(x1)] |
=
|
x1 + 1 |
[U61(x1)] |
=
|
18329 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
2247 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
18839 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
14174 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
30724 |
[U51(x1, x2)] |
=
|
26007 |
[U41(x1, x2)] |
=
|
16484 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U52#(mark(X)) |
→ |
U52#(X) |
(214) |
U52#(ok(X)) |
→ |
U52#(X) |
(123) |
could be deleted.
1.1.6.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
7th
component contains the
pair
isPal#(ok(X)) |
→ |
isPal#(X) |
(175) |
1.1.7 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
2 |
[U11(x1)] |
=
|
2 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
22740 |
[U42(x1)] |
=
|
x1 + 1 |
[u] |
=
|
38026 |
[U71(x1, x2)] |
=
|
x2 + 5437 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
31633 |
[U72(x1)] |
=
|
12524 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
x1 + 0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
14652 |
[o] |
=
|
43122 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 8605 |
[isList(x1)] |
=
|
2 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 29849 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
8240 |
[U52(x1)] |
=
|
x1 + 1 |
[U61(x1)] |
=
|
12448 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
2247 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
8931 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
23381 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
30724 |
[U51(x1, x2)] |
=
|
2 |
[U41(x1, x2)] |
=
|
16484 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
isPal#(ok(X)) |
→ |
isPal#(X) |
(175) |
could be deleted.
1.1.7.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
8th
component contains the
pair
U72#(mark(X)) |
→ |
U72#(X) |
(233) |
U72#(ok(X)) |
→ |
U72#(X) |
(205) |
1.1.8 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
x1 + 0 |
[U21(x1, x2)] |
=
|
2176 |
[U11(x1)] |
=
|
28519 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
22740 |
[U42(x1)] |
=
|
x1 + 20578 |
[u] |
=
|
26631 |
[U71(x1, x2)] |
=
|
x2 + 30707 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
22335 |
[U72(x1)] |
=
|
24855 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
14652 |
[o] |
=
|
11601 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 28710 |
[isList(x1)] |
=
|
2 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 29849 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
8240 |
[U52(x1)] |
=
|
x1 + 1 |
[U61(x1)] |
=
|
11469 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
14095 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
6706 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
17613 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
31853 |
[U51(x1, x2)] |
=
|
31669 |
[U41(x1, x2)] |
=
|
34721 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U72#(mark(X)) |
→ |
U72#(X) |
(233) |
U72#(ok(X)) |
→ |
U72#(X) |
(205) |
could be deleted.
1.1.8.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
9th
component contains the
pair
U11#(ok(X)) |
→ |
U11#(X) |
(150) |
U11#(mark(X)) |
→ |
U11#(X) |
(197) |
1.1.9 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
4634 |
[U11(x1)] |
=
|
10709 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
22740 |
[U42(x1)] |
=
|
x1 + 15815 |
[u] |
=
|
59110 |
[U71(x1, x2)] |
=
|
x2 + 15115 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
22335 |
[U72(x1)] |
=
|
36300 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
21733 |
[o] |
=
|
36730 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 20595 |
[isList(x1)] |
=
|
2 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 29849 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
8240 |
[U52(x1)] |
=
|
x1 + 1 |
[U61(x1)] |
=
|
9795 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
50752 |
[U11#(x1)] |
=
|
x1 + 0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
14470 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 9728 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
31853 |
[U51(x1, x2)] |
=
|
8092 |
[U41(x1, x2)] |
=
|
34721 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U11#(ok(X)) |
→ |
U11#(X) |
(150) |
U11#(mark(X)) |
→ |
U11#(X) |
(197) |
could be deleted.
1.1.9.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
10th
component contains the
pair
__#(X1,mark(X2)) |
→ |
__#(X1,X2) |
(225) |
__#(mark(X1),X2) |
→ |
__#(X1,X2) |
(209) |
__#(ok(X1),ok(X2)) |
→ |
__#(X1,X2) |
(118) |
1.1.10 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
4634 |
[U11(x1)] |
=
|
2 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
22740 |
[U42(x1)] |
=
|
x1 + 11793 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x2 + 15115 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
x1 + x2 + 0 |
[isNePal(x1)] |
=
|
20351 |
[U72(x1)] |
=
|
36300 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
21733 |
[o] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 27297 |
[isList(x1)] |
=
|
10471 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 21817 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
x1 + 1 |
[U61(x1)] |
=
|
2 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
6224 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 16016 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
41429 |
[U51(x1, x2)] |
=
|
26158 |
[U41(x1, x2)] |
=
|
64911 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
__#(X1,mark(X2)) |
→ |
__#(X1,X2) |
(225) |
__#(mark(X1),X2) |
→ |
__#(X1,X2) |
(209) |
__#(ok(X1),ok(X2)) |
→ |
__#(X1,X2) |
(118) |
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#(ok(X1),ok(X2)) |
→ |
U41#(X1,X2) |
(159) |
U41#(mark(X1),X2) |
→ |
U41#(X1,X2) |
(111) |
1.1.11 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
2 |
[U11(x1)] |
=
|
2 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
30145 |
[U42(x1)] |
=
|
x1 + 23479 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x2 + 15115 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
22051 |
[U72(x1)] |
=
|
36300 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
21733 |
[o] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
2 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 21817 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
x1 + 2013 |
[U61(x1)] |
=
|
2 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
24036 |
[U41#(x1, x2)] |
=
|
x1 + 0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 28573 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
41429 |
[U51(x1, x2)] |
=
|
16061 |
[U41(x1, x2)] |
=
|
64911 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U41#(ok(X1),ok(X2)) |
→ |
U41#(X1,X2) |
(159) |
U41#(mark(X1),X2) |
→ |
U41#(X1,X2) |
(111) |
could be deleted.
1.1.11.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
12th
component contains the
pair
U81#(mark(X)) |
→ |
U81#(X) |
(164) |
U81#(ok(X)) |
→ |
U81#(X) |
(219) |
1.1.12 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
10741 |
[U11(x1)] |
=
|
16120 |
[isNeList(x1)] |
=
|
2 |
[isPal(x1)] |
=
|
10802 |
[U42(x1)] |
=
|
x1 + 1 |
[u] |
=
|
51225 |
[U71(x1, x2)] |
=
|
x2 + 21325 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
x1 + 0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
2 |
[U72(x1)] |
=
|
64930 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
935 |
[o] |
=
|
41051 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1 |
[ok(x1)] |
=
|
x1 + 18290 |
[isList(x1)] |
=
|
2 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
12145 |
[mark(x1)] |
=
|
x1 + 21817 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1346 |
[U52(x1)] |
=
|
x1 + 1 |
[U61(x1)] |
=
|
2 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
33606 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
13508 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 1 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
59265 |
[U51(x1, x2)] |
=
|
35794 |
[U41(x1, x2)] |
=
|
85714 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U81#(mark(X)) |
→ |
U81#(X) |
(164) |
U81#(ok(X)) |
→ |
U81#(X) |
(219) |
could be deleted.
1.1.12.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
13th
component contains the
pair
U51#(ok(X1),ok(X2)) |
→ |
U51#(X1,X2) |
(168) |
U51#(mark(X1),X2) |
→ |
U51#(X1,X2) |
(154) |
1.1.13 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + x2 + 43054 |
[U11(x1)] |
=
|
2 |
[isNeList(x1)] |
=
|
7085 |
[isPal(x1)] |
=
|
x1 + 37105 |
[U42(x1)] |
=
|
3 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 13474 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 35412 |
[o] |
=
|
41051 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
x1 + 1 |
[ok(x1)] |
=
|
x1 + 18521 |
[isList(x1)] |
=
|
x1 + 48168 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
3 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
14535 |
[U52(x1)] |
=
|
9612 |
[U61(x1)] |
=
|
x1 + 8257 |
[U51#(x1, x2)] |
=
|
x2 + 0 |
[e] |
=
|
33606 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
2 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 12192 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
2 |
[U51(x1, x2)] |
=
|
2 |
[U41(x1, x2)] |
=
|
2 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isQid(ok(X)) |
→ |
ok(isQid(X)) |
(100) |
U61(mark(X)) |
→ |
mark(U61(X)) |
(55) |
U61(ok(X)) |
→ |
ok(U61(X)) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
U51#(ok(X1),ok(X2)) |
→ |
U51#(X1,X2) |
(168) |
could be deleted.
1.1.13.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
14th
component contains the
pair
isNePal#(ok(X)) |
→ |
isNePal#(X) |
(139) |
1.1.14 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + x2 + 533 |
[U11(x1)] |
=
|
2 |
[isNeList(x1)] |
=
|
53220 |
[isPal(x1)] |
=
|
x1 + 42393 |
[U42(x1)] |
=
|
2 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 0 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(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] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
x1 + 30924 |
[ok(x1)] |
=
|
x1 + 30925 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
x1 + 0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 21391 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
2 |
[U61(x1)] |
=
|
x1 + 1 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
2 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 1 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
2 |
[U51(x1, x2)] |
=
|
2 |
[U41(x1, x2)] |
=
|
28540 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isQid(ok(X)) |
→ |
ok(isQid(X)) |
(100) |
U61(mark(X)) |
→ |
mark(U61(X)) |
(55) |
U61(ok(X)) |
→ |
ok(U61(X)) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
isNePal#(ok(X)) |
→ |
isNePal#(X) |
(139) |
could be deleted.
1.1.14.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
15th
component contains the
pair
isNeList#(ok(X)) |
→ |
isNeList#(X) |
(156) |
1.1.15 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + x2 + 533 |
[U11(x1)] |
=
|
9395 |
[isNeList(x1)] |
=
|
1 |
[isPal(x1)] |
=
|
x1 + 1 |
[U42(x1)] |
=
|
2 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
x1 + x2 + 0 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
x1 + 0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
x1 + 1 |
[U72(x1)] |
=
|
30681 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
x1 + 53120 |
[ok(x1)] |
=
|
x1 + 53121 |
[isList(x1)] |
=
|
x1 + 1 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 2 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
2 |
[U61(x1)] |
=
|
x1 + 1 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
2 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
x1 + 1 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
1 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
27437 |
[U51(x1, x2)] |
=
|
32745 |
[U41(x1, x2)] |
=
|
59928 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 2 |
[U61#(x1)] |
=
|
0 |
together with the usable
rules
isQid(ok(X)) |
→ |
ok(isQid(X)) |
(100) |
U61(mark(X)) |
→ |
mark(U61(X)) |
(55) |
U61(ok(X)) |
→ |
ok(U61(X)) |
(95) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pair
isNeList#(ok(X)) |
→ |
isNeList#(X) |
(156) |
could be deleted.
1.1.15.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
16th
component contains the
pair
U22#(ok(X)) |
→ |
U22#(X) |
(212) |
U22#(mark(X)) |
→ |
U22#(X) |
(121) |
1.1.16 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x1 + 1 |
[U11(x1)] |
=
|
x1 + 28983 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
22084 |
[U42(x1)] |
=
|
15343 |
[u] |
=
|
30351 |
[U71(x1, x2)] |
=
|
22851 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
29195 |
[U72(x1)] |
=
|
8000 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
41308 |
[o] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
x1 + 1 |
[ok(x1)] |
=
|
x1 + 24152 |
[isList(x1)] |
=
|
18436 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
32345 |
[mark(x1)] |
=
|
x1 + 4961 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
30115 |
[U52(x1)] |
=
|
x1 + 7506 |
[U61(x1)] |
=
|
13914 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
2189 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
x1 + 1 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
1672 |
[U22#(x1)] |
=
|
x1 + 0 |
[tt] |
=
|
2438 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
14776 |
[U51(x1, x2)] |
=
|
11721 |
[U41(x1, x2)] |
=
|
29462 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
x1 + 28765 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U22#(ok(X)) |
→ |
U22#(X) |
(212) |
U22#(mark(X)) |
→ |
U22#(X) |
(121) |
could be deleted.
1.1.16.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
17th
component contains the
pair
U61#(ok(X)) |
→ |
U61#(X) |
(146) |
U61#(mark(X)) |
→ |
U61#(X) |
(184) |
1.1.17 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x2 + 1318 |
[U11(x1)] |
=
|
x1 + 874 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
1319 |
[U42(x1)] |
=
|
31213 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
1318 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
1319 |
[U72(x1)] |
=
|
1318 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 30799 |
[o] |
=
|
23562 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
1318 |
[ok(x1)] |
=
|
x1 + 1318 |
[isList(x1)] |
=
|
1319 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
24600 |
[mark(x1)] |
=
|
x1 + 1318 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
9712 |
[U52(x1)] |
=
|
1319 |
[U61(x1)] |
=
|
13914 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
2189 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1317 |
[U31(x1)] |
=
|
x1 + 1 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
1672 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
38165 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
1318 |
[U51(x1, x2)] |
=
|
1318 |
[U41(x1, x2)] |
=
|
1318 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
1319 |
[U61#(x1)] |
=
|
x1 + 0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U61#(ok(X)) |
→ |
U61#(X) |
(146) |
U61#(mark(X)) |
→ |
U61#(X) |
(184) |
could be deleted.
1.1.17.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
18th
component contains the
pair
isList#(ok(X)) |
→ |
isList#(X) |
(149) |
1.1.18 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x2 + 14318 |
[U11(x1)] |
=
|
x1 + 1 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
3 |
[U42(x1)] |
=
|
3 |
[u] |
=
|
1 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
28916 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
1 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[ok(x1)] |
=
|
x1 + 2 |
[isList(x1)] |
=
|
23275 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 26554 |
[isList#(x1)] |
=
|
x1 + 0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
1 |
[U52(x1)] |
=
|
16608 |
[U61(x1)] |
=
|
13914 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
22436 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
x1 + 1 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
3 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
12308 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
2 |
[U51(x1, x2)] |
=
|
2 |
[U41(x1, x2)] |
=
|
2 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
3 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
isList#(ok(X)) |
→ |
isList#(X) |
(149) |
could be deleted.
1.1.18.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
19th
component contains the
pair
U21#(ok(X1),ok(X2)) |
→ |
U21#(X1,X2) |
(222) |
U21#(mark(X1),X2) |
→ |
U21#(X1,X2) |
(211) |
1.1.19 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
2 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x2 + 1773 |
[U11(x1)] |
=
|
x1 + 1 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
3 |
[U42(x1)] |
=
|
3 |
[u] |
=
|
6143 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
3 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
2 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[ok(x1)] |
=
|
x1 + 1 |
[isList(x1)] |
=
|
3 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 31644 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
2 |
[U52(x1)] |
=
|
19817 |
[U61(x1)] |
=
|
3 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
2 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
x1 + 1 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
x1 + 0 |
[U81(x1)] |
=
|
3 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
2 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
2 |
[U51(x1, x2)] |
=
|
2 |
[U41(x1, x2)] |
=
|
2 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
3 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U21#(ok(X1),ok(X2)) |
→ |
U21#(X1,X2) |
(222) |
U21#(mark(X1),X2) |
→ |
U21#(X1,X2) |
(211) |
could be deleted.
1.1.19.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
20th
component contains the
pair
U42#(ok(X)) |
→ |
U42#(X) |
(234) |
U42#(mark(X)) |
→ |
U42#(X) |
(191) |
1.1.20 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x2 + 6030 |
[U11(x1)] |
=
|
x1 + 1 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
3 |
[U42(x1)] |
=
|
13623 |
[u] |
=
|
18972 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
12514 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
28167 |
[U42#(x1)] |
=
|
x1 + 0 |
[proper(x1)] |
=
|
2 |
[ok(x1)] |
=
|
x1 + 2 |
[isList(x1)] |
=
|
31907 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
2 |
[mark(x1)] |
=
|
x1 + 31644 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
658 |
[U52(x1)] |
=
|
4018 |
[U61(x1)] |
=
|
12019 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
1 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
x1 + 1 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
21268 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
32626 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
2 |
[U51(x1, x2)] |
=
|
2 |
[U41(x1, x2)] |
=
|
2 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
3 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pairs
U42#(ok(X)) |
→ |
U42#(X) |
(234) |
U42#(mark(X)) |
→ |
U42#(X) |
(191) |
could be deleted.
1.1.20.1 Dependency Graph Processor
The dependency pairs are split into 0
components.
-
The
21th
component contains the
pair
isQid#(ok(X)) |
→ |
isQid#(X) |
(178) |
1.1.21 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation
[a] |
=
|
1 |
[U72#(x1)] |
=
|
0 |
[U21(x1, x2)] |
=
|
x2 + 6030 |
[U11(x1)] |
=
|
x1 + 1 |
[isNeList(x1)] |
=
|
x1 + 1 |
[isPal(x1)] |
=
|
3 |
[U42(x1)] |
=
|
3 |
[u] |
=
|
47341 |
[U71(x1, x2)] |
=
|
2 |
[top(x1)] |
=
|
0 |
[U81#(x1)] |
=
|
0 |
[isNeList#(x1)] |
=
|
0 |
[top#(x1)] |
=
|
0 |
[__#(x1, x2)] |
=
|
0 |
[isNePal(x1)] |
=
|
12514 |
[U72(x1)] |
=
|
2 |
[isQid#(x1)] |
=
|
x1 + 0 |
[isPal#(x1)] |
=
|
0 |
[U52#(x1)] |
=
|
0 |
[isQid(x1)] |
=
|
x1 + 1 |
[o] |
=
|
30282 |
[U42#(x1)] |
=
|
0 |
[proper(x1)] |
=
|
2 |
[ok(x1)] |
=
|
x1 + 3 |
[isList(x1)] |
=
|
31907 |
[isNePal#(x1)] |
=
|
0 |
[nil] |
=
|
1 |
[mark(x1)] |
=
|
x1 + 31644 |
[isList#(x1)] |
=
|
0 |
[proper#(x1)] |
=
|
0 |
[i] |
=
|
27618 |
[U52(x1)] |
=
|
4018 |
[U61(x1)] |
=
|
3 |
[U51#(x1, x2)] |
=
|
0 |
[e] |
=
|
45054 |
[U11#(x1)] |
=
|
0 |
[active(x1)] |
=
|
1 |
[U31(x1)] |
=
|
x1 + 1 |
[U41#(x1, x2)] |
=
|
0 |
[active#(x1)] |
=
|
0 |
[U21#(x1, x2)] |
=
|
0 |
[U81(x1)] |
=
|
3 |
[U22#(x1)] |
=
|
0 |
[tt] |
=
|
2 |
[U71#(x1, x2)] |
=
|
0 |
[U22(x1)] |
=
|
2 |
[U51(x1, x2)] |
=
|
2 |
[U41(x1, x2)] |
=
|
2 |
[U31#(x1)] |
=
|
0 |
[__(x1, x2)] |
=
|
3 |
[U61#(x1)] |
=
|
0 |
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
pair
isQid#(ok(X)) |
→ |
isQid#(X) |
(178) |
could be deleted.
1.1.21.1 Dependency Graph Processor
The dependency pairs are split into 0
components.