The rewrite relation of the following TRS is considered.
ap(f,x) | → | x | (1) |
ap(ap(ap(g,x),y),ap(s,z)) | → | ap(ap(ap(g,x),y),ap(ap(x,y),0)) | (2) |
t0 | = | ap(ap(ap(g,f),s),ap(ap(f,s),0)) |
→ | ap(ap(ap(g,f),s),ap(s,0)) | |
→ | ap(ap(ap(g,f),s),ap(ap(f,s),0)) | |
= | t2 |