The rewrite relation of the following TRS is considered.
| pairNs |
→ |
cons(0,n__incr(oddNs)) |
(1) |
| oddNs |
→ |
incr(pairNs) |
(2) |
|
incr(cons(X,XS)) |
→ |
cons(s(X),n__incr(activate(XS))) |
(3) |
|
take(0,XS) |
→ |
nil |
(4) |
|
take(s(N),cons(X,XS)) |
→ |
cons(X,n__take(N,activate(XS))) |
(5) |
|
zip(nil,XS) |
→ |
nil |
(6) |
|
zip(X,nil) |
→ |
nil |
(7) |
|
zip(cons(X,XS),cons(Y,YS)) |
→ |
cons(pair(X,Y),n__zip(activate(XS),activate(YS))) |
(8) |
|
tail(cons(X,XS)) |
→ |
activate(XS) |
(9) |
|
repItems(nil) |
→ |
nil |
(10) |
|
repItems(cons(X,XS)) |
→ |
cons(X,n__cons(X,n__repItems(activate(XS)))) |
(11) |
|
incr(X) |
→ |
n__incr(X) |
(12) |
|
take(X1,X2) |
→ |
n__take(X1,X2) |
(13) |
|
zip(X1,X2) |
→ |
n__zip(X1,X2) |
(14) |
|
cons(X1,X2) |
→ |
n__cons(X1,X2) |
(15) |
|
repItems(X) |
→ |
n__repItems(X) |
(16) |
|
activate(n__incr(X)) |
→ |
incr(X) |
(17) |
|
activate(n__take(X1,X2)) |
→ |
take(X1,X2) |
(18) |
|
activate(n__zip(X1,X2)) |
→ |
zip(X1,X2) |
(19) |
|
activate(n__cons(X1,X2)) |
→ |
cons(X1,X2) |
(20) |
|
activate(n__repItems(X)) |
→ |
repItems(X) |
(21) |
|
activate(X) |
→ |
X |
(22) |