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) |
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (20) |
mark(nil) | → | active(nil) | (21) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (22) |
mark(tt) | → | active(tt) | (23) |
mark(isList(X)) | → | active(isList(X)) | (24) |
mark(isNeList(X)) | → | active(isNeList(X)) | (25) |
mark(isQid(X)) | → | active(isQid(X)) | (26) |
mark(isNePal(X)) | → | active(isNePal(X)) | (27) |
mark(isPal(X)) | → | active(isPal(X)) | (28) |
mark(a) | → | active(a) | (29) |
mark(e) | → | active(e) | (30) |
mark(i) | → | active(i) | (31) |
mark(o) | → | active(o) | (32) |
mark(u) | → | active(u) | (33) |
__(mark(X1),X2) | → | __(X1,X2) | (34) |
__(X1,mark(X2)) | → | __(X1,X2) | (35) |
__(active(X1),X2) | → | __(X1,X2) | (36) |
__(X1,active(X2)) | → | __(X1,X2) | (37) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
isList(mark(X)) | → | isList(X) | (42) |
isList(active(X)) | → | isList(X) | (43) |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
isQid(mark(X)) | → | isQid(X) | (46) |
isQid(active(X)) | → | isQid(X) | (47) |
isNePal(mark(X)) | → | isNePal(X) | (48) |
isNePal(active(X)) | → | isNePal(X) | (49) |
isPal(mark(X)) | → | isPal(X) | (50) |
isPal(active(X)) | → | isPal(X) | (51) |
isList#(active(X)) | → | isList#(X) | (52) |
and#(X1,mark(X2)) | → | and#(X1,X2) | (53) |
active#(isNePal(__(I,__(P,I)))) | → | isPal#(P) | (54) |
mark#(__(X1,X2)) | → | active#(__(mark(X1),mark(X2))) | (55) |
active#(__(__(X,Y),Z)) | → | mark#(__(X,__(Y,Z))) | (56) |
active#(isNeList(__(V1,V2))) | → | isNeList#(V1) | (57) |
active#(isList(__(V1,V2))) | → | isList#(V2) | (58) |
active#(isList(__(V1,V2))) | → | isList#(V1) | (59) |
mark#(__(X1,X2)) | → | mark#(X1) | (60) |
isPal#(mark(X)) | → | isPal#(X) | (61) |
active#(isNeList(__(V1,V2))) | → | isList#(V2) | (62) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (63) |
active#(isQid(a)) | → | mark#(tt) | (64) |
mark#(u) | → | active#(u) | (65) |
active#(isQid(o)) | → | mark#(tt) | (66) |
active#(isQid(i)) | → | mark#(tt) | (67) |
mark#(isQid(X)) | → | active#(isQid(X)) | (68) |
mark#(__(X1,X2)) | → | mark#(X2) | (69) |
isList#(mark(X)) | → | isList#(X) | (70) |
mark#(o) | → | active#(o) | (71) |
mark#(and(X1,X2)) | → | mark#(X1) | (72) |
active#(__(__(X,Y),Z)) | → | __#(X,__(Y,Z)) | (73) |
active#(isList(__(V1,V2))) | → | and#(isList(V1),isList(V2)) | (74) |
isNeList#(mark(X)) | → | isNeList#(X) | (75) |
and#(active(X1),X2) | → | and#(X1,X2) | (76) |
isQid#(active(X)) | → | isQid#(X) | (77) |
and#(mark(X1),X2) | → | and#(X1,X2) | (78) |
mark#(isNePal(X)) | → | active#(isNePal(X)) | (79) |
mark#(tt) | → | active#(tt) | (80) |
active#(isNeList(V)) | → | isQid#(V) | (81) |
mark#(isList(X)) | → | active#(isList(X)) | (82) |
active#(isNeList(__(V1,V2))) | → | and#(isNeList(V1),isList(V2)) | (83) |
active#(isNeList(V)) | → | mark#(isQid(V)) | (84) |
active#(isList(nil)) | → | mark#(tt) | (85) |
active#(isPal(nil)) | → | mark#(tt) | (86) |
__#(mark(X1),X2) | → | __#(X1,X2) | (87) |
isPal#(active(X)) | → | isPal#(X) | (88) |
__#(active(X1),X2) | → | __#(X1,X2) | (89) |
mark#(i) | → | active#(i) | (90) |
mark#(isPal(X)) | → | active#(isPal(X)) | (91) |
active#(isList(V)) | → | mark#(isNeList(V)) | (92) |
isNeList#(active(X)) | → | isNeList#(X) | (93) |
active#(isNeList(__(V1,V2))) | → | isNeList#(V2) | (94) |
and#(X1,active(X2)) | → | and#(X1,X2) | (95) |
active#(isList(__(V1,V2))) | → | mark#(and(isList(V1),isList(V2))) | (96) |
isNePal#(mark(X)) | → | isNePal#(X) | (97) |
active#(isQid(e)) | → | mark#(tt) | (98) |
isNePal#(active(X)) | → | isNePal#(X) | (99) |
active#(and(tt,X)) | → | mark#(X) | (100) |
isQid#(mark(X)) | → | isQid#(X) | (101) |
active#(isNeList(__(V1,V2))) | → | mark#(and(isNeList(V1),isList(V2))) | (102) |
active#(__(nil,X)) | → | mark#(X) | (103) |
active#(isNePal(__(I,__(P,I)))) | → | isQid#(I) | (104) |
active#(isNePal(V)) | → | isQid#(V) | (105) |
mark#(isNeList(X)) | → | active#(isNeList(X)) | (106) |
active#(isNePal(__(I,__(P,I)))) | → | and#(isQid(I),isPal(P)) | (107) |
active#(isQid(u)) | → | mark#(tt) | (108) |
active#(isNeList(__(V1,V2))) | → | mark#(and(isList(V1),isNeList(V2))) | (109) |
mark#(e) | → | active#(e) | (110) |
active#(isNeList(__(V1,V2))) | → | isList#(V1) | (111) |
mark#(nil) | → | active#(nil) | (112) |
active#(isNePal(__(I,__(P,I)))) | → | mark#(and(isQid(I),isPal(P))) | (113) |
active#(__(__(X,Y),Z)) | → | __#(Y,Z) | (114) |
mark#(__(X1,X2)) | → | __#(mark(X1),mark(X2)) | (115) |
active#(isNePal(V)) | → | mark#(isQid(V)) | (116) |
active#(isPal(V)) | → | isNePal#(V) | (117) |
mark#(a) | → | active#(a) | (118) |
active#(__(X,nil)) | → | mark#(X) | (119) |
mark#(and(X1,X2)) | → | and#(mark(X1),X2) | (120) |
__#(X1,active(X2)) | → | __#(X1,X2) | (121) |
active#(isPal(V)) | → | mark#(isNePal(V)) | (122) |
__#(X1,mark(X2)) | → | __#(X1,X2) | (123) |
active#(isList(V)) | → | isNeList#(V) | (124) |
active#(isNeList(__(V1,V2))) | → | and#(isList(V1),isNeList(V2)) | (125) |
The dependency pairs are split into 8 components.
mark#(isPal(X)) | → | active#(isPal(X)) | (91) |
active#(isList(V)) | → | mark#(isNeList(V)) | (92) |
active#(isPal(V)) | → | mark#(isNePal(V)) | (122) |
active#(isNeList(V)) | → | mark#(isQid(V)) | (84) |
active#(__(X,nil)) | → | mark#(X) | (119) |
mark#(isList(X)) | → | active#(isList(X)) | (82) |
active#(isNePal(V)) | → | mark#(isQid(V)) | (116) |
mark#(isNePal(X)) | → | active#(isNePal(X)) | (79) |
active#(isNePal(__(I,__(P,I)))) | → | mark#(and(isQid(I),isPal(P))) | (113) |
active#(isNeList(__(V1,V2))) | → | mark#(and(isList(V1),isNeList(V2))) | (109) |
mark#(and(X1,X2)) | → | mark#(X1) | (72) |
mark#(isQid(X)) | → | active#(isQid(X)) | (68) |
mark#(__(X1,X2)) | → | mark#(X2) | (69) |
mark#(isNeList(X)) | → | active#(isNeList(X)) | (106) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (63) |
active#(__(nil,X)) | → | mark#(X) | (103) |
active#(isNeList(__(V1,V2))) | → | mark#(and(isNeList(V1),isList(V2))) | (102) |
active#(and(tt,X)) | → | mark#(X) | (100) |
mark#(__(X1,X2)) | → | mark#(X1) | (60) |
active#(__(__(X,Y),Z)) | → | mark#(__(X,__(Y,Z))) | (56) |
active#(isList(__(V1,V2))) | → | mark#(and(isList(V1),isList(V2))) | (96) |
mark#(__(X1,X2)) | → | active#(__(mark(X1),mark(X2))) | (55) |
[a] | = | 1 |
[isNeList(x1)] | = | 2 |
[isPal(x1)] | = | 2 |
[u] | = | 1 |
[and(x1, x2)] | = | 2 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 2 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 1 |
[o] | = | 1 |
[mark#(x1)] | = | 2 |
[isList(x1)] | = | 2 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[i] | = | 1 |
[e] | = | 1 |
[active(x1)] | = | 4 |
[active#(x1)] | = | x1 + 0 |
[tt] | = | 4 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | 2 |
isPal(mark(X)) | → | isPal(X) | (50) |
__(active(X1),X2) | → | __(X1,X2) | (36) |
__(mark(X1),X2) | → | __(X1,X2) | (34) |
isNeList(mark(X)) | → | isNeList(X) | (44) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
isNePal(active(X)) | → | isNePal(X) | (49) |
isNeList(active(X)) | → | isNeList(X) | (45) |
isPal(active(X)) | → | isPal(X) | (51) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
isNePal(mark(X)) | → | isNePal(X) | (48) |
isQid(active(X)) | → | isQid(X) | (47) |
__(X1,active(X2)) | → | __(X1,X2) | (37) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
isList(mark(X)) | → | isList(X) | (42) |
isQid(mark(X)) | → | isQid(X) | (46) |
__(X1,mark(X2)) | → | __(X1,X2) | (35) |
isList(active(X)) | → | isList(X) | (43) |
mark#(isQid(X)) | → | active#(isQid(X)) | (68) |
The dependency pairs are split into 1 component.
active#(and(tt,X)) | → | mark#(X) | (100) |
active#(isNeList(V)) | → | mark#(isQid(V)) | (84) |
active#(__(__(X,Y),Z)) | → | mark#(__(X,__(Y,Z))) | (56) |
active#(__(nil,X)) | → | mark#(X) | (103) |
mark#(isNePal(X)) | → | active#(isNePal(X)) | (79) |
mark#(and(X1,X2)) | → | mark#(X1) | (72) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (63) |
mark#(isPal(X)) | → | active#(isPal(X)) | (91) |
active#(isList(V)) | → | mark#(isNeList(V)) | (92) |
active#(isNeList(__(V1,V2))) | → | mark#(and(isNeList(V1),isList(V2))) | (102) |
active#(isList(__(V1,V2))) | → | mark#(and(isList(V1),isList(V2))) | (96) |
mark#(__(X1,X2)) | → | mark#(X2) | (69) |
mark#(__(X1,X2)) | → | mark#(X1) | (60) |
mark#(__(X1,X2)) | → | active#(__(mark(X1),mark(X2))) | (55) |
mark#(isNeList(X)) | → | active#(isNeList(X)) | (106) |
active#(isNePal(__(I,__(P,I)))) | → | mark#(and(isQid(I),isPal(P))) | (113) |
mark#(isList(X)) | → | active#(isList(X)) | (82) |
active#(isNePal(V)) | → | mark#(isQid(V)) | (116) |
active#(isNeList(__(V1,V2))) | → | mark#(and(isList(V1),isNeList(V2))) | (109) |
active#(isPal(V)) | → | mark#(isNePal(V)) | (122) |
active#(__(X,nil)) | → | mark#(X) | (119) |
[a] | = | 1 |
[isNeList(x1)] | = | x1 + 34106 |
[isPal(x1)] | = | x1 + 34107 |
[u] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 12330 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | x1 + 34106 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 34105 |
[o] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[isList(x1)] | = | x1 + 34107 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | x1 + 0 |
[isList#(x1)] | = | 0 |
[i] | = | 16468 |
[e] | = | 0 |
[active(x1)] | = | x1 + 0 |
[active#(x1)] | = | x1 + 0 |
[tt] | = | 584 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 46438 |
active(isQid(o)) | → | mark(tt) | (18) |
isPal(mark(X)) | → | isPal(X) | (50) |
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) |
mark(nil) | → | active(nil) | (21) |
__(active(X1),X2) | → | __(X1,X2) | (36) |
mark(isQid(X)) | → | active(isQid(X)) | (26) |
active(isQid(u)) | → | mark(tt) | (19) |
mark(o) | → | active(o) | (32) |
active(isQid(i)) | → | mark(tt) | (17) |
mark(isNePal(X)) | → | active(isNePal(X)) | (27) |
__(mark(X1),X2) | → | __(X1,X2) | (34) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (22) |
mark(isPal(X)) | → | active(isPal(X)) | (28) |
isNeList(mark(X)) | → | isNeList(X) | (44) |
active(isList(V)) | → | mark(isNeList(V)) | (5) |
mark(u) | → | active(u) | (33) |
active(isNeList(__(V1,V2))) | → | mark(and(isNeList(V1),isList(V2))) | (10) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
active(isList(__(V1,V2))) | → | mark(and(isList(V1),isList(V2))) | (7) |
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (20) |
mark(isNeList(X)) | → | active(isNeList(X)) | (25) |
isNePal(active(X)) | → | isNePal(X) | (49) |
mark(e) | → | active(e) | (30) |
active(isPal(nil)) | → | mark(tt) | (14) |
mark(i) | → | active(i) | (31) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
isNeList(active(X)) | → | isNeList(X) | (45) |
mark(tt) | → | active(tt) | (23) |
mark(isList(X)) | → | active(isList(X)) | (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) |
isPal(active(X)) | → | isPal(X) | (51) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
active(isList(nil)) | → | mark(tt) | (6) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
isNePal(mark(X)) | → | isNePal(X) | (48) |
isQid(active(X)) | → | isQid(X) | (47) |
__(X1,active(X2)) | → | __(X1,X2) | (37) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
isList(mark(X)) | → | isList(X) | (42) |
isQid(mark(X)) | → | isQid(X) | (46) |
__(X1,mark(X2)) | → | __(X1,X2) | (35) |
mark(a) | → | active(a) | (29) |
isList(active(X)) | → | isList(X) | (43) |
active(__(X,nil)) | → | mark(X) | (2) |
active#(and(tt,X)) | → | mark#(X) | (100) |
active#(isNeList(V)) | → | mark#(isQid(V)) | (84) |
active#(__(nil,X)) | → | mark#(X) | (103) |
mark#(and(X1,X2)) | → | mark#(X1) | (72) |
active#(isList(V)) | → | mark#(isNeList(V)) | (92) |
active#(isNeList(__(V1,V2))) | → | mark#(and(isNeList(V1),isList(V2))) | (102) |
active#(isList(__(V1,V2))) | → | mark#(and(isList(V1),isList(V2))) | (96) |
mark#(__(X1,X2)) | → | mark#(X2) | (69) |
mark#(__(X1,X2)) | → | mark#(X1) | (60) |
active#(isNePal(__(I,__(P,I)))) | → | mark#(and(isQid(I),isPal(P))) | (113) |
active#(isNePal(V)) | → | mark#(isQid(V)) | (116) |
active#(isNeList(__(V1,V2))) | → | mark#(and(isList(V1),isNeList(V2))) | (109) |
active#(isPal(V)) | → | mark#(isNePal(V)) | (122) |
active#(__(X,nil)) | → | mark#(X) | (119) |
The dependency pairs are split into 1 component.
active#(__(__(X,Y),Z)) | → | mark#(__(X,__(Y,Z))) | (56) |
mark#(isNePal(X)) | → | active#(isNePal(X)) | (79) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (63) |
mark#(isPal(X)) | → | active#(isPal(X)) | (91) |
mark#(__(X1,X2)) | → | active#(__(mark(X1),mark(X2))) | (55) |
mark#(isNeList(X)) | → | active#(isNeList(X)) | (106) |
mark#(isList(X)) | → | active#(isList(X)) | (82) |
[a] | = | 1 |
[isNeList(x1)] | = | 1 |
[isPal(x1)] | = | 625 |
[u] | = | 1 |
[and(x1, x2)] | = | 7066 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 2034 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 1 |
[o] | = | 1 |
[mark#(x1)] | = | 25537 |
[isList(x1)] | = | 25536 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 1 |
[mark(x1)] | = | 1 |
[isList#(x1)] | = | 0 |
[i] | = | 12330 |
[e] | = | 0 |
[active(x1)] | = | 1 |
[active#(x1)] | = | x1 + 0 |
[tt] | = | 0 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | 25537 |
active(isQid(o)) | → | mark(tt) | (18) |
isPal(mark(X)) | → | isPal(X) | (50) |
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) |
mark(nil) | → | active(nil) | (21) |
__(active(X1),X2) | → | __(X1,X2) | (36) |
mark(isQid(X)) | → | active(isQid(X)) | (26) |
active(isQid(u)) | → | mark(tt) | (19) |
mark(o) | → | active(o) | (32) |
active(isQid(i)) | → | mark(tt) | (17) |
mark(isNePal(X)) | → | active(isNePal(X)) | (27) |
__(mark(X1),X2) | → | __(X1,X2) | (34) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (22) |
mark(isPal(X)) | → | active(isPal(X)) | (28) |
isNeList(mark(X)) | → | isNeList(X) | (44) |
active(isList(V)) | → | mark(isNeList(V)) | (5) |
mark(u) | → | active(u) | (33) |
active(isNeList(__(V1,V2))) | → | mark(and(isNeList(V1),isList(V2))) | (10) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
active(isList(__(V1,V2))) | → | mark(and(isList(V1),isList(V2))) | (7) |
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (20) |
mark(isNeList(X)) | → | active(isNeList(X)) | (25) |
isNePal(active(X)) | → | isNePal(X) | (49) |
mark(e) | → | active(e) | (30) |
active(isPal(nil)) | → | mark(tt) | (14) |
mark(i) | → | active(i) | (31) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
isNeList(active(X)) | → | isNeList(X) | (45) |
mark(tt) | → | active(tt) | (23) |
mark(isList(X)) | → | active(isList(X)) | (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) |
isPal(active(X)) | → | isPal(X) | (51) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
active(isList(nil)) | → | mark(tt) | (6) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
isNePal(mark(X)) | → | isNePal(X) | (48) |
isQid(active(X)) | → | isQid(X) | (47) |
__(X1,active(X2)) | → | __(X1,X2) | (37) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
isList(mark(X)) | → | isList(X) | (42) |
isQid(mark(X)) | → | isQid(X) | (46) |
__(X1,mark(X2)) | → | __(X1,X2) | (35) |
mark(a) | → | active(a) | (29) |
isList(active(X)) | → | isList(X) | (43) |
active(__(X,nil)) | → | mark(X) | (2) |
mark#(isNePal(X)) | → | active#(isNePal(X)) | (79) |
mark#(and(X1,X2)) | → | active#(and(mark(X1),X2)) | (63) |
mark#(isPal(X)) | → | active#(isPal(X)) | (91) |
mark#(isNeList(X)) | → | active#(isNeList(X)) | (106) |
mark#(isList(X)) | → | active#(isList(X)) | (82) |
The dependency pairs are split into 1 component.
active#(__(__(X,Y),Z)) | → | mark#(__(X,__(Y,Z))) | (56) |
mark#(__(X1,X2)) | → | active#(__(mark(X1),mark(X2))) | (55) |
π(and) | = | 2 |
π(__#) | = | 1 |
π(isNePal#) | = | 1 |
π(mark) | = | 1 |
π(isList#) | = | 1 |
π(active) | = | 1 |
π(active#) | = | 1 |
π(and#) | = | 1 |
prec(a) | = | 3 | status(a) | = | [] | list-extension(a) | = | Lex | ||
prec(isNeList) | = | 0 | status(isNeList) | = | [] | list-extension(isNeList) | = | Lex | ||
prec(isPal) | = | 2 | status(isPal) | = | [] | list-extension(isPal) | = | Lex | ||
prec(u) | = | 3 | status(u) | = | [] | list-extension(u) | = | Lex | ||
prec(isNeList#) | = | 0 | status(isNeList#) | = | [] | list-extension(isNeList#) | = | Lex | ||
prec(isNePal) | = | 2 | status(isNePal) | = | [] | list-extension(isNePal) | = | Lex | ||
prec(isQid#) | = | 0 | status(isQid#) | = | [] | list-extension(isQid#) | = | Lex | ||
prec(isPal#) | = | 0 | status(isPal#) | = | [] | list-extension(isPal#) | = | Lex | ||
prec(isQid) | = | 0 | status(isQid) | = | [] | list-extension(isQid) | = | Lex | ||
prec(o) | = | 2 | status(o) | = | [] | list-extension(o) | = | Lex | ||
prec(mark#) | = | 1 | status(mark#) | = | [1] | list-extension(mark#) | = | Lex | ||
prec(isList) | = | 0 | status(isList) | = | [] | list-extension(isList) | = | Lex | ||
prec(nil) | = | 1 | status(nil) | = | [] | list-extension(nil) | = | Lex | ||
prec(i) | = | 2 | status(i) | = | [] | list-extension(i) | = | Lex | ||
prec(e) | = | 3 | status(e) | = | [] | list-extension(e) | = | Lex | ||
prec(tt) | = | 0 | status(tt) | = | [] | list-extension(tt) | = | Lex | ||
prec(__) | = | 2 | status(__) | = | [1, 2] | list-extension(__) | = | Lex |
[a] | = | 0 |
[isNeList(x1)] | = | 0 |
[isPal(x1)] | = | 0 |
[u] | = | 0 |
[isNeList#(x1)] | = | 0 |
[isNePal(x1)] | = | 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 0 |
[o] | = | 0 |
[mark#(x1)] | = | x1 + 0 |
[isList(x1)] | = | 0 |
[nil] | = | 0 |
[i] | = | 0 |
[e] | = | 0 |
[tt] | = | 0 |
[__(x1, x2)] | = | max(x1 + 0, x2 + 0, 0) |
active(isQid(o)) | → | mark(tt) | (18) |
isPal(mark(X)) | → | isPal(X) | (50) |
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) |
mark(nil) | → | active(nil) | (21) |
__(active(X1),X2) | → | __(X1,X2) | (36) |
mark(isQid(X)) | → | active(isQid(X)) | (26) |
active(isQid(u)) | → | mark(tt) | (19) |
mark(o) | → | active(o) | (32) |
active(isQid(i)) | → | mark(tt) | (17) |
mark(isNePal(X)) | → | active(isNePal(X)) | (27) |
__(mark(X1),X2) | → | __(X1,X2) | (34) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (22) |
mark(isPal(X)) | → | active(isPal(X)) | (28) |
isNeList(mark(X)) | → | isNeList(X) | (44) |
active(isList(V)) | → | mark(isNeList(V)) | (5) |
mark(u) | → | active(u) | (33) |
active(isNeList(__(V1,V2))) | → | mark(and(isNeList(V1),isList(V2))) | (10) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
active(isList(__(V1,V2))) | → | mark(and(isList(V1),isList(V2))) | (7) |
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (20) |
mark(isNeList(X)) | → | active(isNeList(X)) | (25) |
isNePal(active(X)) | → | isNePal(X) | (49) |
mark(e) | → | active(e) | (30) |
active(isPal(nil)) | → | mark(tt) | (14) |
mark(i) | → | active(i) | (31) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
isNeList(active(X)) | → | isNeList(X) | (45) |
mark(tt) | → | active(tt) | (23) |
mark(isList(X)) | → | active(isList(X)) | (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) |
isPal(active(X)) | → | isPal(X) | (51) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
active(isList(nil)) | → | mark(tt) | (6) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
isNePal(mark(X)) | → | isNePal(X) | (48) |
isQid(active(X)) | → | isQid(X) | (47) |
__(X1,active(X2)) | → | __(X1,X2) | (37) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
isList(mark(X)) | → | isList(X) | (42) |
isQid(mark(X)) | → | isQid(X) | (46) |
__(X1,mark(X2)) | → | __(X1,X2) | (35) |
mark(a) | → | active(a) | (29) |
isList(active(X)) | → | isList(X) | (43) |
active(__(X,nil)) | → | mark(X) | (2) |
active#(__(__(X,Y),Z)) | → | mark#(__(X,__(Y,Z))) | (56) |
mark#(__(X1,X2)) | → | active#(__(mark(X1),mark(X2))) | (55) |
The dependency pairs are split into 0 components.
isNePal#(active(X)) | → | isNePal#(X) | (99) |
isNePal#(mark(X)) | → | isNePal#(X) | (97) |
[a] | = | 0 |
[isNeList(x1)] | = | 437 |
[isPal(x1)] | = | 0 |
[u] | = | 0 |
[and(x1, x2)] | = | 0 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 32573 |
[o] | = | 0 |
[mark#(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | x1 + 0 |
[nil] | = | 25532 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[i] | = | 14459 |
[e] | = | 29273 |
[active(x1)] | = | x1 + 2 |
[active#(x1)] | = | 0 |
[tt] | = | 32575 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | 59112 |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
isNePal#(active(X)) | → | isNePal#(X) | (99) |
isNePal#(mark(X)) | → | isNePal#(X) | (97) |
The dependency pairs are split into 0 components.
__#(X1,mark(X2)) | → | __#(X1,X2) | (123) |
__#(active(X1),X2) | → | __#(X1,X2) | (89) |
__#(mark(X1),X2) | → | __#(X1,X2) | (87) |
__#(X1,active(X2)) | → | __#(X1,X2) | (121) |
[a] | = | 0 |
[isNeList(x1)] | = | 21096 |
[isPal(x1)] | = | 0 |
[u] | = | 0 |
[and(x1, x2)] | = | 0 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | x1 + x2 + 0 |
[isNePal(x1)] | = | 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 32573 |
[o] | = | 0 |
[mark#(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 25532 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[i] | = | 5592 |
[e] | = | 29273 |
[active(x1)] | = | x1 + 2 |
[active#(x1)] | = | 0 |
[tt] | = | 32575 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | 59112 |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
__#(X1,mark(X2)) | → | __#(X1,X2) | (123) |
__#(active(X1),X2) | → | __#(X1,X2) | (89) |
__#(mark(X1),X2) | → | __#(X1,X2) | (87) |
__#(X1,active(X2)) | → | __#(X1,X2) | (121) |
The dependency pairs are split into 0 components.
isQid#(active(X)) | → | isQid#(X) | (77) |
isQid#(mark(X)) | → | isQid#(X) | (101) |
[a] | = | 0 |
[isNeList(x1)] | = | 15082 |
[isPal(x1)] | = | 0 |
[u] | = | 0 |
[and(x1, x2)] | = | 0 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 1 |
[isQid#(x1)] | = | x1 + 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 16146 |
[o] | = | 0 |
[mark#(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 35774 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[i] | = | 25011 |
[e] | = | 23641 |
[active(x1)] | = | x1 + 2 |
[active#(x1)] | = | 0 |
[tt] | = | 16148 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | 1 |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
isQid#(active(X)) | → | isQid#(X) | (77) |
isQid#(mark(X)) | → | isQid#(X) | (101) |
The dependency pairs are split into 0 components.
isPal#(active(X)) | → | isPal#(X) | (88) |
isPal#(mark(X)) | → | isPal#(X) | (61) |
[a] | = | 0 |
[isNeList(x1)] | = | 28472 |
[isPal(x1)] | = | 0 |
[u] | = | 0 |
[and(x1, x2)] | = | 0 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | x1 + 0 |
[isQid(x1)] | = | 56944 |
[o] | = | 0 |
[mark#(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 11592 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[i] | = | 52626 |
[e] | = | 28255 |
[active(x1)] | = | x1 + 28472 |
[active#(x1)] | = | 0 |
[tt] | = | 85416 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | 1 |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
isPal#(active(X)) | → | isPal#(X) | (88) |
isPal#(mark(X)) | → | isPal#(X) | (61) |
The dependency pairs are split into 0 components.
and#(mark(X1),X2) | → | and#(X1,X2) | (78) |
and#(active(X1),X2) | → | and#(X1,X2) | (76) |
and#(X1,active(X2)) | → | and#(X1,X2) | (95) |
and#(X1,mark(X2)) | → | and#(X1,X2) | (53) |
[a] | = | 0 |
[isNeList(x1)] | = | 6438 |
[isPal(x1)] | = | 0 |
[u] | = | 0 |
[and(x1, x2)] | = | 0 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 26351 |
[o] | = | 0 |
[mark#(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 24928 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[i] | = | 30968 |
[e] | = | 28255 |
[active(x1)] | = | x1 + 2 |
[active#(x1)] | = | 0 |
[tt] | = | 26353 |
[and#(x1, x2)] | = | x2 + 0 |
[__(x1, x2)] | = | 32157 |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
and#(X1,active(X2)) | → | and#(X1,X2) | (95) |
and#(X1,mark(X2)) | → | and#(X1,X2) | (53) |
The dependency pairs are split into 1 component.
and#(active(X1),X2) | → | and#(X1,X2) | (76) |
and#(mark(X1),X2) | → | and#(X1,X2) | (78) |
[a] | = | 0 |
[isNeList(x1)] | = | 14757 |
[isPal(x1)] | = | 0 |
[u] | = | 0 |
[and(x1, x2)] | = | 0 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 23613 |
[o] | = | 0 |
[mark#(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 37749 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[i] | = | 15289 |
[e] | = | 18841 |
[active(x1)] | = | x1 + 2 |
[active#(x1)] | = | 0 |
[tt] | = | 23615 |
[and#(x1, x2)] | = | x1 + 0 |
[__(x1, x2)] | = | 32157 |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
and#(active(X1),X2) | → | and#(X1,X2) | (76) |
and#(mark(X1),X2) | → | and#(X1,X2) | (78) |
The dependency pairs are split into 0 components.
isList#(mark(X)) | → | isList#(X) | (70) |
isList#(active(X)) | → | isList#(X) | (52) |
[a] | = | 0 |
[isNeList(x1)] | = | 30216 |
[isPal(x1)] | = | 0 |
[u] | = | 0 |
[and(x1, x2)] | = | 0 |
[isNeList#(x1)] | = | 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 62219 |
[o] | = | 0 |
[mark#(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 12095 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | x1 + 0 |
[i] | = | 15289 |
[e] | = | 24817 |
[active(x1)] | = | x1 + 2 |
[active#(x1)] | = | 0 |
[tt] | = | 62221 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | 26557 |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
isList#(mark(X)) | → | isList#(X) | (70) |
isList#(active(X)) | → | isList#(X) | (52) |
The dependency pairs are split into 0 components.
isNeList#(active(X)) | → | isNeList#(X) | (93) |
isNeList#(mark(X)) | → | isNeList#(X) | (75) |
[a] | = | 0 |
[isNeList(x1)] | = | 24848 |
[isPal(x1)] | = | 0 |
[u] | = | 0 |
[and(x1, x2)] | = | 0 |
[isNeList#(x1)] | = | x1 + 0 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 0 |
[isQid(x1)] | = | 24850 |
[o] | = | 0 |
[mark#(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | 0 |
[nil] | = | 41566 |
[mark(x1)] | = | x1 + 1 |
[isList#(x1)] | = | 0 |
[i] | = | 10883 |
[e] | = | 22280 |
[active(x1)] | = | x1 + 2 |
[active#(x1)] | = | 0 |
[tt] | = | 24852 |
[and#(x1, x2)] | = | 0 |
[__(x1, x2)] | = | 31675 |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
isNeList#(active(X)) | → | isNeList#(X) | (93) |
isNeList#(mark(X)) | → | isNeList#(X) | (75) |
The dependency pairs are split into 0 components.