The rewrite relation of the following TRS is considered.
There are 279 ruless (increase limit for explicit display).
prec(__) | = | 26 | stat(__) | = | lex | |
prec(nil) | = | 27 | stat(nil) | = | mul | |
prec(U11) | = | 3 | stat(U11) | = | mul | |
prec(tt) | = | 9 | stat(tt) | = | mul | |
prec(U12) | = | 2 | stat(U12) | = | mul | |
prec(isNeList) | = | 2 | stat(isNeList) | = | mul | |
prec(U21) | = | 12 | stat(U21) | = | lex | |
prec(U22) | = | 11 | stat(U22) | = | mul | |
prec(U23) | = | 10 | stat(U23) | = | mul | |
prec(U24) | = | 5 | stat(U24) | = | lex | |
prec(U25) | = | 4 | stat(U25) | = | lex | |
prec(isList) | = | 4 | stat(isList) | = | lex | |
prec(U31) | = | 1 | stat(U31) | = | mul | |
prec(U32) | = | 0 | stat(U32) | = | mul | |
prec(isQid) | = | 0 | stat(isQid) | = | mul | |
prec(U41) | = | 15 | stat(U41) | = | lex | |
prec(U42) | = | 14 | stat(U42) | = | lex | |
prec(U43) | = | 13 | stat(U43) | = | mul | |
prec(U44) | = | 4 | stat(U44) | = | lex | |
prec(U45) | = | 2 | stat(U45) | = | mul | |
prec(U51) | = | 19 | stat(U51) | = | mul | |
prec(U52) | = | 18 | stat(U52) | = | mul | |
prec(U53) | = | 17 | stat(U53) | = | mul | |
prec(U54) | = | 16 | stat(U54) | = | lex | |
prec(U55) | = | 7 | stat(U55) | = | mul | |
prec(U56) | = | 6 | stat(U56) | = | mul | |
prec(U61) | = | 20 | stat(U61) | = | mul | |
prec(U62) | = | 0 | stat(U62) | = | mul | |
prec(U71) | = | 24 | stat(U71) | = | mul | |
prec(U72) | = | 24 | stat(U72) | = | mul | |
prec(U73) | = | 21 | stat(U73) | = | mul | |
prec(isPal) | = | 24 | stat(isPal) | = | mul | |
prec(U74) | = | 8 | stat(U74) | = | mul | |
prec(U81) | = | 23 | stat(U81) | = | mul | |
prec(U82) | = | 22 | stat(U82) | = | mul | |
prec(isNePal) | = | 22 | stat(isNePal) | = | mul | |
prec(U91) | = | 25 | stat(U91) | = | mul | |
prec(a) | = | 9 | stat(a) | = | mul | |
prec(e) | = | 28 | stat(e) | = | mul | |
prec(i) | = | 9 | stat(i) | = | mul | |
prec(o) | = | 29 | stat(o) | = | mul | |
prec(u) | = | 9 | stat(u) | = | mul |
π(active) | = | 1 |
π(__) | = | [1,2] |
π(mark) | = | 1 |
π(nil) | = | [] |
π(U11) | = | [1,2] |
π(tt) | = | [] |
π(U12) | = | [1,2] |
π(isPalListKind) | = | 1 |
π(U13) | = | 1 |
π(isNeList) | = | [1] |
π(U21) | = | [1,3,2] |
π(U22) | = | [1,2,3] |
π(U23) | = | [1,2,3] |
π(U24) | = | [3,2,1] |
π(U25) | = | [2,1] |
π(isList) | = | [1] |
π(U26) | = | 1 |
π(U31) | = | [1,2] |
π(U32) | = | [1,2] |
π(U33) | = | 1 |
π(isQid) | = | [1] |
π(U41) | = | [1,2,3] |
π(U42) | = | [3,2,1] |
π(U43) | = | [1,2,3] |
π(U44) | = | [2,3,1] |
π(U45) | = | [1,2] |
π(U46) | = | 1 |
π(U51) | = | [1,2,3] |
π(U52) | = | [1,2,3] |
π(U53) | = | [1,2,3] |
π(U54) | = | [2,1,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) | = | [] |
π(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(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(U31(tt,V)) | → | mark(U32(isPalListKind(V),V)) | (13) |
active(U32(tt,V)) | → | mark(U33(isQid(V))) | (14) |
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(U56(tt)) | → | mark(tt) | (27) |
active(U61(tt,V)) | → | mark(U62(isPalListKind(V),V)) | (28) |
active(U62(tt,V)) | → | mark(U63(isQid(V))) | (29) |
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(U74(tt)) | → | mark(tt) | (34) |
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(e)) | → | mark(tt) | (51) |
active(isPalListKind(nil)) | → | mark(tt) | (53) |
active(isPalListKind(o)) | → | mark(tt) | (54) |
active(isPalListKind(__(V1,V2))) | → | mark(U91(isPalListKind(V1),V2)) | (56) |
active(isQid(a)) | → | mark(tt) | (57) |
active(isQid(e)) | → | mark(tt) | (58) |
active(isQid(i)) | → | mark(tt) | (59) |
active(isQid(o)) | → | mark(tt) | (60) |
active(isQid(u)) | → | mark(tt) | (61) |
prec(U13) | = | 28 | stat(U13) | = | mul | |
prec(tt) | = | 28 | stat(tt) | = | mul | |
prec(mark) | = | 28 | stat(mark) | = | mul | |
prec(U26) | = | 28 | stat(U26) | = | mul | |
prec(U33) | = | 28 | stat(U33) | = | mul | |
prec(U46) | = | 28 | stat(U46) | = | mul | |
prec(U63) | = | 28 | stat(U63) | = | mul | |
prec(U83) | = | 28 | stat(U83) | = | mul | |
prec(U92) | = | 28 | stat(U92) | = | mul | |
prec(isPalListKind) | = | 28 | stat(isPalListKind) | = | mul | |
prec(a) | = | 29 | stat(a) | = | mul | |
prec(i) | = | 30 | stat(i) | = | mul | |
prec(u) | = | 28 | stat(u) | = | mul | |
prec(__) | = | 0 | stat(__) | = | mul | |
prec(nil) | = | 1 | stat(nil) | = | mul | |
prec(U11) | = | 2 | stat(U11) | = | mul | |
prec(U12) | = | 3 | stat(U12) | = | mul | |
prec(isNeList) | = | 4 | stat(isNeList) | = | mul | |
prec(U21) | = | 5 | stat(U21) | = | lex | |
prec(U22) | = | 6 | stat(U22) | = | mul | |
prec(U23) | = | 7 | stat(U23) | = | lex | |
prec(U24) | = | 8 | stat(U24) | = | lex | |
prec(U25) | = | 9 | stat(U25) | = | mul | |
prec(isList) | = | 28 | stat(isList) | = | mul | |
prec(U31) | = | 10 | stat(U31) | = | mul | |
prec(U32) | = | 11 | stat(U32) | = | mul | |
prec(isQid) | = | 28 | stat(isQid) | = | mul | |
prec(U41) | = | 12 | stat(U41) | = | lex | |
prec(U42) | = | 13 | stat(U42) | = | lex | |
prec(U43) | = | 14 | stat(U43) | = | lex | |
prec(U44) | = | 15 | stat(U44) | = | lex | |
prec(U45) | = | 28 | stat(U45) | = | mul | |
prec(U51) | = | 16 | stat(U51) | = | lex | |
prec(U52) | = | 17 | stat(U52) | = | lex | |
prec(U53) | = | 18 | stat(U53) | = | lex | |
prec(U54) | = | 19 | stat(U54) | = | lex | |
prec(U55) | = | 20 | stat(U55) | = | mul | |
prec(U61) | = | 28 | stat(U61) | = | mul | |
prec(U62) | = | 28 | stat(U62) | = | mul | |
prec(U71) | = | 21 | stat(U71) | = | lex | |
prec(U72) | = | 22 | stat(U72) | = | mul | |
prec(U73) | = | 28 | stat(U73) | = | mul | |
prec(isPal) | = | 28 | stat(isPal) | = | mul | |
prec(U74) | = | 28 | stat(U74) | = | mul | |
prec(U81) | = | 23 | stat(U81) | = | mul | |
prec(U82) | = | 24 | stat(U82) | = | mul | |
prec(isNePal) | = | 25 | stat(isNePal) | = | mul | |
prec(U91) | = | 28 | stat(U91) | = | mul | |
prec(e) | = | 26 | stat(e) | = | mul | |
prec(o) | = | 27 | stat(o) | = | mul |
π(active) | = | 1 |
π(U13) | = | [1] |
π(tt) | = | [] |
π(mark) | = | [1] |
π(U26) | = | [1] |
π(U33) | = | [1] |
π(U46) | = | [1] |
π(U63) | = | [1] |
π(U83) | = | [1] |
π(U92) | = | [1] |
π(isPalListKind) | = | [1] |
π(a) | = | [] |
π(i) | = | [] |
π(u) | = | [] |
π(__) | = | [1,2] |
π(nil) | = | [] |
π(U11) | = | [1,2] |
π(U12) | = | [1,2] |
π(isNeList) | = | [1] |
π(U21) | = | [3,1,2] |
π(U22) | = | [1,2,3] |
π(U23) | = | [2,3,1] |
π(U24) | = | [3,2,1] |
π(U25) | = | [1,2] |
π(isList) | = | [1] |
π(U31) | = | [1,2] |
π(U32) | = | [1,2] |
π(isQid) | = | [1] |
π(U41) | = | [3,1,2] |
π(U42) | = | [1,3,2] |
π(U43) | = | [2,3,1] |
π(U44) | = | [3,1,2] |
π(U45) | = | [1,2] |
π(U51) | = | [2,1,3] |
π(U52) | = | [1,3,2] |
π(U53) | = | [3,1,2] |
π(U54) | = | [3,2,1] |
π(U55) | = | [1,2] |
π(U56) | = | 1 |
π(U61) | = | [1,2] |
π(U62) | = | [1,2] |
π(U71) | = | [3,1,2] |
π(U72) | = | [1,2] |
π(U73) | = | [1,2] |
π(isPal) | = | [1] |
π(U74) | = | [1] |
π(U81) | = | [1,2] |
π(U82) | = | [1,2] |
π(isNePal) | = | [1] |
π(U91) | = | [1,2] |
π(e) | = | [] |
π(o) | = | [] |
There are 127 ruless (increase limit for explicit display).
[active(x1)] | = | 1 · x1 |
[U13(x1)] | = | 1 + 2 · x1 |
[tt] | = | 0 |
[mark(x1)] | = | 2 · x1 |
[U26(x1)] | = | 1 + 1 · x1 |
[U33(x1)] | = | 1 + 1 · x1 |
[U46(x1)] | = | 2 + 1 · x1 |
[U63(x1)] | = | 1 + 2 · x1 |
[U83(x1)] | = | 2 · x1 |
[U92(x1)] | = | 1 · x1 |
[isPalListKind(x1)] | = | 1 + 1 · x1 |
[u] | = | 0 |
[U56(x1)] | = | 2 · x1 |
[U74(x1)] | = | 1 · x1 |
[__(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U12(x1, x2)] | = | 2 · x1 + 2 · x2 |
[isNeList(x1)] | = | 2 · 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 + 2 · x2 + 2 · x3 |
[U24(x1, x2, x3)] | = | 2 · x1 + 1 · x2 + 2 · x3 |
[U25(x1, x2)] | = | 2 · x1 + 2 · x2 |
[isList(x1)] | = | 2 · x1 |
[U31(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U32(x1, x2)] | = | 2 · x1 + 2 · x2 |
[isQid(x1)] | = | 2 · x1 |
[U41(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U42(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U44(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U51(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · 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 + 2 · x2 + 2 · x3 |
[U55(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U61(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U62(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U71(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U72(x1, x2)] | = | 1 · x1 + 2 · x2 |
[U73(x1, x2)] | = | 2 · x1 + 2 · x2 |
[isPal(x1)] | = | 2 · x1 |
[U81(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 2 · x1 + 1 · x2 |
[isNePal(x1)] | = | 2 · x1 |
[U91(x1, x2)] | = | 2 · x1 + 2 · x2 |
active(U13(tt)) | → | mark(tt) | (6) |
active(U26(tt)) | → | mark(tt) | (12) |
active(U33(tt)) | → | mark(tt) | (15) |
active(U46(tt)) | → | mark(tt) | (21) |
active(U63(tt)) | → | mark(tt) | (30) |
active(isPalListKind(u)) | → | mark(tt) | (55) |
mark(U13(X)) | → | active(U13(mark(X))) | (68) |
mark(U26(X)) | → | active(U26(mark(X))) | (76) |
mark(U33(X)) | → | active(U33(mark(X))) | (79) |
mark(U46(X)) | → | active(U46(mark(X))) | (86) |
mark(U63(X)) | → | active(U63(mark(X))) | (95) |
[active(x1)] | = | 1 + 1 · x1 |
[U83(x1)] | = | 2 + 2 · x1 |
[tt] | = | 1 |
[mark(x1)] | = | 2 · x1 |
[U92(x1)] | = | 2 + 2 · x1 |
[U56(x1)] | = | 2 + 2 · x1 |
[U74(x1)] | = | 2 + 2 · x1 |
[__(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U11(x1, x2)] | = | 2 · x1 + 1 · x2 |
[U12(x1, x2)] | = | 2 · x1 + 2 · x2 |
[isPalListKind(x1)] | = | 2 · x1 |
[U13(x1)] | = | 2 · x1 |
[isNeList(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 + 2 · x2 + 2 · x3 |
[U24(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U25(x1, x2)] | = | 2 · x1 + 2 · x2 |
[isList(x1)] | = | 2 · x1 |
[U26(x1)] | = | 2 · x1 |
[U31(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U32(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U33(x1)] | = | 2 · x1 |
[isQid(x1)] | = | 2 · x1 |
[U41(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U42(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U43(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U44(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · x3 |
[U45(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U46(x1)] | = | 2 · x1 |
[U51(x1, x2, x3)] | = | 2 · x1 + 2 · x2 + 2 · 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 + 2 · x2 + 2 · x3 |
[U55(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U61(x1, x2)] | = | 2 · x1 + 2 · 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 + 2 · x2 |
[isPal(x1)] | = | 2 · x1 |
[U81(x1, x2)] | = | 2 · x1 + 2 · x2 |
[U82(x1, x2)] | = | 2 · x1 + 2 · x2 |
[isNePal(x1)] | = | 2 · x1 |
[U91(x1, x2)] | = | 2 · x1 + 2 · x2 |
active(U83(tt)) | → | mark(tt) | (37) |
active(U92(tt)) | → | mark(tt) | (39) |
mark(U56(X)) | → | active(U56(mark(X))) | (92) |
mark(U74(X)) | → | active(U74(mark(X))) | (100) |
mark(U83(X)) | → | active(U83(mark(X))) | (103) |
mark(U92(X)) | → | active(U92(mark(X))) | (106) |
__(active(X1),X2) | → | __(X1,X2) | (114) |
__(X1,active(X2)) | → | __(X1,X2) | (115) |
U11(active(X1),X2) | → | U11(X1,X2) | (118) |
U11(X1,active(X2)) | → | U11(X1,X2) | (119) |
U12(active(X1),X2) | → | U12(X1,X2) | (122) |
U12(X1,active(X2)) | → | U12(X1,X2) | (123) |
isPalListKind(active(X)) | → | isPalListKind(X) | (125) |
U13(active(X)) | → | U13(X) | (127) |
isNeList(active(X)) | → | isNeList(X) | (129) |
U21(active(X1),X2,X3) | → | U21(X1,X2,X3) | (133) |
U21(X1,active(X2),X3) | → | U21(X1,X2,X3) | (134) |
U21(X1,X2,active(X3)) | → | U21(X1,X2,X3) | (135) |
U22(active(X1),X2,X3) | → | U22(X1,X2,X3) | (139) |
U22(X1,active(X2),X3) | → | U22(X1,X2,X3) | (140) |
U22(X1,X2,active(X3)) | → | U22(X1,X2,X3) | (141) |
U23(active(X1),X2,X3) | → | U23(X1,X2,X3) | (145) |
U23(X1,active(X2),X3) | → | U23(X1,X2,X3) | (146) |
U23(X1,X2,active(X3)) | → | U23(X1,X2,X3) | (147) |
U24(active(X1),X2,X3) | → | U24(X1,X2,X3) | (151) |
U24(X1,active(X2),X3) | → | U24(X1,X2,X3) | (152) |
U24(X1,X2,active(X3)) | → | U24(X1,X2,X3) | (153) |
U25(active(X1),X2) | → | U25(X1,X2) | (156) |
U25(X1,active(X2)) | → | U25(X1,X2) | (157) |
isList(active(X)) | → | isList(X) | (159) |
U26(active(X)) | → | U26(X) | (161) |
U31(active(X1),X2) | → | U31(X1,X2) | (164) |
U31(X1,active(X2)) | → | U31(X1,X2) | (165) |
U32(active(X1),X2) | → | U32(X1,X2) | (168) |
U32(X1,active(X2)) | → | U32(X1,X2) | (169) |
U33(active(X)) | → | U33(X) | (171) |
isQid(active(X)) | → | isQid(X) | (173) |
U41(active(X1),X2,X3) | → | U41(X1,X2,X3) | (177) |
U41(X1,active(X2),X3) | → | U41(X1,X2,X3) | (178) |
U41(X1,X2,active(X3)) | → | U41(X1,X2,X3) | (179) |
U42(active(X1),X2,X3) | → | U42(X1,X2,X3) | (183) |
U42(X1,active(X2),X3) | → | U42(X1,X2,X3) | (184) |
U42(X1,X2,active(X3)) | → | U42(X1,X2,X3) | (185) |
U43(active(X1),X2,X3) | → | U43(X1,X2,X3) | (189) |
U43(X1,active(X2),X3) | → | U43(X1,X2,X3) | (190) |
U43(X1,X2,active(X3)) | → | U43(X1,X2,X3) | (191) |
U44(active(X1),X2,X3) | → | U44(X1,X2,X3) | (195) |
U44(X1,active(X2),X3) | → | U44(X1,X2,X3) | (196) |
U44(X1,X2,active(X3)) | → | U44(X1,X2,X3) | (197) |
U45(active(X1),X2) | → | U45(X1,X2) | (200) |
U45(X1,active(X2)) | → | U45(X1,X2) | (201) |
U46(active(X)) | → | U46(X) | (203) |
U51(active(X1),X2,X3) | → | U51(X1,X2,X3) | (207) |
U51(X1,active(X2),X3) | → | U51(X1,X2,X3) | (208) |
U51(X1,X2,active(X3)) | → | U51(X1,X2,X3) | (209) |
U52(active(X1),X2,X3) | → | U52(X1,X2,X3) | (213) |
U52(X1,active(X2),X3) | → | U52(X1,X2,X3) | (214) |
U52(X1,X2,active(X3)) | → | U52(X1,X2,X3) | (215) |
U53(active(X1),X2,X3) | → | U53(X1,X2,X3) | (219) |
U53(X1,active(X2),X3) | → | U53(X1,X2,X3) | (220) |
U53(X1,X2,active(X3)) | → | U53(X1,X2,X3) | (221) |
U54(active(X1),X2,X3) | → | U54(X1,X2,X3) | (225) |
U54(X1,active(X2),X3) | → | U54(X1,X2,X3) | (226) |
U54(X1,X2,active(X3)) | → | U54(X1,X2,X3) | (227) |
U55(active(X1),X2) | → | U55(X1,X2) | (230) |
U55(X1,active(X2)) | → | U55(X1,X2) | (231) |
U56(active(X)) | → | U56(X) | (233) |
U61(active(X1),X2) | → | U61(X1,X2) | (236) |
U61(X1,active(X2)) | → | U61(X1,X2) | (237) |
U62(active(X1),X2) | → | U62(X1,X2) | (240) |
U62(X1,active(X2)) | → | U62(X1,X2) | (241) |
U63(active(X)) | → | U63(X) | (243) |
U71(active(X1),X2,X3) | → | U71(X1,X2,X3) | (247) |
U71(X1,active(X2),X3) | → | U71(X1,X2,X3) | (248) |
U71(X1,X2,active(X3)) | → | U71(X1,X2,X3) | (249) |
U72(active(X1),X2) | → | U72(X1,X2) | (252) |
U72(X1,active(X2)) | → | U72(X1,X2) | (253) |
U73(active(X1),X2) | → | U73(X1,X2) | (256) |
U73(X1,active(X2)) | → | U73(X1,X2) | (257) |
isPal(active(X)) | → | isPal(X) | (259) |
U74(active(X)) | → | U74(X) | (261) |
U81(active(X1),X2) | → | U81(X1,X2) | (264) |
U81(X1,active(X2)) | → | U81(X1,X2) | (265) |
U82(active(X1),X2) | → | U82(X1,X2) | (268) |
U82(X1,active(X2)) | → | U82(X1,X2) | (269) |
U83(active(X)) | → | U83(X) | (271) |
isNePal(active(X)) | → | isNePal(X) | (273) |
U91(active(X1),X2) | → | U91(X1,X2) | (276) |
U91(X1,active(X2)) | → | U91(X1,X2) | (277) |
U92(active(X)) | → | U92(X) | (279) |
There are no rules in the TRS. Hence, it is terminating.