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) |
zip(nil,XS) | → | nil | (6) |
zip(X,nil) | → | nil | (7) |
zip(X1,X2) | → | n__zip(X1,X2) | (14) |
tail(cons(X,XS)) | → | activate(XS) | (9) |
repItems(nil) | → | nil | (10) |
repItems(X) | → | n__repItems(X) | (16) |
take(0,XS) | → | nil | (4) |
take(X1,X2) | → | n__take(X1,X2) | (13) |
repItems(cons(X,XS)) | → | cons(X,n__cons(X,n__repItems(activate(XS)))) | (11) |
activate(n__take(X1,X2)) | → | take(X1,X2) | (18) |
activate(n__repItems(X)) | → | repItems(X) | (21) |
take(s(N),cons(X,XS)) | → | cons(X,n__take(N,activate(XS))) | (5) |
activate(n__zip(X1,X2)) | → | zip(X1,X2) | (19) |
zip(cons(X,XS),cons(Y,YS)) | → | cons(pair(X,Y),n__zip(activate(XS),activate(YS))) | (8) |
pairNs# | → | cons#(0,n__incr(oddNs)) | (23) |
pairNs# | → | oddNs# | (24) |
oddNs# | → | incr#(pairNs) | (25) |
oddNs# | → | pairNs# | (26) |
incr#(cons(X,XS)) | → | cons#(s(X),n__incr(activate(XS))) | (27) |
incr#(cons(X,XS)) | → | activate#(XS) | (28) |
activate#(n__incr(X)) | → | incr#(X) | (29) |
activate#(n__cons(X1,X2)) | → | cons#(X1,X2) | (30) |
pairNs# | → | cons#(0,n__incr(oddNs)) | (23) |
oddNs# | → | incr#(pairNs) | (25) |
incr#(cons(X,XS)) | → | cons#(s(X),n__incr(activate(XS))) | (27) |
incr#(cons(X,XS)) | → | activate#(XS) | (28) |
activate#(n__incr(X)) | → | incr#(X) | (29) |
activate#(n__cons(X1,X2)) | → | cons#(X1,X2) | (30) |
pairNs | → | cons(0,n__incr(oddNs)) | (1) |
oddNs | → | incr(pairNs) | (2) |
incr(cons(X,XS)) | → | cons(s(X),n__incr(activate(XS))) | (3) |
incr(X) | → | n__incr(X) | (12) |
cons(X1,X2) | → | n__cons(X1,X2) | (15) |
activate(n__incr(X)) | → | incr(X) | (17) |
activate(n__cons(X1,X2)) | → | cons(X1,X2) | (20) |
activate(X) | → | X | (22) |
t0 | = | oddNs# |
→P | pairNs# | |
→P | oddNs# | |
= | t2 |