The rewrite relation of the following TRS is considered.
app(app(:,app(app(:,app(app(:,app(app(:,C),x)),y)),z)),u) |
→ |
app(app(:,app(app(:,x),z)),app(app(:,app(app(:,app(app(:,x),y)),z)),u)) |
(1) |
app(app(map,f),nil) |
→ |
nil |
(2) |
app(app(map,f),app(app(cons,x),xs)) |
→ |
app(app(cons,app(f,x)),app(app(map,f),xs)) |
(3) |
app(app(filter,f),nil) |
→ |
nil |
(4) |
app(app(filter,f),app(app(cons,x),xs)) |
→ |
app(app(app(app(filter2,app(f,x)),f),x),xs) |
(5) |
app(app(app(app(filter2,true),f),x),xs) |
→ |
app(app(cons,x),app(app(filter,f),xs)) |
(6) |
app(app(app(app(filter2,false),f),x),xs) |
→ |
app(app(filter,f),xs) |
(7) |
:2(:2(:2(:2(C,x),y),z),u) |
→ |
:2(:2(x,z),:2(:2(:2(x,y),z),u)) |
(20) |
map2(f,nil) |
→ |
nil |
(21) |
map2(f,cons2(x,xs)) |
→ |
cons2(app(f,x),map2(f,xs)) |
(22) |
filter3(f,nil) |
→ |
nil |
(23) |
filter3(f,cons2(x,xs)) |
→ |
filter24(app(f,x),f,x,xs) |
(24) |
filter24(true,f,x,xs) |
→ |
cons2(x,filter3(f,xs)) |
(25) |
filter24(false,f,x,xs) |
→ |
filter3(f,xs) |
(26) |
app(:,y1) |
→ |
:1(y1) |
(8) |
app(:1(x0),y1) |
→ |
:2(x0,y1) |
(9) |
app(map,y1) |
→ |
map1(y1) |
(10) |
app(map1(x0),y1) |
→ |
map2(x0,y1) |
(11) |
app(cons,y1) |
→ |
cons1(y1) |
(12) |
app(cons1(x0),y1) |
→ |
cons2(x0,y1) |
(13) |
app(filter,y1) |
→ |
filter1(y1) |
(14) |
app(filter1(x0),y1) |
→ |
filter3(x0,y1) |
(15) |
app(filter2,y1) |
→ |
filter21(y1) |
(16) |
app(filter21(x0),y1) |
→ |
filter22(x0,y1) |
(17) |
app(filter22(x0,x1),y1) |
→ |
filter23(x0,x1,y1) |
(18) |
app(filter23(x0,x1,x2),y1) |
→ |
filter24(x0,x1,x2,y1) |
(19) |
:2(:2(:2(:2(C,x),y),z),u) |
→ |
:2(:2(x,z),:2(:2(:2(x,y),z),u)) |
(20) |
map2(f,nil) |
→ |
nil |
(21) |
map2(f,cons2(x,xs)) |
→ |
cons2(app(f,x),map2(f,xs)) |
(22) |
filter3(f,nil) |
→ |
nil |
(23) |
filter3(f,cons2(x,xs)) |
→ |
filter24(app(f,x),f,x,xs) |
(24) |
filter24(true,f,x,xs) |
→ |
cons2(x,filter3(f,xs)) |
(25) |
filter24(false,f,x,xs) |
→ |
filter3(f,xs) |
(26) |
app(:,y1) |
→ |
:1(y1) |
(8) |
app(:1(x0),y1) |
→ |
:2(x0,y1) |
(9) |
app(map,y1) |
→ |
map1(y1) |
(10) |
app(map1(x0),y1) |
→ |
map2(x0,y1) |
(11) |
app(cons,y1) |
→ |
cons1(y1) |
(12) |
app(cons1(x0),y1) |
→ |
cons2(x0,y1) |
(13) |
app(filter,y1) |
→ |
filter1(y1) |
(14) |
app(filter1(x0),y1) |
→ |
filter3(x0,y1) |
(15) |
app(filter2,y1) |
→ |
filter21(y1) |
(16) |
app(filter21(x0),y1) |
→ |
filter22(x0,y1) |
(17) |
app(filter22(x0,x1),y1) |
→ |
filter23(x0,x1,y1) |
(18) |
app(filter23(x0,x1,x2),y1) |
→ |
filter24(x0,x1,x2,y1) |
(19) |
There are no rules in the TRS. Hence, it is terminating.