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(treemap,f),app(app(node,x),xs)) | → | app(app(node,app(f,x)),app(app(map,app(treemap,f)),xs)) | (3) |
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) |
| treemap | is mapped to | treemap, | treemap1(x1), | treemap2(x1, x2) |
| node | is mapped to | node, | node1(x1), | node2(x1, x2) |
| map2(f,nil) | → | nil | (12) |
| map2(f,cons2(x,xs)) | → | cons2(app(f,x),map2(f,xs)) | (13) |
| treemap2(f,node2(x,xs)) | → | node2(app(f,x),map2(treemap1(f),xs)) | (14) |
| app(map,y1) | → | map1(y1) | (4) |
| app(map1(x0),y1) | → | map2(x0,y1) | (5) |
| app(cons,y1) | → | cons1(y1) | (6) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (7) |
| app(treemap,y1) | → | treemap1(y1) | (8) |
| app(treemap1(x0),y1) | → | treemap2(x0,y1) | (9) |
| app(node,y1) | → | node1(y1) | (10) |
| app(node1(x0),y1) | → | node2(x0,y1) | (11) |
| prec(map2) | = | 3 | stat(map2) | = | lex | |
| prec(nil) | = | 0 | stat(nil) | = | mul | |
| prec(cons2) | = | 1 | stat(cons2) | = | mul | |
| prec(app) | = | 3 | stat(app) | = | lex | |
| prec(treemap2) | = | 3 | stat(treemap2) | = | lex | |
| prec(node2) | = | 2 | stat(node2) | = | mul | |
| prec(treemap1) | = | 2 | stat(treemap1) | = | mul | |
| prec(map) | = | 4 | stat(map) | = | mul | |
| prec(map1) | = | 3 | stat(map1) | = | lex | |
| prec(cons) | = | 5 | stat(cons) | = | mul | |
| prec(cons1) | = | 3 | stat(cons1) | = | lex | |
| prec(treemap) | = | 6 | stat(treemap) | = | mul | |
| prec(node) | = | 7 | stat(node) | = | mul | |
| prec(node1) | = | 3 | stat(node1) | = | lex |
| π(map2) | = | [2,1] |
| π(nil) | = | [] |
| π(cons2) | = | [1,2] |
| π(app) | = | [2,1] |
| π(treemap2) | = | [2,1] |
| π(node2) | = | [1,2] |
| π(treemap1) | = | [1] |
| π(map) | = | [] |
| π(map1) | = | [1] |
| π(cons) | = | [] |
| π(cons1) | = | [1] |
| π(treemap) | = | [] |
| π(node) | = | [] |
| π(node1) | = | [1] |
| map2(f,nil) | → | nil | (12) |
| map2(f,cons2(x,xs)) | → | cons2(app(f,x),map2(f,xs)) | (13) |
| treemap2(f,node2(x,xs)) | → | node2(app(f,x),map2(treemap1(f),xs)) | (14) |
| app(map,y1) | → | map1(y1) | (4) |
| app(map1(x0),y1) | → | map2(x0,y1) | (5) |
| app(cons,y1) | → | cons1(y1) | (6) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (7) |
| app(treemap,y1) | → | treemap1(y1) | (8) |
| app(treemap1(x0),y1) | → | treemap2(x0,y1) | (9) |
| app(node,y1) | → | node1(y1) | (10) |
| app(node1(x0),y1) | → | node2(x0,y1) | (11) |
There are no rules in the TRS. Hence, it is terminating.