The rewrite relation of the following TRS is considered.
app(app(append,nil),ys) | → | ys | (1) |
app(app(append,app(app(cons,x),xs)),ys) | → | app(app(cons,x),app(app(append,xs),ys)) | (2) |
app(app(flatwith,f),app(leaf,x)) | → | app(app(cons,app(f,x)),nil) | (3) |
app(app(flatwith,f),app(node,xs)) | → | app(app(flatwithsub,f),xs) | (4) |
app(app(flatwithsub,f),nil) | → | nil | (5) |
app(app(flatwithsub,f),app(app(cons,x),xs)) | → | app(app(append,app(app(flatwith,f),x)),app(app(flatwithsub,f),xs)) | (6) |
We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.
append | is mapped to | append, | append1(x1), | append2(x1, x2) |
nil | is mapped to | nil | ||
cons | is mapped to | cons, | cons1(x1), | cons2(x1, x2) |
flatwith | is mapped to | flatwith, | flatwith1(x1), | flatwith2(x1, x2) |
leaf | is mapped to | leaf, | leaf1(x1) | |
node | is mapped to | node, | node1(x1) | |
flatwithsub | is mapped to | flatwithsub, | flatwithsub1(x1), | flatwithsub2(x1, x2) |
append2(nil,ys) | → | ys | (17) |
append2(cons2(x,xs),ys) | → | cons2(x,append2(xs,ys)) | (18) |
flatwith2(f,leaf1(x)) | → | cons2(app(f,x),nil) | (19) |
flatwith2(f,node1(xs)) | → | flatwithsub2(f,xs) | (20) |
flatwithsub2(f,nil) | → | nil | (21) |
flatwithsub2(f,cons2(x,xs)) | → | append2(flatwith2(f,x),flatwithsub2(f,xs)) | (22) |
app(append,y1) | → | append1(y1) | (7) |
app(append1(x0),y1) | → | append2(x0,y1) | (8) |
app(cons,y1) | → | cons1(y1) | (9) |
app(cons1(x0),y1) | → | cons2(x0,y1) | (10) |
app(flatwith,y1) | → | flatwith1(y1) | (11) |
app(flatwith1(x0),y1) | → | flatwith2(x0,y1) | (12) |
app(leaf,y1) | → | leaf1(y1) | (13) |
app(node,y1) | → | node1(y1) | (14) |
app(flatwithsub,y1) | → | flatwithsub1(y1) | (15) |
app(flatwithsub1(x0),y1) | → | flatwithsub2(x0,y1) | (16) |
prec(append2) | = | 2 | stat(append2) | = | mul | |
prec(nil) | = | 3 | stat(nil) | = | mul | |
prec(cons2) | = | 1 | stat(cons2) | = | mul | |
prec(flatwith2) | = | 4 | stat(flatwith2) | = | mul | |
prec(leaf1) | = | 3 | stat(leaf1) | = | mul | |
prec(app) | = | 4 | stat(app) | = | mul | |
prec(node1) | = | 0 | stat(node1) | = | mul | |
prec(flatwithsub2) | = | 4 | stat(flatwithsub2) | = | mul | |
prec(append) | = | 5 | stat(append) | = | mul | |
prec(cons) | = | 6 | stat(cons) | = | mul | |
prec(cons1) | = | 0 | stat(cons1) | = | mul | |
prec(flatwith) | = | 7 | stat(flatwith) | = | mul | |
prec(flatwith1) | = | 4 | stat(flatwith1) | = | mul | |
prec(leaf) | = | 3 | stat(leaf) | = | mul | |
prec(node) | = | 8 | stat(node) | = | mul | |
prec(flatwithsub) | = | 0 | stat(flatwithsub) | = | mul | |
prec(flatwithsub1) | = | 0 | stat(flatwithsub1) | = | mul |
π(append2) | = | [1,2] |
π(nil) | = | [] |
π(cons2) | = | [1,2] |
π(flatwith2) | = | [1,2] |
π(leaf1) | = | [1] |
π(app) | = | [1,2] |
π(node1) | = | [1] |
π(flatwithsub2) | = | [1,2] |
π(append) | = | [] |
π(append1) | = | 1 |
π(cons) | = | [] |
π(cons1) | = | [1] |
π(flatwith) | = | [] |
π(flatwith1) | = | [1] |
π(leaf) | = | [] |
π(node) | = | [] |
π(flatwithsub) | = | [] |
π(flatwithsub1) | = | [1] |
append2(nil,ys) | → | ys | (17) |
append2(cons2(x,xs),ys) | → | cons2(x,append2(xs,ys)) | (18) |
flatwith2(f,leaf1(x)) | → | cons2(app(f,x),nil) | (19) |
flatwith2(f,node1(xs)) | → | flatwithsub2(f,xs) | (20) |
flatwithsub2(f,nil) | → | nil | (21) |
flatwithsub2(f,cons2(x,xs)) | → | append2(flatwith2(f,x),flatwithsub2(f,xs)) | (22) |
app(append,y1) | → | append1(y1) | (7) |
app(append1(x0),y1) | → | append2(x0,y1) | (8) |
app(cons,y1) | → | cons1(y1) | (9) |
app(cons1(x0),y1) | → | cons2(x0,y1) | (10) |
app(flatwith,y1) | → | flatwith1(y1) | (11) |
app(flatwith1(x0),y1) | → | flatwith2(x0,y1) | (12) |
app(leaf,y1) | → | leaf1(y1) | (13) |
app(node,y1) | → | node1(y1) | (14) |
app(flatwithsub,y1) | → | flatwithsub1(y1) | (15) |
app(flatwithsub1(x0),y1) | → | flatwithsub2(x0,y1) | (16) |
There are no rules in the TRS. Hence, it is terminating.