YES
TRS:
 {   sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
      sel(0(), cons(X, XS)) -> X,
                 fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))),
               fib1(X1, X2) -> n__fib1(X1, X2),
                     fib(N) -> sel(N, fib1(s(0()), s(0()))),
                add(X1, X2) -> n__add(X1, X2),
               add(s(X), Y) -> s(add(X, Y)),
                add(0(), X) -> X,
                activate(X) -> X,
  activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)),
   activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))}
 DP:
  Strict:
   {   sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS)),
       sel#(s(N), cons(X, XS)) -> activate#(XS),
                       fib#(N) -> sel#(N, fib1(s(0()), s(0()))),
                       fib#(N) -> fib1#(s(0()), s(0())),
                 add#(s(X), Y) -> add#(X, Y),
    activate#(n__fib1(X1, X2)) -> fib1#(activate(X1), activate(X2)),
    activate#(n__fib1(X1, X2)) -> activate#(X1),
    activate#(n__fib1(X1, X2)) -> activate#(X2),
     activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)),
     activate#(n__add(X1, X2)) -> activate#(X1),
     activate#(n__add(X1, X2)) -> activate#(X2)}
  Weak:
  {   sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
       sel(0(), cons(X, XS)) -> X,
                  fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))),
                fib1(X1, X2) -> n__fib1(X1, X2),
                      fib(N) -> sel(N, fib1(s(0()), s(0()))),
                 add(X1, X2) -> n__add(X1, X2),
                add(s(X), Y) -> s(add(X, Y)),
                 add(0(), X) -> X,
                 activate(X) -> X,
   activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)),
    activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))}
  EDG:
   {(add#(s(X), Y) -> add#(X, Y), add#(s(X), Y) -> add#(X, Y))
    (fib#(N) -> sel#(N, fib1(s(0()), s(0()))), sel#(s(N), cons(X, XS)) -> activate#(XS))
    (fib#(N) -> sel#(N, fib1(s(0()), s(0()))), sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS)))
    (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__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__fib1(X1, X2)) -> activate#(X2))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__fib1(X1, X2)) -> activate#(X1))
    (activate#(n__add(X1, X2)) -> activate#(X1), activate#(n__fib1(X1, X2)) -> fib1#(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__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> activate#(X2))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> activate#(X1))
    (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> fib1#(activate(X1), activate(X2)))
    (activate#(n__fib1(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> fib1#(activate(X1), activate(X2)))
    (activate#(n__fib1(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> activate#(X1))
    (activate#(n__fib1(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> activate#(X2))
    (activate#(n__fib1(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__fib1(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__fib1(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X2))
    (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__fib1(X1, X2)) -> fib1#(activate(X1), activate(X2)))
    (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__fib1(X1, X2)) -> activate#(X1))
    (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__fib1(X1, X2)) -> activate#(X2))
    (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> activate#(X1))
    (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> activate#(X2))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__fib1(X1, X2)) -> fib1#(activate(X1), activate(X2)))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__fib1(X1, X2)) -> activate#(X1))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__fib1(X1, X2)) -> activate#(X2))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__add(X1, X2)) -> activate#(X1))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__add(X1, X2)) -> activate#(X2))
    (activate#(n__add(X1, X2)) -> add#(activate(X1), activate(X2)), add#(s(X), Y) -> add#(X, Y))
    (sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS)), sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS)))
    (sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS)), sel#(s(N), cons(X, XS)) -> activate#(XS))}
   SCCS:
    Scc:
     {activate#(n__fib1(X1, X2)) -> activate#(X1),
      activate#(n__fib1(X1, X2)) -> activate#(X2),
       activate#(n__add(X1, X2)) -> activate#(X1),
       activate#(n__add(X1, X2)) -> activate#(X2)}
    Scc:
     {add#(s(X), Y) -> add#(X, Y)}
    Scc:
     {sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS))}
    SCC:
     Strict:
      {activate#(n__fib1(X1, X2)) -> activate#(X1),
       activate#(n__fib1(X1, X2)) -> activate#(X2),
        activate#(n__add(X1, X2)) -> activate#(X1),
        activate#(n__add(X1, X2)) -> activate#(X2)}
     Weak:
     {   sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
          sel(0(), cons(X, XS)) -> X,
                     fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))),
                   fib1(X1, X2) -> n__fib1(X1, X2),
                         fib(N) -> sel(N, fib1(s(0()), s(0()))),
                    add(X1, X2) -> n__add(X1, X2),
                   add(s(X), Y) -> s(add(X, Y)),
                    add(0(), X) -> X,
                    activate(X) -> X,
      activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)),
       activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))}
     SPSC:
      Simple Projection:
       pi(activate#) = 0
      Strict:
       {activate#(n__fib1(X1, X2)) -> activate#(X1),
        activate#(n__fib1(X1, X2)) -> activate#(X2),
         activate#(n__add(X1, X2)) -> activate#(X2)}
      EDG:
       {(activate#(n__fib1(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X2))
        (activate#(n__fib1(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> activate#(X2))
        (activate#(n__fib1(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> activate#(X1))
        (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> activate#(X1))
        (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> activate#(X2))
        (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X2))
        (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__fib1(X1, X2)) -> activate#(X1))
        (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__fib1(X1, X2)) -> activate#(X2))
        (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> activate#(X2))}
       SCCS:
        Scc:
         {activate#(n__fib1(X1, X2)) -> activate#(X1),
          activate#(n__fib1(X1, X2)) -> activate#(X2),
           activate#(n__add(X1, X2)) -> activate#(X2)}
        SCC:
         Strict:
          {activate#(n__fib1(X1, X2)) -> activate#(X1),
           activate#(n__fib1(X1, X2)) -> activate#(X2),
            activate#(n__add(X1, X2)) -> activate#(X2)}
         Weak:
         {   sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
              sel(0(), cons(X, XS)) -> X,
                         fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))),
                       fib1(X1, X2) -> n__fib1(X1, X2),
                             fib(N) -> sel(N, fib1(s(0()), s(0()))),
                        add(X1, X2) -> n__add(X1, X2),
                       add(s(X), Y) -> s(add(X, Y)),
                        add(0(), X) -> X,
                        activate(X) -> X,
          activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)),
           activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))}
         SPSC:
          Simple Projection:
           pi(activate#) = 0
          Strict:
           {activate#(n__fib1(X1, X2)) -> activate#(X1),
             activate#(n__add(X1, X2)) -> activate#(X2)}
          EDG:
           {(activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X2))
            (activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__fib1(X1, X2)) -> activate#(X1))
            (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__fib1(X1, X2)) -> activate#(X1))
            (activate#(n__fib1(X1, X2)) -> activate#(X1), activate#(n__add(X1, X2)) -> activate#(X2))}
           SCCS:
            Scc:
             {activate#(n__fib1(X1, X2)) -> activate#(X1),
               activate#(n__add(X1, X2)) -> activate#(X2)}
            SCC:
             Strict:
              {activate#(n__fib1(X1, X2)) -> activate#(X1),
                activate#(n__add(X1, X2)) -> activate#(X2)}
             Weak:
             {   sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                  sel(0(), cons(X, XS)) -> X,
                             fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))),
                           fib1(X1, X2) -> n__fib1(X1, X2),
                                 fib(N) -> sel(N, fib1(s(0()), s(0()))),
                            add(X1, X2) -> n__add(X1, X2),
                           add(s(X), Y) -> s(add(X, Y)),
                            add(0(), X) -> X,
                            activate(X) -> X,
              activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)),
               activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))}
             SPSC:
              Simple Projection:
               pi(activate#) = 0
              Strict:
               {activate#(n__add(X1, X2)) -> activate#(X2)}
              EDG:
               {(activate#(n__add(X1, X2)) -> activate#(X2), activate#(n__add(X1, X2)) -> activate#(X2))}
               SCCS:
                Scc:
                 {activate#(n__add(X1, X2)) -> activate#(X2)}
                SCC:
                 Strict:
                  {activate#(n__add(X1, X2)) -> activate#(X2)}
                 Weak:
                 {   sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                      sel(0(), cons(X, XS)) -> X,
                                 fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))),
                               fib1(X1, X2) -> n__fib1(X1, X2),
                                     fib(N) -> sel(N, fib1(s(0()), s(0()))),
                                add(X1, X2) -> n__add(X1, X2),
                               add(s(X), Y) -> s(add(X, Y)),
                                add(0(), X) -> X,
                                activate(X) -> X,
                  activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)),
                   activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))}
                 SPSC:
                  Simple Projection:
                   pi(activate#) = 0
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {add#(s(X), Y) -> add#(X, Y)}
     Weak:
     {   sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
          sel(0(), cons(X, XS)) -> X,
                     fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))),
                   fib1(X1, X2) -> n__fib1(X1, X2),
                         fib(N) -> sel(N, fib1(s(0()), s(0()))),
                    add(X1, X2) -> n__add(X1, X2),
                   add(s(X), Y) -> s(add(X, Y)),
                    add(0(), X) -> X,
                    activate(X) -> X,
      activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)),
       activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS))}
     Weak:
     {   sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
          sel(0(), cons(X, XS)) -> X,
                     fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))),
                   fib1(X1, X2) -> n__fib1(X1, X2),
                         fib(N) -> sel(N, fib1(s(0()), s(0()))),
                    add(X1, X2) -> n__add(X1, X2),
                   add(s(X), Y) -> s(add(X, Y)),
                    add(0(), X) -> X,
                    activate(X) -> X,
      activate(n__fib1(X1, X2)) -> fib1(activate(X1), activate(X2)),
       activate(n__add(X1, X2)) -> add(activate(X1), activate(X2))}
     SPSC:
      Simple Projection:
       pi(sel#) = 0
      Strict:
       {}
      Qed