YES
Time: 0.088300
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:
  DP:
   {           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)}
  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()}
  UR:
   {                          from X -> cons(X, n__from n__s X),
                              from X -> n__from X,
                          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(),
                             a(x, y) -> x,
                             a(x, y) -> y}
   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 -> s# activate X)
     (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> from# activate X)
     (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)
     (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> activate# XS)
     (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> sel#(N, activate XS))
     (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))
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__from X -> from# activate X)
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__from X -> activate# X)
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__s X -> activate# X)
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__s X -> s# activate X)
     (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))
     (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y))
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__from X -> from# activate X)
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__from X -> activate# X)
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__s X -> s# 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))
     (activate# n__zWquot(X1, X2) -> zWquot#(activate X1, 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__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y))
     (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))
     (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__s X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__from X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X1)
     (activate# n__from X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X2)
     (activate# n__from X -> activate# X, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2))}
    STATUS:
     arrows: 0.769531
     SCCS (3):
      Scc:
       {sel#(s N, cons(X, XS)) -> sel#(N, activate XS)}
      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:
       {minus#(s X, s Y) -> minus#(X, Y)}
      
      SCC (1):
       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()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cons](x0, x1) = 0,
         
         [sel](x0, x1) = x0 + x1 + 1,
         
         [minus](x0, x1) = x0 + 1,
         
         [quot](x0, x1) = x0 + 1,
         
         [zWquot](x0, x1) = 0,
         
         [n__zWquot](x0, x1) = x0 + 1,
         
         [n__from](x0) = 0,
         
         [n__s](x0) = 0,
         
         [from](x0) = x0 + 1,
         
         [activate](x0) = 1,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [nil] = 0,
         
         [sel#](x0, x1) = x0
        Strict:
         sel#(s N, cons(X, XS)) -> sel#(N, activate XS)
         1 + 0X + 0XS + 1N >= 0 + 0XS + 1N
        Weak:
         zWquot(nil(), XS) -> nil()
         0 + 0XS >= 0
         zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS))
         0 + 0X + 0XS + 0Y + 0YS >= 0 + 0X + 0XS + 0Y + 0YS
         zWquot(X1, X2) -> n__zWquot(X1, X2)
         0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
         zWquot(XS, nil()) -> nil()
         0 + 0XS >= 0
         quot(s X, s Y) -> s quot(minus(X, Y), s Y)
         2 + 0X + 1Y >= 3 + 0X + 1Y
         quot(0(), s Y) -> 0()
         2 + 1Y >= 1
         minus(s X, s Y) -> minus(X, Y)
         2 + 0X + 1Y >= 1 + 0X + 1Y
         minus(X, 0()) -> 0()
         2 + 0X >= 1
         s X -> n__s X
         1 + 1X >= 0 + 0X
         activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2)
         1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
         activate n__s X -> s activate X
         1 + 0X >= 2 + 0X
         activate n__from X -> from activate X
         1 + 0X >= 2 + 0X
         activate X -> X
         1 + 0X >= 1X
         sel(s N, cons(X, XS)) -> sel(N, activate XS)
         2 + 0X + 0XS + 1N >= 2 + 0XS + 1N
         sel(0(), cons(X, XS)) -> X
         2 + 0X + 0XS >= 1X
         from X -> n__from X
         1 + 1X >= 0 + 0X
         from X -> cons(X, n__from n__s X)
         1 + 1X >= 0 + 0X
       Qed
     
     SCC (7):
      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:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [cons](x0, x1) = x0,
        
        [sel](x0, x1) = 0,
        
        [minus](x0, x1) = x0 + 1,
        
        [quot](x0, x1) = 0,
        
        [zWquot](x0, x1) = x0 + x1 + 1,
        
        [n__zWquot](x0, x1) = x0 + x1 + 1,
        
        [n__from](x0) = x0,
        
        [n__s](x0) = x0,
        
        [from](x0) = x0,
        
        [activate](x0) = x0,
        
        [s](x0) = x0,
        
        [0] = 1,
        
        [nil] = 0,
        
        [zWquot#](x0, x1) = x0 + x1 + 1,
        
        [activate#](x0) = x0
       Strict:
        zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS
        1 + 0X + 1XS + 0Y + 1YS >= 0 + 1YS
        zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS
        1 + 0X + 1XS + 0Y + 1YS >= 0 + 1XS
        activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2)
        1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
        activate# n__zWquot(X1, X2) -> activate# X2
        1 + 1X1 + 1X2 >= 0 + 1X2
        activate# n__zWquot(X1, X2) -> activate# X1
        1 + 1X1 + 1X2 >= 0 + 1X1
        activate# n__s X -> activate# X
        0 + 1X >= 0 + 1X
        activate# n__from X -> activate# X
        0 + 1X >= 0 + 1X
       Weak:
        zWquot(nil(), XS) -> nil()
        1 + 1XS >= 0
        zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS))
        1 + 0X + 1XS + 0Y + 1YS >= 1 + 0X + 1XS + 0Y + 1YS
        zWquot(X1, X2) -> n__zWquot(X1, X2)
        1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
        zWquot(XS, nil()) -> nil()
        1 + 1XS >= 0
        quot(s X, s Y) -> s quot(minus(X, Y), s Y)
        0 + 0X + 0Y >= 0 + 0X + 0Y
        quot(0(), s Y) -> 0()
        0 + 0Y >= 1
        minus(s X, s Y) -> minus(X, Y)
        1 + 0X + 1Y >= 1 + 0X + 1Y
        minus(X, 0()) -> 0()
        2 + 0X >= 1
        s X -> n__s X
        0 + 1X >= 0 + 1X
        activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2)
        1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
        activate n__s X -> s activate X
        0 + 1X >= 0 + 1X
        activate n__from X -> from activate X
        0 + 1X >= 0 + 1X
        activate X -> X
        0 + 1X >= 1X
        sel(s N, cons(X, XS)) -> sel(N, activate XS)
        0 + 0X + 0XS + 0N >= 0 + 0XS + 0N
        sel(0(), cons(X, XS)) -> X
        0 + 0X + 0XS >= 1X
        from X -> n__from X
        0 + 1X >= 0 + 1X
        from X -> cons(X, n__from n__s X)
        0 + 1X >= 0 + 1X
      SCCS (1):
       Scc:
        {activate# n__from X -> activate# X,
            activate# n__s X -> activate# X}
       
       SCC (2):
        Strict:
         {activate# n__from X -> activate# X,
             activate# n__s X -> activate# X}
        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:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [cons](x0, x1) = 0,
          
          [sel](x0, x1) = x0 + x1 + 1,
          
          [minus](x0, x1) = x0 + 1,
          
          [quot](x0, x1) = x0 + 1,
          
          [zWquot](x0, x1) = 0,
          
          [n__zWquot](x0, x1) = x0 + 1,
          
          [n__from](x0) = x0,
          
          [n__s](x0) = x0 + 1,
          
          [from](x0) = x0 + 1,
          
          [activate](x0) = 1,
          
          [s](x0) = 1,
          
          [0] = 1,
          
          [nil] = 0,
          
          [activate#](x0) = x0
         Strict:
          activate# n__s X -> activate# X
          1 + 1X >= 0 + 1X
          activate# n__from X -> activate# X
          0 + 1X >= 0 + 1X
         Weak:
          zWquot(nil(), XS) -> nil()
          0 + 0XS >= 0
          zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS))
          0 + 0X + 0XS + 0Y + 0YS >= 0 + 0X + 0XS + 0Y + 0YS
          zWquot(X1, X2) -> n__zWquot(X1, X2)
          0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
          zWquot(XS, nil()) -> nil()
          0 + 0XS >= 0
          quot(s X, s Y) -> s quot(minus(X, Y), s Y)
          2 + 0X + 0Y >= 1 + 0X + 0Y
          quot(0(), s Y) -> 0()
          2 + 0Y >= 1
          minus(s X, s Y) -> minus(X, Y)
          2 + 0X + 0Y >= 1 + 0X + 1Y
          minus(X, 0()) -> 0()
          2 + 0X >= 1
          s X -> n__s X
          1 + 0X >= 1 + 1X
          activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2)
          1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
          activate n__s X -> s activate X
          1 + 0X >= 1 + 0X
          activate n__from X -> from activate X
          1 + 0X >= 2 + 0X
          activate X -> X
          1 + 0X >= 1X
          sel(s N, cons(X, XS)) -> sel(N, activate XS)
          2 + 0X + 0XS + 0N >= 2 + 0XS + 1N
          sel(0(), cons(X, XS)) -> X
          2 + 0X + 0XS >= 1X
          from X -> n__from X
          1 + 1X >= 0 + 1X
          from X -> cons(X, n__from n__s X)
          1 + 1X >= 0 + 0X
        SCCS (1):
         Scc:
          {activate# n__from X -> activate# X}
         
         SCC (1):
          Strict:
           {activate# n__from X -> activate# X}
          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:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [cons](x0, x1) = 0,
            
            [sel](x0, x1) = x0 + x1 + 1,
            
            [minus](x0, x1) = x0 + 1,
            
            [quot](x0, x1) = x0 + 1,
            
            [zWquot](x0, x1) = 0,
            
            [n__zWquot](x0, x1) = x0 + 1,
            
            [n__from](x0) = x0 + 1,
            
            [n__s](x0) = 1,
            
            [from](x0) = x0 + 1,
            
            [activate](x0) = 1,
            
            [s](x0) = 1,
            
            [0] = 1,
            
            [nil] = 0,
            
            [activate#](x0) = x0
           Strict:
            activate# n__from X -> activate# X
            1 + 1X >= 0 + 1X
           Weak:
            zWquot(nil(), XS) -> nil()
            0 + 0XS >= 0
            zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS))
            0 + 0X + 0XS + 0Y + 0YS >= 0 + 0X + 0XS + 0Y + 0YS
            zWquot(X1, X2) -> n__zWquot(X1, X2)
            0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
            zWquot(XS, nil()) -> nil()
            0 + 0XS >= 0
            quot(s X, s Y) -> s quot(minus(X, Y), s Y)
            2 + 0X + 0Y >= 1 + 0X + 0Y
            quot(0(), s Y) -> 0()
            2 + 0Y >= 1
            minus(s X, s Y) -> minus(X, Y)
            2 + 0X + 0Y >= 1 + 0X + 1Y
            minus(X, 0()) -> 0()
            2 + 0X >= 1
            s X -> n__s X
            1 + 0X >= 1 + 0X
            activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2)
            1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
            activate n__s X -> s activate X
            1 + 0X >= 1 + 0X
            activate n__from X -> from activate X
            1 + 0X >= 2 + 0X
            activate X -> X
            1 + 0X >= 1X
            sel(s N, cons(X, XS)) -> sel(N, activate XS)
            2 + 0X + 0XS + 0N >= 2 + 0XS + 1N
            sel(0(), cons(X, XS)) -> X
            2 + 0X + 0XS >= 1X
            from X -> n__from X
            1 + 1X >= 1 + 1X
            from X -> cons(X, n__from n__s X)
            1 + 1X >= 0 + 0X
          Qed
      
    
    
    
    SCC (1):
     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()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [cons](x0, x1) = 1,
       
       [sel](x0, x1) = x0 + 1,
       
       [minus](x0, x1) = x0 + 1,
       
       [quot](x0, x1) = x0 + 1,
       
       [zWquot](x0, x1) = 0,
       
       [n__zWquot](x0, x1) = x0 + 1,
       
       [n__from](x0) = x0 + 1,
       
       [n__s](x0) = 1,
       
       [from](x0) = x0 + 1,
       
       [activate](x0) = 1,
       
       [s](x0) = x0 + 1,
       
       [0] = 1,
       
       [nil] = 0,
       
       [minus#](x0, x1) = x0
      Strict:
       minus#(s X, s Y) -> minus#(X, Y)
       1 + 0X + 1Y >= 0 + 0X + 1Y
      Weak:
       zWquot(nil(), XS) -> nil()
       0 + 0XS >= 0
       zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS))
       0 + 0X + 0XS + 0Y + 0YS >= 1 + 0X + 0XS + 0Y + 0YS
       zWquot(X1, X2) -> n__zWquot(X1, X2)
       0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2
       zWquot(XS, nil()) -> nil()
       0 + 0XS >= 0
       quot(s X, s Y) -> s quot(minus(X, Y), s Y)
       2 + 0X + 1Y >= 3 + 0X + 1Y
       quot(0(), s Y) -> 0()
       2 + 1Y >= 1
       minus(s X, s Y) -> minus(X, Y)
       2 + 0X + 1Y >= 1 + 0X + 1Y
       minus(X, 0()) -> 0()
       2 + 0X >= 1
       s X -> n__s X
       1 + 1X >= 1 + 0X
       activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2)
       1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
       activate n__s X -> s activate X
       1 + 0X >= 2 + 0X
       activate n__from X -> from activate X
       1 + 0X >= 2 + 0X
       activate X -> X
       1 + 0X >= 1X
       sel(s N, cons(X, XS)) -> sel(N, activate XS)
       2 + 0X + 0XS + 0N >= 2 + 0XS + 0N
       sel(0(), cons(X, XS)) -> X
       2 + 0X + 0XS >= 1X
       from X -> n__from X
       1 + 1X >= 1 + 1X
       from X -> cons(X, n__from n__s X)
       1 + 1X >= 1 + 0X
     Qed