The rewrite relation of the following TRS is considered.
f(X) | → | g(n__h(n__f(X))) | (1) |
h(X) | → | n__h(X) | (2) |
f(X) | → | n__f(X) | (3) |
activate(n__h(X)) | → | h(activate(X)) | (4) |
activate(n__f(X)) | → | f(activate(X)) | (5) |
activate(X) | → | X | (6) |
[h(x1)] | = |
|
||||||||||||||||||||||||
[n__f(x1)] | = |
|
||||||||||||||||||||||||
[g(x1)] | = |
|
||||||||||||||||||||||||
[activate(x1)] | = |
|
||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||
[n__h(x1)] | = |
|
f(X) | → | g(n__h(n__f(X))) | (1) |
f(X) | → | n__f(X) | (3) |
prec(activate) | = | 3 | weight(activate) | = | 2 | ||||
prec(h) | = | 1 | weight(h) | = | 4 | ||||
prec(n__h) | = | 0 | weight(n__h) | = | 4 | ||||
prec(n__f) | = | 7 | weight(n__f) | = | 2 | ||||
prec(f) | = | 2 | weight(f) | = | 2 |
h(X) | → | n__h(X) | (2) |
activate(n__h(X)) | → | h(activate(X)) | (4) |
activate(n__f(X)) | → | f(activate(X)) | (5) |
activate(X) | → | X | (6) |
There are no rules in the TRS. Hence, it is terminating.