The rewrite relation of the following TRS is considered.
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(X,nil)) | → | mark(X) | (2) |
active(__(nil,X)) | → | mark(X) | (3) |
active(and(tt,X)) | → | mark(X) | (4) |
active(isList(V)) | → | mark(isNeList(V)) | (5) |
active(isList(nil)) | → | mark(tt) | (6) |
active(isList(__(V1,V2))) | → | mark(and(isList(V1),isList(V2))) | (7) |
active(isNeList(V)) | → | mark(isQid(V)) | (8) |
active(isNeList(__(V1,V2))) | → | mark(and(isList(V1),isNeList(V2))) | (9) |
active(isNeList(__(V1,V2))) | → | mark(and(isNeList(V1),isList(V2))) | (10) |
active(isNePal(V)) | → | mark(isQid(V)) | (11) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
active(isPal(V)) | → | mark(isNePal(V)) | (13) |
active(isPal(nil)) | → | mark(tt) | (14) |
active(isQid(a)) | → | mark(tt) | (15) |
active(isQid(e)) | → | mark(tt) | (16) |
active(isQid(i)) | → | mark(tt) | (17) |
active(isQid(o)) | → | mark(tt) | (18) |
active(isQid(u)) | → | mark(tt) | (19) |
active(__(X1,X2)) | → | __(active(X1),X2) | (20) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (21) |
active(and(X1,X2)) | → | and(active(X1),X2) | (22) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (26) |
proper(nil) | → | ok(nil) | (27) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (28) |
proper(tt) | → | ok(tt) | (29) |
proper(isList(X)) | → | isList(proper(X)) | (30) |
proper(isNeList(X)) | → | isNeList(proper(X)) | (31) |
proper(isQid(X)) | → | isQid(proper(X)) | (32) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (33) |
proper(isPal(X)) | → | isPal(proper(X)) | (34) |
proper(a) | → | ok(a) | (35) |
proper(e) | → | ok(e) | (36) |
proper(i) | → | ok(i) | (37) |
proper(o) | → | ok(o) | (38) |
proper(u) | → | ok(u) | (39) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
isPal(ok(X)) | → | ok(isPal(X)) | (46) |
top(mark(X)) | → | top(proper(X)) | (47) |
top(ok(X)) | → | top(active(X)) | (48) |
isPal#(ok(X)) | → | isPal#(X) | (49) |
proper#(isPal(X)) | → | isPal#(proper(X)) | (50) |
active#(isList(__(V1,V2))) | → | isList#(V1) | (51) |
proper#(isNePal(X)) | → | proper#(X) | (52) |
proper#(isQid(X)) | → | proper#(X) | (53) |
active#(and(X1,X2)) | → | active#(X1) | (54) |
active#(and(X1,X2)) | → | and#(active(X1),X2) | (55) |
isQid#(ok(X)) | → | isQid#(X) | (56) |
proper#(__(X1,X2)) | → | __#(proper(X1),proper(X2)) | (57) |
active#(__(__(X,Y),Z)) | → | __#(Y,Z) | (58) |
proper#(__(X1,X2)) | → | proper#(X1) | (59) |
proper#(and(X1,X2)) | → | and#(proper(X1),proper(X2)) | (60) |
top#(mark(X)) | → | proper#(X) | (61) |
proper#(and(X1,X2)) | → | proper#(X2) | (62) |
active#(__(X1,X2)) | → | active#(X2) | (63) |
active#(isNeList(__(V1,V2))) | → | isNeList#(V2) | (64) |
__#(ok(X1),ok(X2)) | → | __#(X1,X2) | (65) |
active#(isNeList(__(V1,V2))) | → | and#(isList(V1),isNeList(V2)) | (66) |
proper#(isList(X)) | → | proper#(X) | (67) |
proper#(isList(X)) | → | isList#(proper(X)) | (68) |
proper#(isQid(X)) | → | isQid#(proper(X)) | (69) |
active#(isNeList(__(V1,V2))) | → | isList#(V1) | (70) |
active#(isNeList(__(V1,V2))) | → | and#(isNeList(V1),isList(V2)) | (71) |
active#(isNePal(V)) | → | isQid#(V) | (72) |
active#(isList(__(V1,V2))) | → | isList#(V2) | (73) |
active#(__(__(X,Y),Z)) | → | __#(X,__(Y,Z)) | (74) |
proper#(__(X1,X2)) | → | proper#(X2) | (75) |
and#(mark(X1),X2) | → | and#(X1,X2) | (76) |
active#(isNePal(__(I,__(P,I)))) | → | isPal#(P) | (77) |
top#(ok(X)) | → | top#(active(X)) | (78) |
proper#(and(X1,X2)) | → | proper#(X1) | (79) |
active#(isPal(V)) | → | isNePal#(V) | (80) |
active#(isNeList(__(V1,V2))) | → | isList#(V2) | (81) |
top#(mark(X)) | → | top#(proper(X)) | (82) |
proper#(isPal(X)) | → | proper#(X) | (83) |
active#(isList(__(V1,V2))) | → | and#(isList(V1),isList(V2)) | (84) |
proper#(isNeList(X)) | → | proper#(X) | (85) |
proper#(isNePal(X)) | → | isNePal#(proper(X)) | (86) |
active#(__(X1,X2)) | → | active#(X1) | (87) |
isNePal#(ok(X)) | → | isNePal#(X) | (88) |
active#(isNeList(__(V1,V2))) | → | isNeList#(V1) | (89) |
active#(isNePal(__(I,__(P,I)))) | → | isQid#(I) | (90) |
active#(__(X1,X2)) | → | __#(active(X1),X2) | (91) |
active#(isList(V)) | → | isNeList#(V) | (92) |
proper#(isNeList(X)) | → | isNeList#(proper(X)) | (93) |
__#(mark(X1),X2) | → | __#(X1,X2) | (94) |
isList#(ok(X)) | → | isList#(X) | (95) |
isNeList#(ok(X)) | → | isNeList#(X) | (96) |
active#(isNeList(V)) | → | isQid#(V) | (97) |
top#(ok(X)) | → | active#(X) | (98) |
__#(X1,mark(X2)) | → | __#(X1,X2) | (99) |
and#(ok(X1),ok(X2)) | → | and#(X1,X2) | (100) |
active#(__(X1,X2)) | → | __#(X1,active(X2)) | (101) |
active#(isNePal(__(I,__(P,I)))) | → | and#(isQid(I),isPal(P)) | (102) |
The dependency pairs are split into 10 components.
top#(mark(X)) | → | top#(proper(X)) | (82) |
top#(ok(X)) | → | top#(active(X)) | (78) |
π(top#) | = | 1 |
π(__#) | = | 2 |
π(proper) | = | 1 |
π(ok) | = | 1 |
π(active) | = | 1 |
prec(a) | = | 6 | status(a) | = | [] | list-extension(a) | = | Lex | ||
prec(isNeList) | = | 6 | status(isNeList) | = | [1] | list-extension(isNeList) | = | Lex | ||
prec(isPal) | = | 8 | status(isPal) | = | [1] | list-extension(isPal) | = | Lex | ||
prec(u) | = | 4 | status(u) | = | [] | list-extension(u) | = | Lex | ||
prec(top) | = | 0 | status(top) | = | [] | list-extension(top) | = | Lex | ||
prec(and) | = | 6 | status(and) | = | [2, 1] | list-extension(and) | = | Lex | ||
prec(isNeList#) | = | 0 | status(isNeList#) | = | [] | list-extension(isNeList#) | = | Lex | ||
prec(isNePal) | = | 6 | status(isNePal) | = | [1] | list-extension(isNePal) | = | Lex | ||
prec(isQid#) | = | 0 | status(isQid#) | = | [] | list-extension(isQid#) | = | Lex | ||
prec(isPal#) | = | 0 | status(isPal#) | = | [] | list-extension(isPal#) | = | Lex | ||
prec(isQid) | = | 6 | status(isQid) | = | [] | list-extension(isQid) | = | Lex | ||
prec(o) | = | 4 | status(o) | = | [] | list-extension(o) | = | Lex | ||
prec(isList) | = | 7 | status(isList) | = | [1] | list-extension(isList) | = | Lex | ||
prec(isNePal#) | = | 0 | status(isNePal#) | = | [] | list-extension(isNePal#) | = | Lex | ||
prec(nil) | = | 6 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(mark) | = | 5 | 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) | = | 4 | status(i) | = | [] | list-extension(i) | = | Lex | ||
prec(e) | = | 4 | status(e) | = | [] | list-extension(e) | = | Lex | ||
prec(active#) | = | 0 | status(active#) | = | [] | list-extension(active#) | = | Lex | ||
prec(tt) | = | 1 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(and#) | = | 0 | status(and#) | = | [2, 1] | list-extension(and#) | = | Lex | ||
prec(__) | = | 8 | status(__) | = | [1, 2] | list-extension(__) | = | Lex |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 0 |
[isPal(x1)] | = | x1 + 0 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[isNeList#(x1)] | = | 0 |
[isNePal(x1)] | = | x1 + 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 0 |
[o] | = | 0 |
[isList(x1)] | = | x1 + 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 0 |
[e] | = | 0 |
[active#(x1)] | = | 0 |
[tt] | = | 0 |
[and#(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
[__(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
active(isQid(o)) | → | mark(tt) | (18) |
active(and(tt,X)) | → | mark(X) | (4) |
active(isQid(a)) | → | mark(tt) | (15) |
active(isNeList(V)) | → | mark(isQid(V)) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
active(isQid(e)) | → | mark(tt) | (16) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (21) |
proper(e) | → | ok(e) | (36) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (26) |
active(isQid(u)) | → | mark(tt) | (19) |
proper(isQid(X)) | → | isQid(proper(X)) | (32) |
active(isQid(i)) | → | mark(tt) | (17) |
proper(nil) | → | ok(nil) | (27) |
proper(isPal(X)) | → | isPal(proper(X)) | (34) |
active(and(X1,X2)) | → | and(active(X1),X2) | (22) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (28) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
active(isList(V)) | → | mark(isNeList(V)) | (5) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (33) |
active(isNeList(__(V1,V2))) | → | mark(and(isNeList(V1),isList(V2))) | (10) |
proper(u) | → | ok(u) | (39) |
active(isList(__(V1,V2))) | → | mark(and(isList(V1),isList(V2))) | (7) |
active(__(X1,X2)) | → | __(active(X1),X2) | (20) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
proper(isList(X)) | → | isList(proper(X)) | (30) |
active(isPal(nil)) | → | mark(tt) | (14) |
proper(isNeList(X)) | → | isNeList(proper(X)) | (31) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
active(isNePal(V)) | → | mark(isQid(V)) | (11) |
active(isNeList(__(V1,V2))) | → | mark(and(isList(V1),isNeList(V2))) | (9) |
active(isPal(V)) | → | mark(isNePal(V)) | (13) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
active(isList(nil)) | → | mark(tt) | (6) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
isPal(ok(X)) | → | ok(isPal(X)) | (46) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
active(__(X,nil)) | → | mark(X) | (2) |
top#(mark(X)) | → | top#(proper(X)) | (82) |
The dependency pairs are split into 1 component.
top#(ok(X)) | → | top#(active(X)) | (78) |
[a] | = | 1 |
[isNeList(x1)] | = | x1 + 0 |
[isPal(x1)] | = | x1 + 0 |
[u] | = | 1 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + 0 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | x1 + 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 0 |
[o] | = | 1 |
[proper(x1)] | = | 3 |
[ok(x1)] | = | x1 + 2 |
[isList(x1)] | = | x1 + 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 1 |
[e] | = | 1 |
[active(x1)] | = | x1 + 1 |
[active#(x1)] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + 0 |
active(isQid(o)) | → | mark(tt) | (18) |
active(and(tt,X)) | → | mark(X) | (4) |
active(isQid(a)) | → | mark(tt) | (15) |
active(isNeList(V)) | → | mark(isQid(V)) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
active(isQid(e)) | → | mark(tt) | (16) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (21) |
proper(e) | → | ok(e) | (36) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (26) |
active(isQid(u)) | → | mark(tt) | (19) |
proper(isQid(X)) | → | isQid(proper(X)) | (32) |
active(isQid(i)) | → | mark(tt) | (17) |
proper(nil) | → | ok(nil) | (27) |
proper(isPal(X)) | → | isPal(proper(X)) | (34) |
active(and(X1,X2)) | → | and(active(X1),X2) | (22) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (28) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
active(isList(V)) | → | mark(isNeList(V)) | (5) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (33) |
active(isNeList(__(V1,V2))) | → | mark(and(isNeList(V1),isList(V2))) | (10) |
proper(u) | → | ok(u) | (39) |
active(isList(__(V1,V2))) | → | mark(and(isList(V1),isList(V2))) | (7) |
active(__(X1,X2)) | → | __(active(X1),X2) | (20) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
proper(isList(X)) | → | isList(proper(X)) | (30) |
active(isPal(nil)) | → | mark(tt) | (14) |
proper(isNeList(X)) | → | isNeList(proper(X)) | (31) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
active(isNePal(V)) | → | mark(isQid(V)) | (11) |
active(isNeList(__(V1,V2))) | → | mark(and(isList(V1),isNeList(V2))) | (9) |
active(isPal(V)) | → | mark(isNePal(V)) | (13) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
active(isList(nil)) | → | mark(tt) | (6) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
isPal(ok(X)) | → | ok(isPal(X)) | (46) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
active(__(X,nil)) | → | mark(X) | (2) |
top#(ok(X)) | → | top#(active(X)) | (78) |
The dependency pairs are split into 0 components.
active#(__(X1,X2)) | → | active#(X2) | (63) |
active#(__(X1,X2)) | → | active#(X1) | (87) |
active#(and(X1,X2)) | → | active#(X1) | (54) |
[a] | = | 0 |
[isNeList(x1)] | = | 0 |
[isPal(x1)] | = | 1 |
[u] | = | 33049 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | x1 + 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 0 |
[o] | = | 1 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 41531 |
[e] | = | 625 |
[active(x1)] | = | x1 + 2 |
[active#(x1)] | = | x1 + 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 0 |
active(isQid(o)) | → | mark(tt) | (18) |
active(and(tt,X)) | → | mark(X) | (4) |
active(isQid(a)) | → | mark(tt) | (15) |
active(isNeList(V)) | → | mark(isQid(V)) | (8) |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(nil,X)) | → | mark(X) | (3) |
active(isQid(e)) | → | mark(tt) | (16) |
active(__(X1,X2)) | → | __(X1,active(X2)) | (21) |
proper(e) | → | ok(e) | (36) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (26) |
active(isQid(u)) | → | mark(tt) | (19) |
proper(isQid(X)) | → | isQid(proper(X)) | (32) |
active(isQid(i)) | → | mark(tt) | (17) |
proper(nil) | → | ok(nil) | (27) |
proper(isPal(X)) | → | isPal(proper(X)) | (34) |
active(and(X1,X2)) | → | and(active(X1),X2) | (22) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (28) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
active(isList(V)) | → | mark(isNeList(V)) | (5) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (33) |
active(isNeList(__(V1,V2))) | → | mark(and(isNeList(V1),isList(V2))) | (10) |
proper(u) | → | ok(u) | (39) |
active(isList(__(V1,V2))) | → | mark(and(isList(V1),isList(V2))) | (7) |
active(__(X1,X2)) | → | __(active(X1),X2) | (20) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
proper(isList(X)) | → | isList(proper(X)) | (30) |
active(isPal(nil)) | → | mark(tt) | (14) |
proper(isNeList(X)) | → | isNeList(proper(X)) | (31) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
active(isNePal(V)) | → | mark(isQid(V)) | (11) |
active(isNeList(__(V1,V2))) | → | mark(and(isList(V1),isNeList(V2))) | (9) |
active(isPal(V)) | → | mark(isNePal(V)) | (13) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
active(isList(nil)) | → | mark(tt) | (6) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
isPal(ok(X)) | → | ok(isPal(X)) | (46) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
active(__(X,nil)) | → | mark(X) | (2) |
active#(and(X1,X2)) | → | active#(X1) | (54) |
The dependency pairs are split into 1 component.
active#(__(X1,X2)) | → | active#(X2) | (63) |
active#(__(X1,X2)) | → | active#(X1) | (87) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 0 |
[isPal(x1)] | = | 1 |
[u] | = | 33049 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 0 |
[o] | = | 1 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | 0 |
[isList(x1)] | = | x1 + 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 41531 |
[e] | = | 1 |
[active(x1)] | = | 2 |
[active#(x1)] | = | x1 + 0 |
[tt] | = | 3 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
active(isNeList(V)) | → | mark(isQid(V)) | (8) |
proper(e) | → | ok(e) | (36) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (26) |
proper(isQid(X)) | → | isQid(proper(X)) | (32) |
proper(nil) | → | ok(nil) | (27) |
proper(isPal(X)) | → | isPal(proper(X)) | (34) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (28) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (33) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
proper(isList(X)) | → | isList(proper(X)) | (30) |
proper(isNeList(X)) | → | isNeList(proper(X)) | (31) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
active(isNePal(V)) | → | mark(isQid(V)) | (11) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
isPal(ok(X)) | → | ok(isPal(X)) | (46) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
active#(__(X1,X2)) | → | active#(X2) | (63) |
active#(__(X1,X2)) | → | active#(X1) | (87) |
The dependency pairs are split into 0 components.
proper#(__(X1,X2)) | → | proper#(X2) | (75) |
proper#(isList(X)) | → | proper#(X) | (67) |
proper#(and(X1,X2)) | → | proper#(X2) | (62) |
proper#(__(X1,X2)) | → | proper#(X1) | (59) |
proper#(isNeList(X)) | → | proper#(X) | (85) |
proper#(isPal(X)) | → | proper#(X) | (83) |
proper#(isQid(X)) | → | proper#(X) | (53) |
proper#(and(X1,X2)) | → | proper#(X1) | (79) |
proper#(isNePal(X)) | → | proper#(X) | (52) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 0 |
[isPal(x1)] | = | x1 + 2 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 0 |
[o] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | 0 |
[isList(x1)] | = | x1 + 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | x1 + 0 |
[i] | = | 0 |
[e] | = | 0 |
[active(x1)] | = | 2 |
[active#(x1)] | = | 0 |
[tt] | = | 3 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
proper(e) | → | ok(e) | (36) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (26) |
proper(isQid(X)) | → | isQid(proper(X)) | (32) |
proper(nil) | → | ok(nil) | (27) |
proper(isPal(X)) | → | isPal(proper(X)) | (34) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (28) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (33) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
proper(isList(X)) | → | isList(proper(X)) | (30) |
proper(isNeList(X)) | → | isNeList(proper(X)) | (31) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
isPal(ok(X)) | → | ok(isPal(X)) | (46) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
proper#(__(X1,X2)) | → | proper#(X2) | (75) |
proper#(and(X1,X2)) | → | proper#(X2) | (62) |
proper#(__(X1,X2)) | → | proper#(X1) | (59) |
proper#(isPal(X)) | → | proper#(X) | (83) |
proper#(and(X1,X2)) | → | proper#(X1) | (79) |
The dependency pairs are split into 1 component.
proper#(isQid(X)) | → | proper#(X) | (53) |
proper#(isNePal(X)) | → | proper#(X) | (52) |
proper#(isList(X)) | → | proper#(X) | (67) |
proper#(isNeList(X)) | → | proper#(X) | (85) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 16336 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 0 |
[o] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | x1 + 0 |
[isList(x1)] | = | x1 + 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | x1 + 0 |
[i] | = | 0 |
[e] | = | 0 |
[active(x1)] | = | 2 |
[active#(x1)] | = | 0 |
[tt] | = | 3 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
proper(e) | → | ok(e) | (36) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (26) |
proper(isQid(X)) | → | isQid(proper(X)) | (32) |
proper(nil) | → | ok(nil) | (27) |
proper(isPal(X)) | → | isPal(proper(X)) | (34) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (28) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (33) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
proper(isList(X)) | → | isList(proper(X)) | (30) |
proper(isNeList(X)) | → | isNeList(proper(X)) | (31) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
isPal(ok(X)) | → | ok(isPal(X)) | (46) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
proper#(isNePal(X)) | → | proper#(X) | (52) |
proper#(isNeList(X)) | → | proper#(X) | (85) |
The dependency pairs are split into 1 component.
proper#(isQid(X)) | → | proper#(X) | (53) |
proper#(isList(X)) | → | proper#(X) | (67) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 2 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 1 |
[o] | = | 0 |
[proper(x1)] | = | x1 + 0 |
[ok(x1)] | = | x1 + 0 |
[isList(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | x1 + 0 |
[i] | = | 0 |
[e] | = | 0 |
[active(x1)] | = | 3 |
[active#(x1)] | = | 0 |
[tt] | = | 4 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
proper(e) | → | ok(e) | (36) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (26) |
proper(isQid(X)) | → | isQid(proper(X)) | (32) |
proper(nil) | → | ok(nil) | (27) |
proper(isPal(X)) | → | isPal(proper(X)) | (34) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (28) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (33) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
proper(isList(X)) | → | isList(proper(X)) | (30) |
proper(isNeList(X)) | → | isNeList(proper(X)) | (31) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
isPal(ok(X)) | → | ok(isPal(X)) | (46) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
proper#(isQid(X)) | → | proper#(X) | (53) |
proper#(isList(X)) | → | proper#(X) | (67) |
The dependency pairs are split into 0 components.
isNeList#(ok(X)) | → | isNeList#(X) | (96) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 1 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | x1 + 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 1 |
[o] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[isList(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 0 |
[mark(x1)] | = | 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 0 |
[e] | = | 0 |
[active(x1)] | = | 1 |
[active#(x1)] | = | 0 |
[tt] | = | 28386 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x2 + 2 |
proper(e) | → | ok(e) | (36) |
proper(nil) | → | ok(nil) | (27) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
isNeList#(ok(X)) | → | isNeList#(X) | (96) |
The dependency pairs are split into 0 components.
isNePal#(ok(X)) | → | isNePal#(X) | (88) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 1 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 37043 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 52626 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 1 |
[o] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[isList(x1)] | = | x1 + 31274 |
[isNePal#(x1)] | = | x1 + 0 |
[nil] | = | 0 |
[mark(x1)] | = | 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 0 |
[e] | = | 0 |
[active(x1)] | = | 1 |
[active#(x1)] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x2 + 2 |
proper(e) | → | ok(e) | (36) |
proper(nil) | → | ok(nil) | (27) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
isNePal#(ok(X)) | → | isNePal#(X) | (88) |
The dependency pairs are split into 0 components.
and#(mark(X1),X2) | → | and#(X1,X2) | (76) |
and#(ok(X1),ok(X2)) | → | and#(X1,X2) | (100) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 1 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 37043 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 52626 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 1 |
[o] | = | 0 |
[proper(x1)] | = | x1 + 1 |
[ok(x1)] | = | x1 + 1 |
[isList(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 0 |
[mark(x1)] | = | 0 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 0 |
[e] | = | 0 |
[active(x1)] | = | 1 |
[active#(x1)] | = | 0 |
[tt] | = | 13363 |
[and#(x1, x2)] | = | x2 + 0 |
[__(x1, x2)] | = | x2 + 2 |
proper(e) | → | ok(e) | (36) |
proper(nil) | → | ok(nil) | (27) |
isQid(ok(X)) | → | ok(isQid(X)) | (44) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (23) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (24) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (40) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
and#(ok(X1),ok(X2)) | → | and#(X1,X2) | (100) |
The dependency pairs are split into 1 component.
and#(mark(X1),X2) | → | and#(X1,X2) | (76) |
[a] | = | 1 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 1 |
[u] | = | 1 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 19458 |
[o] | = | 1 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | 2 |
[isList(x1)] | = | 2 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 1 |
[e] | = | 1 |
[active(x1)] | = | 19461 |
[active#(x1)] | = | 0 |
[tt] | = | 4 |
[and#(x1, x2)] | = | x1 + 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
proper(e) | → | ok(e) | (36) |
proper(nil) | → | ok(nil) | (27) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
and#(mark(X1),X2) | → | and#(X1,X2) | (76) |
The dependency pairs are split into 0 components.
isQid#(ok(X)) | → | isQid#(X) | (56) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 1 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 0 |
[isQid#(x1)] | = | x1 + 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 19458 |
[o] | = | 0 |
[proper(x1)] | = | 19457 |
[ok(x1)] | = | x1 + 1 |
[isList(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 11028 |
[e] | = | 19456 |
[active(x1)] | = | 19461 |
[active#(x1)] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
proper(e) | → | ok(e) | (36) |
proper(nil) | → | ok(nil) | (27) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
isQid#(ok(X)) | → | isQid#(X) | (56) |
The dependency pairs are split into 0 components.
__#(X1,mark(X2)) | → | __#(X1,X2) | (99) |
__#(mark(X1),X2) | → | __#(X1,X2) | (94) |
__#(ok(X1),ok(X2)) | → | __#(X1,X2) | (65) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 1 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | x2 + 0 |
[isNePal(x1)] | = | x1 + 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 3 |
[o] | = | 0 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | x1 + 1 |
[isList(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 1 |
[e] | = | 1 |
[active(x1)] | = | 6 |
[active#(x1)] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
proper(e) | → | ok(e) | (36) |
proper(nil) | → | ok(nil) | (27) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
__#(X1,mark(X2)) | → | __#(X1,X2) | (99) |
__#(ok(X1),ok(X2)) | → | __#(X1,X2) | (65) |
The dependency pairs are split into 1 component.
__#(mark(X1),X2) | → | __#(X1,X2) | (94) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 1 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | x1 + 0 |
[isNePal(x1)] | = | x1 + 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 3 |
[o] | = | 0 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | x1 + 1 |
[isList(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 1 |
[e] | = | 1 |
[active(x1)] | = | 9 |
[active#(x1)] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
proper(e) | → | ok(e) | (36) |
proper(nil) | → | ok(nil) | (27) |
proper(u) | → | ok(u) | (39) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (45) |
proper(o) | → | ok(o) | (38) |
proper(i) | → | ok(i) | (37) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
proper(a) | → | ok(a) | (35) |
proper(tt) | → | ok(tt) | (29) |
__#(mark(X1),X2) | → | __#(X1,X2) | (94) |
The dependency pairs are split into 0 components.
isList#(ok(X)) | → | isList#(X) | (95) |
[a] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | 1 |
[u] | = | 0 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 17028 |
[o] | = | 0 |
[proper(x1)] | = | 2 |
[ok(x1)] | = | x1 + 1 |
[isList(x1)] | = | x1 + 2631 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 30479 |
[mark(x1)] | = | x1 + 38373 |
[isList#(x1)] | = | x1 + 0 |
[proper#(x1)] | = | 0 |
[i] | = | 1 |
[e] | = | 1 |
[active(x1)] | = | 55401 |
[active#(x1)] | = | 0 |
[tt] | = | 17029 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (25) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (41) |
isList(ok(X)) | → | ok(isList(X)) | (42) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (43) |
isList#(ok(X)) | → | isList#(X) | (95) |
The dependency pairs are split into 0 components.
isPal#(ok(X)) | → | isPal#(X) | (49) |
[a] | = | 1 |
[isNeList(x1)] | = | 2 |
[isPal(x1)] | = | 3011 |
[u] | = | 29191 |
[top(x1)] | = | 0 |
[and(x1, x2)] | = | 3 |
[isNeList#(x1)] | = | 0 |
[top#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 19504 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | x1 + 0 |
[isQid(x1)] | = | 28580 |
[o] | = | 28252 |
[proper(x1)] | = | 1 |
[ok(x1)] | = | x1 + 2 |
[isList(x1)] | = | 13856 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 21885 |
[mark(x1)] | = | 4 |
[isList#(x1)] | = | 0 |
[proper#(x1)] | = | 0 |
[i] | = | 3103 |
[e] | = | 32755 |
[active(x1)] | = | 1 |
[active#(x1)] | = | 0 |
[tt] | = | 17029 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | 2 |
isPal#(ok(X)) | → | isPal#(X) | (49) |
The dependency pairs are split into 0 components.