The rewrite relation of the following TRS is considered.
__(__(X,Y),Z) | → | __(X,__(Y,Z)) | (1) |
__(X,nil) | → | X | (2) |
__(nil,X) | → | X | (3) |
and(tt,X) | → | activate(X) | (4) |
isList(V) | → | isNeList(activate(V)) | (5) |
isList(n__nil) | → | tt | (6) |
isList(n____(V1,V2)) | → | and(isList(activate(V1)),n__isList(activate(V2))) | (7) |
isNeList(V) | → | isQid(activate(V)) | (8) |
isNeList(n____(V1,V2)) | → | and(isList(activate(V1)),n__isNeList(activate(V2))) | (9) |
isNeList(n____(V1,V2)) | → | and(isNeList(activate(V1)),n__isList(activate(V2))) | (10) |
isNePal(V) | → | isQid(activate(V)) | (11) |
isNePal(n____(I,n____(P,I))) | → | and(isQid(activate(I)),n__isPal(activate(P))) | (12) |
isPal(V) | → | isNePal(activate(V)) | (13) |
isPal(n__nil) | → | tt | (14) |
isQid(n__a) | → | tt | (15) |
isQid(n__e) | → | tt | (16) |
isQid(n__i) | → | tt | (17) |
isQid(n__o) | → | tt | (18) |
isQid(n__u) | → | tt | (19) |
nil | → | n__nil | (20) |
__(X1,X2) | → | n____(X1,X2) | (21) |
isList(X) | → | n__isList(X) | (22) |
isNeList(X) | → | n__isNeList(X) | (23) |
isPal(X) | → | n__isPal(X) | (24) |
a | → | n__a | (25) |
e | → | n__e | (26) |
i | → | n__i | (27) |
o | → | n__o | (28) |
u | → | n__u | (29) |
activate(n__nil) | → | nil | (30) |
activate(n____(X1,X2)) | → | __(activate(X1),activate(X2)) | (31) |
activate(n__isList(X)) | → | isList(X) | (32) |
activate(n__isNeList(X)) | → | isNeList(X) | (33) |
activate(n__isPal(X)) | → | isPal(X) | (34) |
activate(n__a) | → | a | (35) |
activate(n__e) | → | e | (36) |
activate(n__i) | → | i | (37) |
activate(n__o) | → | o | (38) |
activate(n__u) | → | u | (39) |
activate(X) | → | X | (40) |
activate#(n__i) | → | i# | (41) |
activate#(n__isNeList(X)) | → | isNeList#(X) | (42) |
__#(__(X,Y),Z) | → | __#(X,__(Y,Z)) | (43) |
isNeList#(V) | → | isQid#(activate(V)) | (44) |
isNeList#(V) | → | activate#(V) | (45) |
isNeList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isNeList(activate(V2))) | (46) |
isNePal#(n____(I,n____(P,I))) | → | isQid#(activate(I)) | (47) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (48) |
isNePal#(V) | → | activate#(V) | (49) |
activate#(n__u) | → | u# | (50) |
isList#(n____(V1,V2)) | → | activate#(V2) | (51) |
isNePal#(n____(I,n____(P,I))) | → | and#(isQid(activate(I)),n__isPal(activate(P))) | (52) |
isList#(V) | → | activate#(V) | (53) |
isNePal#(n____(I,n____(P,I))) | → | activate#(I) | (54) |
isList#(V) | → | isNeList#(activate(V)) | (55) |
isNeList#(n____(V1,V2)) | → | and#(isNeList(activate(V1)),n__isList(activate(V2))) | (56) |
isList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isList(activate(V2))) | (57) |
isNeList#(n____(V1,V2)) | → | isList#(activate(V1)) | (58) |
and#(tt,X) | → | activate#(X) | (59) |
isNePal#(V) | → | isQid#(activate(V)) | (60) |
activate#(n__isList(X)) | → | isList#(X) | (61) |
isPal#(V) | → | activate#(V) | (62) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (48) |
isList#(n____(V1,V2)) | → | activate#(V1) | (63) |
activate#(n__e) | → | e# | (64) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (65) |
activate#(n____(X1,X2)) | → | activate#(X1) | (66) |
activate#(n__isPal(X)) | → | isPal#(X) | (67) |
activate#(n__nil) | → | nil# | (68) |
isNeList#(n____(V1,V2)) | → | isNeList#(activate(V1)) | (69) |
__#(__(X,Y),Z) | → | __#(Y,Z) | (70) |
isList#(n____(V1,V2)) | → | isList#(activate(V1)) | (71) |
activate#(n____(X1,X2)) | → | __#(activate(X1),activate(X2)) | (72) |
activate#(n__o) | → | o# | (73) |
activate#(n__a) | → | a# | (74) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (65) |
isNePal#(n____(I,n____(P,I))) | → | activate#(P) | (75) |
isPal#(V) | → | isNePal#(activate(V)) | (76) |
activate#(n____(X1,X2)) | → | activate#(X2) | (77) |
The dependency pairs are split into 2 components.
activate#(n____(X1,X2)) | → | activate#(X2) | (77) |
isNeList#(n____(V1,V2)) | → | and#(isNeList(activate(V1)),n__isList(activate(V2))) | (56) |
isPal#(V) | → | isNePal#(activate(V)) | (76) |
isList#(V) | → | isNeList#(activate(V)) | (55) |
isNePal#(n____(I,n____(P,I))) | → | activate#(I) | (54) |
isNePal#(n____(I,n____(P,I))) | → | activate#(P) | (75) |
isList#(V) | → | activate#(V) | (53) |
isNePal#(n____(I,n____(P,I))) | → | and#(isQid(activate(I)),n__isPal(activate(P))) | (52) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (65) |
isList#(n____(V1,V2)) | → | activate#(V2) | (51) |
isList#(n____(V1,V2)) | → | isList#(activate(V1)) | (71) |
isNeList#(n____(V1,V2)) | → | isNeList#(activate(V1)) | (69) |
isNePal#(V) | → | activate#(V) | (49) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (48) |
activate#(n__isPal(X)) | → | isPal#(X) | (67) |
activate#(n____(X1,X2)) | → | activate#(X1) | (66) |
isNeList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isNeList(activate(V2))) | (46) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (65) |
isNeList#(V) | → | activate#(V) | (45) |
isList#(n____(V1,V2)) | → | activate#(V1) | (63) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (48) |
isPal#(V) | → | activate#(V) | (62) |
activate#(n__isList(X)) | → | isList#(X) | (61) |
and#(tt,X) | → | activate#(X) | (59) |
isNeList#(n____(V1,V2)) | → | isList#(activate(V1)) | (58) |
activate#(n__isNeList(X)) | → | isNeList#(X) | (42) |
isList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isList(activate(V2))) | (57) |
[a] | = | 1 |
[n__a] | = | 1 |
[n__o] | = | 10451 |
[isNeList(x1)] | = | x1 + 2 |
[isPal(x1)] | = | x1 + 5 |
[e#] | = | 0 |
[u] | = | 26567 |
[activate(x1)] | = | x1 + 0 |
[and(x1, x2)] | = | x1 + x2 + 0 |
[u#] | = | 0 |
[n__isNeList(x1)] | = | x1 + 2 |
[isNeList#(x1)] | = | x1 + 1 |
[activate#(x1)] | = | x1 + 0 |
[n__i] | = | 30613 |
[__#(x1, x2)] | = | 0 |
[n__isList(x1)] | = | x1 + 3 |
[isNePal(x1)] | = | x1 + 2 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | x1 + 4 |
[n__isPal(x1)] | = | x1 + 5 |
[n__nil] | = | 44022 |
[isQid(x1)] | = | 2 |
[n____(x1, x2)] | = | x1 + x2 + 20544 |
[n__e] | = | 10088 |
[o] | = | 10451 |
[isList(x1)] | = | x1 + 3 |
[isNePal#(x1)] | = | x1 + 3 |
[nil] | = | 44022 |
[n__u] | = | 26567 |
[o#] | = | 0 |
[nil#] | = | 0 |
[isList#(x1)] | = | x1 + 2 |
[i] | = | 30613 |
[e] | = | 10088 |
[a#] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | x1 + x2 + 0 |
[__(x1, x2)] | = | x1 + x2 + 20544 |
[i#] | = | 0 |
isQid(n__o) | → | tt | (18) |
and(tt,X) | → | activate(X) | (4) |
isQid(n__a) | → | tt | (15) |
isNeList(V) | → | isQid(activate(V)) | (8) |
__(__(X,Y),Z) | → | __(X,__(Y,Z)) | (1) |
__(nil,X) | → | X | (3) |
isQid(n__e) | → | tt | (16) |
__(X1,X2) | → | n____(X1,X2) | (21) |
activate(n__e) | → | e | (36) |
e | → | n__e | (26) |
isQid(n__u) | → | tt | (19) |
activate(n__isList(X)) | → | isList(X) | (32) |
isQid(n__i) | → | tt | (17) |
i | → | n__i | (27) |
activate(n__isPal(X)) | → | isPal(X) | (34) |
isList(X) | → | n__isList(X) | (22) |
o | → | n__o | (28) |
isList(V) | → | isNeList(activate(V)) | (5) |
activate(n__isNeList(X)) | → | isNeList(X) | (33) |
isNeList(n____(V1,V2)) | → | and(isNeList(activate(V1)),n__isList(activate(V2))) | (10) |
activate(n__u) | → | u | (39) |
isList(n____(V1,V2)) | → | and(isList(activate(V1)),n__isList(activate(V2))) | (7) |
nil | → | n__nil | (20) |
a | → | n__a | (25) |
activate(n__nil) | → | nil | (30) |
isPal(n__nil) | → | tt | (14) |
activate(n____(X1,X2)) | → | __(activate(X1),activate(X2)) | (31) |
isNePal(n____(I,n____(P,I))) | → | and(isQid(activate(I)),n__isPal(activate(P))) | (12) |
isNeList(X) | → | n__isNeList(X) | (23) |
isPal(X) | → | n__isPal(X) | (24) |
isNePal(V) | → | isQid(activate(V)) | (11) |
isNeList(n____(V1,V2)) | → | and(isList(activate(V1)),n__isNeList(activate(V2))) | (9) |
isPal(V) | → | isNePal(activate(V)) | (13) |
activate(X) | → | X | (40) |
isList(n__nil) | → | tt | (6) |
activate(n__o) | → | o | (38) |
activate(n__i) | → | i | (37) |
activate(n__a) | → | a | (35) |
u | → | n__u | (29) |
__(X,nil) | → | X | (2) |
activate#(n____(X1,X2)) | → | activate#(X2) | (77) |
isNeList#(n____(V1,V2)) | → | and#(isNeList(activate(V1)),n__isList(activate(V2))) | (56) |
isPal#(V) | → | isNePal#(activate(V)) | (76) |
isList#(V) | → | isNeList#(activate(V)) | (55) |
isNePal#(n____(I,n____(P,I))) | → | activate#(I) | (54) |
isNePal#(n____(I,n____(P,I))) | → | activate#(P) | (75) |
isList#(V) | → | activate#(V) | (53) |
isNePal#(n____(I,n____(P,I))) | → | and#(isQid(activate(I)),n__isPal(activate(P))) | (52) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (65) |
isList#(n____(V1,V2)) | → | activate#(V2) | (51) |
isList#(n____(V1,V2)) | → | isList#(activate(V1)) | (71) |
isNeList#(n____(V1,V2)) | → | isNeList#(activate(V1)) | (69) |
isNePal#(V) | → | activate#(V) | (49) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (48) |
activate#(n__isPal(X)) | → | isPal#(X) | (67) |
activate#(n____(X1,X2)) | → | activate#(X1) | (66) |
isNeList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isNeList(activate(V2))) | (46) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (65) |
isNeList#(V) | → | activate#(V) | (45) |
isList#(n____(V1,V2)) | → | activate#(V1) | (63) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (48) |
isPal#(V) | → | activate#(V) | (62) |
activate#(n__isList(X)) | → | isList#(X) | (61) |
and#(tt,X) | → | activate#(X) | (59) |
isNeList#(n____(V1,V2)) | → | isList#(activate(V1)) | (58) |
activate#(n__isNeList(X)) | → | isNeList#(X) | (42) |
isList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isList(activate(V2))) | (57) |
The dependency pairs are split into 0 components.
__#(__(X,Y),Z) | → | __#(Y,Z) | (70) |
__#(__(X,Y),Z) | → | __#(X,__(Y,Z)) | (43) |
[a] | = | 1 |
[n__a] | = | 1 |
[n__o] | = | 44364 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | x1 + 1 |
[e#] | = | 0 |
[u] | = | 26567 |
[activate(x1)] | = | x1 + 0 |
[and(x1, x2)] | = | x1 + x2 + 0 |
[u#] | = | 0 |
[n__isNeList(x1)] | = | x1 + 1 |
[isNeList#(x1)] | = | x1 + 1 |
[activate#(x1)] | = | 0 |
[n__i] | = | 30613 |
[__#(x1, x2)] | = | x1 + 0 |
[n__isList(x1)] | = | x1 + 1 |
[isNePal(x1)] | = | x1 + 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 4 |
[n__isPal(x1)] | = | x1 + 1 |
[n__nil] | = | 1 |
[isQid(x1)] | = | 1 |
[n____(x1, x2)] | = | x1 + x2 + 1 |
[n__e] | = | 10088 |
[o] | = | 44364 |
[isList(x1)] | = | x1 + 1 |
[isNePal#(x1)] | = | x1 + 3 |
[nil] | = | 1 |
[n__u] | = | 26567 |
[o#] | = | 0 |
[nil#] | = | 0 |
[isList#(x1)] | = | x1 + 2 |
[i] | = | 30613 |
[e] | = | 10088 |
[a#] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | x1 + x2 + 0 |
[__(x1, x2)] | = | x1 + x2 + 1 |
[i#] | = | 0 |
isQid(n__o) | → | tt | (18) |
and(tt,X) | → | activate(X) | (4) |
isQid(n__a) | → | tt | (15) |
isNeList(V) | → | isQid(activate(V)) | (8) |
__(__(X,Y),Z) | → | __(X,__(Y,Z)) | (1) |
__(nil,X) | → | X | (3) |
isQid(n__e) | → | tt | (16) |
__(X1,X2) | → | n____(X1,X2) | (21) |
activate(n__e) | → | e | (36) |
e | → | n__e | (26) |
isQid(n__u) | → | tt | (19) |
activate(n__isList(X)) | → | isList(X) | (32) |
isQid(n__i) | → | tt | (17) |
i | → | n__i | (27) |
activate(n__isPal(X)) | → | isPal(X) | (34) |
isList(X) | → | n__isList(X) | (22) |
o | → | n__o | (28) |
isList(V) | → | isNeList(activate(V)) | (5) |
activate(n__isNeList(X)) | → | isNeList(X) | (33) |
isNeList(n____(V1,V2)) | → | and(isNeList(activate(V1)),n__isList(activate(V2))) | (10) |
activate(n__u) | → | u | (39) |
isList(n____(V1,V2)) | → | and(isList(activate(V1)),n__isList(activate(V2))) | (7) |
nil | → | n__nil | (20) |
a | → | n__a | (25) |
activate(n__nil) | → | nil | (30) |
isPal(n__nil) | → | tt | (14) |
activate(n____(X1,X2)) | → | __(activate(X1),activate(X2)) | (31) |
isNePal(n____(I,n____(P,I))) | → | and(isQid(activate(I)),n__isPal(activate(P))) | (12) |
isNeList(X) | → | n__isNeList(X) | (23) |
isPal(X) | → | n__isPal(X) | (24) |
isNePal(V) | → | isQid(activate(V)) | (11) |
isNeList(n____(V1,V2)) | → | and(isList(activate(V1)),n__isNeList(activate(V2))) | (9) |
isPal(V) | → | isNePal(activate(V)) | (13) |
activate(X) | → | X | (40) |
isList(n__nil) | → | tt | (6) |
activate(n__o) | → | o | (38) |
activate(n__i) | → | i | (37) |
activate(n__a) | → | a | (35) |
u | → | n__u | (29) |
__(X,nil) | → | X | (2) |
__#(__(X,Y),Z) | → | __#(Y,Z) | (70) |
__#(__(X,Y),Z) | → | __#(X,__(Y,Z)) | (43) |
The dependency pairs are split into 0 components.