The rewrite relation of the following TRS is considered.
| app(app(app(f,app(g,x)),app(s,0)),y) | → | app(app(app(f,y),y),app(g,x)) | (1) |
| app(g,app(s,x)) | → | app(s,app(g,x)) | (2) |
| app(g,0) | → | 0 | (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#(app(app(f,app(g,x)),app(s,0)),y) | → | app#(app(app(f,y),y),app(g,x)) | (10) |
| app#(app(app(f,app(g,x)),app(s,0)),y) | → | app#(app(f,y),y) | (11) |
| app#(app(app(f,app(g,x)),app(s,0)),y) | → | app#(f,y) | (12) |
| app#(g,app(s,x)) | → | app#(s,app(g,x)) | (13) |
| app#(g,app(s,x)) | → | app#(g,x) | (14) |
| app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(cons,app(fun,x)),app(app(map,fun),xs)) | (15) |
| app#(app(map,fun),app(app(cons,x),xs)) | → | app#(cons,app(fun,x)) | (16) |
| app#(app(map,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (17) |
| app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(map,fun),xs) | (18) |
| app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(app(app(app(filter2,app(fun,x)),fun),x),xs) | (19) |
| app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(app(app(filter2,app(fun,x)),fun),x) | (20) |
| app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(app(filter2,app(fun,x)),fun) | (21) |
| app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(filter2,app(fun,x)) | (22) |
| app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (23) |
| app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(cons,x),app(app(filter,fun),xs)) | (24) |
| app#(app(app(app(filter2,true),fun),x),xs) | → | app#(cons,x) | (25) |
| app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(filter,fun),xs) | (26) |
| app#(app(app(app(filter2,true),fun),x),xs) | → | app#(filter,fun) | (27) |
| app#(app(app(app(filter2,false),fun),x),xs) | → | app#(app(filter,fun),xs) | (28) |
| app#(app(app(app(filter2,false),fun),x),xs) | → | app#(filter,fun) | (29) |
The dependency pairs are split into 2 components.
| app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(map,fun),xs) | (18) |
| app#(app(map,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (17) |
| app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (23) |
| app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(filter,fun),xs) | (26) |
| app#(app(app(app(filter2,false),fun),x),xs) | → | app#(app(filter,fun),xs) | (28) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (23) |
| 1 | > | 1 | |
| 2 | > | 2 | |
| app#(app(map,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (17) |
| 1 | > | 1 | |
| 2 | > | 2 | |
| app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(map,fun),xs) | (18) |
| 1 | ≥ | 1 | |
| 2 | > | 2 | |
| app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(filter,fun),xs) | (26) |
| 2 | ≥ | 2 | |
| app#(app(app(app(filter2,false),fun),x),xs) | → | app#(app(filter,fun),xs) | (28) |
| 2 | ≥ | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| app#(g,app(s,x)) | → | app#(g,x) | (14) |
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(g,app(s,x)) | → | app#(g,x) | (14) |
| 1 | ≥ | 1 | |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.