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) |
app#(app(f,0),n) |
→ |
app#(app(hd,app(app(map,f),app(app(cons,0),nil))),n) |
(4) |
app#(app(f,0),n) |
→ |
app#(hd,app(app(map,f),app(app(cons,0),nil))) |
(5) |
app#(app(f,0),n) |
→ |
app#(app(map,f),app(app(cons,0),nil)) |
(6) |
app#(app(f,0),n) |
→ |
app#(map,f) |
(7) |
app#(app(f,0),n) |
→ |
app#(app(cons,0),nil) |
(8) |
app#(app(f,0),n) |
→ |
app#(cons,0) |
(9) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(app(cons,app(f,x)),app(app(map,f),xs)) |
(10) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(cons,app(f,x)) |
(11) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(f,x) |
(12) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(app(map,f),xs) |
(13) |
It remains to prove infiniteness of the resulting DP problem.
app#(app(0,0),y1) |
→ |
app#(app(hd,app(app(hd,app(app(map,map),app(app(cons,0),nil))),app(app(cons,0),nil))),y1) |
(14) |
app#(app(x0,0),y1) |
→ |
app#(app(hd,app(app(cons,app(x0,0)),app(app(map,x0),nil))),y1) |
(15) |
app#(app(y0,0),y1) |
→ |
app#(app(hd,app(app(map,y0),app(app(hd,app(app(map,cons),app(app(cons,0),nil))),nil))),y1) |
(16) |