(STRATEGY
    INNERMOST)

(VAR
    N X X1 X2 XS Y YS)
(DATATYPES
    A = µX.< pairNs, mark(X), 0, oddNs, nil, ok(X) >)
(SIGNATURES
    active :: [A] -> A
    cons :: [A x A] -> A
    incr :: [A] -> A
    s :: [A] -> A
    take :: [A x A] -> A
    zip :: [A x A] -> A
    pair :: [A x A] -> A
    tail :: [A] -> A
    repItems :: [A] -> A
    proper :: [A] -> A
    top :: [A] -> A)
(RULES
    active(pairNs()) ->
      mark(cons(0(),incr(oddNs())))
    active(oddNs()) ->
      mark(incr(pairNs()))
    active(incr(cons(X,XS))) ->
      mark(cons(s(X),incr(XS)))
    active(take(0(),XS)) ->
      mark(nil())
    active(take(s(N),cons(X,XS))) ->
      mark(cons(X,take(N,XS)))
    active(zip(nil(),XS)) ->
      mark(nil())
    active(zip(X,nil())) ->
      mark(nil())
    active(zip(cons(X,XS)
              ,cons(Y,YS))) ->
      mark(cons(pair(X,Y),zip(XS,YS)))
    active(tail(cons(X,XS))) ->
      mark(XS)
    active(repItems(nil())) ->
      mark(nil())
    active(repItems(cons(X,XS))) ->
      mark(cons(X
               ,cons(X,repItems(XS))))
    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)))