YES
TRS:
 {                  active(2nd(X)) -> 2nd(active(X)),
  active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
              active(cons(X1, X2)) -> cons(active(X1), X2),
                   active(from(X)) -> mark(cons(X, from(s(X)))),
                   active(from(X)) -> from(active(X)),
                      active(s(X)) -> s(active(X)),
                      2nd(mark(X)) -> mark(2nd(X)),
                        2nd(ok(X)) -> ok(2nd(X)),
                cons(mark(X1), X2) -> mark(cons(X1, X2)),
              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                     from(mark(X)) -> mark(from(X)),
                       from(ok(X)) -> ok(from(X)),
                        s(mark(X)) -> mark(s(X)),
                          s(ok(X)) -> ok(s(X)),
                    proper(2nd(X)) -> 2nd(proper(X)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                   proper(from(X)) -> from(proper(X)),
                      proper(s(X)) -> s(proper(X)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {      active#(2nd(X)) -> active#(X),
          active#(2nd(X)) -> 2nd#(active(X)),
    active#(cons(X1, X2)) -> active#(X1),
    active#(cons(X1, X2)) -> cons#(active(X1), X2),
         active#(from(X)) -> active#(X),
         active#(from(X)) -> cons#(X, from(s(X))),
         active#(from(X)) -> from#(active(X)),
         active#(from(X)) -> from#(s(X)),
         active#(from(X)) -> s#(X),
            active#(s(X)) -> active#(X),
            active#(s(X)) -> s#(active(X)),
            2nd#(mark(X)) -> 2nd#(X),
              2nd#(ok(X)) -> 2nd#(X),
      cons#(mark(X1), X2) -> cons#(X1, X2),
    cons#(ok(X1), ok(X2)) -> cons#(X1, X2),
           from#(mark(X)) -> from#(X),
             from#(ok(X)) -> from#(X),
              s#(mark(X)) -> s#(X),
                s#(ok(X)) -> s#(X),
          proper#(2nd(X)) -> 2nd#(proper(X)),
          proper#(2nd(X)) -> proper#(X),
    proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)),
    proper#(cons(X1, X2)) -> proper#(X1),
    proper#(cons(X1, X2)) -> proper#(X2),
         proper#(from(X)) -> from#(proper(X)),
         proper#(from(X)) -> proper#(X),
            proper#(s(X)) -> s#(proper(X)),
            proper#(s(X)) -> proper#(X),
            top#(mark(X)) -> proper#(X),
            top#(mark(X)) -> top#(proper(X)),
              top#(ok(X)) -> active#(X),
              top#(ok(X)) -> top#(active(X))}
  Weak:
  {                  active(2nd(X)) -> 2nd(active(X)),
   active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
               active(cons(X1, X2)) -> cons(active(X1), X2),
                    active(from(X)) -> mark(cons(X, from(s(X)))),
                    active(from(X)) -> from(active(X)),
                       active(s(X)) -> s(active(X)),
                       2nd(mark(X)) -> mark(2nd(X)),
                         2nd(ok(X)) -> ok(2nd(X)),
                 cons(mark(X1), X2) -> mark(cons(X1, X2)),
               cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                      from(mark(X)) -> mark(from(X)),
                        from(ok(X)) -> ok(from(X)),
                         s(mark(X)) -> mark(s(X)),
                           s(ok(X)) -> ok(s(X)),
                     proper(2nd(X)) -> 2nd(proper(X)),
               proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                    proper(from(X)) -> from(proper(X)),
                       proper(s(X)) -> s(proper(X)),
                       top(mark(X)) -> top(proper(X)),
                         top(ok(X)) -> top(active(X))}
  EDG:
   {
    (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#(from(X)) -> from#(active(X)), from#(ok(X)) -> from#(X))
    (active#(from(X)) -> from#(active(X)), from#(mark(X)) -> from#(X))
    (active#(s(X)) -> s#(active(X)), s#(ok(X)) -> s#(X))
    (active#(s(X)) -> s#(active(X)), s#(mark(X)) -> s#(X))
    (proper#(from(X)) -> from#(proper(X)), from#(ok(X)) -> from#(X))
    (proper#(from(X)) -> from#(proper(X)), from#(mark(X)) -> from#(X))
    (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))
    (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))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(from(X)) -> from#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> 2nd#(proper(X)))
    (active#(from(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(from(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(from(X)) -> active#(X), active#(from(X)) -> s#(X))
    (active#(from(X)) -> active#(X), active#(from(X)) -> from#(s(X)))
    (active#(from(X)) -> active#(X), active#(from(X)) -> from#(active(X)))
    (active#(from(X)) -> active#(X), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(from(X)) -> active#(X), active#(from(X)) -> active#(X))
    (active#(from(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(from(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(from(X)) -> active#(X), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(from(X)) -> active#(X), active#(2nd(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(from(X)) -> s#(X))
    (active#(s(X)) -> active#(X), active#(from(X)) -> from#(s(X)))
    (active#(s(X)) -> active#(X), active#(from(X)) -> from#(active(X)))
    (active#(s(X)) -> active#(X), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(s(X)) -> active#(X), active#(from(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(s(X)) -> active#(X), active#(2nd(X)) -> active#(X))
    (2nd#(ok(X)) -> 2nd#(X), 2nd#(ok(X)) -> 2nd#(X))
    (2nd#(ok(X)) -> 2nd#(X), 2nd#(mark(X)) -> 2nd#(X))
    (from#(ok(X)) -> from#(X), from#(ok(X)) -> from#(X))
    (from#(ok(X)) -> from#(X), from#(mark(X)) -> from#(X))
    (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (s#(ok(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(from(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (proper#(from(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(from(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
    (proper#(from(X)) -> proper#(X), proper#(2nd(X)) -> 2nd#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> from#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> 2nd#(proper(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
    (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> from#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> from#(s(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> s#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (top#(ok(X)) -> active#(X), active#(2nd(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(2nd(X)) -> 2nd#(active(X)))
    (top#(ok(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> cons#(X, from(s(X))))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> from#(active(X)))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> from#(s(X)))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> s#(X))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(from(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#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
    (proper#(2nd(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(2nd(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(2nd(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(2nd(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (proper#(2nd(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (from#(mark(X)) -> from#(X), from#(mark(X)) -> from#(X))
    (from#(mark(X)) -> from#(X), from#(ok(X)) -> from#(X))
    (2nd#(mark(X)) -> 2nd#(X), 2nd#(mark(X)) -> 2nd#(X))
    (2nd#(mark(X)) -> 2nd#(X), 2nd#(ok(X)) -> 2nd#(X))
    (active#(from(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (active#(from(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
    (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(2nd(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(2nd(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(2nd(X)) -> active#(X), active#(from(X)) -> active#(X))
    (active#(2nd(X)) -> active#(X), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(2nd(X)) -> active#(X), active#(from(X)) -> from#(active(X)))
    (active#(2nd(X)) -> active#(X), active#(from(X)) -> from#(s(X)))
    (active#(2nd(X)) -> active#(X), active#(from(X)) -> s#(X))
    (active#(2nd(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(2nd(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(ok(X1), ok(X2)) -> cons#(X1, X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))
    (proper#(s(X)) -> s#(proper(X)), s#(mark(X)) -> s#(X))
    (proper#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X))
    (proper#(2nd(X)) -> 2nd#(proper(X)), 2nd#(mark(X)) -> 2nd#(X))
    (proper#(2nd(X)) -> 2nd#(proper(X)), 2nd#(ok(X)) -> 2nd#(X))
    (active#(from(X)) -> from#(s(X)), from#(mark(X)) -> from#(X))
    (active#(from(X)) -> from#(s(X)), from#(ok(X)) -> from#(X))
    (active#(2nd(X)) -> 2nd#(active(X)), 2nd#(mark(X)) -> 2nd#(X))
    (active#(2nd(X)) -> 2nd#(active(X)), 2nd#(ok(X)) -> 2nd#(X))
    (active#(from(X)) -> cons#(X, from(s(X))), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(from(X)) -> cons#(X, from(s(X))), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
   }
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {      proper#(2nd(X)) -> proper#(X),
      proper#(cons(X1, X2)) -> proper#(X1),
      proper#(cons(X1, X2)) -> proper#(X2),
           proper#(from(X)) -> proper#(X),
              proper#(s(X)) -> proper#(X)}
    Scc:
     {s#(mark(X)) -> s#(X),
        s#(ok(X)) -> s#(X)}
    Scc:
     {from#(mark(X)) -> from#(X),
        from#(ok(X)) -> from#(X)}
    Scc:
     {  cons#(mark(X1), X2) -> cons#(X1, X2),
      cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
    Scc:
     {2nd#(mark(X)) -> 2nd#(X),
        2nd#(ok(X)) -> 2nd#(X)}
    Scc:
     {      active#(2nd(X)) -> active#(X),
      active#(cons(X1, X2)) -> active#(X1),
           active#(from(X)) -> active#(X),
              active#(s(X)) -> active#(X)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {                  active(2nd(X)) -> 2nd(active(X)),
      active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                       active(from(X)) -> mark(cons(X, from(s(X)))),
                       active(from(X)) -> from(active(X)),
                          active(s(X)) -> s(active(X)),
                          2nd(mark(X)) -> mark(2nd(X)),
                            2nd(ok(X)) -> ok(2nd(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                         from(mark(X)) -> mark(from(X)),
                           from(ok(X)) -> ok(from(X)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                        proper(2nd(X)) -> 2nd(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                       proper(from(X)) -> from(proper(X)),
                          proper(s(X)) -> s(proper(X)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))}
     POLY:
      Argument Filtering:
       pi(top#) = 0, pi(top) = [], pi(ok) = [0], pi(proper) = [], pi(s) = 0, pi(from) = 0, pi(cons) = 0, pi(2nd) = 0, pi(active) = 0, pi(mark) = []
      Usable Rules:
       {}
      Interpretation:
       [ok](x0) = x0 + 1,
       [proper] = 0,
       [mark] = 0
      Strict:
       {top#(mark(X)) -> top#(proper(X))}
      Weak:
       {                  active(2nd(X)) -> 2nd(active(X)),
        active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                    active(cons(X1, X2)) -> cons(active(X1), X2),
                         active(from(X)) -> mark(cons(X, from(s(X)))),
                         active(from(X)) -> from(active(X)),
                            active(s(X)) -> s(active(X)),
                            2nd(mark(X)) -> mark(2nd(X)),
                              2nd(ok(X)) -> ok(2nd(X)),
                      cons(mark(X1), X2) -> mark(cons(X1, X2)),
                    cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                           from(mark(X)) -> mark(from(X)),
                             from(ok(X)) -> ok(from(X)),
                              s(mark(X)) -> mark(s(X)),
                                s(ok(X)) -> ok(s(X)),
                          proper(2nd(X)) -> 2nd(proper(X)),
                    proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                         proper(from(X)) -> from(proper(X)),
                            proper(s(X)) -> s(proper(X)),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
      EDG:
       {(top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))}
       SCCS:
        Scc:
         {top#(mark(X)) -> top#(proper(X))}
        SCC:
         Strict:
          {top#(mark(X)) -> top#(proper(X))}
         Weak:
         {                  active(2nd(X)) -> 2nd(active(X)),
          active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                           active(from(X)) -> mark(cons(X, from(s(X)))),
                           active(from(X)) -> from(active(X)),
                              active(s(X)) -> s(active(X)),
                              2nd(mark(X)) -> mark(2nd(X)),
                                2nd(ok(X)) -> ok(2nd(X)),
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                             from(mark(X)) -> mark(from(X)),
                               from(ok(X)) -> ok(from(X)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                            proper(2nd(X)) -> 2nd(proper(X)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                           proper(from(X)) -> from(proper(X)),
                              proper(s(X)) -> s(proper(X)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))}
         POLY:
          Argument Filtering:
           pi(top#) = 0, pi(top) = [], pi(ok) = [], pi(proper) = 0, pi(s) = [0], pi(from) = [0], pi(cons) = 0, pi(2nd) = 0, pi(active) = [], pi(mark) = [0]
          Usable Rules:
           {}
          Interpretation:
           [mark](x0) = x0 + 1
          Strict:
           {}
          Weak:
           {                  active(2nd(X)) -> 2nd(active(X)),
            active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                        active(cons(X1, X2)) -> cons(active(X1), X2),
                             active(from(X)) -> mark(cons(X, from(s(X)))),
                             active(from(X)) -> from(active(X)),
                                active(s(X)) -> s(active(X)),
                                2nd(mark(X)) -> mark(2nd(X)),
                                  2nd(ok(X)) -> ok(2nd(X)),
                          cons(mark(X1), X2) -> mark(cons(X1, X2)),
                        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                               from(mark(X)) -> mark(from(X)),
                                 from(ok(X)) -> ok(from(X)),
                                  s(mark(X)) -> mark(s(X)),
                                    s(ok(X)) -> ok(s(X)),
                              proper(2nd(X)) -> 2nd(proper(X)),
                        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                             proper(from(X)) -> from(proper(X)),
                                proper(s(X)) -> s(proper(X)),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))}
          Qed
    SCC:
     Strict:
      {      proper#(2nd(X)) -> proper#(X),
       proper#(cons(X1, X2)) -> proper#(X1),
       proper#(cons(X1, X2)) -> proper#(X2),
            proper#(from(X)) -> proper#(X),
               proper#(s(X)) -> proper#(X)}
     Weak:
     {                  active(2nd(X)) -> 2nd(active(X)),
      active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                       active(from(X)) -> mark(cons(X, from(s(X)))),
                       active(from(X)) -> from(active(X)),
                          active(s(X)) -> s(active(X)),
                          2nd(mark(X)) -> mark(2nd(X)),
                            2nd(ok(X)) -> ok(2nd(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                         from(mark(X)) -> mark(from(X)),
                           from(ok(X)) -> ok(from(X)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                        proper(2nd(X)) -> 2nd(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                       proper(from(X)) -> from(proper(X)),
                          proper(s(X)) -> s(proper(X)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {      proper#(2nd(X)) -> proper#(X),
        proper#(cons(X1, X2)) -> proper#(X1),
        proper#(cons(X1, X2)) -> proper#(X2),
                proper#(s(X)) -> proper#(X)}
      EDG:
       {(proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(2nd(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(2nd(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
        (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#(X2), proper#(s(X)) -> proper#(X))}
       SCCS:
        Scc:
         {      proper#(2nd(X)) -> proper#(X),
          proper#(cons(X1, X2)) -> proper#(X1),
          proper#(cons(X1, X2)) -> proper#(X2),
                  proper#(s(X)) -> proper#(X)}
        SCC:
         Strict:
          {      proper#(2nd(X)) -> proper#(X),
           proper#(cons(X1, X2)) -> proper#(X1),
           proper#(cons(X1, X2)) -> proper#(X2),
                   proper#(s(X)) -> proper#(X)}
         Weak:
         {                  active(2nd(X)) -> 2nd(active(X)),
          active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                           active(from(X)) -> mark(cons(X, from(s(X)))),
                           active(from(X)) -> from(active(X)),
                              active(s(X)) -> s(active(X)),
                              2nd(mark(X)) -> mark(2nd(X)),
                                2nd(ok(X)) -> ok(2nd(X)),
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                             from(mark(X)) -> mark(from(X)),
                               from(ok(X)) -> ok(from(X)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                            proper(2nd(X)) -> 2nd(proper(X)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                           proper(from(X)) -> from(proper(X)),
                              proper(s(X)) -> s(proper(X)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {      proper#(2nd(X)) -> proper#(X),
            proper#(cons(X1, X2)) -> proper#(X1),
                    proper#(s(X)) -> proper#(X)}
          EDG:
           {(proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(2nd(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))}
           SCCS:
            Scc:
             {      proper#(2nd(X)) -> proper#(X),
              proper#(cons(X1, X2)) -> proper#(X1),
                      proper#(s(X)) -> proper#(X)}
            SCC:
             Strict:
              {      proper#(2nd(X)) -> proper#(X),
               proper#(cons(X1, X2)) -> proper#(X1),
                       proper#(s(X)) -> proper#(X)}
             Weak:
             {                  active(2nd(X)) -> 2nd(active(X)),
              active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                          active(cons(X1, X2)) -> cons(active(X1), X2),
                               active(from(X)) -> mark(cons(X, from(s(X)))),
                               active(from(X)) -> from(active(X)),
                                  active(s(X)) -> s(active(X)),
                                  2nd(mark(X)) -> mark(2nd(X)),
                                    2nd(ok(X)) -> ok(2nd(X)),
                            cons(mark(X1), X2) -> mark(cons(X1, X2)),
                          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                 from(mark(X)) -> mark(from(X)),
                                   from(ok(X)) -> ok(from(X)),
                                    s(mark(X)) -> mark(s(X)),
                                      s(ok(X)) -> ok(s(X)),
                                proper(2nd(X)) -> 2nd(proper(X)),
                          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                               proper(from(X)) -> from(proper(X)),
                                  proper(s(X)) -> s(proper(X)),
                                  top(mark(X)) -> top(proper(X)),
                                    top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(proper#) = 0
              Strict:
               {proper#(2nd(X)) -> proper#(X),
                  proper#(s(X)) -> proper#(X)}
              EDG:
               {(proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                (proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> proper#(X))}
               SCCS:
                Scc:
                 {proper#(2nd(X)) -> proper#(X),
                    proper#(s(X)) -> proper#(X)}
                SCC:
                 Strict:
                  {proper#(2nd(X)) -> proper#(X),
                     proper#(s(X)) -> proper#(X)}
                 Weak:
                 {                  active(2nd(X)) -> 2nd(active(X)),
                  active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                              active(cons(X1, X2)) -> cons(active(X1), X2),
                                   active(from(X)) -> mark(cons(X, from(s(X)))),
                                   active(from(X)) -> from(active(X)),
                                      active(s(X)) -> s(active(X)),
                                      2nd(mark(X)) -> mark(2nd(X)),
                                        2nd(ok(X)) -> ok(2nd(X)),
                                cons(mark(X1), X2) -> mark(cons(X1, X2)),
                              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                     from(mark(X)) -> mark(from(X)),
                                       from(ok(X)) -> ok(from(X)),
                                        s(mark(X)) -> mark(s(X)),
                                          s(ok(X)) -> ok(s(X)),
                                    proper(2nd(X)) -> 2nd(proper(X)),
                              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                   proper(from(X)) -> from(proper(X)),
                                      proper(s(X)) -> s(proper(X)),
                                      top(mark(X)) -> top(proper(X)),
                                        top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(proper#) = 0
                  Strict:
                   {proper#(s(X)) -> proper#(X)}
                  EDG:
                   {(proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))}
                   SCCS:
                    Scc:
                     {proper#(s(X)) -> proper#(X)}
                    SCC:
                     Strict:
                      {proper#(s(X)) -> proper#(X)}
                     Weak:
                     {                  active(2nd(X)) -> 2nd(active(X)),
                      active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                                  active(cons(X1, X2)) -> cons(active(X1), X2),
                                       active(from(X)) -> mark(cons(X, from(s(X)))),
                                       active(from(X)) -> from(active(X)),
                                          active(s(X)) -> s(active(X)),
                                          2nd(mark(X)) -> mark(2nd(X)),
                                            2nd(ok(X)) -> ok(2nd(X)),
                                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                         from(mark(X)) -> mark(from(X)),
                                           from(ok(X)) -> ok(from(X)),
                                            s(mark(X)) -> mark(s(X)),
                                              s(ok(X)) -> ok(s(X)),
                                        proper(2nd(X)) -> 2nd(proper(X)),
                                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                       proper(from(X)) -> from(proper(X)),
                                          proper(s(X)) -> s(proper(X)),
                                          top(mark(X)) -> top(proper(X)),
                                            top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(proper#) = 0
                      Strict:
                       {}
                      Qed
    SCC:
     Strict:
      {s#(mark(X)) -> s#(X),
         s#(ok(X)) -> s#(X)}
     Weak:
     {                  active(2nd(X)) -> 2nd(active(X)),
      active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                       active(from(X)) -> mark(cons(X, from(s(X)))),
                       active(from(X)) -> from(active(X)),
                          active(s(X)) -> s(active(X)),
                          2nd(mark(X)) -> mark(2nd(X)),
                            2nd(ok(X)) -> ok(2nd(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                         from(mark(X)) -> mark(from(X)),
                           from(ok(X)) -> ok(from(X)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                        proper(2nd(X)) -> 2nd(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                       proper(from(X)) -> from(proper(X)),
                          proper(s(X)) -> s(proper(X)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(s#) = 0
      Strict:
       {s#(ok(X)) -> s#(X)}
      EDG:
       {(s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))}
       SCCS:
        Scc:
         {s#(ok(X)) -> s#(X)}
        SCC:
         Strict:
          {s#(ok(X)) -> s#(X)}
         Weak:
         {                  active(2nd(X)) -> 2nd(active(X)),
          active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                           active(from(X)) -> mark(cons(X, from(s(X)))),
                           active(from(X)) -> from(active(X)),
                              active(s(X)) -> s(active(X)),
                              2nd(mark(X)) -> mark(2nd(X)),
                                2nd(ok(X)) -> ok(2nd(X)),
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                             from(mark(X)) -> mark(from(X)),
                               from(ok(X)) -> ok(from(X)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                            proper(2nd(X)) -> 2nd(proper(X)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                           proper(from(X)) -> from(proper(X)),
                              proper(s(X)) -> s(proper(X)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(s#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {from#(mark(X)) -> from#(X),
         from#(ok(X)) -> from#(X)}
     Weak:
     {                  active(2nd(X)) -> 2nd(active(X)),
      active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                       active(from(X)) -> mark(cons(X, from(s(X)))),
                       active(from(X)) -> from(active(X)),
                          active(s(X)) -> s(active(X)),
                          2nd(mark(X)) -> mark(2nd(X)),
                            2nd(ok(X)) -> ok(2nd(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                         from(mark(X)) -> mark(from(X)),
                           from(ok(X)) -> ok(from(X)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                        proper(2nd(X)) -> 2nd(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                       proper(from(X)) -> from(proper(X)),
                          proper(s(X)) -> s(proper(X)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(from#) = 0
      Strict:
       {from#(mark(X)) -> from#(X)}
      EDG:
       {(from#(mark(X)) -> from#(X), from#(mark(X)) -> from#(X))}
       SCCS:
        Scc:
         {from#(mark(X)) -> from#(X)}
        SCC:
         Strict:
          {from#(mark(X)) -> from#(X)}
         Weak:
         {                  active(2nd(X)) -> 2nd(active(X)),
          active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                           active(from(X)) -> mark(cons(X, from(s(X)))),
                           active(from(X)) -> from(active(X)),
                              active(s(X)) -> s(active(X)),
                              2nd(mark(X)) -> mark(2nd(X)),
                                2nd(ok(X)) -> ok(2nd(X)),
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                             from(mark(X)) -> mark(from(X)),
                               from(ok(X)) -> ok(from(X)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                            proper(2nd(X)) -> 2nd(proper(X)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                           proper(from(X)) -> from(proper(X)),
                              proper(s(X)) -> s(proper(X)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(from#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  cons#(mark(X1), X2) -> cons#(X1, X2),
       cons#(ok(X1), ok(X2)) -> cons#(X1, X2)}
     Weak:
     {                  active(2nd(X)) -> 2nd(active(X)),
      active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                       active(from(X)) -> mark(cons(X, from(s(X)))),
                       active(from(X)) -> from(active(X)),
                          active(s(X)) -> s(active(X)),
                          2nd(mark(X)) -> mark(2nd(X)),
                            2nd(ok(X)) -> ok(2nd(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                         from(mark(X)) -> mark(from(X)),
                           from(ok(X)) -> ok(from(X)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                        proper(2nd(X)) -> 2nd(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                       proper(from(X)) -> from(proper(X)),
                          proper(s(X)) -> s(proper(X)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(cons#) = 0
      Strict:
       {cons#(mark(X1), X2) -> cons#(X1, X2)}
      EDG:
       {(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))}
       SCCS:
        Scc:
         {cons#(mark(X1), X2) -> cons#(X1, X2)}
        SCC:
         Strict:
          {cons#(mark(X1), X2) -> cons#(X1, X2)}
         Weak:
         {                  active(2nd(X)) -> 2nd(active(X)),
          active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                           active(from(X)) -> mark(cons(X, from(s(X)))),
                           active(from(X)) -> from(active(X)),
                              active(s(X)) -> s(active(X)),
                              2nd(mark(X)) -> mark(2nd(X)),
                                2nd(ok(X)) -> ok(2nd(X)),
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                             from(mark(X)) -> mark(from(X)),
                               from(ok(X)) -> ok(from(X)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                            proper(2nd(X)) -> 2nd(proper(X)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                           proper(from(X)) -> from(proper(X)),
                              proper(s(X)) -> s(proper(X)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(cons#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {2nd#(mark(X)) -> 2nd#(X),
         2nd#(ok(X)) -> 2nd#(X)}
     Weak:
     {                  active(2nd(X)) -> 2nd(active(X)),
      active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                       active(from(X)) -> mark(cons(X, from(s(X)))),
                       active(from(X)) -> from(active(X)),
                          active(s(X)) -> s(active(X)),
                          2nd(mark(X)) -> mark(2nd(X)),
                            2nd(ok(X)) -> ok(2nd(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                         from(mark(X)) -> mark(from(X)),
                           from(ok(X)) -> ok(from(X)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                        proper(2nd(X)) -> 2nd(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                       proper(from(X)) -> from(proper(X)),
                          proper(s(X)) -> s(proper(X)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(2nd#) = 0
      Strict:
       {2nd#(ok(X)) -> 2nd#(X)}
      EDG:
       {(2nd#(ok(X)) -> 2nd#(X), 2nd#(ok(X)) -> 2nd#(X))}
       SCCS:
        Scc:
         {2nd#(ok(X)) -> 2nd#(X)}
        SCC:
         Strict:
          {2nd#(ok(X)) -> 2nd#(X)}
         Weak:
         {                  active(2nd(X)) -> 2nd(active(X)),
          active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                           active(from(X)) -> mark(cons(X, from(s(X)))),
                           active(from(X)) -> from(active(X)),
                              active(s(X)) -> s(active(X)),
                              2nd(mark(X)) -> mark(2nd(X)),
                                2nd(ok(X)) -> ok(2nd(X)),
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                             from(mark(X)) -> mark(from(X)),
                               from(ok(X)) -> ok(from(X)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                            proper(2nd(X)) -> 2nd(proper(X)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                           proper(from(X)) -> from(proper(X)),
                              proper(s(X)) -> s(proper(X)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(2nd#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {      active#(2nd(X)) -> active#(X),
       active#(cons(X1, X2)) -> active#(X1),
            active#(from(X)) -> active#(X),
               active#(s(X)) -> active#(X)}
     Weak:
     {                  active(2nd(X)) -> 2nd(active(X)),
      active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                  active(cons(X1, X2)) -> cons(active(X1), X2),
                       active(from(X)) -> mark(cons(X, from(s(X)))),
                       active(from(X)) -> from(active(X)),
                          active(s(X)) -> s(active(X)),
                          2nd(mark(X)) -> mark(2nd(X)),
                            2nd(ok(X)) -> ok(2nd(X)),
                    cons(mark(X1), X2) -> mark(cons(X1, X2)),
                  cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                         from(mark(X)) -> mark(from(X)),
                           from(ok(X)) -> ok(from(X)),
                            s(mark(X)) -> mark(s(X)),
                              s(ok(X)) -> ok(s(X)),
                        proper(2nd(X)) -> 2nd(proper(X)),
                  proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                       proper(from(X)) -> from(proper(X)),
                          proper(s(X)) -> s(proper(X)),
                          top(mark(X)) -> top(proper(X)),
                            top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {      active#(2nd(X)) -> active#(X),
        active#(cons(X1, X2)) -> active#(X1),
                active#(s(X)) -> active#(X)}
      EDG:
       {(active#(2nd(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(2nd(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(2nd(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
        (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))}
       SCCS:
        Scc:
         {      active#(2nd(X)) -> active#(X),
          active#(cons(X1, X2)) -> active#(X1),
                  active#(s(X)) -> active#(X)}
        SCC:
         Strict:
          {      active#(2nd(X)) -> active#(X),
           active#(cons(X1, X2)) -> active#(X1),
                   active#(s(X)) -> active#(X)}
         Weak:
         {                  active(2nd(X)) -> 2nd(active(X)),
          active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                      active(cons(X1, X2)) -> cons(active(X1), X2),
                           active(from(X)) -> mark(cons(X, from(s(X)))),
                           active(from(X)) -> from(active(X)),
                              active(s(X)) -> s(active(X)),
                              2nd(mark(X)) -> mark(2nd(X)),
                                2nd(ok(X)) -> ok(2nd(X)),
                        cons(mark(X1), X2) -> mark(cons(X1, X2)),
                      cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                             from(mark(X)) -> mark(from(X)),
                               from(ok(X)) -> ok(from(X)),
                                s(mark(X)) -> mark(s(X)),
                                  s(ok(X)) -> ok(s(X)),
                            proper(2nd(X)) -> 2nd(proper(X)),
                      proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                           proper(from(X)) -> from(proper(X)),
                              proper(s(X)) -> s(proper(X)),
                              top(mark(X)) -> top(proper(X)),
                                top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(active#) = 0
          Strict:
           {active#(2nd(X)) -> active#(X),
              active#(s(X)) -> active#(X)}
          EDG:
           {(active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(2nd(X)) -> active#(X))
            (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
            (active#(2nd(X)) -> active#(X), active#(s(X)) -> active#(X))}
           SCCS:
            Scc:
             {active#(2nd(X)) -> active#(X),
                active#(s(X)) -> active#(X)}
            SCC:
             Strict:
              {active#(2nd(X)) -> active#(X),
                 active#(s(X)) -> active#(X)}
             Weak:
             {                  active(2nd(X)) -> 2nd(active(X)),
              active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                          active(cons(X1, X2)) -> cons(active(X1), X2),
                               active(from(X)) -> mark(cons(X, from(s(X)))),
                               active(from(X)) -> from(active(X)),
                                  active(s(X)) -> s(active(X)),
                                  2nd(mark(X)) -> mark(2nd(X)),
                                    2nd(ok(X)) -> ok(2nd(X)),
                            cons(mark(X1), X2) -> mark(cons(X1, X2)),
                          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                 from(mark(X)) -> mark(from(X)),
                                   from(ok(X)) -> ok(from(X)),
                                    s(mark(X)) -> mark(s(X)),
                                      s(ok(X)) -> ok(s(X)),
                                proper(2nd(X)) -> 2nd(proper(X)),
                          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                               proper(from(X)) -> from(proper(X)),
                                  proper(s(X)) -> s(proper(X)),
                                  top(mark(X)) -> top(proper(X)),
                                    top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(active#) = 0
              Strict:
               {active#(s(X)) -> active#(X)}
              EDG:
               {(active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))}
               SCCS:
                Scc:
                 {active#(s(X)) -> active#(X)}
                SCC:
                 Strict:
                  {active#(s(X)) -> active#(X)}
                 Weak:
                 {                  active(2nd(X)) -> 2nd(active(X)),
                  active(2nd(cons(X, cons(Y, Z)))) -> mark(Y),
                              active(cons(X1, X2)) -> cons(active(X1), X2),
                                   active(from(X)) -> mark(cons(X, from(s(X)))),
                                   active(from(X)) -> from(active(X)),
                                      active(s(X)) -> s(active(X)),
                                      2nd(mark(X)) -> mark(2nd(X)),
                                        2nd(ok(X)) -> ok(2nd(X)),
                                cons(mark(X1), X2) -> mark(cons(X1, X2)),
                              cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                                     from(mark(X)) -> mark(from(X)),
                                       from(ok(X)) -> ok(from(X)),
                                        s(mark(X)) -> mark(s(X)),
                                          s(ok(X)) -> ok(s(X)),
                                    proper(2nd(X)) -> 2nd(proper(X)),
                              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                   proper(from(X)) -> from(proper(X)),
                                      proper(s(X)) -> s(proper(X)),
                                      top(mark(X)) -> top(proper(X)),
                                        top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(active#) = 0
                  Strict:
                   {}
                  Qed