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__isNePal(__(I,__(P,I))) | → | tt | (5) |
mark(__(X1,X2)) | → | a____(mark(X1),mark(X2)) | (6) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (7) |
mark(isNePal(X)) | → | a__isNePal(mark(X)) | (8) |
mark(nil) | → | nil | (9) |
mark(tt) | → | tt | (10) |
a____(X1,X2) | → | __(X1,X2) | (11) |
a__and(X1,X2) | → | and(X1,X2) | (12) |
a__isNePal(X) | → | isNePal(X) | (13) |
mark#(__(X1,X2)) | → | a____#(mark(X1),mark(X2)) | (14) |
mark#(and(X1,X2)) | → | mark#(X1) | (15) |
mark#(isNePal(X)) | → | a__isNePal#(mark(X)) | (16) |
a____#(__(X,Y),Z) | → | mark#(X) | (17) |
a____#(__(X,Y),Z) | → | mark#(Y) | (18) |
a____#(__(X,Y),Z) | → | mark#(Z) | (19) |
mark#(isNePal(X)) | → | mark#(X) | (20) |
a____#(nil,X) | → | mark#(X) | (21) |
a____#(__(X,Y),Z) | → | a____#(mark(Y),mark(Z)) | (22) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (23) |
mark#(__(X1,X2)) | → | mark#(X1) | (24) |
a____#(X,nil) | → | mark#(X) | (25) |
a____#(__(X,Y),Z) | → | a____#(mark(X),a____(mark(Y),mark(Z))) | (26) |
a__and#(tt,X) | → | mark#(X) | (27) |
mark#(__(X1,X2)) | → | mark#(X2) | (28) |
The dependency pairs are split into 1 component.
mark#(__(X1,X2)) | → | mark#(X2) | (28) |
mark#(isNePal(X)) | → | mark#(X) | (20) |
a__and#(tt,X) | → | mark#(X) | (27) |
a____#(__(X,Y),Z) | → | mark#(Z) | (19) |
a____#(__(X,Y),Z) | → | a____#(mark(X),a____(mark(Y),mark(Z))) | (26) |
a____#(X,nil) | → | mark#(X) | (25) |
mark#(__(X1,X2)) | → | mark#(X1) | (24) |
a____#(__(X,Y),Z) | → | mark#(Y) | (18) |
a____#(__(X,Y),Z) | → | mark#(X) | (17) |
mark#(and(X1,X2)) | → | mark#(X1) | (15) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (23) |
a____#(__(X,Y),Z) | → | a____#(mark(Y),mark(Z)) | (22) |
a____#(nil,X) | → | mark#(X) | (21) |
mark#(__(X1,X2)) | → | a____#(mark(X1),mark(X2)) | (14) |
[a__isNePal#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNePal(x1)] | = | x1 + 2438 |
[a____#(x1, x2)] | = | x1 + x2 + 0 |
[a____(x1, x2)] | = | x1 + x2 + 1 |
[mark#(x1)] | = | x1 + 0 |
[a__and#(x1, x2)] | = | x1 + x2 + 0 |
[nil] | = | 8856 |
[mark(x1)] | = | x1 + 0 |
[a__isNePal(x1)] | = | x1 + 2438 |
[tt] | = | 1 |
[a__and(x1, x2)] | = | x1 + x2 + 1 |
[__(x1, x2)] | = | x1 + x2 + 1 |
a__and(tt,X) | → | mark(X) | (4) |
mark(isNePal(X)) | → | a__isNePal(mark(X)) | (8) |
a____(__(X,Y),Z) | → | a____(mark(X),a____(mark(Y),mark(Z))) | (1) |
a____(nil,X) | → | mark(X) | (3) |
a__isNePal(__(I,__(P,I))) | → | tt | (5) |
mark(tt) | → | tt | (10) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (7) |
a__and(X1,X2) | → | and(X1,X2) | (12) |
a____(X1,X2) | → | __(X1,X2) | (11) |
mark(nil) | → | nil | (9) |
a__isNePal(X) | → | isNePal(X) | (13) |
mark(__(X1,X2)) | → | a____(mark(X1),mark(X2)) | (6) |
a____(X,nil) | → | mark(X) | (2) |
mark#(__(X1,X2)) | → | mark#(X2) | (28) |
mark#(isNePal(X)) | → | mark#(X) | (20) |
a__and#(tt,X) | → | mark#(X) | (27) |
a____#(__(X,Y),Z) | → | mark#(Z) | (19) |
a____#(X,nil) | → | mark#(X) | (25) |
mark#(__(X1,X2)) | → | mark#(X1) | (24) |
a____#(__(X,Y),Z) | → | mark#(Y) | (18) |
a____#(__(X,Y),Z) | → | mark#(X) | (17) |
mark#(and(X1,X2)) | → | mark#(X1) | (15) |
mark#(and(X1,X2)) | → | a__and#(mark(X1),X2) | (23) |
a____#(__(X,Y),Z) | → | a____#(mark(Y),mark(Z)) | (22) |
a____#(nil,X) | → | mark#(X) | (21) |
mark#(__(X1,X2)) | → | a____#(mark(X1),mark(X2)) | (14) |
The dependency pairs are split into 1 component.
a____#(__(X,Y),Z) | → | a____#(mark(X),a____(mark(Y),mark(Z))) | (26) |
[a__isNePal#(x1)] | = | 0 |
[and(x1, x2)] | = | x1 + x2 + 1 |
[isNePal(x1)] | = | x1 + 2438 |
[a____#(x1, x2)] | = | x1 + 0 |
[a____(x1, x2)] | = | x1 + x2 + 1 |
[mark#(x1)] | = | 0 |
[a__and#(x1, x2)] | = | 0 |
[nil] | = | 50349 |
[mark(x1)] | = | x1 + 0 |
[a__isNePal(x1)] | = | x1 + 2438 |
[tt] | = | 1507 |
[a__and(x1, x2)] | = | x1 + x2 + 1 |
[__(x1, x2)] | = | x1 + x2 + 1 |
a__and(tt,X) | → | mark(X) | (4) |
mark(isNePal(X)) | → | a__isNePal(mark(X)) | (8) |
a____(__(X,Y),Z) | → | a____(mark(X),a____(mark(Y),mark(Z))) | (1) |
a____(nil,X) | → | mark(X) | (3) |
a__isNePal(__(I,__(P,I))) | → | tt | (5) |
mark(tt) | → | tt | (10) |
mark(and(X1,X2)) | → | a__and(mark(X1),X2) | (7) |
a__and(X1,X2) | → | and(X1,X2) | (12) |
a____(X1,X2) | → | __(X1,X2) | (11) |
mark(nil) | → | nil | (9) |
a__isNePal(X) | → | isNePal(X) | (13) |
mark(__(X1,X2)) | → | a____(mark(X1),mark(X2)) | (6) |
a____(X,nil) | → | mark(X) | (2) |
a____#(__(X,Y),Z) | → | a____#(mark(X),a____(mark(Y),mark(Z))) | (26) |
The dependency pairs are split into 0 components.