The rewrite relation of the following TRS is considered.
ap(ap(g,x),y) | → | y | (1) |
ap(f,x) | → | ap(f,app(g,x)) | (2) |
ap(ap(g,x),y) | → | y | (1) |
ap(f,x0) |
ap#(f,x) | → | ap#(f,app(g,x)) | (3) |
ap(f,x) | → | ap(f,app(g,x)) | (2) |
We restrict the innermost strategy to the following left hand sides.
There are no lhss.
ap#(f,app(g,z0)) | → | ap#(f,app(g,app(g,z0))) | (4) |
ap#(f,app(g,app(g,z0))) | → | ap#(f,app(g,app(g,app(g,z0)))) | (5) |
t0 | = | ap#(f,app(g,app(g,z0))) |
→P | ap#(f,app(g,app(g,app(g,z0)))) | |
= | t1 |