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) |
f#(g(X),Y) | → | f#(X,n__f(n__g(X),activate(Y))) | (7) |
f#(g(X),Y) | → | activate#(Y) | (8) |
activate#(n__f(X1,X2)) | → | f#(activate(X1),X2) | (9) |
activate#(n__f(X1,X2)) | → | activate#(X1) | (10) |
activate#(n__g(X)) | → | g#(activate(X)) | (11) |
activate#(n__g(X)) | → | activate#(X) | (12) |
activate#(n__g(X)) | → | g#(activate(X)) | (11) |
activate#(n__g(X)) | → | activate#(X) | (12) |
activate#(n__f(X1,X2)) | → | activate#(X1) | (10) |
activate#(n__f(n__f(x0,x1),y1)) | → | f#(f(activate(x0),x1),y1) | (13) |
activate#(n__f(n__g(x0),y1)) | → | f#(g(activate(x0)),y1) | (14) |
activate#(n__f(x0,y1)) | → | f#(x0,y1) | (15) |
t0 | = | activate#(n__f(n__g(g(X)),y1)) |
→P | f#(g(activate(g(X))),y1) | |
→R | f#(g(g(X)),y1) | |
→P | f#(g(X),n__f(n__g(g(X)),activate(y1))) | |
→P | activate#(n__f(n__g(g(X)),activate(y1))) | |
= | t4 |