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) |
active(and(X1,X2)) | → | and(active(X1),X2) | (4) |
active(plus(X1,X2)) | → | plus(active(X1),X2) | (5) |
active(plus(X1,X2)) | → | plus(X1,active(X2)) | (6) |
active(s(X)) | → | s(active(X)) | (7) |
and(mark(X1),X2) | → | mark(and(X1,X2)) | (8) |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (9) |
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (10) |
s(mark(X)) | → | mark(s(X)) | (11) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (12) |
proper(tt) | → | ok(tt) | (13) |
proper(plus(X1,X2)) | → | plus(proper(X1),proper(X2)) | (14) |
proper(0) | → | ok(0) | (15) |
proper(s(X)) | → | s(proper(X)) | (16) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (17) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (18) |
s(ok(X)) | → | ok(s(X)) | (19) |
top(mark(X)) | → | top(proper(X)) | (20) |
top(ok(X)) | → | top(active(X)) | (21) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
active(and(tt,X)) | → | mark(X) | (1) |
active(plus(N,0)) | → | mark(N) | (2) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
active(plus(N,s(M))) | → | mark(s(plus(N,M))) | (3) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
and(mark(X1),X2) | → | mark(and(X1,X2)) | (8) |
top(mark(X)) | → | top(proper(X)) | (20) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
proper(plus(X1,X2)) | → | plus(proper(X1),proper(X2)) | (14) |
and(ok(X1),ok(X2)) | → | ok(and(X1,X2)) | (17) |
plus(ok(X1),ok(X2)) | → | ok(plus(X1,X2)) | (18) |
top(ok(X)) | → | top(active(X)) | (21) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tt] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
proper(tt) | → | ok(tt) | (13) |
[0] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[and(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[plus(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
plus(X1,mark(X2)) | → | mark(plus(X1,X2)) | (10) |
proper(0) | → | ok(0) | (15) |
prec(ok) | = | 2 | weight(ok) | = | 4 | ||||
prec(proper) | = | 7 | weight(proper) | = | 0 | ||||
prec(s) | = | 3 | weight(s) | = | 2 | ||||
prec(plus) | = | 4 | weight(plus) | = | 0 | ||||
prec(mark) | = | 1 | weight(mark) | = | 2 | ||||
prec(active) | = | 5 | weight(active) | = | 2 | ||||
prec(and) | = | 0 | weight(and) | = | 0 |
active(and(X1,X2)) | → | and(active(X1),X2) | (4) |
active(plus(X1,X2)) | → | plus(active(X1),X2) | (5) |
active(plus(X1,X2)) | → | plus(X1,active(X2)) | (6) |
active(s(X)) | → | s(active(X)) | (7) |
plus(mark(X1),X2) | → | mark(plus(X1,X2)) | (9) |
s(mark(X)) | → | mark(s(X)) | (11) |
proper(and(X1,X2)) | → | and(proper(X1),proper(X2)) | (12) |
proper(s(X)) | → | s(proper(X)) | (16) |
s(ok(X)) | → | ok(s(X)) | (19) |
There are no rules in the TRS. Hence, it is terminating.