The rewrite relation of the following TRS is considered.
There are 232 ruless (increase limit for explicit display).
prec(__) | = | 30 | stat(__) | = | lex | |
prec(nil) | = | 31 | stat(nil) | = | mul | |
prec(U11) | = | 8 | stat(U11) | = | mul | |
prec(tt) | = | 1 | stat(tt) | = | mul | |
prec(U12) | = | 7 | stat(U12) | = | lex | |
prec(isPalListKind) | = | 2 | stat(isPalListKind) | = | mul | |
prec(isNeList) | = | 6 | stat(isNeList) | = | mul | |
prec(U21) | = | 15 | stat(U21) | = | mul | |
prec(U22) | = | 14 | stat(U22) | = | lex | |
prec(U23) | = | 13 | stat(U23) | = | lex | |
prec(U24) | = | 12 | stat(U24) | = | lex | |
prec(U25) | = | 11 | stat(U25) | = | mul | |
prec(isList) | = | 11 | stat(isList) | = | mul | |
prec(U26) | = | 9 | stat(U26) | = | mul | |
prec(U31) | = | 5 | stat(U31) | = | mul | |
prec(U32) | = | 4 | stat(U32) | = | mul | |
prec(U33) | = | 3 | stat(U33) | = | mul | |
prec(U41) | = | 18 | stat(U41) | = | lex | |
prec(U42) | = | 17 | stat(U42) | = | lex | |
prec(U43) | = | 16 | stat(U43) | = | mul | |
prec(U44) | = | 11 | stat(U44) | = | mul | |
prec(U45) | = | 10 | stat(U45) | = | mul | |
prec(U51) | = | 22 | stat(U51) | = | mul | |
prec(U52) | = | 21 | stat(U52) | = | lex | |
prec(U53) | = | 20 | stat(U53) | = | mul | |
prec(U54) | = | 19 | stat(U54) | = | mul | |
prec(U55) | = | 11 | stat(U55) | = | mul | |
prec(U61) | = | 24 | stat(U61) | = | mul | |
prec(U62) | = | 23 | stat(U62) | = | mul | |
prec(U63) | = | 0 | stat(U63) | = | mul | |
prec(U71) | = | 29 | stat(U71) | = | lex | |
prec(U72) | = | 28 | stat(U72) | = | lex | |
prec(U73) | = | 2 | stat(U73) | = | mul | |
prec(isPal) | = | 27 | stat(isPal) | = | mul | |
prec(U81) | = | 26 | stat(U81) | = | mul | |
prec(U82) | = | 25 | stat(U82) | = | mul | |
prec(isNePal) | = | 25 | stat(isNePal) | = | mul | |
prec(U91) | = | 2 | stat(U91) | = | mul | |
prec(a) | = | 1 | stat(a) | = | mul | |
prec(e) | = | 1 | stat(e) | = | mul | |
prec(i) | = | 32 | stat(i) | = | mul | |
prec(o) | = | 1 | stat(o) | = | mul | |
prec(u) | = | 1 | stat(u) | = | mul | |
prec(top) | = | 33 | stat(top) | = | mul |
π(active) | = | 1 |
π(__) | = | [1,2] |
π(mark) | = | 1 |
π(nil) | = | [] |
π(U11) | = | [1,2] |
π(tt) | = | [] |
π(U12) | = | [1,2] |
π(isPalListKind) | = | [1] |
π(U13) | = | 1 |
π(isNeList) | = | [1] |
π(U21) | = | [1,2,3] |
π(U22) | = | [1,3,2] |
π(U23) | = | [3,2,1] |
π(U24) | = | [2,1,3] |
π(U25) | = | [1,2] |
π(isList) | = | [1] |
π(U26) | = | [1] |
π(U31) | = | [1,2] |
π(U32) | = | [1,2] |
π(U33) | = | [1] |
π(isQid) | = | 1 |
π(U41) | = | [2,1,3] |
π(U42) | = | [3,1,2] |
π(U43) | = | [1,2,3] |
π(U44) | = | [1,2,3] |
π(U45) | = | [1,2] |
π(U46) | = | 1 |
π(U51) | = | [1,2,3] |
π(U52) | = | [3,1,2] |
π(U53) | = | [1,2,3] |
π(U54) | = | [1,2,3] |
π(U55) | = | [1,2] |
π(U56) | = | 1 |
π(U61) | = | [1,2] |
π(U62) | = | [1,2] |
π(U63) | = | [1] |
π(U71) | = | [2,3,1] |
π(U72) | = | [2,1] |
π(U73) | = | [1,2] |
π(isPal) | = | [1] |
π(U74) | = | 1 |
π(U81) | = | [1,2] |
π(U82) | = | [1,2] |
π(U83) | = | 1 |
π(isNePal) | = | [1] |
π(U91) | = | [1,2] |
π(U92) | = | 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(isPalListKind(V),V)) | (4) |
active(U12(tt,V)) | → | mark(U13(isNeList(V))) | (5) |
active(U21(tt,V1,V2)) | → | mark(U22(isPalListKind(V1),V1,V2)) | (7) |
active(U22(tt,V1,V2)) | → | mark(U23(isPalListKind(V2),V1,V2)) | (8) |
active(U23(tt,V1,V2)) | → | mark(U24(isPalListKind(V2),V1,V2)) | (9) |
active(U24(tt,V1,V2)) | → | mark(U25(isList(V1),V2)) | (10) |
active(U25(tt,V2)) | → | mark(U26(isList(V2))) | (11) |
active(U26(tt)) | → | mark(tt) | (12) |
active(U31(tt,V)) | → | mark(U32(isPalListKind(V),V)) | (13) |
active(U32(tt,V)) | → | mark(U33(isQid(V))) | (14) |
active(U33(tt)) | → | mark(tt) | (15) |
active(U41(tt,V1,V2)) | → | mark(U42(isPalListKind(V1),V1,V2)) | (16) |
active(U42(tt,V1,V2)) | → | mark(U43(isPalListKind(V2),V1,V2)) | (17) |
active(U43(tt,V1,V2)) | → | mark(U44(isPalListKind(V2),V1,V2)) | (18) |
active(U44(tt,V1,V2)) | → | mark(U45(isList(V1),V2)) | (19) |
active(U45(tt,V2)) | → | mark(U46(isNeList(V2))) | (20) |
active(U51(tt,V1,V2)) | → | mark(U52(isPalListKind(V1),V1,V2)) | (22) |
active(U52(tt,V1,V2)) | → | mark(U53(isPalListKind(V2),V1,V2)) | (23) |
active(U53(tt,V1,V2)) | → | mark(U54(isPalListKind(V2),V1,V2)) | (24) |
active(U54(tt,V1,V2)) | → | mark(U55(isNeList(V1),V2)) | (25) |
active(U55(tt,V2)) | → | mark(U56(isList(V2))) | (26) |
active(U61(tt,V)) | → | mark(U62(isPalListKind(V),V)) | (28) |
active(U62(tt,V)) | → | mark(U63(isQid(V))) | (29) |
active(U63(tt)) | → | mark(tt) | (30) |
active(U71(tt,I,P)) | → | mark(U72(isPalListKind(I),P)) | (31) |
active(U72(tt,P)) | → | mark(U73(isPal(P),P)) | (32) |
active(U73(tt,P)) | → | mark(U74(isPalListKind(P))) | (33) |
active(U81(tt,V)) | → | mark(U82(isPalListKind(V),V)) | (35) |
active(U82(tt,V)) | → | mark(U83(isNePal(V))) | (36) |
active(U91(tt,V2)) | → | mark(U92(isPalListKind(V2))) | (38) |
active(isList(V)) | → | mark(U11(isPalListKind(V),V)) | (40) |
active(isList(nil)) | → | mark(tt) | (41) |
active(isList(__(V1,V2))) | → | mark(U21(isPalListKind(V1),V1,V2)) | (42) |
active(isNeList(V)) | → | mark(U31(isPalListKind(V),V)) | (43) |
active(isNeList(__(V1,V2))) | → | mark(U41(isPalListKind(V1),V1,V2)) | (44) |
active(isNeList(__(V1,V2))) | → | mark(U51(isPalListKind(V1),V1,V2)) | (45) |
active(isNePal(V)) | → | mark(U61(isPalListKind(V),V)) | (46) |
active(isNePal(__(I,__(P,I)))) | → | mark(U71(isQid(I),I,P)) | (47) |
active(isPal(V)) | → | mark(U81(isPalListKind(V),V)) | (48) |
active(isPal(nil)) | → | mark(tt) | (49) |
active(isPalListKind(a)) | → | mark(tt) | (50) |
active(isPalListKind(e)) | → | mark(tt) | (51) |
active(isPalListKind(i)) | → | mark(tt) | (52) |
active(isPalListKind(nil)) | → | mark(tt) | (53) |
active(isPalListKind(o)) | → | mark(tt) | (54) |
active(isPalListKind(u)) | → | mark(tt) | (55) |
active(isPalListKind(__(V1,V2))) | → | mark(U91(isPalListKind(V1),V2)) | (56) |
active(isQid(i)) | → | mark(tt) | (59) |
[active(x1)] | = | 1 · x1 |
[U13(x1)] | = | 1 · x1 |
[tt] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[U46(x1)] | = | 1 · x1 |
[U56(x1)] | = | 2 · x1 |
[U74(x1)] | = | 1 · x1 |
[U83(x1)] | = | 2 · x1 |
[U92(x1)] | = | 2 · x1 |
[isQid(x1)] | = | 2 · x1 |
[a] | = | 0 |
[e] | = | 0 |
[o] | = | 1 |
[u] | = | 0 |
[__(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U21(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U22(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U23(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U24(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U25(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U26(x1)] | = | 2 · x1 |
[U31(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U32(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U33(x1)] | = | 2 · x1 |
[U41(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U42(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U44(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U51(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 |
[U52(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U53(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 |
[U54(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 |
[U55(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U61(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U63(x1)] | = | 1 · x1 |
[U71(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U72(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U73(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U81(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U91(x1, x2)] | = | 1 · x1 + 1 · x2 |
[proper(x1)] | = | 1 · x1 |
[nil] | = | 0 |
[ok(x1)] | = | 1 · x1 |
[isPalListKind(x1)] | = | 1 · x1 |
[isNeList(x1)] | = | 2 · x1 |
[isList(x1)] | = | 1 · x1 |
[isPal(x1)] | = | 1 · x1 |
[isNePal(x1)] | = | 2 · x1 |
[i] | = | 0 |
[top(x1)] | = | 2 · x1 |
active(isQid(o)) | → | mark(tt) | (60) |
[active(x1)] | = | 1 · x1 |
[U13(x1)] | = | 2 · x1 |
[tt] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[U46(x1)] | = | 2 · x1 |
[U56(x1)] | = | 2 · x1 |
[U74(x1)] | = | 1 · x1 |
[U83(x1)] | = | 2 · x1 |
[U92(x1)] | = | 2 + 1 · x1 |
[isQid(x1)] | = | 1 · x1 |
[a] | = | 1 |
[e] | = | 0 |
[u] | = | 2 |
[__(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U21(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U22(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 |
[U23(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U24(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U25(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U26(x1)] | = | 1 · x1 |
[U31(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U32(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U33(x1)] | = | 2 · x1 |
[U41(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U42(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U44(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U51(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U52(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 |
[U53(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U54(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U55(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U61(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U63(x1)] | = | 2 · x1 |
[U71(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U72(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U73(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U81(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U82(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U91(x1, x2)] | = | 1 · x1 + 2 · x2 |
[proper(x1)] | = | 1 · x1 |
[nil] | = | 0 |
[ok(x1)] | = | 1 · x1 |
[isPalListKind(x1)] | = | 2 · x1 |
[isNeList(x1)] | = | 1 · x1 |
[isList(x1)] | = | 1 · x1 |
[isPal(x1)] | = | 2 · x1 |
[isNePal(x1)] | = | 1 · x1 |
[i] | = | 0 |
[o] | = | 0 |
[top(x1)] | = | 1 · x1 |
active(U92(tt)) | → | mark(tt) | (39) |
active(isQid(a)) | → | mark(tt) | (57) |
active(isQid(u)) | → | mark(tt) | (61) |
[active(x1)] | = | 1 · x1 |
[U13(x1)] | = | 1 · x1 |
[tt] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[U46(x1)] | = | 1 · x1 |
[U56(x1)] | = | 1 · x1 |
[U74(x1)] | = | 1 · x1 |
[U83(x1)] | = | 2 · x1 |
[isQid(x1)] | = | 1 · x1 |
[e] | = | 1 |
[__(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U21(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U22(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 |
[U23(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U24(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U25(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U26(x1)] | = | 2 · x1 |
[U31(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U32(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U33(x1)] | = | 1 · x1 |
[U41(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U42(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U44(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U51(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U52(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U53(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U54(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U55(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U61(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U63(x1)] | = | 1 · x1 |
[U71(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U72(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U73(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U81(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U82(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U91(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U92(x1)] | = | 2 · x1 |
[proper(x1)] | = | 1 · x1 |
[nil] | = | 0 |
[ok(x1)] | = | 1 · x1 |
[isPalListKind(x1)] | = | 2 · x1 |
[isNeList(x1)] | = | 2 · x1 |
[isList(x1)] | = | 2 · x1 |
[isPal(x1)] | = | 1 · x1 |
[isNePal(x1)] | = | 2 · x1 |
[a] | = | 0 |
[i] | = | 0 |
[o] | = | 0 |
[u] | = | 0 |
[top(x1)] | = | 2 · x1 |
active(isQid(e)) | → | mark(tt) | (58) |
[active(x1)] | = | 1 · x1 |
[U13(x1)] | = | 1 + 2 · x1 |
[tt] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[U46(x1)] | = | 2 · x1 |
[U56(x1)] | = | 2 · x1 |
[U74(x1)] | = | 1 · x1 |
[U83(x1)] | = | 2 · x1 |
[__(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U21(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U22(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 |
[U23(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U24(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U25(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U26(x1)] | = | 2 · x1 |
[U31(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U32(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U33(x1)] | = | 2 · x1 |
[U41(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U42(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U44(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U51(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U52(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U53(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U54(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U55(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U61(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U63(x1)] | = | 2 · x1 |
[U71(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U72(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U73(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U81(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U91(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U92(x1)] | = | 2 · x1 |
[proper(x1)] | = | 1 · x1 |
[nil] | = | 0 |
[ok(x1)] | = | 1 · x1 |
[isPalListKind(x1)] | = | 1 · x1 |
[isNeList(x1)] | = | 1 · x1 |
[isList(x1)] | = | 2 · x1 |
[isQid(x1)] | = | 2 · x1 |
[isPal(x1)] | = | 2 · x1 |
[isNePal(x1)] | = | 2 · x1 |
[a] | = | 0 |
[e] | = | 0 |
[i] | = | 0 |
[o] | = | 0 |
[u] | = | 0 |
[top(x1)] | = | 2 · x1 |
active(U13(tt)) | → | mark(tt) | (6) |
[active(x1)] | = | 1 · x1 |
[U46(x1)] | = | 1 + 2 · x1 |
[tt] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[U56(x1)] | = | 2 · x1 |
[U74(x1)] | = | 1 + 2 · x1 |
[U83(x1)] | = | 1 + 1 · x1 |
[__(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U13(x1)] | = | 2 · x1 |
[U21(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U22(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U23(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 |
[U24(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 1 · x3 |
[U25(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U26(x1)] | = | 1 · x1 |
[U31(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U32(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U33(x1)] | = | 1 · x1 |
[U41(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U42(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U43(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U44(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U51(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U52(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U53(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U54(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U55(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U61(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U63(x1)] | = | 1 · x1 |
[U71(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U72(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U73(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U81(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U91(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U92(x1)] | = | 2 · x1 |
[proper(x1)] | = | 1 · x1 |
[nil] | = | 0 |
[ok(x1)] | = | 1 · x1 |
[isPalListKind(x1)] | = | 1 · x1 |
[isNeList(x1)] | = | 1 · x1 |
[isList(x1)] | = | 2 · x1 |
[isQid(x1)] | = | 1 · x1 |
[isPal(x1)] | = | 2 · x1 |
[isNePal(x1)] | = | 2 · x1 |
[a] | = | 0 |
[e] | = | 0 |
[i] | = | 0 |
[o] | = | 0 |
[u] | = | 0 |
[top(x1)] | = | 2 · x1 |
active(U46(tt)) | → | mark(tt) | (21) |
active(U74(tt)) | → | mark(tt) | (34) |
active(U83(tt)) | → | mark(tt) | (37) |
[active(x1)] | = | 1 · x1 |
[U56(x1)] | = | 2 · x1 |
[tt] | = | 2 |
[mark(x1)] | = | 1 · x1 |
[__(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U13(x1)] | = | 2 · x1 |
[U21(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U22(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U23(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U24(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U25(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U26(x1)] | = | 2 · x1 |
[U31(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U32(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U33(x1)] | = | 2 · x1 |
[U41(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U42(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U43(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U44(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U45(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U46(x1)] | = | 1 · x1 |
[U51(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U52(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U53(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U54(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U55(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U61(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U63(x1)] | = | 1 · x1 |
[U71(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U72(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U73(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U74(x1)] | = | 2 · x1 |
[U81(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U82(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U83(x1)] | = | 2 · x1 |
[U91(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U92(x1)] | = | 2 · x1 |
[proper(x1)] | = | 1 · x1 |
[nil] | = | 0 |
[ok(x1)] | = | 1 · x1 |
[isPalListKind(x1)] | = | 1 · x1 |
[isNeList(x1)] | = | 1 · x1 |
[isList(x1)] | = | 1 · x1 |
[isQid(x1)] | = | 2 · x1 |
[isPal(x1)] | = | 2 · x1 |
[isNePal(x1)] | = | 2 · x1 |
[a] | = | 0 |
[e] | = | 0 |
[i] | = | 0 |
[o] | = | 0 |
[u] | = | 0 |
[top(x1)] | = | 2 · x1 |
active(U56(tt)) | → | mark(tt) | (27) |
[active(x1)] | = | 1 · x1 |
[__(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U13(x1)] | = | 2 · x1 |
[U21(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U22(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U23(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U24(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U25(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U26(x1)] | = | 2 · x1 |
[U31(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U32(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U33(x1)] | = | 2 · x1 |
[U41(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U42(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U44(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U46(x1)] | = | 2 · x1 |
[U51(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U52(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U53(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U54(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 1 · x3 |
[U55(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U56(x1)] | = | 2 · x1 |
[U61(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U62(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U63(x1)] | = | 2 · x1 |
[U71(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U72(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U73(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U74(x1)] | = | 2 · x1 |
[U81(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U83(x1)] | = | 2 · x1 |
[U91(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U92(x1)] | = | 2 · x1 |
[mark(x1)] | = | 2 + 1 · x1 |
[proper(x1)] | = | 1 · x1 |
[nil] | = | 0 |
[ok(x1)] | = | 2 · x1 |
[tt] | = | 0 |
[isPalListKind(x1)] | = | 1 · x1 |
[isNeList(x1)] | = | 1 · x1 |
[isList(x1)] | = | 1 · x1 |
[isQid(x1)] | = | 2 · x1 |
[isPal(x1)] | = | 2 · x1 |
[isNePal(x1)] | = | 2 · x1 |
[a] | = | 0 |
[e] | = | 0 |
[i] | = | 0 |
[o] | = | 0 |
[u] | = | 0 |
[top(x1)] | = | 1 · x1 |
__(mark(X1),X2) | → | mark(__(X1,X2)) | (100) |
__(X1,mark(X2)) | → | mark(__(X1,X2)) | (101) |
U11(mark(X1),X2) | → | mark(U11(X1,X2)) | (102) |
U12(mark(X1),X2) | → | mark(U12(X1,X2)) | (103) |
U13(mark(X)) | → | mark(U13(X)) | (104) |
U21(mark(X1),X2,X3) | → | mark(U21(X1,X2,X3)) | (105) |
U22(mark(X1),X2,X3) | → | mark(U22(X1,X2,X3)) | (106) |
U23(mark(X1),X2,X3) | → | mark(U23(X1,X2,X3)) | (107) |
U24(mark(X1),X2,X3) | → | mark(U24(X1,X2,X3)) | (108) |
U25(mark(X1),X2) | → | mark(U25(X1,X2)) | (109) |
U26(mark(X)) | → | mark(U26(X)) | (110) |
U31(mark(X1),X2) | → | mark(U31(X1,X2)) | (111) |
U32(mark(X1),X2) | → | mark(U32(X1,X2)) | (112) |
U33(mark(X)) | → | mark(U33(X)) | (113) |
U41(mark(X1),X2,X3) | → | mark(U41(X1,X2,X3)) | (114) |
U42(mark(X1),X2,X3) | → | mark(U42(X1,X2,X3)) | (115) |
U43(mark(X1),X2,X3) | → | mark(U43(X1,X2,X3)) | (116) |
U44(mark(X1),X2,X3) | → | mark(U44(X1,X2,X3)) | (117) |
U45(mark(X1),X2) | → | mark(U45(X1,X2)) | (118) |
U46(mark(X)) | → | mark(U46(X)) | (119) |
U51(mark(X1),X2,X3) | → | mark(U51(X1,X2,X3)) | (120) |
U52(mark(X1),X2,X3) | → | mark(U52(X1,X2,X3)) | (121) |
U53(mark(X1),X2,X3) | → | mark(U53(X1,X2,X3)) | (122) |
U54(mark(X1),X2,X3) | → | mark(U54(X1,X2,X3)) | (123) |
U55(mark(X1),X2) | → | mark(U55(X1,X2)) | (124) |
U56(mark(X)) | → | mark(U56(X)) | (125) |
U61(mark(X1),X2) | → | mark(U61(X1,X2)) | (126) |
U62(mark(X1),X2) | → | mark(U62(X1,X2)) | (127) |
U63(mark(X)) | → | mark(U63(X)) | (128) |
U71(mark(X1),X2,X3) | → | mark(U71(X1,X2,X3)) | (129) |
U72(mark(X1),X2) | → | mark(U72(X1,X2)) | (130) |
U73(mark(X1),X2) | → | mark(U73(X1,X2)) | (131) |
U74(mark(X)) | → | mark(U74(X)) | (132) |
U81(mark(X1),X2) | → | mark(U81(X1,X2)) | (133) |
U82(mark(X1),X2) | → | mark(U82(X1,X2)) | (134) |
U83(mark(X)) | → | mark(U83(X)) | (135) |
U91(mark(X1),X2) | → | mark(U91(X1,X2)) | (136) |
U92(mark(X)) | → | mark(U92(X)) | (137) |
top(mark(X)) | → | top(proper(X)) | (231) |
[active(x1)] | = | 1 · x1 |
[__(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U11(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U12(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U13(x1)] | = | 1 · x1 |
[U21(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U22(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U23(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U24(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U25(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U26(x1)] | = | 1 + 1 · x1 |
[U31(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U32(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U33(x1)] | = | 1 · x1 |
[U41(x1, x2, x3)] | = | 1 · x1 + 2 · x2 + 2 · x3 |
[U42(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U43(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 2 · x3 |
[U44(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U46(x1)] | = | 2 + 1 · x1 |
[U51(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U52(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U53(x1, x2, x3)] | = | 1 · x1 + 1 · x2 + 1 · x3 |
[U54(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 1 · x3 |
[U55(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U56(x1)] | = | 2 · x1 |
[U61(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U63(x1)] | = | 1 · x1 |
[U71(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U72(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U73(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U74(x1)] | = | 1 + 1 · x1 |
[U81(x1, x2)] | = | 1 · x1 + 1 · x2 |
[U82(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U83(x1)] | = | 2 · x1 |
[U91(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U92(x1)] | = | 2 · x1 |
[proper(x1)] | = | 2 · x1 |
[nil] | = | 2 |
[ok(x1)] | = | 1 · x1 |
[tt] | = | 2 |
[isPalListKind(x1)] | = | 1 + 1 · x1 |
[isNeList(x1)] | = | 1 · x1 |
[isList(x1)] | = | 1 + 1 · x1 |
[isQid(x1)] | = | 1 + 2 · x1 |
[isPal(x1)] | = | 1 · x1 |
[isNePal(x1)] | = | 1 · x1 |
[a] | = | 2 |
[e] | = | 2 |
[i] | = | 2 |
[o] | = | 2 |
[u] | = | 2 |
[top(x1)] | = | 2 · x1 |
proper(nil) | → | ok(nil) | (139) |
proper(tt) | → | ok(tt) | (141) |
proper(isPalListKind(X)) | → | isPalListKind(proper(X)) | (143) |
proper(isList(X)) | → | isList(proper(X)) | (151) |
proper(U26(X)) | → | U26(proper(X)) | (152) |
proper(isQid(X)) | → | isQid(proper(X)) | (156) |
proper(U46(X)) | → | U46(proper(X)) | (162) |
proper(U73(X1,X2)) | → | U73(proper(X1),proper(X2)) | (174) |
proper(U74(X)) | → | U74(proper(X)) | (176) |
proper(a) | → | ok(a) | (183) |
proper(e) | → | ok(e) | (184) |
proper(i) | → | ok(i) | (185) |
proper(o) | → | ok(o) | (186) |
proper(u) | → | ok(u) | (187) |
[active(x1)] | = | 1 + 2 · x1 |
[__(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U13(x1)] | = | 1 + 2 · x1 |
[U21(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U22(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U23(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U24(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U25(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U26(x1)] | = | 1 + 2 · x1 |
[U31(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U32(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U33(x1)] | = | 1 + 2 · x1 |
[U41(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U42(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U44(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U46(x1)] | = | 1 + 2 · x1 |
[U51(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U52(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U53(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U54(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U55(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U56(x1)] | = | 1 + 2 · x1 |
[U61(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U63(x1)] | = | 1 + 2 · x1 |
[U71(x1, x2, x3)] | = | 1 + 1 · x1 + 2 · x2 + 2 · x3 |
[U72(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U73(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U74(x1)] | = | 1 + 2 · x1 |
[U81(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U83(x1)] | = | 1 + 2 · x1 |
[U91(x1, x2)] | = | 1 + 2 · x1 + 1 · x2 |
[U92(x1)] | = | 1 + 2 · x1 |
[proper(x1)] | = | 2 · x1 |
[isNeList(x1)] | = | 1 + 2 · x1 |
[isPal(x1)] | = | 1 + 2 · x1 |
[isNePal(x1)] | = | 2 · x1 |
[ok(x1)] | = | 2 + 2 · x1 |
[isPalListKind(x1)] | = | 1 + 2 · x1 |
[isList(x1)] | = | 1 + 2 · x1 |
[isQid(x1)] | = | 1 + 2 · x1 |
[top(x1)] | = | 1 · x1 |
active(__(X1,X2)) | → | __(active(X1),X2) | (62) |
active(U21(X1,X2,X3)) | → | U21(active(X1),X2,X3) | (67) |
active(U22(X1,X2,X3)) | → | U22(active(X1),X2,X3) | (68) |
active(U23(X1,X2,X3)) | → | U23(active(X1),X2,X3) | (69) |
active(U24(X1,X2,X3)) | → | U24(active(X1),X2,X3) | (70) |
active(U41(X1,X2,X3)) | → | U41(active(X1),X2,X3) | (76) |
active(U42(X1,X2,X3)) | → | U42(active(X1),X2,X3) | (77) |
active(U43(X1,X2,X3)) | → | U43(active(X1),X2,X3) | (78) |
active(U44(X1,X2,X3)) | → | U44(active(X1),X2,X3) | (79) |
active(U51(X1,X2,X3)) | → | U51(active(X1),X2,X3) | (82) |
active(U52(X1,X2,X3)) | → | U52(active(X1),X2,X3) | (83) |
active(U53(X1,X2,X3)) | → | U53(active(X1),X2,X3) | (84) |
active(U54(X1,X2,X3)) | → | U54(active(X1),X2,X3) | (85) |
active(U71(X1,X2,X3)) | → | U71(active(X1),X2,X3) | (91) |
proper(__(X1,X2)) | → | __(proper(X1),proper(X2)) | (138) |
proper(U11(X1,X2)) | → | U11(proper(X1),proper(X2)) | (140) |
proper(U12(X1,X2)) | → | U12(proper(X1),proper(X2)) | (142) |
proper(U13(X)) | → | U13(proper(X)) | (144) |
proper(isNeList(X)) | → | isNeList(proper(X)) | (145) |
proper(U21(X1,X2,X3)) | → | U21(proper(X1),proper(X2),proper(X3)) | (146) |
proper(U22(X1,X2,X3)) | → | U22(proper(X1),proper(X2),proper(X3)) | (147) |
proper(U23(X1,X2,X3)) | → | U23(proper(X1),proper(X2),proper(X3)) | (148) |
proper(U24(X1,X2,X3)) | → | U24(proper(X1),proper(X2),proper(X3)) | (149) |
proper(U25(X1,X2)) | → | U25(proper(X1),proper(X2)) | (150) |
proper(U31(X1,X2)) | → | U31(proper(X1),proper(X2)) | (153) |
proper(U32(X1,X2)) | → | U32(proper(X1),proper(X2)) | (154) |
proper(U33(X)) | → | U33(proper(X)) | (155) |
proper(U41(X1,X2,X3)) | → | U41(proper(X1),proper(X2),proper(X3)) | (157) |
proper(U42(X1,X2,X3)) | → | U42(proper(X1),proper(X2),proper(X3)) | (158) |
proper(U43(X1,X2,X3)) | → | U43(proper(X1),proper(X2),proper(X3)) | (159) |
proper(U44(X1,X2,X3)) | → | U44(proper(X1),proper(X2),proper(X3)) | (160) |
proper(U45(X1,X2)) | → | U45(proper(X1),proper(X2)) | (161) |
proper(U51(X1,X2,X3)) | → | U51(proper(X1),proper(X2),proper(X3)) | (163) |
proper(U52(X1,X2,X3)) | → | U52(proper(X1),proper(X2),proper(X3)) | (164) |
proper(U53(X1,X2,X3)) | → | U53(proper(X1),proper(X2),proper(X3)) | (165) |
proper(U54(X1,X2,X3)) | → | U54(proper(X1),proper(X2),proper(X3)) | (166) |
proper(U55(X1,X2)) | → | U55(proper(X1),proper(X2)) | (167) |
proper(U56(X)) | → | U56(proper(X)) | (168) |
proper(U61(X1,X2)) | → | U61(proper(X1),proper(X2)) | (169) |
proper(U62(X1,X2)) | → | U62(proper(X1),proper(X2)) | (170) |
proper(U63(X)) | → | U63(proper(X)) | (171) |
proper(U71(X1,X2,X3)) | → | U71(proper(X1),proper(X2),proper(X3)) | (172) |
proper(U72(X1,X2)) | → | U72(proper(X1),proper(X2)) | (173) |
proper(isPal(X)) | → | isPal(proper(X)) | (175) |
proper(U81(X1,X2)) | → | U81(proper(X1),proper(X2)) | (177) |
proper(U82(X1,X2)) | → | U82(proper(X1),proper(X2)) | (178) |
proper(U83(X)) | → | U83(proper(X)) | (179) |
proper(U91(X1,X2)) | → | U91(proper(X1),proper(X2)) | (181) |
proper(U92(X)) | → | U92(proper(X)) | (182) |
__(ok(X1),ok(X2)) | → | ok(__(X1,X2)) | (188) |
U11(ok(X1),ok(X2)) | → | ok(U11(X1,X2)) | (189) |
U12(ok(X1),ok(X2)) | → | ok(U12(X1,X2)) | (190) |
isPalListKind(ok(X)) | → | ok(isPalListKind(X)) | (191) |
U13(ok(X)) | → | ok(U13(X)) | (192) |
isNeList(ok(X)) | → | ok(isNeList(X)) | (193) |
U21(ok(X1),ok(X2),ok(X3)) | → | ok(U21(X1,X2,X3)) | (194) |
U22(ok(X1),ok(X2),ok(X3)) | → | ok(U22(X1,X2,X3)) | (195) |
U23(ok(X1),ok(X2),ok(X3)) | → | ok(U23(X1,X2,X3)) | (196) |
U24(ok(X1),ok(X2),ok(X3)) | → | ok(U24(X1,X2,X3)) | (197) |
U25(ok(X1),ok(X2)) | → | ok(U25(X1,X2)) | (198) |
isList(ok(X)) | → | ok(isList(X)) | (199) |
U26(ok(X)) | → | ok(U26(X)) | (200) |
U31(ok(X1),ok(X2)) | → | ok(U31(X1,X2)) | (201) |
U32(ok(X1),ok(X2)) | → | ok(U32(X1,X2)) | (202) |
U33(ok(X)) | → | ok(U33(X)) | (203) |
isQid(ok(X)) | → | ok(isQid(X)) | (204) |
U41(ok(X1),ok(X2),ok(X3)) | → | ok(U41(X1,X2,X3)) | (205) |
U42(ok(X1),ok(X2),ok(X3)) | → | ok(U42(X1,X2,X3)) | (206) |
U43(ok(X1),ok(X2),ok(X3)) | → | ok(U43(X1,X2,X3)) | (207) |
U44(ok(X1),ok(X2),ok(X3)) | → | ok(U44(X1,X2,X3)) | (208) |
U45(ok(X1),ok(X2)) | → | ok(U45(X1,X2)) | (209) |
U46(ok(X)) | → | ok(U46(X)) | (210) |
U51(ok(X1),ok(X2),ok(X3)) | → | ok(U51(X1,X2,X3)) | (211) |
U52(ok(X1),ok(X2),ok(X3)) | → | ok(U52(X1,X2,X3)) | (212) |
U53(ok(X1),ok(X2),ok(X3)) | → | ok(U53(X1,X2,X3)) | (213) |
U54(ok(X1),ok(X2),ok(X3)) | → | ok(U54(X1,X2,X3)) | (214) |
U55(ok(X1),ok(X2)) | → | ok(U55(X1,X2)) | (215) |
U56(ok(X)) | → | ok(U56(X)) | (216) |
U61(ok(X1),ok(X2)) | → | ok(U61(X1,X2)) | (217) |
U62(ok(X1),ok(X2)) | → | ok(U62(X1,X2)) | (218) |
U63(ok(X)) | → | ok(U63(X)) | (219) |
U71(ok(X1),ok(X2),ok(X3)) | → | ok(U71(X1,X2,X3)) | (220) |
U72(ok(X1),ok(X2)) | → | ok(U72(X1,X2)) | (221) |
U73(ok(X1),ok(X2)) | → | ok(U73(X1,X2)) | (222) |
isPal(ok(X)) | → | ok(isPal(X)) | (223) |
U74(ok(X)) | → | ok(U74(X)) | (224) |
U81(ok(X1),ok(X2)) | → | ok(U81(X1,X2)) | (225) |
U82(ok(X1),ok(X2)) | → | ok(U82(X1,X2)) | (226) |
U83(ok(X)) | → | ok(U83(X)) | (227) |
isNePal(ok(X)) | → | ok(isNePal(X)) | (228) |
U91(ok(X1),ok(X2)) | → | ok(U91(X1,X2)) | (229) |
U92(ok(X)) | → | ok(U92(X)) | (230) |
top(ok(X)) | → | top(active(X)) | (232) |
[active(x1)] | = | 2 · x1 |
[__(x1, x2)] | = | 2 + 2 · x1 + 1 · x2 |
[U11(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[U13(x1)] | = | 1 · x1 |
[U25(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U26(x1)] | = | 1 + 2 · x1 |
[U31(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[U32(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U33(x1)] | = | 1 + 1 · x1 |
[U45(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U46(x1)] | = | 1 + 1 · x1 |
[U55(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U56(x1)] | = | 1 + 1 · x1 |
[U61(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 1 + 2 · x1 + 2 · x2 |
[U63(x1)] | = | 1 + 1 · x1 |
[U72(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U73(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U74(x1)] | = | 1 + 1 · x1 |
[U81(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U83(x1)] | = | 1 + 1 · x1 |
[U91(x1, x2)] | = | 1 + 1 · x1 + 2 · x2 |
[U92(x1)] | = | 1 + 1 · x1 |
[proper(x1)] | = | 2 + 2 · x1 |
[isNePal(x1)] | = | 1 + 1 · x1 |
active(__(X1,X2)) | → | __(X1,active(X2)) | (63) |
active(U11(X1,X2)) | → | U11(active(X1),X2) | (64) |
active(U12(X1,X2)) | → | U12(active(X1),X2) | (65) |
active(U25(X1,X2)) | → | U25(active(X1),X2) | (71) |
active(U26(X)) | → | U26(active(X)) | (72) |
active(U31(X1,X2)) | → | U31(active(X1),X2) | (73) |
active(U32(X1,X2)) | → | U32(active(X1),X2) | (74) |
active(U33(X)) | → | U33(active(X)) | (75) |
active(U45(X1,X2)) | → | U45(active(X1),X2) | (80) |
active(U46(X)) | → | U46(active(X)) | (81) |
active(U55(X1,X2)) | → | U55(active(X1),X2) | (86) |
active(U56(X)) | → | U56(active(X)) | (87) |
active(U61(X1,X2)) | → | U61(active(X1),X2) | (88) |
active(U62(X1,X2)) | → | U62(active(X1),X2) | (89) |
active(U63(X)) | → | U63(active(X)) | (90) |
active(U72(X1,X2)) | → | U72(active(X1),X2) | (92) |
active(U73(X1,X2)) | → | U73(active(X1),X2) | (93) |
active(U74(X)) | → | U74(active(X)) | (94) |
active(U81(X1,X2)) | → | U81(active(X1),X2) | (95) |
active(U82(X1,X2)) | → | U82(active(X1),X2) | (96) |
active(U83(X)) | → | U83(active(X)) | (97) |
active(U91(X1,X2)) | → | U91(active(X1),X2) | (98) |
active(U92(X)) | → | U92(active(X)) | (99) |
proper(isNePal(X)) | → | isNePal(proper(X)) | (180) |
prec(active) | = | 1 | weight(active) | = | 2 | ||||
prec(U13) | = | 0 | weight(U13) | = | 1 |
active(U13(X)) | → | U13(active(X)) | (66) |
There are no rules in the TRS. Hence, it is terminating.