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