MAYBE

Problem:
 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))))
 active(cons(X1,X2)) -> cons(active(X1),X2)
 active(incr(X)) -> incr(active(X))
 active(s(X)) -> s(active(X))
 active(take(X1,X2)) -> take(active(X1),X2)
 active(take(X1,X2)) -> take(X1,active(X2))
 active(zip(X1,X2)) -> zip(active(X1),X2)
 active(zip(X1,X2)) -> zip(X1,active(X2))
 active(pair(X1,X2)) -> pair(active(X1),X2)
 active(pair(X1,X2)) -> pair(X1,active(X2))
 active(tail(X)) -> tail(active(X))
 active(repItems(X)) -> repItems(active(X))
 cons(mark(X1),X2) -> mark(cons(X1,X2))
 incr(mark(X)) -> mark(incr(X))
 s(mark(X)) -> mark(s(X))
 take(mark(X1),X2) -> mark(take(X1,X2))
 take(X1,mark(X2)) -> mark(take(X1,X2))
 zip(mark(X1),X2) -> mark(zip(X1,X2))
 zip(X1,mark(X2)) -> mark(zip(X1,X2))
 pair(mark(X1),X2) -> mark(pair(X1,X2))
 pair(X1,mark(X2)) -> mark(pair(X1,X2))
 tail(mark(X)) -> mark(tail(X))
 repItems(mark(X)) -> mark(repItems(X))
 proper(pairNs()) -> ok(pairNs())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(incr(X)) -> incr(proper(X))
 proper(oddNs()) -> ok(oddNs())
 proper(s(X)) -> s(proper(X))
 proper(take(X1,X2)) -> take(proper(X1),proper(X2))
 proper(nil()) -> ok(nil())
 proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
 proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
 proper(tail(X)) -> tail(proper(X))
 proper(repItems(X)) -> repItems(proper(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 incr(ok(X)) -> ok(incr(X))
 s(ok(X)) -> ok(s(X))
 take(ok(X1),ok(X2)) -> ok(take(X1,X2))
 zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
 pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
 tail(ok(X)) -> ok(tail(X))
 repItems(ok(X)) -> ok(repItems(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 DP Processor:
  DPs:
   active#(pairNs()) -> incr#(oddNs())
   active#(pairNs()) -> cons#(0(),incr(oddNs()))
   active#(oddNs()) -> incr#(pairNs())
   active#(incr(cons(X,XS))) -> incr#(XS)
   active#(incr(cons(X,XS))) -> s#(X)
   active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
   active#(take(s(N),cons(X,XS))) -> take#(N,XS)
   active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
   active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
   active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
   active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
   active#(repItems(cons(X,XS))) -> repItems#(XS)
   active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
   active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
   active#(cons(X1,X2)) -> active#(X1)
   active#(cons(X1,X2)) -> cons#(active(X1),X2)
   active#(incr(X)) -> active#(X)
   active#(incr(X)) -> incr#(active(X))
   active#(s(X)) -> active#(X)
   active#(s(X)) -> s#(active(X))
   active#(take(X1,X2)) -> active#(X1)
   active#(take(X1,X2)) -> take#(active(X1),X2)
   active#(take(X1,X2)) -> active#(X2)
   active#(take(X1,X2)) -> take#(X1,active(X2))
   active#(zip(X1,X2)) -> active#(X1)
   active#(zip(X1,X2)) -> zip#(active(X1),X2)
   active#(zip(X1,X2)) -> active#(X2)
   active#(zip(X1,X2)) -> zip#(X1,active(X2))
   active#(pair(X1,X2)) -> active#(X1)
   active#(pair(X1,X2)) -> pair#(active(X1),X2)
   active#(pair(X1,X2)) -> active#(X2)
   active#(pair(X1,X2)) -> pair#(X1,active(X2))
   active#(tail(X)) -> active#(X)
   active#(tail(X)) -> tail#(active(X))
   active#(repItems(X)) -> active#(X)
   active#(repItems(X)) -> repItems#(active(X))
   cons#(mark(X1),X2) -> cons#(X1,X2)
   incr#(mark(X)) -> incr#(X)
   s#(mark(X)) -> s#(X)
   take#(mark(X1),X2) -> take#(X1,X2)
   take#(X1,mark(X2)) -> take#(X1,X2)
   zip#(mark(X1),X2) -> zip#(X1,X2)
   zip#(X1,mark(X2)) -> zip#(X1,X2)
   pair#(mark(X1),X2) -> pair#(X1,X2)
   pair#(X1,mark(X2)) -> pair#(X1,X2)
   tail#(mark(X)) -> tail#(X)
   repItems#(mark(X)) -> repItems#(X)
   proper#(cons(X1,X2)) -> proper#(X2)
   proper#(cons(X1,X2)) -> proper#(X1)
   proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
   proper#(incr(X)) -> proper#(X)
   proper#(incr(X)) -> incr#(proper(X))
   proper#(s(X)) -> proper#(X)
   proper#(s(X)) -> s#(proper(X))
   proper#(take(X1,X2)) -> proper#(X2)
   proper#(take(X1,X2)) -> proper#(X1)
   proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
   proper#(zip(X1,X2)) -> proper#(X2)
   proper#(zip(X1,X2)) -> proper#(X1)
   proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
   proper#(pair(X1,X2)) -> proper#(X2)
   proper#(pair(X1,X2)) -> proper#(X1)
   proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
   proper#(tail(X)) -> proper#(X)
   proper#(tail(X)) -> tail#(proper(X))
   proper#(repItems(X)) -> proper#(X)
   proper#(repItems(X)) -> repItems#(proper(X))
   cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
   incr#(ok(X)) -> incr#(X)
   s#(ok(X)) -> s#(X)
   take#(ok(X1),ok(X2)) -> take#(X1,X2)
   zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
   pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
   tail#(ok(X)) -> tail#(X)
   repItems#(ok(X)) -> repItems#(X)
   top#(mark(X)) -> proper#(X)
   top#(mark(X)) -> top#(proper(X))
   top#(ok(X)) -> active#(X)
   top#(ok(X)) -> top#(active(X))
  TRS:
   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))))
   active(cons(X1,X2)) -> cons(active(X1),X2)
   active(incr(X)) -> incr(active(X))
   active(s(X)) -> s(active(X))
   active(take(X1,X2)) -> take(active(X1),X2)
   active(take(X1,X2)) -> take(X1,active(X2))
   active(zip(X1,X2)) -> zip(active(X1),X2)
   active(zip(X1,X2)) -> zip(X1,active(X2))
   active(pair(X1,X2)) -> pair(active(X1),X2)
   active(pair(X1,X2)) -> pair(X1,active(X2))
   active(tail(X)) -> tail(active(X))
   active(repItems(X)) -> repItems(active(X))
   cons(mark(X1),X2) -> mark(cons(X1,X2))
   incr(mark(X)) -> mark(incr(X))
   s(mark(X)) -> mark(s(X))
   take(mark(X1),X2) -> mark(take(X1,X2))
   take(X1,mark(X2)) -> mark(take(X1,X2))
   zip(mark(X1),X2) -> mark(zip(X1,X2))
   zip(X1,mark(X2)) -> mark(zip(X1,X2))
   pair(mark(X1),X2) -> mark(pair(X1,X2))
   pair(X1,mark(X2)) -> mark(pair(X1,X2))
   tail(mark(X)) -> mark(tail(X))
   repItems(mark(X)) -> mark(repItems(X))
   proper(pairNs()) -> ok(pairNs())
   proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
   proper(0()) -> ok(0())
   proper(incr(X)) -> incr(proper(X))
   proper(oddNs()) -> ok(oddNs())
   proper(s(X)) -> s(proper(X))
   proper(take(X1,X2)) -> take(proper(X1),proper(X2))
   proper(nil()) -> ok(nil())
   proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
   proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
   proper(tail(X)) -> tail(proper(X))
   proper(repItems(X)) -> repItems(proper(X))
   cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
   incr(ok(X)) -> ok(incr(X))
   s(ok(X)) -> ok(s(X))
   take(ok(X1),ok(X2)) -> ok(take(X1,X2))
   zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
   pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
   tail(ok(X)) -> ok(tail(X))
   repItems(ok(X)) -> ok(repItems(X))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  TDG Processor:
   DPs:
    active#(pairNs()) -> incr#(oddNs())
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(oddNs()) -> incr#(pairNs())
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(incr(cons(X,XS))) -> s#(X)
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(cons(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(incr(X)) -> active#(X)
    active#(incr(X)) -> incr#(active(X))
    active#(s(X)) -> active#(X)
    active#(s(X)) -> s#(active(X))
    active#(take(X1,X2)) -> active#(X1)
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(take(X1,X2)) -> active#(X2)
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(zip(X1,X2)) -> active#(X1)
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(zip(X1,X2)) -> active#(X2)
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(pair(X1,X2)) -> active#(X1)
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(pair(X1,X2)) -> active#(X2)
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(tail(X)) -> active#(X)
    active#(tail(X)) -> tail#(active(X))
    active#(repItems(X)) -> active#(X)
    active#(repItems(X)) -> repItems#(active(X))
    cons#(mark(X1),X2) -> cons#(X1,X2)
    incr#(mark(X)) -> incr#(X)
    s#(mark(X)) -> s#(X)
    take#(mark(X1),X2) -> take#(X1,X2)
    take#(X1,mark(X2)) -> take#(X1,X2)
    zip#(mark(X1),X2) -> zip#(X1,X2)
    zip#(X1,mark(X2)) -> zip#(X1,X2)
    pair#(mark(X1),X2) -> pair#(X1,X2)
    pair#(X1,mark(X2)) -> pair#(X1,X2)
    tail#(mark(X)) -> tail#(X)
    repItems#(mark(X)) -> repItems#(X)
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(incr(X)) -> proper#(X)
    proper#(incr(X)) -> incr#(proper(X))
    proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> s#(proper(X))
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(tail(X)) -> proper#(X)
    proper#(tail(X)) -> tail#(proper(X))
    proper#(repItems(X)) -> proper#(X)
    proper#(repItems(X)) -> repItems#(proper(X))
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    incr#(ok(X)) -> incr#(X)
    s#(ok(X)) -> s#(X)
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
    tail#(ok(X)) -> tail#(X)
    repItems#(ok(X)) -> repItems#(X)
    top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X))
   TRS:
    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))))
    active(cons(X1,X2)) -> cons(active(X1),X2)
    active(incr(X)) -> incr(active(X))
    active(s(X)) -> s(active(X))
    active(take(X1,X2)) -> take(active(X1),X2)
    active(take(X1,X2)) -> take(X1,active(X2))
    active(zip(X1,X2)) -> zip(active(X1),X2)
    active(zip(X1,X2)) -> zip(X1,active(X2))
    active(pair(X1,X2)) -> pair(active(X1),X2)
    active(pair(X1,X2)) -> pair(X1,active(X2))
    active(tail(X)) -> tail(active(X))
    active(repItems(X)) -> repItems(active(X))
    cons(mark(X1),X2) -> mark(cons(X1,X2))
    incr(mark(X)) -> mark(incr(X))
    s(mark(X)) -> mark(s(X))
    take(mark(X1),X2) -> mark(take(X1,X2))
    take(X1,mark(X2)) -> mark(take(X1,X2))
    zip(mark(X1),X2) -> mark(zip(X1,X2))
    zip(X1,mark(X2)) -> mark(zip(X1,X2))
    pair(mark(X1),X2) -> mark(pair(X1,X2))
    pair(X1,mark(X2)) -> mark(pair(X1,X2))
    tail(mark(X)) -> mark(tail(X))
    repItems(mark(X)) -> mark(repItems(X))
    proper(pairNs()) -> ok(pairNs())
    proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    proper(0()) -> ok(0())
    proper(incr(X)) -> incr(proper(X))
    proper(oddNs()) -> ok(oddNs())
    proper(s(X)) -> s(proper(X))
    proper(take(X1,X2)) -> take(proper(X1),proper(X2))
    proper(nil()) -> ok(nil())
    proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
    proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
    proper(tail(X)) -> tail(proper(X))
    proper(repItems(X)) -> repItems(proper(X))
    cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    incr(ok(X)) -> ok(incr(X))
    s(ok(X)) -> ok(s(X))
    take(ok(X1),ok(X2)) -> ok(take(X1,X2))
    zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
    pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
    tail(ok(X)) -> ok(tail(X))
    repItems(ok(X)) -> ok(repItems(X))
    top(mark(X)) -> top(proper(X))
    top(ok(X)) -> top(active(X))
   graph:
    top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X))
    top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
    top#(ok(X)) -> active#(X) ->
    active#(repItems(X)) -> repItems#(active(X))
    top#(ok(X)) -> active#(X) -> active#(repItems(X)) -> active#(X)
    top#(ok(X)) -> active#(X) -> active#(tail(X)) -> tail#(active(X))
    top#(ok(X)) -> active#(X) -> active#(tail(X)) -> active#(X)
    top#(ok(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    top#(ok(X)) -> active#(X) -> active#(pair(X1,X2)) -> active#(X2)
    top#(ok(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(pair(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    top#(ok(X)) -> active#(X) -> active#(zip(X1,X2)) -> active#(X2)
    top#(ok(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(zip(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    top#(ok(X)) -> active#(X) -> active#(take(X1,X2)) -> active#(X2)
    top#(ok(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(take(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    top#(ok(X)) -> active#(X) -> active#(incr(X)) -> incr#(active(X))
    top#(ok(X)) -> active#(X) -> active#(incr(X)) -> active#(X)
    top#(ok(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    top#(ok(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    top#(ok(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    top#(ok(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    top#(ok(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    top#(ok(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    top#(ok(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    top#(ok(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    top#(ok(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    top#(ok(X)) -> active#(X) -> active#(incr(cons(X,XS))) -> s#(X)
    top#(ok(X)) -> active#(X) -> active#(incr(cons(X,XS))) -> incr#(XS)
    top#(ok(X)) -> active#(X) -> active#(oddNs()) -> incr#(pairNs())
    top#(ok(X)) -> active#(X) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    top#(ok(X)) -> active#(X) ->
    active#(pairNs()) -> incr#(oddNs())
    top#(mark(X)) -> top#(proper(X)) ->
    top#(ok(X)) -> top#(active(X))
    top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
    top#(mark(X)) -> top#(proper(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(repItems(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) -> proper#(tail(X)) -> tail#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(pair(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(pair(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(zip(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(zip(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(take(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(take(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) -> proper#(incr(X)) -> incr#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(incr(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(repItems(X)) -> proper#(X) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(repItems(X)) -> proper#(X) ->
    proper#(tail(X)) -> proper#(X)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(repItems(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(repItems(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(repItems(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(repItems(X)) -> proper#(X) ->
    proper#(s(X)) -> proper#(X)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(repItems(X)) -> proper#(X) ->
    proper#(incr(X)) -> proper#(X)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(repItems(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(repItems(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(repItems(X)) -> repItems#(proper(X)) ->
    repItems#(ok(X)) -> repItems#(X)
    proper#(repItems(X)) -> repItems#(proper(X)) ->
    repItems#(mark(X)) -> repItems#(X)
    proper#(tail(X)) -> proper#(X) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(tail(X)) -> proper#(X) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(tail(X)) -> proper#(X) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(tail(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X)
    proper#(tail(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(tail(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(tail(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(tail(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(tail(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(tail(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(tail(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(tail(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(tail(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(tail(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(tail(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(tail(X)) -> proper#(X) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(tail(X)) -> proper#(X) -> proper#(incr(X)) -> proper#(X)
    proper#(tail(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(tail(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(tail(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(tail(X)) -> tail#(proper(X)) ->
    tail#(ok(X)) -> tail#(X)
    proper#(tail(X)) -> tail#(proper(X)) ->
    tail#(mark(X)) -> tail#(X)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(tail(X)) -> proper#(X)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(incr(X)) -> proper#(X)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(pair(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(tail(X)) -> proper#(X)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(incr(X)) -> proper#(X)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(pair(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2)) ->
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2)) ->
    pair#(X1,mark(X2)) -> pair#(X1,X2)
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2)) ->
    pair#(mark(X1),X2) -> pair#(X1,X2)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(tail(X)) -> proper#(X)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(incr(X)) -> proper#(X)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(zip(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(tail(X)) -> proper#(X)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(incr(X)) -> proper#(X)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(zip(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2)) ->
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2)) ->
    zip#(X1,mark(X2)) -> zip#(X1,X2)
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2)) ->
    zip#(mark(X1),X2) -> zip#(X1,X2)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(tail(X)) -> proper#(X)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(incr(X)) -> proper#(X)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(tail(X)) -> proper#(X)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(incr(X)) -> proper#(X)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2)) ->
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2)) ->
    take#(X1,mark(X2)) -> take#(X1,X2)
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2)) ->
    take#(mark(X1),X2) -> take#(X1,X2)
    proper#(s(X)) -> proper#(X) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(repItems(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) -> proper#(tail(X)) -> tail#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(pair(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(pair(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(zip(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(zip(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(take(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(take(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) -> proper#(incr(X)) -> incr#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(incr(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
    proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(tail(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(incr(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(tail(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(incr(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    proper#(incr(X)) -> proper#(X) ->
    proper#(repItems(X)) -> repItems#(proper(X))
    proper#(incr(X)) -> proper#(X) ->
    proper#(repItems(X)) -> proper#(X)
    proper#(incr(X)) -> proper#(X) ->
    proper#(tail(X)) -> tail#(proper(X))
    proper#(incr(X)) -> proper#(X) -> proper#(tail(X)) -> proper#(X)
    proper#(incr(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> pair#(proper(X1),proper(X2))
    proper#(incr(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> proper#(X1)
    proper#(incr(X)) -> proper#(X) ->
    proper#(pair(X1,X2)) -> proper#(X2)
    proper#(incr(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> zip#(proper(X1),proper(X2))
    proper#(incr(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> proper#(X1)
    proper#(incr(X)) -> proper#(X) ->
    proper#(zip(X1,X2)) -> proper#(X2)
    proper#(incr(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(incr(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(incr(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(incr(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(incr(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(incr(X)) -> proper#(X) ->
    proper#(incr(X)) -> incr#(proper(X))
    proper#(incr(X)) -> proper#(X) -> proper#(incr(X)) -> proper#(X)
    proper#(incr(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(incr(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(incr(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(incr(X)) -> incr#(proper(X)) ->
    incr#(ok(X)) -> incr#(X)
    proper#(incr(X)) -> incr#(proper(X)) -> incr#(mark(X)) -> incr#(X)
    tail#(ok(X)) -> tail#(X) -> tail#(ok(X)) -> tail#(X)
    tail#(ok(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
    tail#(mark(X)) -> tail#(X) -> tail#(ok(X)) -> tail#(X)
    tail#(mark(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
    repItems#(ok(X)) -> repItems#(X) ->
    repItems#(ok(X)) -> repItems#(X)
    repItems#(ok(X)) -> repItems#(X) ->
    repItems#(mark(X)) -> repItems#(X)
    repItems#(mark(X)) -> repItems#(X) ->
    repItems#(ok(X)) -> repItems#(X)
    repItems#(mark(X)) -> repItems#(X) ->
    repItems#(mark(X)) -> repItems#(X)
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2) ->
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2) ->
    pair#(X1,mark(X2)) -> pair#(X1,X2)
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2) ->
    pair#(mark(X1),X2) -> pair#(X1,X2)
    pair#(mark(X1),X2) -> pair#(X1,X2) ->
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
    pair#(mark(X1),X2) -> pair#(X1,X2) ->
    pair#(X1,mark(X2)) -> pair#(X1,X2)
    pair#(mark(X1),X2) -> pair#(X1,X2) ->
    pair#(mark(X1),X2) -> pair#(X1,X2)
    pair#(X1,mark(X2)) -> pair#(X1,X2) ->
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
    pair#(X1,mark(X2)) -> pair#(X1,X2) ->
    pair#(X1,mark(X2)) -> pair#(X1,X2)
    pair#(X1,mark(X2)) -> pair#(X1,X2) ->
    pair#(mark(X1),X2) -> pair#(X1,X2)
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2) ->
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2) ->
    zip#(X1,mark(X2)) -> zip#(X1,X2)
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2) ->
    zip#(mark(X1),X2) -> zip#(X1,X2)
    zip#(mark(X1),X2) -> zip#(X1,X2) ->
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
    zip#(mark(X1),X2) -> zip#(X1,X2) ->
    zip#(X1,mark(X2)) -> zip#(X1,X2)
    zip#(mark(X1),X2) -> zip#(X1,X2) ->
    zip#(mark(X1),X2) -> zip#(X1,X2)
    zip#(X1,mark(X2)) -> zip#(X1,X2) ->
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
    zip#(X1,mark(X2)) -> zip#(X1,X2) ->
    zip#(X1,mark(X2)) -> zip#(X1,X2)
    zip#(X1,mark(X2)) -> zip#(X1,X2) ->
    zip#(mark(X1),X2) -> zip#(X1,X2)
    take#(ok(X1),ok(X2)) -> take#(X1,X2) ->
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    take#(ok(X1),ok(X2)) -> take#(X1,X2) ->
    take#(X1,mark(X2)) -> take#(X1,X2)
    take#(ok(X1),ok(X2)) -> take#(X1,X2) ->
    take#(mark(X1),X2) -> take#(X1,X2)
    take#(mark(X1),X2) -> take#(X1,X2) ->
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    take#(mark(X1),X2) -> take#(X1,X2) ->
    take#(X1,mark(X2)) -> take#(X1,X2)
    take#(mark(X1),X2) -> take#(X1,X2) ->
    take#(mark(X1),X2) -> take#(X1,X2)
    take#(X1,mark(X2)) -> take#(X1,X2) ->
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    take#(X1,mark(X2)) -> take#(X1,X2) ->
    take#(X1,mark(X2)) -> take#(X1,X2)
    take#(X1,mark(X2)) -> take#(X1,X2) -> take#(mark(X1),X2) -> take#(X1,X2)
    s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    incr#(ok(X)) -> incr#(X) -> incr#(ok(X)) -> incr#(X)
    incr#(ok(X)) -> incr#(X) -> incr#(mark(X)) -> incr#(X)
    incr#(mark(X)) -> incr#(X) -> incr#(ok(X)) -> incr#(X)
    incr#(mark(X)) -> incr#(X) ->
    incr#(mark(X)) -> incr#(X)
    active#(repItems(cons(X,XS))) -> repItems#(XS) ->
    repItems#(ok(X)) -> repItems#(X)
    active#(repItems(cons(X,XS))) -> repItems#(XS) ->
    repItems#(mark(X)) -> repItems#(X)
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS)) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS))) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS))) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(repItems(X)) -> repItems#(active(X)) ->
    repItems#(ok(X)) -> repItems#(X)
    active#(repItems(X)) -> repItems#(active(X)) ->
    repItems#(mark(X)) -> repItems#(X)
    active#(repItems(X)) -> active#(X) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(repItems(X)) -> active#(X) ->
    active#(repItems(X)) -> active#(X)
    active#(repItems(X)) -> active#(X) ->
    active#(tail(X)) -> tail#(active(X))
    active#(repItems(X)) -> active#(X) ->
    active#(tail(X)) -> active#(X)
    active#(repItems(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(repItems(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(repItems(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(repItems(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(repItems(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(repItems(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(repItems(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(repItems(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(repItems(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(repItems(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(repItems(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(repItems(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(repItems(X)) -> active#(X) ->
    active#(s(X)) -> s#(active(X))
    active#(repItems(X)) -> active#(X) ->
    active#(s(X)) -> active#(X)
    active#(repItems(X)) -> active#(X) ->
    active#(incr(X)) -> incr#(active(X))
    active#(repItems(X)) -> active#(X) ->
    active#(incr(X)) -> active#(X)
    active#(repItems(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(repItems(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(repItems(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(repItems(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(repItems(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(repItems(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(repItems(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(repItems(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(repItems(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(repItems(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(repItems(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(repItems(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(repItems(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(repItems(X)) -> active#(X) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(repItems(X)) -> active#(X) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(repItems(X)) -> active#(X) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(tail(X)) -> tail#(active(X)) ->
    tail#(ok(X)) -> tail#(X)
    active#(tail(X)) -> tail#(active(X)) ->
    tail#(mark(X)) -> tail#(X)
    active#(tail(X)) -> active#(X) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(tail(X)) -> active#(X) ->
    active#(repItems(X)) -> active#(X)
    active#(tail(X)) -> active#(X) ->
    active#(tail(X)) -> tail#(active(X))
    active#(tail(X)) -> active#(X) -> active#(tail(X)) -> active#(X)
    active#(tail(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(tail(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(tail(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(tail(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(tail(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(tail(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(tail(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(tail(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(tail(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(tail(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(tail(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(tail(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(tail(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    active#(tail(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    active#(tail(X)) -> active#(X) ->
    active#(incr(X)) -> incr#(active(X))
    active#(tail(X)) -> active#(X) -> active#(incr(X)) -> active#(X)
    active#(tail(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(tail(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(tail(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(tail(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(tail(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(tail(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(tail(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(tail(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(tail(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(tail(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(tail(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(tail(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(tail(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(tail(X)) -> active#(X) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(tail(X)) -> active#(X) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(tail(X)) -> active#(X) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(pair(X1,X2)) -> pair#(active(X1),X2) ->
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
    active#(pair(X1,X2)) -> pair#(active(X1),X2) ->
    pair#(X1,mark(X2)) -> pair#(X1,X2)
    active#(pair(X1,X2)) -> pair#(active(X1),X2) ->
    pair#(mark(X1),X2) -> pair#(X1,X2)
    active#(pair(X1,X2)) -> pair#(X1,active(X2)) ->
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
    active#(pair(X1,X2)) -> pair#(X1,active(X2)) ->
    pair#(X1,mark(X2)) -> pair#(X1,X2)
    active#(pair(X1,X2)) -> pair#(X1,active(X2)) ->
    pair#(mark(X1),X2) -> pair#(X1,X2)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(repItems(X)) -> active#(X)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(tail(X)) -> tail#(active(X))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(tail(X)) -> active#(X)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> s#(active(X))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> active#(X)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(incr(X)) -> incr#(active(X))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(incr(X)) -> active#(X)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(pair(X1,X2)) -> active#(X2) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(repItems(X)) -> active#(X)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(tail(X)) -> tail#(active(X))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(tail(X)) -> active#(X)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(incr(X)) -> incr#(active(X))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(incr(X)) -> active#(X)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(pair(X1,X2)) -> active#(X1) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y) ->
    pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y) ->
    pair#(X1,mark(X2)) -> pair#(X1,X2)
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y) ->
    pair#(mark(X1),X2) -> pair#(X1,X2)
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS) ->
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS) ->
    zip#(X1,mark(X2)) -> zip#(X1,X2)
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS) ->
    zip#(mark(X1),X2) -> zip#(X1,X2)
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS)) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(zip(X1,X2)) -> zip#(active(X1),X2) ->
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
    active#(zip(X1,X2)) -> zip#(active(X1),X2) ->
    zip#(X1,mark(X2)) -> zip#(X1,X2)
    active#(zip(X1,X2)) -> zip#(active(X1),X2) ->
    zip#(mark(X1),X2) -> zip#(X1,X2)
    active#(zip(X1,X2)) -> zip#(X1,active(X2)) ->
    zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
    active#(zip(X1,X2)) -> zip#(X1,active(X2)) ->
    zip#(X1,mark(X2)) -> zip#(X1,X2)
    active#(zip(X1,X2)) -> zip#(X1,active(X2)) ->
    zip#(mark(X1),X2) -> zip#(X1,X2)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(repItems(X)) -> active#(X)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(tail(X)) -> tail#(active(X))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(tail(X)) -> active#(X)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> s#(active(X))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> active#(X)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(incr(X)) -> incr#(active(X))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(incr(X)) -> active#(X)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(zip(X1,X2)) -> active#(X2) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(repItems(X)) -> active#(X)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(tail(X)) -> tail#(active(X))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(tail(X)) -> active#(X)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(incr(X)) -> incr#(active(X))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(incr(X)) -> active#(X)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(zip(X1,X2)) -> active#(X1) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(take(s(N),cons(X,XS))) -> take#(N,XS) ->
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    active#(take(s(N),cons(X,XS))) -> take#(N,XS) ->
    take#(X1,mark(X2)) -> take#(X1,X2)
    active#(take(s(N),cons(X,XS))) -> take#(N,XS) ->
    take#(mark(X1),X2) -> take#(X1,X2)
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS)) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(take(X1,X2)) -> take#(active(X1),X2) ->
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    active#(take(X1,X2)) -> take#(active(X1),X2) ->
    take#(X1,mark(X2)) -> take#(X1,X2)
    active#(take(X1,X2)) -> take#(active(X1),X2) ->
    take#(mark(X1),X2) -> take#(X1,X2)
    active#(take(X1,X2)) -> take#(X1,active(X2)) ->
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    active#(take(X1,X2)) -> take#(X1,active(X2)) ->
    take#(X1,mark(X2)) -> take#(X1,X2)
    active#(take(X1,X2)) -> take#(X1,active(X2)) ->
    take#(mark(X1),X2) -> take#(X1,X2)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(repItems(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(tail(X)) -> tail#(active(X))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(tail(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> s#(active(X))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(incr(X)) -> incr#(active(X))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(incr(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(take(X1,X2)) -> active#(X2) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(take(X1,X2)) -> active#(X1) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(repItems(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(tail(X)) -> tail#(active(X))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(tail(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(incr(X)) -> incr#(active(X))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(incr(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(take(X1,X2)) -> active#(X1) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X)
    active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X)
    active#(s(X)) -> active#(X) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(s(X)) -> active#(X) -> active#(repItems(X)) -> active#(X)
    active#(s(X)) -> active#(X) -> active#(tail(X)) -> tail#(active(X))
    active#(s(X)) -> active#(X) -> active#(tail(X)) -> active#(X)
    active#(s(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(s(X)) -> active#(X) -> active#(pair(X1,X2)) -> active#(X2)
    active#(s(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(pair(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(s(X)) -> active#(X) -> active#(zip(X1,X2)) -> active#(X2)
    active#(s(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(zip(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(s(X)) -> active#(X) -> active#(take(X1,X2)) -> active#(X2)
    active#(s(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(take(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    active#(s(X)) -> active#(X) -> active#(incr(X)) -> incr#(active(X))
    active#(s(X)) -> active#(X) -> active#(incr(X)) -> active#(X)
    active#(s(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(s(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(s(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(s(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(s(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(s(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(s(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(s(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(s(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(s(X)) -> active#(X) -> active#(incr(cons(X,XS))) -> s#(X)
    active#(s(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(s(X)) -> active#(X) -> active#(oddNs()) -> incr#(pairNs())
    active#(s(X)) -> active#(X) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(s(X)) -> active#(X) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(repItems(X)) -> active#(X)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(tail(X)) -> tail#(active(X))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(tail(X)) -> active#(X)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(incr(X)) -> incr#(active(X))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(incr(X)) -> active#(X)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(incr(cons(X,XS))) -> s#(X) -> s#(ok(X)) -> s#(X)
    active#(incr(cons(X,XS))) -> s#(X) ->
    s#(mark(X)) -> s#(X)
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS)) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(incr(cons(X,XS))) -> incr#(XS) ->
    incr#(ok(X)) -> incr#(X)
    active#(incr(cons(X,XS))) -> incr#(XS) ->
    incr#(mark(X)) -> incr#(X)
    active#(incr(X)) -> incr#(active(X)) ->
    incr#(ok(X)) -> incr#(X)
    active#(incr(X)) -> incr#(active(X)) ->
    incr#(mark(X)) -> incr#(X)
    active#(incr(X)) -> active#(X) ->
    active#(repItems(X)) -> repItems#(active(X))
    active#(incr(X)) -> active#(X) ->
    active#(repItems(X)) -> active#(X)
    active#(incr(X)) -> active#(X) ->
    active#(tail(X)) -> tail#(active(X))
    active#(incr(X)) -> active#(X) -> active#(tail(X)) -> active#(X)
    active#(incr(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(X1,active(X2))
    active#(incr(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> active#(X2)
    active#(incr(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> pair#(active(X1),X2)
    active#(incr(X)) -> active#(X) ->
    active#(pair(X1,X2)) -> active#(X1)
    active#(incr(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(X1,active(X2))
    active#(incr(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> active#(X2)
    active#(incr(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> zip#(active(X1),X2)
    active#(incr(X)) -> active#(X) ->
    active#(zip(X1,X2)) -> active#(X1)
    active#(incr(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(incr(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(incr(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(incr(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(incr(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    active#(incr(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    active#(incr(X)) -> active#(X) ->
    active#(incr(X)) -> incr#(active(X))
    active#(incr(X)) -> active#(X) -> active#(incr(X)) -> active#(X)
    active#(incr(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(incr(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(incr(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,cons(X,repItems(XS)))
    active#(incr(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> cons#(X,repItems(XS))
    active#(incr(X)) -> active#(X) ->
    active#(repItems(cons(X,XS))) -> repItems#(XS)
    active#(incr(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> cons#(pair(X,Y),zip(XS,YS))
    active#(incr(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> pair#(X,Y)
    active#(incr(X)) -> active#(X) ->
    active#(zip(cons(X,XS),cons(Y,YS))) -> zip#(XS,YS)
    active#(incr(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> cons#(X,take(N,XS))
    active#(incr(X)) -> active#(X) ->
    active#(take(s(N),cons(X,XS))) -> take#(N,XS)
    active#(incr(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> cons#(s(X),incr(XS))
    active#(incr(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> s#(X)
    active#(incr(X)) -> active#(X) ->
    active#(incr(cons(X,XS))) -> incr#(XS)
    active#(incr(X)) -> active#(X) ->
    active#(oddNs()) -> incr#(pairNs())
    active#(incr(X)) -> active#(X) ->
    active#(pairNs()) -> cons#(0(),incr(oddNs()))
    active#(incr(X)) -> active#(X) ->
    active#(pairNs()) -> incr#(oddNs())
    active#(oddNs()) -> incr#(pairNs()) ->
    incr#(ok(X)) -> incr#(X)
    active#(oddNs()) -> incr#(pairNs()) ->
    incr#(mark(X)) -> incr#(X)
    active#(pairNs()) -> cons#(0(),incr(oddNs())) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(pairNs()) -> cons#(0(),incr(oddNs())) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(pairNs()) -> incr#(oddNs()) ->
    incr#(ok(X)) -> incr#(X)
    active#(pairNs()) -> incr#(oddNs()) -> incr#(mark(X)) -> incr#(X)
   SCC Processor:
    #sccs: 11
    #rules: 44
    #arcs: 825/6241
    DPs:
     top#(ok(X)) -> top#(active(X))
     top#(mark(X)) -> top#(proper(X))
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     active#(cons(X1,X2)) -> active#(X1)
     active#(incr(X)) -> active#(X)
     active#(s(X)) -> active#(X)
     active#(take(X1,X2)) -> active#(X1)
     active#(take(X1,X2)) -> active#(X2)
     active#(zip(X1,X2)) -> active#(X1)
     active#(zip(X1,X2)) -> active#(X2)
     active#(pair(X1,X2)) -> active#(X1)
     active#(pair(X1,X2)) -> active#(X2)
     active#(tail(X)) -> active#(X)
     active#(repItems(X)) -> active#(X)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(active#) = 0
     problem:
      DPs:
       
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed
    
    DPs:
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(incr(X)) -> proper#(X)
     proper#(s(X)) -> proper#(X)
     proper#(take(X1,X2)) -> proper#(X2)
     proper#(take(X1,X2)) -> proper#(X1)
     proper#(zip(X1,X2)) -> proper#(X2)
     proper#(zip(X1,X2)) -> proper#(X1)
     proper#(pair(X1,X2)) -> proper#(X2)
     proper#(pair(X1,X2)) -> proper#(X1)
     proper#(tail(X)) -> proper#(X)
     proper#(repItems(X)) -> proper#(X)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(proper#) = 0
     problem:
      DPs:
       
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed
    
    DPs:
     repItems#(mark(X)) -> repItems#(X)
     repItems#(ok(X)) -> repItems#(X)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(repItems#) = 0
     problem:
      DPs:
       
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed
    
    DPs:
     tail#(mark(X)) -> tail#(X)
     tail#(ok(X)) -> tail#(X)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(tail#) = 0
     problem:
      DPs:
       
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed
    
    DPs:
     pair#(mark(X1),X2) -> pair#(X1,X2)
     pair#(X1,mark(X2)) -> pair#(X1,X2)
     pair#(ok(X1),ok(X2)) -> pair#(X1,X2)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(pair#) = 1
     problem:
      DPs:
       pair#(mark(X1),X2) -> pair#(X1,X2)
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(pair#) = 0
      problem:
       DPs:
        
       TRS:
        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))))
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(incr(X)) -> incr(active(X))
        active(s(X)) -> s(active(X))
        active(take(X1,X2)) -> take(active(X1),X2)
        active(take(X1,X2)) -> take(X1,active(X2))
        active(zip(X1,X2)) -> zip(active(X1),X2)
        active(zip(X1,X2)) -> zip(X1,active(X2))
        active(pair(X1,X2)) -> pair(active(X1),X2)
        active(pair(X1,X2)) -> pair(X1,active(X2))
        active(tail(X)) -> tail(active(X))
        active(repItems(X)) -> repItems(active(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        incr(mark(X)) -> mark(incr(X))
        s(mark(X)) -> mark(s(X))
        take(mark(X1),X2) -> mark(take(X1,X2))
        take(X1,mark(X2)) -> mark(take(X1,X2))
        zip(mark(X1),X2) -> mark(zip(X1,X2))
        zip(X1,mark(X2)) -> mark(zip(X1,X2))
        pair(mark(X1),X2) -> mark(pair(X1,X2))
        pair(X1,mark(X2)) -> mark(pair(X1,X2))
        tail(mark(X)) -> mark(tail(X))
        repItems(mark(X)) -> mark(repItems(X))
        proper(pairNs()) -> ok(pairNs())
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(0()) -> ok(0())
        proper(incr(X)) -> incr(proper(X))
        proper(oddNs()) -> ok(oddNs())
        proper(s(X)) -> s(proper(X))
        proper(take(X1,X2)) -> take(proper(X1),proper(X2))
        proper(nil()) -> ok(nil())
        proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
        proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
        proper(tail(X)) -> tail(proper(X))
        proper(repItems(X)) -> repItems(proper(X))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        incr(ok(X)) -> ok(incr(X))
        s(ok(X)) -> ok(s(X))
        take(ok(X1),ok(X2)) -> ok(take(X1,X2))
        zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
        pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
        tail(ok(X)) -> ok(tail(X))
        repItems(ok(X)) -> ok(repItems(X))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed
    
    DPs:
     zip#(mark(X1),X2) -> zip#(X1,X2)
     zip#(X1,mark(X2)) -> zip#(X1,X2)
     zip#(ok(X1),ok(X2)) -> zip#(X1,X2)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(zip#) = 1
     problem:
      DPs:
       zip#(mark(X1),X2) -> zip#(X1,X2)
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(zip#) = 0
      problem:
       DPs:
        
       TRS:
        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))))
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(incr(X)) -> incr(active(X))
        active(s(X)) -> s(active(X))
        active(take(X1,X2)) -> take(active(X1),X2)
        active(take(X1,X2)) -> take(X1,active(X2))
        active(zip(X1,X2)) -> zip(active(X1),X2)
        active(zip(X1,X2)) -> zip(X1,active(X2))
        active(pair(X1,X2)) -> pair(active(X1),X2)
        active(pair(X1,X2)) -> pair(X1,active(X2))
        active(tail(X)) -> tail(active(X))
        active(repItems(X)) -> repItems(active(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        incr(mark(X)) -> mark(incr(X))
        s(mark(X)) -> mark(s(X))
        take(mark(X1),X2) -> mark(take(X1,X2))
        take(X1,mark(X2)) -> mark(take(X1,X2))
        zip(mark(X1),X2) -> mark(zip(X1,X2))
        zip(X1,mark(X2)) -> mark(zip(X1,X2))
        pair(mark(X1),X2) -> mark(pair(X1,X2))
        pair(X1,mark(X2)) -> mark(pair(X1,X2))
        tail(mark(X)) -> mark(tail(X))
        repItems(mark(X)) -> mark(repItems(X))
        proper(pairNs()) -> ok(pairNs())
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(0()) -> ok(0())
        proper(incr(X)) -> incr(proper(X))
        proper(oddNs()) -> ok(oddNs())
        proper(s(X)) -> s(proper(X))
        proper(take(X1,X2)) -> take(proper(X1),proper(X2))
        proper(nil()) -> ok(nil())
        proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
        proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
        proper(tail(X)) -> tail(proper(X))
        proper(repItems(X)) -> repItems(proper(X))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        incr(ok(X)) -> ok(incr(X))
        s(ok(X)) -> ok(s(X))
        take(ok(X1),ok(X2)) -> ok(take(X1,X2))
        zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
        pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
        tail(ok(X)) -> ok(tail(X))
        repItems(ok(X)) -> ok(repItems(X))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed
    
    DPs:
     take#(mark(X1),X2) -> take#(X1,X2)
     take#(X1,mark(X2)) -> take#(X1,X2)
     take#(ok(X1),ok(X2)) -> take#(X1,X2)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(take#) = 1
     problem:
      DPs:
       take#(mark(X1),X2) -> take#(X1,X2)
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(take#) = 0
      problem:
       DPs:
        
       TRS:
        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))))
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(incr(X)) -> incr(active(X))
        active(s(X)) -> s(active(X))
        active(take(X1,X2)) -> take(active(X1),X2)
        active(take(X1,X2)) -> take(X1,active(X2))
        active(zip(X1,X2)) -> zip(active(X1),X2)
        active(zip(X1,X2)) -> zip(X1,active(X2))
        active(pair(X1,X2)) -> pair(active(X1),X2)
        active(pair(X1,X2)) -> pair(X1,active(X2))
        active(tail(X)) -> tail(active(X))
        active(repItems(X)) -> repItems(active(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        incr(mark(X)) -> mark(incr(X))
        s(mark(X)) -> mark(s(X))
        take(mark(X1),X2) -> mark(take(X1,X2))
        take(X1,mark(X2)) -> mark(take(X1,X2))
        zip(mark(X1),X2) -> mark(zip(X1,X2))
        zip(X1,mark(X2)) -> mark(zip(X1,X2))
        pair(mark(X1),X2) -> mark(pair(X1,X2))
        pair(X1,mark(X2)) -> mark(pair(X1,X2))
        tail(mark(X)) -> mark(tail(X))
        repItems(mark(X)) -> mark(repItems(X))
        proper(pairNs()) -> ok(pairNs())
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(0()) -> ok(0())
        proper(incr(X)) -> incr(proper(X))
        proper(oddNs()) -> ok(oddNs())
        proper(s(X)) -> s(proper(X))
        proper(take(X1,X2)) -> take(proper(X1),proper(X2))
        proper(nil()) -> ok(nil())
        proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
        proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
        proper(tail(X)) -> tail(proper(X))
        proper(repItems(X)) -> repItems(proper(X))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        incr(ok(X)) -> ok(incr(X))
        s(ok(X)) -> ok(s(X))
        take(ok(X1),ok(X2)) -> ok(take(X1,X2))
        zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
        pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
        tail(ok(X)) -> ok(tail(X))
        repItems(ok(X)) -> ok(repItems(X))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(ok(X)) -> s#(X)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed
    
    DPs:
     incr#(mark(X)) -> incr#(X)
     incr#(ok(X)) -> incr#(X)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(incr#) = 0
     problem:
      DPs:
       
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Qed
    
    DPs:
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    TRS:
     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))))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(incr(X)) -> incr(active(X))
     active(s(X)) -> s(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(zip(X1,X2)) -> zip(active(X1),X2)
     active(zip(X1,X2)) -> zip(X1,active(X2))
     active(pair(X1,X2)) -> pair(active(X1),X2)
     active(pair(X1,X2)) -> pair(X1,active(X2))
     active(tail(X)) -> tail(active(X))
     active(repItems(X)) -> repItems(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     incr(mark(X)) -> mark(incr(X))
     s(mark(X)) -> mark(s(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     zip(mark(X1),X2) -> mark(zip(X1,X2))
     zip(X1,mark(X2)) -> mark(zip(X1,X2))
     pair(mark(X1),X2) -> mark(pair(X1,X2))
     pair(X1,mark(X2)) -> mark(pair(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     repItems(mark(X)) -> mark(repItems(X))
     proper(pairNs()) -> ok(pairNs())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(incr(X)) -> incr(proper(X))
     proper(oddNs()) -> ok(oddNs())
     proper(s(X)) -> s(proper(X))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
     proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
     proper(tail(X)) -> tail(proper(X))
     proper(repItems(X)) -> repItems(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     incr(ok(X)) -> ok(incr(X))
     s(ok(X)) -> ok(s(X))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
     pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     repItems(ok(X)) -> ok(repItems(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Subterm Criterion Processor:
     simple projection:
      pi(cons#) = 1
     problem:
      DPs:
       cons#(mark(X1),X2) -> cons#(X1,X2)
      TRS:
       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))))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(incr(X)) -> incr(active(X))
       active(s(X)) -> s(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(zip(X1,X2)) -> zip(active(X1),X2)
       active(zip(X1,X2)) -> zip(X1,active(X2))
       active(pair(X1,X2)) -> pair(active(X1),X2)
       active(pair(X1,X2)) -> pair(X1,active(X2))
       active(tail(X)) -> tail(active(X))
       active(repItems(X)) -> repItems(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       incr(mark(X)) -> mark(incr(X))
       s(mark(X)) -> mark(s(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       zip(mark(X1),X2) -> mark(zip(X1,X2))
       zip(X1,mark(X2)) -> mark(zip(X1,X2))
       pair(mark(X1),X2) -> mark(pair(X1,X2))
       pair(X1,mark(X2)) -> mark(pair(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       repItems(mark(X)) -> mark(repItems(X))
       proper(pairNs()) -> ok(pairNs())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(incr(X)) -> incr(proper(X))
       proper(oddNs()) -> ok(oddNs())
       proper(s(X)) -> s(proper(X))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
       proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
       proper(tail(X)) -> tail(proper(X))
       proper(repItems(X)) -> repItems(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       incr(ok(X)) -> ok(incr(X))
       s(ok(X)) -> ok(s(X))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
       pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       repItems(ok(X)) -> ok(repItems(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Subterm Criterion Processor:
      simple projection:
       pi(cons#) = 0
      problem:
       DPs:
        
       TRS:
        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))))
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(incr(X)) -> incr(active(X))
        active(s(X)) -> s(active(X))
        active(take(X1,X2)) -> take(active(X1),X2)
        active(take(X1,X2)) -> take(X1,active(X2))
        active(zip(X1,X2)) -> zip(active(X1),X2)
        active(zip(X1,X2)) -> zip(X1,active(X2))
        active(pair(X1,X2)) -> pair(active(X1),X2)
        active(pair(X1,X2)) -> pair(X1,active(X2))
        active(tail(X)) -> tail(active(X))
        active(repItems(X)) -> repItems(active(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        incr(mark(X)) -> mark(incr(X))
        s(mark(X)) -> mark(s(X))
        take(mark(X1),X2) -> mark(take(X1,X2))
        take(X1,mark(X2)) -> mark(take(X1,X2))
        zip(mark(X1),X2) -> mark(zip(X1,X2))
        zip(X1,mark(X2)) -> mark(zip(X1,X2))
        pair(mark(X1),X2) -> mark(pair(X1,X2))
        pair(X1,mark(X2)) -> mark(pair(X1,X2))
        tail(mark(X)) -> mark(tail(X))
        repItems(mark(X)) -> mark(repItems(X))
        proper(pairNs()) -> ok(pairNs())
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(0()) -> ok(0())
        proper(incr(X)) -> incr(proper(X))
        proper(oddNs()) -> ok(oddNs())
        proper(s(X)) -> s(proper(X))
        proper(take(X1,X2)) -> take(proper(X1),proper(X2))
        proper(nil()) -> ok(nil())
        proper(zip(X1,X2)) -> zip(proper(X1),proper(X2))
        proper(pair(X1,X2)) -> pair(proper(X1),proper(X2))
        proper(tail(X)) -> tail(proper(X))
        proper(repItems(X)) -> repItems(proper(X))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        incr(ok(X)) -> ok(incr(X))
        s(ok(X)) -> ok(s(X))
        take(ok(X1),ok(X2)) -> ok(take(X1,X2))
        zip(ok(X1),ok(X2)) -> ok(zip(X1,X2))
        pair(ok(X1),ok(X2)) -> ok(pair(X1,X2))
        tail(ok(X)) -> ok(tail(X))
        repItems(ok(X)) -> ok(repItems(X))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed