The rewrite relation of the following TRS is considered.
|
app(app(app(if,true),xs),ys) |
→ |
xs |
(1) |
|
app(app(app(if,false),xs),ys) |
→ |
ys |
(2) |
|
app(app(lt,app(s,x)),app(s,y)) |
→ |
app(app(lt,x),y) |
(3) |
|
app(app(lt,0),app(s,y)) |
→ |
true |
(4) |
|
app(app(lt,y),0) |
→ |
false |
(5) |
|
app(app(eq,x),x) |
→ |
true |
(6) |
|
app(app(eq,app(s,x)),0) |
→ |
false |
(7) |
|
app(app(eq,0),app(s,x)) |
→ |
false |
(8) |
|
app(app(merge,xs),nil) |
→ |
xs |
(9) |
|
app(app(merge,nil),ys) |
→ |
ys |
(10) |
|
app(app(merge,app(app(cons,x),xs)),app(app(cons,y),ys)) |
→ |
app(app(app(if,app(app(lt,x),y)),app(app(cons,x),app(app(merge,xs),app(app(cons,y),ys)))),app(app(app(if,app(app(eq,x),y)),app(app(cons,x),app(app(merge,xs),ys))),app(app(cons,y),app(app(merge,app(app(cons,x),xs)),ys)))) |
(11) |
|
app(app(map,f),nil) |
→ |
nil |
(12) |
|
app(app(map,f),app(app(cons,x),xs)) |
→ |
app(app(cons,app(f,x)),app(app(map,f),xs)) |
(13) |
|
app(app(mult,0),x) |
→ |
0 |
(14) |
|
app(app(mult,app(s,x)),y) |
→ |
app(app(plus,y),app(app(mult,x),y)) |
(15) |
|
app(app(plus,0),x) |
→ |
0 |
(16) |
|
app(app(plus,app(s,x)),y) |
→ |
app(s,app(app(plus,x),y)) |
(17) |
| list1 |
→ |
app(app(map,app(mult,app(s,app(s,0)))),hamming) |
(18) |
| list2 |
→ |
app(app(map,app(mult,app(s,app(s,app(s,0))))),hamming) |
(19) |
| list3 |
→ |
app(app(map,app(mult,app(s,app(s,app(s,app(s,app(s,0))))))),hamming) |
(20) |
| hamming |
→ |
app(app(cons,app(s,0)),app(app(merge,list1),app(app(merge,list2),list3))) |
(21) |