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(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (6) |
mark(nil) | → | active(nil) | (7) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (8) |
mark(tt) | → | active(tt) | (9) |
mark(isNePal(X)) | → | active(isNePal(mark(X))) | (10) |
__(mark(X1),X2) | → | __(X1,X2) | (11) |
__(X1,mark(X2)) | → | __(X1,X2) | (12) |
__(active(X1),X2) | → | __(X1,X2) | (13) |
__(X1,active(X2)) | → | __(X1,X2) | (14) |
and(mark(X1),X2) | → | and(X1,X2) | (15) |
and(X1,mark(X2)) | → | and(X1,X2) | (16) |
and(active(X1),X2) | → | and(X1,X2) | (17) |
and(X1,active(X2)) | → | and(X1,X2) | (18) |
isNePal(mark(X)) | → | isNePal(X) | (19) |
isNePal(active(X)) | → | isNePal(X) | (20) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
active(isNePal(__(I,__(P,I)))) | → | mark(tt) | (5) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
active(__(X,nil)) | → | mark(X) | (2) |
active(__(nil,X)) | → | mark(X) | (3) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
active(and(tt,X)) | → | mark(X) | (4) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
and(X1,mark(X2)) | → | and(X1,X2) | (16) |
and(X1,active(X2)) | → | and(X1,X2) | (18) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
active(__(__(X,Y),Z)) | → | mark(__(X,__(Y,Z))) | (1) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
__(mark(X1),X2) | → | __(X1,X2) | (11) |
and(mark(X1),X2) | → | and(X1,X2) | (15) |
isNePal(mark(X)) | → | isNePal(X) | (19) |
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[nil] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
mark(nil) | → | active(nil) | (7) |
mark(tt) | → | active(tt) | (9) |
mark(isNePal(X)) | → | active(isNePal(mark(X))) | (10) |
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[isNePal(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
isNePal(active(X)) | → | isNePal(X) | (20) |
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
__(X1,mark(X2)) | → | __(X1,X2) | (12) |
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[__(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
mark(__(X1,X2)) | → | active(__(mark(X1),mark(X2))) | (6) |
mark#(and(X1,X2)) | → | mark#(X1) | (21) |
mark#(and(X1,X2)) | → | and#(mark(X1),X2) | (22) |
__#(active(X1),X2) | → | __#(X1,X2) | (23) |
__#(X1,active(X2)) | → | __#(X1,X2) | (24) |
and#(active(X1),X2) | → | and#(X1,X2) | (25) |
The dependency pairs are split into 3 components.
mark#(and(X1,X2)) | → | mark#(X1) | (21) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
mark#(and(X1,X2)) | → | mark#(X1) | (21) |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
and#(active(X1),X2) | → | and#(X1,X2) | (25) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
and#(active(X1),X2) | → | and#(X1,X2) | (25) |
2 | ≥ | 2 | |
1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
__#(active(X1),X2) | → | __#(X1,X2) | (23) |
__#(X1,active(X2)) | → | __#(X1,X2) | (24) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
__#(active(X1),X2) | → | __#(X1,X2) | (23) |
2 | ≥ | 2 | |
1 | > | 1 | |
__#(X1,active(X2)) | → | __#(X1,X2) | (24) |
2 | > | 2 | |
1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.