The rewrite relation of the following TRS is considered.
f(f(X)) | → | c(n__f(n__g(n__f(X)))) | (1) |
c(X) | → | d(activate(X)) | (2) |
h(X) | → | c(n__d(X)) | (3) |
f(X) | → | n__f(X) | (4) |
g(X) | → | n__g(X) | (5) |
d(X) | → | n__d(X) | (6) |
activate(n__f(X)) | → | f(activate(X)) | (7) |
activate(n__g(X)) | → | g(X) | (8) |
activate(n__d(X)) | → | d(X) | (9) |
activate(X) | → | X | (10) |
f(f(X)) | → | n__f(n__g(n__f(c(X)))) | (11) |
c(X) | → | activate(d(X)) | (12) |
h(X) | → | n__d(c(X)) | (13) |
f(X) | → | n__f(X) | (4) |
g(X) | → | n__g(X) | (5) |
d(X) | → | n__d(X) | (6) |
n__f(activate(X)) | → | activate(f(X)) | (14) |
n__g(activate(X)) | → | g(X) | (15) |
n__d(activate(X)) | → | d(X) | (16) |
activate(X) | → | X | (10) |
[activate(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
||||||||||||||||||||||||
[n__f(x1)] | = |
|
||||||||||||||||||||||||
[c(x1)] | = |
|
||||||||||||||||||||||||
[d(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[n__d(x1)] | = |
|
||||||||||||||||||||||||
[h(x1)] | = |
|
||||||||||||||||||||||||
[n__g(x1)] | = |
|
h(X) | → | n__d(c(X)) | (13) |
[activate(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
||||||||||||||||||||||||
[n__f(x1)] | = |
|
||||||||||||||||||||||||
[c(x1)] | = |
|
||||||||||||||||||||||||
[d(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[n__d(x1)] | = |
|
||||||||||||||||||||||||
[n__g(x1)] | = |
|
n__f(activate(X)) | → | activate(f(X)) | (14) |
n__d(activate(X)) | → | d(X) | (16) |
prec(g) | = | 0 | weight(g) | = | 4 | ||||
prec(n__d) | = | 6 | weight(n__d) | = | 1 | ||||
prec(d) | = | 1 | weight(d) | = | 2 | ||||
prec(activate) | = | 3 | weight(activate) | = | 1 | ||||
prec(c) | = | 2 | weight(c) | = | 4 | ||||
prec(n__g) | = | 4 | weight(n__g) | = | 3 | ||||
prec(n__f) | = | 7 | weight(n__f) | = | 0 | ||||
prec(f) | = | 5 | weight(f) | = | 4 |
f(f(X)) | → | n__f(n__g(n__f(c(X)))) | (11) |
c(X) | → | activate(d(X)) | (12) |
f(X) | → | n__f(X) | (4) |
g(X) | → | n__g(X) | (5) |
d(X) | → | n__d(X) | (6) |
n__g(activate(X)) | → | g(X) | (15) |
activate(X) | → | X | (10) |
There are no rules in the TRS. Hence, it is terminating.