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,__(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)) | → | __(X1,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) |
isList#(V) | → | activate#(V) | (42) |
isNeList#(V) | → | isQid#(activate(V)) | (43) |
and#(tt,X) | → | activate#(X) | (44) |
isNeList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isNeList(activate(V2))) | (45) |
isNePal#(n____(I,__(P,I))) | → | isQid#(activate(I)) | (46) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (47) |
isNePal#(V) | → | activate#(V) | (48) |
isNeList#(n____(V1,V2)) | → | isNeList#(activate(V1)) | (49) |
isNeList#(n____(V1,V2)) | → | and#(isNeList(activate(V1)),n__isList(activate(V2))) | (50) |
isNePal#(n____(I,__(P,I))) | → | and#(isQid(activate(I)),n__isPal(activate(P))) | (51) |
activate#(n__isList(X)) | → | isList#(X) | (52) |
isNePal#(n____(I,__(P,I))) | → | activate#(I) | (53) |
activate#(n__isPal(X)) | → | isPal#(X) | (54) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (55) |
isList#(n____(V1,V2)) | → | activate#(V1) | (56) |
isNeList#(n____(V1,V2)) | → | isList#(activate(V1)) | (57) |
isNePal#(V) | → | isQid#(activate(V)) | (58) |
__#(__(X,Y),Z) | → | __#(X,__(Y,Z)) | (59) |
isPal#(V) | → | activate#(V) | (60) |
isList#(V) | → | isNeList#(activate(V)) | (61) |
activate#(n__u) | → | u# | (62) |
__#(__(X,Y),Z) | → | __#(Y,Z) | (63) |
activate#(n__isNeList(X)) | → | isNeList#(X) | (64) |
activate#(n__nil) | → | nil# | (65) |
activate#(n__e) | → | e# | (66) |
isList#(n____(V1,V2)) | → | isList#(activate(V1)) | (67) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (47) |
isNeList#(V) | → | activate#(V) | (68) |
isList#(n____(V1,V2)) | → | activate#(V2) | (69) |
activate#(n____(X1,X2)) | → | __#(X1,X2) | (70) |
activate#(n__o) | → | o# | (71) |
activate#(n__a) | → | a# | (72) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (55) |
isNePal#(n____(I,__(P,I))) | → | activate#(P) | (73) |
isPal#(V) | → | isNePal#(activate(V)) | (74) |
isList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isList(activate(V2))) | (75) |
The dependency pairs are split into 2 components.
isList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isList(activate(V2))) | (75) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (55) |
isPal#(V) | → | isNePal#(activate(V)) | (74) |
activate#(n__isPal(X)) | → | isPal#(X) | (54) |
isNePal#(n____(I,__(P,I))) | → | activate#(I) | (53) |
isNePal#(n____(I,__(P,I))) | → | activate#(P) | (73) |
activate#(n__isList(X)) | → | isList#(X) | (52) |
isNePal#(n____(I,__(P,I))) | → | and#(isQid(activate(I)),n__isPal(activate(P))) | (51) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (55) |
isNeList#(n____(V1,V2)) | → | and#(isNeList(activate(V1)),n__isList(activate(V2))) | (50) |
isNeList#(n____(V1,V2)) | → | isNeList#(activate(V1)) | (49) |
isList#(n____(V1,V2)) | → | activate#(V2) | (69) |
isNeList#(V) | → | activate#(V) | (68) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (47) |
isNePal#(V) | → | activate#(V) | (48) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (47) |
isList#(n____(V1,V2)) | → | isList#(activate(V1)) | (67) |
isNeList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isNeList(activate(V2))) | (45) |
activate#(n__isNeList(X)) | → | isNeList#(X) | (64) |
isList#(V) | → | isNeList#(activate(V)) | (61) |
isPal#(V) | → | activate#(V) | (60) |
and#(tt,X) | → | activate#(X) | (44) |
isNeList#(n____(V1,V2)) | → | isList#(activate(V1)) | (57) |
isList#(V) | → | activate#(V) | (42) |
isList#(n____(V1,V2)) | → | activate#(V1) | (56) |
[a] | = | 1 |
[n__a] | = | 1 |
[n__o] | = | 2438 |
[isNeList(x1)] | = | x1 + 2 |
[isPal(x1)] | = | x1 + 39471 |
[e#] | = | 0 |
[u] | = | 10451 |
[activate(x1)] | = | x1 + 39468 |
[and(x1, x2)] | = | x1 + x2 + 39467 |
[u#] | = | 0 |
[n__isNeList(x1)] | = | x1 + 2 |
[isNeList#(x1)] | = | x1 + 1 |
[activate#(x1)] | = | x1 + 0 |
[n__i] | = | 11798 |
[__#(x1, x2)] | = | 0 |
[n__isList(x1)] | = | x1 + 39471 |
[isNePal(x1)] | = | x1 + 1 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | x1 + 39470 |
[n__isPal(x1)] | = | x1 + 39471 |
[n__nil] | = | 14219 |
[isQid(x1)] | = | 1 |
[n____(x1, x2)] | = | x1 + x2 + 157874 |
[n__e] | = | 32286 |
[o] | = | 2438 |
[isList(x1)] | = | x1 + 39471 |
[isNePal#(x1)] | = | x1 + 1 |
[nil] | = | 14219 |
[n__u] | = | 10451 |
[o#] | = | 0 |
[nil#] | = | 0 |
[isList#(x1)] | = | x1 + 39470 |
[i] | = | 11798 |
[e] | = | 32286 |
[a#] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | x2 + 78935 |
[__(x1, x2)] | = | x1 + x2 + 157874 |
[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)) | → | __(X1,X2) | (31) |
isNePal(n____(I,__(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) |
isList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isList(activate(V2))) | (75) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (55) |
isPal#(V) | → | isNePal#(activate(V)) | (74) |
activate#(n__isPal(X)) | → | isPal#(X) | (54) |
isNePal#(n____(I,__(P,I))) | → | activate#(I) | (53) |
isNePal#(n____(I,__(P,I))) | → | activate#(P) | (73) |
activate#(n__isList(X)) | → | isList#(X) | (52) |
isNePal#(n____(I,__(P,I))) | → | and#(isQid(activate(I)),n__isPal(activate(P))) | (51) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (55) |
isNeList#(n____(V1,V2)) | → | and#(isNeList(activate(V1)),n__isList(activate(V2))) | (50) |
isNeList#(n____(V1,V2)) | → | isNeList#(activate(V1)) | (49) |
isList#(n____(V1,V2)) | → | activate#(V2) | (69) |
isNeList#(V) | → | activate#(V) | (68) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (47) |
isNePal#(V) | → | activate#(V) | (48) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (47) |
isList#(n____(V1,V2)) | → | isList#(activate(V1)) | (67) |
isNeList#(n____(V1,V2)) | → | and#(isList(activate(V1)),n__isNeList(activate(V2))) | (45) |
activate#(n__isNeList(X)) | → | isNeList#(X) | (64) |
isList#(V) | → | isNeList#(activate(V)) | (61) |
isPal#(V) | → | activate#(V) | (60) |
and#(tt,X) | → | activate#(X) | (44) |
isNeList#(n____(V1,V2)) | → | isList#(activate(V1)) | (57) |
isList#(V) | → | activate#(V) | (42) |
isList#(n____(V1,V2)) | → | activate#(V1) | (56) |
The dependency pairs are split into 0 components.
__#(__(X,Y),Z) | → | __#(Y,Z) | (63) |
__#(__(X,Y),Z) | → | __#(X,__(Y,Z)) | (59) |
[a] | = | 2 |
[n__a] | = | 1 |
[n__o] | = | 42193 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | x1 + 39471 |
[e#] | = | 0 |
[u] | = | 46572 |
[activate(x1)] | = | x1 + 1 |
[and(x1, x2)] | = | x1 + x2 + 0 |
[u#] | = | 0 |
[n__isNeList(x1)] | = | x1 + 1 |
[isNeList#(x1)] | = | x1 + 1 |
[activate#(x1)] | = | 0 |
[n__i] | = | 15922 |
[__#(x1, x2)] | = | x1 + x2 + 0 |
[n__isList(x1)] | = | x1 + 2 |
[isNePal(x1)] | = | x1 + 39467 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 39470 |
[n__isPal(x1)] | = | x1 + 39471 |
[n__nil] | = | 1 |
[isQid(x1)] | = | 1 |
[n____(x1, x2)] | = | x1 + x2 + 4 |
[n__e] | = | 47262 |
[o] | = | 42194 |
[isList(x1)] | = | x1 + 2 |
[isNePal#(x1)] | = | x1 + 1 |
[nil] | = | 1 |
[n__u] | = | 46572 |
[o#] | = | 0 |
[nil#] | = | 0 |
[isList#(x1)] | = | x1 + 39470 |
[i] | = | 15923 |
[e] | = | 47263 |
[a#] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | x2 + 78935 |
[__(x1, x2)] | = | x1 + x2 + 4 |
[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)) | → | __(X1,X2) | (31) |
isNePal(n____(I,__(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) | (63) |
The dependency pairs are split into 1 component.
__#(__(X,Y),Z) | → | __#(X,__(Y,Z)) | (59) |
[a] | = | 3 |
[n__a] | = | 1 |
[n__o] | = | 46441 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | x1 + 39471 |
[e#] | = | 0 |
[u] | = | 46572 |
[activate(x1)] | = | x1 + 2 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[u#] | = | 0 |
[n__isNeList(x1)] | = | x1 + 1 |
[isNeList#(x1)] | = | x1 + 1 |
[activate#(x1)] | = | 0 |
[n__i] | = | 23612 |
[__#(x1, x2)] | = | x1 + 0 |
[n__isList(x1)] | = | x1 + 1 |
[isNePal(x1)] | = | x1 + 39466 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | 39470 |
[n__isPal(x1)] | = | x1 + 39471 |
[n__nil] | = | 1 |
[isQid(x1)] | = | 1 |
[n____(x1, x2)] | = | x1 + x2 + 8 |
[n__e] | = | 47262 |
[o] | = | 46443 |
[isList(x1)] | = | x1 + 3 |
[isNePal#(x1)] | = | x1 + 1 |
[nil] | = | 1 |
[n__u] | = | 46572 |
[o#] | = | 0 |
[nil#] | = | 0 |
[isList#(x1)] | = | x1 + 39470 |
[i] | = | 23614 |
[e] | = | 47264 |
[a#] | = | 0 |
[tt] | = | 1 |
[and#(x1, x2)] | = | x2 + 78935 |
[__(x1, x2)] | = | x1 + x2 + 8 |
[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)) | → | __(X1,X2) | (31) |
isNePal(n____(I,__(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) | → | __#(X,__(Y,Z)) | (59) |
The dependency pairs are split into 0 components.