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