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