YES
TRS:
 {                         from(X) -> cons(X, n__from(n__s(X))),
                           from(X) -> n__from(X),
             sel(0(), cons(X, XS)) -> X,
            sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                       activate(X) -> X,
              activate(n__from(X)) -> from(activate(X)),
                 activate(n__s(X)) -> s(activate(X)),
       activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                              s(X) -> n__s(X),
                     minus(X, 0()) -> 0(),
                 minus(s(X), s(Y)) -> minus(X, Y),
                   quot(0(), s(Y)) -> 0(),
                  quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                 zWquot(XS, nil()) -> nil(),
                    zWquot(X1, X2) -> n__zWquot(X1, X2),
  zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                 zWquot(nil(), XS) -> nil()}
 DP:
  Strict:
   {          sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS)),
              sel#(s(N), cons(X, XS)) -> activate#(XS),
                activate#(n__from(X)) -> from#(activate(X)),
                activate#(n__from(X)) -> activate#(X),
                   activate#(n__s(X)) -> activate#(X),
                   activate#(n__s(X)) -> s#(activate(X)),
         activate#(n__zWquot(X1, X2)) -> activate#(X1),
         activate#(n__zWquot(X1, X2)) -> activate#(X2),
         activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)),
                   minus#(s(X), s(Y)) -> minus#(X, Y),
                    quot#(s(X), s(Y)) -> s#(quot(minus(X, Y), s(Y))),
                    quot#(s(X), s(Y)) -> minus#(X, Y),
                    quot#(s(X), s(Y)) -> quot#(minus(X, Y), s(Y)),
    zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
    zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS),
    zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)}
  Weak:
  {                         from(X) -> cons(X, n__from(n__s(X))),
                            from(X) -> n__from(X),
              sel(0(), cons(X, XS)) -> X,
             sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                        activate(X) -> X,
               activate(n__from(X)) -> from(activate(X)),
                  activate(n__s(X)) -> s(activate(X)),
        activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                               s(X) -> n__s(X),
                      minus(X, 0()) -> 0(),
                  minus(s(X), s(Y)) -> minus(X, Y),
                    quot(0(), s(Y)) -> 0(),
                   quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                  zWquot(XS, nil()) -> nil(),
                     zWquot(X1, X2) -> n__zWquot(X1, X2),
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                  zWquot(nil(), XS) -> nil()}
  EDG:
   {(sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> activate#(X2))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> activate#(X1))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__s(X)) -> s#(activate(X)))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__s(X)) -> activate#(X))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> activate#(X))
    (sel#(s(N), cons(X, XS)) -> activate#(XS), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
    (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__zWquot(X1, X2)) -> activate#(X2))
    (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__zWquot(X1, X2)) -> activate#(X1))
    (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X))
    (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> activate#(X))
    (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)), zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y))
    (activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)), zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS))
    (activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)), zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS))
    (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
    (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__zWquot(X1, X2)) -> activate#(X2))
    (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__zWquot(X1, X2)) -> activate#(X1))
    (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> activate#(X))
    (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__from(X)) -> activate#(X))
    (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__from(X)) -> activate#(X), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
    (activate#(n__from(X)) -> activate#(X), activate#(n__zWquot(X1, X2)) -> activate#(X2))
    (activate#(n__from(X)) -> activate#(X), activate#(n__zWquot(X1, X2)) -> activate#(X1))
    (activate#(n__from(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__from(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__from(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
    (activate#(n__from(X)) -> activate#(X), activate#(n__from(X)) -> from#(activate(X)))
    (minus#(s(X), s(Y)) -> minus#(X, Y), minus#(s(X), s(Y)) -> minus#(X, Y))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(s(X), s(Y)) -> quot#(minus(X, Y), s(Y)))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(s(X), s(Y)) -> minus#(X, Y))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(s(X), s(Y)) -> s#(quot(minus(X, Y), s(Y))))
    (quot#(s(X), s(Y)) -> minus#(X, Y), minus#(s(X), s(Y)) -> minus#(X, Y))
    (activate#(n__s(X)) -> activate#(X), activate#(n__from(X)) -> from#(activate(X)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__from(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
    (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> s#(activate(X)))
    (activate#(n__s(X)) -> activate#(X), activate#(n__zWquot(X1, X2)) -> activate#(X1))
    (activate#(n__s(X)) -> activate#(X), activate#(n__zWquot(X1, X2)) -> activate#(X2))
    (activate#(n__s(X)) -> activate#(X), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
    (quot#(s(X), s(Y)) -> quot#(minus(X, Y), s(Y)), quot#(s(X), s(Y)) -> s#(quot(minus(X, Y), s(Y))))
    (quot#(s(X), s(Y)) -> quot#(minus(X, Y), s(Y)), quot#(s(X), s(Y)) -> minus#(X, Y))
    (quot#(s(X), s(Y)) -> quot#(minus(X, Y), s(Y)), quot#(s(X), s(Y)) -> quot#(minus(X, Y), s(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))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__from(X)) -> from#(activate(X)))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__from(X)) -> activate#(X))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__s(X)) -> activate#(X))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__s(X)) -> s#(activate(X)))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> activate#(X1))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> activate#(X2))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__from(X)) -> from#(activate(X)))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__from(X)) -> activate#(X))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__s(X)) -> activate#(X))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__s(X)) -> s#(activate(X)))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__zWquot(X1, X2)) -> activate#(X1))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__zWquot(X1, X2)) -> activate#(X2))
    (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))}
   SCCS:
    Scc:
     {quot#(s(X), s(Y)) -> quot#(minus(X, Y), s(Y))}
    Scc:
     {minus#(s(X), s(Y)) -> minus#(X, Y)}
    Scc:
     {            activate#(n__from(X)) -> activate#(X),
                     activate#(n__s(X)) -> activate#(X),
           activate#(n__zWquot(X1, X2)) -> activate#(X1),
           activate#(n__zWquot(X1, X2)) -> activate#(X2),
           activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)),
      zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
      zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)}
    Scc:
     {sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS))}
    SCC:
     Strict:
      {quot#(s(X), s(Y)) -> quot#(minus(X, Y), s(Y))}
     Weak:
     {                         from(X) -> cons(X, n__from(n__s(X))),
                               from(X) -> n__from(X),
                 sel(0(), cons(X, XS)) -> X,
                sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                           activate(X) -> X,
                  activate(n__from(X)) -> from(activate(X)),
                     activate(n__s(X)) -> s(activate(X)),
           activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                  s(X) -> n__s(X),
                         minus(X, 0()) -> 0(),
                     minus(s(X), s(Y)) -> minus(X, Y),
                       quot(0(), s(Y)) -> 0(),
                      quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                     zWquot(XS, nil()) -> nil(),
                        zWquot(X1, X2) -> n__zWquot(X1, X2),
      zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                     zWquot(nil(), XS) -> nil()}
     POLY:
      Argument Filtering:
       pi(n__zWquot) = [], pi(zWquot) = [], pi(nil) = [], pi(quot#) = 0, pi(quot) = [], pi(minus) = [], pi(s) = [], pi(activate) = [], pi(0) = [], pi(sel) = [], pi(from) = [], pi(n__s) = [], pi(n__from) = [], pi(cons) = []
      Usable Rules:
       {}
      Interpretation:
       [minus] = 0,
       [s] = 1
      Strict:
       {}
      Weak:
       {                         from(X) -> cons(X, n__from(n__s(X))),
                                 from(X) -> n__from(X),
                   sel(0(), cons(X, XS)) -> X,
                  sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                             activate(X) -> X,
                    activate(n__from(X)) -> from(activate(X)),
                       activate(n__s(X)) -> s(activate(X)),
             activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                    s(X) -> n__s(X),
                           minus(X, 0()) -> 0(),
                       minus(s(X), s(Y)) -> minus(X, Y),
                         quot(0(), s(Y)) -> 0(),
                        quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                       zWquot(XS, nil()) -> nil(),
                          zWquot(X1, X2) -> n__zWquot(X1, X2),
        zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                       zWquot(nil(), XS) -> nil()}
      Qed
    SCC:
     Strict:
      {minus#(s(X), s(Y)) -> minus#(X, Y)}
     Weak:
     {                         from(X) -> cons(X, n__from(n__s(X))),
                               from(X) -> n__from(X),
                 sel(0(), cons(X, XS)) -> X,
                sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                           activate(X) -> X,
                  activate(n__from(X)) -> from(activate(X)),
                     activate(n__s(X)) -> s(activate(X)),
           activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                  s(X) -> n__s(X),
                         minus(X, 0()) -> 0(),
                     minus(s(X), s(Y)) -> minus(X, Y),
                       quot(0(), s(Y)) -> 0(),
                      quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                     zWquot(XS, nil()) -> nil(),
                        zWquot(X1, X2) -> n__zWquot(X1, X2),
      zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                     zWquot(nil(), XS) -> nil()}
     SPSC:
      Simple Projection:
       pi(minus#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {            activate#(n__from(X)) -> activate#(X),
                      activate#(n__s(X)) -> activate#(X),
            activate#(n__zWquot(X1, X2)) -> activate#(X1),
            activate#(n__zWquot(X1, X2)) -> activate#(X2),
            activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)),
       zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
       zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)}
     Weak:
     {                         from(X) -> cons(X, n__from(n__s(X))),
                               from(X) -> n__from(X),
                 sel(0(), cons(X, XS)) -> X,
                sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                           activate(X) -> X,
                  activate(n__from(X)) -> from(activate(X)),
                     activate(n__s(X)) -> s(activate(X)),
           activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                  s(X) -> n__s(X),
                         minus(X, 0()) -> 0(),
                     minus(s(X), s(Y)) -> minus(X, Y),
                       quot(0(), s(Y)) -> 0(),
                      quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                     zWquot(XS, nil()) -> nil(),
                        zWquot(X1, X2) -> n__zWquot(X1, X2),
      zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                     zWquot(nil(), XS) -> nil()}
     POLY:
      Argument Filtering:
       pi(n__zWquot) = [0,1], pi(zWquot#) = [0,1], pi(zWquot) = [0,1], pi(nil) = [], pi(quot) = [], pi(minus) = [], pi(s) = 0, pi(activate#) = [0], pi(activate) = 0, pi(0) = [], pi(sel) = [], pi(from) = [0], pi(n__s) = 0, pi(n__from) = [0], pi(cons) = 1
      Usable Rules:
       {}
      Interpretation:
       [zWquot#](x0, x1) = x0 + x1 + 1,
       [activate#](x0) = x0 + 1,
       [n__zWquot](x0, x1) = x0 + x1,
       [n__from](x0) = x0 + 1
      Strict:
       {               activate#(n__s(X)) -> activate#(X),
             activate#(n__zWquot(X1, X2)) -> activate#(X1),
             activate#(n__zWquot(X1, X2)) -> activate#(X2),
             activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)),
        zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
        zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)}
      Weak:
       {                         from(X) -> cons(X, n__from(n__s(X))),
                                 from(X) -> n__from(X),
                   sel(0(), cons(X, XS)) -> X,
                  sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                             activate(X) -> X,
                    activate(n__from(X)) -> from(activate(X)),
                       activate(n__s(X)) -> s(activate(X)),
             activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                    s(X) -> n__s(X),
                           minus(X, 0()) -> 0(),
                       minus(s(X), s(Y)) -> minus(X, Y),
                         quot(0(), s(Y)) -> 0(),
                        quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                       zWquot(XS, nil()) -> nil(),
                          zWquot(X1, X2) -> n__zWquot(X1, X2),
        zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                       zWquot(nil(), XS) -> nil()}
      EDG:
       {(activate#(n__s(X)) -> activate#(X), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
        (activate#(n__s(X)) -> activate#(X), activate#(n__zWquot(X1, X2)) -> activate#(X2))
        (activate#(n__s(X)) -> activate#(X), activate#(n__zWquot(X1, X2)) -> activate#(X1))
        (activate#(n__s(X)) -> activate#(X), activate#(n__s(X)) -> activate#(X))
        (activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)), zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS))
        (activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)), zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS))
        (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
        (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__zWquot(X1, X2)) -> activate#(X2))
        (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__zWquot(X1, X2)) -> activate#(X1))
        (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> activate#(X))
        (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__s(X)) -> activate#(X))
        (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> activate#(X1))
        (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> activate#(X2))
        (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
        (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> activate#(X))
        (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__zWquot(X1, X2)) -> activate#(X1))
        (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__zWquot(X1, X2)) -> activate#(X2))
        (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
        (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__s(X)) -> activate#(X))
        (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__zWquot(X1, X2)) -> activate#(X1))
        (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__zWquot(X1, X2)) -> activate#(X2))
        (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))}
       SCCS:
        Scc:
         {               activate#(n__s(X)) -> activate#(X),
               activate#(n__zWquot(X1, X2)) -> activate#(X1),
               activate#(n__zWquot(X1, X2)) -> activate#(X2),
               activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)),
          zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
          zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)}
        SCC:
         Strict:
          {               activate#(n__s(X)) -> activate#(X),
                activate#(n__zWquot(X1, X2)) -> activate#(X1),
                activate#(n__zWquot(X1, X2)) -> activate#(X2),
                activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)),
           zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
           zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)}
         Weak:
         {                         from(X) -> cons(X, n__from(n__s(X))),
                                   from(X) -> n__from(X),
                     sel(0(), cons(X, XS)) -> X,
                    sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                               activate(X) -> X,
                      activate(n__from(X)) -> from(activate(X)),
                         activate(n__s(X)) -> s(activate(X)),
               activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                      s(X) -> n__s(X),
                             minus(X, 0()) -> 0(),
                         minus(s(X), s(Y)) -> minus(X, Y),
                           quot(0(), s(Y)) -> 0(),
                          quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                         zWquot(XS, nil()) -> nil(),
                            zWquot(X1, X2) -> n__zWquot(X1, X2),
          zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                         zWquot(nil(), XS) -> nil()}
         POLY:
          Argument Filtering:
           pi(n__zWquot) = [0,1], pi(zWquot#) = [0,1], pi(zWquot) = [0,1], pi(nil) = [], pi(quot) = [], pi(minus) = [], pi(s) = [0], pi(activate#) = 0, pi(activate) = 0, pi(0) = [], pi(sel) = [], pi(from) = [], pi(n__s) = [0], pi(n__from) = [], pi(cons) = 1
          Usable Rules:
           {}
          Interpretation:
           [zWquot#](x0, x1) = x0 + x1,
           [n__zWquot](x0, x1) = x0 + x1,
           [n__s](x0) = x0 + 1
          Strict:
           {     activate#(n__zWquot(X1, X2)) -> activate#(X1),
                 activate#(n__zWquot(X1, X2)) -> activate#(X2),
                 activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)),
            zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
            zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)}
          Weak:
           {                         from(X) -> cons(X, n__from(n__s(X))),
                                     from(X) -> n__from(X),
                       sel(0(), cons(X, XS)) -> X,
                      sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                                 activate(X) -> X,
                        activate(n__from(X)) -> from(activate(X)),
                           activate(n__s(X)) -> s(activate(X)),
                 activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                        s(X) -> n__s(X),
                               minus(X, 0()) -> 0(),
                           minus(s(X), s(Y)) -> minus(X, Y),
                             quot(0(), s(Y)) -> 0(),
                            quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                           zWquot(XS, nil()) -> nil(),
                              zWquot(X1, X2) -> n__zWquot(X1, X2),
            zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                           zWquot(nil(), XS) -> nil()}
          EDG:
           {(zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
            (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__zWquot(X1, X2)) -> activate#(X2))
            (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS), activate#(n__zWquot(X1, X2)) -> activate#(X1))
            (activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)), zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS))
            (activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)), zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS))
            (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__zWquot(X1, X2)) -> activate#(X1))
            (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__zWquot(X1, X2)) -> activate#(X2))
            (activate#(n__zWquot(X1, X2)) -> activate#(X2), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
            (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__zWquot(X1, X2)) -> activate#(X1))
            (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__zWquot(X1, X2)) -> activate#(X2))
            (activate#(n__zWquot(X1, X2)) -> activate#(X1), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))
            (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> activate#(X1))
            (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> activate#(X2))
            (zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS), activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)))}
           SCCS:
            Scc:
             {     activate#(n__zWquot(X1, X2)) -> activate#(X1),
                   activate#(n__zWquot(X1, X2)) -> activate#(X2),
                   activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)),
              zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
              zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)}
            SCC:
             Strict:
              {     activate#(n__zWquot(X1, X2)) -> activate#(X1),
                    activate#(n__zWquot(X1, X2)) -> activate#(X2),
                    activate#(n__zWquot(X1, X2)) -> zWquot#(activate(X1), activate(X2)),
               zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
               zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)}
             Weak:
             {                         from(X) -> cons(X, n__from(n__s(X))),
                                       from(X) -> n__from(X),
                         sel(0(), cons(X, XS)) -> X,
                        sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                                   activate(X) -> X,
                          activate(n__from(X)) -> from(activate(X)),
                             activate(n__s(X)) -> s(activate(X)),
                   activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                          s(X) -> n__s(X),
                                 minus(X, 0()) -> 0(),
                             minus(s(X), s(Y)) -> minus(X, Y),
                               quot(0(), s(Y)) -> 0(),
                              quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                             zWquot(XS, nil()) -> nil(),
                                zWquot(X1, X2) -> n__zWquot(X1, X2),
              zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                             zWquot(nil(), XS) -> nil()}
             POLY:
              Argument Filtering:
               pi(n__zWquot) = [0,1], pi(zWquot#) = [0,1], pi(zWquot) = [0,1], pi(nil) = [], pi(quot) = [], pi(minus) = [], pi(s) = [], pi(activate#) = 0, pi(activate) = 0, pi(0) = [], pi(sel) = [], pi(from) = [], pi(n__s) = [], pi(n__from) = [], pi(cons) = 1
              Usable Rules:
               {}
              Interpretation:
               [zWquot#](x0, x1) = x0 + x1,
               [n__zWquot](x0, x1) = x0 + x1 + 1
              Strict:
               {zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(XS),
                zWquot#(cons(X, XS), cons(Y, YS)) -> activate#(YS)}
              Weak:
               {                         from(X) -> cons(X, n__from(n__s(X))),
                                         from(X) -> n__from(X),
                           sel(0(), cons(X, XS)) -> X,
                          sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                                     activate(X) -> X,
                            activate(n__from(X)) -> from(activate(X)),
                               activate(n__s(X)) -> s(activate(X)),
                     activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                            s(X) -> n__s(X),
                                   minus(X, 0()) -> 0(),
                               minus(s(X), s(Y)) -> minus(X, Y),
                                 quot(0(), s(Y)) -> 0(),
                                quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                               zWquot(XS, nil()) -> nil(),
                                  zWquot(X1, X2) -> n__zWquot(X1, X2),
                zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                               zWquot(nil(), XS) -> nil()}
              EDG:
               {}
               SCCS:
                
                Qed
    SCC:
     Strict:
      {sel#(s(N), cons(X, XS)) -> sel#(N, activate(XS))}
     Weak:
     {                         from(X) -> cons(X, n__from(n__s(X))),
                               from(X) -> n__from(X),
                 sel(0(), cons(X, XS)) -> X,
                sel(s(N), cons(X, XS)) -> sel(N, activate(XS)),
                           activate(X) -> X,
                  activate(n__from(X)) -> from(activate(X)),
                     activate(n__s(X)) -> s(activate(X)),
           activate(n__zWquot(X1, X2)) -> zWquot(activate(X1), activate(X2)),
                                  s(X) -> n__s(X),
                         minus(X, 0()) -> 0(),
                     minus(s(X), s(Y)) -> minus(X, Y),
                       quot(0(), s(Y)) -> 0(),
                      quot(s(X), s(Y)) -> s(quot(minus(X, Y), s(Y))),
                     zWquot(XS, nil()) -> nil(),
                        zWquot(X1, X2) -> n__zWquot(X1, X2),
      zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate(XS), activate(YS))),
                     zWquot(nil(), XS) -> nil()}
     SPSC:
      Simple Projection:
       pi(sel#) = 0
      Strict:
       {}
      Qed