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