YES
TRS:
 {                    mark(nil()) -> active(nil()),
              mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                        mark(0()) -> active(0()),
               mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                       mark(s(X)) -> active(s(mark(X))),
                    mark(from(X)) -> active(from(mark(X))),
            active(first(0(), X)) -> mark(nil()),
  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                  active(from(X)) -> mark(cons(X, from(s(X)))),
              first(X1, mark(X2)) -> first(X1, X2),
            first(X1, active(X2)) -> first(X1, X2),
              first(mark(X1), X2) -> first(X1, X2),
            first(active(X1), X2) -> first(X1, X2),
               cons(X1, mark(X2)) -> cons(X1, X2),
             cons(X1, active(X2)) -> cons(X1, X2),
               cons(mark(X1), X2) -> cons(X1, X2),
             cons(active(X1), X2) -> cons(X1, X2),
                       s(mark(X)) -> s(X),
                     s(active(X)) -> s(X),
                    from(mark(X)) -> from(X),
                  from(active(X)) -> from(X)}
 DP:
  Strict:
   {                    mark#(nil()) -> active#(nil()),
                mark#(first(X1, X2)) -> mark#(X1),
                mark#(first(X1, X2)) -> mark#(X2),
                mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))),
                mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)),
                          mark#(0()) -> active#(0()),
                 mark#(cons(X1, X2)) -> mark#(X1),
                 mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
                 mark#(cons(X1, X2)) -> cons#(mark(X1), X2),
                         mark#(s(X)) -> mark#(X),
                         mark#(s(X)) -> active#(s(mark(X))),
                         mark#(s(X)) -> s#(mark(X)),
                      mark#(from(X)) -> mark#(X),
                      mark#(from(X)) -> active#(from(mark(X))),
                      mark#(from(X)) -> from#(mark(X)),
              active#(first(0(), X)) -> mark#(nil()),
    active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))),
    active#(first(s(X), cons(Y, Z))) -> first#(X, Z),
    active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)),
                    active#(from(X)) -> mark#(cons(X, from(s(X)))),
                    active#(from(X)) -> cons#(X, from(s(X))),
                    active#(from(X)) -> s#(X),
                    active#(from(X)) -> from#(s(X)),
                first#(X1, mark(X2)) -> first#(X1, X2),
              first#(X1, active(X2)) -> first#(X1, X2),
                first#(mark(X1), X2) -> first#(X1, X2),
              first#(active(X1), X2) -> first#(X1, X2),
                 cons#(X1, mark(X2)) -> cons#(X1, X2),
               cons#(X1, active(X2)) -> cons#(X1, X2),
                 cons#(mark(X1), X2) -> cons#(X1, X2),
               cons#(active(X1), X2) -> cons#(X1, X2),
                         s#(mark(X)) -> s#(X),
                       s#(active(X)) -> s#(X),
                      from#(mark(X)) -> from#(X),
                    from#(active(X)) -> from#(X)}
  Weak:
  {                    mark(nil()) -> active(nil()),
               mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                         mark(0()) -> active(0()),
                mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                        mark(s(X)) -> active(s(mark(X))),
                     mark(from(X)) -> active(from(mark(X))),
             active(first(0(), X)) -> mark(nil()),
   active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                   active(from(X)) -> mark(cons(X, from(s(X)))),
               first(X1, mark(X2)) -> first(X1, X2),
             first(X1, active(X2)) -> first(X1, X2),
               first(mark(X1), X2) -> first(X1, X2),
             first(active(X1), X2) -> first(X1, X2),
                cons(X1, mark(X2)) -> cons(X1, X2),
              cons(X1, active(X2)) -> cons(X1, X2),
                cons(mark(X1), X2) -> cons(X1, X2),
              cons(active(X1), X2) -> cons(X1, X2),
                        s(mark(X)) -> s(X),
                      s(active(X)) -> s(X),
                     from(mark(X)) -> from(X),
                   from(active(X)) -> from(X)}
  EDG:
   {
    (mark#(first(X1, X2)) -> mark#(X2), mark#(from(X)) -> from#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0()))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(nil()) -> active#(nil()))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> from#(s(X)))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> s#(X))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> cons#(X, from(s(X))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> mark#(cons(X, from(s(X)))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(first(0(), X)) -> mark#(nil()))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(nil()) -> active#(nil()))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(from(X)) -> from#(mark(X)))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(from(X)) -> active#(from(mark(X))))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(from(X)) -> mark#(X))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(s(X)) -> s#(mark(X)))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(s(X)) -> active#(s(mark(X))))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(s(X)) -> mark#(X))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(first(X1, X2)) -> mark#(X2))
    (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, active(X2)) -> cons#(X1, X2))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (mark#(from(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X)))
    (mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
    (mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
    (mark#(from(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (mark#(from(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(from(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(from(X)) -> mark#(X), mark#(0()) -> active#(0()))
    (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)))
    (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
    (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(from(X)) -> mark#(X), mark#(nil()) -> active#(nil()))
    (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X))
    (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X))
    (from#(mark(X)) -> from#(X), from#(mark(X)) -> from#(X))
    (mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(from(X)) -> from#(s(X)))
    (mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(from(X)) -> s#(X))
    (mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(from(X)) -> cons#(X, from(s(X))))
    (mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X)))))
    (mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))))
    (mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(first(0(), X)) -> mark#(nil()))
    (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> from#(s(X)))
    (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> s#(X))
    (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> cons#(X, from(s(X))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X)))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (mark#(s(X)) -> active#(s(mark(X))), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (mark#(s(X)) -> active#(s(mark(X))), active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(first(0(), X)) -> mark#(nil()))
    (active#(first(0(), X)) -> mark#(nil()), mark#(nil()) -> active#(nil()))
    (mark#(from(X)) -> from#(mark(X)), from#(active(X)) -> from#(X))
    (mark#(from(X)) -> from#(mark(X)), from#(mark(X)) -> from#(X))
    (first#(X1, mark(X2)) -> first#(X1, X2), first#(active(X1), X2) -> first#(X1, X2))
    (first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
    (first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, active(X2)) -> first#(X1, X2))
    (first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
    (first#(mark(X1), X2) -> first#(X1, X2), first#(active(X1), X2) -> first#(X1, X2))
    (first#(mark(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
    (first#(mark(X1), X2) -> first#(X1, X2), first#(X1, active(X2)) -> first#(X1, X2))
    (first#(mark(X1), X2) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (first#(active(X1), X2) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
    (first#(active(X1), X2) -> first#(X1, X2), first#(X1, active(X2)) -> first#(X1, X2))
    (first#(active(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
    (first#(active(X1), X2) -> first#(X1, X2), first#(active(X1), X2) -> first#(X1, X2))
    (first#(X1, active(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
    (first#(X1, active(X2)) -> first#(X1, X2), first#(X1, active(X2)) -> first#(X1, X2))
    (first#(X1, active(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
    (first#(X1, active(X2)) -> first#(X1, X2), first#(active(X1), X2) -> first#(X1, X2))
    (active#(from(X)) -> from#(s(X)), from#(mark(X)) -> from#(X))
    (active#(from(X)) -> from#(s(X)), from#(active(X)) -> from#(X))
    (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X))
    (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X))
    (mark#(from(X)) -> active#(from(mark(X))), active#(first(0(), X)) -> mark#(nil()))
    (mark#(from(X)) -> active#(from(mark(X))), active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))))
    (mark#(from(X)) -> active#(from(mark(X))), active#(first(s(X), cons(Y, Z))) -> first#(X, Z))
    (mark#(from(X)) -> active#(from(mark(X))), active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)))
    (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X)))))
    (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> cons#(X, from(s(X))))
    (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> s#(X))
    (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> from#(s(X)))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(first(X1, X2)) -> mark#(X1))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(first(X1, X2)) -> mark#(X2))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> mark#(X))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> active#(s(mark(X))))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> s#(mark(X)))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> mark#(X))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> active#(from(mark(X))))
    (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> from#(mark(X)))
    (from#(active(X)) -> from#(X), from#(mark(X)) -> from#(X))
    (from#(active(X)) -> from#(X), from#(active(X)) -> from#(X))
    (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))
    (active#(from(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (active#(from(X)) -> s#(X), s#(active(X)) -> s#(X))
    (mark#(s(X)) -> mark#(X), mark#(nil()) -> active#(nil()))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0()))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
    (mark#(s(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X)))
    (mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)), first#(X1, mark(X2)) -> first#(X1, X2))
    (mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)), first#(X1, active(X2)) -> first#(X1, X2))
    (mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)), first#(mark(X1), X2) -> first#(X1, X2))
    (mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)), first#(active(X1), X2) -> first#(X1, X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(nil()) -> active#(nil()))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> first#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X)))
    (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(X1, mark(X2)) -> first#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(X1, active(X2)) -> first#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(mark(X1), X2) -> first#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> first#(X, Z), first#(active(X1), X2) -> first#(X1, X2))
    (active#(from(X)) -> cons#(X, from(s(X))), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (active#(from(X)) -> cons#(X, from(s(X))), cons#(X1, active(X2)) -> cons#(X1, X2))
    (active#(from(X)) -> cons#(X, from(s(X))), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(from(X)) -> cons#(X, from(s(X))), cons#(active(X1), X2) -> cons#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)), cons#(X1, active(X2)) -> cons#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(first(s(X), cons(Y, Z))) -> cons#(Y, first(X, Z)), cons#(active(X1), X2) -> cons#(X1, X2))
   }
   SCCS:
    Scc:
     {  from#(mark(X)) -> from#(X),
      from#(active(X)) -> from#(X)}
    Scc:
     {  s#(mark(X)) -> s#(X),
      s#(active(X)) -> s#(X)}
    Scc:
     {  cons#(X1, mark(X2)) -> cons#(X1, X2),
      cons#(X1, active(X2)) -> cons#(X1, X2),
        cons#(mark(X1), X2) -> cons#(X1, X2),
      cons#(active(X1), X2) -> cons#(X1, X2)}
    Scc:
     {  first#(X1, mark(X2)) -> first#(X1, X2),
      first#(X1, active(X2)) -> first#(X1, X2),
        first#(mark(X1), X2) -> first#(X1, X2),
      first#(active(X1), X2) -> first#(X1, X2)}
    Scc:
     {            mark#(first(X1, X2)) -> mark#(X1),
                  mark#(first(X1, X2)) -> mark#(X2),
                  mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))),
                   mark#(cons(X1, X2)) -> mark#(X1),
                   mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
                           mark#(s(X)) -> mark#(X),
                           mark#(s(X)) -> active#(s(mark(X))),
                        mark#(from(X)) -> mark#(X),
                        mark#(from(X)) -> active#(from(mark(X))),
      active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))),
                      active#(from(X)) -> mark#(cons(X, from(s(X))))}
    SCC:
     Strict:
      {  from#(mark(X)) -> from#(X),
       from#(active(X)) -> from#(X)}
     Weak:
     {                    mark(nil()) -> active(nil()),
                  mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                            mark(0()) -> active(0()),
                   mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(s(X)) -> active(s(mark(X))),
                        mark(from(X)) -> active(from(mark(X))),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                  first(X1, mark(X2)) -> first(X1, X2),
                first(X1, active(X2)) -> first(X1, X2),
                  first(mark(X1), X2) -> first(X1, X2),
                first(active(X1), X2) -> first(X1, X2),
                   cons(X1, mark(X2)) -> cons(X1, X2),
                 cons(X1, active(X2)) -> cons(X1, X2),
                   cons(mark(X1), X2) -> cons(X1, X2),
                 cons(active(X1), X2) -> cons(X1, X2),
                           s(mark(X)) -> s(X),
                         s(active(X)) -> s(X),
                        from(mark(X)) -> from(X),
                      from(active(X)) -> from(X)}
     SPSC:
      Simple Projection:
       pi(from#) = 0
      Strict:
       {from#(active(X)) -> from#(X)}
      EDG:
       {(from#(active(X)) -> from#(X), from#(active(X)) -> from#(X))}
       SCCS:
        Scc:
         {from#(active(X)) -> from#(X)}
        SCC:
         Strict:
          {from#(active(X)) -> from#(X)}
         Weak:
         {                    mark(nil()) -> active(nil()),
                      mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                mark(0()) -> active(0()),
                       mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(s(X)) -> active(s(mark(X))),
                            mark(from(X)) -> active(from(mark(X))),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                      first(X1, mark(X2)) -> first(X1, X2),
                    first(X1, active(X2)) -> first(X1, X2),
                      first(mark(X1), X2) -> first(X1, X2),
                    first(active(X1), X2) -> first(X1, X2),
                       cons(X1, mark(X2)) -> cons(X1, X2),
                     cons(X1, active(X2)) -> cons(X1, X2),
                       cons(mark(X1), X2) -> cons(X1, X2),
                     cons(active(X1), X2) -> cons(X1, X2),
                               s(mark(X)) -> s(X),
                             s(active(X)) -> s(X),
                            from(mark(X)) -> from(X),
                          from(active(X)) -> from(X)}
         SPSC:
          Simple Projection:
           pi(from#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  s#(mark(X)) -> s#(X),
       s#(active(X)) -> s#(X)}
     Weak:
     {                    mark(nil()) -> active(nil()),
                  mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                            mark(0()) -> active(0()),
                   mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(s(X)) -> active(s(mark(X))),
                        mark(from(X)) -> active(from(mark(X))),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                  first(X1, mark(X2)) -> first(X1, X2),
                first(X1, active(X2)) -> first(X1, X2),
                  first(mark(X1), X2) -> first(X1, X2),
                first(active(X1), X2) -> first(X1, X2),
                   cons(X1, mark(X2)) -> cons(X1, X2),
                 cons(X1, active(X2)) -> cons(X1, X2),
                   cons(mark(X1), X2) -> cons(X1, X2),
                 cons(active(X1), X2) -> cons(X1, X2),
                           s(mark(X)) -> s(X),
                         s(active(X)) -> s(X),
                        from(mark(X)) -> from(X),
                      from(active(X)) -> from(X)}
     SPSC:
      Simple Projection:
       pi(s#) = 0
      Strict:
       {s#(active(X)) -> s#(X)}
      EDG:
       {(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))}
       SCCS:
        Scc:
         {s#(active(X)) -> s#(X)}
        SCC:
         Strict:
          {s#(active(X)) -> s#(X)}
         Weak:
         {                    mark(nil()) -> active(nil()),
                      mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                mark(0()) -> active(0()),
                       mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(s(X)) -> active(s(mark(X))),
                            mark(from(X)) -> active(from(mark(X))),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                      first(X1, mark(X2)) -> first(X1, X2),
                    first(X1, active(X2)) -> first(X1, X2),
                      first(mark(X1), X2) -> first(X1, X2),
                    first(active(X1), X2) -> first(X1, X2),
                       cons(X1, mark(X2)) -> cons(X1, X2),
                     cons(X1, active(X2)) -> cons(X1, X2),
                       cons(mark(X1), X2) -> cons(X1, X2),
                     cons(active(X1), X2) -> cons(X1, X2),
                               s(mark(X)) -> s(X),
                             s(active(X)) -> s(X),
                            from(mark(X)) -> from(X),
                          from(active(X)) -> from(X)}
         SPSC:
          Simple Projection:
           pi(s#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  cons#(X1, mark(X2)) -> cons#(X1, X2),
       cons#(X1, active(X2)) -> cons#(X1, X2),
         cons#(mark(X1), X2) -> cons#(X1, X2),
       cons#(active(X1), X2) -> cons#(X1, X2)}
     Weak:
     {                    mark(nil()) -> active(nil()),
                  mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                            mark(0()) -> active(0()),
                   mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(s(X)) -> active(s(mark(X))),
                        mark(from(X)) -> active(from(mark(X))),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                  first(X1, mark(X2)) -> first(X1, X2),
                first(X1, active(X2)) -> first(X1, X2),
                  first(mark(X1), X2) -> first(X1, X2),
                first(active(X1), X2) -> first(X1, X2),
                   cons(X1, mark(X2)) -> cons(X1, X2),
                 cons(X1, active(X2)) -> cons(X1, X2),
                   cons(mark(X1), X2) -> cons(X1, X2),
                 cons(active(X1), X2) -> cons(X1, X2),
                           s(mark(X)) -> s(X),
                         s(active(X)) -> s(X),
                        from(mark(X)) -> from(X),
                      from(active(X)) -> from(X)}
     SPSC:
      Simple Projection:
       pi(cons#) = 0
      Strict:
       {  cons#(X1, mark(X2)) -> cons#(X1, X2),
        cons#(X1, active(X2)) -> cons#(X1, X2),
          cons#(mark(X1), X2) -> cons#(X1, X2)}
      EDG:
       {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
        (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
        (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
        (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
        (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
        (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
        (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
        (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
        (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))}
       SCCS:
        Scc:
         {  cons#(X1, mark(X2)) -> cons#(X1, X2),
          cons#(X1, active(X2)) -> cons#(X1, X2),
            cons#(mark(X1), X2) -> cons#(X1, X2)}
        SCC:
         Strict:
          {  cons#(X1, mark(X2)) -> cons#(X1, X2),
           cons#(X1, active(X2)) -> cons#(X1, X2),
             cons#(mark(X1), X2) -> cons#(X1, X2)}
         Weak:
         {                    mark(nil()) -> active(nil()),
                      mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                mark(0()) -> active(0()),
                       mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(s(X)) -> active(s(mark(X))),
                            mark(from(X)) -> active(from(mark(X))),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                      first(X1, mark(X2)) -> first(X1, X2),
                    first(X1, active(X2)) -> first(X1, X2),
                      first(mark(X1), X2) -> first(X1, X2),
                    first(active(X1), X2) -> first(X1, X2),
                       cons(X1, mark(X2)) -> cons(X1, X2),
                     cons(X1, active(X2)) -> cons(X1, X2),
                       cons(mark(X1), X2) -> cons(X1, X2),
                     cons(active(X1), X2) -> cons(X1, X2),
                               s(mark(X)) -> s(X),
                             s(active(X)) -> s(X),
                            from(mark(X)) -> from(X),
                          from(active(X)) -> from(X)}
         SPSC:
          Simple Projection:
           pi(cons#) = 1
          Strict:
           {cons#(X1, mark(X2)) -> cons#(X1, X2),
            cons#(mark(X1), X2) -> cons#(X1, X2)}
          EDG:
           {(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
            (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
            (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
            (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))}
           SCCS:
            Scc:
             {cons#(X1, mark(X2)) -> cons#(X1, X2),
              cons#(mark(X1), X2) -> cons#(X1, X2)}
            SCC:
             Strict:
              {cons#(X1, mark(X2)) -> cons#(X1, X2),
               cons#(mark(X1), X2) -> cons#(X1, X2)}
             Weak:
             {                    mark(nil()) -> active(nil()),
                          mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                    mark(0()) -> active(0()),
                           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                   mark(s(X)) -> active(s(mark(X))),
                                mark(from(X)) -> active(from(mark(X))),
                        active(first(0(), X)) -> mark(nil()),
              active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                              active(from(X)) -> mark(cons(X, from(s(X)))),
                          first(X1, mark(X2)) -> first(X1, X2),
                        first(X1, active(X2)) -> first(X1, X2),
                          first(mark(X1), X2) -> first(X1, X2),
                        first(active(X1), X2) -> first(X1, X2),
                           cons(X1, mark(X2)) -> cons(X1, X2),
                         cons(X1, active(X2)) -> cons(X1, X2),
                           cons(mark(X1), X2) -> cons(X1, X2),
                         cons(active(X1), X2) -> cons(X1, X2),
                                   s(mark(X)) -> s(X),
                                 s(active(X)) -> s(X),
                                from(mark(X)) -> from(X),
                              from(active(X)) -> from(X)}
             SPSC:
              Simple Projection:
               pi(cons#) = 0
              Strict:
               {cons#(X1, mark(X2)) -> cons#(X1, X2)}
              EDG:
               {(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))}
               SCCS:
                Scc:
                 {cons#(X1, mark(X2)) -> cons#(X1, X2)}
                SCC:
                 Strict:
                  {cons#(X1, mark(X2)) -> cons#(X1, X2)}
                 Weak:
                 {                    mark(nil()) -> active(nil()),
                              mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                        mark(0()) -> active(0()),
                               mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                       mark(s(X)) -> active(s(mark(X))),
                                    mark(from(X)) -> active(from(mark(X))),
                            active(first(0(), X)) -> mark(nil()),
                  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                  active(from(X)) -> mark(cons(X, from(s(X)))),
                              first(X1, mark(X2)) -> first(X1, X2),
                            first(X1, active(X2)) -> first(X1, X2),
                              first(mark(X1), X2) -> first(X1, X2),
                            first(active(X1), X2) -> first(X1, X2),
                               cons(X1, mark(X2)) -> cons(X1, X2),
                             cons(X1, active(X2)) -> cons(X1, X2),
                               cons(mark(X1), X2) -> cons(X1, X2),
                             cons(active(X1), X2) -> cons(X1, X2),
                                       s(mark(X)) -> s(X),
                                     s(active(X)) -> s(X),
                                    from(mark(X)) -> from(X),
                                  from(active(X)) -> from(X)}
                 SPSC:
                  Simple Projection:
                   pi(cons#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {  first#(X1, mark(X2)) -> first#(X1, X2),
       first#(X1, active(X2)) -> first#(X1, X2),
         first#(mark(X1), X2) -> first#(X1, X2),
       first#(active(X1), X2) -> first#(X1, X2)}
     Weak:
     {                    mark(nil()) -> active(nil()),
                  mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                            mark(0()) -> active(0()),
                   mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(s(X)) -> active(s(mark(X))),
                        mark(from(X)) -> active(from(mark(X))),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                  first(X1, mark(X2)) -> first(X1, X2),
                first(X1, active(X2)) -> first(X1, X2),
                  first(mark(X1), X2) -> first(X1, X2),
                first(active(X1), X2) -> first(X1, X2),
                   cons(X1, mark(X2)) -> cons(X1, X2),
                 cons(X1, active(X2)) -> cons(X1, X2),
                   cons(mark(X1), X2) -> cons(X1, X2),
                 cons(active(X1), X2) -> cons(X1, X2),
                           s(mark(X)) -> s(X),
                         s(active(X)) -> s(X),
                        from(mark(X)) -> from(X),
                      from(active(X)) -> from(X)}
     SPSC:
      Simple Projection:
       pi(first#) = 1
      Strict:
       {  first#(X1, mark(X2)) -> first#(X1, X2),
          first#(mark(X1), X2) -> first#(X1, X2),
        first#(active(X1), X2) -> first#(X1, X2)}
      EDG:
       {(first#(mark(X1), X2) -> first#(X1, X2), first#(active(X1), X2) -> first#(X1, X2))
        (first#(mark(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
        (first#(mark(X1), X2) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
        (first#(active(X1), X2) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
        (first#(active(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
        (first#(active(X1), X2) -> first#(X1, X2), first#(active(X1), X2) -> first#(X1, X2))
        (first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
        (first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
        (first#(X1, mark(X2)) -> first#(X1, X2), first#(active(X1), X2) -> first#(X1, X2))}
       SCCS:
        Scc:
         {  first#(X1, mark(X2)) -> first#(X1, X2),
            first#(mark(X1), X2) -> first#(X1, X2),
          first#(active(X1), X2) -> first#(X1, X2)}
        SCC:
         Strict:
          {  first#(X1, mark(X2)) -> first#(X1, X2),
             first#(mark(X1), X2) -> first#(X1, X2),
           first#(active(X1), X2) -> first#(X1, X2)}
         Weak:
         {                    mark(nil()) -> active(nil()),
                      mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                mark(0()) -> active(0()),
                       mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(s(X)) -> active(s(mark(X))),
                            mark(from(X)) -> active(from(mark(X))),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                      first(X1, mark(X2)) -> first(X1, X2),
                    first(X1, active(X2)) -> first(X1, X2),
                      first(mark(X1), X2) -> first(X1, X2),
                    first(active(X1), X2) -> first(X1, X2),
                       cons(X1, mark(X2)) -> cons(X1, X2),
                     cons(X1, active(X2)) -> cons(X1, X2),
                       cons(mark(X1), X2) -> cons(X1, X2),
                     cons(active(X1), X2) -> cons(X1, X2),
                               s(mark(X)) -> s(X),
                             s(active(X)) -> s(X),
                            from(mark(X)) -> from(X),
                          from(active(X)) -> from(X)}
         SPSC:
          Simple Projection:
           pi(first#) = 0
          Strict:
           {first#(X1, mark(X2)) -> first#(X1, X2),
            first#(mark(X1), X2) -> first#(X1, X2)}
          EDG:
           {(first#(mark(X1), X2) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))
            (first#(mark(X1), X2) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
            (first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))
            (first#(X1, mark(X2)) -> first#(X1, X2), first#(mark(X1), X2) -> first#(X1, X2))}
           SCCS:
            Scc:
             {first#(X1, mark(X2)) -> first#(X1, X2),
              first#(mark(X1), X2) -> first#(X1, X2)}
            SCC:
             Strict:
              {first#(X1, mark(X2)) -> first#(X1, X2),
               first#(mark(X1), X2) -> first#(X1, X2)}
             Weak:
             {                    mark(nil()) -> active(nil()),
                          mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                    mark(0()) -> active(0()),
                           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                   mark(s(X)) -> active(s(mark(X))),
                                mark(from(X)) -> active(from(mark(X))),
                        active(first(0(), X)) -> mark(nil()),
              active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                              active(from(X)) -> mark(cons(X, from(s(X)))),
                          first(X1, mark(X2)) -> first(X1, X2),
                        first(X1, active(X2)) -> first(X1, X2),
                          first(mark(X1), X2) -> first(X1, X2),
                        first(active(X1), X2) -> first(X1, X2),
                           cons(X1, mark(X2)) -> cons(X1, X2),
                         cons(X1, active(X2)) -> cons(X1, X2),
                           cons(mark(X1), X2) -> cons(X1, X2),
                         cons(active(X1), X2) -> cons(X1, X2),
                                   s(mark(X)) -> s(X),
                                 s(active(X)) -> s(X),
                                from(mark(X)) -> from(X),
                              from(active(X)) -> from(X)}
             SPSC:
              Simple Projection:
               pi(first#) = 0
              Strict:
               {first#(X1, mark(X2)) -> first#(X1, X2)}
              EDG:
               {(first#(X1, mark(X2)) -> first#(X1, X2), first#(X1, mark(X2)) -> first#(X1, X2))}
               SCCS:
                Scc:
                 {first#(X1, mark(X2)) -> first#(X1, X2)}
                SCC:
                 Strict:
                  {first#(X1, mark(X2)) -> first#(X1, X2)}
                 Weak:
                 {                    mark(nil()) -> active(nil()),
                              mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                        mark(0()) -> active(0()),
                               mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                       mark(s(X)) -> active(s(mark(X))),
                                    mark(from(X)) -> active(from(mark(X))),
                            active(first(0(), X)) -> mark(nil()),
                  active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                                  active(from(X)) -> mark(cons(X, from(s(X)))),
                              first(X1, mark(X2)) -> first(X1, X2),
                            first(X1, active(X2)) -> first(X1, X2),
                              first(mark(X1), X2) -> first(X1, X2),
                            first(active(X1), X2) -> first(X1, X2),
                               cons(X1, mark(X2)) -> cons(X1, X2),
                             cons(X1, active(X2)) -> cons(X1, X2),
                               cons(mark(X1), X2) -> cons(X1, X2),
                             cons(active(X1), X2) -> cons(X1, X2),
                                       s(mark(X)) -> s(X),
                                     s(active(X)) -> s(X),
                                    from(mark(X)) -> from(X),
                                  from(active(X)) -> from(X)}
                 SPSC:
                  Simple Projection:
                   pi(first#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {            mark#(first(X1, X2)) -> mark#(X1),
                   mark#(first(X1, X2)) -> mark#(X2),
                   mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))),
                    mark#(cons(X1, X2)) -> mark#(X1),
                    mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
                            mark#(s(X)) -> mark#(X),
                            mark#(s(X)) -> active#(s(mark(X))),
                         mark#(from(X)) -> mark#(X),
                         mark#(from(X)) -> active#(from(mark(X))),
       active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))),
                       active#(from(X)) -> mark#(cons(X, from(s(X))))}
     Weak:
     {                    mark(nil()) -> active(nil()),
                  mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                            mark(0()) -> active(0()),
                   mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(s(X)) -> active(s(mark(X))),
                        mark(from(X)) -> active(from(mark(X))),
                active(first(0(), X)) -> mark(nil()),
      active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                      active(from(X)) -> mark(cons(X, from(s(X)))),
                  first(X1, mark(X2)) -> first(X1, X2),
                first(X1, active(X2)) -> first(X1, X2),
                  first(mark(X1), X2) -> first(X1, X2),
                first(active(X1), X2) -> first(X1, X2),
                   cons(X1, mark(X2)) -> cons(X1, X2),
                 cons(X1, active(X2)) -> cons(X1, X2),
                   cons(mark(X1), X2) -> cons(X1, X2),
                 cons(active(X1), X2) -> cons(X1, X2),
                           s(mark(X)) -> s(X),
                         s(active(X)) -> s(X),
                        from(mark(X)) -> from(X),
                      from(active(X)) -> from(X)}
     POLY:
      Argument Filtering:
       pi(from) = [], pi(s) = [], pi(cons) = [], pi(0) = [], pi(first) = [], pi(active#) = 0, pi(active) = [], pi(nil) = [], pi(mark#) = [], pi(mark) = []
      Usable Rules:
       {}
      Interpretation:
       [mark#] = 1,
       [cons] = 0,
       [first] = 1,
       [from] = 1,
       [s] = 0
      Strict:
       {            mark#(first(X1, X2)) -> mark#(X1),
                    mark#(first(X1, X2)) -> mark#(X2),
                    mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))),
                     mark#(cons(X1, X2)) -> mark#(X1),
                             mark#(s(X)) -> mark#(X),
                          mark#(from(X)) -> mark#(X),
                          mark#(from(X)) -> active#(from(mark(X))),
        active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))),
                        active#(from(X)) -> mark#(cons(X, from(s(X))))}
      Weak:
       {                    mark(nil()) -> active(nil()),
                    mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                              mark(0()) -> active(0()),
                     mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                             mark(s(X)) -> active(s(mark(X))),
                          mark(from(X)) -> active(from(mark(X))),
                  active(first(0(), X)) -> mark(nil()),
        active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                        active(from(X)) -> mark(cons(X, from(s(X)))),
                    first(X1, mark(X2)) -> first(X1, X2),
                  first(X1, active(X2)) -> first(X1, X2),
                    first(mark(X1), X2) -> first(X1, X2),
                  first(active(X1), X2) -> first(X1, X2),
                     cons(X1, mark(X2)) -> cons(X1, X2),
                   cons(X1, active(X2)) -> cons(X1, X2),
                     cons(mark(X1), X2) -> cons(X1, X2),
                   cons(active(X1), X2) -> cons(X1, X2),
                             s(mark(X)) -> s(X),
                           s(active(X)) -> s(X),
                          from(mark(X)) -> from(X),
                        from(active(X)) -> from(X)}
      EDG:
       {(mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X)))))
        (mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))), active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))))
        (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> active#(from(mark(X))))
        (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> mark#(X))
        (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> mark#(X))
        (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
        (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(first(X1, X2)) -> mark#(X2))
        (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
        (mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
        (mark#(from(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
        (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(first(X1, X2)) -> mark#(X1))
        (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(first(X1, X2)) -> mark#(X2))
        (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
        (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(s(X)) -> mark#(X))
        (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(from(X)) -> mark#(X))
        (active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))), mark#(from(X)) -> active#(from(mark(X))))
        (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
        (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X))))
        (mark#(from(X)) -> active#(from(mark(X))), active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))))
        (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X)))))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X))))}
       SCCS:
        Scc:
         {            mark#(first(X1, X2)) -> mark#(X1),
                      mark#(first(X1, X2)) -> mark#(X2),
                      mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))),
                       mark#(cons(X1, X2)) -> mark#(X1),
                               mark#(s(X)) -> mark#(X),
                            mark#(from(X)) -> mark#(X),
                            mark#(from(X)) -> active#(from(mark(X))),
          active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))),
                          active#(from(X)) -> mark#(cons(X, from(s(X))))}
        SCC:
         Strict:
          {            mark#(first(X1, X2)) -> mark#(X1),
                       mark#(first(X1, X2)) -> mark#(X2),
                       mark#(first(X1, X2)) -> active#(first(mark(X1), mark(X2))),
                        mark#(cons(X1, X2)) -> mark#(X1),
                                mark#(s(X)) -> mark#(X),
                             mark#(from(X)) -> mark#(X),
                             mark#(from(X)) -> active#(from(mark(X))),
           active#(first(s(X), cons(Y, Z))) -> mark#(cons(Y, first(X, Z))),
                           active#(from(X)) -> mark#(cons(X, from(s(X))))}
         Weak:
         {                    mark(nil()) -> active(nil()),
                      mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                mark(0()) -> active(0()),
                       mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(s(X)) -> active(s(mark(X))),
                            mark(from(X)) -> active(from(mark(X))),
                    active(first(0(), X)) -> mark(nil()),
          active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                          active(from(X)) -> mark(cons(X, from(s(X)))),
                      first(X1, mark(X2)) -> first(X1, X2),
                    first(X1, active(X2)) -> first(X1, X2),
                      first(mark(X1), X2) -> first(X1, X2),
                    first(active(X1), X2) -> first(X1, X2),
                       cons(X1, mark(X2)) -> cons(X1, X2),
                     cons(X1, active(X2)) -> cons(X1, X2),
                       cons(mark(X1), X2) -> cons(X1, X2),
                     cons(active(X1), X2) -> cons(X1, X2),
                               s(mark(X)) -> s(X),
                             s(active(X)) -> s(X),
                            from(mark(X)) -> from(X),
                          from(active(X)) -> from(X)}
         POLY:
          Argument Filtering:
           pi(from) = [0], pi(s) = [0], pi(cons) = 0, pi(0) = [], pi(first) = [0,1], pi(active#) = 0, pi(active) = 0, pi(nil) = [], pi(mark#) = [0], pi(mark) = 0
          Usable Rules:
           {}
          Interpretation:
           [mark#](x0) = x0 + 1,
           [first](x0, x1) = x0 + x1 + 1,
           [from](x0) = x0 + 1,
           [s](x0) = x0 + 1
          Strict:
           {mark#(cons(X1, X2)) -> mark#(X1),
               active#(from(X)) -> mark#(cons(X, from(s(X))))}
          Weak:
           {                    mark(nil()) -> active(nil()),
                        mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                  mark(0()) -> active(0()),
                         mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                 mark(s(X)) -> active(s(mark(X))),
                              mark(from(X)) -> active(from(mark(X))),
                      active(first(0(), X)) -> mark(nil()),
            active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                            active(from(X)) -> mark(cons(X, from(s(X)))),
                        first(X1, mark(X2)) -> first(X1, X2),
                      first(X1, active(X2)) -> first(X1, X2),
                        first(mark(X1), X2) -> first(X1, X2),
                      first(active(X1), X2) -> first(X1, X2),
                         cons(X1, mark(X2)) -> cons(X1, X2),
                       cons(X1, active(X2)) -> cons(X1, X2),
                         cons(mark(X1), X2) -> cons(X1, X2),
                       cons(active(X1), X2) -> cons(X1, X2),
                                 s(mark(X)) -> s(X),
                               s(active(X)) -> s(X),
                              from(mark(X)) -> from(X),
                            from(active(X)) -> from(X)}
          EDG:
           {(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
            (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> mark#(X1))}
           SCCS:
            Scc:
             {mark#(cons(X1, X2)) -> mark#(X1)}
            SCC:
             Strict:
              {mark#(cons(X1, X2)) -> mark#(X1)}
             Weak:
             {                    mark(nil()) -> active(nil()),
                          mark(first(X1, X2)) -> active(first(mark(X1), mark(X2))),
                                    mark(0()) -> active(0()),
                           mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                                   mark(s(X)) -> active(s(mark(X))),
                                mark(from(X)) -> active(from(mark(X))),
                        active(first(0(), X)) -> mark(nil()),
              active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))),
                              active(from(X)) -> mark(cons(X, from(s(X)))),
                          first(X1, mark(X2)) -> first(X1, X2),
                        first(X1, active(X2)) -> first(X1, X2),
                          first(mark(X1), X2) -> first(X1, X2),
                        first(active(X1), X2) -> first(X1, X2),
                           cons(X1, mark(X2)) -> cons(X1, X2),
                         cons(X1, active(X2)) -> cons(X1, X2),
                           cons(mark(X1), X2) -> cons(X1, X2),
                         cons(active(X1), X2) -> cons(X1, X2),
                                   s(mark(X)) -> s(X),
                                 s(active(X)) -> s(X),
                                from(mark(X)) -> from(X),
                              from(active(X)) -> from(X)}
             SPSC:
              Simple Projection:
               pi(mark#) = 0
              Strict:
               {}
              Qed