The rewrite relation of the following TRS is considered.
There are 154 ruless (increase limit for explicit display).
The evaluation strategy is innermost.prec(a____) | = | 30 | stat(a____) | = | lex | |
prec(__) | = | 30 | stat(__) | = | lex | |
prec(nil) | = | 14 | stat(nil) | = | mul | |
prec(a__U11) | = | 4 | stat(a__U11) | = | mul | |
prec(tt) | = | 14 | stat(tt) | = | mul | |
prec(a__U12) | = | 3 | stat(a__U12) | = | mul | |
prec(a__isNeList) | = | 3 | stat(a__isNeList) | = | mul | |
prec(a__U21) | = | 18 | stat(a__U21) | = | mul | |
prec(a__U22) | = | 17 | stat(a__U22) | = | mul | |
prec(a__U23) | = | 16 | stat(a__U23) | = | mul | |
prec(a__U24) | = | 15 | stat(a__U24) | = | mul | |
prec(a__U25) | = | 6 | stat(a__U25) | = | mul | |
prec(a__isList) | = | 6 | stat(a__isList) | = | mul | |
prec(a__U31) | = | 2 | stat(a__U31) | = | mul | |
prec(a__U32) | = | 1 | stat(a__U32) | = | mul | |
prec(a__isQid) | = | 0 | stat(a__isQid) | = | mul | |
prec(a__U41) | = | 24 | stat(a__U41) | = | mul | |
prec(a__U42) | = | 23 | stat(a__U42) | = | mul | |
prec(a__U43) | = | 22 | stat(a__U43) | = | mul | |
prec(a__U44) | = | 21 | stat(a__U44) | = | mul | |
prec(a__U45) | = | 20 | stat(a__U45) | = | mul | |
prec(a__U46) | = | 19 | stat(a__U46) | = | mul | |
prec(a__U51) | = | 27 | stat(a__U51) | = | mul | |
prec(a__U52) | = | 26 | stat(a__U52) | = | mul | |
prec(a__U53) | = | 25 | stat(a__U53) | = | mul | |
prec(a__U54) | = | 14 | stat(a__U54) | = | mul | |
prec(a__U55) | = | 6 | stat(a__U55) | = | mul | |
prec(a__U56) | = | 5 | stat(a__U56) | = | mul | |
prec(a__U61) | = | 7 | stat(a__U61) | = | mul | |
prec(a__U62) | = | 0 | stat(a__U62) | = | mul | |
prec(a__U71) | = | 28 | stat(a__U71) | = | mul | |
prec(a__U72) | = | 13 | stat(a__U72) | = | mul | |
prec(a__U73) | = | 8 | stat(a__U73) | = | mul | |
prec(a__isPal) | = | 12 | stat(a__isPal) | = | mul | |
prec(a__U81) | = | 11 | stat(a__U81) | = | mul | |
prec(a__U82) | = | 10 | stat(a__U82) | = | mul | |
prec(a__isNePal) | = | 9 | stat(a__isNePal) | = | mul | |
prec(a__U91) | = | 29 | stat(a__U91) | = | mul | |
prec(a) | = | 31 | stat(a) | = | mul | |
prec(e) | = | 32 | stat(e) | = | mul | |
prec(i) | = | 33 | stat(i) | = | mul | |
prec(o) | = | 14 | stat(o) | = | mul | |
prec(u) | = | 34 | stat(u) | = | mul | |
prec(U11) | = | 4 | stat(U11) | = | mul | |
prec(U12) | = | 3 | stat(U12) | = | mul | |
prec(isNeList) | = | 3 | stat(isNeList) | = | mul | |
prec(U21) | = | 18 | stat(U21) | = | mul | |
prec(U22) | = | 17 | stat(U22) | = | mul | |
prec(U23) | = | 16 | stat(U23) | = | mul | |
prec(U24) | = | 15 | stat(U24) | = | mul | |
prec(U25) | = | 6 | stat(U25) | = | mul | |
prec(isList) | = | 6 | stat(isList) | = | mul | |
prec(U31) | = | 2 | stat(U31) | = | mul | |
prec(U32) | = | 1 | stat(U32) | = | mul | |
prec(isQid) | = | 0 | stat(isQid) | = | mul | |
prec(U41) | = | 24 | stat(U41) | = | mul | |
prec(U42) | = | 23 | stat(U42) | = | mul | |
prec(U43) | = | 22 | stat(U43) | = | mul | |
prec(U44) | = | 21 | stat(U44) | = | mul | |
prec(U45) | = | 20 | stat(U45) | = | mul | |
prec(U46) | = | 19 | stat(U46) | = | mul | |
prec(U51) | = | 27 | stat(U51) | = | mul | |
prec(U52) | = | 26 | stat(U52) | = | mul | |
prec(U53) | = | 25 | stat(U53) | = | mul | |
prec(U54) | = | 14 | stat(U54) | = | mul | |
prec(U55) | = | 6 | stat(U55) | = | mul | |
prec(U56) | = | 5 | stat(U56) | = | mul | |
prec(U61) | = | 7 | stat(U61) | = | mul | |
prec(U62) | = | 0 | stat(U62) | = | mul | |
prec(U71) | = | 28 | stat(U71) | = | mul | |
prec(U72) | = | 13 | stat(U72) | = | mul | |
prec(U73) | = | 8 | stat(U73) | = | mul | |
prec(isPal) | = | 12 | stat(isPal) | = | mul | |
prec(U81) | = | 11 | stat(U81) | = | mul | |
prec(U82) | = | 10 | stat(U82) | = | mul | |
prec(isNePal) | = | 9 | stat(isNePal) | = | mul | |
prec(U91) | = | 29 | stat(U91) | = | mul |
π(a____) | = | [1,2] |
π(__) | = | [1,2] |
π(mark) | = | 1 |
π(nil) | = | [] |
π(a__U11) | = | [1,2] |
π(tt) | = | [] |
π(a__U12) | = | [1,2] |
π(a__isPalListKind) | = | 1 |
π(a__U13) | = | 1 |
π(a__isNeList) | = | [1] |
π(a__U21) | = | [1,2,3] |
π(a__U22) | = | [1,2,3] |
π(a__U23) | = | [1,2,3] |
π(a__U24) | = | [1,2,3] |
π(a__U25) | = | [1,2] |
π(a__isList) | = | [1] |
π(a__U26) | = | 1 |
π(a__U31) | = | [1,2] |
π(a__U32) | = | [1,2] |
π(a__U33) | = | 1 |
π(a__isQid) | = | [1] |
π(a__U41) | = | [1,2,3] |
π(a__U42) | = | [1,2,3] |
π(a__U43) | = | [1,2,3] |
π(a__U44) | = | [1,2,3] |
π(a__U45) | = | [1,2] |
π(a__U46) | = | [1] |
π(a__U51) | = | [1,2,3] |
π(a__U52) | = | [1,2,3] |
π(a__U53) | = | [1,2,3] |
π(a__U54) | = | [1,2,3] |
π(a__U55) | = | [1,2] |
π(a__U56) | = | [1] |
π(a__U61) | = | [1,2] |
π(a__U62) | = | [1,2] |
π(a__U63) | = | 1 |
π(a__U71) | = | [1,2,3] |
π(a__U72) | = | [1,2] |
π(a__U73) | = | [1,2] |
π(a__isPal) | = | [1] |
π(a__U74) | = | 1 |
π(a__U81) | = | [1,2] |
π(a__U82) | = | [1,2] |
π(a__U83) | = | 1 |
π(a__isNePal) | = | [1] |
π(a__U91) | = | [1,2] |
π(a__U92) | = | 1 |
π(a) | = | [] |
π(e) | = | [] |
π(i) | = | [] |
π(o) | = | [] |
π(u) | = | [] |
π(U11) | = | [1,2] |
π(U12) | = | [1,2] |
π(isPalListKind) | = | 1 |
π(U13) | = | 1 |
π(isNeList) | = | [1] |
π(U21) | = | [1,2,3] |
π(U22) | = | [1,2,3] |
π(U23) | = | [1,2,3] |
π(U24) | = | [1,2,3] |
π(U25) | = | [1,2] |
π(isList) | = | [1] |
π(U26) | = | 1 |
π(U31) | = | [1,2] |
π(U32) | = | [1,2] |
π(U33) | = | 1 |
π(isQid) | = | [1] |
π(U41) | = | [1,2,3] |
π(U42) | = | [1,2,3] |
π(U43) | = | [1,2,3] |
π(U44) | = | [1,2,3] |
π(U45) | = | [1,2] |
π(U46) | = | [1] |
π(U51) | = | [1,2,3] |
π(U52) | = | [1,2,3] |
π(U53) | = | [1,2,3] |
π(U54) | = | [1,2,3] |
π(U55) | = | [1,2] |
π(U56) | = | [1] |
π(U61) | = | [1,2] |
π(U62) | = | [1,2] |
π(U63) | = | 1 |
π(U71) | = | [1,2,3] |
π(U72) | = | [1,2] |
π(U73) | = | [1,2] |
π(isPal) | = | [1] |
π(U74) | = | 1 |
π(U81) | = | [1,2] |
π(U82) | = | [1,2] |
π(U83) | = | 1 |
π(isNePal) | = | [1] |
π(U91) | = | [1,2] |
π(U92) | = | 1 |
a____(__(X,Y),Z) | → | a____(mark(X),a____(mark(Y),mark(Z))) | (1) |
a____(X,nil) | → | mark(X) | (2) |
a____(nil,X) | → | mark(X) | (3) |
a__U11(tt,V) | → | a__U12(a__isPalListKind(V),V) | (4) |
a__U12(tt,V) | → | a__U13(a__isNeList(V)) | (5) |
a__U21(tt,V1,V2) | → | a__U22(a__isPalListKind(V1),V1,V2) | (7) |
a__U22(tt,V1,V2) | → | a__U23(a__isPalListKind(V2),V1,V2) | (8) |
a__U23(tt,V1,V2) | → | a__U24(a__isPalListKind(V2),V1,V2) | (9) |
a__U24(tt,V1,V2) | → | a__U25(a__isList(V1),V2) | (10) |
a__U25(tt,V2) | → | a__U26(a__isList(V2)) | (11) |
a__U31(tt,V) | → | a__U32(a__isPalListKind(V),V) | (13) |
a__U32(tt,V) | → | a__U33(a__isQid(V)) | (14) |
a__U41(tt,V1,V2) | → | a__U42(a__isPalListKind(V1),V1,V2) | (16) |
a__U42(tt,V1,V2) | → | a__U43(a__isPalListKind(V2),V1,V2) | (17) |
a__U43(tt,V1,V2) | → | a__U44(a__isPalListKind(V2),V1,V2) | (18) |
a__U44(tt,V1,V2) | → | a__U45(a__isList(V1),V2) | (19) |
a__U45(tt,V2) | → | a__U46(a__isNeList(V2)) | (20) |
a__U46(tt) | → | tt | (21) |
a__U51(tt,V1,V2) | → | a__U52(a__isPalListKind(V1),V1,V2) | (22) |
a__U52(tt,V1,V2) | → | a__U53(a__isPalListKind(V2),V1,V2) | (23) |
a__U53(tt,V1,V2) | → | a__U54(a__isPalListKind(V2),V1,V2) | (24) |
a__U54(tt,V1,V2) | → | a__U55(a__isNeList(V1),V2) | (25) |
a__U55(tt,V2) | → | a__U56(a__isList(V2)) | (26) |
a__U56(tt) | → | tt | (27) |
a__U61(tt,V) | → | a__U62(a__isPalListKind(V),V) | (28) |
a__U62(tt,V) | → | a__U63(a__isQid(V)) | (29) |
a__U71(tt,I,P) | → | a__U72(a__isPalListKind(I),P) | (31) |
a__U72(tt,P) | → | a__U73(a__isPal(P),P) | (32) |
a__U73(tt,P) | → | a__U74(a__isPalListKind(P)) | (33) |
a__U81(tt,V) | → | a__U82(a__isPalListKind(V),V) | (35) |
a__U82(tt,V) | → | a__U83(a__isNePal(V)) | (36) |
a__U91(tt,V2) | → | a__U92(a__isPalListKind(V2)) | (38) |
a__isList(V) | → | a__U11(a__isPalListKind(V),V) | (40) |
a__isList(nil) | → | tt | (41) |
a__isList(__(V1,V2)) | → | a__U21(a__isPalListKind(V1),V1,V2) | (42) |
a__isNeList(V) | → | a__U31(a__isPalListKind(V),V) | (43) |
a__isNeList(__(V1,V2)) | → | a__U41(a__isPalListKind(V1),V1,V2) | (44) |
a__isNeList(__(V1,V2)) | → | a__U51(a__isPalListKind(V1),V1,V2) | (45) |
a__isNePal(V) | → | a__U61(a__isPalListKind(V),V) | (46) |
a__isNePal(__(I,__(P,I))) | → | a__U71(a__isQid(I),I,P) | (47) |
a__isPal(V) | → | a__U81(a__isPalListKind(V),V) | (48) |
a__isPal(nil) | → | tt | (49) |
a__isPalListKind(a) | → | tt | (50) |
a__isPalListKind(e) | → | tt | (51) |
a__isPalListKind(i) | → | tt | (52) |
a__isPalListKind(u) | → | tt | (55) |
a__isPalListKind(__(V1,V2)) | → | a__U91(a__isPalListKind(V1),V2) | (56) |
a__isQid(a) | → | tt | (57) |
a__isQid(e) | → | tt | (58) |
a__isQid(i) | → | tt | (59) |
a__isQid(o) | → | tt | (60) |
a__isQid(u) | → | tt | (61) |
[a__U13(x1)] | = | 2 + 2 · x1 |
[tt] | = | 1 |
[a__U26(x1)] | = | 2 + 2 · x1 |
[a__U33(x1)] | = | 2 + 2 · x1 |
[a__U63(x1)] | = | 2 + 2 · x1 |
[a__U74(x1)] | = | 2 + 2 · x1 |
[a__U83(x1)] | = | 2 + 2 · x1 |
[a__U92(x1)] | = | 2 + 2 · x1 |
[a__isPalListKind(x1)] | = | 2 + 2 · x1 |
[nil] | = | 1 |
[o] | = | 1 |
[mark(x1)] | = | 2 · x1 |
[__(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a____(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U11(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U12(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[isPalListKind(x1)] | = | 1 + 2 · x1 |
[U13(x1)] | = | 1 + 2 · x1 |
[isNeList(x1)] | = | 1 + 2 · x1 |
[a__isNeList(x1)] | = | 2 + 2 · x1 |
[U21(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U21(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U22(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U22(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U23(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[a__U23(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U24(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U24(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U25(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U25(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[isList(x1)] | = | 1 + 2 · x1 |
[a__isList(x1)] | = | 2 + 2 · x1 |
[U26(x1)] | = | 1 + 2 · x1 |
[U31(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U31(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U32(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U32(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U33(x1)] | = | 1 + 2 · x1 |
[isQid(x1)] | = | 1 + 2 · x1 |
[a__isQid(x1)] | = | 2 + 2 · x1 |
[U41(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U41(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U42(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U42(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U43(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U44(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U44(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U45(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U46(x1)] | = | 1 + 1 · x1 |
[a__U46(x1)] | = | 2 + 1 · x1 |
[U51(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U51(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U52(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U52(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U53(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U53(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U54(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U54(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U55(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U55(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U56(x1)] | = | 1 + 1 · x1 |
[a__U56(x1)] | = | 2 + 1 · x1 |
[U61(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U61(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U62(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U63(x1)] | = | 1 + 2 · x1 |
[U71(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[a__U71(x1, x2, x3)] | = | 2 + 1 · x1 + 2 · x2 + 2 · x3 |
[U72(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U72(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U73(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U73(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[isPal(x1)] | = | 1 + 2 · x1 |
[a__isPal(x1)] | = | 2 + 2 · x1 |
[U74(x1)] | = | 1 + 2 · x1 |
[U81(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U81(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[a__U82(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U83(x1)] | = | 1 + 2 · x1 |
[isNePal(x1)] | = | 1 + 2 · x1 |
[a__isNePal(x1)] | = | 2 + 2 · x1 |
[U91(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[a__U91(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U92(x1)] | = | 1 + 2 · x1 |
[a] | = | 1 |
[e] | = | 1 |
[i] | = | 1 |
[u] | = | 1 |
a__U13(tt) | → | tt | (6) |
a__U26(tt) | → | tt | (12) |
a__U33(tt) | → | tt | (15) |
a__U63(tt) | → | tt | (30) |
a__U74(tt) | → | tt | (34) |
a__U83(tt) | → | tt | (37) |
a__U92(tt) | → | tt | (39) |
a__isPalListKind(nil) | → | tt | (53) |
a__isPalListKind(o) | → | tt | (54) |
mark(nil) | → | nil | (105) |
mark(tt) | → | tt | (106) |
mark(a) | → | a | (107) |
mark(e) | → | e | (108) |
mark(i) | → | i | (109) |
mark(o) | → | o | (110) |
mark(u) | → | u | (111) |
a____(X1,X2) | → | __(X1,X2) | (112) |
a__U11(X1,X2) | → | U11(X1,X2) | (113) |
a__U12(X1,X2) | → | U12(X1,X2) | (114) |
a__isPalListKind(X) | → | isPalListKind(X) | (115) |
a__U13(X) | → | U13(X) | (116) |
a__isNeList(X) | → | isNeList(X) | (117) |
a__U21(X1,X2,X3) | → | U21(X1,X2,X3) | (118) |
a__U22(X1,X2,X3) | → | U22(X1,X2,X3) | (119) |
a__U23(X1,X2,X3) | → | U23(X1,X2,X3) | (120) |
a__U24(X1,X2,X3) | → | U24(X1,X2,X3) | (121) |
a__U25(X1,X2) | → | U25(X1,X2) | (122) |
a__isList(X) | → | isList(X) | (123) |
a__U26(X) | → | U26(X) | (124) |
a__U31(X1,X2) | → | U31(X1,X2) | (125) |
a__U32(X1,X2) | → | U32(X1,X2) | (126) |
a__U33(X) | → | U33(X) | (127) |
a__isQid(X) | → | isQid(X) | (128) |
a__U41(X1,X2,X3) | → | U41(X1,X2,X3) | (129) |
a__U42(X1,X2,X3) | → | U42(X1,X2,X3) | (130) |
a__U43(X1,X2,X3) | → | U43(X1,X2,X3) | (131) |
a__U44(X1,X2,X3) | → | U44(X1,X2,X3) | (132) |
a__U45(X1,X2) | → | U45(X1,X2) | (133) |
a__U46(X) | → | U46(X) | (134) |
a__U51(X1,X2,X3) | → | U51(X1,X2,X3) | (135) |
a__U52(X1,X2,X3) | → | U52(X1,X2,X3) | (136) |
a__U53(X1,X2,X3) | → | U53(X1,X2,X3) | (137) |
a__U54(X1,X2,X3) | → | U54(X1,X2,X3) | (138) |
a__U55(X1,X2) | → | U55(X1,X2) | (139) |
a__U56(X) | → | U56(X) | (140) |
a__U61(X1,X2) | → | U61(X1,X2) | (141) |
a__U62(X1,X2) | → | U62(X1,X2) | (142) |
a__U63(X) | → | U63(X) | (143) |
a__U71(X1,X2,X3) | → | U71(X1,X2,X3) | (144) |
a__U72(X1,X2) | → | U72(X1,X2) | (145) |
a__U73(X1,X2) | → | U73(X1,X2) | (146) |
a__isPal(X) | → | isPal(X) | (147) |
a__U74(X) | → | U74(X) | (148) |
a__U81(X1,X2) | → | U81(X1,X2) | (149) |
a__U82(X1,X2) | → | U82(X1,X2) | (150) |
a__U83(X) | → | U83(X) | (151) |
a__isNePal(X) | → | isNePal(X) | (152) |
a__U91(X1,X2) | → | U91(X1,X2) | (153) |
a__U92(X) | → | U92(X) | (154) |
[mark(x1)] | = | 1 + 2 · x1 |
[__(x1, x2)] | = | 2 + 2 · x1 + 2 · x2 |
[a____(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U11(x1, x2)] | = | 2 + 2 · x1 + 2 · x2 |
[a__U11(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 2 + 2 · x1 + 1 · x2 |
[a__U12(x1, x2)] | = | 2 · x1 + 2 · x2 |
[isPalListKind(x1)] | = | 2 · x1 |
[a__isPalListKind(x1)] | = | 2 · x1 |
[U13(x1)] | = | 2 + 2 · x1 |
[a__U13(x1)] | = | 1 + 1 · x1 |
[isNeList(x1)] | = | 2 + 1 · x1 |
[a__isNeList(x1)] | = | 2 + 2 · x1 |
[U21(x1, x2, x3)] | = | 1 + 2 · x1 + 2 · x2 + 1 · x3 |
[a__U21(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U22(x1, x2, x3)] | = | 2 + 2 · x1 + 1 · x2 + 1 · x3 |
[a__U22(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U23(x1, x2, x3)] | = | 1 + 2 · x1 + 2 · x2 + 2 · x3 |
[a__U23(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U24(x1, x2, x3)] | = | 2 + 2 · x1 + 1 · x2 + 1 · x3 |
[a__U24(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U25(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[a__U25(x1, x2)] | = | 1 · x1 + 2 · x2 |
[isList(x1)] | = | 1 · x1 |
[a__isList(x1)] | = | 2 · x1 |
[U26(x1)] | = | 2 · x1 |
[a__U26(x1)] | = | 1 · x1 |
[U31(x1, x2)] | = | 2 · x1 + 1 · x2 |
[a__U31(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U32(x1, x2)] | = | 2 + 2 · x1 + 1 · x2 |
[a__U32(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U33(x1)] | = | 2 + 2 · x1 |
[a__U33(x1)] | = | 2 · x1 |
[isQid(x1)] | = | 2 · x1 |
[a__isQid(x1)] | = | 2 · x1 |
[U41(x1, x2, x3)] | = | 2 + 2 · x1 + 1 · x2 + 2 · x3 |
[a__U41(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U42(x1, x2, x3)] | = | 2 + 2 · x1 + 2 · x2 + 2 · x3 |
[a__U42(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 2 + 2 · x1 + 2 · x2 + 2 · x3 |
[a__U43(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U44(x1, x2, x3)] | = | 2 + 2 · x1 + 1 · x2 + 1 · x3 |
[a__U44(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 2 + 2 · x1 + 2 · x2 |
[a__U45(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U46(x1)] | = | 2 + 2 · x1 |
[a__U46(x1)] | = | 1 + 1 · x1 |
[U51(x1, x2, x3)] | = | 2 + 2 · x1 + 2 · x2 + 2 · x3 |
[a__U51(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U52(x1, x2, x3)] | = | 1 + 2 · x1 + 2 · x2 + 2 · x3 |
[a__U52(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U53(x1, x2, x3)] | = | 2 + 2 · x1 + 2 · x2 + 2 · x3 |
[a__U53(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U54(x1, x2, x3)] | = | 1 + 2 · x1 + 2 · x2 + 1 · x3 |
[a__U54(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U55(x1, x2)] | = | 2 + 2 · x1 + 1 · x2 |
[a__U55(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U56(x1)] | = | 2 + 2 · x1 |
[a__U56(x1)] | = | 1 + 1 · x1 |
[U61(x1, x2)] | = | 1 + 2 · x1 + 1 · x2 |
[a__U61(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 2 + 2 · x1 + 1 · x2 |
[a__U62(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U63(x1)] | = | 2 + 2 · x1 |
[a__U63(x1)] | = | 1 + 1 · x1 |
[U71(x1, x2, x3)] | = | 2 + 2 · x1 + 1 · x2 + 2 · x3 |
[a__U71(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U72(x1, x2)] | = | 2 + 2 · x1 + 2 · x2 |
[a__U72(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U73(x1, x2)] | = | 2 + 2 · x1 + 2 · x2 |
[a__U73(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[isPal(x1)] | = | 1 · x1 |
[a__isPal(x1)] | = | 1 + 2 · x1 |
[U74(x1)] | = | 2 + 2 · x1 |
[a__U74(x1)] | = | 1 + 1 · x1 |
[U81(x1, x2)] | = | 2 + 2 · x1 + 1 · x2 |
[a__U81(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 2 + 2 · x1 + 2 · x2 |
[a__U82(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U83(x1)] | = | 2 + 2 · x1 |
[a__U83(x1)] | = | 1 + 1 · x1 |
[isNePal(x1)] | = | 2 · x1 |
[a__isNePal(x1)] | = | 1 + 2 · x1 |
[U91(x1, x2)] | = | 2 + 2 · x1 + 2 · x2 |
[a__U91(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U92(x1)] | = | 2 + 2 · x1 |
[a__U92(x1)] | = | 2 · x1 |
mark(__(X1,X2)) | → | a____(mark(X1),mark(X2)) | (62) |
mark(U11(X1,X2)) | → | a__U11(mark(X1),X2) | (63) |
mark(U12(X1,X2)) | → | a__U12(mark(X1),X2) | (64) |
mark(isPalListKind(X)) | → | a__isPalListKind(X) | (65) |
mark(U13(X)) | → | a__U13(mark(X)) | (66) |
mark(isNeList(X)) | → | a__isNeList(X) | (67) |
mark(U21(X1,X2,X3)) | → | a__U21(mark(X1),X2,X3) | (68) |
mark(U22(X1,X2,X3)) | → | a__U22(mark(X1),X2,X3) | (69) |
mark(U23(X1,X2,X3)) | → | a__U23(mark(X1),X2,X3) | (70) |
mark(U24(X1,X2,X3)) | → | a__U24(mark(X1),X2,X3) | (71) |
mark(U25(X1,X2)) | → | a__U25(mark(X1),X2) | (72) |
mark(isList(X)) | → | a__isList(X) | (73) |
mark(U32(X1,X2)) | → | a__U32(mark(X1),X2) | (76) |
mark(U33(X)) | → | a__U33(mark(X)) | (77) |
mark(isQid(X)) | → | a__isQid(X) | (78) |
mark(U41(X1,X2,X3)) | → | a__U41(mark(X1),X2,X3) | (79) |
mark(U42(X1,X2,X3)) | → | a__U42(mark(X1),X2,X3) | (80) |
mark(U43(X1,X2,X3)) | → | a__U43(mark(X1),X2,X3) | (81) |
mark(U44(X1,X2,X3)) | → | a__U44(mark(X1),X2,X3) | (82) |
mark(U45(X1,X2)) | → | a__U45(mark(X1),X2) | (83) |
mark(U46(X)) | → | a__U46(mark(X)) | (84) |
mark(U51(X1,X2,X3)) | → | a__U51(mark(X1),X2,X3) | (85) |
mark(U52(X1,X2,X3)) | → | a__U52(mark(X1),X2,X3) | (86) |
mark(U53(X1,X2,X3)) | → | a__U53(mark(X1),X2,X3) | (87) |
mark(U54(X1,X2,X3)) | → | a__U54(mark(X1),X2,X3) | (88) |
mark(U55(X1,X2)) | → | a__U55(mark(X1),X2) | (89) |
mark(U56(X)) | → | a__U56(mark(X)) | (90) |
mark(U61(X1,X2)) | → | a__U61(mark(X1),X2) | (91) |
mark(U62(X1,X2)) | → | a__U62(mark(X1),X2) | (92) |
mark(U63(X)) | → | a__U63(mark(X)) | (93) |
mark(U71(X1,X2,X3)) | → | a__U71(mark(X1),X2,X3) | (94) |
mark(U72(X1,X2)) | → | a__U72(mark(X1),X2) | (95) |
mark(U73(X1,X2)) | → | a__U73(mark(X1),X2) | (96) |
mark(U74(X)) | → | a__U74(mark(X)) | (98) |
mark(U81(X1,X2)) | → | a__U81(mark(X1),X2) | (99) |
mark(U82(X1,X2)) | → | a__U82(mark(X1),X2) | (100) |
mark(U83(X)) | → | a__U83(mark(X)) | (101) |
mark(U91(X1,X2)) | → | a__U91(mark(X1),X2) | (103) |
mark(U92(X)) | → | a__U92(mark(X)) | (104) |
prec(mark) | = | 7 | weight(mark) | = | 3 | ||||
prec(U26) | = | 0 | weight(U26) | = | 2 | ||||
prec(a__U26) | = | 8 | weight(a__U26) | = | 1 | ||||
prec(isPal) | = | 2 | weight(isPal) | = | 1 | ||||
prec(a__isPal) | = | 4 | weight(a__isPal) | = | 4 | ||||
prec(isNePal) | = | 1 | weight(isNePal) | = | 1 | ||||
prec(a__isNePal) | = | 5 | weight(a__isNePal) | = | 3 | ||||
prec(U31) | = | 6 | weight(U31) | = | 1 | ||||
prec(a__U31) | = | 3 | weight(a__U31) | = | 0 |
mark(U26(X)) | → | a__U26(mark(X)) | (74) |
mark(U31(X1,X2)) | → | a__U31(mark(X1),X2) | (75) |
mark(isPal(X)) | → | a__isPal(X) | (97) |
mark(isNePal(X)) | → | a__isNePal(X) | (102) |
There are no rules in the TRS. Hence, it is terminating.