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(minus,x),0) | → | x | (3) |
| app(app(minus,app(s,x)),app(s,y)) | → | app(app(minus,app(p,app(s,x))),app(p,app(s,y))) | (4) |
| app(p,app(s,x)) | → | x | (5) |
| app(app(div,0),app(s,y)) | → | 0 | (6) |
| app(app(div,app(s,x)),app(s,y)) | → | app(s,app(app(div,app(app(minus,x),app(id,y))),app(s,y))) | (7) |
| app(id,x) | → | x | (8) |
| app(id,x) | → | app(s,app(s,app(s,x))) | (9) |
| app(id,app(p,x)) | → | app(id,app(s,app(id,x))) | (10) |
We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.
| 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) |
| minus | is mapped to | minus, | minus1(x1), | minus2(x1, x2) |
| 0 | is mapped to | 0 | ||
| s | is mapped to | s, | s1(x1) | |
| p | is mapped to | p, | p1(x1) | |
| div | is mapped to | div, | div1(x1), | div2(x1, x2) |
| id | is mapped to | id, | id1(x1) |
| map2(f,nil) | → | nil | (22) |
| map2(f,cons2(x,xs)) | → | cons2(app(f,x),map2(f,xs)) | (23) |
| minus2(x,0) | → | x | (24) |
| minus2(s1(x),s1(y)) | → | minus2(p1(s1(x)),p1(s1(y))) | (25) |
| p1(s1(x)) | → | x | (26) |
| div2(0,s1(y)) | → | 0 | (27) |
| div2(s1(x),s1(y)) | → | s1(div2(minus2(x,id1(y)),s1(y))) | (28) |
| id1(x) | → | x | (29) |
| id1(x) | → | s1(s1(s1(x))) | (30) |
| id1(p1(x)) | → | id1(s1(id1(x))) | (31) |
| app(map,y1) | → | map1(y1) | (11) |
| app(map1(x0),y1) | → | map2(x0,y1) | (12) |
| app(cons,y1) | → | cons1(y1) | (13) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (14) |
| app(minus,y1) | → | minus1(y1) | (15) |
| app(minus1(x0),y1) | → | minus2(x0,y1) | (16) |
| app(s,y1) | → | s1(y1) | (17) |
| app(p,y1) | → | p1(y1) | (18) |
| app(div,y1) | → | div1(y1) | (19) |
| app(div1(x0),y1) | → | div2(x0,y1) | (20) |
| app(id,y1) | → | id1(y1) | (21) |
| map2#(f,cons2(x,xs)) | → | app#(f,x) | (32) |
| map2#(f,cons2(x,xs)) | → | map2#(f,xs) | (33) |
| minus2#(s1(x),s1(y)) | → | minus2#(p1(s1(x)),p1(s1(y))) | (34) |
| minus2#(s1(x),s1(y)) | → | p1#(s1(x)) | (35) |
| minus2#(s1(x),s1(y)) | → | p1#(s1(y)) | (36) |
| div2#(s1(x),s1(y)) | → | div2#(minus2(x,id1(y)),s1(y)) | (37) |
| div2#(s1(x),s1(y)) | → | minus2#(x,id1(y)) | (38) |
| div2#(s1(x),s1(y)) | → | id1#(y) | (39) |
| id1#(p1(x)) | → | id1#(s1(id1(x))) | (40) |
| id1#(p1(x)) | → | id1#(x) | (41) |
| app#(map1(x0),y1) | → | map2#(x0,y1) | (42) |
| app#(minus1(x0),y1) | → | minus2#(x0,y1) | (43) |
| app#(p,y1) | → | p1#(y1) | (44) |
| app#(div1(x0),y1) | → | div2#(x0,y1) | (45) |
| app#(id,y1) | → | id1#(y1) | (46) |
The dependency pairs are split into 4 components.
| app#(map1(x0),y1) | → | map2#(x0,y1) | (42) |
| map2#(f,cons2(x,xs)) | → | app#(f,x) | (32) |
| map2#(f,cons2(x,xs)) | → | map2#(f,xs) | (33) |
| [map1(x1)] | = | 1 · x1 |
| [cons2(x1, x2)] | = | 1 · x1 + 1 · x2 |
| [map2#(x1, x2)] | = | 1 · x1 + 1 · x2 |
| [app#(x1, x2)] | = | 1 · x1 + 1 · x2 |
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) | (32) |
| 1 | ≥ | 1 | |
| 2 | > | 2 | |
| map2#(f,cons2(x,xs)) | → | map2#(f,xs) | (33) |
| 1 | ≥ | 1 | |
| 2 | > | 2 | |
| app#(map1(x0),y1) | → | map2#(x0,y1) | (42) |
| 1 | > | 1 | |
| 2 | ≥ | 2 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| div2#(s1(x),s1(y)) | → | div2#(minus2(x,id1(y)),s1(y)) | (37) |
| prec(s1) | = | 1 | weight(s1) | = | 1 |
| π(div2#) | = | 1 |
| π(s1) | = | [1] |
| π(minus2) | = | 1 |
| π(p1) | = | 1 |
| minus2(x,0) | → | x | (24) |
| minus2(s1(x),s1(y)) | → | minus2(p1(s1(x)),p1(s1(y))) | (25) |
| p1(s1(x)) | → | x | (26) |
| div2#(s1(x),s1(y)) | → | div2#(minus2(x,id1(y)),s1(y)) | (37) |
There are no pairs anymore.
| minus2#(s1(x),s1(y)) | → | minus2#(p1(s1(x)),p1(s1(y))) | (34) |
| [p1(x1)] | = | 1 · x1 |
| [s1(x1)] | = | 1 · x1 |
| [minus2#(x1, x2)] | = | 1 · x1 + 1 · x2 |
| p1(s1(x)) | → | x | (26) |
20
Hence, it suffices to show innermost termination in the following.| [p1(x1)] | = | 1 · x1 |
| [s1(x1)] | = | 2 + 2 · x1 |
| [minus2#(x1, x2)] | = | 2 · x1 + 2 · x2 |
| p1(s1(x)) | → | x | (26) |
| prec(s1) | = | 1 | weight(s1) | = | 1 | ||||
| prec(p1) | = | 0 | weight(p1) | = | 1 |
| π(minus2#) | = | 2 |
| π(s1) | = | [] |
| π(p1) | = | [] |
| minus2#(s1(x),s1(y)) | → | minus2#(p1(s1(x)),p1(s1(y))) | (34) |
There are no pairs anymore.
| id1#(p1(x)) | → | id1#(x) | (41) |
| [p1(x1)] | = | 1 · x1 |
| [id1#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| id1#(p1(x)) | → | id1#(x) | (41) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.