The rewrite relation of the following TRS is considered.
app(f,app(app(cons,nil),y)) | → | y | (1) |
app(f,app(app(cons,app(f,app(app(cons,nil),y))),z)) | → | app(app(app(copy,n),y),z) | (2) |
app(app(app(copy,0),y),z) | → | app(f,z) | (3) |
app(app(app(copy,app(s,x)),y),z) | → | app(app(app(copy,x),y),app(app(cons,app(f,y)),z)) | (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) |
We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.
f | is mapped to | f, | f1(x1) | |||
cons | is mapped to | cons, | cons1(x1), | cons2(x1, x2) | ||
nil | is mapped to | nil | ||||
copy | is mapped to | copy, | copy1(x1), | copy2(x1, x2), | copy3(x1, x2, x3) | |
n | is mapped to | n | ||||
0 | is mapped to | 0 | ||||
s | is mapped to | s, | s1(x1) | |||
map | is mapped to | map, | map1(x1), | map2(x1, x2) | ||
filter | is mapped to | filter, | filter1(x1), | filter3(x1, x2) | ||
filter2 | is mapped to | filter2, | filter21(x1), | filter22(x1, x2), | filter23(x1, x2, x3), | filter24(x1,...,x4) |
true | is mapped to | true | ||||
false | is mapped to | false |
f1(cons2(nil,y)) | → | y | (26) |
f1(cons2(f1(cons2(nil,y)),z)) | → | copy3(n,y,z) | (27) |
copy3(0,y,z) | → | f1(z) | (28) |
copy3(s1(x),y,z) | → | copy3(x,y,cons2(f1(y),z)) | (29) |
map2(fun,nil) | → | nil | (30) |
map2(fun,cons2(x,xs)) | → | cons2(app(fun,x),map2(fun,xs)) | (31) |
filter3(fun,nil) | → | nil | (32) |
filter3(fun,cons2(x,xs)) | → | filter24(app(fun,x),fun,x,xs) | (33) |
filter24(true,fun,x,xs) | → | cons2(x,filter3(fun,xs)) | (34) |
filter24(false,fun,x,xs) | → | filter3(fun,xs) | (35) |
app(f,y1) | → | f1(y1) | (11) |
app(cons,y1) | → | cons1(y1) | (12) |
app(cons1(x0),y1) | → | cons2(x0,y1) | (13) |
app(copy,y1) | → | copy1(y1) | (14) |
app(copy1(x0),y1) | → | copy2(x0,y1) | (15) |
app(copy2(x0,x1),y1) | → | copy3(x0,x1,y1) | (16) |
app(s,y1) | → | s1(y1) | (17) |
app(map,y1) | → | map1(y1) | (18) |
app(map1(x0),y1) | → | map2(x0,y1) | (19) |
app(filter,y1) | → | filter1(y1) | (20) |
app(filter1(x0),y1) | → | filter3(x0,y1) | (21) |
app(filter2,y1) | → | filter21(y1) | (22) |
app(filter21(x0),y1) | → | filter22(x0,y1) | (23) |
app(filter22(x0,x1),y1) | → | filter23(x0,x1,y1) | (24) |
app(filter23(x0,x1,x2),y1) | → | filter24(x0,x1,x2,y1) | (25) |
f1#(cons2(f1(cons2(nil,y)),z)) | → | copy3#(n,y,z) | (36) |
copy3#(0,y,z) | → | f1#(z) | (37) |
copy3#(s1(x),y,z) | → | copy3#(x,y,cons2(f1(y),z)) | (38) |
copy3#(s1(x),y,z) | → | f1#(y) | (39) |
map2#(fun,cons2(x,xs)) | → | app#(fun,x) | (40) |
map2#(fun,cons2(x,xs)) | → | map2#(fun,xs) | (41) |
filter3#(fun,cons2(x,xs)) | → | filter24#(app(fun,x),fun,x,xs) | (42) |
filter3#(fun,cons2(x,xs)) | → | app#(fun,x) | (43) |
filter24#(true,fun,x,xs) | → | filter3#(fun,xs) | (44) |
filter24#(false,fun,x,xs) | → | filter3#(fun,xs) | (45) |
app#(f,y1) | → | f1#(y1) | (46) |
app#(copy2(x0,x1),y1) | → | copy3#(x0,x1,y1) | (47) |
app#(map1(x0),y1) | → | map2#(x0,y1) | (48) |
app#(filter1(x0),y1) | → | filter3#(x0,y1) | (49) |
app#(filter23(x0,x1,x2),y1) | → | filter24#(x0,x1,x2,y1) | (50) |
The dependency pairs are split into 2 components.
app#(map1(x0),y1) | → | map2#(x0,y1) | (48) |
map2#(fun,cons2(x,xs)) | → | app#(fun,x) | (40) |
app#(filter1(x0),y1) | → | filter3#(x0,y1) | (49) |
filter3#(fun,cons2(x,xs)) | → | filter24#(app(fun,x),fun,x,xs) | (42) |
filter24#(true,fun,x,xs) | → | filter3#(fun,xs) | (44) |
filter3#(fun,cons2(x,xs)) | → | app#(fun,x) | (43) |
app#(filter23(x0,x1,x2),y1) | → | filter24#(x0,x1,x2,y1) | (50) |
filter24#(false,fun,x,xs) | → | filter3#(fun,xs) | (45) |
map2#(fun,cons2(x,xs)) | → | map2#(fun,xs) | (41) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
map2#(fun,cons2(x,xs)) | → | app#(fun,x) | (40) |
1 | ≥ | 1 | |
2 | > | 2 | |
map2#(fun,cons2(x,xs)) | → | map2#(fun,xs) | (41) |
1 | ≥ | 1 | |
2 | > | 2 | |
filter3#(fun,cons2(x,xs)) | → | app#(fun,x) | (43) |
1 | ≥ | 1 | |
2 | > | 2 | |
app#(map1(x0),y1) | → | map2#(x0,y1) | (48) |
1 | > | 1 | |
2 | ≥ | 2 | |
filter3#(fun,cons2(x,xs)) | → | filter24#(app(fun,x),fun,x,xs) | (42) |
1 | ≥ | 2 | |
2 | > | 3 | |
2 | > | 4 | |
app#(filter1(x0),y1) | → | filter3#(x0,y1) | (49) |
1 | > | 1 | |
2 | ≥ | 2 | |
app#(filter23(x0,x1,x2),y1) | → | filter24#(x0,x1,x2,y1) | (50) |
1 | > | 1 | |
1 | > | 2 | |
1 | > | 3 | |
2 | ≥ | 4 | |
filter24#(true,fun,x,xs) | → | filter3#(fun,xs) | (44) |
2 | ≥ | 1 | |
4 | ≥ | 2 | |
filter24#(false,fun,x,xs) | → | filter3#(fun,xs) | (45) |
2 | ≥ | 1 | |
4 | ≥ | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
copy3#(s1(x),y,z) | → | copy3#(x,y,cons2(f1(y),z)) | (38) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
copy3#(s1(x),y,z) | → | copy3#(x,y,cons2(f1(y),z)) | (38) |
1 | > | 1 | |
2 | ≥ | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.