The rewrite relation of the following TRS is considered.
There are 155 ruless (increase limit for explicit display).
prec(__) | = | 12 | stat(__) | = | lex | |
prec(nil) | = | 14 | stat(nil) | = | mul | |
prec(U11) | = | 1 | stat(U11) | = | mul | |
prec(tt) | = | 13 | stat(tt) | = | mul | |
prec(isNeList) | = | 1 | stat(isNeList) | = | mul | |
prec(U21) | = | 4 | stat(U21) | = | lex | |
prec(U22) | = | 3 | stat(U22) | = | mul | |
prec(isList) | = | 2 | stat(isList) | = | mul | |
prec(U31) | = | 0 | stat(U31) | = | mul | |
prec(U41) | = | 5 | stat(U41) | = | lex | |
prec(U42) | = | 1 | stat(U42) | = | mul | |
prec(U51) | = | 6 | stat(U51) | = | lex | |
prec(U52) | = | 2 | stat(U52) | = | mul | |
prec(U61) | = | 7 | stat(U61) | = | mul | |
prec(U71) | = | 9 | stat(U71) | = | mul | |
prec(isNePal) | = | 8 | stat(isNePal) | = | mul | |
prec(and) | = | 10 | stat(and) | = | lex | |
prec(isPal) | = | 11 | stat(isPal) | = | mul | |
prec(a) | = | 15 | stat(a) | = | mul | |
prec(e) | = | 13 | stat(e) | = | mul | |
prec(i) | = | 13 | stat(i) | = | mul | |
prec(o) | = | 16 | stat(o) | = | mul | |
prec(u) | = | 13 | stat(u) | = | mul |
π(active) | = | 1 |
π(__) | = | [1,2] |
π(mark) | = | 1 |
π(nil) | = | [] |
π(U11) | = | [1,2] |
π(tt) | = | [] |
π(U12) | = | 1 |
π(isNeList) | = | [1] |
π(U21) | = | [1,2,3] |
π(U22) | = | [1,2] |
π(isList) | = | [1] |
π(U23) | = | 1 |
π(U31) | = | [1,2] |
π(U32) | = | 1 |
π(isQid) | = | 1 |
π(U41) | = | [1,3,2] |
π(U42) | = | [1,2] |
π(U43) | = | 1 |
π(U51) | = | [1,2,3] |
π(U52) | = | [1,2] |
π(U53) | = | 1 |
π(U61) | = | [1,2] |
π(U62) | = | 1 |
π(U71) | = | [1,2] |
π(U72) | = | 1 |
π(isNePal) | = | [1] |
π(and) | = | [2,1] |
π(isPalListKind) | = | 1 |
π(isPal) | = | [1] |
π(a) | = | [] |
π(e) | = | [] |
π(i) | = | [] |
π(o) | = | [] |
π(u) | = | [] |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(X,nil)) | → | mark(X) | (2) |
active(__(nil,X)) | → | mark(X) | (3) |
active(U11(tt,V)) | → | mark(U12(isNeList(V))) | (4) |
active(U21(tt,V1,V2)) | → | mark(U22(isList(V1),V2)) | (6) |
active(U22(tt,V2)) | → | mark(U23(isList(V2))) | (7) |
active(U31(tt,V)) | → | mark(U32(isQid(V))) | (9) |
active(U41(tt,V1,V2)) | → | mark(U42(isList(V1),V2)) | (11) |
active(U42(tt,V2)) | → | mark(U43(isNeList(V2))) | (12) |
active(U51(tt,V1,V2)) | → | mark(U52(isNeList(V1),V2)) | (14) |
active(U52(tt,V2)) | → | mark(U53(isList(V2))) | (15) |
active(U61(tt,V)) | → | mark(U62(isQid(V))) | (17) |
active(U71(tt,V)) | → | mark(U72(isNePal(V))) | (19) |
active(and(tt,X)) | → | mark(X) | (21) |
active(isList(V)) | → | mark(U11(isPalListKind(V),V)) | (22) |
active(isList(nil)) | → | mark(tt) | (23) |
active(isList(__(V1,V2))) | → | mark(U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)) | (24) |
active(isNeList(V)) | → | mark(U31(isPalListKind(V),V)) | (25) |
active(isNeList(__(V1,V2))) | → | mark(U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)) | (26) |
active(isNeList(__(V1,V2))) | → | mark(U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2)) | (27) |
active(isNePal(V)) | → | mark(U61(isPalListKind(V),V)) | (28) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))) | (29) |
active(isPal(V)) | → | mark(U71(isPalListKind(V),V)) | (30) |
active(isPal(nil)) | → | mark(tt) | (31) |
active(isPalListKind(a)) | → | mark(tt) | (32) |
active(isPalListKind(nil)) | → | mark(tt) | (35) |
active(isPalListKind(o)) | → | mark(tt) | (36) |
active(isPalListKind(__(V1,V2))) | → | mark(and(isPalListKind(V1),isPalListKind(V2))) | (38) |
active(isQid(a)) | → | mark(tt) | (39) |
active(isQid(o)) | → | mark(tt) | (42) |
[active(x1)] | = | 1 · x1 |
[U12(x1)] | = | 1 + 1 · x1 |
[tt] | = | 1 |
[mark(x1)] | = | 2 · x1 |
[U23(x1)] | = | 1 + 2 · x1 |
[U32(x1)] | = | 1 + 2 · x1 |
[U43(x1)] | = | 1 + 1 · x1 |
[U53(x1)] | = | 1 + 2 · x1 |
[U62(x1)] | = | 1 + 2 · x1 |
[U72(x1)] | = | 1 + 2 · x1 |
[isPalListKind(x1)] | = | 1 + 2 · x1 |
[e] | = | 1 |
[i] | = | 1 |
[u] | = | 1 |
[isQid(x1)] | = | 1 + 2 · x1 |
[__(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[nil] | = | 2 |
[U11(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[isNeList(x1)] | = | 1 + 2 · x1 |
[U21(x1, x2, x3)] | = | 1 + 2 · x1 + 2 · x2 + 2 · x3 |
[U22(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[isList(x1)] | = | 1 + 2 · x1 |
[U31(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U41(x1, x2, x3)] | = | 1 + 2 · x1 + 2 · x2 + 2 · x3 |
[U42(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U51(x1, x2, x3)] | = | 1 + 2 · x1 + 2 · x2 + 2 · x3 |
[U52(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U61(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U71(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[isNePal(x1)] | = | 1 + 2 · x1 |
[and(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[isPal(x1)] | = | 1 + 2 · x1 |
[a] | = | 1 |
[o] | = | 1 |
active(U23(tt)) | → | mark(tt) | (8) |
active(U32(tt)) | → | mark(tt) | (10) |
active(U53(tt)) | → | mark(tt) | (16) |
active(U62(tt)) | → | mark(tt) | (18) |
active(U72(tt)) | → | mark(tt) | (20) |
active(isPalListKind(e)) | → | mark(tt) | (33) |
active(isPalListKind(i)) | → | mark(tt) | (34) |
active(isPalListKind(u)) | → | mark(tt) | (37) |
active(isQid(e)) | → | mark(tt) | (40) |
active(isQid(i)) | → | mark(tt) | (41) |
active(isQid(u)) | → | mark(tt) | (43) |
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (44) |
mark(nil) | → | active(nil) | (45) |
mark(U11(X1,X2)) | → | active(U11(mark(X1),X2)) | (46) |
mark(tt) | → | active(tt) | (47) |
mark(U12(X)) | → | active(U12(mark(X))) | (48) |
mark(isNeList(X)) | → | active(isNeList(X)) | (49) |
mark(U21(X1,X2,X3)) | → | active(U21(mark(X1),X2,X3)) | (50) |
mark(U22(X1,X2)) | → | active(U22(mark(X1),X2)) | (51) |
mark(isList(X)) | → | active(isList(X)) | (52) |
mark(U23(X)) | → | active(U23(mark(X))) | (53) |
mark(U31(X1,X2)) | → | active(U31(mark(X1),X2)) | (54) |
mark(U32(X)) | → | active(U32(mark(X))) | (55) |
mark(isQid(X)) | → | active(isQid(X)) | (56) |
mark(U41(X1,X2,X3)) | → | active(U41(mark(X1),X2,X3)) | (57) |
mark(U42(X1,X2)) | → | active(U42(mark(X1),X2)) | (58) |
mark(U43(X)) | → | active(U43(mark(X))) | (59) |
mark(U51(X1,X2,X3)) | → | active(U51(mark(X1),X2,X3)) | (60) |
mark(U52(X1,X2)) | → | active(U52(mark(X1),X2)) | (61) |
mark(U53(X)) | → | active(U53(mark(X))) | (62) |
mark(U61(X1,X2)) | → | active(U61(mark(X1),X2)) | (63) |
mark(U62(X)) | → | active(U62(mark(X))) | (64) |
mark(U71(X1,X2)) | → | active(U71(mark(X1),X2)) | (65) |
mark(U72(X)) | → | active(U72(mark(X))) | (66) |
mark(isNePal(X)) | → | active(isNePal(X)) | (67) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (68) |
mark(isPalListKind(X)) | → | active(isPalListKind(X)) | (69) |
mark(isPal(X)) | → | active(isPal(X)) | (70) |
mark(a) | → | active(a) | (71) |
mark(e) | → | active(e) | (72) |
mark(i) | → | active(i) | (73) |
mark(o) | → | active(o) | (74) |
mark(u) | → | active(u) | (75) |
prec(tt) | = | 1 | weight(tt) | = | 1 | ||||
prec(active) | = | 27 | weight(active) | = | 0 | ||||
prec(U12) | = | 0 | weight(U12) | = | 1 | ||||
prec(mark) | = | 2 | weight(mark) | = | 1 | ||||
prec(U43) | = | 3 | weight(U43) | = | 1 | ||||
prec(isNeList) | = | 6 | weight(isNeList) | = | 1 | ||||
prec(isList) | = | 9 | weight(isList) | = | 1 | ||||
prec(U23) | = | 10 | weight(U23) | = | 1 | ||||
prec(U32) | = | 12 | weight(U32) | = | 1 | ||||
prec(isQid) | = | 13 | weight(isQid) | = | 1 | ||||
prec(U53) | = | 18 | weight(U53) | = | 1 | ||||
prec(U62) | = | 20 | weight(U62) | = | 1 | ||||
prec(U72) | = | 22 | weight(U72) | = | 1 | ||||
prec(isNePal) | = | 23 | weight(isNePal) | = | 1 | ||||
prec(isPalListKind) | = | 25 | weight(isPalListKind) | = | 1 | ||||
prec(isPal) | = | 26 | weight(isPal) | = | 1 | ||||
prec(__) | = | 4 | weight(__) | = | 0 | ||||
prec(U11) | = | 5 | weight(U11) | = | 0 | ||||
prec(U21) | = | 7 | weight(U21) | = | 0 | ||||
prec(U22) | = | 8 | weight(U22) | = | 0 | ||||
prec(U31) | = | 11 | weight(U31) | = | 0 | ||||
prec(U41) | = | 14 | weight(U41) | = | 0 | ||||
prec(U42) | = | 15 | weight(U42) | = | 0 | ||||
prec(U51) | = | 16 | weight(U51) | = | 0 | ||||
prec(U52) | = | 17 | weight(U52) | = | 0 | ||||
prec(U61) | = | 19 | weight(U61) | = | 0 | ||||
prec(U71) | = | 21 | weight(U71) | = | 0 | ||||
prec(and) | = | 24 | weight(and) | = | 0 |
active(U12(tt)) | → | mark(tt) | (5) |
active(U43(tt)) | → | mark(tt) | (13) |
__(mark(X1),X2) | → | __(X1,X2) | (76) |
__(X1,mark(X2)) | → | __(X1,X2) | (77) |
__(active(X1),X2) | → | __(X1,X2) | (78) |
__(X1,active(X2)) | → | __(X1,X2) | (79) |
U11(mark(X1),X2) | → | U11(X1,X2) | (80) |
U11(X1,mark(X2)) | → | U11(X1,X2) | (81) |
U11(active(X1),X2) | → | U11(X1,X2) | (82) |
U11(X1,active(X2)) | → | U11(X1,X2) | (83) |
U12(mark(X)) | → | U12(X) | (84) |
U12(active(X)) | → | U12(X) | (85) |
isNeList(mark(X)) | → | isNeList(X) | (86) |
isNeList(active(X)) | → | isNeList(X) | (87) |
U21(mark(X1),X2,X3) | → | U21(X1,X2,X3) | (88) |
U21(X1,mark(X2),X3) | → | U21(X1,X2,X3) | (89) |
U21(X1,X2,mark(X3)) | → | U21(X1,X2,X3) | (90) |
U21(active(X1),X2,X3) | → | U21(X1,X2,X3) | (91) |
U21(X1,active(X2),X3) | → | U21(X1,X2,X3) | (92) |
U21(X1,X2,active(X3)) | → | U21(X1,X2,X3) | (93) |
U22(mark(X1),X2) | → | U22(X1,X2) | (94) |
U22(X1,mark(X2)) | → | U22(X1,X2) | (95) |
U22(active(X1),X2) | → | U22(X1,X2) | (96) |
U22(X1,active(X2)) | → | U22(X1,X2) | (97) |
isList(mark(X)) | → | isList(X) | (98) |
isList(active(X)) | → | isList(X) | (99) |
U23(mark(X)) | → | U23(X) | (100) |
U23(active(X)) | → | U23(X) | (101) |
U31(mark(X1),X2) | → | U31(X1,X2) | (102) |
U31(X1,mark(X2)) | → | U31(X1,X2) | (103) |
U31(active(X1),X2) | → | U31(X1,X2) | (104) |
U31(X1,active(X2)) | → | U31(X1,X2) | (105) |
U32(mark(X)) | → | U32(X) | (106) |
U32(active(X)) | → | U32(X) | (107) |
isQid(mark(X)) | → | isQid(X) | (108) |
isQid(active(X)) | → | isQid(X) | (109) |
U41(mark(X1),X2,X3) | → | U41(X1,X2,X3) | (110) |
U41(X1,mark(X2),X3) | → | U41(X1,X2,X3) | (111) |
U41(X1,X2,mark(X3)) | → | U41(X1,X2,X3) | (112) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (113) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (114) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (115) |
U42(mark(X1),X2) | → | U42(X1,X2) | (116) |
U42(X1,mark(X2)) | → | U42(X1,X2) | (117) |
U42(active(X1),X2) | → | U42(X1,X2) | (118) |
U42(X1,active(X2)) | → | U42(X1,X2) | (119) |
U43(mark(X)) | → | U43(X) | (120) |
U43(active(X)) | → | U43(X) | (121) |
U51(mark(X1),X2,X3) | → | U51(X1,X2,X3) | (122) |
U51(X1,mark(X2),X3) | → | U51(X1,X2,X3) | (123) |
U51(X1,X2,mark(X3)) | → | U51(X1,X2,X3) | (124) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (125) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (126) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (127) |
U52(mark(X1),X2) | → | U52(X1,X2) | (128) |
U52(X1,mark(X2)) | → | U52(X1,X2) | (129) |
U52(active(X1),X2) | → | U52(X1,X2) | (130) |
U52(X1,active(X2)) | → | U52(X1,X2) | (131) |
U53(mark(X)) | → | U53(X) | (132) |
U53(active(X)) | → | U53(X) | (133) |
U61(mark(X1),X2) | → | U61(X1,X2) | (134) |
U61(X1,mark(X2)) | → | U61(X1,X2) | (135) |
U61(active(X1),X2) | → | U61(X1,X2) | (136) |
U61(X1,active(X2)) | → | U61(X1,X2) | (137) |
U62(mark(X)) | → | U62(X) | (138) |
U62(active(X)) | → | U62(X) | (139) |
U71(mark(X1),X2) | → | U71(X1,X2) | (140) |
U71(X1,mark(X2)) | → | U71(X1,X2) | (141) |
U71(active(X1),X2) | → | U71(X1,X2) | (142) |
U71(X1,active(X2)) | → | U71(X1,X2) | (143) |
U72(mark(X)) | → | U72(X) | (144) |
U72(active(X)) | → | U72(X) | (145) |
isNePal(mark(X)) | → | isNePal(X) | (146) |
isNePal(active(X)) | → | isNePal(X) | (147) |
and(mark(X1),X2) | → | and(X1,X2) | (148) |
and(X1,mark(X2)) | → | and(X1,X2) | (149) |
and(active(X1),X2) | → | and(X1,X2) | (150) |
and(X1,active(X2)) | → | and(X1,X2) | (151) |
isPalListKind(mark(X)) | → | isPalListKind(X) | (152) |
isPalListKind(active(X)) | → | isPalListKind(X) | (153) |
isPal(mark(X)) | → | isPal(X) | (154) |
isPal(active(X)) | → | isPal(X) | (155) |
There are no rules in the TRS. Hence, it is terminating.