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) |
prec(nil) | = | 9 | weight(nil) | = | 3 | ||||
prec(tt) | = | 2 | weight(tt) | = | 7 | ||||
prec(n__nil) | = | 19 | weight(n__nil) | = | 1 | ||||
prec(n__a) | = | 11 | weight(n__a) | = | 6 | ||||
prec(n__e) | = | 12 | weight(n__e) | = | 6 | ||||
prec(n__i) | = | 13 | weight(n__i) | = | 6 | ||||
prec(n__o) | = | 17 | weight(n__o) | = | 6 | ||||
prec(n__u) | = | 14 | weight(n__u) | = | 6 | ||||
prec(a) | = | 15 | weight(a) | = | 7 | ||||
prec(e) | = | 18 | weight(e) | = | 7 | ||||
prec(i) | = | 21 | weight(i) | = | 7 | ||||
prec(o) | = | 22 | weight(o) | = | 8 | ||||
prec(u) | = | 24 | weight(u) | = | 7 | ||||
prec(activate) | = | 23 | weight(activate) | = | 2 | ||||
prec(isList) | = | 3 | weight(isList) | = | 7 | ||||
prec(isNeList) | = | 4 | weight(isNeList) | = | 4 | ||||
prec(n__isList) | = | 16 | weight(n__isList) | = | 5 | ||||
prec(isQid) | = | 6 | weight(isQid) | = | 1 | ||||
prec(n__isNeList) | = | 7 | weight(n__isNeList) | = | 2 | ||||
prec(isNePal) | = | 5 | weight(isNePal) | = | 4 | ||||
prec(n__isPal) | = | 8 | weight(n__isPal) | = | 19 | ||||
prec(isPal) | = | 20 | weight(isPal) | = | 20 | ||||
prec(__) | = | 0 | weight(__) | = | 10 | ||||
prec(and) | = | 1 | weight(and) | = | 0 | ||||
prec(n____) | = | 10 | weight(n____) | = | 9 |
__(__(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) |
There are no rules in the TRS. Hence, it is terminating.