The rewrite relation of the following TRS is considered.
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(X,nil)) | → | mark(X) | (2) |
active(__(nil,X)) | → | mark(X) | (3) |
active(and(tt,X)) | → | mark(X) | (4) |
active(isList(V)) | → | mark(isNeList(V)) | (5) |
active(isList(nil)) | → | mark(tt) | (6) |
active(isList(__(V1,V2))) | → | mark(and(isList(V1),isList(V2))) | (7) |
active(isNeList(V)) | → | mark(isQid(V)) | (8) |
active(isNeList(__(V1,V2))) | → | mark(and(isList(V1),isNeList(V2))) | (9) |
active(isNeList(__(V1,V2))) | → | mark(and(isNeList(V1),isList(V2))) | (10) |
active(isNePal(V)) | → | mark(isQid(V)) | (11) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
active(isPal(V)) | → | mark(isNePal(V)) | (13) |
active(isPal(nil)) | → | mark(tt) | (14) |
active(isQid(a)) | → | mark(tt) | (15) |
active(isQid(e)) | → | mark(tt) | (16) |
active(isQid(i)) | → | mark(tt) | (17) |
active(isQid(o)) | → | mark(tt) | (18) |
active(isQid(u)) | → | mark(tt) | (19) |
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (20) |
mark(nil) | → | active(nil) | (21) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (22) |
mark(tt) | → | active(tt) | (23) |
mark(isList(X)) | → | active(isList(X)) | (24) |
mark(isNeList(X)) | → | active(isNeList(X)) | (25) |
mark(isQid(X)) | → | active(isQid(X)) | (26) |
mark(isNePal(X)) | → | active(isNePal(X)) | (27) |
mark(isPal(X)) | → | active(isPal(X)) | (28) |
mark(a) | → | active(a) | (29) |
mark(e) | → | active(e) | (30) |
mark(i) | → | active(i) | (31) |
mark(o) | → | active(o) | (32) |
mark(u) | → | active(u) | (33) |
__(mark(X1),X2) | → | __(X1,X2) | (34) |
__(X1,mark(X2)) | → | __(X1,X2) | (35) |
__(active(X1),X2) | → | __(X1,X2) | (36) |
__(X1,active(X2)) | → | __(X1,X2) | (37) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
isList(mark(X)) | → | isList(X) | (42) |
isList(active(X)) | → | isList(X) | (43) |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isNeList(active(X)) | → | isNeList(X) | (45) |
isQid(mark(X)) | → | isQid(X) | (46) |
isQid(active(X)) | → | isQid(X) | (47) |
isNePal(mark(X)) | → | isNePal(X) | (48) |
isNePal(active(X)) | → | isNePal(X) | (49) |
isPal(mark(X)) | → | isPal(X) | (50) |
isPal(active(X)) | → | isPal(X) | (51) |
[active(x1)] | = | 1 · x1 |
[__(x1, x2)] | = | 2 + 2 · x1 + 1 · x2 |
[mark(x1)] | = | 1 · x1 |
[nil] | = | 0 |
[and(x1, x2)] | = | 1 · x1 + 1 · x2 |
[tt] | = | 0 |
[isList(x1)] | = | 2 + 1 · x1 |
[isNeList(x1)] | = | 1 · x1 |
[isQid(x1)] | = | 1 · x1 |
[isNePal(x1)] | = | 1 · x1 |
[isPal(x1)] | = | 2 · x1 |
[a] | = | 2 |
[e] | = | 0 |
[i] | = | 1 |
[o] | = | 1 |
[u] | = | 0 |
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
active(__(X,nil)) | → | mark(X) | (2) |
active(__(nil,X)) | → | mark(X) | (3) |
active(isList(V)) | → | mark(isNeList(V)) | (5) |
active(isList(nil)) | → | mark(tt) | (6) |
active(isNePal(__(I,__(P,I)))) | → | mark(and(isQid(I),isPal(P))) | (12) |
active(isQid(a)) | → | mark(tt) | (15) |
active(isQid(i)) | → | mark(tt) | (17) |
active(isQid(o)) | → | mark(tt) | (18) |
[active(x1)] | = | 1 · x1 |
[and(x1, x2)] | = | 1 · x1 + 1 · x2 |
[tt] | = | 0 |
[mark(x1)] | = | 1 · x1 |
[isList(x1)] | = | 1 · x1 |
[__(x1, x2)] | = | 2 · x1 + 1 · x2 |
[isNeList(x1)] | = | 1 · x1 |
[isQid(x1)] | = | 1 · x1 |
[isNePal(x1)] | = | 2 · x1 |
[isPal(x1)] | = | 2 · x1 |
[nil] | = | 0 |
[e] | = | 2 |
[u] | = | 0 |
[a] | = | 0 |
[i] | = | 0 |
[o] | = | 0 |
active(isQid(e)) | → | mark(tt) | (16) |
[active(x1)] | = | 1 · x1 |
[and(x1, x2)] | = | 1 · x1 + 1 · x2 |
[tt] | = | 2 |
[mark(x1)] | = | 1 · x1 |
[isList(x1)] | = | 1 + 2 · x1 |
[__(x1, x2)] | = | 2 + 2 · x1 + 1 · x2 |
[isNeList(x1)] | = | 1 + 2 · x1 |
[isQid(x1)] | = | 2 · x1 |
[isNePal(x1)] | = | 2 + 2 · x1 |
[isPal(x1)] | = | 2 + 2 · x1 |
[nil] | = | 2 |
[u] | = | 2 |
[a] | = | 0 |
[e] | = | 0 |
[i] | = | 0 |
[o] | = | 0 |
active(and(tt,X)) | → | mark(X) | (4) |
active(isList(__(V1,V2))) | → | mark(and(isList(V1),isList(V2))) | (7) |
active(isNeList(V)) | → | mark(isQid(V)) | (8) |
active(isNeList(__(V1,V2))) | → | mark(and(isList(V1),isNeList(V2))) | (9) |
active(isNeList(__(V1,V2))) | → | mark(and(isNeList(V1),isList(V2))) | (10) |
active(isNePal(V)) | → | mark(isQid(V)) | (11) |
active(isPal(nil)) | → | mark(tt) | (14) |
active(isQid(u)) | → | mark(tt) | (19) |
[active(x1)] | = | 1 · x1 |
[isPal(x1)] | = | 2 + 1 · x1 |
[mark(x1)] | = | 1 · x1 |
[isNePal(x1)] | = | 1 + 1 · x1 |
[__(x1, x2)] | = | 2 · x1 + 2 · x2 |
[nil] | = | 0 |
[and(x1, x2)] | = | 1 · x1 + 1 · x2 |
[tt] | = | 0 |
[isList(x1)] | = | 2 · x1 |
[isNeList(x1)] | = | 2 · x1 |
[isQid(x1)] | = | 2 · x1 |
[a] | = | 0 |
[e] | = | 0 |
[i] | = | 0 |
[o] | = | 0 |
[u] | = | 0 |
active(isPal(V)) | → | mark(isNePal(V)) | (13) |
[mark(x1)] | = | 1 + 2 · x1 |
[__(x1, x2)] | = | 2 + 1 · x1 + 1 · x2 |
[active(x1)] | = | 1 · x1 |
[nil] | = | 2 |
[and(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[tt] | = | 2 |
[isList(x1)] | = | 2 + 1 · x1 |
[isNeList(x1)] | = | 2 + 1 · x1 |
[isQid(x1)] | = | 2 + 1 · x1 |
[isNePal(x1)] | = | 2 + 1 · x1 |
[isPal(x1)] | = | 2 + 1 · x1 |
[a] | = | 2 |
[e] | = | 2 |
[i] | = | 2 |
[o] | = | 1 |
[u] | = | 2 |
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (20) |
mark(nil) | → | active(nil) | (21) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (22) |
mark(tt) | → | active(tt) | (23) |
mark(isList(X)) | → | active(isList(X)) | (24) |
mark(isNeList(X)) | → | active(isNeList(X)) | (25) |
mark(isQid(X)) | → | active(isQid(X)) | (26) |
mark(isNePal(X)) | → | active(isNePal(X)) | (27) |
mark(isPal(X)) | → | active(isPal(X)) | (28) |
mark(a) | → | active(a) | (29) |
mark(e) | → | active(e) | (30) |
mark(i) | → | active(i) | (31) |
mark(o) | → | active(o) | (32) |
mark(u) | → | active(u) | (33) |
__(mark(X1),X2) | → | __(X1,X2) | (34) |
__(X1,mark(X2)) | → | __(X1,X2) | (35) |
and(mark(X1),X2) | → | and(X1,X2) | (38) |
and(X1,mark(X2)) | → | and(X1,X2) | (39) |
isList(mark(X)) | → | isList(X) | (42) |
isNeList(mark(X)) | → | isNeList(X) | (44) |
isQid(mark(X)) | → | isQid(X) | (46) |
isNePal(mark(X)) | → | isNePal(X) | (48) |
isPal(mark(X)) | → | isPal(X) | (50) |
prec(active) | = | 7 | weight(active) | = | 0 | ||||
prec(isList) | = | 2 | weight(isList) | = | 1 | ||||
prec(isNeList) | = | 3 | weight(isNeList) | = | 1 | ||||
prec(isQid) | = | 4 | weight(isQid) | = | 1 | ||||
prec(isNePal) | = | 5 | weight(isNePal) | = | 1 | ||||
prec(isPal) | = | 6 | weight(isPal) | = | 1 | ||||
prec(__) | = | 0 | weight(__) | = | 0 | ||||
prec(and) | = | 1 | weight(and) | = | 0 |
__(active(X1),X2) | → | __(X1,X2) | (36) |
__(X1,active(X2)) | → | __(X1,X2) | (37) |
and(active(X1),X2) | → | and(X1,X2) | (40) |
and(X1,active(X2)) | → | and(X1,X2) | (41) |
isList(active(X)) | → | isList(X) | (43) |
isNeList(active(X)) | → | isNeList(X) | (45) |
isQid(active(X)) | → | isQid(X) | (47) |
isNePal(active(X)) | → | isNePal(X) | (49) |
isPal(active(X)) | → | isPal(X) | (51) |
There are no rules in the TRS. Hence, it is terminating.