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) |
a__isPal#(V) | → | a__isNePal#(V) | (41) |
a__isNeList#(V) | → | a__isQid#(V) | (42) |
mark#(isQid(X)) | → | a__isQid#(X) | (43) |
mark#(__(X1,X2)) | → | mark#(X2) | (44) |
a__isNePal#(__(I,__(P,I))) | → | a__isQid#(I) | (45) |
mark#(__(X1,X2)) | → | a____#(mark(X1),mark(X2)) | (46) |
a____#(__(X,Y),Z) | → | a____#(mark(X),a____(mark(Y),mark(Z))) | (47) |
a____#(nil,X) | → | mark#(X) | (48) |
mark#(__(X1,X2)) | → | mark#(X1) | (49) |
a__isList#(__(V1,V2)) | → | a__and#(a__isList(V1),isList(V2)) | (50) |
a__and#(tt,X) | → | mark#(X) | (51) |
a____#(__(X,Y),Z) | → | mark#(X) | (52) |
mark#(isPal(X)) | → | a__isPal#(X) | (53) |
mark#(isNeList(X)) | → | a__isNeList#(X) | (54) |
mark#(isNePal(X)) | → | a__isNePal#(X) | (55) |
a__isNePal#(V) | → | a__isQid#(V) | (56) |
a____#(__(X,Y),Z) | → | mark#(Z) | (57) |
mark#(and(X1,X2)) | → | mark#(X1) | (58) |
a____#(__(X,Y),Z) | → | mark#(Y) | (59) |
a__isNeList#(__(V1,V2)) | → | a__isNeList#(V1) | (60) |
mark#(isList(X)) | → | a__isList#(X) | (61) |
a____#(__(X,Y),Z) | → | a____#(mark(Y),mark(Z)) | (62) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (63) |
a__isNeList#(__(V1,V2)) | → | a__and#(a__isNeList(V1),isList(V2)) | (64) |
a__isNeList#(__(V1,V2)) | → | a__and#(a__isList(V1),isNeList(V2)) | (65) |
a____#(X,nil) | → | mark#(X) | (66) |
a__isNePal#(__(I,__(P,I))) | → | a__and#(a__isQid(I),isPal(P)) | (67) |
a__isList#(__(V1,V2)) | → | a__isList#(V1) | (68) |
a__isNeList#(__(V1,V2)) | → | a__isList#(V1) | (69) |
a__isList#(V) | → | a__isNeList#(V) | (70) |
The dependency pairs are split into 1 component.
a__isList#(V) | → | a__isNeList#(V) | (70) |
a____#(__(X,Y),Z) | → | mark#(X) | (52) |
a__isNeList#(__(V1,V2)) | → | a__isList#(V1) | (69) |
a__and#(tt,X) | → | mark#(X) | (51) |
a__isList#(__(V1,V2)) | → | a__and#(a__isList(V1),isList(V2)) | (50) |
a__isList#(__(V1,V2)) | → | a__isList#(V1) | (68) |
mark#(__(X1,X2)) | → | mark#(X1) | (49) |
a__isNePal#(__(I,__(P,I))) | → | a__and#(a__isQid(I),isPal(P)) | (67) |
a____#(X,nil) | → | mark#(X) | (66) |
a____#(nil,X) | → | mark#(X) | (48) |
a__isNeList#(__(V1,V2)) | → | a__and#(a__isList(V1),isNeList(V2)) | (65) |
a____#(__(X,Y),Z) | → | a____#(mark(X),a____(mark(Y),mark(Z))) | (47) |
a__isNeList#(__(V1,V2)) | → | a__and#(a__isNeList(V1),isList(V2)) | (64) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (63) |
a____#(__(X,Y),Z) | → | a____#(mark(Y),mark(Z)) | (62) |
mark#(__(X1,X2)) | → | a____#(mark(X1),mark(X2)) | (46) |
mark#(__(X1,X2)) | → | mark#(X2) | (44) |
mark#(isList(X)) | → | a__isList#(X) | (61) |
a__isNeList#(__(V1,V2)) | → | a__isNeList#(V1) | (60) |
a____#(__(X,Y),Z) | → | mark#(Y) | (59) |
mark#(and(X1,X2)) | → | mark#(X1) | (58) |
a____#(__(X,Y),Z) | → | mark#(Z) | (57) |
mark#(isNePal(X)) | → | a__isNePal#(X) | (55) |
mark#(isNeList(X)) | → | a__isNeList#(X) | (54) |
a__isPal#(V) | → | a__isNePal#(V) | (41) |
mark#(isPal(X)) | → | a__isPal#(X) | (53) |
[a] | = | 1 |
[a__isNePal#(x1)] | = | x1 + 0 |
[a__isNeList#(x1)] | = | x1 + 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | x1 + 1 |
[u] | = | 51150 |
[and(x1, x2)] | = | x1 + x2 + 283 |
[a__isPal#(x1)] | = | x1 + 1 |
[isNePal(x1)] | = | x1 + 1 |
[a____#(x1, x2)] | = | x1 + x2 + 285 |
[isQid(x1)] | = | x1 + 1 |
[a____(x1, x2)] | = | x1 + x2 + 285 |
[a__isList(x1)] | = | x1 + 1 |
[a__isNeList(x1)] | = | x1 + 1 |
[o] | = | 1 |
[mark#(x1)] | = | x1 + 1 |
[isList(x1)] | = | x1 + 1 |
[a__and#(x1, x2)] | = | x2 + 283 |
[nil] | = | 1 |
[a__isQid#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[a__isNePal(x1)] | = | x1 + 1 |
[i] | = | 21775 |
[e] | = | 1 |
[a__isPal(x1)] | = | x1 + 1 |
[tt] | = | 1 |
[a__isQid(x1)] | = | x1 + 1 |
[a__isList#(x1)] | = | x1 + 1 |
[a__and(x1, x2)] | = | x1 + x2 + 283 |
[__(x1, x2)] | = | x1 + x2 + 285 |
a__isQid(o) | → | tt | (18) |
a__and(tt,X) | → | mark(X) | (4) |
a__isQid(a) | → | tt | (15) |
a__isNeList(V) | → | a__isQid(V) | (8) |
a____(__(X,Y),Z) | → | a____(mark(X),a____(mark(Y),mark(Z))) | (1) |
a____(nil,X) | → | mark(X) | (3) |
a__isQid(e) | → | tt | (16) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (21) |
a__isList(X) | → | isList(X) | (36) |
mark(isPal(X)) | → | a__isPal(X) | (26) |
a__isQid(u) | → | tt | (19) |
mark(o) | → | o | (32) |
a__isQid(i) | → | tt | (17) |
mark(nil) | → | nil | (27) |
a____(X1,X2) | → | __(X1,X2) | (34) |
mark(isList(X)) | → | a__isList(X) | (22) |
mark(tt) | → | tt | (28) |
a__isList(V) | → | a__isNeList(V) | (5) |
mark(u) | → | u | (33) |
a__isNeList(__(V1,V2)) | → | a__and(a__isNeList(V1),isList(V2)) | (10) |
a__isNePal(X) | → | isNePal(X) | (39) |
a__isList(__(V1,V2)) | → | a__and(a__isList(V1),isList(V2)) | (7) |
mark(__(X1,X2)) | → | a____(mark(X1),mark(X2)) | (20) |
mark(isNePal(X)) | → | a__isNePal(X) | (25) |
mark(e) | → | e | (30) |
a__isPal(nil) | → | tt | (14) |
mark(i) | → | i | (31) |
a__isNePal(__(I,__(P,I))) | → | a__and(a__isQid(I),isPal(P)) | (12) |
mark(isNeList(X)) | → | a__isNeList(X) | (23) |
mark(isQid(X)) | → | a__isQid(X) | (24) |
a__isNePal(V) | → | a__isQid(V) | (11) |
a__isNeList(__(V1,V2)) | → | a__and(a__isList(V1),isNeList(V2)) | (9) |
a__isPal(V) | → | a__isNePal(V) | (13) |
a__isPal(X) | → | isPal(X) | (40) |
a__isList(nil) | → | tt | (6) |
a__isQid(X) | → | isQid(X) | (38) |
a__isNeList(X) | → | isNeList(X) | (37) |
a__and(X1,X2) | → | and(X1,X2) | (35) |
mark(a) | → | a | (29) |
a____(X,nil) | → | mark(X) | (2) |
a__isList#(V) | → | a__isNeList#(V) | (70) |
a____#(__(X,Y),Z) | → | mark#(X) | (52) |
a__isNeList#(__(V1,V2)) | → | a__isList#(V1) | (69) |
a__and#(tt,X) | → | mark#(X) | (51) |
a__isList#(__(V1,V2)) | → | a__and#(a__isList(V1),isList(V2)) | (50) |
a__isList#(__(V1,V2)) | → | a__isList#(V1) | (68) |
mark#(__(X1,X2)) | → | mark#(X1) | (49) |
a__isNePal#(__(I,__(P,I))) | → | a__and#(a__isQid(I),isPal(P)) | (67) |
a____#(X,nil) | → | mark#(X) | (66) |
a____#(nil,X) | → | mark#(X) | (48) |
a__isNeList#(__(V1,V2)) | → | a__and#(a__isList(V1),isNeList(V2)) | (65) |
a__isNeList#(__(V1,V2)) | → | a__and#(a__isNeList(V1),isList(V2)) | (64) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (63) |
a____#(__(X,Y),Z) | → | a____#(mark(Y),mark(Z)) | (62) |
mark#(__(X1,X2)) | → | a____#(mark(X1),mark(X2)) | (46) |
mark#(__(X1,X2)) | → | mark#(X2) | (44) |
mark#(isList(X)) | → | a__isList#(X) | (61) |
a__isNeList#(__(V1,V2)) | → | a__isNeList#(V1) | (60) |
a____#(__(X,Y),Z) | → | mark#(Y) | (59) |
mark#(and(X1,X2)) | → | mark#(X1) | (58) |
a____#(__(X,Y),Z) | → | mark#(Z) | (57) |
mark#(isNePal(X)) | → | a__isNePal#(X) | (55) |
mark#(isNeList(X)) | → | a__isNeList#(X) | (54) |
a__isPal#(V) | → | a__isNePal#(V) | (41) |
mark#(isPal(X)) | → | a__isPal#(X) | (53) |
The dependency pairs are split into 1 component.
a____#(__(X,Y),Z) | → | a____#(mark(X),a____(mark(Y),mark(Z))) | (47) |
[a] | = | 1 |
[a__isNePal#(x1)] | = | 0 |
[a__isNeList#(x1)] | = | 0 |
[isNeList(x1)] | = | x1 + 1 |
[isPal(x1)] | = | x1 + 21238 |
[u] | = | 1 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[a__isPal#(x1)] | = | 1 |
[isNePal(x1)] | = | x1 + 21238 |
[a____#(x1, x2)] | = | x1 + 285 |
[isQid(x1)] | = | x1 + 1 |
[a____(x1, x2)] | = | x1 + x2 + 2 |
[a__isList(x1)] | = | x1 + 1 |
[a__isNeList(x1)] | = | x1 + 1 |
[o] | = | 1 |
[mark#(x1)] | = | 1 |
[isList(x1)] | = | x1 + 1 |
[a__and#(x1, x2)] | = | 283 |
[nil] | = | 1 |
[a__isQid#(x1)] | = | 0 |
[mark(x1)] | = | x1 + 0 |
[a__isNePal(x1)] | = | x1 + 21238 |
[i] | = | 1 |
[e] | = | 1 |
[a__isPal(x1)] | = | x1 + 21238 |
[tt] | = | 2 |
[a__isQid(x1)] | = | x1 + 1 |
[a__isList#(x1)] | = | 1 |
[a__and(x1, x2)] | = | x1 + x2 + 1 |
[__(x1, x2)] | = | x1 + x2 + 2 |
a__isQid(o) | → | tt | (18) |
a__and(tt,X) | → | mark(X) | (4) |
a__isQid(a) | → | tt | (15) |
a__isNeList(V) | → | a__isQid(V) | (8) |
a____(__(X,Y),Z) | → | a____(mark(X),a____(mark(Y),mark(Z))) | (1) |
a____(nil,X) | → | mark(X) | (3) |
a__isQid(e) | → | tt | (16) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (21) |
a__isList(X) | → | isList(X) | (36) |
mark(isPal(X)) | → | a__isPal(X) | (26) |
a__isQid(u) | → | tt | (19) |
mark(o) | → | o | (32) |
a__isQid(i) | → | tt | (17) |
mark(nil) | → | nil | (27) |
a____(X1,X2) | → | __(X1,X2) | (34) |
mark(isList(X)) | → | a__isList(X) | (22) |
mark(tt) | → | tt | (28) |
a__isList(V) | → | a__isNeList(V) | (5) |
mark(u) | → | u | (33) |
a__isNeList(__(V1,V2)) | → | a__and(a__isNeList(V1),isList(V2)) | (10) |
a__isNePal(X) | → | isNePal(X) | (39) |
a__isList(__(V1,V2)) | → | a__and(a__isList(V1),isList(V2)) | (7) |
mark(__(X1,X2)) | → | a____(mark(X1),mark(X2)) | (20) |
mark(isNePal(X)) | → | a__isNePal(X) | (25) |
mark(e) | → | e | (30) |
a__isPal(nil) | → | tt | (14) |
mark(i) | → | i | (31) |
a__isNePal(__(I,__(P,I))) | → | a__and(a__isQid(I),isPal(P)) | (12) |
mark(isNeList(X)) | → | a__isNeList(X) | (23) |
mark(isQid(X)) | → | a__isQid(X) | (24) |
a__isNePal(V) | → | a__isQid(V) | (11) |
a__isNeList(__(V1,V2)) | → | a__and(a__isList(V1),isNeList(V2)) | (9) |
a__isPal(V) | → | a__isNePal(V) | (13) |
a__isPal(X) | → | isPal(X) | (40) |
a__isList(nil) | → | tt | (6) |
a__isQid(X) | → | isQid(X) | (38) |
a__isNeList(X) | → | isNeList(X) | (37) |
a__and(X1,X2) | → | and(X1,X2) | (35) |
mark(a) | → | a | (29) |
a____(X,nil) | → | mark(X) | (2) |
a____#(__(X,Y),Z) | → | a____#(mark(X),a____(mark(Y),mark(Z))) | (47) |
The dependency pairs are split into 0 components.