YES
TRS:
 {             fst(X1, X2) -> n__fst(X1, X2),
               fst(0(), Z) -> nil(),
     fst(s(X), cons(Y, Z)) -> cons(Y, n__fst(activate(X), activate(Z))),
               activate(X) -> X,
  activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)),
      activate(n__from(X)) -> from(activate(X)),
         activate(n__s(X)) -> s(X),
  activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)),
       activate(n__len(X)) -> len(activate(X)),
                      s(X) -> n__s(X),
                   from(X) -> cons(X, n__from(n__s(X))),
                   from(X) -> n__from(X),
               add(X1, X2) -> n__add(X1, X2),
               add(0(), X) -> X,
              add(s(X), Y) -> s(n__add(activate(X), Y)),
                    len(X) -> n__len(X),
                len(nil()) -> 0(),
           len(cons(X, Z)) -> s(n__len(activate(Z)))}
 DP:
  Strict:
   {   fst#(s(X), cons(Y, Z)) -> activate#(Z),
       fst#(s(X), cons(Y, Z)) -> activate#(X),
    activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)),
    activate#(n__fst(X1, X2)) -> activate#(X1),
    activate#(n__fst(X1, X2)) -> activate#(X2),
        activate#(n__from(X)) -> activate#(X),
        activate#(n__from(X)) -> from#(activate(X)),
           activate#(n__s(X)) -> s#(X),
    activate#(n__add(X1, X2)) -> activate#(X1),
    activate#(n__add(X1, X2)) -> activate#(X2),
    activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)),
         activate#(n__len(X)) -> activate#(X),
         activate#(n__len(X)) -> len#(activate(X)),
                add#(s(X), Y) -> activate#(X),
                add#(s(X), Y) -> s#(n__add(activate(X), Y)),
             len#(cons(X, Z)) -> activate#(Z),
             len#(cons(X, Z)) -> s#(n__len(activate(Z)))}
  Weak:
  {             fst(X1, X2) -> n__fst(X1, X2),
                fst(0(), Z) -> nil(),
      fst(s(X), cons(Y, Z)) -> cons(Y, n__fst(activate(X), activate(Z))),
                activate(X) -> X,
   activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)),
       activate(n__from(X)) -> from(activate(X)),
          activate(n__s(X)) -> s(X),
   activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)),
        activate(n__len(X)) -> len(activate(X)),
                       s(X) -> n__s(X),
                    from(X) -> cons(X, n__from(n__s(X))),
                    from(X) -> n__from(X),
                add(X1, X2) -> n__add(X1, X2),
                add(0(), X) -> X,
               add(s(X), Y) -> s(n__add(activate(X), Y)),
                     len(X) -> n__len(X),
                 len(nil()) -> 0(),
            len(cons(X, Z)) -> s(n__len(activate(Z)))}
  EDG:
   {(activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)), add#(s(X), Y) -> s#(n__add(activate(X), Y)))
    (activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)), add#(s(X), Y) -> activate#(X))
    (activate#(n__len(X)) -> len#(activate(X)), len#(cons(X, Z)) -> s#(n__len(activate(Z))))
    (activate#(n__len(X)) -> len#(activate(X)), len#(cons(X, Z)) -> activate#(Z))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__len(X)) -> len#(activate(X)))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__len(X)) -> activate#(X))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X2))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(X))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__from(X)) -> activate#(X))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__fst(X1, X2)) -> activate#(X2))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__fst(X1, X2)) -> activate#(X1))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__len(X)) -> len#(activate(X)))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__len(X)) -> activate#(X))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> activate#(X2))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(X))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> activate#(X))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__fst(X1, X2)) -> activate#(X2))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__fst(X1, X2)) -> activate#(X1))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (activate#(n__from(X)) -> activate#(X), activate#(n__len(X)) -> len#(activate(X)))
    (activate#(n__from(X)) -> activate#(X), activate#(n__len(X)) -> activate#(X))
    (activate#(n__from(X)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__from(X)) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X2))
    (activate#(n__from(X)) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__from(X)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (activate#(n__from(X)) -> activate#(X), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__from(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
    (activate#(n__from(X)) -> activate#(X), activate#(n__fst(X1, X2)) -> activate#(X2))
    (activate#(n__from(X)) -> activate#(X), activate#(n__fst(X1, X2)) -> activate#(X1))
    (activate#(n__from(X)) -> activate#(X), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (activate#(n__len(X)) -> activate#(X), activate#(n__len(X)) -> len#(activate(X)))
    (activate#(n__len(X)) -> activate#(X), activate#(n__len(X)) -> activate#(X))
    (activate#(n__len(X)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__len(X)) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X2))
    (activate#(n__len(X)) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__len(X)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (activate#(n__len(X)) -> activate#(X), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__len(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
    (activate#(n__len(X)) -> activate#(X), activate#(n__fst(X1, X2)) -> activate#(X2))
    (activate#(n__len(X)) -> activate#(X), activate#(n__fst(X1, X2)) -> activate#(X1))
    (activate#(n__len(X)) -> activate#(X), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__len(X)) -> len#(activate(X)))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__len(X)) -> activate#(X))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> activate#(X2))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> activate#(X1))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__s(X)) -> s#(X))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__from(X)) -> from#(activate(X)))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__from(X)) -> activate#(X))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__fst(X1, X2)) -> activate#(X2))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__fst(X1, X2)) -> activate#(X1))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__fst(X1, X2)) -> activate#(X1))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__fst(X1, X2)) -> activate#(X2))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__from(X)) -> activate#(X))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__from(X)) -> from#(activate(X)))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__s(X)) -> s#(X))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> activate#(X1))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> activate#(X2))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__len(X)) -> activate#(X))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__len(X)) -> len#(activate(X)))
    (add#(s(X), Y) -> activate#(X), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (add#(s(X), Y) -> activate#(X), activate#(n__fst(X1, X2)) -> activate#(X1))
    (add#(s(X), Y) -> activate#(X), activate#(n__fst(X1, X2)) -> activate#(X2))
    (add#(s(X), Y) -> activate#(X), activate#(n__from(X)) -> activate#(X))
    (add#(s(X), Y) -> activate#(X), activate#(n__from(X)) -> from#(activate(X)))
    (add#(s(X), Y) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (add#(s(X), Y) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X1))
    (add#(s(X), Y) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X2))
    (add#(s(X), Y) -> activate#(X), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (add#(s(X), Y) -> activate#(X), activate#(n__len(X)) -> activate#(X))
    (add#(s(X), Y) -> activate#(X), activate#(n__len(X)) -> len#(activate(X)))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__fst(X1, X2)) -> activate#(X1))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__fst(X1, X2)) -> activate#(X2))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__from(X)) -> from#(activate(X)))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X1))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__add(X1, X2)) -> activate#(X2))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__len(X)) -> activate#(X))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__len(X)) -> len#(activate(X)))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__fst(X1, X2)) -> activate#(X1))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__fst(X1, X2)) -> activate#(X2))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> activate#(X))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(X))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> activate#(X2))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__len(X)) -> activate#(X))
    (activate#(n__fst(X1, X2)) -> activate#(X1), activate#(n__len(X)) -> len#(activate(X)))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__fst(X1, X2)) -> activate#(X1))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__fst(X1, X2)) -> activate#(X2))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__from(X)) -> activate#(X))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(X))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X2))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__len(X)) -> activate#(X))
    (activate#(n__fst(X1, X2)) -> activate#(X2), activate#(n__len(X)) -> len#(activate(X)))
    (activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)), fst#(s(X), cons(Y, Z)) -> activate#(Z))
    (activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)), fst#(s(X), cons(Y, Z)) -> activate#(X))}
   SCCS:
    Scc:
     {   fst#(s(X), cons(Y, Z)) -> activate#(Z),
         fst#(s(X), cons(Y, Z)) -> activate#(X),
      activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)),
      activate#(n__fst(X1, X2)) -> activate#(X1),
      activate#(n__fst(X1, X2)) -> activate#(X2),
          activate#(n__from(X)) -> activate#(X),
      activate#(n__add(X1, X2)) -> activate#(X1),
      activate#(n__add(X1, X2)) -> activate#(X2),
      activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)),
           activate#(n__len(X)) -> activate#(X),
           activate#(n__len(X)) -> len#(activate(X)),
                  add#(s(X), Y) -> activate#(X),
               len#(cons(X, Z)) -> activate#(Z)}
    SCC:
     Strict:
      {   fst#(s(X), cons(Y, Z)) -> activate#(Z),
          fst#(s(X), cons(Y, Z)) -> activate#(X),
       activate#(n__fst(X1, X2)) -> fst#(activate(X1), activate(X2)),
       activate#(n__fst(X1, X2)) -> activate#(X1),
       activate#(n__fst(X1, X2)) -> activate#(X2),
           activate#(n__from(X)) -> activate#(X),
       activate#(n__add(X1, X2)) -> activate#(X1),
       activate#(n__add(X1, X2)) -> activate#(X2),
       activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)),
            activate#(n__len(X)) -> activate#(X),
            activate#(n__len(X)) -> len#(activate(X)),
                   add#(s(X), Y) -> activate#(X),
                len#(cons(X, Z)) -> activate#(Z)}
     Weak:
     {             fst(X1, X2) -> n__fst(X1, X2),
                   fst(0(), Z) -> nil(),
         fst(s(X), cons(Y, Z)) -> cons(Y, n__fst(activate(X), activate(Z))),
                   activate(X) -> X,
      activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)),
          activate(n__from(X)) -> from(activate(X)),
             activate(n__s(X)) -> s(X),
      activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)),
           activate(n__len(X)) -> len(activate(X)),
                          s(X) -> n__s(X),
                       from(X) -> cons(X, n__from(n__s(X))),
                       from(X) -> n__from(X),
                   add(X1, X2) -> n__add(X1, X2),
                   add(0(), X) -> X,
                  add(s(X), Y) -> s(n__add(activate(X), Y)),
                        len(X) -> n__len(X),
                    len(nil()) -> 0(),
               len(cons(X, Z)) -> s(n__len(activate(Z)))}
     POLY:
      Argument Filtering:
       pi(n__len) = [0], pi(len#) = [0], pi(len) = [0], pi(n__add) = [0,1], pi(add#) = [0], pi(add) = [0,1], pi(from) = 0, pi(n__s) = 0, pi(n__from) = 0, pi(s) = 0, pi(activate#) = [0], pi(activate) = 0, pi(n__fst) = [0,1], pi(cons) = 1, pi(0) = [], pi(fst#) = [0,1], pi(fst) = [0,1], pi(nil) = []
      Usable Rules:
       {}
      Interpretation:
       [add#](x0) = x0 + 1,
       [fst#](x0, x1) = x0 + x1 + 1,
       [len#](x0) = x0 + 1,
       [activate#](x0) = x0 + 1,
       [n__add](x0, x1) = x0 + x1 + 1,
       [n__fst](x0, x1) = x0 + x1 + 1,
       [n__len](x0) = x0 + 1
      Strict:
       {fst#(s(X), cons(Y, Z)) -> activate#(Z),
        fst#(s(X), cons(Y, Z)) -> activate#(X),
         activate#(n__from(X)) -> activate#(X),
                 add#(s(X), Y) -> activate#(X),
              len#(cons(X, Z)) -> activate#(Z)}
      Weak:
       {             fst(X1, X2) -> n__fst(X1, X2),
                     fst(0(), Z) -> nil(),
           fst(s(X), cons(Y, Z)) -> cons(Y, n__fst(activate(X), activate(Z))),
                     activate(X) -> X,
        activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)),
            activate(n__from(X)) -> from(activate(X)),
               activate(n__s(X)) -> s(X),
        activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)),
             activate(n__len(X)) -> len(activate(X)),
                            s(X) -> n__s(X),
                         from(X) -> cons(X, n__from(n__s(X))),
                         from(X) -> n__from(X),
                     add(X1, X2) -> n__add(X1, X2),
                     add(0(), X) -> X,
                    add(s(X), Y) -> s(n__add(activate(X), Y)),
                          len(X) -> n__len(X),
                      len(nil()) -> 0(),
                 len(cons(X, Z)) -> s(n__len(activate(Z)))}
      EDG:
       {(len#(cons(X, Z)) -> activate#(Z), activate#(n__from(X)) -> activate#(X))
        (activate#(n__from(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
        (add#(s(X), Y) -> activate#(X), activate#(n__from(X)) -> activate#(X))
        (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
        (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__from(X)) -> activate#(X))}
       SCCS:
        Scc:
         {activate#(n__from(X)) -> activate#(X)}
        SCC:
         Strict:
          {activate#(n__from(X)) -> activate#(X)}
         Weak:
         {             fst(X1, X2) -> n__fst(X1, X2),
                       fst(0(), Z) -> nil(),
             fst(s(X), cons(Y, Z)) -> cons(Y, n__fst(activate(X), activate(Z))),
                       activate(X) -> X,
          activate(n__fst(X1, X2)) -> fst(activate(X1), activate(X2)),
              activate(n__from(X)) -> from(activate(X)),
                 activate(n__s(X)) -> s(X),
          activate(n__add(X1, X2)) -> add(activate(X1), activate(X2)),
               activate(n__len(X)) -> len(activate(X)),
                              s(X) -> n__s(X),
                           from(X) -> cons(X, n__from(n__s(X))),
                           from(X) -> n__from(X),
                       add(X1, X2) -> n__add(X1, X2),
                       add(0(), X) -> X,
                      add(s(X), Y) -> s(n__add(activate(X), Y)),
                            len(X) -> n__len(X),
                        len(nil()) -> 0(),
                   len(cons(X, Z)) -> s(n__len(activate(Z)))}
         SPSC:
          Simple Projection:
           pi(activate#) = 0
          Strict:
           {}
          Qed