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