The rewrite relation of the following TRS is considered.
active(and(tt,X)) | → | mark(X) | (1) |
active(plus(N,0)) | → | mark(N) | (2) |
active(plus(N,s(M))) | → | mark(s(plus(N,M))) | (3) |
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (4) |
mark(tt) | → | active(tt) | (5) |
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (6) |
mark(0) | → | active(0) | (7) |
mark(s(X)) | → | active(s(mark(X))) | (8) |
and(mark(X1),X2) | → | and(X1,X2) | (9) |
and(X1,mark(X2)) | → | and(X1,X2) | (10) |
and(active(X1),X2) | → | and(X1,X2) | (11) |
and(X1,active(X2)) | → | and(X1,X2) | (12) |
plus(mark(X1),X2) | → | plus(X1,X2) | (13) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (14) |
plus(active(X1),X2) | → | plus(X1,X2) | (15) |
plus(X1,active(X2)) | → | plus(X1,X2) | (16) |
s(mark(X)) | → | s(X) | (17) |
s(active(X)) | → | s(X) | (18) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
active(and(tt,X)) | → | mark(X) | (1) |
active(plus(N,0)) | → | mark(N) | (2) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
and(X1,mark(X2)) | → | and(X1,X2) | (10) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
active(plus(N,s(M))) | → | mark(s(plus(N,M))) | (3) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
mark(tt) | → | active(tt) | (5) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
and(X1,active(X2)) | → | and(X1,X2) | (12) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
and(mark(X1),X2) | → | and(X1,X2) | (9) |
and(active(X1),X2) | → | and(X1,X2) | (11) |
plus(mark(X1),X2) | → | plus(X1,X2) | (13) |
plus(active(X1),X2) | → | plus(X1,X2) | (15) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
plus(X1,active(X2)) | → | plus(X1,X2) | (16) |
s(active(X)) | → | s(X) | (18) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
mark(s(X)) | → | active(s(mark(X))) | (8) |
plus(X1,mark(X2)) | → | plus(X1,X2) | (14) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
s(mark(X)) | → | s(X) | (17) |
[0] | = | 18 |
[and(x1, x2)] | = | 1 · x1 + 16 · x2 + 1 |
[mark(x1)] | = | 4 · x1 + 0 |
[plus(x1, x2)] | = | 16 · x1 + 2 · x2 + 1 |
[active(x1)] | = | 1 · x1 + 3 |
mark(0) | → | active(0) | (7) |
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
mark(plus(X1,X2)) | → | active(plus(mark(X1),mark(X2))) | (6) |
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
mark(and(X1,X2)) | → | active(and(mark(X1),X2)) | (4) |
There are no rules in the TRS. Hence, it is terminating.