The rewrite relation of the following TRS is considered.
f(a,f(a,f(b,f(x,y)))) | → | f(b,f(c,f(b,f(a,f(a,f(a,f(x,y))))))) | (1) |
f(a,f(c,f(x,y))) | → | f(b,f(x,y)) | (2) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(b,f(c,f(b,f(a,f(a,f(a,f(x,y))))))) | (3) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(c,f(b,f(a,f(a,f(a,f(x,y)))))) | (4) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(b,f(a,f(a,f(a,f(x,y))))) | (5) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(a,f(a,f(a,f(x,y)))) | (6) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(a,f(a,f(x,y))) | (7) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(a,f(x,y)) | (8) |
f#(a,f(c,f(x,y))) | → | f#(b,f(x,y)) | (9) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(b,f(c,f(b,f(a,f(a,f(a,f(x,y))))))) | (3) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(c,f(b,f(a,f(a,f(a,f(x,y)))))) | (4) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(b,f(a,f(a,f(a,f(x,y))))) | (5) |
f#(a,f(c,f(x,y))) | → | f#(b,f(x,y)) | (9) |
f#(a,f(a,f(b,f(b,f(x0,x1))))) | → | f#(a,f(b,f(c,f(b,f(a,f(a,f(a,f(x0,x1)))))))) | (10) |
f#(a,f(a,f(b,f(a,f(b,f(x0,x1)))))) | → | f#(a,f(a,f(b,f(c,f(b,f(a,f(a,f(a,f(x0,x1))))))))) | (11) |
f#(a,f(a,f(b,f(c,f(x0,x1))))) | → | f#(a,f(a,f(b,f(x0,x1)))) | (12) |
f#(a,f(a,f(b,f(a,f(a,f(b,f(x0,x1))))))) | → | f#(a,f(a,f(a,f(b,f(c,f(b,f(a,f(a,f(a,f(x0,x1)))))))))) | (13) |
f#(a,f(a,f(b,f(a,f(c,f(x0,x1)))))) | → | f#(a,f(a,f(a,f(b,f(x0,x1))))) | (14) |
f#(a,f(a,f(b,f(b,f(x0,x1))))) | → | f#(a,f(b,f(c,f(b,f(a,f(a,f(a,f(x0,x1)))))))) | (10) |
f#(a,f(a,f(b,f(x,y)))) | → | f#(a,f(a,f(x,y))) | (7) |
f#(a,f(a,f(b,f(a,f(b,f(x0,x1)))))) | → | f#(a,f(a,f(b,f(c,f(b,f(a,f(a,f(a,f(x0,x1))))))))) | (11) |
f#(a,f(a,f(b,f(c,f(x0,x1))))) | → | f#(a,f(a,f(b,f(x0,x1)))) | (12) |
f#(a,f(a,f(b,f(a,f(a,f(b,f(x0,x1))))))) | → | f#(a,f(a,f(a,f(b,f(c,f(b,f(a,f(a,f(a,f(x0,x1)))))))))) | (13) |
f#(a,f(a,f(b,f(a,f(c,f(x0,x1)))))) | → | f#(a,f(a,f(a,f(b,f(x0,x1))))) | (14) |
f#(a,f(a,f(b,f(a,x1)))) | → | f#(a,f(a,x1)) | (15) |
t0 | = | f#(a,f(a,f(a,f(a,f(a,f(c,f(b,f(x,y)))))))) |
→R | f#(a,f(a,f(a,f(a,f(b,f(b,f(x,y))))))) | |
→R | f#(a,f(a,f(b,f(c,f(b,f(a,f(a,f(a,f(b,f(x,y)))))))))) | |
→R | f#(a,f(a,f(b,f(c,f(b,f(a,f(b,f(c,f(b,f(a,f(a,f(a,f(x,y))))))))))))) | |
→P | f#(a,f(a,f(b,f(b,f(a,f(b,f(c,f(b,f(a,f(a,f(a,f(x,y)))))))))))) | |
→P | f#(a,f(a,f(b,f(a,f(b,f(c,f(b,f(a,f(a,f(a,f(x,y))))))))))) | |
→P | f#(a,f(a,f(b,f(c,f(b,f(a,f(a,f(a,f(c,f(b,f(a,f(a,f(a,f(x,y)))))))))))))) | |
→P | f#(a,f(a,f(b,f(b,f(a,f(a,f(a,f(c,f(b,f(a,f(a,f(a,f(x,y))))))))))))) | |
→P | f#(a,f(a,f(b,f(a,f(a,f(a,f(c,f(b,f(a,f(a,f(a,f(x,y)))))))))))) | |
→P | f#(a,f(a,f(a,f(a,f(a,f(c,f(b,f(a,f(a,f(a,f(x,y))))))))))) | |
= | t9 |