The rewrite relation of the following TRS is considered.
| app(app(neq,0),0) | → | false | (1) |
| app(app(neq,0),app(s,y)) | → | true | (2) |
| app(app(neq,app(s,x)),0) | → | true | (3) |
| app(app(neq,app(s,x)),app(s,y)) | → | app(app(neq,x),y) | (4) |
| app(app(filter,f),nil) | → | nil | (5) |
| app(app(filter,f),app(app(cons,y),ys)) | → | app(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys)) | (6) |
| app(app(app(filtersub,true),f),app(app(cons,y),ys)) | → | app(app(cons,y),app(app(filter,f),ys)) | (7) |
| app(app(app(filtersub,false),f),app(app(cons,y),ys)) | → | app(app(filter,f),ys) | (8) |
| nonzero | → | app(filter,app(neq,0)) | (9) |
| app#(app(neq,app(s,x)),app(s,y)) | → | app#(neq,x) | (10) |
| app#(app(neq,app(s,x)),app(s,y)) | → | app#(app(neq,x),y) | (11) |
| app#(app(filter,f),app(app(cons,y),ys)) | → | app#(f,y) | (12) |
| app#(app(filter,f),app(app(cons,y),ys)) | → | app#(filtersub,app(f,y)) | (13) |
| app#(app(filter,f),app(app(cons,y),ys)) | → | app#(app(filtersub,app(f,y)),f) | (14) |
| app#(app(filter,f),app(app(cons,y),ys)) | → | app#(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys)) | (15) |
| app#(app(app(filtersub,true),f),app(app(cons,y),ys)) | → | app#(filter,f) | (16) |
| app#(app(app(filtersub,true),f),app(app(cons,y),ys)) | → | app#(app(filter,f),ys) | (17) |
| app#(app(app(filtersub,true),f),app(app(cons,y),ys)) | → | app#(app(cons,y),app(app(filter,f),ys)) | (18) |
| app#(app(app(filtersub,false),f),app(app(cons,y),ys)) | → | app#(filter,f) | (19) |
| app#(app(app(filtersub,false),f),app(app(cons,y),ys)) | → | app#(app(filter,f),ys) | (20) |
| nonzero# | → | app#(neq,0) | (21) |
| nonzero# | → | app#(filter,app(neq,0)) | (22) |
The dependency pairs are split into 2 components.
| app#(app(filter,f),app(app(cons,y),ys)) | → | app#(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys)) | (15) |
| app#(app(app(filtersub,false),f),app(app(cons,y),ys)) | → | app#(app(filter,f),ys) | (20) |
| app#(app(filter,f),app(app(cons,y),ys)) | → | app#(f,y) | (12) |
| app#(app(app(filtersub,true),f),app(app(cons,y),ys)) | → | app#(app(filter,f),ys) | (17) |
| π(app#) | = | 2 |
| app#(app(app(filtersub,false),f),app(app(cons,y),ys)) | → | app#(app(filter,f),ys) | (20) |
| app#(app(filter,f),app(app(cons,y),ys)) | → | app#(f,y) | (12) |
| app#(app(app(filtersub,true),f),app(app(cons,y),ys)) | → | app#(app(filter,f),ys) | (17) |
The dependency pairs are split into 0 components.
| app#(app(neq,app(s,x)),app(s,y)) | → | app#(app(neq,x),y) | (11) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(app(neq,app(s,x)),app(s,y)) | → | app#(app(neq,x),y) | (11) |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.