MAYBE
TRS:
 {             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)),
             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)),
                  active(head(X)) -> head(active(X)),
        active(head(cons(X, XS))) -> mark(X),
                   active(2nd(X)) -> 2nd(active(X)),
         active(2nd(cons(X, XS))) -> mark(head(XS)),
             active(take(X1, X2)) -> take(X1, active(X2)),
             active(take(X1, X2)) -> take(active(X1), X2),
  active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
            active(take(0(), XS)) -> mark(nil()),
              active(sel(X1, X2)) -> sel(X1, active(X2)),
              active(sel(X1, X2)) -> sel(active(X1), X2),
   active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
    active(sel(0(), cons(X, XS))) -> mark(X),
                    head(mark(X)) -> mark(head(X)),
                      head(ok(X)) -> ok(head(X)),
                     2nd(mark(X)) -> mark(2nd(X)),
                       2nd(ok(X)) -> ok(2nd(X)),
               take(X1, mark(X2)) -> mark(take(X1, X2)),
               take(mark(X1), X2) -> mark(take(X1, X2)),
             take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                sel(mark(X1), X2) -> mark(sel(X1, X2)),
              sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                  proper(from(X)) -> from(proper(X)),
                     proper(s(X)) -> s(proper(X)),
                  proper(head(X)) -> head(proper(X)),
                   proper(2nd(X)) -> 2nd(proper(X)),
                    proper(nil()) -> ok(nil()),
             proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                      proper(0()) -> ok(0()),
              proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                     top(mark(X)) -> top(proper(X)),
                       top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {             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),
               active#(cons(X1, X2)) -> cons#(active(X1), X2),
               active#(cons(X1, X2)) -> active#(X1),
                    active#(from(X)) -> cons#(X, from(s(X))),
                    active#(from(X)) -> from#(s(X)),
                    active#(from(X)) -> from#(active(X)),
                    active#(from(X)) -> s#(X),
                    active#(from(X)) -> active#(X),
                       active#(s(X)) -> s#(active(X)),
                       active#(s(X)) -> active#(X),
                    active#(head(X)) -> active#(X),
                    active#(head(X)) -> head#(active(X)),
                     active#(2nd(X)) -> active#(X),
                     active#(2nd(X)) -> 2nd#(active(X)),
           active#(2nd(cons(X, XS))) -> head#(XS),
               active#(take(X1, X2)) -> active#(X1),
               active#(take(X1, X2)) -> active#(X2),
               active#(take(X1, X2)) -> take#(X1, active(X2)),
               active#(take(X1, X2)) -> take#(active(X1), X2),
    active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)),
    active#(take(s(N), cons(X, XS))) -> take#(N, XS),
                active#(sel(X1, X2)) -> active#(X1),
                active#(sel(X1, X2)) -> active#(X2),
                active#(sel(X1, X2)) -> sel#(X1, active(X2)),
                active#(sel(X1, X2)) -> sel#(active(X1), X2),
     active#(sel(s(N), cons(X, XS))) -> sel#(N, XS),
                      head#(mark(X)) -> head#(X),
                        head#(ok(X)) -> head#(X),
                       2nd#(mark(X)) -> 2nd#(X),
                         2nd#(ok(X)) -> 2nd#(X),
                 take#(X1, mark(X2)) -> take#(X1, X2),
                 take#(mark(X1), X2) -> take#(X1, X2),
               take#(ok(X1), ok(X2)) -> take#(X1, X2),
                  sel#(X1, mark(X2)) -> sel#(X1, X2),
                  sel#(mark(X1), X2) -> sel#(X1, X2),
                sel#(ok(X1), ok(X2)) -> sel#(X1, X2),
               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),
                    proper#(head(X)) -> head#(proper(X)),
                    proper#(head(X)) -> proper#(X),
                     proper#(2nd(X)) -> 2nd#(proper(X)),
                     proper#(2nd(X)) -> proper#(X),
               proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)),
               proper#(take(X1, X2)) -> proper#(X1),
               proper#(take(X1, X2)) -> proper#(X2),
                proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)),
                proper#(sel(X1, X2)) -> proper#(X1),
                proper#(sel(X1, X2)) -> proper#(X2),
                       top#(mark(X)) -> proper#(X),
                       top#(mark(X)) -> top#(proper(X)),
                         top#(ok(X)) -> active#(X),
                         top#(ok(X)) -> top#(active(X))}
  Weak:
  {             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)),
              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)),
                   active(head(X)) -> head(active(X)),
         active(head(cons(X, XS))) -> mark(X),
                    active(2nd(X)) -> 2nd(active(X)),
          active(2nd(cons(X, XS))) -> mark(head(XS)),
              active(take(X1, X2)) -> take(X1, active(X2)),
              active(take(X1, X2)) -> take(active(X1), X2),
   active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
             active(take(0(), XS)) -> mark(nil()),
               active(sel(X1, X2)) -> sel(X1, active(X2)),
               active(sel(X1, X2)) -> sel(active(X1), X2),
    active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
     active(sel(0(), cons(X, XS))) -> mark(X),
                     head(mark(X)) -> mark(head(X)),
                       head(ok(X)) -> ok(head(X)),
                      2nd(mark(X)) -> mark(2nd(X)),
                        2nd(ok(X)) -> ok(2nd(X)),
                take(X1, mark(X2)) -> mark(take(X1, X2)),
                take(mark(X1), X2) -> mark(take(X1, X2)),
              take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                 sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                 sel(mark(X1), X2) -> mark(sel(X1, X2)),
               sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
              proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                   proper(from(X)) -> from(proper(X)),
                      proper(s(X)) -> s(proper(X)),
                   proper(head(X)) -> head(proper(X)),
                    proper(2nd(X)) -> 2nd(proper(X)),
                     proper(nil()) -> ok(nil()),
              proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                       proper(0()) -> ok(0()),
               proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                      top(mark(X)) -> top(proper(X)),
                        top(ok(X)) -> top(active(X))}
  EDG:
   {
    (active#(sel(X1, X2)) -> sel#(X1, active(X2)), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(X1, active(X2)), sel#(mark(X1), X2) -> sel#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(X1, active(X2)), sel#(X1, mark(X2)) -> sel#(X1, 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#(mark(X1), X2) -> take#(X1, X2))
    (proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)), take#(X1, mark(X2)) -> take#(X1, X2))
    (from#(mark(X)) -> from#(X), from#(ok(X)) -> from#(X))
    (from#(mark(X)) -> from#(X), from#(mark(X)) -> from#(X))
    (s#(mark(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (active#(from(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (active#(from(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (active#(s(X)) -> active#(X), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
    (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (active#(s(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (active#(s(X)) -> active#(X), active#(take(X1, X2)) -> take#(active(X1), X2))
    (active#(s(X)) -> active#(X), active#(take(X1, X2)) -> take#(X1, active(X2)))
    (active#(s(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
    (active#(s(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(2nd(cons(X, XS))) -> head#(XS))
    (active#(s(X)) -> active#(X), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(s(X)) -> active#(X), active#(2nd(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(s(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(s(X)) -> active#(X), active#(from(X)) -> active#(X))
    (active#(s(X)) -> active#(X), active#(from(X)) -> s#(X))
    (active#(s(X)) -> active#(X), active#(from(X)) -> from#(active(X)))
    (active#(s(X)) -> active#(X), active#(from(X)) -> from#(s(X)))
    (active#(s(X)) -> active#(X), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(2nd(X)) -> active#(X), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(2nd(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(2nd(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(2nd(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
    (active#(2nd(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
    (active#(2nd(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (active#(2nd(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (active#(2nd(X)) -> active#(X), active#(take(X1, X2)) -> take#(active(X1), X2))
    (active#(2nd(X)) -> active#(X), active#(take(X1, X2)) -> take#(X1, active(X2)))
    (active#(2nd(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
    (active#(2nd(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1))
    (active#(2nd(X)) -> active#(X), active#(2nd(cons(X, XS))) -> head#(XS))
    (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
    (active#(2nd(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(2nd(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(2nd(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(2nd(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(2nd(X)) -> active#(X), active#(from(X)) -> active#(X))
    (active#(2nd(X)) -> active#(X), active#(from(X)) -> 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)) -> cons#(X, from(s(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))
    (head#(ok(X)) -> head#(X), head#(ok(X)) -> head#(X))
    (head#(ok(X)) -> head#(X), head#(mark(X)) -> head#(X))
    (2nd#(ok(X)) -> 2nd#(X), 2nd#(ok(X)) -> 2nd#(X))
    (2nd#(ok(X)) -> 2nd#(X), 2nd#(mark(X)) -> 2nd#(X))
    (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)))
    (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (proper#(s(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(2nd(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(2nd(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(2nd(X)) -> proper#(X), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(2nd(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
    (proper#(2nd(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
    (proper#(2nd(X)) -> proper#(X), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)))
    (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
    (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(2nd(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(2nd(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(2nd(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (proper#(2nd(X)) -> proper#(X), proper#(from(X)) -> from#(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#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (top#(ok(X)) -> active#(X), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (top#(ok(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (top#(ok(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (top#(ok(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
    (top#(ok(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (top#(ok(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (top#(ok(X)) -> active#(X), active#(take(X1, X2)) -> take#(active(X1), X2))
    (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)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(2nd(cons(X, XS))) -> head#(XS))
    (top#(ok(X)) -> active#(X), active#(2nd(X)) -> 2nd#(active(X)))
    (top#(ok(X)) -> active#(X), active#(2nd(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (top#(ok(X)) -> active#(X), active#(head(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> active#(X))
    (top#(ok(X)) -> active#(X), active#(from(X)) -> 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)) -> cons#(X, from(s(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))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(mark(X1), X2) -> sel#(X1, X2))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X2), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (active#(sel(X1, X2)) -> active#(X2), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (active#(sel(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> take#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> take#(X1, active(X2)))
    (active#(sel(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X2), active#(2nd(cons(X, XS))) -> head#(XS))
    (active#(sel(X1, X2)) -> active#(X2), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(sel(X1, X2)) -> active#(X2), active#(2nd(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X2), active#(head(X)) -> head#(active(X)))
    (active#(sel(X1, X2)) -> active#(X2), active#(head(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X)))
    (active#(sel(X1, X2)) -> active#(X2), active#(from(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X2), active#(from(X)) -> s#(X))
    (active#(sel(X1, X2)) -> active#(X2), active#(from(X)) -> from#(active(X)))
    (active#(sel(X1, X2)) -> active#(X2), active#(from(X)) -> from#(s(X)))
    (active#(sel(X1, X2)) -> active#(X2), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(sel(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(head(X)) -> head#(proper(X)))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(from(X)) -> from#(proper(X)))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(take(X1, X2)) -> take#(active(X1), X2), take#(ok(X1), ok(X2)) -> take#(X1, X2))
    (active#(take(X1, X2)) -> take#(active(X1), X2), take#(mark(X1), X2) -> take#(X1, X2))
    (active#(take(X1, X2)) -> take#(active(X1), X2), take#(X1, mark(X2)) -> take#(X1, X2))
    (active#(2nd(cons(X, XS))) -> head#(XS), head#(ok(X)) -> head#(X))
    (active#(2nd(cons(X, XS))) -> head#(XS), head#(mark(X)) -> head#(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))
    (take#(mark(X1), 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#(mark(X1), X2) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (sel#(ok(X1), ok(X2)) -> sel#(X1, X2), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (sel#(ok(X1), ok(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(ok(X1), ok(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (active#(from(X)) -> from#(s(X)), from#(ok(X)) -> from#(X))
    (active#(from(X)) -> from#(s(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))
    (active#(2nd(X)) -> 2nd#(active(X)), 2nd#(ok(X)) -> 2nd#(X))
    (active#(2nd(X)) -> 2nd#(active(X)), 2nd#(mark(X)) -> 2nd#(X))
    (proper#(s(X)) -> s#(proper(X)), s#(ok(X)) -> s#(X))
    (proper#(s(X)) -> s#(proper(X)), s#(mark(X)) -> s#(X))
    (proper#(2nd(X)) -> 2nd#(proper(X)), 2nd#(ok(X)) -> 2nd#(X))
    (proper#(2nd(X)) -> 2nd#(proper(X)), 2nd#(mark(X)) -> 2nd#(X))
    (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))
    (active#(take(X1, X2)) -> active#(X1), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(take(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(take(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(take(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X2))
    (active#(take(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
    (active#(take(X1, X2)) -> active#(X1), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (active#(take(X1, X2)) -> active#(X1), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (active#(take(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> take#(active(X1), X2))
    (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)) -> active#(X1))
    (active#(take(X1, X2)) -> active#(X1), active#(2nd(cons(X, XS))) -> head#(XS))
    (active#(take(X1, X2)) -> active#(X1), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(take(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
    (active#(take(X1, X2)) -> active#(X1), active#(head(X)) -> head#(active(X)))
    (active#(take(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
    (active#(take(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(take(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(take(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
    (active#(take(X1, X2)) -> active#(X1), active#(from(X)) -> s#(X))
    (active#(take(X1, X2)) -> active#(X1), active#(from(X)) -> from#(active(X)))
    (active#(take(X1, X2)) -> active#(X1), active#(from(X)) -> from#(s(X)))
    (active#(take(X1, X2)) -> active#(X1), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(take(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
    (active#(take(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> take#(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)))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> head#(proper(X)))
    (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#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(head(X)) -> head#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(s(X)) -> s#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(from(X)) -> from#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(from(X)) -> from#(proper(X)))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(from(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#(head(X)) -> head#(proper(X)))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(2nd(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#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(take(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X1), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(sel(X1, X2)) -> active#(X1), active#(from(X)) -> from#(s(X)))
    (active#(sel(X1, X2)) -> active#(X1), active#(from(X)) -> from#(active(X)))
    (active#(sel(X1, X2)) -> active#(X1), active#(from(X)) -> s#(X))
    (active#(sel(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X1), active#(head(X)) -> head#(active(X)))
    (active#(sel(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
    (active#(sel(X1, X2)) -> active#(X1), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(sel(X1, X2)) -> active#(X1), active#(2nd(cons(X, XS))) -> head#(XS))
    (active#(sel(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> take#(X1, active(X2)))
    (active#(sel(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> take#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (active#(sel(X1, X2)) -> active#(X1), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(sel(X1, X2)) -> active#(X1), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (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#(from(X)) -> cons#(X, from(s(X))))
    (active#(cons(X1, X2)) -> active#(X1), active#(from(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)) -> s#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> s#(active(X)))
    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
    (active#(cons(X1, X2)) -> active#(X1), active#(head(X)) -> head#(active(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#(2nd(cons(X, XS))) -> head#(XS))
    (active#(cons(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X1))
    (active#(cons(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> take#(X1, active(X2)))
    (active#(cons(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> take#(active(X1), X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (active#(cons(X1, X2)) -> active#(X1), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(cons(X1, X2)) -> active#(X1), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X)))
    (proper#(head(X)) -> head#(proper(X)), head#(mark(X)) -> head#(X))
    (proper#(head(X)) -> head#(proper(X)), head#(ok(X)) -> head#(X))
    (proper#(from(X)) -> from#(proper(X)), from#(mark(X)) -> from#(X))
    (proper#(from(X)) -> from#(proper(X)), from#(ok(X)) -> from#(X))
    (active#(head(X)) -> head#(active(X)), head#(mark(X)) -> head#(X))
    (active#(head(X)) -> head#(active(X)), head#(ok(X)) -> head#(X))
    (active#(from(X)) -> from#(active(X)), from#(mark(X)) -> from#(X))
    (active#(from(X)) -> from#(active(X)), from#(ok(X)) -> from#(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))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(ok(X1), ok(X2)) -> sel#(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#(ok(X1), ok(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))
    (take#(X1, mark(X2)) -> take#(X1, X2), take#(ok(X1), ok(X2)) -> take#(X1, X2))
    (cons#(mark(X1), 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))
    (active#(sel(X1, X2)) -> sel#(active(X1), X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(active(X1), X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (active#(sel(X1, X2)) -> sel#(active(X1), X2), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (active#(cons(X1, X2)) -> cons#(active(X1), X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(cons(X1, X2)) -> cons#(active(X1), X2), cons#(ok(X1), ok(X2)) -> cons#(X1, X2))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(from(X)) -> from#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(head(X)) -> head#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
    (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#(X2), proper#(from(X)) -> from#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> s#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(head(X)) -> head#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(cons(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
    (active#(take(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(take(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
    (active#(take(X1, X2)) -> active#(X2), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(take(X1, X2)) -> active#(X2), active#(from(X)) -> from#(s(X)))
    (active#(take(X1, X2)) -> active#(X2), active#(from(X)) -> from#(active(X)))
    (active#(take(X1, X2)) -> active#(X2), active#(from(X)) -> s#(X))
    (active#(take(X1, X2)) -> active#(X2), active#(from(X)) -> active#(X))
    (active#(take(X1, X2)) -> active#(X2), active#(s(X)) -> s#(active(X)))
    (active#(take(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
    (active#(take(X1, X2)) -> active#(X2), active#(head(X)) -> active#(X))
    (active#(take(X1, X2)) -> active#(X2), active#(head(X)) -> head#(active(X)))
    (active#(take(X1, X2)) -> active#(X2), active#(2nd(X)) -> active#(X))
    (active#(take(X1, X2)) -> active#(X2), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(take(X1, X2)) -> active#(X2), active#(2nd(cons(X, XS))) -> head#(XS))
    (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> active#(X1))
    (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> active#(X2))
    (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> take#(X1, active(X2)))
    (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> take#(active(X1), X2))
    (active#(take(X1, X2)) -> active#(X2), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (active#(take(X1, X2)) -> active#(X2), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (active#(take(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
    (active#(take(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X2))
    (active#(take(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(take(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(take(X1, X2)) -> active#(X2), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (active#(take(s(N), cons(X, XS))) -> take#(N, XS), take#(X1, mark(X2)) -> take#(X1, X2))
    (active#(take(s(N), cons(X, XS))) -> take#(N, XS), take#(mark(X1), X2) -> take#(X1, X2))
    (active#(take(s(N), cons(X, XS))) -> take#(N, XS), take#(ok(X1), ok(X2)) -> take#(X1, X2))
    (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))
    (top#(mark(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(from(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#(head(X)) -> head#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(2nd(X)) -> 2nd#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(2nd(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#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (top#(mark(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(head(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(head(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
    (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)))
    (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
    (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
    (proper#(head(X)) -> proper#(X), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(head(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(head(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)))
    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
    (proper#(from(X)) -> proper#(X), proper#(from(X)) -> from#(proper(X)))
    (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
    (proper#(from(X)) -> proper#(X), proper#(s(X)) -> s#(proper(X)))
    (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
    (proper#(from(X)) -> proper#(X), proper#(head(X)) -> head#(proper(X)))
    (proper#(from(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
    (proper#(from(X)) -> proper#(X), proper#(2nd(X)) -> 2nd#(proper(X)))
    (proper#(from(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
    (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> take#(proper(X1), proper(X2)))
    (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
    (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
    (proper#(from(X)) -> proper#(X), proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)))
    (proper#(from(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X1))
    (proper#(from(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
    (2nd#(mark(X)) -> 2nd#(X), 2nd#(mark(X)) -> 2nd#(X))
    (2nd#(mark(X)) -> 2nd#(X), 2nd#(ok(X)) -> 2nd#(X))
    (head#(mark(X)) -> head#(X), head#(mark(X)) -> head#(X))
    (head#(mark(X)) -> head#(X), head#(ok(X)) -> head#(X))
    (active#(head(X)) -> active#(X), active#(cons(X1, X2)) -> cons#(active(X1), X2))
    (active#(head(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
    (active#(head(X)) -> active#(X), active#(from(X)) -> cons#(X, from(s(X))))
    (active#(head(X)) -> active#(X), active#(from(X)) -> from#(s(X)))
    (active#(head(X)) -> active#(X), active#(from(X)) -> from#(active(X)))
    (active#(head(X)) -> active#(X), active#(from(X)) -> s#(X))
    (active#(head(X)) -> active#(X), active#(from(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(s(X)) -> s#(active(X)))
    (active#(head(X)) -> active#(X), active#(s(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(head(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(head(X)) -> active#(X), active#(2nd(X)) -> active#(X))
    (active#(head(X)) -> active#(X), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(head(X)) -> active#(X), active#(2nd(cons(X, XS))) -> head#(XS))
    (active#(head(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1))
    (active#(head(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
    (active#(head(X)) -> active#(X), active#(take(X1, X2)) -> take#(X1, active(X2)))
    (active#(head(X)) -> active#(X), active#(take(X1, X2)) -> take#(active(X1), X2))
    (active#(head(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (active#(head(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (active#(head(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
    (active#(head(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
    (active#(head(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(head(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(head(X)) -> active#(X), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (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#(from(X)) -> cons#(X, from(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)) -> s#(X))
    (active#(from(X)) -> active#(X), active#(from(X)) -> active#(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#(head(X)) -> active#(X))
    (active#(from(X)) -> active#(X), active#(head(X)) -> head#(active(X)))
    (active#(from(X)) -> active#(X), active#(2nd(X)) -> active#(X))
    (active#(from(X)) -> active#(X), active#(2nd(X)) -> 2nd#(active(X)))
    (active#(from(X)) -> active#(X), active#(2nd(cons(X, XS))) -> head#(XS))
    (active#(from(X)) -> active#(X), active#(take(X1, X2)) -> active#(X1))
    (active#(from(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
    (active#(from(X)) -> active#(X), active#(take(X1, X2)) -> take#(X1, active(X2)))
    (active#(from(X)) -> active#(X), active#(take(X1, X2)) -> take#(active(X1), X2))
    (active#(from(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> cons#(X, take(N, XS)))
    (active#(from(X)) -> active#(X), active#(take(s(N), cons(X, XS))) -> take#(N, XS))
    (active#(from(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
    (active#(from(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
    (active#(from(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(X1, active(X2)))
    (active#(from(X)) -> active#(X), active#(sel(X1, X2)) -> sel#(active(X1), X2))
    (active#(from(X)) -> active#(X), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (s#(ok(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (s#(ok(X)) -> s#(X), s#(ok(X)) -> s#(X))
    (from#(ok(X)) -> from#(X), from#(mark(X)) -> from#(X))
    (from#(ok(X)) -> from#(X), from#(ok(X)) -> from#(X))
    (proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)), sel#(mark(X1), X2) -> sel#(X1, X2))
    (proper#(sel(X1, X2)) -> sel#(proper(X1), proper(X2)), sel#(ok(X1), ok(X2)) -> sel#(X1, X2))
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (proper#(cons(X1, X2)) -> cons#(proper(X1), proper(X2)), cons#(ok(X1), ok(X2)) -> cons#(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)) -> take#(X1, active(X2)), take#(ok(X1), ok(X2)) -> take#(X1, X2))
   }
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {proper#(cons(X1, X2)) -> proper#(X1),
      proper#(cons(X1, X2)) -> proper#(X2),
           proper#(from(X)) -> proper#(X),
              proper#(s(X)) -> proper#(X),
           proper#(head(X)) -> proper#(X),
            proper#(2nd(X)) -> proper#(X),
      proper#(take(X1, X2)) -> proper#(X1),
      proper#(take(X1, X2)) -> proper#(X2),
       proper#(sel(X1, X2)) -> proper#(X1),
       proper#(sel(X1, X2)) -> proper#(X2)}
    Scc:
     {  sel#(X1, mark(X2)) -> sel#(X1, X2),
        sel#(mark(X1), X2) -> sel#(X1, X2),
      sel#(ok(X1), ok(X2)) -> sel#(X1, X2)}
    Scc:
     {  take#(X1, mark(X2)) -> take#(X1, X2),
        take#(mark(X1), X2) -> take#(X1, X2),
      take#(ok(X1), ok(X2)) -> take#(X1, X2)}
    Scc:
     {2nd#(mark(X)) -> 2nd#(X),
        2nd#(ok(X)) -> 2nd#(X)}
    Scc:
     {head#(mark(X)) -> head#(X),
        head#(ok(X)) -> head#(X)}
    Scc:
     {active#(cons(X1, X2)) -> active#(X1),
           active#(from(X)) -> active#(X),
              active#(s(X)) -> active#(X),
           active#(head(X)) -> active#(X),
            active#(2nd(X)) -> active#(X),
      active#(take(X1, X2)) -> active#(X1),
      active#(take(X1, X2)) -> active#(X2),
       active#(sel(X1, X2)) -> active#(X1),
       active#(sel(X1, X2)) -> active#(X2)}
    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:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     Fail
    SCC:
     Strict:
      {proper#(cons(X1, X2)) -> proper#(X1),
       proper#(cons(X1, X2)) -> proper#(X2),
            proper#(from(X)) -> proper#(X),
               proper#(s(X)) -> proper#(X),
            proper#(head(X)) -> proper#(X),
             proper#(2nd(X)) -> proper#(X),
       proper#(take(X1, X2)) -> proper#(X1),
       proper#(take(X1, X2)) -> proper#(X2),
        proper#(sel(X1, X2)) -> proper#(X1),
        proper#(sel(X1, X2)) -> proper#(X2)}
     Weak:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {proper#(cons(X1, X2)) -> proper#(X1),
        proper#(cons(X1, X2)) -> proper#(X2),
             proper#(from(X)) -> proper#(X),
                proper#(s(X)) -> proper#(X),
             proper#(head(X)) -> proper#(X),
              proper#(2nd(X)) -> proper#(X),
        proper#(take(X1, X2)) -> proper#(X1),
        proper#(take(X1, X2)) -> proper#(X2),
         proper#(sel(X1, X2)) -> proper#(X2)}
      EDG:
       {(proper#(take(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2))
        (proper#(take(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1))
        (proper#(take(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
        (proper#(take(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
        (proper#(take(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(take(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
        (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(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#(from(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
        (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
        (proper#(from(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
        (proper#(from(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
        (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(from(X)) -> proper#(X), proper#(from(X)) -> 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#(head(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
        (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
        (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
        (proper#(head(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
        (proper#(head(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
        (proper#(head(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(head(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
        (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
        (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)) -> proper#(X))
        (proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(2nd(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
        (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
        (proper#(2nd(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
        (proper#(2nd(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
        (proper#(2nd(X)) -> proper#(X), proper#(sel(X1, X2)) -> 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)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
        (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
        (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#(sel(X1, X2)) -> proper#(X2))
        (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(take(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
        (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
        (proper#(take(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
        (proper#(take(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
        (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#(sel(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2))
        (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(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)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2))
        (proper#(cons(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))}
       SCCS:
        Scc:
         {proper#(cons(X1, X2)) -> proper#(X1),
          proper#(cons(X1, X2)) -> proper#(X2),
               proper#(from(X)) -> proper#(X),
                  proper#(s(X)) -> proper#(X),
               proper#(head(X)) -> proper#(X),
                proper#(2nd(X)) -> proper#(X),
          proper#(take(X1, X2)) -> proper#(X1),
          proper#(take(X1, X2)) -> proper#(X2),
           proper#(sel(X1, X2)) -> proper#(X2)}
        SCC:
         Strict:
          {proper#(cons(X1, X2)) -> proper#(X1),
           proper#(cons(X1, X2)) -> proper#(X2),
                proper#(from(X)) -> proper#(X),
                   proper#(s(X)) -> proper#(X),
                proper#(head(X)) -> proper#(X),
                 proper#(2nd(X)) -> proper#(X),
           proper#(take(X1, X2)) -> proper#(X1),
           proper#(take(X1, X2)) -> proper#(X2),
            proper#(sel(X1, X2)) -> proper#(X2)}
         Weak:
         {             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)),
                     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)),
                          active(head(X)) -> head(active(X)),
                active(head(cons(X, XS))) -> mark(X),
                           active(2nd(X)) -> 2nd(active(X)),
                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                     active(take(X1, X2)) -> take(X1, active(X2)),
                     active(take(X1, X2)) -> take(active(X1), X2),
          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                    active(take(0(), XS)) -> mark(nil()),
                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                      active(sel(X1, X2)) -> sel(active(X1), X2),
           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
            active(sel(0(), cons(X, XS))) -> mark(X),
                            head(mark(X)) -> mark(head(X)),
                              head(ok(X)) -> ok(head(X)),
                             2nd(mark(X)) -> mark(2nd(X)),
                               2nd(ok(X)) -> ok(2nd(X)),
                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                       take(mark(X1), X2) -> mark(take(X1, X2)),
                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             proper(s(X)) -> s(proper(X)),
                          proper(head(X)) -> head(proper(X)),
                           proper(2nd(X)) -> 2nd(proper(X)),
                            proper(nil()) -> ok(nil()),
                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {proper#(cons(X1, X2)) -> proper#(X1),
                 proper#(from(X)) -> proper#(X),
                    proper#(s(X)) -> proper#(X),
                 proper#(head(X)) -> proper#(X),
                  proper#(2nd(X)) -> proper#(X),
            proper#(take(X1, X2)) -> proper#(X1),
            proper#(take(X1, X2)) -> proper#(X2),
             proper#(sel(X1, X2)) -> proper#(X2)}
          EDG:
           {(proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X2))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
            (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(take(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2))
            (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
            (proper#(take(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
            (proper#(take(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
            (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(take(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
            (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
            (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
            (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
            (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(2nd(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(2nd(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
            (proper#(2nd(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
            (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
            (proper#(2nd(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
            (proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(2nd(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
            (proper#(2nd(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(head(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
            (proper#(head(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(head(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
            (proper#(head(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
            (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
            (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
            (proper#(head(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
            (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
            (proper#(from(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
            (proper#(from(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
            (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
            (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X2))
            (proper#(from(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X2))
            (proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
            (proper#(take(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
            (proper#(take(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
            (proper#(take(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
            (proper#(take(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
            (proper#(take(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
            (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#(sel(X1, X2)) -> proper#(X2))}
           SCCS:
            Scc:
             {proper#(cons(X1, X2)) -> proper#(X1),
                   proper#(from(X)) -> proper#(X),
                      proper#(s(X)) -> proper#(X),
                   proper#(head(X)) -> proper#(X),
                    proper#(2nd(X)) -> proper#(X),
              proper#(take(X1, X2)) -> proper#(X1),
              proper#(take(X1, X2)) -> proper#(X2),
               proper#(sel(X1, X2)) -> proper#(X2)}
            SCC:
             Strict:
              {proper#(cons(X1, X2)) -> proper#(X1),
                    proper#(from(X)) -> proper#(X),
                       proper#(s(X)) -> proper#(X),
                    proper#(head(X)) -> proper#(X),
                     proper#(2nd(X)) -> proper#(X),
               proper#(take(X1, X2)) -> proper#(X1),
               proper#(take(X1, X2)) -> proper#(X2),
                proper#(sel(X1, X2)) -> proper#(X2)}
             Weak:
             {             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)),
                         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)),
                              active(head(X)) -> head(active(X)),
                    active(head(cons(X, XS))) -> mark(X),
                               active(2nd(X)) -> 2nd(active(X)),
                     active(2nd(cons(X, XS))) -> mark(head(XS)),
                         active(take(X1, X2)) -> take(X1, active(X2)),
                         active(take(X1, X2)) -> take(active(X1), X2),
              active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                        active(take(0(), XS)) -> mark(nil()),
                          active(sel(X1, X2)) -> sel(X1, active(X2)),
                          active(sel(X1, X2)) -> sel(active(X1), X2),
               active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                active(sel(0(), cons(X, XS))) -> mark(X),
                                head(mark(X)) -> mark(head(X)),
                                  head(ok(X)) -> ok(head(X)),
                                 2nd(mark(X)) -> mark(2nd(X)),
                                   2nd(ok(X)) -> ok(2nd(X)),
                           take(X1, mark(X2)) -> mark(take(X1, X2)),
                           take(mark(X1), X2) -> mark(take(X1, X2)),
                         take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                            sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                            sel(mark(X1), X2) -> mark(sel(X1, X2)),
                          sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                              proper(from(X)) -> from(proper(X)),
                                 proper(s(X)) -> s(proper(X)),
                              proper(head(X)) -> head(proper(X)),
                               proper(2nd(X)) -> 2nd(proper(X)),
                                proper(nil()) -> ok(nil()),
                         proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                  proper(0()) -> ok(0()),
                          proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                 top(mark(X)) -> top(proper(X)),
                                   top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(proper#) = 0
              Strict:
               {proper#(cons(X1, X2)) -> proper#(X1),
                     proper#(from(X)) -> proper#(X),
                        proper#(s(X)) -> proper#(X),
                     proper#(head(X)) -> proper#(X),
                      proper#(2nd(X)) -> proper#(X),
                proper#(take(X1, X2)) -> proper#(X1),
                 proper#(sel(X1, X2)) -> proper#(X2)}
              EDG:
               {(proper#(cons(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(from(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
                (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                (proper#(from(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                (proper#(from(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(head(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
                (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                (proper#(head(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                (proper#(head(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                (proper#(head(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(head(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(2nd(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(2nd(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                (proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(2nd(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                (proper#(2nd(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                (proper#(2nd(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
                (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                (proper#(s(X)) -> proper#(X), proper#(sel(X1, X2)) -> proper#(X2))
                (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(take(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                (proper#(take(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
                (proper#(take(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
                (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                (proper#(take(X1, X2)) -> proper#(X1), proper#(sel(X1, X2)) -> proper#(X2))
                (proper#(sel(X1, X2)) -> proper#(X2), proper#(cons(X1, X2)) -> proper#(X1))
                (proper#(sel(X1, X2)) -> proper#(X2), proper#(from(X)) -> proper#(X))
                (proper#(sel(X1, X2)) -> proper#(X2), proper#(s(X)) -> proper#(X))
                (proper#(sel(X1, X2)) -> proper#(X2), proper#(head(X)) -> proper#(X))
                (proper#(sel(X1, X2)) -> proper#(X2), proper#(2nd(X)) -> proper#(X))
                (proper#(sel(X1, X2)) -> proper#(X2), proper#(take(X1, X2)) -> proper#(X1))
                (proper#(sel(X1, X2)) -> proper#(X2), proper#(sel(X1, X2)) -> proper#(X2))}
               SCCS:
                Scc:
                 {proper#(cons(X1, X2)) -> proper#(X1),
                       proper#(from(X)) -> proper#(X),
                          proper#(s(X)) -> proper#(X),
                       proper#(head(X)) -> proper#(X),
                        proper#(2nd(X)) -> proper#(X),
                  proper#(take(X1, X2)) -> proper#(X1),
                   proper#(sel(X1, X2)) -> proper#(X2)}
                SCC:
                 Strict:
                  {proper#(cons(X1, X2)) -> proper#(X1),
                        proper#(from(X)) -> proper#(X),
                           proper#(s(X)) -> proper#(X),
                        proper#(head(X)) -> proper#(X),
                         proper#(2nd(X)) -> proper#(X),
                   proper#(take(X1, X2)) -> proper#(X1),
                    proper#(sel(X1, X2)) -> proper#(X2)}
                 Weak:
                 {             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)),
                             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)),
                                  active(head(X)) -> head(active(X)),
                        active(head(cons(X, XS))) -> mark(X),
                                   active(2nd(X)) -> 2nd(active(X)),
                         active(2nd(cons(X, XS))) -> mark(head(XS)),
                             active(take(X1, X2)) -> take(X1, active(X2)),
                             active(take(X1, X2)) -> take(active(X1), X2),
                  active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                            active(take(0(), XS)) -> mark(nil()),
                              active(sel(X1, X2)) -> sel(X1, active(X2)),
                              active(sel(X1, X2)) -> sel(active(X1), X2),
                   active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                    active(sel(0(), cons(X, XS))) -> mark(X),
                                    head(mark(X)) -> mark(head(X)),
                                      head(ok(X)) -> ok(head(X)),
                                     2nd(mark(X)) -> mark(2nd(X)),
                                       2nd(ok(X)) -> ok(2nd(X)),
                               take(X1, mark(X2)) -> mark(take(X1, X2)),
                               take(mark(X1), X2) -> mark(take(X1, X2)),
                             take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                sel(mark(X1), X2) -> mark(sel(X1, X2)),
                              sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                  proper(from(X)) -> from(proper(X)),
                                     proper(s(X)) -> s(proper(X)),
                                  proper(head(X)) -> head(proper(X)),
                                   proper(2nd(X)) -> 2nd(proper(X)),
                                    proper(nil()) -> ok(nil()),
                             proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                      proper(0()) -> ok(0()),
                              proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                     top(mark(X)) -> top(proper(X)),
                                       top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(proper#) = 0
                  Strict:
                   {proper#(cons(X1, X2)) -> proper#(X1),
                         proper#(from(X)) -> proper#(X),
                            proper#(s(X)) -> proper#(X),
                         proper#(head(X)) -> proper#(X),
                          proper#(2nd(X)) -> proper#(X),
                    proper#(take(X1, X2)) -> proper#(X1)}
                  EDG:
                   {(proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                    (proper#(s(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                    (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(2nd(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                    (proper#(2nd(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                    (proper#(2nd(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                    (proper#(2nd(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(2nd(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                    (proper#(2nd(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                    (proper#(take(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
                    (proper#(take(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
                    (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                    (proper#(take(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                    (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(2nd(X)) -> proper#(X))
                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                    (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(head(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                    (proper#(head(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(head(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                    (proper#(head(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                    (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                    (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                    (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                    (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                    (proper#(from(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                    (proper#(from(X)) -> proper#(X), proper#(2nd(X)) -> proper#(X))
                    (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))}
                   SCCS:
                    Scc:
                     {proper#(cons(X1, X2)) -> proper#(X1),
                           proper#(from(X)) -> proper#(X),
                              proper#(s(X)) -> proper#(X),
                           proper#(head(X)) -> proper#(X),
                            proper#(2nd(X)) -> proper#(X),
                      proper#(take(X1, X2)) -> proper#(X1)}
                    SCC:
                     Strict:
                      {proper#(cons(X1, X2)) -> proper#(X1),
                            proper#(from(X)) -> proper#(X),
                               proper#(s(X)) -> proper#(X),
                            proper#(head(X)) -> proper#(X),
                             proper#(2nd(X)) -> proper#(X),
                       proper#(take(X1, X2)) -> proper#(X1)}
                     Weak:
                     {             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)),
                                 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)),
                                      active(head(X)) -> head(active(X)),
                            active(head(cons(X, XS))) -> mark(X),
                                       active(2nd(X)) -> 2nd(active(X)),
                             active(2nd(cons(X, XS))) -> mark(head(XS)),
                                 active(take(X1, X2)) -> take(X1, active(X2)),
                                 active(take(X1, X2)) -> take(active(X1), X2),
                      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                active(take(0(), XS)) -> mark(nil()),
                                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                                  active(sel(X1, X2)) -> sel(active(X1), X2),
                       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                        active(sel(0(), cons(X, XS))) -> mark(X),
                                        head(mark(X)) -> mark(head(X)),
                                          head(ok(X)) -> ok(head(X)),
                                         2nd(mark(X)) -> mark(2nd(X)),
                                           2nd(ok(X)) -> ok(2nd(X)),
                                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                                   take(mark(X1), X2) -> mark(take(X1, X2)),
                                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                      proper(from(X)) -> from(proper(X)),
                                         proper(s(X)) -> s(proper(X)),
                                      proper(head(X)) -> head(proper(X)),
                                       proper(2nd(X)) -> 2nd(proper(X)),
                                        proper(nil()) -> ok(nil()),
                                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                          proper(0()) -> ok(0()),
                                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                         top(mark(X)) -> top(proper(X)),
                                           top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(proper#) = 0
                      Strict:
                       {proper#(cons(X1, X2)) -> proper#(X1),
                             proper#(from(X)) -> proper#(X),
                                proper#(s(X)) -> proper#(X),
                             proper#(head(X)) -> proper#(X),
                        proper#(take(X1, X2)) -> proper#(X1)}
                      EDG:
                       {(proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                        (proper#(s(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                        (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(s(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                        (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                        (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(take(X1, X2)) -> proper#(X1), proper#(from(X)) -> proper#(X))
                        (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                        (proper#(take(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
                        (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                        (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(head(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                        (proper#(head(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(head(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                        (proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                        (proper#(from(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                        (proper#(from(X)) -> proper#(X), proper#(from(X)) -> proper#(X))
                        (proper#(from(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                        (proper#(from(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                        (proper#(from(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))}
                       SCCS:
                        Scc:
                         {proper#(cons(X1, X2)) -> proper#(X1),
                               proper#(from(X)) -> proper#(X),
                                  proper#(s(X)) -> proper#(X),
                               proper#(head(X)) -> proper#(X),
                          proper#(take(X1, X2)) -> proper#(X1)}
                        SCC:
                         Strict:
                          {proper#(cons(X1, X2)) -> proper#(X1),
                                proper#(from(X)) -> proper#(X),
                                   proper#(s(X)) -> proper#(X),
                                proper#(head(X)) -> proper#(X),
                           proper#(take(X1, X2)) -> proper#(X1)}
                         Weak:
                         {             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)),
                                     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)),
                                          active(head(X)) -> head(active(X)),
                                active(head(cons(X, XS))) -> mark(X),
                                           active(2nd(X)) -> 2nd(active(X)),
                                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                                     active(take(X1, X2)) -> take(X1, active(X2)),
                                     active(take(X1, X2)) -> take(active(X1), X2),
                          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                    active(take(0(), XS)) -> mark(nil()),
                                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                                      active(sel(X1, X2)) -> sel(active(X1), X2),
                           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                            active(sel(0(), cons(X, XS))) -> mark(X),
                                            head(mark(X)) -> mark(head(X)),
                                              head(ok(X)) -> ok(head(X)),
                                             2nd(mark(X)) -> mark(2nd(X)),
                                               2nd(ok(X)) -> ok(2nd(X)),
                                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                                       take(mark(X1), X2) -> mark(take(X1, X2)),
                                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                          proper(from(X)) -> from(proper(X)),
                                             proper(s(X)) -> s(proper(X)),
                                          proper(head(X)) -> head(proper(X)),
                                           proper(2nd(X)) -> 2nd(proper(X)),
                                            proper(nil()) -> ok(nil()),
                                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                              proper(0()) -> ok(0()),
                                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                             top(mark(X)) -> top(proper(X)),
                                               top(ok(X)) -> top(active(X))}
                         SPSC:
                          Simple Projection:
                           pi(proper#) = 0
                          Strict:
                           {proper#(cons(X1, X2)) -> proper#(X1),
                                    proper#(s(X)) -> proper#(X),
                                 proper#(head(X)) -> proper#(X),
                            proper#(take(X1, X2)) -> proper#(X1)}
                          EDG:
                           {(proper#(head(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                            (proper#(head(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                            (proper#(head(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                            (proper#(head(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                            (proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                            (proper#(take(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
                            (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                            (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                            (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                            (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                            (proper#(cons(X1, X2)) -> proper#(X1), proper#(head(X)) -> proper#(X))
                            (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                            (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                            (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                            (proper#(s(X)) -> proper#(X), proper#(head(X)) -> proper#(X))
                            (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))}
                           SCCS:
                            Scc:
                             {proper#(cons(X1, X2)) -> proper#(X1),
                                      proper#(s(X)) -> proper#(X),
                                   proper#(head(X)) -> proper#(X),
                              proper#(take(X1, X2)) -> proper#(X1)}
                            SCC:
                             Strict:
                              {proper#(cons(X1, X2)) -> proper#(X1),
                                       proper#(s(X)) -> proper#(X),
                                    proper#(head(X)) -> proper#(X),
                               proper#(take(X1, X2)) -> proper#(X1)}
                             Weak:
                             {             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)),
                                         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)),
                                              active(head(X)) -> head(active(X)),
                                    active(head(cons(X, XS))) -> mark(X),
                                               active(2nd(X)) -> 2nd(active(X)),
                                     active(2nd(cons(X, XS))) -> mark(head(XS)),
                                         active(take(X1, X2)) -> take(X1, active(X2)),
                                         active(take(X1, X2)) -> take(active(X1), X2),
                              active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                        active(take(0(), XS)) -> mark(nil()),
                                          active(sel(X1, X2)) -> sel(X1, active(X2)),
                                          active(sel(X1, X2)) -> sel(active(X1), X2),
                               active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                active(sel(0(), cons(X, XS))) -> mark(X),
                                                head(mark(X)) -> mark(head(X)),
                                                  head(ok(X)) -> ok(head(X)),
                                                 2nd(mark(X)) -> mark(2nd(X)),
                                                   2nd(ok(X)) -> ok(2nd(X)),
                                           take(X1, mark(X2)) -> mark(take(X1, X2)),
                                           take(mark(X1), X2) -> mark(take(X1, X2)),
                                         take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                            sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                            sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                          sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                              proper(from(X)) -> from(proper(X)),
                                                 proper(s(X)) -> s(proper(X)),
                                              proper(head(X)) -> head(proper(X)),
                                               proper(2nd(X)) -> 2nd(proper(X)),
                                                proper(nil()) -> ok(nil()),
                                         proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                                  proper(0()) -> ok(0()),
                                          proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                 top(mark(X)) -> top(proper(X)),
                                                   top(ok(X)) -> top(active(X))}
                             SPSC:
                              Simple Projection:
                               pi(proper#) = 0
                              Strict:
                               {proper#(cons(X1, X2)) -> proper#(X1),
                                        proper#(s(X)) -> proper#(X),
                                proper#(take(X1, X2)) -> proper#(X1)}
                              EDG:
                               {(proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                                (proper#(take(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                                (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                                (proper#(s(X)) -> proper#(X), proper#(cons(X1, X2)) -> proper#(X1))
                                (proper#(s(X)) -> proper#(X), proper#(s(X)) -> proper#(X))
                                (proper#(s(X)) -> proper#(X), proper#(take(X1, X2)) -> proper#(X1))
                                (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                                (proper#(cons(X1, X2)) -> proper#(X1), proper#(s(X)) -> proper#(X))
                                (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))}
                               SCCS:
                                Scc:
                                 {proper#(cons(X1, X2)) -> proper#(X1),
                                          proper#(s(X)) -> proper#(X),
                                  proper#(take(X1, X2)) -> proper#(X1)}
                                SCC:
                                 Strict:
                                  {proper#(cons(X1, X2)) -> proper#(X1),
                                           proper#(s(X)) -> proper#(X),
                                   proper#(take(X1, X2)) -> proper#(X1)}
                                 Weak:
                                 {             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)),
                                             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)),
                                                  active(head(X)) -> head(active(X)),
                                        active(head(cons(X, XS))) -> mark(X),
                                                   active(2nd(X)) -> 2nd(active(X)),
                                         active(2nd(cons(X, XS))) -> mark(head(XS)),
                                             active(take(X1, X2)) -> take(X1, active(X2)),
                                             active(take(X1, X2)) -> take(active(X1), X2),
                                  active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                            active(take(0(), XS)) -> mark(nil()),
                                              active(sel(X1, X2)) -> sel(X1, active(X2)),
                                              active(sel(X1, X2)) -> sel(active(X1), X2),
                                   active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                    active(sel(0(), cons(X, XS))) -> mark(X),
                                                    head(mark(X)) -> mark(head(X)),
                                                      head(ok(X)) -> ok(head(X)),
                                                     2nd(mark(X)) -> mark(2nd(X)),
                                                       2nd(ok(X)) -> ok(2nd(X)),
                                               take(X1, mark(X2)) -> mark(take(X1, X2)),
                                               take(mark(X1), X2) -> mark(take(X1, X2)),
                                             take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                                sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                                sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                              sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                  proper(from(X)) -> from(proper(X)),
                                                     proper(s(X)) -> s(proper(X)),
                                                  proper(head(X)) -> head(proper(X)),
                                                   proper(2nd(X)) -> 2nd(proper(X)),
                                                    proper(nil()) -> ok(nil()),
                                             proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                                      proper(0()) -> ok(0()),
                                              proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                     top(mark(X)) -> top(proper(X)),
                                                       top(ok(X)) -> top(active(X))}
                                 SPSC:
                                  Simple Projection:
                                   pi(proper#) = 0
                                  Strict:
                                   {proper#(cons(X1, X2)) -> proper#(X1),
                                    proper#(take(X1, X2)) -> proper#(X1)}
                                  EDG:
                                   {(proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))
                                    (proper#(take(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(cons(X1, X2)) -> proper#(X1))
                                    (proper#(cons(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))}
                                   SCCS:
                                    Scc:
                                     {proper#(cons(X1, X2)) -> proper#(X1),
                                      proper#(take(X1, X2)) -> proper#(X1)}
                                    SCC:
                                     Strict:
                                      {proper#(cons(X1, X2)) -> proper#(X1),
                                       proper#(take(X1, X2)) -> proper#(X1)}
                                     Weak:
                                     {             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)),
                                                 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)),
                                                      active(head(X)) -> head(active(X)),
                                            active(head(cons(X, XS))) -> mark(X),
                                                       active(2nd(X)) -> 2nd(active(X)),
                                             active(2nd(cons(X, XS))) -> mark(head(XS)),
                                                 active(take(X1, X2)) -> take(X1, active(X2)),
                                                 active(take(X1, X2)) -> take(active(X1), X2),
                                      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                                active(take(0(), XS)) -> mark(nil()),
                                                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                                                  active(sel(X1, X2)) -> sel(active(X1), X2),
                                       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                        active(sel(0(), cons(X, XS))) -> mark(X),
                                                        head(mark(X)) -> mark(head(X)),
                                                          head(ok(X)) -> ok(head(X)),
                                                         2nd(mark(X)) -> mark(2nd(X)),
                                                           2nd(ok(X)) -> ok(2nd(X)),
                                                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                                                   take(mark(X1), X2) -> mark(take(X1, X2)),
                                                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                      proper(from(X)) -> from(proper(X)),
                                                         proper(s(X)) -> s(proper(X)),
                                                      proper(head(X)) -> head(proper(X)),
                                                       proper(2nd(X)) -> 2nd(proper(X)),
                                                        proper(nil()) -> ok(nil()),
                                                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                                          proper(0()) -> ok(0()),
                                                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                         top(mark(X)) -> top(proper(X)),
                                                           top(ok(X)) -> top(active(X))}
                                     SPSC:
                                      Simple Projection:
                                       pi(proper#) = 0
                                      Strict:
                                       {proper#(take(X1, X2)) -> proper#(X1)}
                                      EDG:
                                       {(proper#(take(X1, X2)) -> proper#(X1), proper#(take(X1, X2)) -> proper#(X1))}
                                       SCCS:
                                        Scc:
                                         {proper#(take(X1, X2)) -> proper#(X1)}
                                        SCC:
                                         Strict:
                                          {proper#(take(X1, X2)) -> proper#(X1)}
                                         Weak:
                                         {             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)),
                                                     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)),
                                                          active(head(X)) -> head(active(X)),
                                                active(head(cons(X, XS))) -> mark(X),
                                                           active(2nd(X)) -> 2nd(active(X)),
                                                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                                                     active(take(X1, X2)) -> take(X1, active(X2)),
                                                     active(take(X1, X2)) -> take(active(X1), X2),
                                          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                                    active(take(0(), XS)) -> mark(nil()),
                                                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                                                      active(sel(X1, X2)) -> sel(active(X1), X2),
                                           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                            active(sel(0(), cons(X, XS))) -> mark(X),
                                                            head(mark(X)) -> mark(head(X)),
                                                              head(ok(X)) -> ok(head(X)),
                                                             2nd(mark(X)) -> mark(2nd(X)),
                                                               2nd(ok(X)) -> ok(2nd(X)),
                                                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                                                       take(mark(X1), X2) -> mark(take(X1, X2)),
                                                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                          proper(from(X)) -> from(proper(X)),
                                                             proper(s(X)) -> s(proper(X)),
                                                          proper(head(X)) -> head(proper(X)),
                                                           proper(2nd(X)) -> 2nd(proper(X)),
                                                            proper(nil()) -> ok(nil()),
                                                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                                              proper(0()) -> ok(0()),
                                                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                             top(mark(X)) -> top(proper(X)),
                                                               top(ok(X)) -> top(active(X))}
                                         SPSC:
                                          Simple Projection:
                                           pi(proper#) = 0
                                          Strict:
                                           {}
                                          Qed
    SCC:
     Strict:
      {  sel#(X1, mark(X2)) -> sel#(X1, X2),
         sel#(mark(X1), X2) -> sel#(X1, X2),
       sel#(ok(X1), ok(X2)) -> sel#(X1, X2)}
     Weak:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(sel#) = 0
      Strict:
       {sel#(X1, mark(X2)) -> sel#(X1, X2),
        sel#(mark(X1), X2) -> sel#(X1, X2)}
      EDG:
       {(sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
        (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
        (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
        (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))}
       SCCS:
        Scc:
         {sel#(X1, mark(X2)) -> sel#(X1, X2),
          sel#(mark(X1), X2) -> sel#(X1, X2)}
        SCC:
         Strict:
          {sel#(X1, mark(X2)) -> sel#(X1, X2),
           sel#(mark(X1), X2) -> sel#(X1, X2)}
         Weak:
         {             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)),
                     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)),
                          active(head(X)) -> head(active(X)),
                active(head(cons(X, XS))) -> mark(X),
                           active(2nd(X)) -> 2nd(active(X)),
                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                     active(take(X1, X2)) -> take(X1, active(X2)),
                     active(take(X1, X2)) -> take(active(X1), X2),
          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                    active(take(0(), XS)) -> mark(nil()),
                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                      active(sel(X1, X2)) -> sel(active(X1), X2),
           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
            active(sel(0(), cons(X, XS))) -> mark(X),
                            head(mark(X)) -> mark(head(X)),
                              head(ok(X)) -> ok(head(X)),
                             2nd(mark(X)) -> mark(2nd(X)),
                               2nd(ok(X)) -> ok(2nd(X)),
                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                       take(mark(X1), X2) -> mark(take(X1, X2)),
                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             proper(s(X)) -> s(proper(X)),
                          proper(head(X)) -> head(proper(X)),
                           proper(2nd(X)) -> 2nd(proper(X)),
                            proper(nil()) -> ok(nil()),
                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(sel#) = 1
          Strict:
           {sel#(mark(X1), X2) -> sel#(X1, X2)}
          EDG:
           {(sel#(mark(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))}
           SCCS:
            Scc:
             {sel#(mark(X1), X2) -> sel#(X1, X2)}
            SCC:
             Strict:
              {sel#(mark(X1), X2) -> sel#(X1, X2)}
             Weak:
             {             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)),
                         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)),
                              active(head(X)) -> head(active(X)),
                    active(head(cons(X, XS))) -> mark(X),
                               active(2nd(X)) -> 2nd(active(X)),
                     active(2nd(cons(X, XS))) -> mark(head(XS)),
                         active(take(X1, X2)) -> take(X1, active(X2)),
                         active(take(X1, X2)) -> take(active(X1), X2),
              active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                        active(take(0(), XS)) -> mark(nil()),
                          active(sel(X1, X2)) -> sel(X1, active(X2)),
                          active(sel(X1, X2)) -> sel(active(X1), X2),
               active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                active(sel(0(), cons(X, XS))) -> mark(X),
                                head(mark(X)) -> mark(head(X)),
                                  head(ok(X)) -> ok(head(X)),
                                 2nd(mark(X)) -> mark(2nd(X)),
                                   2nd(ok(X)) -> ok(2nd(X)),
                           take(X1, mark(X2)) -> mark(take(X1, X2)),
                           take(mark(X1), X2) -> mark(take(X1, X2)),
                         take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                            sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                            sel(mark(X1), X2) -> mark(sel(X1, X2)),
                          sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                              proper(from(X)) -> from(proper(X)),
                                 proper(s(X)) -> s(proper(X)),
                              proper(head(X)) -> head(proper(X)),
                               proper(2nd(X)) -> 2nd(proper(X)),
                                proper(nil()) -> ok(nil()),
                         proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                  proper(0()) -> ok(0()),
                          proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                 top(mark(X)) -> top(proper(X)),
                                   top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(sel#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {  take#(X1, mark(X2)) -> take#(X1, X2),
         take#(mark(X1), X2) -> take#(X1, X2),
       take#(ok(X1), ok(X2)) -> take#(X1, X2)}
     Weak:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(take#) = 0
      Strict:
       {  take#(X1, mark(X2)) -> take#(X1, X2),
        take#(ok(X1), ok(X2)) -> take#(X1, X2)}
      EDG:
       {(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#(X1, mark(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2))
        (take#(X1, mark(X2)) -> take#(X1, X2), take#(ok(X1), ok(X2)) -> take#(X1, X2))}
       SCCS:
        Scc:
         {  take#(X1, mark(X2)) -> take#(X1, X2),
          take#(ok(X1), ok(X2)) -> take#(X1, X2)}
        SCC:
         Strict:
          {  take#(X1, mark(X2)) -> take#(X1, X2),
           take#(ok(X1), ok(X2)) -> take#(X1, X2)}
         Weak:
         {             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)),
                     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)),
                          active(head(X)) -> head(active(X)),
                active(head(cons(X, XS))) -> mark(X),
                           active(2nd(X)) -> 2nd(active(X)),
                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                     active(take(X1, X2)) -> take(X1, active(X2)),
                     active(take(X1, X2)) -> take(active(X1), X2),
          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                    active(take(0(), XS)) -> mark(nil()),
                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                      active(sel(X1, X2)) -> sel(active(X1), X2),
           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
            active(sel(0(), cons(X, XS))) -> mark(X),
                            head(mark(X)) -> mark(head(X)),
                              head(ok(X)) -> ok(head(X)),
                             2nd(mark(X)) -> mark(2nd(X)),
                               2nd(ok(X)) -> ok(2nd(X)),
                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                       take(mark(X1), X2) -> mark(take(X1, X2)),
                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             proper(s(X)) -> s(proper(X)),
                          proper(head(X)) -> head(proper(X)),
                           proper(2nd(X)) -> 2nd(proper(X)),
                            proper(nil()) -> ok(nil()),
                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(take#) = 0
          Strict:
           {take#(X1, mark(X2)) -> take#(X1, X2)}
          EDG:
           {(take#(X1, mark(X2)) -> take#(X1, X2), take#(X1, mark(X2)) -> take#(X1, X2))}
           SCCS:
            Scc:
             {take#(X1, mark(X2)) -> take#(X1, X2)}
            SCC:
             Strict:
              {take#(X1, mark(X2)) -> take#(X1, X2)}
             Weak:
             {             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)),
                         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)),
                              active(head(X)) -> head(active(X)),
                    active(head(cons(X, XS))) -> mark(X),
                               active(2nd(X)) -> 2nd(active(X)),
                     active(2nd(cons(X, XS))) -> mark(head(XS)),
                         active(take(X1, X2)) -> take(X1, active(X2)),
                         active(take(X1, X2)) -> take(active(X1), X2),
              active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                        active(take(0(), XS)) -> mark(nil()),
                          active(sel(X1, X2)) -> sel(X1, active(X2)),
                          active(sel(X1, X2)) -> sel(active(X1), X2),
               active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                active(sel(0(), cons(X, XS))) -> mark(X),
                                head(mark(X)) -> mark(head(X)),
                                  head(ok(X)) -> ok(head(X)),
                                 2nd(mark(X)) -> mark(2nd(X)),
                                   2nd(ok(X)) -> ok(2nd(X)),
                           take(X1, mark(X2)) -> mark(take(X1, X2)),
                           take(mark(X1), X2) -> mark(take(X1, X2)),
                         take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                            sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                            sel(mark(X1), X2) -> mark(sel(X1, X2)),
                          sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                              proper(from(X)) -> from(proper(X)),
                                 proper(s(X)) -> s(proper(X)),
                              proper(head(X)) -> head(proper(X)),
                               proper(2nd(X)) -> 2nd(proper(X)),
                                proper(nil()) -> ok(nil()),
                         proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                  proper(0()) -> ok(0()),
                          proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                 top(mark(X)) -> top(proper(X)),
                                   top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(take#) = 1
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {2nd#(mark(X)) -> 2nd#(X),
         2nd#(ok(X)) -> 2nd#(X)}
     Weak:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         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:
         {             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)),
                     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)),
                          active(head(X)) -> head(active(X)),
                active(head(cons(X, XS))) -> mark(X),
                           active(2nd(X)) -> 2nd(active(X)),
                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                     active(take(X1, X2)) -> take(X1, active(X2)),
                     active(take(X1, X2)) -> take(active(X1), X2),
          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                    active(take(0(), XS)) -> mark(nil()),
                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                      active(sel(X1, X2)) -> sel(active(X1), X2),
           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
            active(sel(0(), cons(X, XS))) -> mark(X),
                            head(mark(X)) -> mark(head(X)),
                              head(ok(X)) -> ok(head(X)),
                             2nd(mark(X)) -> mark(2nd(X)),
                               2nd(ok(X)) -> ok(2nd(X)),
                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                       take(mark(X1), X2) -> mark(take(X1, X2)),
                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             proper(s(X)) -> s(proper(X)),
                          proper(head(X)) -> head(proper(X)),
                           proper(2nd(X)) -> 2nd(proper(X)),
                            proper(nil()) -> ok(nil()),
                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(2nd#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {head#(mark(X)) -> head#(X),
         head#(ok(X)) -> head#(X)}
     Weak:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(head#) = 0
      Strict:
       {head#(ok(X)) -> head#(X)}
      EDG:
       {(head#(ok(X)) -> head#(X), head#(ok(X)) -> head#(X))}
       SCCS:
        Scc:
         {head#(ok(X)) -> head#(X)}
        SCC:
         Strict:
          {head#(ok(X)) -> head#(X)}
         Weak:
         {             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)),
                     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)),
                          active(head(X)) -> head(active(X)),
                active(head(cons(X, XS))) -> mark(X),
                           active(2nd(X)) -> 2nd(active(X)),
                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                     active(take(X1, X2)) -> take(X1, active(X2)),
                     active(take(X1, X2)) -> take(active(X1), X2),
          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                    active(take(0(), XS)) -> mark(nil()),
                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                      active(sel(X1, X2)) -> sel(active(X1), X2),
           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
            active(sel(0(), cons(X, XS))) -> mark(X),
                            head(mark(X)) -> mark(head(X)),
                              head(ok(X)) -> ok(head(X)),
                             2nd(mark(X)) -> mark(2nd(X)),
                               2nd(ok(X)) -> ok(2nd(X)),
                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                       take(mark(X1), X2) -> mark(take(X1, X2)),
                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             proper(s(X)) -> s(proper(X)),
                          proper(head(X)) -> head(proper(X)),
                           proper(2nd(X)) -> 2nd(proper(X)),
                            proper(nil()) -> ok(nil()),
                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(head#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {active#(cons(X1, X2)) -> active#(X1),
            active#(from(X)) -> active#(X),
               active#(s(X)) -> active#(X),
            active#(head(X)) -> active#(X),
             active#(2nd(X)) -> active#(X),
       active#(take(X1, X2)) -> active#(X1),
       active#(take(X1, X2)) -> active#(X2),
        active#(sel(X1, X2)) -> active#(X1),
        active#(sel(X1, X2)) -> active#(X2)}
     Weak:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {active#(cons(X1, X2)) -> active#(X1),
             active#(from(X)) -> active#(X),
                active#(s(X)) -> active#(X),
             active#(head(X)) -> active#(X),
              active#(2nd(X)) -> active#(X),
        active#(take(X1, X2)) -> active#(X2),
         active#(sel(X1, X2)) -> active#(X1),
         active#(sel(X1, X2)) -> active#(X2)}
      EDG:
       {(active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X2))
        (active#(sel(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
        (active#(sel(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> active#(X2))
        (active#(sel(X1, X2)) -> active#(X2), active#(2nd(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X2), active#(head(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X2), active#(from(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
        (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X2))
        (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
        (active#(sel(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2))
        (active#(sel(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
        (active#(sel(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
        (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
        (active#(s(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
        (active#(s(X)) -> active#(X), active#(2nd(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(head(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(from(X)) -> active#(X))
        (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(2nd(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
        (active#(2nd(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
        (active#(2nd(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
        (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
        (active#(2nd(X)) -> active#(X), active#(head(X)) -> active#(X))
        (active#(2nd(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(2nd(X)) -> active#(X), active#(from(X)) -> active#(X))
        (active#(2nd(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(head(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(head(X)) -> active#(X), active#(from(X)) -> active#(X))
        (active#(head(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(head(X)) -> active#(X), active#(head(X)) -> active#(X))
        (active#(head(X)) -> active#(X), active#(2nd(X)) -> active#(X))
        (active#(head(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
        (active#(head(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
        (active#(head(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
        (active#(from(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
        (active#(from(X)) -> active#(X), active#(from(X)) -> active#(X))
        (active#(from(X)) -> active#(X), active#(s(X)) -> active#(X))
        (active#(from(X)) -> active#(X), active#(head(X)) -> active#(X))
        (active#(from(X)) -> active#(X), active#(2nd(X)) -> active#(X))
        (active#(from(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
        (active#(from(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
        (active#(from(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X2))
        (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
        (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
        (active#(cons(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2))
        (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
        (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X2))
        (active#(take(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
        (active#(take(X1, X2)) -> active#(X2), active#(from(X)) -> active#(X))
        (active#(take(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
        (active#(take(X1, X2)) -> active#(X2), active#(head(X)) -> active#(X))
        (active#(take(X1, X2)) -> active#(X2), active#(2nd(X)) -> active#(X))
        (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> active#(X2))
        (active#(take(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))
        (active#(take(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X2))}
       SCCS:
        Scc:
         {active#(cons(X1, X2)) -> active#(X1),
               active#(from(X)) -> active#(X),
                  active#(s(X)) -> active#(X),
               active#(head(X)) -> active#(X),
                active#(2nd(X)) -> active#(X),
          active#(take(X1, X2)) -> active#(X2),
           active#(sel(X1, X2)) -> active#(X1),
           active#(sel(X1, X2)) -> active#(X2)}
        SCC:
         Strict:
          {active#(cons(X1, X2)) -> active#(X1),
                active#(from(X)) -> active#(X),
                   active#(s(X)) -> active#(X),
                active#(head(X)) -> active#(X),
                 active#(2nd(X)) -> active#(X),
           active#(take(X1, X2)) -> active#(X2),
            active#(sel(X1, X2)) -> active#(X1),
            active#(sel(X1, X2)) -> active#(X2)}
         Weak:
         {             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)),
                     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)),
                          active(head(X)) -> head(active(X)),
                active(head(cons(X, XS))) -> mark(X),
                           active(2nd(X)) -> 2nd(active(X)),
                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                     active(take(X1, X2)) -> take(X1, active(X2)),
                     active(take(X1, X2)) -> take(active(X1), X2),
          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                    active(take(0(), XS)) -> mark(nil()),
                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                      active(sel(X1, X2)) -> sel(active(X1), X2),
           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
            active(sel(0(), cons(X, XS))) -> mark(X),
                            head(mark(X)) -> mark(head(X)),
                              head(ok(X)) -> ok(head(X)),
                             2nd(mark(X)) -> mark(2nd(X)),
                               2nd(ok(X)) -> ok(2nd(X)),
                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                       take(mark(X1), X2) -> mark(take(X1, X2)),
                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             proper(s(X)) -> s(proper(X)),
                          proper(head(X)) -> head(proper(X)),
                           proper(2nd(X)) -> 2nd(proper(X)),
                            proper(nil()) -> ok(nil()),
                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(active#) = 0
          Strict:
           {active#(cons(X1, X2)) -> active#(X1),
                 active#(from(X)) -> active#(X),
                    active#(s(X)) -> active#(X),
                 active#(head(X)) -> active#(X),
                  active#(2nd(X)) -> active#(X),
            active#(take(X1, X2)) -> active#(X2),
             active#(sel(X1, X2)) -> active#(X1)}
          EDG:
           {(active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
            (active#(cons(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2))
            (active#(cons(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
            (active#(cons(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
            (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
            (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
            (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
            (active#(from(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
            (active#(from(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
            (active#(from(X)) -> active#(X), active#(2nd(X)) -> active#(X))
            (active#(from(X)) -> active#(X), active#(head(X)) -> active#(X))
            (active#(from(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(from(X)) -> active#(X), active#(from(X)) -> active#(X))
            (active#(from(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(head(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
            (active#(head(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
            (active#(head(X)) -> active#(X), active#(2nd(X)) -> active#(X))
            (active#(head(X)) -> active#(X), active#(head(X)) -> active#(X))
            (active#(head(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(head(X)) -> active#(X), active#(from(X)) -> active#(X))
            (active#(head(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(2nd(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(2nd(X)) -> active#(X), active#(from(X)) -> active#(X))
            (active#(2nd(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(2nd(X)) -> active#(X), active#(head(X)) -> active#(X))
            (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
            (active#(2nd(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
            (active#(2nd(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
            (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
            (active#(s(X)) -> active#(X), active#(from(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(head(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(2nd(X)) -> active#(X))
            (active#(s(X)) -> active#(X), active#(take(X1, X2)) -> active#(X2))
            (active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
            (active#(sel(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
            (active#(sel(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
            (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
            (active#(sel(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
            (active#(sel(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
            (active#(sel(X1, X2)) -> active#(X1), active#(take(X1, X2)) -> active#(X2))
            (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
            (active#(take(X1, X2)) -> active#(X2), active#(cons(X1, X2)) -> active#(X1))
            (active#(take(X1, X2)) -> active#(X2), active#(from(X)) -> active#(X))
            (active#(take(X1, X2)) -> active#(X2), active#(s(X)) -> active#(X))
            (active#(take(X1, X2)) -> active#(X2), active#(head(X)) -> active#(X))
            (active#(take(X1, X2)) -> active#(X2), active#(2nd(X)) -> active#(X))
            (active#(take(X1, X2)) -> active#(X2), active#(take(X1, X2)) -> active#(X2))
            (active#(take(X1, X2)) -> active#(X2), active#(sel(X1, X2)) -> active#(X1))}
           SCCS:
            Scc:
             {active#(cons(X1, X2)) -> active#(X1),
                   active#(from(X)) -> active#(X),
                      active#(s(X)) -> active#(X),
                   active#(head(X)) -> active#(X),
                    active#(2nd(X)) -> active#(X),
              active#(take(X1, X2)) -> active#(X2),
               active#(sel(X1, X2)) -> active#(X1)}
            SCC:
             Strict:
              {active#(cons(X1, X2)) -> active#(X1),
                    active#(from(X)) -> active#(X),
                       active#(s(X)) -> active#(X),
                    active#(head(X)) -> active#(X),
                     active#(2nd(X)) -> active#(X),
               active#(take(X1, X2)) -> active#(X2),
                active#(sel(X1, X2)) -> active#(X1)}
             Weak:
             {             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)),
                         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)),
                              active(head(X)) -> head(active(X)),
                    active(head(cons(X, XS))) -> mark(X),
                               active(2nd(X)) -> 2nd(active(X)),
                     active(2nd(cons(X, XS))) -> mark(head(XS)),
                         active(take(X1, X2)) -> take(X1, active(X2)),
                         active(take(X1, X2)) -> take(active(X1), X2),
              active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                        active(take(0(), XS)) -> mark(nil()),
                          active(sel(X1, X2)) -> sel(X1, active(X2)),
                          active(sel(X1, X2)) -> sel(active(X1), X2),
               active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                active(sel(0(), cons(X, XS))) -> mark(X),
                                head(mark(X)) -> mark(head(X)),
                                  head(ok(X)) -> ok(head(X)),
                                 2nd(mark(X)) -> mark(2nd(X)),
                                   2nd(ok(X)) -> ok(2nd(X)),
                           take(X1, mark(X2)) -> mark(take(X1, X2)),
                           take(mark(X1), X2) -> mark(take(X1, X2)),
                         take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                            sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                            sel(mark(X1), X2) -> mark(sel(X1, X2)),
                          sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                              proper(from(X)) -> from(proper(X)),
                                 proper(s(X)) -> s(proper(X)),
                              proper(head(X)) -> head(proper(X)),
                               proper(2nd(X)) -> 2nd(proper(X)),
                                proper(nil()) -> ok(nil()),
                         proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                  proper(0()) -> ok(0()),
                          proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                 top(mark(X)) -> top(proper(X)),
                                   top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(active#) = 0
              Strict:
               {active#(cons(X1, X2)) -> active#(X1),
                     active#(from(X)) -> active#(X),
                        active#(s(X)) -> active#(X),
                     active#(head(X)) -> active#(X),
                      active#(2nd(X)) -> active#(X),
                 active#(sel(X1, X2)) -> active#(X1)}
              EDG:
               {(active#(s(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
                (active#(s(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(head(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(from(X)) -> active#(X))
                (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                (active#(2nd(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
                (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                (active#(2nd(X)) -> active#(X), active#(head(X)) -> active#(X))
                (active#(2nd(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(2nd(X)) -> active#(X), active#(from(X)) -> active#(X))
                (active#(2nd(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                (active#(sel(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                (active#(sel(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
                (active#(sel(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
                (active#(sel(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                (active#(sel(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
                (active#(sel(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
                (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
                (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
                (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                (active#(cons(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
                (active#(cons(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
                (active#(cons(X1, X2)) -> active#(X1), active#(sel(X1, X2)) -> active#(X1))
                (active#(head(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                (active#(head(X)) -> active#(X), active#(from(X)) -> active#(X))
                (active#(head(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(head(X)) -> active#(X), active#(head(X)) -> active#(X))
                (active#(head(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                (active#(head(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))
                (active#(from(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                (active#(from(X)) -> active#(X), active#(from(X)) -> active#(X))
                (active#(from(X)) -> active#(X), active#(s(X)) -> active#(X))
                (active#(from(X)) -> active#(X), active#(head(X)) -> active#(X))
                (active#(from(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                (active#(from(X)) -> active#(X), active#(sel(X1, X2)) -> active#(X1))}
               SCCS:
                Scc:
                 {active#(cons(X1, X2)) -> active#(X1),
                       active#(from(X)) -> active#(X),
                          active#(s(X)) -> active#(X),
                       active#(head(X)) -> active#(X),
                        active#(2nd(X)) -> active#(X),
                   active#(sel(X1, X2)) -> active#(X1)}
                SCC:
                 Strict:
                  {active#(cons(X1, X2)) -> active#(X1),
                        active#(from(X)) -> active#(X),
                           active#(s(X)) -> active#(X),
                        active#(head(X)) -> active#(X),
                         active#(2nd(X)) -> active#(X),
                    active#(sel(X1, X2)) -> active#(X1)}
                 Weak:
                 {             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)),
                             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)),
                                  active(head(X)) -> head(active(X)),
                        active(head(cons(X, XS))) -> mark(X),
                                   active(2nd(X)) -> 2nd(active(X)),
                         active(2nd(cons(X, XS))) -> mark(head(XS)),
                             active(take(X1, X2)) -> take(X1, active(X2)),
                             active(take(X1, X2)) -> take(active(X1), X2),
                  active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                            active(take(0(), XS)) -> mark(nil()),
                              active(sel(X1, X2)) -> sel(X1, active(X2)),
                              active(sel(X1, X2)) -> sel(active(X1), X2),
                   active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                    active(sel(0(), cons(X, XS))) -> mark(X),
                                    head(mark(X)) -> mark(head(X)),
                                      head(ok(X)) -> ok(head(X)),
                                     2nd(mark(X)) -> mark(2nd(X)),
                                       2nd(ok(X)) -> ok(2nd(X)),
                               take(X1, mark(X2)) -> mark(take(X1, X2)),
                               take(mark(X1), X2) -> mark(take(X1, X2)),
                             take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                sel(mark(X1), X2) -> mark(sel(X1, X2)),
                              sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                  proper(from(X)) -> from(proper(X)),
                                     proper(s(X)) -> s(proper(X)),
                                  proper(head(X)) -> head(proper(X)),
                                   proper(2nd(X)) -> 2nd(proper(X)),
                                    proper(nil()) -> ok(nil()),
                             proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                      proper(0()) -> ok(0()),
                              proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                     top(mark(X)) -> top(proper(X)),
                                       top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(active#) = 0
                  Strict:
                   {active#(cons(X1, X2)) -> active#(X1),
                         active#(from(X)) -> active#(X),
                            active#(s(X)) -> active#(X),
                         active#(head(X)) -> active#(X),
                          active#(2nd(X)) -> active#(X)}
                  EDG:
                   {(active#(s(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                    (active#(s(X)) -> active#(X), active#(head(X)) -> active#(X))
                    (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                    (active#(s(X)) -> active#(X), active#(from(X)) -> active#(X))
                    (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                    (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                    (active#(2nd(X)) -> active#(X), active#(head(X)) -> active#(X))
                    (active#(2nd(X)) -> active#(X), active#(s(X)) -> active#(X))
                    (active#(2nd(X)) -> active#(X), active#(from(X)) -> active#(X))
                    (active#(2nd(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                    (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
                    (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
                    (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                    (active#(cons(X1, X2)) -> active#(X1), active#(head(X)) -> active#(X))
                    (active#(cons(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
                    (active#(head(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                    (active#(head(X)) -> active#(X), active#(from(X)) -> active#(X))
                    (active#(head(X)) -> active#(X), active#(s(X)) -> active#(X))
                    (active#(head(X)) -> active#(X), active#(head(X)) -> active#(X))
                    (active#(head(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                    (active#(from(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                    (active#(from(X)) -> active#(X), active#(from(X)) -> active#(X))
                    (active#(from(X)) -> active#(X), active#(s(X)) -> active#(X))
                    (active#(from(X)) -> active#(X), active#(head(X)) -> active#(X))
                    (active#(from(X)) -> active#(X), active#(2nd(X)) -> active#(X))}
                   SCCS:
                    Scc:
                     {active#(cons(X1, X2)) -> active#(X1),
                           active#(from(X)) -> active#(X),
                              active#(s(X)) -> active#(X),
                           active#(head(X)) -> active#(X),
                            active#(2nd(X)) -> active#(X)}
                    SCC:
                     Strict:
                      {active#(cons(X1, X2)) -> active#(X1),
                            active#(from(X)) -> active#(X),
                               active#(s(X)) -> active#(X),
                            active#(head(X)) -> active#(X),
                             active#(2nd(X)) -> active#(X)}
                     Weak:
                     {             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)),
                                 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)),
                                      active(head(X)) -> head(active(X)),
                            active(head(cons(X, XS))) -> mark(X),
                                       active(2nd(X)) -> 2nd(active(X)),
                             active(2nd(cons(X, XS))) -> mark(head(XS)),
                                 active(take(X1, X2)) -> take(X1, active(X2)),
                                 active(take(X1, X2)) -> take(active(X1), X2),
                      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                active(take(0(), XS)) -> mark(nil()),
                                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                                  active(sel(X1, X2)) -> sel(active(X1), X2),
                       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                        active(sel(0(), cons(X, XS))) -> mark(X),
                                        head(mark(X)) -> mark(head(X)),
                                          head(ok(X)) -> ok(head(X)),
                                         2nd(mark(X)) -> mark(2nd(X)),
                                           2nd(ok(X)) -> ok(2nd(X)),
                                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                                   take(mark(X1), X2) -> mark(take(X1, X2)),
                                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                      proper(from(X)) -> from(proper(X)),
                                         proper(s(X)) -> s(proper(X)),
                                      proper(head(X)) -> head(proper(X)),
                                       proper(2nd(X)) -> 2nd(proper(X)),
                                        proper(nil()) -> ok(nil()),
                                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                          proper(0()) -> ok(0()),
                                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                         top(mark(X)) -> top(proper(X)),
                                           top(ok(X)) -> top(active(X))}
                     SPSC:
                      Simple Projection:
                       pi(active#) = 0
                      Strict:
                       {active#(cons(X1, X2)) -> active#(X1),
                             active#(from(X)) -> active#(X),
                                active#(s(X)) -> active#(X),
                              active#(2nd(X)) -> active#(X)}
                      EDG:
                       {(active#(s(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                        (active#(s(X)) -> active#(X), active#(s(X)) -> active#(X))
                        (active#(s(X)) -> active#(X), active#(from(X)) -> active#(X))
                        (active#(s(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                        (active#(cons(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))
                        (active#(cons(X1, X2)) -> active#(X1), active#(s(X)) -> active#(X))
                        (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
                        (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
                        (active#(2nd(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                        (active#(2nd(X)) -> active#(X), active#(from(X)) -> active#(X))
                        (active#(2nd(X)) -> active#(X), active#(s(X)) -> active#(X))
                        (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                        (active#(from(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                        (active#(from(X)) -> active#(X), active#(from(X)) -> active#(X))
                        (active#(from(X)) -> active#(X), active#(s(X)) -> active#(X))
                        (active#(from(X)) -> active#(X), active#(2nd(X)) -> active#(X))}
                       SCCS:
                        Scc:
                         {active#(cons(X1, X2)) -> active#(X1),
                               active#(from(X)) -> active#(X),
                                  active#(s(X)) -> active#(X),
                                active#(2nd(X)) -> active#(X)}
                        SCC:
                         Strict:
                          {active#(cons(X1, X2)) -> active#(X1),
                                active#(from(X)) -> active#(X),
                                   active#(s(X)) -> active#(X),
                                 active#(2nd(X)) -> active#(X)}
                         Weak:
                         {             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)),
                                     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)),
                                          active(head(X)) -> head(active(X)),
                                active(head(cons(X, XS))) -> mark(X),
                                           active(2nd(X)) -> 2nd(active(X)),
                                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                                     active(take(X1, X2)) -> take(X1, active(X2)),
                                     active(take(X1, X2)) -> take(active(X1), X2),
                          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                    active(take(0(), XS)) -> mark(nil()),
                                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                                      active(sel(X1, X2)) -> sel(active(X1), X2),
                           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                            active(sel(0(), cons(X, XS))) -> mark(X),
                                            head(mark(X)) -> mark(head(X)),
                                              head(ok(X)) -> ok(head(X)),
                                             2nd(mark(X)) -> mark(2nd(X)),
                                               2nd(ok(X)) -> ok(2nd(X)),
                                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                                       take(mark(X1), X2) -> mark(take(X1, X2)),
                                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                          proper(from(X)) -> from(proper(X)),
                                             proper(s(X)) -> s(proper(X)),
                                          proper(head(X)) -> head(proper(X)),
                                           proper(2nd(X)) -> 2nd(proper(X)),
                                            proper(nil()) -> ok(nil()),
                                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                              proper(0()) -> ok(0()),
                                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                             top(mark(X)) -> top(proper(X)),
                                               top(ok(X)) -> top(active(X))}
                         SPSC:
                          Simple Projection:
                           pi(active#) = 0
                          Strict:
                           {active#(cons(X1, X2)) -> active#(X1),
                                 active#(from(X)) -> active#(X),
                                  active#(2nd(X)) -> active#(X)}
                          EDG:
                           {(active#(from(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                            (active#(from(X)) -> active#(X), active#(from(X)) -> active#(X))
                            (active#(from(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                            (active#(2nd(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                            (active#(2nd(X)) -> active#(X), active#(from(X)) -> active#(X))
                            (active#(2nd(X)) -> active#(X), active#(2nd(X)) -> active#(X))
                            (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
                            (active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
                            (active#(cons(X1, X2)) -> active#(X1), active#(2nd(X)) -> active#(X))}
                           SCCS:
                            Scc:
                             {active#(cons(X1, X2)) -> active#(X1),
                                   active#(from(X)) -> active#(X),
                                    active#(2nd(X)) -> active#(X)}
                            SCC:
                             Strict:
                              {active#(cons(X1, X2)) -> active#(X1),
                                    active#(from(X)) -> active#(X),
                                     active#(2nd(X)) -> active#(X)}
                             Weak:
                             {             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)),
                                         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)),
                                              active(head(X)) -> head(active(X)),
                                    active(head(cons(X, XS))) -> mark(X),
                                               active(2nd(X)) -> 2nd(active(X)),
                                     active(2nd(cons(X, XS))) -> mark(head(XS)),
                                         active(take(X1, X2)) -> take(X1, active(X2)),
                                         active(take(X1, X2)) -> take(active(X1), X2),
                              active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                        active(take(0(), XS)) -> mark(nil()),
                                          active(sel(X1, X2)) -> sel(X1, active(X2)),
                                          active(sel(X1, X2)) -> sel(active(X1), X2),
                               active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                active(sel(0(), cons(X, XS))) -> mark(X),
                                                head(mark(X)) -> mark(head(X)),
                                                  head(ok(X)) -> ok(head(X)),
                                                 2nd(mark(X)) -> mark(2nd(X)),
                                                   2nd(ok(X)) -> ok(2nd(X)),
                                           take(X1, mark(X2)) -> mark(take(X1, X2)),
                                           take(mark(X1), X2) -> mark(take(X1, X2)),
                                         take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                            sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                            sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                          sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                         proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                              proper(from(X)) -> from(proper(X)),
                                                 proper(s(X)) -> s(proper(X)),
                                              proper(head(X)) -> head(proper(X)),
                                               proper(2nd(X)) -> 2nd(proper(X)),
                                                proper(nil()) -> ok(nil()),
                                         proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                                  proper(0()) -> ok(0()),
                                          proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                 top(mark(X)) -> top(proper(X)),
                                                   top(ok(X)) -> top(active(X))}
                             SPSC:
                              Simple Projection:
                               pi(active#) = 0
                              Strict:
                               {active#(cons(X1, X2)) -> active#(X1),
                                     active#(from(X)) -> active#(X)}
                              EDG:
                               {(active#(cons(X1, X2)) -> active#(X1), active#(from(X)) -> active#(X))
                                (active#(cons(X1, X2)) -> active#(X1), active#(cons(X1, X2)) -> active#(X1))
                                (active#(from(X)) -> active#(X), active#(cons(X1, X2)) -> active#(X1))
                                (active#(from(X)) -> active#(X), active#(from(X)) -> active#(X))}
                               SCCS:
                                Scc:
                                 {active#(cons(X1, X2)) -> active#(X1),
                                       active#(from(X)) -> active#(X)}
                                SCC:
                                 Strict:
                                  {active#(cons(X1, X2)) -> active#(X1),
                                        active#(from(X)) -> active#(X)}
                                 Weak:
                                 {             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)),
                                             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)),
                                                  active(head(X)) -> head(active(X)),
                                        active(head(cons(X, XS))) -> mark(X),
                                                   active(2nd(X)) -> 2nd(active(X)),
                                         active(2nd(cons(X, XS))) -> mark(head(XS)),
                                             active(take(X1, X2)) -> take(X1, active(X2)),
                                             active(take(X1, X2)) -> take(active(X1), X2),
                                  active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                            active(take(0(), XS)) -> mark(nil()),
                                              active(sel(X1, X2)) -> sel(X1, active(X2)),
                                              active(sel(X1, X2)) -> sel(active(X1), X2),
                                   active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                    active(sel(0(), cons(X, XS))) -> mark(X),
                                                    head(mark(X)) -> mark(head(X)),
                                                      head(ok(X)) -> ok(head(X)),
                                                     2nd(mark(X)) -> mark(2nd(X)),
                                                       2nd(ok(X)) -> ok(2nd(X)),
                                               take(X1, mark(X2)) -> mark(take(X1, X2)),
                                               take(mark(X1), X2) -> mark(take(X1, X2)),
                                             take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                                sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                                sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                              sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                             proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                  proper(from(X)) -> from(proper(X)),
                                                     proper(s(X)) -> s(proper(X)),
                                                  proper(head(X)) -> head(proper(X)),
                                                   proper(2nd(X)) -> 2nd(proper(X)),
                                                    proper(nil()) -> ok(nil()),
                                             proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                                      proper(0()) -> ok(0()),
                                              proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                     top(mark(X)) -> top(proper(X)),
                                                       top(ok(X)) -> top(active(X))}
                                 SPSC:
                                  Simple Projection:
                                   pi(active#) = 0
                                  Strict:
                                   {active#(from(X)) -> active#(X)}
                                  EDG:
                                   {(active#(from(X)) -> active#(X), active#(from(X)) -> active#(X))}
                                   SCCS:
                                    Scc:
                                     {active#(from(X)) -> active#(X)}
                                    SCC:
                                     Strict:
                                      {active#(from(X)) -> active#(X)}
                                     Weak:
                                     {             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)),
                                                 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)),
                                                      active(head(X)) -> head(active(X)),
                                            active(head(cons(X, XS))) -> mark(X),
                                                       active(2nd(X)) -> 2nd(active(X)),
                                             active(2nd(cons(X, XS))) -> mark(head(XS)),
                                                 active(take(X1, X2)) -> take(X1, active(X2)),
                                                 active(take(X1, X2)) -> take(active(X1), X2),
                                      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                                                active(take(0(), XS)) -> mark(nil()),
                                                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                                                  active(sel(X1, X2)) -> sel(active(X1), X2),
                                       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                                        active(sel(0(), cons(X, XS))) -> mark(X),
                                                        head(mark(X)) -> mark(head(X)),
                                                          head(ok(X)) -> ok(head(X)),
                                                         2nd(mark(X)) -> mark(2nd(X)),
                                                           2nd(ok(X)) -> ok(2nd(X)),
                                                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                                                   take(mark(X1), X2) -> mark(take(X1, X2)),
                                                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                                                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                                                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                                                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                                                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                                                      proper(from(X)) -> from(proper(X)),
                                                         proper(s(X)) -> s(proper(X)),
                                                      proper(head(X)) -> head(proper(X)),
                                                       proper(2nd(X)) -> 2nd(proper(X)),
                                                        proper(nil()) -> ok(nil()),
                                                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                                                          proper(0()) -> ok(0()),
                                                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                                                         top(mark(X)) -> top(proper(X)),
                                                           top(ok(X)) -> top(active(X))}
                                     SPSC:
                                      Simple Projection:
                                       pi(active#) = 0
                                      Strict:
                                       {}
                                      Qed
    SCC:
     Strict:
      {s#(mark(X)) -> s#(X),
         s#(ok(X)) -> s#(X)}
     Weak:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         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:
         {             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)),
                     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)),
                          active(head(X)) -> head(active(X)),
                active(head(cons(X, XS))) -> mark(X),
                           active(2nd(X)) -> 2nd(active(X)),
                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                     active(take(X1, X2)) -> take(X1, active(X2)),
                     active(take(X1, X2)) -> take(active(X1), X2),
          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                    active(take(0(), XS)) -> mark(nil()),
                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                      active(sel(X1, X2)) -> sel(active(X1), X2),
           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
            active(sel(0(), cons(X, XS))) -> mark(X),
                            head(mark(X)) -> mark(head(X)),
                              head(ok(X)) -> ok(head(X)),
                             2nd(mark(X)) -> mark(2nd(X)),
                               2nd(ok(X)) -> ok(2nd(X)),
                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                       take(mark(X1), X2) -> mark(take(X1, X2)),
                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             proper(s(X)) -> s(proper(X)),
                          proper(head(X)) -> head(proper(X)),
                           proper(2nd(X)) -> 2nd(proper(X)),
                            proper(nil()) -> ok(nil()),
                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                             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:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(from#) = 0
      Strict:
       {from#(ok(X)) -> from#(X)}
      EDG:
       {(from#(ok(X)) -> from#(X), from#(ok(X)) -> from#(X))}
       SCCS:
        Scc:
         {from#(ok(X)) -> from#(X)}
        SCC:
         Strict:
          {from#(ok(X)) -> from#(X)}
         Weak:
         {             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)),
                     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)),
                          active(head(X)) -> head(active(X)),
                active(head(cons(X, XS))) -> mark(X),
                           active(2nd(X)) -> 2nd(active(X)),
                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                     active(take(X1, X2)) -> take(X1, active(X2)),
                     active(take(X1, X2)) -> take(active(X1), X2),
          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                    active(take(0(), XS)) -> mark(nil()),
                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                      active(sel(X1, X2)) -> sel(active(X1), X2),
           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
            active(sel(0(), cons(X, XS))) -> mark(X),
                            head(mark(X)) -> mark(head(X)),
                              head(ok(X)) -> ok(head(X)),
                             2nd(mark(X)) -> mark(2nd(X)),
                               2nd(ok(X)) -> ok(2nd(X)),
                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                       take(mark(X1), X2) -> mark(take(X1, X2)),
                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             proper(s(X)) -> s(proper(X)),
                          proper(head(X)) -> head(proper(X)),
                           proper(2nd(X)) -> 2nd(proper(X)),
                            proper(nil()) -> ok(nil()),
                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                             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:
     {             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)),
                 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)),
                      active(head(X)) -> head(active(X)),
            active(head(cons(X, XS))) -> mark(X),
                       active(2nd(X)) -> 2nd(active(X)),
             active(2nd(cons(X, XS))) -> mark(head(XS)),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
      active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                active(take(0(), XS)) -> mark(nil()),
                  active(sel(X1, X2)) -> sel(X1, active(X2)),
                  active(sel(X1, X2)) -> sel(active(X1), X2),
       active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
        active(sel(0(), cons(X, XS))) -> mark(X),
                        head(mark(X)) -> mark(head(X)),
                          head(ok(X)) -> ok(head(X)),
                         2nd(mark(X)) -> mark(2nd(X)),
                           2nd(ok(X)) -> ok(2nd(X)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                    sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                    sel(mark(X1), X2) -> mark(sel(X1, X2)),
                  sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                      proper(from(X)) -> from(proper(X)),
                         proper(s(X)) -> s(proper(X)),
                      proper(head(X)) -> head(proper(X)),
                       proper(2nd(X)) -> 2nd(proper(X)),
                        proper(nil()) -> ok(nil()),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                  proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                         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:
         {             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)),
                     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)),
                          active(head(X)) -> head(active(X)),
                active(head(cons(X, XS))) -> mark(X),
                           active(2nd(X)) -> 2nd(active(X)),
                 active(2nd(cons(X, XS))) -> mark(head(XS)),
                     active(take(X1, X2)) -> take(X1, active(X2)),
                     active(take(X1, X2)) -> take(active(X1), X2),
          active(take(s(N), cons(X, XS))) -> mark(cons(X, take(N, XS))),
                    active(take(0(), XS)) -> mark(nil()),
                      active(sel(X1, X2)) -> sel(X1, active(X2)),
                      active(sel(X1, X2)) -> sel(active(X1), X2),
           active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
            active(sel(0(), cons(X, XS))) -> mark(X),
                            head(mark(X)) -> mark(head(X)),
                              head(ok(X)) -> ok(head(X)),
                             2nd(mark(X)) -> mark(2nd(X)),
                               2nd(ok(X)) -> ok(2nd(X)),
                       take(X1, mark(X2)) -> mark(take(X1, X2)),
                       take(mark(X1), X2) -> mark(take(X1, X2)),
                     take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                        sel(X1, mark(X2)) -> mark(sel(X1, X2)),
                        sel(mark(X1), X2) -> mark(sel(X1, X2)),
                      sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)),
                     proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(from(X)) -> from(proper(X)),
                             proper(s(X)) -> s(proper(X)),
                          proper(head(X)) -> head(proper(X)),
                           proper(2nd(X)) -> 2nd(proper(X)),
                            proper(nil()) -> ok(nil()),
                     proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                              proper(0()) -> ok(0()),
                      proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)),
                             top(mark(X)) -> top(proper(X)),
                               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(cons#) = 0
          Strict:
           {}
          Qed