YES
TRS:
 {               activate(X) -> X,
    activate(n__add(X1, X2)) -> add(X1, X2),
  activate(n__first(X1, X2)) -> first(X1, X2),
        activate(n__from(X)) -> from(X),
           activate(n__s(X)) -> s(X),
              and(true(), X) -> activate(X),
             and(false(), Y) -> false(),
            if(true(), X, Y) -> activate(X),
           if(false(), X, Y) -> activate(Y),
                 add(X1, X2) -> n__add(X1, X2),
                 add(0(), X) -> activate(X),
                add(s(X), Y) -> s(n__add(activate(X), activate(Y))),
                        s(X) -> n__s(X),
               first(X1, X2) -> n__first(X1, X2),
               first(0(), X) -> nil(),
     first(s(X), cons(Y, Z)) -> cons(activate(Y), n__first(activate(X), activate(Z))),
                     from(X) -> cons(activate(X), n__from(n__s(activate(X)))),
                     from(X) -> n__from(X)}
 DP:
  Strict:
   {  activate#(n__add(X1, X2)) -> add#(X1, X2),
    activate#(n__first(X1, X2)) -> first#(X1, X2),
          activate#(n__from(X)) -> from#(X),
             activate#(n__s(X)) -> s#(X),
                and#(true(), X) -> activate#(X),
              if#(true(), X, Y) -> activate#(X),
             if#(false(), X, Y) -> activate#(Y),
                   add#(0(), X) -> activate#(X),
                  add#(s(X), Y) -> activate#(X),
                  add#(s(X), Y) -> activate#(Y),
                  add#(s(X), Y) -> s#(n__add(activate(X), activate(Y))),
       first#(s(X), cons(Y, Z)) -> activate#(X),
       first#(s(X), cons(Y, Z)) -> activate#(Y),
       first#(s(X), cons(Y, Z)) -> activate#(Z),
                       from#(X) -> activate#(X)}
  Weak:
  {               activate(X) -> X,
     activate(n__add(X1, X2)) -> add(X1, X2),
   activate(n__first(X1, X2)) -> first(X1, X2),
         activate(n__from(X)) -> from(X),
            activate(n__s(X)) -> s(X),
               and(true(), X) -> activate(X),
              and(false(), Y) -> false(),
             if(true(), X, Y) -> activate(X),
            if(false(), X, Y) -> activate(Y),
                  add(X1, X2) -> n__add(X1, X2),
                  add(0(), X) -> activate(X),
                 add(s(X), Y) -> s(n__add(activate(X), activate(Y))),
                         s(X) -> n__s(X),
                first(X1, X2) -> n__first(X1, X2),
                first(0(), X) -> nil(),
      first(s(X), cons(Y, Z)) -> cons(activate(Y), n__first(activate(X), activate(Z))),
                      from(X) -> cons(activate(X), n__from(n__s(activate(X)))),
                      from(X) -> n__from(X)}
  EDG:
   {(activate#(n__from(X)) -> from#(X), from#(X) -> activate#(X))
    (and#(true(), X) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (and#(true(), X) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (and#(true(), X) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (and#(true(), X) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (add#(0(), X) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (add#(0(), X) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (add#(0(), X) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (add#(0(), X) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (first#(s(X), cons(Y, Z)) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (activate#(n__add(X1, X2)) -> add#(X1, X2), add#(s(X), Y) -> s#(n__add(activate(X), activate(Y))))
    (activate#(n__add(X1, X2)) -> add#(X1, X2), add#(s(X), Y) -> activate#(Y))
    (activate#(n__add(X1, X2)) -> add#(X1, X2), add#(s(X), Y) -> activate#(X))
    (activate#(n__add(X1, X2)) -> add#(X1, X2), add#(0(), X) -> activate#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__from(X)) -> from#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__from(X)) -> from#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (first#(s(X), cons(Y, Z)) -> activate#(Y), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (add#(s(X), Y) -> activate#(Y), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (add#(s(X), Y) -> activate#(Y), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (add#(s(X), Y) -> activate#(Y), activate#(n__from(X)) -> from#(X))
    (add#(s(X), Y) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(X))
    (activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(Y))
    (activate#(n__first(X1, X2)) -> first#(X1, X2), first#(s(X), cons(Y, Z)) -> activate#(Z))
    (from#(X) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (from#(X) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (from#(X) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (from#(X) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (add#(s(X), Y) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (add#(s(X), Y) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (add#(s(X), Y) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (add#(s(X), Y) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (if#(true(), X, Y) -> activate#(X), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (if#(true(), X, Y) -> activate#(X), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (if#(true(), X, Y) -> activate#(X), activate#(n__from(X)) -> from#(X))
    (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__add(X1, X2)) -> add#(X1, X2))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__first(X1, X2)) -> first#(X1, X2))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__from(X)) -> from#(X))
    (first#(s(X), cons(Y, Z)) -> activate#(Z), activate#(n__s(X)) -> s#(X))}
   SCCS:
    Scc:
     {  activate#(n__add(X1, X2)) -> add#(X1, X2),
      activate#(n__first(X1, X2)) -> first#(X1, X2),
            activate#(n__from(X)) -> from#(X),
                     add#(0(), X) -> activate#(X),
                    add#(s(X), Y) -> activate#(X),
                    add#(s(X), Y) -> activate#(Y),
         first#(s(X), cons(Y, Z)) -> activate#(X),
         first#(s(X), cons(Y, Z)) -> activate#(Y),
         first#(s(X), cons(Y, Z)) -> activate#(Z),
                         from#(X) -> activate#(X)}
    SCC:
     Strict:
      {  activate#(n__add(X1, X2)) -> add#(X1, X2),
       activate#(n__first(X1, X2)) -> first#(X1, X2),
             activate#(n__from(X)) -> from#(X),
                      add#(0(), X) -> activate#(X),
                     add#(s(X), Y) -> activate#(X),
                     add#(s(X), Y) -> activate#(Y),
          first#(s(X), cons(Y, Z)) -> activate#(X),
          first#(s(X), cons(Y, Z)) -> activate#(Y),
          first#(s(X), cons(Y, Z)) -> activate#(Z),
                          from#(X) -> activate#(X)}
     Weak:
     {               activate(X) -> X,
        activate(n__add(X1, X2)) -> add(X1, X2),
      activate(n__first(X1, X2)) -> first(X1, X2),
            activate(n__from(X)) -> from(X),
               activate(n__s(X)) -> s(X),
                  and(true(), X) -> activate(X),
                 and(false(), Y) -> false(),
                if(true(), X, Y) -> activate(X),
               if(false(), X, Y) -> activate(Y),
                     add(X1, X2) -> n__add(X1, X2),
                     add(0(), X) -> activate(X),
                    add(s(X), Y) -> s(n__add(activate(X), activate(Y))),
                            s(X) -> n__s(X),
                   first(X1, X2) -> n__first(X1, X2),
                   first(0(), X) -> nil(),
         first(s(X), cons(Y, Z)) -> cons(activate(Y), n__first(activate(X), activate(Z))),
                         from(X) -> cons(activate(X), n__from(n__s(activate(X)))),
                         from(X) -> n__from(X)}
     POLY:
      Argument Filtering:
       pi(from#) = [0], pi(from) = [], pi(n__s) = [], pi(n__from) = [0], pi(n__first) = [0,1], pi(cons) = [0,1], pi(first#) = [0,1], pi(first) = [], pi(nil) = [], pi(n__add) = [0,1], pi(s) = 0, pi(0) = [], pi(add#) = [0,1], pi(add) = [], pi(if) = [], pi(false) = [], pi(true) = [], pi(and) = [], pi(activate#) = [0], pi(activate) = []
      Usable Rules:
       {}
      Interpretation:
       [first#](x0, x1) = x0 + x1,
       [add#](x0, x1) = x0 + x1 + 1,
       [from#](x0) = x0 + 1,
       [activate#](x0) = x0 + 1,
       [n__first](x0, x1) = x0 + x1 + 1,
       [cons](x0, x1) = x0 + x1 + 1,
       [n__add](x0, x1) = x0 + x1 + 1,
       [n__from](x0) = x0 + 1,
       [0] = 0
      Strict:
       {            add#(0(), X) -> activate#(X),
                   add#(s(X), Y) -> activate#(X),
                   add#(s(X), Y) -> activate#(Y),
        first#(s(X), cons(Y, Z)) -> activate#(X),
        first#(s(X), cons(Y, Z)) -> activate#(Y),
        first#(s(X), cons(Y, Z)) -> activate#(Z),
                        from#(X) -> activate#(X)}
      Weak:
       {               activate(X) -> X,
          activate(n__add(X1, X2)) -> add(X1, X2),
        activate(n__first(X1, X2)) -> first(X1, X2),
              activate(n__from(X)) -> from(X),
                 activate(n__s(X)) -> s(X),
                    and(true(), X) -> activate(X),
                   and(false(), Y) -> false(),
                  if(true(), X, Y) -> activate(X),
                 if(false(), X, Y) -> activate(Y),
                       add(X1, X2) -> n__add(X1, X2),
                       add(0(), X) -> activate(X),
                      add(s(X), Y) -> s(n__add(activate(X), activate(Y))),
                              s(X) -> n__s(X),
                     first(X1, X2) -> n__first(X1, X2),
                     first(0(), X) -> nil(),
           first(s(X), cons(Y, Z)) -> cons(activate(Y), n__first(activate(X), activate(Z))),
                           from(X) -> cons(activate(X), n__from(n__s(activate(X)))),
                           from(X) -> n__from(X)}
      EDG:
       {}
       SCCS:
        
        Qed