(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
active(pairNs) → mark(cons(0, incr(oddNs)))
active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))
active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))
active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)
active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)
active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))
mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))
mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))
mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)
take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)
zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)
zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)
pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)
pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)
repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)
Q is empty.