The rewrite relation of the following TRS is considered.
| app(app(map,f),nil) | → | nil | (1) |
| app(app(map,f),app(app(cons,x),xs)) | → | app(app(cons,app(f,x)),app(app(map,f),xs)) | (2) |
| app(app(le,0),y) | → | true | (3) |
| app(app(le,app(s,x)),0) | → | false | (4) |
| app(app(le,app(s,x)),app(s,y)) | → | app(app(le,x),y) | (5) |
| app(app(maxlist,x),app(app(cons,y),ys)) | → | app(app(if,app(app(le,x),y)),app(app(maxlist,y),ys)) | (6) |
| app(app(maxlist,x),nil) | → | x | (7) |
| app(height,app(app(node,x),xs)) | → | app(s,app(app(maxlist,0),app(app(map,height),xs))) | (8) |
| app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (9) |
| app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (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#(app(cons,app(f,x)),app(app(map,f),xs)) | (12) |
| app#(app(le,app(s,x)),app(s,y)) | → | app#(le,x) | (13) |
| app#(app(le,app(s,x)),app(s,y)) | → | app#(app(le,x),y) | (14) |
| app#(app(maxlist,x),app(app(cons,y),ys)) | → | app#(maxlist,y) | (15) |
| app#(app(maxlist,x),app(app(cons,y),ys)) | → | app#(app(maxlist,y),ys) | (16) |
| app#(app(maxlist,x),app(app(cons,y),ys)) | → | app#(le,x) | (17) |
| app#(app(maxlist,x),app(app(cons,y),ys)) | → | app#(app(le,x),y) | (18) |
| app#(app(maxlist,x),app(app(cons,y),ys)) | → | app#(if,app(app(le,x),y)) | (19) |
| app#(app(maxlist,x),app(app(cons,y),ys)) | → | app#(app(if,app(app(le,x),y)),app(app(maxlist,y),ys)) | (20) |
| app#(height,app(app(node,x),xs)) | → | app#(map,height) | (21) |
| app#(height,app(app(node,x),xs)) | → | app#(app(map,height),xs) | (22) |
| app#(height,app(app(node,x),xs)) | → | app#(maxlist,0) | (23) |
| app#(height,app(app(node,x),xs)) | → | app#(app(maxlist,0),app(app(map,height),xs)) | (24) |
| app#(height,app(app(node,x),xs)) | → | app#(s,app(app(maxlist,0),app(app(map,height),xs))) | (25) |
The dependency pairs are split into 3 components.
| app#(height,app(app(node,x),xs)) | → | app#(app(map,height),xs) | (22) |
| app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (10) |
| app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (9) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(height,app(app(node,x),xs)) | → | app#(app(map,height),xs) | (22) |
| 2 | > | 2 | |
| app#(app(map,f),app(app(cons,x),xs)) | → | app#(f,x) | (10) |
| 2 | > | 2 | |
| 1 | > | 1 | |
| app#(app(map,f),app(app(cons,x),xs)) | → | app#(app(map,f),xs) | (9) |
| 2 | > | 2 | |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| app#(app(maxlist,x),app(app(cons,y),ys)) | → | app#(app(maxlist,y),ys) | (16) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(app(maxlist,x),app(app(cons,y),ys)) | → | app#(app(maxlist,y),ys) | (16) |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| app#(app(le,app(s,x)),app(s,y)) | → | app#(app(le,x),y) | (14) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| app#(app(le,app(s,x)),app(s,y)) | → | app#(app(le,x),y) | (14) |
| 2 | > | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.