The rewrite relation of the following TRS is considered.
app(perfectp,0) |
→ |
false |
(1) |
app(perfectp,app(s,x)) |
→ |
app(app(app(app(f,x),app(s,0)),app(s,x)),app(s,x)) |
(2) |
app(app(app(app(f,0),y),0),u) |
→ |
true |
(3) |
app(app(app(app(f,0),y),app(s,z)),u) |
→ |
false |
(4) |
app(app(app(app(f,app(s,x)),0),z),u) |
→ |
app(app(app(app(f,x),u),app(app(minus,z),app(s,x))),u) |
(5) |
app(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app(app(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)),app(app(app(app(f,x),u),z),u)) |
(6) |
app(app(map,fun),nil) |
→ |
nil |
(7) |
app(app(map,fun),app(app(cons,x),xs)) |
→ |
app(app(cons,app(fun,x)),app(app(map,fun),xs)) |
(8) |
app(app(filter,fun),nil) |
→ |
nil |
(9) |
app(app(filter,fun),app(app(cons,x),xs)) |
→ |
app(app(app(app(filter2,app(fun,x)),fun),x),xs) |
(10) |
app(app(app(app(filter2,true),fun),x),xs) |
→ |
app(app(cons,x),app(app(filter,fun),xs)) |
(11) |
app(app(app(app(filter2,false),fun),x),xs) |
→ |
app(app(filter,fun),xs) |
(12) |
app#(perfectp,app(s,x)) |
→ |
app#(s,0) |
(13) |
app#(perfectp,app(s,x)) |
→ |
app#(f,x) |
(14) |
app#(perfectp,app(s,x)) |
→ |
app#(app(f,x),app(s,0)) |
(15) |
app#(perfectp,app(s,x)) |
→ |
app#(app(app(f,x),app(s,0)),app(s,x)) |
(16) |
app#(perfectp,app(s,x)) |
→ |
app#(app(app(app(f,x),app(s,0)),app(s,x)),app(s,x)) |
(17) |
app#(app(app(app(f,app(s,x)),0),z),u) |
→ |
app#(minus,z) |
(18) |
app#(app(app(app(f,app(s,x)),0),z),u) |
→ |
app#(app(minus,z),app(s,x)) |
(19) |
app#(app(app(app(f,app(s,x)),0),z),u) |
→ |
app#(f,x) |
(20) |
app#(app(app(app(f,app(s,x)),0),z),u) |
→ |
app#(app(f,x),u) |
(21) |
app#(app(app(app(f,app(s,x)),0),z),u) |
→ |
app#(app(app(f,x),u),app(app(minus,z),app(s,x))) |
(22) |
app#(app(app(app(f,app(s,x)),0),z),u) |
→ |
app#(app(app(app(f,x),u),app(app(minus,z),app(s,x))),u) |
(23) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(f,x) |
(24) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(f,x),u) |
(25) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(app(f,x),u),z) |
(26) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(app(app(f,x),u),z),u) |
(27) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(minus,y) |
(28) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(minus,y),x) |
(29) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(f,app(s,x)),app(app(minus,y),x)) |
(30) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(app(f,app(s,x)),app(app(minus,y),x)),z) |
(31) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u) |
(32) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(le,x) |
(33) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(le,x),y) |
(34) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(if,app(app(le,x),y)) |
(35) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)) |
(36) |
app#(app(app(app(f,app(s,x)),app(s,y)),z),u) |
→ |
app#(app(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)),app(app(app(app(f,x),u),z),u)) |
(37) |
app#(app(map,fun),app(app(cons,x),xs)) |
→ |
app#(app(map,fun),xs) |
(38) |
app#(app(map,fun),app(app(cons,x),xs)) |
→ |
app#(fun,x) |
(39) |
app#(app(map,fun),app(app(cons,x),xs)) |
→ |
app#(cons,app(fun,x)) |
(40) |
app#(app(map,fun),app(app(cons,x),xs)) |
→ |
app#(app(cons,app(fun,x)),app(app(map,fun),xs)) |
(41) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(fun,x) |
(42) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(filter2,app(fun,x)) |
(43) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(app(filter2,app(fun,x)),fun) |
(44) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(app(app(filter2,app(fun,x)),fun),x) |
(45) |
app#(app(filter,fun),app(app(cons,x),xs)) |
→ |
app#(app(app(app(filter2,app(fun,x)),fun),x),xs) |
(46) |
app#(app(app(app(filter2,true),fun),x),xs) |
→ |
app#(filter,fun) |
(47) |
app#(app(app(app(filter2,true),fun),x),xs) |
→ |
app#(app(filter,fun),xs) |
(48) |
app#(app(app(app(filter2,true),fun),x),xs) |
→ |
app#(cons,x) |
(49) |
app#(app(app(app(filter2,true),fun),x),xs) |
→ |
app#(app(cons,x),app(app(filter,fun),xs)) |
(50) |
app#(app(app(app(filter2,false),fun),x),xs) |
→ |
app#(filter,fun) |
(51) |
app#(app(app(app(filter2,false),fun),x),xs) |
→ |
app#(app(filter,fun),xs) |
(52) |
The dependency pairs are split into 2
components.