The rewrite relation of the following TRS is considered.
app(g,app(h,app(g,x))) | → | app(g,x) | (1) |
app(g,app(g,x)) | → | app(g,app(h,app(g,x))) | (2) |
app(h,app(h,x)) | → | app(h,app(app(f,app(h,x)),x)) | (3) |
app(app(map,fun),nil) | → | nil | (4) |
app(app(map,fun),app(app(cons,x),xs)) | → | app(app(cons,app(fun,x)),app(app(map,fun),xs)) | (5) |
app(app(filter,fun),nil) | → | nil | (6) |
app(app(filter,fun),app(app(cons,x),xs)) | → | app(app(app(app(filter2,app(fun,x)),fun),x),xs) | (7) |
app(app(app(app(filter2,true),fun),x),xs) | → | app(app(cons,x),app(app(filter,fun),xs)) | (8) |
app(app(app(app(filter2,false),fun),x),xs) | → | app(app(filter,fun),xs) | (9) |
app#(g,app(g,x)) | → | app#(h,app(g,x)) | (10) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(app(app(filter2,app(fun,x)),fun),x) | (11) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(map,fun),xs) | (12) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (13) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(cons,app(fun,x)) | (14) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (15) |
app#(h,app(h,x)) | → | app#(h,app(app(f,app(h,x)),x)) | (16) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(filter,fun) | (17) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(app(filter2,app(fun,x)),fun) | (18) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(cons,app(fun,x)),app(app(map,fun),xs)) | (19) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(app(app(app(filter2,app(fun,x)),fun),x),xs) | (20) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(cons,x),app(app(filter,fun),xs)) | (21) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(filter,fun),xs) | (22) |
app#(h,app(h,x)) | → | app#(f,app(h,x)) | (23) |
app#(app(app(app(filter2,false),fun),x),xs) | → | app#(app(filter,fun),xs) | (24) |
app#(g,app(g,x)) | → | app#(g,app(h,app(g,x))) | (25) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(filter2,app(fun,x)) | (26) |
app#(h,app(h,x)) | → | app#(app(f,app(h,x)),x) | (27) |
app#(app(app(app(filter2,false),fun),x),xs) | → | app#(filter,fun) | (28) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(cons,x) | (29) |
The dependency pairs are split into 2 components.
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (15) |
app#(app(app(app(filter2,false),fun),x),xs) | → | app#(app(filter,fun),xs) | (24) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (13) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(map,fun),xs) | (12) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(filter,fun),xs) | (22) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(app(app(app(filter2,app(fun,x)),fun),x),xs) | (20) |
[h] | = | 1 |
[false] | = | 35919 |
[true] | = | 282 |
[f] | = | 35141 |
[filter2] | = | 32335 |
[nil] | = | 36466 |
[app#(x1, x2)] | = | x2 + 0 |
[map] | = | 33428 |
[cons] | = | 26372 |
[filter] | = | 85957 |
[g] | = | 39558 |
[app(x1, x2)] | = | x1 + x2 + 8851 |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (15) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (13) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(map,fun),xs) | (12) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(app(app(app(filter2,app(fun,x)),fun),x),xs) | (20) |
The dependency pairs are split into 0 components.
app#(g,app(g,x)) | → | app#(g,app(h,app(g,x))) | (25) |
[h] | = | 591 |
[false] | = | 0 |
[true] | = | 0 |
[f] | = | 0 |
[filter2] | = | 28183 |
[nil] | = | 0 |
[app#(x1, x2)] | = | x2 + 0 |
[map] | = | 3564 |
[cons] | = | 203 |
[filter] | = | 29865 |
[g] | = | 3038 |
[app(x1, x2)] | = | x1 + 841 |
app(app(map,fun),nil) | → | nil | (4) |
app(app(app(app(filter2,true),fun),x),xs) | → | app(app(cons,x),app(app(filter,fun),xs)) | (8) |
app(g,app(h,app(g,x))) | → | app(g,x) | (1) |
app(h,app(h,x)) | → | app(h,app(app(f,app(h,x)),x)) | (3) |
app(app(map,fun),app(app(cons,x),xs)) | → | app(app(cons,app(fun,x)),app(app(map,fun),xs)) | (5) |
app(app(filter,fun),app(app(cons,x),xs)) | → | app(app(app(app(filter2,app(fun,x)),fun),x),xs) | (7) |
app(app(app(app(filter2,false),fun),x),xs) | → | app(app(filter,fun),xs) | (9) |
app(app(filter,fun),nil) | → | nil | (6) |
app(g,app(g,x)) | → | app(g,app(h,app(g,x))) | (2) |
app#(g,app(g,x)) | → | app#(g,app(h,app(g,x))) | (25) |
The dependency pairs are split into 0 components.