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