The rewrite relation of the following TRS is considered.
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__and(tt,X) |
→ |
mark(X) |
(4) |
a__isList(V) |
→ |
a__isNeList(V) |
(5) |
a__isList(nil) |
→ |
tt |
(6) |
a__isList(__(V1,V2)) |
→ |
a__and(a__isList(V1),isList(V2)) |
(7) |
a__isNeList(V) |
→ |
a__isQid(V) |
(8) |
a__isNeList(__(V1,V2)) |
→ |
a__and(a__isList(V1),isNeList(V2)) |
(9) |
a__isNeList(__(V1,V2)) |
→ |
a__and(a__isNeList(V1),isList(V2)) |
(10) |
a__isNePal(V) |
→ |
a__isQid(V) |
(11) |
a__isNePal(__(I,__(P,I))) |
→ |
a__and(a__isQid(I),isPal(P)) |
(12) |
a__isPal(V) |
→ |
a__isNePal(V) |
(13) |
a__isPal(nil) |
→ |
tt |
(14) |
a__isQid(a) |
→ |
tt |
(15) |
a__isQid(e) |
→ |
tt |
(16) |
a__isQid(i) |
→ |
tt |
(17) |
a__isQid(o) |
→ |
tt |
(18) |
a__isQid(u) |
→ |
tt |
(19) |
mark(__(X1,X2)) |
→ |
a____(mark(X1),mark(X2)) |
(20) |
mark(and(X1,X2)) |
→ |
a__and(mark(X1),X2) |
(21) |
mark(isList(X)) |
→ |
a__isList(X) |
(22) |
mark(isNeList(X)) |
→ |
a__isNeList(X) |
(23) |
mark(isQid(X)) |
→ |
a__isQid(X) |
(24) |
mark(isNePal(X)) |
→ |
a__isNePal(X) |
(25) |
mark(isPal(X)) |
→ |
a__isPal(X) |
(26) |
mark(nil) |
→ |
nil |
(27) |
mark(tt) |
→ |
tt |
(28) |
mark(a) |
→ |
a |
(29) |
mark(e) |
→ |
e |
(30) |
mark(i) |
→ |
i |
(31) |
mark(o) |
→ |
o |
(32) |
mark(u) |
→ |
u |
(33) |
a____(X1,X2) |
→ |
__(X1,X2) |
(34) |
a__and(X1,X2) |
→ |
and(X1,X2) |
(35) |
a__isList(X) |
→ |
isList(X) |
(36) |
a__isNeList(X) |
→ |
isNeList(X) |
(37) |
a__isQid(X) |
→ |
isQid(X) |
(38) |
a__isNePal(X) |
→ |
isNePal(X) |
(39) |
a__isPal(X) |
→ |
isPal(X) |
(40) |
The evaluation strategy is innermost.
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__and(tt,X) |
→ |
mark(X) |
(4) |
a__isList(V) |
→ |
a__isNeList(V) |
(5) |
a__isList(nil) |
→ |
tt |
(6) |
a__isList(__(V1,V2)) |
→ |
a__and(a__isList(V1),isList(V2)) |
(7) |
a__isNeList(V) |
→ |
a__isQid(V) |
(8) |
a__isNeList(__(V1,V2)) |
→ |
a__and(a__isList(V1),isNeList(V2)) |
(9) |
a__isNeList(__(V1,V2)) |
→ |
a__and(a__isNeList(V1),isList(V2)) |
(10) |
a__isNePal(V) |
→ |
a__isQid(V) |
(11) |
a__isNePal(__(I,__(P,I))) |
→ |
a__and(a__isQid(I),isPal(P)) |
(12) |
a__isPal(V) |
→ |
a__isNePal(V) |
(13) |
a__isPal(nil) |
→ |
tt |
(14) |
a__isQid(a) |
→ |
tt |
(15) |
a__isQid(e) |
→ |
tt |
(16) |
a__isQid(i) |
→ |
tt |
(17) |
a__isQid(o) |
→ |
tt |
(18) |
a__isQid(u) |
→ |
tt |
(19) |
mark(__(X1,X2)) |
→ |
a____(mark(X1),mark(X2)) |
(20) |
mark(and(X1,X2)) |
→ |
a__and(mark(X1),X2) |
(21) |
mark(isList(X)) |
→ |
a__isList(X) |
(22) |
mark(isNeList(X)) |
→ |
a__isNeList(X) |
(23) |
mark(isQid(X)) |
→ |
a__isQid(X) |
(24) |
mark(isNePal(X)) |
→ |
a__isNePal(X) |
(25) |
mark(isPal(X)) |
→ |
a__isPal(X) |
(26) |
mark(nil) |
→ |
nil |
(27) |
mark(tt) |
→ |
tt |
(28) |
mark(a) |
→ |
a |
(29) |
mark(e) |
→ |
e |
(30) |
mark(i) |
→ |
i |
(31) |
mark(o) |
→ |
o |
(32) |
mark(u) |
→ |
u |
(33) |
a____(X1,X2) |
→ |
__(X1,X2) |
(34) |
a__and(X1,X2) |
→ |
and(X1,X2) |
(35) |
a__isList(X) |
→ |
isList(X) |
(36) |
a__isNeList(X) |
→ |
isNeList(X) |
(37) |
a__isQid(X) |
→ |
isQid(X) |
(38) |
a__isNePal(X) |
→ |
isNePal(X) |
(39) |
a__isPal(X) |
→ |
isPal(X) |
(40) |
There are no rules in the TRS. Hence, it is terminating.