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(D,app(minus,x)) |
→ |
app(minus,app(D,x)) |
(6) |
app(D,app(app(div,x),y)) |
→ |
app(app(-,app(app(div,app(D,x)),y)),app(app(div,app(app(*,x),app(D,y))),app(app(pow,y),2))) |
(7) |
app(D,app(ln,x)) |
→ |
app(app(div,app(D,x)),x) |
(8) |
app(D,app(app(pow,x),y)) |
→ |
app(app(+,app(app(*,app(app(*,y),app(app(pow,x),app(app(-,y),1)))),app(D,x))),app(app(*,app(app(*,app(app(pow,x),y)),app(ln,x))),app(D,y))) |
(9) |
app(app(map,f),nil) |
→ |
nil |
(10) |
app(app(map,f),app(app(cons,x),xs)) |
→ |
app(app(cons,app(f,x)),app(app(map,f),xs)) |
(11) |
app(app(filter,f),nil) |
→ |
nil |
(12) |
app(app(filter,f),app(app(cons,x),xs)) |
→ |
app(app(app(app(filter2,app(f,x)),f),x),xs) |
(13) |
app(app(app(app(filter2,true),f),x),xs) |
→ |
app(app(cons,x),app(app(filter,f),xs)) |
(14) |
app(app(app(app(filter2,false),f),x),xs) |
→ |
app(app(filter,f),xs) |
(15) |
D1(t) |
→ |
1 |
(39) |
D1(constant) |
→ |
0 |
(40) |
D1(+2(x,y)) |
→ |
+2(D1(x),D1(y)) |
(41) |
D1(*2(x,y)) |
→ |
+2(*2(y,D1(x)),*2(x,D1(y))) |
(42) |
D1(-2(x,y)) |
→ |
-2(D1(x),D1(y)) |
(43) |
D1(minus1(x)) |
→ |
minus1(D1(x)) |
(44) |
D1(div2(x,y)) |
→ |
-2(div2(D1(x),y),div2(*2(x,D1(y)),pow2(y,2))) |
(45) |
D1(ln1(x)) |
→ |
div2(D1(x),x) |
(46) |
D1(pow2(x,y)) |
→ |
+2(*2(*2(y,pow2(x,-2(y,1))),D1(x)),*2(*2(pow2(x,y),ln1(x)),D1(y))) |
(47) |
map2(f,nil) |
→ |
nil |
(48) |
map2(f,cons2(x,xs)) |
→ |
cons2(app(f,x),map2(f,xs)) |
(49) |
filter3(f,nil) |
→ |
nil |
(50) |
filter3(f,cons2(x,xs)) |
→ |
filter24(app(f,x),f,x,xs) |
(51) |
filter24(true,f,x,xs) |
→ |
cons2(x,filter3(f,xs)) |
(52) |
filter24(false,f,x,xs) |
→ |
filter3(f,xs) |
(53) |
app(D,y1) |
→ |
D1(y1) |
(16) |
app(+,y1) |
→ |
+1(y1) |
(17) |
app(+1(x0),y1) |
→ |
+2(x0,y1) |
(18) |
app(*,y1) |
→ |
*1(y1) |
(19) |
app(*1(x0),y1) |
→ |
*2(x0,y1) |
(20) |
app(-,y1) |
→ |
-1(y1) |
(21) |
app(-1(x0),y1) |
→ |
-2(x0,y1) |
(22) |
app(minus,y1) |
→ |
minus1(y1) |
(23) |
app(div,y1) |
→ |
div1(y1) |
(24) |
app(div1(x0),y1) |
→ |
div2(x0,y1) |
(25) |
app(pow,y1) |
→ |
pow1(y1) |
(26) |
app(pow1(x0),y1) |
→ |
pow2(x0,y1) |
(27) |
app(ln,y1) |
→ |
ln1(y1) |
(28) |
app(map,y1) |
→ |
map1(y1) |
(29) |
app(map1(x0),y1) |
→ |
map2(x0,y1) |
(30) |
app(cons,y1) |
→ |
cons1(y1) |
(31) |
app(cons1(x0),y1) |
→ |
cons2(x0,y1) |
(32) |
app(filter,y1) |
→ |
filter1(y1) |
(33) |
app(filter1(x0),y1) |
→ |
filter3(x0,y1) |
(34) |
app(filter2,y1) |
→ |
filter21(y1) |
(35) |
app(filter21(x0),y1) |
→ |
filter22(x0,y1) |
(36) |
app(filter22(x0,x1),y1) |
→ |
filter23(x0,x1,y1) |
(37) |
app(filter23(x0,x1,x2),y1) |
→ |
filter24(x0,x1,x2,y1) |
(38) |
D1(t) |
→ |
1 |
(39) |
D1(constant) |
→ |
0 |
(40) |
D1(+2(x,y)) |
→ |
+2(D1(x),D1(y)) |
(41) |
D1(*2(x,y)) |
→ |
+2(*2(y,D1(x)),*2(x,D1(y))) |
(42) |
D1(-2(x,y)) |
→ |
-2(D1(x),D1(y)) |
(43) |
D1(div2(x,y)) |
→ |
-2(div2(D1(x),y),div2(*2(x,D1(y)),pow2(y,2))) |
(45) |
D1(ln1(x)) |
→ |
div2(D1(x),x) |
(46) |
D1(pow2(x,y)) |
→ |
+2(*2(*2(y,pow2(x,-2(y,1))),D1(x)),*2(*2(pow2(x,y),ln1(x)),D1(y))) |
(47) |
map2(f,nil) |
→ |
nil |
(48) |
map2(f,cons2(x,xs)) |
→ |
cons2(app(f,x),map2(f,xs)) |
(49) |
filter3(f,nil) |
→ |
nil |
(50) |
filter3(f,cons2(x,xs)) |
→ |
filter24(app(f,x),f,x,xs) |
(51) |
filter24(true,f,x,xs) |
→ |
cons2(x,filter3(f,xs)) |
(52) |
filter24(false,f,x,xs) |
→ |
filter3(f,xs) |
(53) |
app(D,y1) |
→ |
D1(y1) |
(16) |
app(+,y1) |
→ |
+1(y1) |
(17) |
app(+1(x0),y1) |
→ |
+2(x0,y1) |
(18) |
app(*,y1) |
→ |
*1(y1) |
(19) |
app(*1(x0),y1) |
→ |
*2(x0,y1) |
(20) |
app(-,y1) |
→ |
-1(y1) |
(21) |
app(-1(x0),y1) |
→ |
-2(x0,y1) |
(22) |
app(minus,y1) |
→ |
minus1(y1) |
(23) |
app(div,y1) |
→ |
div1(y1) |
(24) |
app(div1(x0),y1) |
→ |
div2(x0,y1) |
(25) |
app(pow,y1) |
→ |
pow1(y1) |
(26) |
app(pow1(x0),y1) |
→ |
pow2(x0,y1) |
(27) |
app(ln,y1) |
→ |
ln1(y1) |
(28) |
app(map,y1) |
→ |
map1(y1) |
(29) |
app(map1(x0),y1) |
→ |
map2(x0,y1) |
(30) |
app(cons,y1) |
→ |
cons1(y1) |
(31) |
app(cons1(x0),y1) |
→ |
cons2(x0,y1) |
(32) |
app(filter,y1) |
→ |
filter1(y1) |
(33) |
app(filter2,y1) |
→ |
filter21(y1) |
(35) |
app(filter21(x0),y1) |
→ |
filter22(x0,y1) |
(36) |
app(filter22(x0,x1),y1) |
→ |
filter23(x0,x1,y1) |
(37) |
app(filter23(x0,x1,x2),y1) |
→ |
filter24(x0,x1,x2,y1) |
(38) |
There are no rules in the TRS. Hence, it is terminating.