The rewrite relation of the following TRS is considered.
| app(app(mapt,f),app(leaf,x)) | → | app(leaf,app(f,x)) | (1) |
| app(app(mapt,f),app(node,xs)) | → | app(node,app(app(maptlist,f),xs)) | (2) |
| app(app(maptlist,f),nil) | → | nil | (3) |
| app(app(maptlist,f),app(app(cons,x),xs)) | → | app(app(cons,app(app(mapt,f),x)),app(app(maptlist,f),xs)) | (4) |
We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.
| mapt | is mapped to | mapt, | mapt1(x1), | mapt2(x1, x2) |
| leaf | is mapped to | leaf, | leaf1(x1) | |
| node | is mapped to | node, | node1(x1) | |
| maptlist | is mapped to | maptlist, | maptlist1(x1), | maptlist2(x1, x2) |
| nil | is mapped to | nil | ||
| cons | is mapped to | cons, | cons1(x1), | cons2(x1, x2) |
| mapt2(f,leaf1(x)) | → | leaf1(app(f,x)) | (13) |
| mapt2(f,node1(xs)) | → | node1(maptlist2(f,xs)) | (14) |
| maptlist2(f,nil) | → | nil | (15) |
| maptlist2(f,cons2(x,xs)) | → | cons2(mapt2(f,x),maptlist2(f,xs)) | (16) |
| app(mapt,y1) | → | mapt1(y1) | (5) |
| app(mapt1(x0),y1) | → | mapt2(x0,y1) | (6) |
| app(leaf,y1) | → | leaf1(y1) | (7) |
| app(node,y1) | → | node1(y1) | (8) |
| app(maptlist,y1) | → | maptlist1(y1) | (9) |
| app(maptlist1(x0),y1) | → | maptlist2(x0,y1) | (10) |
| app(cons,y1) | → | cons1(y1) | (11) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (12) |
| prec(mapt2) | = | 4 | stat(mapt2) | = | mul | |
| prec(app) | = | 4 | stat(app) | = | mul | |
| prec(maptlist2) | = | 4 | stat(maptlist2) | = | mul | |
| prec(nil) | = | 0 | stat(nil) | = | mul | |
| prec(cons2) | = | 1 | stat(cons2) | = | mul | |
| prec(mapt) | = | 5 | stat(mapt) | = | mul | |
| prec(mapt1) | = | 2 | stat(mapt1) | = | mul | |
| prec(leaf) | = | 6 | stat(leaf) | = | mul | |
| prec(node) | = | 7 | stat(node) | = | mul | |
| prec(maptlist) | = | 8 | stat(maptlist) | = | mul | |
| prec(maptlist1) | = | 3 | stat(maptlist1) | = | mul | |
| prec(cons) | = | 9 | stat(cons) | = | mul |
| π(mapt2) | = | [1,2] |
| π(leaf1) | = | 1 |
| π(app) | = | [1,2] |
| π(node1) | = | 1 |
| π(maptlist2) | = | [1,2] |
| π(nil) | = | [] |
| π(cons2) | = | [1,2] |
| π(mapt) | = | [] |
| π(mapt1) | = | [1] |
| π(leaf) | = | [] |
| π(node) | = | [] |
| π(maptlist) | = | [] |
| π(maptlist1) | = | [1] |
| π(cons) | = | [] |
| π(cons1) | = | 1 |
| maptlist2(f,nil) | → | nil | (15) |
| maptlist2(f,cons2(x,xs)) | → | cons2(mapt2(f,x),maptlist2(f,xs)) | (16) |
| app(mapt,y1) | → | mapt1(y1) | (5) |
| app(mapt1(x0),y1) | → | mapt2(x0,y1) | (6) |
| app(leaf,y1) | → | leaf1(y1) | (7) |
| app(node,y1) | → | node1(y1) | (8) |
| app(maptlist,y1) | → | maptlist1(y1) | (9) |
| app(maptlist1(x0),y1) | → | maptlist2(x0,y1) | (10) |
| app(cons,y1) | → | cons1(y1) | (11) |
| app(cons1(x0),y1) | → | cons2(x0,y1) | (12) |
| prec(leaf1) | = | 0 | weight(leaf1) | = | 1 | ||||
| prec(node1) | = | 2 | weight(node1) | = | 1 | ||||
| prec(mapt2) | = | 3 | weight(mapt2) | = | 0 | ||||
| prec(app) | = | 1 | weight(app) | = | 0 | ||||
| prec(maptlist2) | = | 4 | weight(maptlist2) | = | 0 |
| mapt2(f,leaf1(x)) | → | leaf1(app(f,x)) | (13) |
| mapt2(f,node1(xs)) | → | node1(maptlist2(f,xs)) | (14) |
There are no rules in the TRS. Hence, it is terminating.