The rewrite relation of the following TRS is considered.
a__f(X,g(X),Y) | → | a__f(Y,Y,Y) | (1) |
a__g(b) | → | c | (2) |
a__b | → | c | (3) |
mark(f(X1,X2,X3)) | → | a__f(X1,X2,X3) | (4) |
mark(g(X)) | → | a__g(mark(X)) | (5) |
mark(b) | → | a__b | (6) |
mark(c) | → | c | (7) |
a__f(X1,X2,X3) | → | f(X1,X2,X3) | (8) |
a__g(X) | → | g(X) | (9) |
a__b | → | b | (10) |
a__f#(X,g(X),Y) | → | a__f#(Y,Y,Y) | (11) |
mark#(f(X1,X2,X3)) | → | a__f#(X1,X2,X3) | (12) |
mark#(g(X)) | → | a__g#(mark(X)) | (13) |
mark#(g(X)) | → | mark#(X) | (14) |
mark#(b) | → | a__b# | (15) |
mark#(f(X1,X2,X3)) | → | a__f#(X1,X2,X3) | (12) |
mark#(g(X)) | → | a__g#(mark(X)) | (13) |
mark#(g(X)) | → | mark#(X) | (14) |
mark#(b) | → | a__b# | (15) |
t0 | = | a__f#(a__g(a__b),a__g(a__b),a__g(a__b)) |
→R | a__f#(a__g(a__b),a__g(c),a__g(a__b)) | |
→R | a__f#(a__g(a__b),g(c),a__g(a__b)) | |
→R | a__f#(a__g(b),g(c),a__g(a__b)) | |
→R | a__f#(c,g(c),a__g(a__b)) | |
→P | a__f#(a__g(a__b),a__g(a__b),a__g(a__b)) | |
= | t5 |