MAYBE

Problem:
 active(eq(0(),0())) -> mark(true())
 active(eq(s(X),s(Y))) -> mark(eq(X,Y))
 active(eq(X,Y)) -> mark(false())
 active(inf(X)) -> mark(cons(X,inf(s(X))))
 active(take(0(),X)) -> mark(nil())
 active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
 active(length(nil())) -> mark(0())
 active(length(cons(X,L))) -> mark(s(length(L)))
 active(inf(X)) -> inf(active(X))
 active(take(X1,X2)) -> take(active(X1),X2)
 active(take(X1,X2)) -> take(X1,active(X2))
 active(length(X)) -> length(active(X))
 inf(mark(X)) -> mark(inf(X))
 take(mark(X1),X2) -> mark(take(X1,X2))
 take(X1,mark(X2)) -> mark(take(X1,X2))
 length(mark(X)) -> mark(length(X))
 proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(true()) -> ok(true())
 proper(s(X)) -> s(proper(X))
 proper(false()) -> ok(false())
 proper(inf(X)) -> inf(proper(X))
 proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
 proper(take(X1,X2)) -> take(proper(X1),proper(X2))
 proper(nil()) -> ok(nil())
 proper(length(X)) -> length(proper(X))
 eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
 s(ok(X)) -> ok(s(X))
 inf(ok(X)) -> ok(inf(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 take(ok(X1),ok(X2)) -> ok(take(X1,X2))
 length(ok(X)) -> ok(length(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))
 any(X) -> s(X)
 any(proper(X)) -> any(any(any(X)))

Proof:
 DP Processor:
  DPs:
   active#(eq(s(X),s(Y))) -> eq#(X,Y)
   active#(inf(X)) -> s#(X)
   active#(inf(X)) -> inf#(s(X))
   active#(inf(X)) -> cons#(X,inf(s(X)))
   active#(take(s(X),cons(Y,L))) -> take#(X,L)
   active#(take(s(X),cons(Y,L))) -> cons#(Y,take(X,L))
   active#(length(cons(X,L))) -> length#(L)
   active#(length(cons(X,L))) -> s#(length(L))
   active#(inf(X)) -> active#(X)
   active#(inf(X)) -> inf#(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#(length(X)) -> active#(X)
   active#(length(X)) -> length#(active(X))
   inf#(mark(X)) -> inf#(X)
   take#(mark(X1),X2) -> take#(X1,X2)
   take#(X1,mark(X2)) -> take#(X1,X2)
   length#(mark(X)) -> length#(X)
   proper#(eq(X1,X2)) -> proper#(X2)
   proper#(eq(X1,X2)) -> proper#(X1)
   proper#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
   proper#(s(X)) -> proper#(X)
   proper#(s(X)) -> s#(proper(X))
   proper#(inf(X)) -> proper#(X)
   proper#(inf(X)) -> inf#(proper(X))
   proper#(cons(any(X1),X2)) -> proper#(X2)
   proper#(cons(any(X1),X2)) -> any#(proper(X2))
   proper#(cons(any(X1),X2)) -> proper#(X1)
   proper#(cons(any(X1),X2)) -> any#(proper(X1))
   proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
   proper#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
   proper#(take(X1,X2)) -> proper#(X2)
   proper#(take(X1,X2)) -> proper#(X1)
   proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
   proper#(length(X)) -> proper#(X)
   proper#(length(X)) -> length#(proper(X))
   eq#(ok(X1),ok(X2)) -> eq#(X1,X2)
   s#(ok(X)) -> s#(X)
   inf#(ok(X)) -> inf#(X)
   cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
   take#(ok(X1),ok(X2)) -> take#(X1,X2)
   length#(ok(X)) -> length#(X)
   top#(mark(X)) -> proper#(X)
   top#(mark(X)) -> top#(proper(X))
   top#(ok(X)) -> active#(X)
   top#(ok(X)) -> top#(active(X))
   any#(X) -> s#(X)
   any#(proper(X)) -> any#(X)
   any#(proper(X)) -> any#(any(X))
   any#(proper(X)) -> any#(any(any(X)))
  TRS:
   active(eq(0(),0())) -> mark(true())
   active(eq(s(X),s(Y))) -> mark(eq(X,Y))
   active(eq(X,Y)) -> mark(false())
   active(inf(X)) -> mark(cons(X,inf(s(X))))
   active(take(0(),X)) -> mark(nil())
   active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
   active(length(nil())) -> mark(0())
   active(length(cons(X,L))) -> mark(s(length(L)))
   active(inf(X)) -> inf(active(X))
   active(take(X1,X2)) -> take(active(X1),X2)
   active(take(X1,X2)) -> take(X1,active(X2))
   active(length(X)) -> length(active(X))
   inf(mark(X)) -> mark(inf(X))
   take(mark(X1),X2) -> mark(take(X1,X2))
   take(X1,mark(X2)) -> mark(take(X1,X2))
   length(mark(X)) -> mark(length(X))
   proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
   proper(0()) -> ok(0())
   proper(true()) -> ok(true())
   proper(s(X)) -> s(proper(X))
   proper(false()) -> ok(false())
   proper(inf(X)) -> inf(proper(X))
   proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
   proper(take(X1,X2)) -> take(proper(X1),proper(X2))
   proper(nil()) -> ok(nil())
   proper(length(X)) -> length(proper(X))
   eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
   s(ok(X)) -> ok(s(X))
   inf(ok(X)) -> ok(inf(X))
   cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
   take(ok(X1),ok(X2)) -> ok(take(X1,X2))
   length(ok(X)) -> ok(length(X))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
   any(X) -> s(X)
   any(proper(X)) -> any(any(any(X)))
  TDG Processor:
   DPs:
    active#(eq(s(X),s(Y))) -> eq#(X,Y)
    active#(inf(X)) -> s#(X)
    active#(inf(X)) -> inf#(s(X))
    active#(inf(X)) -> cons#(X,inf(s(X)))
    active#(take(s(X),cons(Y,L))) -> take#(X,L)
    active#(take(s(X),cons(Y,L))) -> cons#(Y,take(X,L))
    active#(length(cons(X,L))) -> length#(L)
    active#(length(cons(X,L))) -> s#(length(L))
    active#(inf(X)) -> active#(X)
    active#(inf(X)) -> inf#(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#(length(X)) -> active#(X)
    active#(length(X)) -> length#(active(X))
    inf#(mark(X)) -> inf#(X)
    take#(mark(X1),X2) -> take#(X1,X2)
    take#(X1,mark(X2)) -> take#(X1,X2)
    length#(mark(X)) -> length#(X)
    proper#(eq(X1,X2)) -> proper#(X2)
    proper#(eq(X1,X2)) -> proper#(X1)
    proper#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> s#(proper(X))
    proper#(inf(X)) -> proper#(X)
    proper#(inf(X)) -> inf#(proper(X))
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(length(X)) -> proper#(X)
    proper#(length(X)) -> length#(proper(X))
    eq#(ok(X1),ok(X2)) -> eq#(X1,X2)
    s#(ok(X)) -> s#(X)
    inf#(ok(X)) -> inf#(X)
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    length#(ok(X)) -> length#(X)
    top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X))
    any#(X) -> s#(X)
    any#(proper(X)) -> any#(X)
    any#(proper(X)) -> any#(any(X))
    any#(proper(X)) -> any#(any(any(X)))
   TRS:
    active(eq(0(),0())) -> mark(true())
    active(eq(s(X),s(Y))) -> mark(eq(X,Y))
    active(eq(X,Y)) -> mark(false())
    active(inf(X)) -> mark(cons(X,inf(s(X))))
    active(take(0(),X)) -> mark(nil())
    active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
    active(length(nil())) -> mark(0())
    active(length(cons(X,L))) -> mark(s(length(L)))
    active(inf(X)) -> inf(active(X))
    active(take(X1,X2)) -> take(active(X1),X2)
    active(take(X1,X2)) -> take(X1,active(X2))
    active(length(X)) -> length(active(X))
    inf(mark(X)) -> mark(inf(X))
    take(mark(X1),X2) -> mark(take(X1,X2))
    take(X1,mark(X2)) -> mark(take(X1,X2))
    length(mark(X)) -> mark(length(X))
    proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
    proper(0()) -> ok(0())
    proper(true()) -> ok(true())
    proper(s(X)) -> s(proper(X))
    proper(false()) -> ok(false())
    proper(inf(X)) -> inf(proper(X))
    proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
    proper(take(X1,X2)) -> take(proper(X1),proper(X2))
    proper(nil()) -> ok(nil())
    proper(length(X)) -> length(proper(X))
    eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
    s(ok(X)) -> ok(s(X))
    inf(ok(X)) -> ok(inf(X))
    cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    take(ok(X1),ok(X2)) -> ok(take(X1,X2))
    length(ok(X)) -> ok(length(X))
    top(mark(X)) -> top(proper(X))
    top(ok(X)) -> top(active(X))
    any(X) -> s(X)
    any(proper(X)) -> any(any(any(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#(length(X)) -> length#(active(X))
    top#(ok(X)) -> active#(X) -> active#(length(X)) -> active#(X)
    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#(inf(X)) -> inf#(active(X))
    top#(ok(X)) -> active#(X) -> active#(inf(X)) -> active#(X)
    top#(ok(X)) -> active#(X) ->
    active#(length(cons(X,L))) -> s#(length(L))
    top#(ok(X)) -> active#(X) -> active#(length(cons(X,L))) -> length#(L)
    top#(ok(X)) -> active#(X) ->
    active#(take(s(X),cons(Y,L))) -> cons#(Y,take(X,L))
    top#(ok(X)) -> active#(X) ->
    active#(take(s(X),cons(Y,L))) -> take#(X,L)
    top#(ok(X)) -> active#(X) -> active#(inf(X)) -> cons#(X,inf(s(X)))
    top#(ok(X)) -> active#(X) -> active#(inf(X)) -> inf#(s(X))
    top#(ok(X)) -> active#(X) -> active#(inf(X)) -> s#(X)
    top#(ok(X)) -> active#(X) -> active#(eq(s(X),s(Y))) -> eq#(X,Y)
    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#(length(X)) -> length#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(length(X)) -> proper#(X)
    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#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(inf(X)) -> inf#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(inf(X)) -> proper#(X)
    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#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(eq(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(eq(X1,X2)) -> proper#(X2)
    any#(proper(X)) -> any#(any(any(X))) ->
    any#(proper(X)) -> any#(any(any(X)))
    any#(proper(X)) -> any#(any(any(X))) ->
    any#(proper(X)) -> any#(any(X))
    any#(proper(X)) -> any#(any(any(X))) ->
    any#(proper(X)) -> any#(X)
    any#(proper(X)) -> any#(any(any(X))) -> any#(X) -> s#(X)
    any#(proper(X)) -> any#(any(X)) ->
    any#(proper(X)) -> any#(any(any(X)))
    any#(proper(X)) -> any#(any(X)) ->
    any#(proper(X)) -> any#(any(X))
    any#(proper(X)) -> any#(any(X)) -> any#(proper(X)) -> any#(X)
    any#(proper(X)) -> any#(any(X)) -> any#(X) -> s#(X)
    any#(proper(X)) -> any#(X) -> any#(proper(X)) -> any#(any(any(X)))
    any#(proper(X)) -> any#(X) -> any#(proper(X)) -> any#(any(X))
    any#(proper(X)) -> any#(X) -> any#(proper(X)) -> any#(X)
    any#(proper(X)) -> any#(X) -> any#(X) -> s#(X)
    any#(X) -> s#(X) -> s#(ok(X)) -> s#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(length(X)) -> proper#(X) ->
    proper#(length(X)) -> proper#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(length(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(length(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(length(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(length(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(length(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(length(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(length(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(length(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(length(X)) -> proper#(X) ->
    proper#(inf(X)) -> inf#(proper(X))
    proper#(length(X)) -> proper#(X) ->
    proper#(inf(X)) -> proper#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(length(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(length(X)) -> proper#(X) ->
    proper#(eq(X1,X2)) -> proper#(X1)
    proper#(length(X)) -> proper#(X) ->
    proper#(eq(X1,X2)) -> proper#(X2)
    proper#(length(X)) -> length#(proper(X)) ->
    length#(ok(X)) -> length#(X)
    proper#(length(X)) -> length#(proper(X)) ->
    length#(mark(X)) -> length#(X)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> proper#(X)
    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#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(inf(X)) -> inf#(proper(X))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(inf(X)) -> proper#(X)
    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#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(eq(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X2) ->
    proper#(eq(X1,X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> proper#(X)
    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#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(inf(X)) -> inf#(proper(X))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(inf(X)) -> proper#(X)
    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#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(eq(X1,X2)) -> proper#(X1)
    proper#(take(X1,X2)) -> proper#(X1) ->
    proper#(eq(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#(cons(any(X1),X2)) -> any#(any(proper(X1))) ->
    any#(proper(X)) -> any#(any(any(X)))
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1))) ->
    any#(proper(X)) -> any#(any(X))
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1))) ->
    any#(proper(X)) -> any#(X)
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1))) ->
    any#(X) -> s#(X)
    proper#(cons(any(X1),X2)) -> any#(proper(X2)) ->
    any#(proper(X)) -> any#(any(any(X)))
    proper#(cons(any(X1),X2)) -> any#(proper(X2)) ->
    any#(proper(X)) -> any#(any(X))
    proper#(cons(any(X1),X2)) -> any#(proper(X2)) ->
    any#(proper(X)) -> any#(X)
    proper#(cons(any(X1),X2)) -> any#(proper(X2)) ->
    any#(X) -> s#(X)
    proper#(cons(any(X1),X2)) -> any#(proper(X1)) ->
    any#(proper(X)) -> any#(any(any(X)))
    proper#(cons(any(X1),X2)) -> any#(proper(X1)) ->
    any#(proper(X)) -> any#(any(X))
    proper#(cons(any(X1),X2)) -> any#(proper(X1)) ->
    any#(proper(X)) -> any#(X)
    proper#(cons(any(X1),X2)) -> any#(proper(X1)) ->
    any#(X) -> s#(X)
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(length(X)) -> proper#(X)
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(inf(X)) -> inf#(proper(X))
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(inf(X)) -> proper#(X)
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(eq(X1,X2)) -> proper#(X1)
    proper#(cons(any(X1),X2)) -> proper#(X2) ->
    proper#(eq(X1,X2)) -> proper#(X2)
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(length(X)) -> proper#(X)
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(inf(X)) -> inf#(proper(X))
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(inf(X)) -> proper#(X)
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(eq(X1,X2)) -> proper#(X1)
    proper#(cons(any(X1),X2)) -> proper#(X1) ->
    proper#(eq(X1,X2)) -> proper#(X2)
    proper#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2))) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    proper#(inf(X)) -> proper#(X) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(inf(X)) -> proper#(X) -> proper#(length(X)) -> proper#(X)
    proper#(inf(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(inf(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(inf(X)) -> proper#(X) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(inf(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(inf(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(inf(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(inf(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(inf(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(inf(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(inf(X)) -> proper#(X) ->
    proper#(inf(X)) -> inf#(proper(X))
    proper#(inf(X)) -> proper#(X) -> proper#(inf(X)) -> proper#(X)
    proper#(inf(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(inf(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(inf(X)) -> proper#(X) ->
    proper#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(inf(X)) -> proper#(X) -> proper#(eq(X1,X2)) -> proper#(X1)
    proper#(inf(X)) -> proper#(X) ->
    proper#(eq(X1,X2)) -> proper#(X2)
    proper#(inf(X)) -> inf#(proper(X)) -> inf#(ok(X)) -> inf#(X)
    proper#(inf(X)) -> inf#(proper(X)) -> inf#(mark(X)) -> inf#(X)
    proper#(s(X)) -> proper#(X) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(length(X)) -> proper#(X)
    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#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(inf(X)) -> inf#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(inf(X)) -> proper#(X)
    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#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(eq(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(eq(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> proper#(X)
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(inf(X)) -> inf#(proper(X))
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(inf(X)) -> proper#(X)
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(eq(X1,X2)) -> proper#(X1)
    proper#(eq(X1,X2)) -> proper#(X2) ->
    proper#(eq(X1,X2)) -> proper#(X2)
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> proper#(X)
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> take#(proper(X1),proper(X2))
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X1)
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(take(X1,X2)) -> proper#(X2)
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> cons#(any(any(proper(X1))),any(proper(X2)))
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> any#(any(proper(X1)))
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X1))
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> proper#(X1)
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> any#(proper(X2))
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(cons(any(X1),X2)) -> proper#(X2)
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(inf(X)) -> inf#(proper(X))
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(inf(X)) -> proper#(X)
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(eq(X1,X2)) -> eq#(proper(X1),proper(X2))
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(eq(X1,X2)) -> proper#(X1)
    proper#(eq(X1,X2)) -> proper#(X1) ->
    proper#(eq(X1,X2)) -> proper#(X2)
    proper#(eq(X1,X2)) -> eq#(proper(X1),proper(X2)) ->
    eq#(ok(X1),ok(X2)) -> eq#(X1,X2)
    length#(ok(X)) -> length#(X) -> length#(ok(X)) -> length#(X)
    length#(ok(X)) -> length#(X) -> length#(mark(X)) -> length#(X)
    length#(mark(X)) -> length#(X) -> length#(ok(X)) -> length#(X)
    length#(mark(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    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)
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    inf#(ok(X)) -> inf#(X) -> inf#(ok(X)) -> inf#(X)
    inf#(ok(X)) -> inf#(X) -> inf#(mark(X)) -> inf#(X)
    inf#(mark(X)) -> inf#(X) -> inf#(ok(X)) -> inf#(X)
    inf#(mark(X)) -> inf#(X) -> inf#(mark(X)) -> inf#(X)
    s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    eq#(ok(X1),ok(X2)) -> eq#(X1,X2) ->
    eq#(ok(X1),ok(X2)) -> eq#(X1,X2)
    active#(length(cons(X,L))) -> length#(L) ->
    length#(ok(X)) -> length#(X)
    active#(length(cons(X,L))) -> length#(L) ->
    length#(mark(X)) -> length#(X)
    active#(length(cons(X,L))) -> s#(length(L)) ->
    s#(ok(X)) -> s#(X)
    active#(length(X)) -> length#(active(X)) ->
    length#(ok(X)) -> length#(X)
    active#(length(X)) -> length#(active(X)) ->
    length#(mark(X)) -> length#(X)
    active#(length(X)) -> active#(X) ->
    active#(length(X)) -> length#(active(X))
    active#(length(X)) -> active#(X) ->
    active#(length(X)) -> active#(X)
    active#(length(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(length(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(length(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(length(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(length(X)) -> active#(X) ->
    active#(inf(X)) -> inf#(active(X))
    active#(length(X)) -> active#(X) ->
    active#(inf(X)) -> active#(X)
    active#(length(X)) -> active#(X) ->
    active#(length(cons(X,L))) -> s#(length(L))
    active#(length(X)) -> active#(X) ->
    active#(length(cons(X,L))) -> length#(L)
    active#(length(X)) -> active#(X) ->
    active#(take(s(X),cons(Y,L))) -> cons#(Y,take(X,L))
    active#(length(X)) -> active#(X) ->
    active#(take(s(X),cons(Y,L))) -> take#(X,L)
    active#(length(X)) -> active#(X) ->
    active#(inf(X)) -> cons#(X,inf(s(X)))
    active#(length(X)) -> active#(X) ->
    active#(inf(X)) -> inf#(s(X))
    active#(length(X)) -> active#(X) -> active#(inf(X)) -> s#(X)
    active#(length(X)) -> active#(X) ->
    active#(eq(s(X),s(Y))) -> eq#(X,Y)
    active#(take(s(X),cons(Y,L))) -> take#(X,L) ->
    take#(ok(X1),ok(X2)) -> take#(X1,X2)
    active#(take(s(X),cons(Y,L))) -> take#(X,L) ->
    take#(X1,mark(X2)) -> take#(X1,X2)
    active#(take(s(X),cons(Y,L))) -> take#(X,L) ->
    take#(mark(X1),X2) -> take#(X1,X2)
    active#(take(s(X),cons(Y,L))) -> cons#(Y,take(X,L)) ->
    cons#(ok(X1),ok(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#(length(X)) -> length#(active(X))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(length(X)) -> active#(X)
    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#(inf(X)) -> inf#(active(X))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(inf(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(length(cons(X,L))) -> s#(length(L))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(length(cons(X,L))) -> length#(L)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(take(s(X),cons(Y,L))) -> cons#(Y,take(X,L))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(take(s(X),cons(Y,L))) -> take#(X,L)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(inf(X)) -> cons#(X,inf(s(X)))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(inf(X)) -> inf#(s(X))
    active#(take(X1,X2)) -> active#(X2) ->
    active#(inf(X)) -> s#(X)
    active#(take(X1,X2)) -> active#(X2) ->
    active#(eq(s(X),s(Y))) -> eq#(X,Y)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(length(X)) -> length#(active(X))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(length(X)) -> active#(X)
    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#(inf(X)) -> inf#(active(X))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(inf(X)) -> active#(X)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(length(cons(X,L))) -> s#(length(L))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(length(cons(X,L))) -> length#(L)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(take(s(X),cons(Y,L))) -> cons#(Y,take(X,L))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(take(s(X),cons(Y,L))) -> take#(X,L)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(inf(X)) -> cons#(X,inf(s(X)))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(inf(X)) -> inf#(s(X))
    active#(take(X1,X2)) -> active#(X1) ->
    active#(inf(X)) -> s#(X)
    active#(take(X1,X2)) -> active#(X1) ->
    active#(eq(s(X),s(Y))) -> eq#(X,Y)
    active#(inf(X)) -> cons#(X,inf(s(X))) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(inf(X)) -> inf#(s(X)) -> inf#(ok(X)) -> inf#(X)
    active#(inf(X)) -> inf#(s(X)) -> inf#(mark(X)) -> inf#(X)
    active#(inf(X)) -> inf#(active(X)) -> inf#(ok(X)) -> inf#(X)
    active#(inf(X)) -> inf#(active(X)) -> inf#(mark(X)) -> inf#(X)
    active#(inf(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    active#(inf(X)) -> active#(X) ->
    active#(length(X)) -> length#(active(X))
    active#(inf(X)) -> active#(X) -> active#(length(X)) -> active#(X)
    active#(inf(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(X1,active(X2))
    active#(inf(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X2)
    active#(inf(X)) -> active#(X) ->
    active#(take(X1,X2)) -> take#(active(X1),X2)
    active#(inf(X)) -> active#(X) ->
    active#(take(X1,X2)) -> active#(X1)
    active#(inf(X)) -> active#(X) ->
    active#(inf(X)) -> inf#(active(X))
    active#(inf(X)) -> active#(X) -> active#(inf(X)) -> active#(X)
    active#(inf(X)) -> active#(X) ->
    active#(length(cons(X,L))) -> s#(length(L))
    active#(inf(X)) -> active#(X) ->
    active#(length(cons(X,L))) -> length#(L)
    active#(inf(X)) -> active#(X) ->
    active#(take(s(X),cons(Y,L))) -> cons#(Y,take(X,L))
    active#(inf(X)) -> active#(X) ->
    active#(take(s(X),cons(Y,L))) -> take#(X,L)
    active#(inf(X)) -> active#(X) ->
    active#(inf(X)) -> cons#(X,inf(s(X)))
    active#(inf(X)) -> active#(X) -> active#(inf(X)) -> inf#(s(X))
    active#(inf(X)) -> active#(X) -> active#(inf(X)) -> s#(X)
    active#(inf(X)) -> active#(X) ->
    active#(eq(s(X),s(Y))) -> eq#(X,Y)
    active#(eq(s(X),s(Y))) -> eq#(X,Y) -> eq#(ok(X1),ok(X2)) -> eq#(X1,X2)
   SCC Processor:
    #sccs: 10
    #rules: 28
    #arcs: 345/2704
    DPs:
     top#(ok(X)) -> top#(active(X))
     top#(mark(X)) -> top#(proper(X))
    TRS:
     active(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    Open
    
    DPs:
     active#(inf(X)) -> active#(X)
     active#(take(X1,X2)) -> active#(X1)
     active#(take(X1,X2)) -> active#(X2)
     active#(length(X)) -> active#(X)
    TRS:
     active(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    Subterm Criterion Processor:
     simple projection:
      pi(active#) = 0
     problem:
      DPs:
       
      TRS:
       active(eq(0(),0())) -> mark(true())
       active(eq(s(X),s(Y))) -> mark(eq(X,Y))
       active(eq(X,Y)) -> mark(false())
       active(inf(X)) -> mark(cons(X,inf(s(X))))
       active(take(0(),X)) -> mark(nil())
       active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
       active(length(nil())) -> mark(0())
       active(length(cons(X,L))) -> mark(s(length(L)))
       active(inf(X)) -> inf(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(length(X)) -> length(active(X))
       inf(mark(X)) -> mark(inf(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       length(mark(X)) -> mark(length(X))
       proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(true()) -> ok(true())
       proper(s(X)) -> s(proper(X))
       proper(false()) -> ok(false())
       proper(inf(X)) -> inf(proper(X))
       proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(length(X)) -> length(proper(X))
       eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
       s(ok(X)) -> ok(s(X))
       inf(ok(X)) -> ok(inf(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       length(ok(X)) -> ok(length(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
       any(X) -> s(X)
       any(proper(X)) -> any(any(any(X)))
     Qed
    
    DPs:
     proper#(eq(X1,X2)) -> proper#(X2)
     proper#(eq(X1,X2)) -> proper#(X1)
     proper#(s(X)) -> proper#(X)
     proper#(inf(X)) -> proper#(X)
     proper#(cons(any(X1),X2)) -> proper#(X2)
     proper#(cons(any(X1),X2)) -> proper#(X1)
     proper#(take(X1,X2)) -> proper#(X2)
     proper#(take(X1,X2)) -> proper#(X1)
     proper#(length(X)) -> proper#(X)
    TRS:
     active(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    Subterm Criterion Processor:
     simple projection:
      pi(proper#) = 0
     problem:
      DPs:
       
      TRS:
       active(eq(0(),0())) -> mark(true())
       active(eq(s(X),s(Y))) -> mark(eq(X,Y))
       active(eq(X,Y)) -> mark(false())
       active(inf(X)) -> mark(cons(X,inf(s(X))))
       active(take(0(),X)) -> mark(nil())
       active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
       active(length(nil())) -> mark(0())
       active(length(cons(X,L))) -> mark(s(length(L)))
       active(inf(X)) -> inf(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(length(X)) -> length(active(X))
       inf(mark(X)) -> mark(inf(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       length(mark(X)) -> mark(length(X))
       proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(true()) -> ok(true())
       proper(s(X)) -> s(proper(X))
       proper(false()) -> ok(false())
       proper(inf(X)) -> inf(proper(X))
       proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(length(X)) -> length(proper(X))
       eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
       s(ok(X)) -> ok(s(X))
       inf(ok(X)) -> ok(inf(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       length(ok(X)) -> ok(length(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
       any(X) -> s(X)
       any(proper(X)) -> any(any(any(X)))
     Qed
    
    DPs:
     length#(mark(X)) -> length#(X)
     length#(ok(X)) -> length#(X)
    TRS:
     active(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    Subterm Criterion Processor:
     simple projection:
      pi(length#) = 0
     problem:
      DPs:
       
      TRS:
       active(eq(0(),0())) -> mark(true())
       active(eq(s(X),s(Y))) -> mark(eq(X,Y))
       active(eq(X,Y)) -> mark(false())
       active(inf(X)) -> mark(cons(X,inf(s(X))))
       active(take(0(),X)) -> mark(nil())
       active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
       active(length(nil())) -> mark(0())
       active(length(cons(X,L))) -> mark(s(length(L)))
       active(inf(X)) -> inf(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(length(X)) -> length(active(X))
       inf(mark(X)) -> mark(inf(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       length(mark(X)) -> mark(length(X))
       proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(true()) -> ok(true())
       proper(s(X)) -> s(proper(X))
       proper(false()) -> ok(false())
       proper(inf(X)) -> inf(proper(X))
       proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(length(X)) -> length(proper(X))
       eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
       s(ok(X)) -> ok(s(X))
       inf(ok(X)) -> ok(inf(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       length(ok(X)) -> ok(length(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
       any(X) -> s(X)
       any(proper(X)) -> any(any(any(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(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    Subterm Criterion Processor:
     simple projection:
      pi(take#) = 1
     problem:
      DPs:
       take#(mark(X1),X2) -> take#(X1,X2)
      TRS:
       active(eq(0(),0())) -> mark(true())
       active(eq(s(X),s(Y))) -> mark(eq(X,Y))
       active(eq(X,Y)) -> mark(false())
       active(inf(X)) -> mark(cons(X,inf(s(X))))
       active(take(0(),X)) -> mark(nil())
       active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
       active(length(nil())) -> mark(0())
       active(length(cons(X,L))) -> mark(s(length(L)))
       active(inf(X)) -> inf(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(length(X)) -> length(active(X))
       inf(mark(X)) -> mark(inf(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       length(mark(X)) -> mark(length(X))
       proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(true()) -> ok(true())
       proper(s(X)) -> s(proper(X))
       proper(false()) -> ok(false())
       proper(inf(X)) -> inf(proper(X))
       proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(length(X)) -> length(proper(X))
       eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
       s(ok(X)) -> ok(s(X))
       inf(ok(X)) -> ok(inf(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       length(ok(X)) -> ok(length(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
       any(X) -> s(X)
       any(proper(X)) -> any(any(any(X)))
     Subterm Criterion Processor:
      simple projection:
       pi(take#) = 0
      problem:
       DPs:
        
       TRS:
        active(eq(0(),0())) -> mark(true())
        active(eq(s(X),s(Y))) -> mark(eq(X,Y))
        active(eq(X,Y)) -> mark(false())
        active(inf(X)) -> mark(cons(X,inf(s(X))))
        active(take(0(),X)) -> mark(nil())
        active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
        active(length(nil())) -> mark(0())
        active(length(cons(X,L))) -> mark(s(length(L)))
        active(inf(X)) -> inf(active(X))
        active(take(X1,X2)) -> take(active(X1),X2)
        active(take(X1,X2)) -> take(X1,active(X2))
        active(length(X)) -> length(active(X))
        inf(mark(X)) -> mark(inf(X))
        take(mark(X1),X2) -> mark(take(X1,X2))
        take(X1,mark(X2)) -> mark(take(X1,X2))
        length(mark(X)) -> mark(length(X))
        proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
        proper(0()) -> ok(0())
        proper(true()) -> ok(true())
        proper(s(X)) -> s(proper(X))
        proper(false()) -> ok(false())
        proper(inf(X)) -> inf(proper(X))
        proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
        proper(take(X1,X2)) -> take(proper(X1),proper(X2))
        proper(nil()) -> ok(nil())
        proper(length(X)) -> length(proper(X))
        eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
        s(ok(X)) -> ok(s(X))
        inf(ok(X)) -> ok(inf(X))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        take(ok(X1),ok(X2)) -> ok(take(X1,X2))
        length(ok(X)) -> ok(length(X))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
        any(X) -> s(X)
        any(proper(X)) -> any(any(any(X)))
      Qed
    
    DPs:
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    TRS:
     active(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    Subterm Criterion Processor:
     simple projection:
      pi(cons#) = 1
     problem:
      DPs:
       
      TRS:
       active(eq(0(),0())) -> mark(true())
       active(eq(s(X),s(Y))) -> mark(eq(X,Y))
       active(eq(X,Y)) -> mark(false())
       active(inf(X)) -> mark(cons(X,inf(s(X))))
       active(take(0(),X)) -> mark(nil())
       active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
       active(length(nil())) -> mark(0())
       active(length(cons(X,L))) -> mark(s(length(L)))
       active(inf(X)) -> inf(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(length(X)) -> length(active(X))
       inf(mark(X)) -> mark(inf(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       length(mark(X)) -> mark(length(X))
       proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(true()) -> ok(true())
       proper(s(X)) -> s(proper(X))
       proper(false()) -> ok(false())
       proper(inf(X)) -> inf(proper(X))
       proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(length(X)) -> length(proper(X))
       eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
       s(ok(X)) -> ok(s(X))
       inf(ok(X)) -> ok(inf(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       length(ok(X)) -> ok(length(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
       any(X) -> s(X)
       any(proper(X)) -> any(any(any(X)))
     Qed
    
    DPs:
     any#(proper(X)) -> any#(X)
     any#(proper(X)) -> any#(any(X))
     any#(proper(X)) -> any#(any(any(X)))
    TRS:
     active(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    EDG Processor:
     DPs:
      any#(proper(X)) -> any#(X)
      any#(proper(X)) -> any#(any(X))
      any#(proper(X)) -> any#(any(any(X)))
     TRS:
      active(eq(0(),0())) -> mark(true())
      active(eq(s(X),s(Y))) -> mark(eq(X,Y))
      active(eq(X,Y)) -> mark(false())
      active(inf(X)) -> mark(cons(X,inf(s(X))))
      active(take(0(),X)) -> mark(nil())
      active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
      active(length(nil())) -> mark(0())
      active(length(cons(X,L))) -> mark(s(length(L)))
      active(inf(X)) -> inf(active(X))
      active(take(X1,X2)) -> take(active(X1),X2)
      active(take(X1,X2)) -> take(X1,active(X2))
      active(length(X)) -> length(active(X))
      inf(mark(X)) -> mark(inf(X))
      take(mark(X1),X2) -> mark(take(X1,X2))
      take(X1,mark(X2)) -> mark(take(X1,X2))
      length(mark(X)) -> mark(length(X))
      proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(true()) -> ok(true())
      proper(s(X)) -> s(proper(X))
      proper(false()) -> ok(false())
      proper(inf(X)) -> inf(proper(X))
      proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
      proper(take(X1,X2)) -> take(proper(X1),proper(X2))
      proper(nil()) -> ok(nil())
      proper(length(X)) -> length(proper(X))
      eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
      s(ok(X)) -> ok(s(X))
      inf(ok(X)) -> ok(inf(X))
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      take(ok(X1),ok(X2)) -> ok(take(X1,X2))
      length(ok(X)) -> ok(length(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
      any(X) -> s(X)
      any(proper(X)) -> any(any(any(X)))
     graph:
      any#(proper(X)) -> any#(X) -> any#(proper(X)) -> any#(X)
      any#(proper(X)) -> any#(X) -> any#(proper(X)) -> any#(any(X))
      any#(proper(X)) -> any#(X) -> any#(proper(X)) -> any#(any(any(X)))
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 3/9
      DPs:
       any#(proper(X)) -> any#(X)
      TRS:
       active(eq(0(),0())) -> mark(true())
       active(eq(s(X),s(Y))) -> mark(eq(X,Y))
       active(eq(X,Y)) -> mark(false())
       active(inf(X)) -> mark(cons(X,inf(s(X))))
       active(take(0(),X)) -> mark(nil())
       active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
       active(length(nil())) -> mark(0())
       active(length(cons(X,L))) -> mark(s(length(L)))
       active(inf(X)) -> inf(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(length(X)) -> length(active(X))
       inf(mark(X)) -> mark(inf(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       length(mark(X)) -> mark(length(X))
       proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(true()) -> ok(true())
       proper(s(X)) -> s(proper(X))
       proper(false()) -> ok(false())
       proper(inf(X)) -> inf(proper(X))
       proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(length(X)) -> length(proper(X))
       eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
       s(ok(X)) -> ok(s(X))
       inf(ok(X)) -> ok(inf(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       length(ok(X)) -> ok(length(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
       any(X) -> s(X)
       any(proper(X)) -> any(any(any(X)))
      Subterm Criterion Processor:
       simple projection:
        pi(any#) = 0
       problem:
        DPs:
         
        TRS:
         active(eq(0(),0())) -> mark(true())
         active(eq(s(X),s(Y))) -> mark(eq(X,Y))
         active(eq(X,Y)) -> mark(false())
         active(inf(X)) -> mark(cons(X,inf(s(X))))
         active(take(0(),X)) -> mark(nil())
         active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
         active(length(nil())) -> mark(0())
         active(length(cons(X,L))) -> mark(s(length(L)))
         active(inf(X)) -> inf(active(X))
         active(take(X1,X2)) -> take(active(X1),X2)
         active(take(X1,X2)) -> take(X1,active(X2))
         active(length(X)) -> length(active(X))
         inf(mark(X)) -> mark(inf(X))
         take(mark(X1),X2) -> mark(take(X1,X2))
         take(X1,mark(X2)) -> mark(take(X1,X2))
         length(mark(X)) -> mark(length(X))
         proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
         proper(0()) -> ok(0())
         proper(true()) -> ok(true())
         proper(s(X)) -> s(proper(X))
         proper(false()) -> ok(false())
         proper(inf(X)) -> inf(proper(X))
         proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
         proper(take(X1,X2)) -> take(proper(X1),proper(X2))
         proper(nil()) -> ok(nil())
         proper(length(X)) -> length(proper(X))
         eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
         s(ok(X)) -> ok(s(X))
         inf(ok(X)) -> ok(inf(X))
         cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
         take(ok(X1),ok(X2)) -> ok(take(X1,X2))
         length(ok(X)) -> ok(length(X))
         top(mark(X)) -> top(proper(X))
         top(ok(X)) -> top(active(X))
         any(X) -> s(X)
         any(proper(X)) -> any(any(any(X)))
       Qed
    
    DPs:
     inf#(mark(X)) -> inf#(X)
     inf#(ok(X)) -> inf#(X)
    TRS:
     active(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    Subterm Criterion Processor:
     simple projection:
      pi(inf#) = 0
     problem:
      DPs:
       
      TRS:
       active(eq(0(),0())) -> mark(true())
       active(eq(s(X),s(Y))) -> mark(eq(X,Y))
       active(eq(X,Y)) -> mark(false())
       active(inf(X)) -> mark(cons(X,inf(s(X))))
       active(take(0(),X)) -> mark(nil())
       active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
       active(length(nil())) -> mark(0())
       active(length(cons(X,L))) -> mark(s(length(L)))
       active(inf(X)) -> inf(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(length(X)) -> length(active(X))
       inf(mark(X)) -> mark(inf(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       length(mark(X)) -> mark(length(X))
       proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(true()) -> ok(true())
       proper(s(X)) -> s(proper(X))
       proper(false()) -> ok(false())
       proper(inf(X)) -> inf(proper(X))
       proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(length(X)) -> length(proper(X))
       eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
       s(ok(X)) -> ok(s(X))
       inf(ok(X)) -> ok(inf(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       length(ok(X)) -> ok(length(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
       any(X) -> s(X)
       any(proper(X)) -> any(any(any(X)))
     Qed
    
    DPs:
     s#(ok(X)) -> s#(X)
    TRS:
     active(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      TRS:
       active(eq(0(),0())) -> mark(true())
       active(eq(s(X),s(Y))) -> mark(eq(X,Y))
       active(eq(X,Y)) -> mark(false())
       active(inf(X)) -> mark(cons(X,inf(s(X))))
       active(take(0(),X)) -> mark(nil())
       active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
       active(length(nil())) -> mark(0())
       active(length(cons(X,L))) -> mark(s(length(L)))
       active(inf(X)) -> inf(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(length(X)) -> length(active(X))
       inf(mark(X)) -> mark(inf(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       length(mark(X)) -> mark(length(X))
       proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(true()) -> ok(true())
       proper(s(X)) -> s(proper(X))
       proper(false()) -> ok(false())
       proper(inf(X)) -> inf(proper(X))
       proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(length(X)) -> length(proper(X))
       eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
       s(ok(X)) -> ok(s(X))
       inf(ok(X)) -> ok(inf(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       length(ok(X)) -> ok(length(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
       any(X) -> s(X)
       any(proper(X)) -> any(any(any(X)))
     Qed
    
    DPs:
     eq#(ok(X1),ok(X2)) -> eq#(X1,X2)
    TRS:
     active(eq(0(),0())) -> mark(true())
     active(eq(s(X),s(Y))) -> mark(eq(X,Y))
     active(eq(X,Y)) -> mark(false())
     active(inf(X)) -> mark(cons(X,inf(s(X))))
     active(take(0(),X)) -> mark(nil())
     active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
     active(length(nil())) -> mark(0())
     active(length(cons(X,L))) -> mark(s(length(L)))
     active(inf(X)) -> inf(active(X))
     active(take(X1,X2)) -> take(active(X1),X2)
     active(take(X1,X2)) -> take(X1,active(X2))
     active(length(X)) -> length(active(X))
     inf(mark(X)) -> mark(inf(X))
     take(mark(X1),X2) -> mark(take(X1,X2))
     take(X1,mark(X2)) -> mark(take(X1,X2))
     length(mark(X)) -> mark(length(X))
     proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(true()) -> ok(true())
     proper(s(X)) -> s(proper(X))
     proper(false()) -> ok(false())
     proper(inf(X)) -> inf(proper(X))
     proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
     proper(take(X1,X2)) -> take(proper(X1),proper(X2))
     proper(nil()) -> ok(nil())
     proper(length(X)) -> length(proper(X))
     eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
     s(ok(X)) -> ok(s(X))
     inf(ok(X)) -> ok(inf(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     take(ok(X1),ok(X2)) -> ok(take(X1,X2))
     length(ok(X)) -> ok(length(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
     any(X) -> s(X)
     any(proper(X)) -> any(any(any(X)))
    Subterm Criterion Processor:
     simple projection:
      pi(eq#) = 1
     problem:
      DPs:
       
      TRS:
       active(eq(0(),0())) -> mark(true())
       active(eq(s(X),s(Y))) -> mark(eq(X,Y))
       active(eq(X,Y)) -> mark(false())
       active(inf(X)) -> mark(cons(X,inf(s(X))))
       active(take(0(),X)) -> mark(nil())
       active(take(s(X),cons(Y,L))) -> mark(cons(Y,take(X,L)))
       active(length(nil())) -> mark(0())
       active(length(cons(X,L))) -> mark(s(length(L)))
       active(inf(X)) -> inf(active(X))
       active(take(X1,X2)) -> take(active(X1),X2)
       active(take(X1,X2)) -> take(X1,active(X2))
       active(length(X)) -> length(active(X))
       inf(mark(X)) -> mark(inf(X))
       take(mark(X1),X2) -> mark(take(X1,X2))
       take(X1,mark(X2)) -> mark(take(X1,X2))
       length(mark(X)) -> mark(length(X))
       proper(eq(X1,X2)) -> eq(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(true()) -> ok(true())
       proper(s(X)) -> s(proper(X))
       proper(false()) -> ok(false())
       proper(inf(X)) -> inf(proper(X))
       proper(cons(any(X1),X2)) -> cons(any(any(proper(X1))),any(proper(X2)))
       proper(take(X1,X2)) -> take(proper(X1),proper(X2))
       proper(nil()) -> ok(nil())
       proper(length(X)) -> length(proper(X))
       eq(ok(X1),ok(X2)) -> ok(eq(X1,X2))
       s(ok(X)) -> ok(s(X))
       inf(ok(X)) -> ok(inf(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       take(ok(X1),ok(X2)) -> ok(take(X1,X2))
       length(ok(X)) -> ok(length(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
       any(X) -> s(X)
       any(proper(X)) -> any(any(any(X)))
     Qed