The rewrite relation of the following TRS is considered.
__(__(X,Y),Z) | → | __(X,__(Y,Z)) | (1) |
__(X,nil) | → | X | (2) |
__(nil,X) | → | X | (3) |
U11(tt) | → | tt | (4) |
U21(tt,V2) | → | U22(isList(activate(V2))) | (5) |
U22(tt) | → | tt | (6) |
U31(tt) | → | tt | (7) |
U41(tt,V2) | → | U42(isNeList(activate(V2))) | (8) |
U42(tt) | → | tt | (9) |
U51(tt,V2) | → | U52(isList(activate(V2))) | (10) |
U52(tt) | → | tt | (11) |
U61(tt) | → | tt | (12) |
U71(tt,P) | → | U72(isPal(activate(P))) | (13) |
U72(tt) | → | tt | (14) |
U81(tt) | → | tt | (15) |
isList(V) | → | U11(isNeList(activate(V))) | (16) |
isList(n__nil) | → | tt | (17) |
isList(n____(V1,V2)) | → | U21(isList(activate(V1)),activate(V2)) | (18) |
isNeList(V) | → | U31(isQid(activate(V))) | (19) |
isNeList(n____(V1,V2)) | → | U41(isList(activate(V1)),activate(V2)) | (20) |
isNeList(n____(V1,V2)) | → | U51(isNeList(activate(V1)),activate(V2)) | (21) |
isNePal(V) | → | U61(isQid(activate(V))) | (22) |
isNePal(n____(I,__(P,I))) | → | U71(isQid(activate(I)),activate(P)) | (23) |
isPal(V) | → | U81(isNePal(activate(V))) | (24) |
isPal(n__nil) | → | tt | (25) |
isQid(n__a) | → | tt | (26) |
isQid(n__e) | → | tt | (27) |
isQid(n__i) | → | tt | (28) |
isQid(n__o) | → | tt | (29) |
isQid(n__u) | → | tt | (30) |
nil | → | n__nil | (31) |
__(X1,X2) | → | n____(X1,X2) | (32) |
a | → | n__a | (33) |
e | → | n__e | (34) |
i | → | n__i | (35) |
o | → | n__o | (36) |
u | → | n__u | (37) |
activate(n__nil) | → | nil | (38) |
activate(n____(X1,X2)) | → | __(X1,X2) | (39) |
activate(n__a) | → | a | (40) |
activate(n__e) | → | e | (41) |
activate(n__i) | → | i | (42) |
activate(n__o) | → | o | (43) |
activate(n__u) | → | u | (44) |
activate(X) | → | X | (45) |
activate#(n__i) | → | i# | (46) |
U41#(tt,V2) | → | U42#(isNeList(activate(V2))) | (47) |
isNePal#(V) | → | isQid#(activate(V)) | (48) |
isNeList#(n____(V1,V2)) | → | isNeList#(activate(V1)) | (49) |
isList#(n____(V1,V2)) | → | U21#(isList(activate(V1)),activate(V2)) | (50) |
__#(__(X,Y),Z) | → | __#(Y,Z) | (51) |
__#(__(X,Y),Z) | → | __#(X,__(Y,Z)) | (52) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (53) |
isList#(n____(V1,V2)) | → | isList#(activate(V1)) | (54) |
isList#(n____(V1,V2)) | → | activate#(V1) | (55) |
isList#(V) | → | U11#(isNeList(activate(V))) | (56) |
U71#(tt,P) | → | U72#(isPal(activate(P))) | (57) |
isList#(V) | → | activate#(V) | (58) |
isNePal#(n____(I,__(P,I))) | → | isQid#(activate(I)) | (59) |
isPal#(V) | → | U81#(isNePal(activate(V))) | (60) |
isPal#(V) | → | activate#(V) | (61) |
U21#(tt,V2) | → | U22#(isList(activate(V2))) | (62) |
U51#(tt,V2) | → | activate#(V2) | (63) |
U41#(tt,V2) | → | activate#(V2) | (64) |
isNePal#(n____(I,__(P,I))) | → | U71#(isQid(activate(I)),activate(P)) | (65) |
isNeList#(V) | → | U31#(isQid(activate(V))) | (66) |
isNePal#(n____(I,__(P,I))) | → | activate#(I) | (67) |
isNePal#(V) | → | activate#(V) | (68) |
isList#(n____(V1,V2)) | → | activate#(V2) | (69) |
U21#(tt,V2) | → | isList#(activate(V2)) | (70) |
activate#(n____(X1,X2)) | → | __#(X1,X2) | (71) |
U71#(tt,P) | → | isPal#(activate(P)) | (72) |
isList#(V) | → | isNeList#(activate(V)) | (73) |
isPal#(V) | → | isNePal#(activate(V)) | (74) |
isNeList#(V) | → | activate#(V) | (75) |
activate#(n__a) | → | a# | (76) |
U41#(tt,V2) | → | isNeList#(activate(V2)) | (77) |
isNePal#(V) | → | U61#(isQid(activate(V))) | (78) |
U51#(tt,V2) | → | isList#(activate(V2)) | (79) |
isNeList#(n____(V1,V2)) | → | U51#(isNeList(activate(V1)),activate(V2)) | (80) |
activate#(n__u) | → | u# | (81) |
isNeList#(n____(V1,V2)) | → | isList#(activate(V1)) | (82) |
isNeList#(V) | → | isQid#(activate(V)) | (83) |
isNeList#(n____(V1,V2)) | → | activate#(V2) | (53) |
U21#(tt,V2) | → | activate#(V2) | (84) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (85) |
U51#(tt,V2) | → | U52#(isList(activate(V2))) | (86) |
isNeList#(n____(V1,V2)) | → | U41#(isList(activate(V1)),activate(V2)) | (87) |
activate#(n__e) | → | e# | (88) |
activate#(n__o) | → | o# | (89) |
U71#(tt,P) | → | activate#(P) | (90) |
isNePal#(n____(I,__(P,I))) | → | activate#(P) | (91) |
activate#(n__nil) | → | nil# | (92) |
isNeList#(n____(V1,V2)) | → | activate#(V1) | (85) |
The dependency pairs are split into 3 components.
isNePal#(n____(I,__(P,I))) | → | U71#(isQid(activate(I)),activate(P)) | (65) |
isPal#(V) | → | isNePal#(activate(V)) | (74) |
U71#(tt,P) | → | isPal#(activate(P)) | (72) |
[a] | = | 27543 |
[n__a] | = | 27543 |
[U72#(x1)] | = | 0 |
[U21(x1, x2)] | = | 0 |
[U11(x1)] | = | 0 |
[n__o] | = | 58155 |
[isNeList(x1)] | = | 0 |
[isPal(x1)] | = | 0 |
[U42(x1)] | = | 0 |
[e#] | = | 0 |
[u] | = | 27543 |
[activate(x1)] | = | x1 + 1 |
[U71(x1, x2)] | = | 0 |
[U81#(x1)] | = | 0 |
[u#] | = | 0 |
[isNeList#(x1)] | = | 0 |
[activate#(x1)] | = | 0 |
[n__i] | = | 33396 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 0 |
[U72(x1)] | = | 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | x1 + 48078 |
[n__nil] | = | 1 |
[U52#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 20537 |
[n____(x1, x2)] | = | x1 + x2 + 282 |
[n__e] | = | 27543 |
[o] | = | 58155 |
[U42#(x1)] | = | 0 |
[isList(x1)] | = | 0 |
[isNePal#(x1)] | = | x1 + 48076 |
[nil] | = | 1 |
[n__u] | = | 27543 |
[o#] | = | 0 |
[nil#] | = | 0 |
[isList#(x1)] | = | 0 |
[i] | = | 33396 |
[U52(x1)] | = | 0 |
[U61(x1)] | = | 0 |
[U51#(x1, x2)] | = | 0 |
[e] | = | 27543 |
[U11#(x1)] | = | 0 |
[U31(x1)] | = | 0 |
[U41#(x1, x2)] | = | 0 |
[a#] | = | 0 |
[U21#(x1, x2)] | = | 0 |
[U81(x1)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 48080 |
[U71#(x1, x2)] | = | x1 + x2 + 0 |
[U22(x1)] | = | 0 |
[U51(x1, x2)] | = | 0 |
[U41(x1, x2)] | = | 0 |
[U31#(x1)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 282 |
[U61#(x1)] | = | 0 |
[i#] | = | 0 |
__(__(X,Y),Z) | → | __(X,__(Y,Z)) | (1) |
__(nil,X) | → | X | (3) |
o | → | n__o | (36) |
isQid(n__a) | → | tt | (26) |
__(X1,X2) | → | n____(X1,X2) | (32) |
isQid(n__e) | → | tt | (27) |
e | → | n__e | (34) |
isQid(n__i) | → | tt | (28) |
activate(n__u) | → | u | (44) |
a | → | n__a | (33) |
activate(n____(X1,X2)) | → | __(X1,X2) | (39) |
isQid(n__u) | → | tt | (30) |
nil | → | n__nil | (31) |
activate(X) | → | X | (45) |
activate(n__a) | → | a | (40) |
activate(n__nil) | → | nil | (38) |
u | → | n__u | (37) |
activate(n__e) | → | e | (41) |
activate(n__i) | → | i | (42) |
i | → | n__i | (35) |
isQid(n__o) | → | tt | (29) |
activate(n__o) | → | o | (43) |
__(X,nil) | → | X | (2) |
isNePal#(n____(I,__(P,I))) | → | U71#(isQid(activate(I)),activate(P)) | (65) |
isPal#(V) | → | isNePal#(activate(V)) | (74) |
U71#(tt,P) | → | isPal#(activate(P)) | (72) |
The dependency pairs are split into 0 components.
U21#(tt,V2) | → | isList#(activate(V2)) | (70) |
isNeList#(n____(V1,V2)) | → | U41#(isList(activate(V1)),activate(V2)) | (87) |
isNeList#(n____(V1,V2)) | → | isList#(activate(V1)) | (82) |
isNeList#(n____(V1,V2)) | → | U51#(isNeList(activate(V1)),activate(V2)) | (80) |
U51#(tt,V2) | → | isList#(activate(V2)) | (79) |
isList#(n____(V1,V2)) | → | isList#(activate(V1)) | (54) |
U41#(tt,V2) | → | isNeList#(activate(V2)) | (77) |
isList#(n____(V1,V2)) | → | U21#(isList(activate(V1)),activate(V2)) | (50) |
isList#(V) | → | isNeList#(activate(V)) | (73) |
isNeList#(n____(V1,V2)) | → | isNeList#(activate(V1)) | (49) |
[a] | = | 1 |
[n__a] | = | 1 |
[U72#(x1)] | = | 0 |
[U21(x1, x2)] | = | x1 + x2 + 6705 |
[U11(x1)] | = | x1 + 0 |
[n__o] | = | 22078 |
[isNeList(x1)] | = | x1 + 6704 |
[isPal(x1)] | = | 0 |
[U42(x1)] | = | x1 + 0 |
[e#] | = | 0 |
[u] | = | 10206 |
[activate(x1)] | = | x1 + 1 |
[U71(x1, x2)] | = | 0 |
[U81#(x1)] | = | 0 |
[u#] | = | 0 |
[isNeList#(x1)] | = | x1 + 0 |
[activate#(x1)] | = | 0 |
[n__i] | = | 11885 |
[__#(x1, x2)] | = | 0 |
[isNePal(x1)] | = | 0 |
[U72(x1)] | = | 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | x1 + 48078 |
[n__nil] | = | 1 |
[U52#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 6703 |
[n____(x1, x2)] | = | x1 + x2 + 6710 |
[n__e] | = | 27543 |
[o] | = | 22079 |
[U42#(x1)] | = | 0 |
[isList(x1)] | = | x1 + 6705 |
[isNePal#(x1)] | = | x1 + 48076 |
[nil] | = | 1 |
[n__u] | = | 10205 |
[o#] | = | 0 |
[nil#] | = | 0 |
[isList#(x1)] | = | x1 + 2 |
[i] | = | 11886 |
[U52(x1)] | = | x1 + 3 |
[U61(x1)] | = | 0 |
[U51#(x1, x2)] | = | x1 + x2 + 3 |
[e] | = | 27543 |
[U11#(x1)] | = | 0 |
[U31(x1)] | = | x1 + 0 |
[U41#(x1, x2)] | = | x1 + x2 + 2 |
[a#] | = | 0 |
[U21#(x1, x2)] | = | x1 + x2 + 3 |
[U81(x1)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 1 |
[U71#(x1, x2)] | = | x1 + x2 + 0 |
[U22(x1)] | = | x1 + 0 |
[U51(x1, x2)] | = | x1 + x2 + 6708 |
[U41(x1, x2)] | = | x1 + x2 + 6707 |
[U31#(x1)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 6711 |
[U61#(x1)] | = | 0 |
[i#] | = | 0 |
isList(n____(V1,V2)) | → | U21(isList(activate(V1)),activate(V2)) | (18) |
U11(tt) | → | tt | (4) |
U41(tt,V2) | → | U42(isNeList(activate(V2))) | (8) |
__(__(X,Y),Z) | → | __(X,__(Y,Z)) | (1) |
__(nil,X) | → | X | (3) |
isList(V) | → | U11(isNeList(activate(V))) | (16) |
isNeList(n____(V1,V2)) | → | U51(isNeList(activate(V1)),activate(V2)) | (21) |
o | → | n__o | (36) |
isQid(n__a) | → | tt | (26) |
isNeList(V) | → | U31(isQid(activate(V))) | (19) |
__(X1,X2) | → | n____(X1,X2) | (32) |
isList(n__nil) | → | tt | (17) |
isQid(n__e) | → | tt | (27) |
e | → | n__e | (34) |
isQid(n__i) | → | tt | (28) |
activate(n__u) | → | u | (44) |
U21(tt,V2) | → | U22(isList(activate(V2))) | (5) |
a | → | n__a | (33) |
U51(tt,V2) | → | U52(isList(activate(V2))) | (10) |
activate(n____(X1,X2)) | → | __(X1,X2) | (39) |
U31(tt) | → | tt | (7) |
isNeList(n____(V1,V2)) | → | U41(isList(activate(V1)),activate(V2)) | (20) |
isQid(n__u) | → | tt | (30) |
nil | → | n__nil | (31) |
activate(X) | → | X | (45) |
U52(tt) | → | tt | (11) |
U42(tt) | → | tt | (9) |
activate(n__a) | → | a | (40) |
U22(tt) | → | tt | (6) |
activate(n__nil) | → | nil | (38) |
u | → | n__u | (37) |
activate(n__e) | → | e | (41) |
activate(n__i) | → | i | (42) |
i | → | n__i | (35) |
isQid(n__o) | → | tt | (29) |
activate(n__o) | → | o | (43) |
__(X,nil) | → | X | (2) |
U21#(tt,V2) | → | isList#(activate(V2)) | (70) |
isNeList#(n____(V1,V2)) | → | U41#(isList(activate(V1)),activate(V2)) | (87) |
isNeList#(n____(V1,V2)) | → | isList#(activate(V1)) | (82) |
isNeList#(n____(V1,V2)) | → | U51#(isNeList(activate(V1)),activate(V2)) | (80) |
U51#(tt,V2) | → | isList#(activate(V2)) | (79) |
isList#(n____(V1,V2)) | → | isList#(activate(V1)) | (54) |
U41#(tt,V2) | → | isNeList#(activate(V2)) | (77) |
isList#(n____(V1,V2)) | → | U21#(isList(activate(V1)),activate(V2)) | (50) |
isList#(V) | → | isNeList#(activate(V)) | (73) |
isNeList#(n____(V1,V2)) | → | isNeList#(activate(V1)) | (49) |
The dependency pairs are split into 0 components.
__#(__(X,Y),Z) | → | __#(X,__(Y,Z)) | (52) |
__#(__(X,Y),Z) | → | __#(Y,Z) | (51) |
[a] | = | 1 |
[n__a] | = | 1 |
[U72#(x1)] | = | 0 |
[U21(x1, x2)] | = | x1 + x2 + 4 |
[U11(x1)] | = | x1 + 0 |
[n__o] | = | 1 |
[isNeList(x1)] | = | x1 + 3 |
[isPal(x1)] | = | 0 |
[U42(x1)] | = | x1 + 0 |
[e#] | = | 0 |
[u] | = | 14099 |
[activate(x1)] | = | x1 + 1 |
[U71(x1, x2)] | = | 0 |
[U81#(x1)] | = | 0 |
[u#] | = | 0 |
[isNeList#(x1)] | = | x1 + 0 |
[activate#(x1)] | = | 0 |
[n__i] | = | 44560 |
[__#(x1, x2)] | = | x1 + 0 |
[isNePal(x1)] | = | 0 |
[U72(x1)] | = | 0 |
[isQid#(x1)] | = | 0 |
[isPal#(x1)] | = | x1 + 48078 |
[n__nil] | = | 1 |
[U52#(x1)] | = | 0 |
[isQid(x1)] | = | x1 + 0 |
[n____(x1, x2)] | = | x1 + x2 + 6 |
[n__e] | = | 10282 |
[o] | = | 2 |
[U42#(x1)] | = | 0 |
[isList(x1)] | = | x1 + 4 |
[isNePal#(x1)] | = | x1 + 48076 |
[nil] | = | 1 |
[n__u] | = | 14098 |
[o#] | = | 0 |
[nil#] | = | 0 |
[isList#(x1)] | = | x1 + 2 |
[i] | = | 44561 |
[U52(x1)] | = | x1 + 0 |
[U61(x1)] | = | 0 |
[U51#(x1, x2)] | = | x1 + x2 + 3 |
[e] | = | 10282 |
[U11#(x1)] | = | 0 |
[U31(x1)] | = | x1 + 0 |
[U41#(x1, x2)] | = | x1 + x2 + 2 |
[a#] | = | 0 |
[U21#(x1, x2)] | = | x1 + x2 + 3 |
[U81(x1)] | = | 0 |
[U22#(x1)] | = | 0 |
[tt] | = | 1 |
[U71#(x1, x2)] | = | x1 + x2 + 0 |
[U22(x1)] | = | x1 + 0 |
[U51(x1, x2)] | = | x1 + x2 + 4 |
[U41(x1, x2)] | = | x1 + x2 + 3 |
[U31#(x1)] | = | 0 |
[__(x1, x2)] | = | x1 + x2 + 6 |
[U61#(x1)] | = | 0 |
[i#] | = | 0 |
isList(n____(V1,V2)) | → | U21(isList(activate(V1)),activate(V2)) | (18) |
U11(tt) | → | tt | (4) |
U41(tt,V2) | → | U42(isNeList(activate(V2))) | (8) |
__(__(X,Y),Z) | → | __(X,__(Y,Z)) | (1) |
__(nil,X) | → | X | (3) |
isList(V) | → | U11(isNeList(activate(V))) | (16) |
isNeList(n____(V1,V2)) | → | U51(isNeList(activate(V1)),activate(V2)) | (21) |
o | → | n__o | (36) |
isQid(n__a) | → | tt | (26) |
isNeList(V) | → | U31(isQid(activate(V))) | (19) |
__(X1,X2) | → | n____(X1,X2) | (32) |
isList(n__nil) | → | tt | (17) |
isQid(n__e) | → | tt | (27) |
e | → | n__e | (34) |
isQid(n__i) | → | tt | (28) |
activate(n__u) | → | u | (44) |
U21(tt,V2) | → | U22(isList(activate(V2))) | (5) |
a | → | n__a | (33) |
U51(tt,V2) | → | U52(isList(activate(V2))) | (10) |
activate(n____(X1,X2)) | → | __(X1,X2) | (39) |
U31(tt) | → | tt | (7) |
isNeList(n____(V1,V2)) | → | U41(isList(activate(V1)),activate(V2)) | (20) |
isQid(n__u) | → | tt | (30) |
nil | → | n__nil | (31) |
activate(X) | → | X | (45) |
U52(tt) | → | tt | (11) |
U42(tt) | → | tt | (9) |
activate(n__a) | → | a | (40) |
U22(tt) | → | tt | (6) |
activate(n__nil) | → | nil | (38) |
u | → | n__u | (37) |
activate(n__e) | → | e | (41) |
activate(n__i) | → | i | (42) |
i | → | n__i | (35) |
isQid(n__o) | → | tt | (29) |
activate(n__o) | → | o | (43) |
__(X,nil) | → | X | (2) |
__#(__(X,Y),Z) | → | __#(X,__(Y,Z)) | (52) |
__#(__(X,Y),Z) | → | __#(Y,Z) | (51) |
The dependency pairs are split into 0 components.