The rewrite relation of the following TRS is considered.
f(g(X),Y) | → | f(X,n__f(n__g(X),activate(Y))) | (1) |
f(X1,X2) | → | n__f(X1,X2) | (2) |
g(X) | → | n__g(X) | (3) |
activate(n__f(X1,X2)) | → | f(activate(X1),X2) | (4) |
activate(n__g(X)) | → | g(activate(X)) | (5) |
activate(X) | → | X | (6) |
t0 | = | activate(n__f(n__g(g(X)),x2947)) |
→ | f(activate(n__g(g(X))),x2947) | |
→ | f(g(activate(g(X))),x2947) | |
→ | f(g(g(X)),x2947) | |
→ | f(g(X),n__f(n__g(g(X)),activate(x2947))) | |
→ | f(X,n__f(n__g(X),activate(n__f(n__g(g(X)),activate(x2947))))) | |
= | t5 |