The rewrite relation of the following TRS is considered.
app(app(f,0),n) | → | app(app(hd,app(app(map,f),app(app(cons,0),nil))),n) | (1) |
app(app(map,f),nil) | → | nil | (2) |
app(app(map,f),app(app(cons,x),xs)) | → | app(app(cons,app(f,x)),app(app(map,f),xs)) | (3) |
t0 | = | app(app(f,0),n) |
→ | app(app(hd,app(app(map,f),app(app(cons,0),nil))),n) | |
= | t1 |