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(U11(tt)) | → | mark(U12(tt)) | (4) |
active(U12(tt)) | → | mark(tt) | (5) |
active(isNePal(__(I,__(P,I)))) | → | mark(U11(tt)) | (6) |
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (7) |
mark(nil) | → | active(nil) | (8) |
mark(U11(X)) | → | active(U11(mark(X))) | (9) |
mark(tt) | → | active(tt) | (10) |
mark(U12(X)) | → | active(U12(mark(X))) | (11) |
mark(isNePal(X)) | → | active(isNePal(mark(X))) | (12) |
__(mark(X1),X2) | → | __(X1,X2) | (13) |
__(X1,mark(X2)) | → | __(X1,X2) | (14) |
__(active(X1),X2) | → | __(X1,X2) | (15) |
__(X1,active(X2)) | → | __(X1,X2) | (16) |
U11(mark(X)) | → | U11(X) | (17) |
U11(active(X)) | → | U11(X) | (18) |
U12(mark(X)) | → | U12(X) | (19) |
U12(active(X)) | → | U12(X) | (20) |
isNePal(mark(X)) | → | isNePal(X) | (21) |
isNePal(active(X)) | → | isNePal(X) | (22) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[U12(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
active(__(X,nil)) | → | mark(X) | (2) |
active(__(nil,X)) | → | mark(X) | (3) |
active(isNePal(__(I,__(P,I)))) | → | mark(U11(tt)) | (6) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[U12(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
active(U11(tt)) | → | mark(U12(tt)) | (4) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[U12(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
active(U12(tt)) | → | mark(tt) | (5) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[U12(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[U12(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
mark(tt) | → | active(tt) | (10) |
mark(U12(X)) | → | active(U12(mark(X))) | (11) |
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[U12(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
U12(mark(X)) | → | U12(X) | (19) |
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[U12(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
__(mark(X1),X2) | → | __(X1,X2) | (13) |
__(active(X1),X2) | → | __(X1,X2) | (15) |
__(X1,active(X2)) | → | __(X1,X2) | (16) |
U11(mark(X)) | → | U11(X) | (17) |
U11(active(X)) | → | U11(X) | (18) |
U12(active(X)) | → | U12(X) | (20) |
isNePal(mark(X)) | → | isNePal(X) | (21) |
isNePal(active(X)) | → | isNePal(X) | (22) |
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
__(X1,mark(X2)) | → | __(X1,X2) | (14) |
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[U11(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
mark(isNePal(X)) | → | active(isNePal(mark(X))) | (12) |
final states:
{6}
transitions:
mark1(6) | → | 10 |
mark1(6) | → | 11 |
__1(11,10) | → | 12 |
active0(6) | → | 6 |
nil0 | → | 6 |
__0(6,6) | → | 6 |
U110(6) | → | 6 |
active1(12) | → | 6 |
active1(12) | → | 11 |
active1(12) | → | 10 |
mark0(6) | → | 6 |
nil1 | → | 12 |
U111(10) | → | 12 |