The rewrite relation of the following TRS is considered.
app(f,app(s,x)) | → | app(f,x) | (1) |
app(g,app(app(cons,0),y)) | → | app(g,y) | (2) |
app(g,app(app(cons,app(s,x)),y)) | → | app(s,x) | (3) |
app(h,app(app(cons,x),y)) | → | app(h,app(g,app(app(cons,x),y))) | (4) |
app(app(map,fun),nil) | → | nil | (5) |
app(app(map,fun),app(app(cons,x),xs)) | → | app(app(cons,app(fun,x)),app(app(map,fun),xs)) | (6) |
app(app(filter,fun),nil) | → | nil | (7) |
app(app(filter,fun),app(app(cons,x),xs)) | → | app(app(app(app(filter2,app(fun,x)),fun),x),xs) | (8) |
app(app(app(app(filter2,true),fun),x),xs) | → | app(app(cons,x),app(app(filter,fun),xs)) | (9) |
app(app(app(app(filter2,false),fun),x),xs) | → | app(app(filter,fun),xs) | (10) |
app#(f,app(s,x)) | → | app#(f,x) | (11) |
app#(g,app(app(cons,0),y)) | → | app#(g,y) | (12) |
app#(h,app(app(cons,x),y)) | → | app#(g,app(app(cons,x),y)) | (13) |
app#(h,app(app(cons,x),y)) | → | app#(h,app(g,app(app(cons,x),y))) | (14) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(map,fun),xs) | (15) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (16) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(cons,app(fun,x)) | (17) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(cons,app(fun,x)),app(app(map,fun),xs)) | (18) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (19) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(filter2,app(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#(app(app(filter2,app(fun,x)),fun),x) | (22) |
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(app(app(app(filter2,app(fun,x)),fun),x),xs) | (23) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(filter,fun) | (24) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(filter,fun),xs) | (25) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(cons,x) | (26) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(cons,x),app(app(filter,fun),xs)) | (27) |
app#(app(app(app(filter2,false),fun),x),xs) | → | app#(filter,fun) | (28) |
app#(app(app(app(filter2,false),fun),x),xs) | → | app#(app(filter,fun),xs) | (29) |
The dependency pairs are split into 4 components.
app#(app(filter,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (19) |
app#(app(app(app(filter2,false),fun),x),xs) | → | app#(app(filter,fun),xs) | (29) |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(filter,fun),xs) | (25) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (16) |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(map,fun),xs) | (15) |
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) | (19) |
2 | > | 2 | |
1 | > | 1 | |
app#(app(app(app(filter2,false),fun),x),xs) | → | app#(app(filter,fun),xs) | (29) |
2 | ≥ | 2 | |
app#(app(app(app(filter2,true),fun),x),xs) | → | app#(app(filter,fun),xs) | (25) |
2 | ≥ | 2 | |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(fun,x) | (16) |
2 | > | 2 | |
1 | > | 1 | |
app#(app(map,fun),app(app(cons,x),xs)) | → | app#(app(map,fun),xs) | (15) |
2 | > | 2 | |
1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
app#(f,app(s,x)) | → | app#(f,x) | (11) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
app#(f,app(s,x)) | → | app#(f,x) | (11) |
2 | > | 2 | |
1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
app#(h,app(app(cons,x),y)) | → | app#(h,app(g,app(app(cons,x),y))) | (14) |
prec(app#) | = | 0 | stat(app#) | = | lex | |
prec(h) | = | 0 | stat(h) | = | lex | |
prec(0) | = | 0 | stat(0) | = | lex | |
prec(cons) | = | 3 | stat(cons) | = | lex | |
prec(g) | = | 2 | stat(g) | = | lex | |
prec(app) | = | 0 | stat(app) | = | lex | |
prec(s) | = | 0 | stat(s) | = | lex |
π(app#) | = | 2 |
π(h) | = | [] |
π(0) | = | [] |
π(cons) | = | [] |
π(g) | = | [] |
π(app) | = | 1 |
π(s) | = | [] |
app(g,app(app(cons,0),y)) | → | app(g,y) | (2) |
app(g,app(app(cons,app(s,x)),y)) | → | app(s,x) | (3) |
app#(h,app(app(cons,x),y)) | → | app#(h,app(g,app(app(cons,x),y))) | (14) |
There are no pairs anymore.
app#(g,app(app(cons,0),y)) | → | app#(g,y) | (12) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
app#(g,app(app(cons,0),y)) | → | app#(g,y) | (12) |
2 | > | 2 | |
1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.