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) |
app#(D,app(app(+,x),y)) |
→ |
app#(D,y) |
(16) |
app#(D,app(app(+,x),y)) |
→ |
app#(D,x) |
(17) |
app#(D,app(app(+,x),y)) |
→ |
app#(+,app(D,x)) |
(18) |
app#(D,app(app(+,x),y)) |
→ |
app#(app(+,app(D,x)),app(D,y)) |
(19) |
app#(D,app(app(*,x),y)) |
→ |
app#(D,y) |
(20) |
app#(D,app(app(*,x),y)) |
→ |
app#(app(*,x),app(D,y)) |
(21) |
app#(D,app(app(*,x),y)) |
→ |
app#(D,x) |
(22) |
app#(D,app(app(*,x),y)) |
→ |
app#(*,y) |
(23) |
app#(D,app(app(*,x),y)) |
→ |
app#(app(*,y),app(D,x)) |
(24) |
app#(D,app(app(*,x),y)) |
→ |
app#(+,app(app(*,y),app(D,x))) |
(25) |
app#(D,app(app(*,x),y)) |
→ |
app#(app(+,app(app(*,y),app(D,x))),app(app(*,x),app(D,y))) |
(26) |
app#(D,app(app(-,x),y)) |
→ |
app#(D,y) |
(27) |
app#(D,app(app(-,x),y)) |
→ |
app#(D,x) |
(28) |
app#(D,app(app(-,x),y)) |
→ |
app#(-,app(D,x)) |
(29) |
app#(D,app(app(-,x),y)) |
→ |
app#(app(-,app(D,x)),app(D,y)) |
(30) |
app#(D,app(minus,x)) |
→ |
app#(D,x) |
(31) |
app#(D,app(minus,x)) |
→ |
app#(minus,app(D,x)) |
(32) |
app#(D,app(app(div,x),y)) |
→ |
app#(pow,y) |
(33) |
app#(D,app(app(div,x),y)) |
→ |
app#(app(pow,y),2) |
(34) |
app#(D,app(app(div,x),y)) |
→ |
app#(D,y) |
(35) |
app#(D,app(app(div,x),y)) |
→ |
app#(*,x) |
(36) |
app#(D,app(app(div,x),y)) |
→ |
app#(app(*,x),app(D,y)) |
(37) |
app#(D,app(app(div,x),y)) |
→ |
app#(div,app(app(*,x),app(D,y))) |
(38) |
app#(D,app(app(div,x),y)) |
→ |
app#(app(div,app(app(*,x),app(D,y))),app(app(pow,y),2)) |
(39) |
app#(D,app(app(div,x),y)) |
→ |
app#(D,x) |
(40) |
app#(D,app(app(div,x),y)) |
→ |
app#(div,app(D,x)) |
(41) |
app#(D,app(app(div,x),y)) |
→ |
app#(app(div,app(D,x)),y) |
(42) |
app#(D,app(app(div,x),y)) |
→ |
app#(-,app(app(div,app(D,x)),y)) |
(43) |
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))) |
(44) |
app#(D,app(ln,x)) |
→ |
app#(D,x) |
(45) |
app#(D,app(ln,x)) |
→ |
app#(div,app(D,x)) |
(46) |
app#(D,app(ln,x)) |
→ |
app#(app(div,app(D,x)),x) |
(47) |
app#(D,app(app(pow,x),y)) |
→ |
app#(D,y) |
(48) |
app#(D,app(app(pow,x),y)) |
→ |
app#(ln,x) |
(49) |
app#(D,app(app(pow,x),y)) |
→ |
app#(*,app(app(pow,x),y)) |
(50) |
app#(D,app(app(pow,x),y)) |
→ |
app#(app(*,app(app(pow,x),y)),app(ln,x)) |
(51) |
app#(D,app(app(pow,x),y)) |
→ |
app#(*,app(app(*,app(app(pow,x),y)),app(ln,x))) |
(52) |
app#(D,app(app(pow,x),y)) |
→ |
app#(app(*,app(app(*,app(app(pow,x),y)),app(ln,x))),app(D,y)) |
(53) |
app#(D,app(app(pow,x),y)) |
→ |
app#(D,x) |
(54) |
app#(D,app(app(pow,x),y)) |
→ |
app#(-,y) |
(55) |
app#(D,app(app(pow,x),y)) |
→ |
app#(app(-,y),1) |
(56) |
app#(D,app(app(pow,x),y)) |
→ |
app#(app(pow,x),app(app(-,y),1)) |
(57) |
app#(D,app(app(pow,x),y)) |
→ |
app#(*,y) |
(58) |
app#(D,app(app(pow,x),y)) |
→ |
app#(app(*,y),app(app(pow,x),app(app(-,y),1))) |
(59) |
app#(D,app(app(pow,x),y)) |
→ |
app#(*,app(app(*,y),app(app(pow,x),app(app(-,y),1)))) |
(60) |
app#(D,app(app(pow,x),y)) |
→ |
app#(app(*,app(app(*,y),app(app(pow,x),app(app(-,y),1)))),app(D,x)) |
(61) |
app#(D,app(app(pow,x),y)) |
→ |
app#(+,app(app(*,app(app(*,y),app(app(pow,x),app(app(-,y),1)))),app(D,x))) |
(62) |
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))) |
(63) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(app(map,f),xs) |
(64) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(f,x) |
(65) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(cons,app(f,x)) |
(66) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(app(cons,app(f,x)),app(app(map,f),xs)) |
(67) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(f,x) |
(68) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(filter2,app(f,x)) |
(69) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(app(filter2,app(f,x)),f) |
(70) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(app(app(filter2,app(f,x)),f),x) |
(71) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(app(app(app(filter2,app(f,x)),f),x),xs) |
(72) |
app#(app(app(app(filter2,true),f),x),xs) |
→ |
app#(filter,f) |
(73) |
app#(app(app(app(filter2,true),f),x),xs) |
→ |
app#(app(filter,f),xs) |
(74) |
app#(app(app(app(filter2,true),f),x),xs) |
→ |
app#(cons,x) |
(75) |
app#(app(app(app(filter2,true),f),x),xs) |
→ |
app#(app(cons,x),app(app(filter,f),xs)) |
(76) |
app#(app(app(app(filter2,false),f),x),xs) |
→ |
app#(filter,f) |
(77) |
app#(app(app(app(filter2,false),f),x),xs) |
→ |
app#(app(filter,f),xs) |
(78) |
The dependency pairs are split into 2
components.