YES

Problem:
 active(zeros()) -> mark(cons(0(),zeros()))
 active(tail(cons(X,XS))) -> mark(XS)
 active(cons(X1,X2)) -> cons(active(X1),X2)
 active(tail(X)) -> tail(active(X))
 cons(mark(X1),X2) -> mark(cons(X1,X2))
 tail(mark(X)) -> mark(tail(X))
 proper(zeros()) -> ok(zeros())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(tail(X)) -> tail(proper(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 tail(ok(X)) -> ok(tail(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 DP Processor:
  DPs:
   active#(zeros()) -> cons#(0(),zeros())
   active#(cons(X1,X2)) -> active#(X1)
   active#(cons(X1,X2)) -> cons#(active(X1),X2)
   active#(tail(X)) -> active#(X)
   active#(tail(X)) -> tail#(active(X))
   cons#(mark(X1),X2) -> cons#(X1,X2)
   tail#(mark(X)) -> tail#(X)
   proper#(cons(X1,X2)) -> proper#(X2)
   proper#(cons(X1,X2)) -> proper#(X1)
   proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
   proper#(tail(X)) -> proper#(X)
   proper#(tail(X)) -> tail#(proper(X))
   cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
   tail#(ok(X)) -> tail#(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(zeros()) -> mark(cons(0(),zeros()))
   active(tail(cons(X,XS))) -> mark(XS)
   active(cons(X1,X2)) -> cons(active(X1),X2)
   active(tail(X)) -> tail(active(X))
   cons(mark(X1),X2) -> mark(cons(X1,X2))
   tail(mark(X)) -> mark(tail(X))
   proper(zeros()) -> ok(zeros())
   proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
   proper(0()) -> ok(0())
   proper(tail(X)) -> tail(proper(X))
   cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
   tail(ok(X)) -> ok(tail(X))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  TDG Processor:
   DPs:
    active#(zeros()) -> cons#(0(),zeros())
    active#(cons(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(tail(X)) -> active#(X)
    active#(tail(X)) -> tail#(active(X))
    cons#(mark(X1),X2) -> cons#(X1,X2)
    tail#(mark(X)) -> tail#(X)
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(tail(X)) -> proper#(X)
    proper#(tail(X)) -> tail#(proper(X))
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    tail#(ok(X)) -> tail#(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(zeros()) -> mark(cons(0(),zeros()))
    active(tail(cons(X,XS))) -> mark(XS)
    active(cons(X1,X2)) -> cons(active(X1),X2)
    active(tail(X)) -> tail(active(X))
    cons(mark(X1),X2) -> mark(cons(X1,X2))
    tail(mark(X)) -> mark(tail(X))
    proper(zeros()) -> ok(zeros())
    proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    proper(0()) -> ok(0())
    proper(tail(X)) -> tail(proper(X))
    cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    tail(ok(X)) -> ok(tail(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#(tail(X)) -> tail#(active(X))
    top#(ok(X)) -> active#(X) -> active#(tail(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#(zeros()) -> cons#(0(),zeros())
    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#(tail(X)) -> tail#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(tail(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#(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#(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#(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#(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#(tail(X)) -> tail#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(tail(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)
    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)
    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)
    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#(tail(X)) -> tail#(active(X))
    active#(tail(X)) -> active#(X) -> active#(tail(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#(zeros()) -> cons#(0(),zeros())
    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#(tail(X)) -> tail#(active(X))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(tail(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#(zeros()) -> cons#(0(),zeros())
    active#(zeros()) -> cons#(0(),zeros()) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(zeros()) -> cons#(0(),zeros()) -> cons#(mark(X1),X2) -> cons#(X1,X2)
   SCC Processor:
    #sccs: 5
    #rules: 11
    #arcs: 61/324
    DPs:
     top#(ok(X)) -> top#(active(X))
     top#(mark(X)) -> top#(proper(X))
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(tail(cons(X,XS))) -> mark(XS)
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(tail(X)) -> tail(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     proper(zeros()) -> ok(zeros())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(tail(X)) -> tail(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     tail(ok(X)) -> ok(tail(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [top#](x0) = 1/2x0 + 1/2,
      
      [top](x0) = x0 + 7/2,
      
      [ok](x0) = x0,
      
      [proper](x0) = x0,
      
      [tail](x0) = 2x0 + 2,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 2x0 + 1/2x1,
      
      [0] = 0,
      
      [active](x0) = x0,
      
      [zeros] = 2
     orientation:
      top#(ok(X)) = 1/2X + 1/2 >= 1/2X + 1/2 = top#(active(X))
      
      top#(mark(X)) = 1/2X + 1 >= 1/2X + 1/2 = top#(proper(X))
      
      active(zeros()) = 2 >= 2 = mark(cons(0(),zeros()))
      
      active(tail(cons(X,XS))) = 4X + XS + 2 >= XS + 1 = mark(XS)
      
      active(cons(X1,X2)) = 2X1 + 1/2X2 >= 2X1 + 1/2X2 = cons(active(X1),X2)
      
      active(tail(X)) = 2X + 2 >= 2X + 2 = tail(active(X))
      
      cons(mark(X1),X2) = 2X1 + 1/2X2 + 2 >= 2X1 + 1/2X2 + 1 = mark(cons(X1,X2))
      
      tail(mark(X)) = 2X + 4 >= 2X + 3 = mark(tail(X))
      
      proper(zeros()) = 2 >= 2 = ok(zeros())
      
      proper(cons(X1,X2)) = 2X1 + 1/2X2 >= 2X1 + 1/2X2 = cons(proper(X1),proper(X2))
      
      proper(0()) = 0 >= 0 = ok(0())
      
      proper(tail(X)) = 2X + 2 >= 2X + 2 = tail(proper(X))
      
      cons(ok(X1),ok(X2)) = 2X1 + 1/2X2 >= 2X1 + 1/2X2 = ok(cons(X1,X2))
      
      tail(ok(X)) = 2X + 2 >= 2X + 2 = ok(tail(X))
      
      top(mark(X)) = X + 9/2 >= X + 7/2 = top(proper(X))
      
      top(ok(X)) = X + 7/2 >= X + 7/2 = top(active(X))
     problem:
      DPs:
       top#(ok(X)) -> top#(active(X))
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(X))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     KBO Processor:
      argument filtering:
       pi(zeros) = []
       pi(active) = 0
       pi(0) = []
       pi(cons) = 1
       pi(mark) = 0
       pi(tail) = 0
       pi(proper) = [0]
       pi(ok) = [0]
       pi(top) = []
       pi(top#) = 0
      weight function:
       w0 = 1
       w(top#) = w(top) = w(proper) = w(mark) = w(0) = w(active) = w(
       zeros) = 1
       w(ok) = w(tail) = w(cons) = 0
      precedence:
       active > top# > top ~ ok ~ proper ~ tail ~ mark ~ cons ~ 0 ~ zeros
      problem:
       DPs:
        
       TRS:
        active(zeros()) -> mark(cons(0(),zeros()))
        active(tail(cons(X,XS))) -> mark(XS)
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(tail(X)) -> tail(active(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        tail(mark(X)) -> mark(tail(X))
        proper(zeros()) -> ok(zeros())
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(0()) -> ok(0())
        proper(tail(X)) -> tail(proper(X))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        tail(ok(X)) -> ok(tail(X))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed
    
    DPs:
     active#(cons(X1,X2)) -> active#(X1)
     active#(tail(X)) -> active#(X)
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(tail(cons(X,XS))) -> mark(XS)
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(tail(X)) -> tail(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     proper(zeros()) -> ok(zeros())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(tail(X)) -> tail(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     tail(ok(X)) -> ok(tail(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(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(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#(tail(X)) -> proper#(X)
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(tail(cons(X,XS))) -> mark(XS)
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(tail(X)) -> tail(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     proper(zeros()) -> ok(zeros())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(tail(X)) -> tail(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     tail(ok(X)) -> ok(tail(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(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(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(zeros()) -> mark(cons(0(),zeros()))
     active(tail(cons(X,XS))) -> mark(XS)
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(tail(X)) -> tail(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     proper(zeros()) -> ok(zeros())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(tail(X)) -> tail(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     tail(ok(X)) -> ok(tail(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(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(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(zeros()) -> mark(cons(0(),zeros()))
     active(tail(cons(X,XS))) -> mark(XS)
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(tail(X)) -> tail(active(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     tail(mark(X)) -> mark(tail(X))
     proper(zeros()) -> ok(zeros())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(tail(X)) -> tail(proper(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     tail(ok(X)) -> ok(tail(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(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(tail(X)) -> tail(active(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       tail(mark(X)) -> mark(tail(X))
       proper(zeros()) -> ok(zeros())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(0()) -> ok(0())
       proper(tail(X)) -> tail(proper(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       tail(ok(X)) -> ok(tail(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(zeros()) -> mark(cons(0(),zeros()))
        active(tail(cons(X,XS))) -> mark(XS)
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(tail(X)) -> tail(active(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        tail(mark(X)) -> mark(tail(X))
        proper(zeros()) -> ok(zeros())
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(0()) -> ok(0())
        proper(tail(X)) -> tail(proper(X))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        tail(ok(X)) -> ok(tail(X))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Qed