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) |
f#(g(X),Y) | → | f#(X,n__f(g(X),activate(Y))) | (5) |
f#(g(X),Y) | → | activate#(Y) | (6) |
activate#(n__f(X1,X2)) | → | f#(X1,X2) | (7) |
t0 | = | f#(g(X'),n__f(g(g(X'')),X2)) |
→P | activate#(n__f(g(g(X'')),X2)) | |
→P | f#(g(g(X'')),X2) | |
→P | f#(g(X''),n__f(g(g(X'')),activate(X2))) | |
= | t3 |