The rewrite relation of the following TRS is considered.
app(f,app(g,x)) | → | app(g,app(g,app(f,x))) | (1) |
app(f,app(g,x)) | → | app(g,app(g,app(g,x))) | (2) |
app(app(map,fun),nil) | → | nil | (3) |
app(app(map,fun),app(app(cons,x),xs)) | → | app(app(cons,app(fun,x)),app(app(map,fun),xs)) | (4) |
app(app(filter,fun),nil) | → | nil | (5) |
app(app(filter,fun),app(app(cons,x),xs)) | → | app(app(app(app(filter2,app(fun,x)),fun),x),xs) | (6) |
app(app(app(app(filter2,true),fun),x),xs) | → | app(app(cons,x),app(app(filter,fun),xs)) | (7) |
app(app(app(app(filter2,false),fun),x),xs) | → | app(app(filter,fun),xs) | (8) |
We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.
f | is mapped to | f, | f1(x1) | |||
g | is mapped to | g, | g1(x1) | |||
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 |
f1(g1(x)) | → | g1(g1(f1(x))) | (21) |
f1(g1(x)) | → | g1(g1(g1(x))) | (22) |
map2(fun,nil) | → | nil | (23) |
map2(fun,cons2(x,xs)) | → | cons2(app(fun,x),map2(fun,xs)) | (24) |
filter3(fun,nil) | → | nil | (25) |
filter3(fun,cons2(x,xs)) | → | filter24(app(fun,x),fun,x,xs) | (26) |
filter24(true,fun,x,xs) | → | cons2(x,filter3(fun,xs)) | (27) |
filter24(false,fun,x,xs) | → | filter3(fun,xs) | (28) |
app(f,y1) | → | f1(y1) | (9) |
app(g,y1) | → | g1(y1) | (10) |
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(filter,y1) | → | filter1(y1) | (15) |
app(filter1(x0),y1) | → | filter3(x0,y1) | (16) |
app(filter2,y1) | → | filter21(y1) | (17) |
app(filter21(x0),y1) | → | filter22(x0,y1) | (18) |
app(filter22(x0,x1),y1) | → | filter23(x0,x1,y1) | (19) |
app(filter23(x0,x1,x2),y1) | → | filter24(x0,x1,x2,y1) | (20) |
prec(f1) | = | 0 | stat(f1) | = | mul | |
prec(map2) | = | 1 | stat(map2) | = | lex | |
prec(nil) | = | 2 | stat(nil) | = | mul | |
prec(cons2) | = | 0 | stat(cons2) | = | mul | |
prec(app) | = | 1 | stat(app) | = | lex | |
prec(filter3) | = | 1 | stat(filter3) | = | lex | |
prec(filter24) | = | 1 | stat(filter24) | = | lex | |
prec(true) | = | 3 | stat(true) | = | mul | |
prec(false) | = | 4 | stat(false) | = | mul | |
prec(f) | = | 5 | stat(f) | = | mul | |
prec(g) | = | 6 | stat(g) | = | mul | |
prec(map) | = | 0 | stat(map) | = | mul | |
prec(map1) | = | 0 | stat(map1) | = | lex | |
prec(cons) | = | 0 | stat(cons) | = | mul | |
prec(cons1) | = | 0 | stat(cons1) | = | lex | |
prec(filter) | = | 7 | stat(filter) | = | mul | |
prec(filter2) | = | 8 | stat(filter2) | = | mul | |
prec(filter21) | = | 0 | stat(filter21) | = | lex | |
prec(filter22) | = | 0 | stat(filter22) | = | mul | |
prec(filter23) | = | 0 | stat(filter23) | = | lex |
π(f1) | = | [1] |
π(g1) | = | 1 |
π(map2) | = | [1,2] |
π(nil) | = | [] |
π(cons2) | = | [1,2] |
π(app) | = | [1,2] |
π(filter3) | = | [1,2] |
π(filter24) | = | [2,4,3,1] |
π(true) | = | [] |
π(false) | = | [] |
π(f) | = | [] |
π(g) | = | [] |
π(map) | = | [] |
π(map1) | = | [1] |
π(cons) | = | [] |
π(cons1) | = | [1] |
π(filter) | = | [] |
π(filter1) | = | 1 |
π(filter2) | = | [] |
π(filter21) | = | [1] |
π(filter22) | = | [1,2] |
π(filter23) | = | [3,1,2] |
f1(g1(x)) | → | g1(g1(g1(x))) | (22) |
map2(fun,nil) | → | nil | (23) |
map2(fun,cons2(x,xs)) | → | cons2(app(fun,x),map2(fun,xs)) | (24) |
filter3(fun,nil) | → | nil | (25) |
filter3(fun,cons2(x,xs)) | → | filter24(app(fun,x),fun,x,xs) | (26) |
filter24(true,fun,x,xs) | → | cons2(x,filter3(fun,xs)) | (27) |
filter24(false,fun,x,xs) | → | filter3(fun,xs) | (28) |
app(f,y1) | → | f1(y1) | (9) |
app(g,y1) | → | g1(y1) | (10) |
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(filter,y1) | → | filter1(y1) | (15) |
app(filter2,y1) | → | filter21(y1) | (17) |
app(filter21(x0),y1) | → | filter22(x0,y1) | (18) |
app(filter22(x0,x1),y1) | → | filter23(x0,x1,y1) | (19) |
app(filter23(x0,x1,x2),y1) | → | filter24(x0,x1,x2,y1) | (20) |
[f1(x1)] | = | 2 + 2 · x1 |
[g1(x1)] | = | 1 + 1 · x1 |
[app(x1, x2)] | = | 2 + 1 · x1 + 2 · x2 |
[filter1(x1)] | = | 2 + 2 · x1 |
[filter3(x1, x2)] | = | 2 · x1 + 2 · x2 |
app(filter1(x0),y1) | → | filter3(x0,y1) | (16) |
prec(f1) | = | 1 | stat(f1) | = | lex | |
prec(g1) | = | 0 | stat(g1) | = | lex |
π(f1) | = | [1] |
π(g1) | = | [1] |
f1(g1(x)) | → | g1(g1(f1(x))) | (21) |
There are no rules in the TRS. Hence, it is terminating.