The rewrite relation of the following TRS is considered.
app(app(:,app(app(:,x),y)),z) |
→ |
app(app(:,x),app(app(:,y),z)) |
(1) |
app(app(:,app(app(+,x),y)),z) |
→ |
app(app(+,app(app(:,x),z)),app(app(:,y),z)) |
(2) |
app(app(:,z),app(app(+,x),app(f,y))) |
→ |
app(app(:,app(app(g,z),y)),app(app(+,x),a)) |
(3) |
app(app(map,f),nil) |
→ |
nil |
(4) |
app(app(map,f),app(app(cons,x),xs)) |
→ |
app(app(cons,app(f,x)),app(app(map,f),xs)) |
(5) |
app(app(filter,f),nil) |
→ |
nil |
(6) |
app(app(filter,f),app(app(cons,x),xs)) |
→ |
app(app(app(app(filter2,app(f,x)),f),x),xs) |
(7) |
app(app(app(app(filter2,true),f),x),xs) |
→ |
app(app(cons,x),app(app(filter,f),xs)) |
(8) |
app(app(app(app(filter2,false),f),x),xs) |
→ |
app(app(filter,f),xs) |
(9) |
app#(app(:,app(app(:,x),y)),z) |
→ |
app#(app(:,x),app(app(:,y),z)) |
(10) |
app#(app(:,app(app(:,x),y)),z) |
→ |
app#(app(:,y),z) |
(11) |
app#(app(:,app(app(:,x),y)),z) |
→ |
app#(:,y) |
(12) |
app#(app(:,app(app(+,x),y)),z) |
→ |
app#(app(+,app(app(:,x),z)),app(app(:,y),z)) |
(13) |
app#(app(:,app(app(+,x),y)),z) |
→ |
app#(+,app(app(:,x),z)) |
(14) |
app#(app(:,app(app(+,x),y)),z) |
→ |
app#(app(:,x),z) |
(15) |
app#(app(:,app(app(+,x),y)),z) |
→ |
app#(:,x) |
(16) |
app#(app(:,app(app(+,x),y)),z) |
→ |
app#(app(:,y),z) |
(17) |
app#(app(:,app(app(+,x),y)),z) |
→ |
app#(:,y) |
(18) |
app#(app(:,z),app(app(+,x),app(f,y))) |
→ |
app#(app(:,app(app(g,z),y)),app(app(+,x),a)) |
(19) |
app#(app(:,z),app(app(+,x),app(f,y))) |
→ |
app#(:,app(app(g,z),y)) |
(20) |
app#(app(:,z),app(app(+,x),app(f,y))) |
→ |
app#(app(g,z),y) |
(21) |
app#(app(:,z),app(app(+,x),app(f,y))) |
→ |
app#(g,z) |
(22) |
app#(app(:,z),app(app(+,x),app(f,y))) |
→ |
app#(app(+,x),a) |
(23) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(app(cons,app(f,x)),app(app(map,f),xs)) |
(24) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(cons,app(f,x)) |
(25) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(f,x) |
(26) |
app#(app(map,f),app(app(cons,x),xs)) |
→ |
app#(app(map,f),xs) |
(27) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(app(app(app(filter2,app(f,x)),f),x),xs) |
(28) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(app(app(filter2,app(f,x)),f),x) |
(29) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(app(filter2,app(f,x)),f) |
(30) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(filter2,app(f,x)) |
(31) |
app#(app(filter,f),app(app(cons,x),xs)) |
→ |
app#(f,x) |
(32) |
app#(app(app(app(filter2,true),f),x),xs) |
→ |
app#(app(cons,x),app(app(filter,f),xs)) |
(33) |
app#(app(app(app(filter2,true),f),x),xs) |
→ |
app#(cons,x) |
(34) |
app#(app(app(app(filter2,true),f),x),xs) |
→ |
app#(app(filter,f),xs) |
(35) |
app#(app(app(app(filter2,true),f),x),xs) |
→ |
app#(filter,f) |
(36) |
app#(app(app(app(filter2,false),f),x),xs) |
→ |
app#(app(filter,f),xs) |
(37) |
app#(app(app(app(filter2,false),f),x),xs) |
→ |
app#(filter,f) |
(38) |
The dependency pairs are split into 2
components.