The rewrite relation of the following TRS is considered.
app(D,t) | → | 1 | (1) |
app(D,constant) | → | 0 | (2) |
app(D,app(app(+,x),y)) | → | app(app(+,app(D,x)),app(D,y)) | (3) |
app(D,app(app(*,x),y)) | → | app(app(+,app(app(*,y),app(D,x))),app(app(*,x),app(D,y))) | (4) |
app(D,app(app(-,x),y)) | → | app(app(-,app(D,x)),app(D,y)) | (5) |
app(app(map,f),nil) | → | nil | (6) |
app(app(map,f),app(app(cons,x),xs)) | → | app(app(cons,app(f,x)),app(app(map,f),xs)) | (7) |
app(app(filter,f),nil) | → | nil | (8) |
app(app(filter,f),app(app(cons,x),xs)) | → | app(app(app(app(filter2,app(f,x)),f),x),xs) | (9) |
app(app(app(app(filter2,true),f),x),xs) | → | app(app(cons,x),app(app(filter,f),xs)) | (10) |
app(app(app(app(filter2,false),f),x),xs) | → | app(app(filter,f),xs) | (11) |
We uncurry the binary symbol app in combination with the following symbol map which also determines the applicative arities of these symbols.
D | is mapped to | D, | D1(x1) | |||
t | is mapped to | t | ||||
1 | is mapped to | 1 | ||||
constant | is mapped to | constant | ||||
0 | is mapped to | 0 | ||||
+ | is mapped to | +, | +1(x1), | +2(x1, x2) | ||
* | is mapped to | *, | *1(x1), | *2(x1, x2) | ||
- | is mapped to | -, | -1(x1), | -2(x1, x2) | ||
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 |
D1(t) | → | 1 | (29) |
D1(constant) | → | 0 | (30) |
D1(+2(x,y)) | → | +2(D1(x),D1(y)) | (31) |
D1(*2(x,y)) | → | +2(*2(y,D1(x)),*2(x,D1(y))) | (32) |
D1(-2(x,y)) | → | -2(D1(x),D1(y)) | (33) |
map2(f,nil) | → | nil | (34) |
map2(f,cons2(x,xs)) | → | cons2(app(f,x),map2(f,xs)) | (35) |
filter3(f,nil) | → | nil | (36) |
filter3(f,cons2(x,xs)) | → | filter24(app(f,x),f,x,xs) | (37) |
filter24(true,f,x,xs) | → | cons2(x,filter3(f,xs)) | (38) |
filter24(false,f,x,xs) | → | filter3(f,xs) | (39) |
app(D,y1) | → | D1(y1) | (12) |
app(+,y1) | → | +1(y1) | (13) |
app(+1(x0),y1) | → | +2(x0,y1) | (14) |
app(*,y1) | → | *1(y1) | (15) |
app(*1(x0),y1) | → | *2(x0,y1) | (16) |
app(-,y1) | → | -1(y1) | (17) |
app(-1(x0),y1) | → | -2(x0,y1) | (18) |
app(map,y1) | → | map1(y1) | (19) |
app(map1(x0),y1) | → | map2(x0,y1) | (20) |
app(cons,y1) | → | cons1(y1) | (21) |
app(cons1(x0),y1) | → | cons2(x0,y1) | (22) |
app(filter,y1) | → | filter1(y1) | (23) |
app(filter1(x0),y1) | → | filter3(x0,y1) | (24) |
app(filter2,y1) | → | filter21(y1) | (25) |
app(filter21(x0),y1) | → | filter22(x0,y1) | (26) |
app(filter22(x0,x1),y1) | → | filter23(x0,x1,y1) | (27) |
app(filter23(x0,x1,x2),y1) | → | filter24(x0,x1,x2,y1) | (28) |
prec(D1) | = | 9 | stat(D1) | = | lex | |
prec(t) | = | 10 | stat(t) | = | mul | |
prec(1) | = | 1 | stat(1) | = | mul | |
prec(constant) | = | 12 | stat(constant) | = | mul | |
prec(0) | = | 11 | stat(0) | = | mul | |
prec(+2) | = | 2 | stat(+2) | = | mul | |
prec(*2) | = | 3 | stat(*2) | = | mul | |
prec(-2) | = | 4 | stat(-2) | = | mul | |
prec(map2) | = | 9 | stat(map2) | = | lex | |
prec(nil) | = | 13 | stat(nil) | = | mul | |
prec(cons2) | = | 5 | stat(cons2) | = | mul | |
prec(app) | = | 9 | stat(app) | = | lex | |
prec(filter3) | = | 9 | stat(filter3) | = | lex | |
prec(filter24) | = | 9 | stat(filter24) | = | lex | |
prec(true) | = | 14 | stat(true) | = | mul | |
prec(false) | = | 15 | stat(false) | = | mul | |
prec(D) | = | 16 | stat(D) | = | mul | |
prec(+) | = | 17 | stat(+) | = | mul | |
prec(+1) | = | 0 | stat(+1) | = | lex | |
prec(*) | = | 18 | stat(*) | = | mul | |
prec(-) | = | 19 | stat(-) | = | mul | |
prec(map) | = | 20 | stat(map) | = | mul | |
prec(map1) | = | 6 | stat(map1) | = | lex | |
prec(cons) | = | 21 | stat(cons) | = | mul | |
prec(filter) | = | 22 | stat(filter) | = | mul | |
prec(filter2) | = | 23 | stat(filter2) | = | mul | |
prec(filter21) | = | 9 | stat(filter21) | = | lex | |
prec(filter22) | = | 8 | stat(filter22) | = | mul | |
prec(filter23) | = | 7 | stat(filter23) | = | lex |
π(D1) | = | [1] |
π(t) | = | [] |
π(1) | = | [] |
π(constant) | = | [] |
π(0) | = | [] |
π(+2) | = | [1,2] |
π(*2) | = | [1,2] |
π(-2) | = | [1,2] |
π(map2) | = | [2,1] |
π(nil) | = | [] |
π(cons2) | = | [1,2] |
π(app) | = | [2,1] |
π(filter3) | = | [2,1] |
π(filter24) | = | [4,2,1,3] |
π(true) | = | [] |
π(false) | = | [] |
π(D) | = | [] |
π(+) | = | [] |
π(+1) | = | [1] |
π(*) | = | [] |
π(*1) | = | 1 |
π(-) | = | [] |
π(-1) | = | 1 |
π(map) | = | [] |
π(map1) | = | [1] |
π(cons) | = | [] |
π(cons1) | = | 1 |
π(filter) | = | [] |
π(filter1) | = | 1 |
π(filter2) | = | [] |
π(filter21) | = | [1] |
π(filter22) | = | [1,2] |
π(filter23) | = | [1,3,2] |
D1(t) | → | 1 | (29) |
D1(constant) | → | 0 | (30) |
D1(+2(x,y)) | → | +2(D1(x),D1(y)) | (31) |
D1(*2(x,y)) | → | +2(*2(y,D1(x)),*2(x,D1(y))) | (32) |
D1(-2(x,y)) | → | -2(D1(x),D1(y)) | (33) |
map2(f,nil) | → | nil | (34) |
map2(f,cons2(x,xs)) | → | cons2(app(f,x),map2(f,xs)) | (35) |
filter3(f,nil) | → | nil | (36) |
filter3(f,cons2(x,xs)) | → | filter24(app(f,x),f,x,xs) | (37) |
filter24(true,f,x,xs) | → | cons2(x,filter3(f,xs)) | (38) |
filter24(false,f,x,xs) | → | filter3(f,xs) | (39) |
app(D,y1) | → | D1(y1) | (12) |
app(+,y1) | → | +1(y1) | (13) |
app(+1(x0),y1) | → | +2(x0,y1) | (14) |
app(*,y1) | → | *1(y1) | (15) |
app(*1(x0),y1) | → | *2(x0,y1) | (16) |
app(-,y1) | → | -1(y1) | (17) |
app(-1(x0),y1) | → | -2(x0,y1) | (18) |
app(map,y1) | → | map1(y1) | (19) |
app(map1(x0),y1) | → | map2(x0,y1) | (20) |
app(cons,y1) | → | cons1(y1) | (21) |
app(cons1(x0),y1) | → | cons2(x0,y1) | (22) |
app(filter,y1) | → | filter1(y1) | (23) |
app(filter2,y1) | → | filter21(y1) | (25) |
app(filter21(x0),y1) | → | filter22(x0,y1) | (26) |
app(filter22(x0,x1),y1) | → | filter23(x0,x1,y1) | (27) |
app(filter23(x0,x1,x2),y1) | → | filter24(x0,x1,x2,y1) | (28) |
prec(filter1) | = | 0 | weight(filter1) | = | 1 | ||||
prec(app) | = | 2 | weight(app) | = | 0 | ||||
prec(filter3) | = | 1 | weight(filter3) | = | 1 |
app(filter1(x0),y1) | → | filter3(x0,y1) | (24) |
There are no rules in the TRS. Hence, it is terminating.