The rewrite relation of the following TRS is considered.
active(zeros) | → | mark(cons(0,zeros)) | (1) |
active(tail(cons(X,XS))) | → | mark(XS) | (2) |
active(cons(X1,X2)) | → | cons(active(X1),X2) | (3) |
active(tail(X)) | → | tail(active(X)) | (4) |
cons(mark(X1),X2) | → | mark(cons(X1,X2)) | (5) |
tail(mark(X)) | → | mark(tail(X)) | (6) |
proper(zeros) | → | ok(zeros) | (7) |
proper(cons(X1,X2)) | → | cons(proper(X1),proper(X2)) | (8) |
proper(0) | → | ok(0) | (9) |
proper(tail(X)) | → | tail(proper(X)) | (10) |
cons(ok(X1),ok(X2)) | → | ok(cons(X1,X2)) | (11) |
tail(ok(X)) | → | ok(tail(X)) | (12) |
top(mark(X)) | → | top(proper(X)) | (13) |
top(ok(X)) | → | top(active(X)) | (14) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tail(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[zeros] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[0] | = |
|
active(tail(cons(X,XS))) | → | mark(XS) | (2) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tail(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[zeros] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[0] | = |
|
active(zeros) | → | mark(cons(0,zeros)) | (1) |
[mark(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tail(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[zeros] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[0] | = |
|
cons(mark(X1),X2) | → | mark(cons(X1,X2)) | (5) |
tail(mark(X)) | → | mark(tail(X)) | (6) |
top(mark(X)) | → | top(proper(X)) | (13) |
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tail(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[zeros] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[0] | = |
|
proper(zeros) | → | ok(zeros) | (7) |
cons(ok(X1),ok(X2)) | → | ok(cons(X1,X2)) | (11) |
[top(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tail(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[0] | = |
|
top(ok(X)) | → | top(active(X)) | (14) |
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tail(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[0] | = |
|
active(cons(X1,X2)) | → | cons(active(X1),X2) | (3) |
[active(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[cons(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[tail(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[ok(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[proper(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[0] | = |
|
proper(0) | → | ok(0) | (9) |
prec(ok) | = | 0 | weight(ok) | = | 2 | ||||
prec(proper) | = | 7 | weight(proper) | = | 0 | ||||
prec(tail) | = | 2 | weight(tail) | = | 2 | ||||
prec(cons) | = | 6 | weight(cons) | = | 0 | ||||
prec(active) | = | 3 | weight(active) | = | 2 |
active(tail(X)) | → | tail(active(X)) | (4) |
proper(cons(X1,X2)) | → | cons(proper(X1),proper(X2)) | (8) |
proper(tail(X)) | → | tail(proper(X)) | (10) |
tail(ok(X)) | → | ok(tail(X)) | (12) |
There are no rules in the TRS. Hence, it is terminating.