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(X1, X2),
      activate(n__from(X)) -> from(X),
  activate(n__add(X1, X2)) -> add(X1, X2),
       activate(n__len(X)) -> len(X),
                   from(X) -> cons(X, n__from(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#(X1, X2),
        activate#(n__from(X)) -> from#(X),
    activate#(n__add(X1, X2)) -> add#(X1, X2),
         activate#(n__len(X)) -> len#(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(X1, X2),
       activate(n__from(X)) -> from(X),
   activate(n__add(X1, X2)) -> add(X1, X2),
        activate(n__len(X)) -> len(X),
                    from(X) -> cons(X, n__from(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#(X1, X2), add#(s(X), Y) -> activate#(X))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__len(X)) -> len#(X))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__from(X)) -> from#(X))
    (len#(cons(X, Z)) -> activate#(Z), activate#(n__fst(X1, X2)) -> fst#(X1, X2))
    (add#(s(X), Y) -> activate#(X), activate#(n__len(X)) -> len#(X))
    (add#(s(X), Y) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (add#(s(X), Y) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (add#(s(X), Y) -> activate#(X), activate#(n__fst(X1, X2)) -> fst#(X1, X2))
    (activate#(n__len(X)) -> len#(X), len#(cons(X, Z)) -> activate#(Z))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__fst(X1, X2)) -> fst#(X1, X2))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__len(X)) -> len#(X))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__fst(X1, X2)) -> fst#(X1, X2))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__from(X)) -> from#(X))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__len(X)) -> len#(X))
    (activate#(n__fst(X1, X2)) -> fst#(X1, X2), fst#(s(X), cons(Y, Z)) -> activate#(Z))
    (activate#(n__fst(X1, X2)) -> fst#(X1, 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#(X1, X2),
      activate#(n__add(X1, X2)) -> add#(X1, X2),
           activate#(n__len(X)) -> len#(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#(X1, X2),
       activate#(n__add(X1, X2)) -> add#(X1, X2),
            activate#(n__len(X)) -> len#(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(X1, X2),
          activate(n__from(X)) -> from(X),
      activate(n__add(X1, X2)) -> add(X1, X2),
           activate(n__len(X)) -> len(X),
                       from(X) -> cons(X, n__from(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) = [], pi(n__add) = 0, pi(add#) = 0, pi(add) = [], pi(from) = [], pi(n__from) = [], pi(s) = 0, pi(activate#) = 0, pi(activate) = [], pi(n__fst) = [0,1], pi(cons) = 1, pi(0) = [], pi(fst#) = [0,1], pi(fst) = [], pi(nil) = []
      Usable Rules:
       {}
      Interpretation:
       [fst#](x0, x1) = x0 + x1,
       [len#](x0) = x0 + 1,
       [n__fst](x0, x1) = x0 + x1,
       [n__len](x0) = x0 + 1
      Strict:
       {   fst#(s(X), cons(Y, Z)) -> activate#(Z),
           fst#(s(X), cons(Y, Z)) -> activate#(X),
        activate#(n__fst(X1, X2)) -> fst#(X1, X2),
        activate#(n__add(X1, X2)) -> add#(X1, X2),
             activate#(n__len(X)) -> len#(X),
                    add#(s(X), Y) -> 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(X1, X2),
            activate(n__from(X)) -> from(X),
        activate(n__add(X1, X2)) -> add(X1, X2),
             activate(n__len(X)) -> len(X),
                         from(X) -> cons(X, n__from(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#(X1, X2), add#(s(X), Y) -> activate#(X))
        (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__len(X)) -> len#(X))
        (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> add#(X1, X2))
        (fst#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__fst(X1, X2)) -> fst#(X1, X2))
        (add#(s(X), Y) -> activate#(X), activate#(n__fst(X1, X2)) -> fst#(X1, X2))
        (add#(s(X), Y) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
        (add#(s(X), Y) -> activate#(X), activate#(n__len(X)) -> len#(X))
        (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__fst(X1, X2)) -> fst#(X1, X2))
        (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
        (fst#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__len(X)) -> len#(X))
        (activate#(n__fst(X1, X2)) -> fst#(X1, X2), fst#(s(X), cons(Y, Z)) -> activate#(Z))
        (activate#(n__fst(X1, X2)) -> fst#(X1, 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#(X1, X2),
          activate#(n__add(X1, X2)) -> add#(X1, X2),
                      add#(s(X), Y) -> activate#(X)}
        SCC:
         Strict:
          {   fst#(s(X), cons(Y, Z)) -> activate#(Z),
              fst#(s(X), cons(Y, Z)) -> activate#(X),
           activate#(n__fst(X1, X2)) -> fst#(X1, X2),
           activate#(n__add(X1, X2)) -> add#(X1, X2),
                       add#(s(X), Y) -> 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(X1, X2),
              activate(n__from(X)) -> from(X),
          activate(n__add(X1, X2)) -> add(X1, X2),
               activate(n__len(X)) -> len(X),
                           from(X) -> cons(X, n__from(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) = [], pi(len) = [], pi(n__add) = [0], pi(add#) = 0, pi(add) = [], pi(from) = [], pi(n__from) = [], pi(s) = 0, pi(activate#) = 0, pi(activate) = [], pi(n__fst) = [0,1], pi(cons) = [1], pi(0) = [], pi(fst#) = [0,1], pi(fst) = [], pi(nil) = []
          Usable Rules:
           {}
          Interpretation:
           [fst#](x0, x1) = x0 + x1,
           [n__add](x0) = x0 + 1,
           [n__fst](x0, x1) = x0 + x1 + 1,
           [cons](x0) = x0 + 1
          Strict:
           {add#(s(X), Y) -> 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(X1, X2),
                activate(n__from(X)) -> from(X),
            activate(n__add(X1, X2)) -> add(X1, X2),
                 activate(n__len(X)) -> len(X),
                             from(X) -> cons(X, n__from(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:
           {}
           SCCS:
            
            Qed