The rewrite relation of the following TRS is considered.
app(f,a) |
→ |
app(f,b) |
(1) |
app(g,b) |
→ |
app(g,a) |
(2) |
app(app(map,fun),nil) |
→ |
nil |
(3) |
app(app(map,fun),app(app(cons,x),xs)) |
→ |
app(app(cons,app(fun,x)),app(app(map,fun),xs)) |
(4) |
app(app(filter,fun),nil) |
→ |
nil |
(5) |
app(app(filter,fun),app(app(cons,x),xs)) |
→ |
app(app(app(app(filter2,app(fun,x)),fun),x),xs) |
(6) |
app(app(app(app(filter2,true),fun),x),xs) |
→ |
app(app(cons,x),app(app(filter,fun),xs)) |
(7) |
app(app(app(app(filter2,false),fun),x),xs) |
→ |
app(app(filter,fun),xs) |
(8) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(app(app(app(filter2,app(fun,x)),fun),x),xs) |
(9) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(fun,x) |
(10) |
app#(app(app(app(filter2,false),fun),x),xs) |
→ |
app#(filter,fun) |
(11) |
app#(app(app(app(filter2,true),fun),x),xs) |
→ |
app#(app(filter,fun),xs) |
(12) |
app#(f,a) |
→ |
app#(f,b) |
(13) |
app#(app(app(app(filter2,false),fun),x),xs) |
→ |
app#(app(filter,fun),xs) |
(14) |
app#(app(map,fun),app(app(cons,x),xs)) |
→ |
app#(app(cons,app(fun,x)),app(app(map,fun),xs)) |
(15) |
app#(app(app(app(filter2,true),fun),x),xs) |
→ |
app#(app(cons,x),app(app(filter,fun),xs)) |
(16) |
app#(app(app(app(filter2,true),fun),x),xs) |
→ |
app#(filter,fun) |
(17) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(filter2,app(fun,x)) |
(18) |
app#(app(map,fun),app(app(cons,x),xs)) |
→ |
app#(app(map,fun),xs) |
(19) |
app#(app(map,fun),app(app(cons,x),xs)) |
→ |
app#(fun,x) |
(20) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(app(app(filter2,app(fun,x)),fun),x) |
(21) |
app#(g,b) |
→ |
app#(g,a) |
(22) |
app#(app(app(app(filter2,true),fun),x),xs) |
→ |
app#(cons,x) |
(23) |
app#(app(map,fun),app(app(cons,x),xs)) |
→ |
app#(cons,app(fun,x)) |
(24) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(app(filter2,app(fun,x)),fun) |
(25) |
The dependency pairs are split into 1
component.