YES
Time: 0.061217
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:
  DP:
   {   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}
  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}
  EDG:
   {(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__add(X1, X2) -> add#(X1, X2), add#(s X, Y) -> activate# 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)
    (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)}
   STATUS:
    arrows: 0.687500
    SCCS (1):
     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 (7):
      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:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [fst](x0, x1) = 0,
        
        [cons](x0, x1) = x0,
        
        [n__fst](x0, x1) = x0 + x1 + 1,
        
        [add](x0, x1) = 0,
        
        [n__add](x0, x1) = x0,
        
        [activate](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [n__from](x0) = 0,
        
        [from](x0) = 0,
        
        [len](x0) = 0,
        
        [n__len](x0) = x0,
        
        [nil] = 0,
        
        [0] = 0,
        
        [fst#](x0, x1) = x0 + x1 + 1,
        
        [add#](x0, x1) = x0,
        
        [activate#](x0) = x0,
        
        [len#](x0) = x0
       Strict:
        len# cons(X, Z) -> activate# Z
        0 + 1Z + 0X >= 0 + 1Z
        add#(s X, Y) -> activate# X
        1 + 0Y + 1X >= 0 + 1X
        activate# n__len X -> len# X
        0 + 1X >= 0 + 1X
        activate# n__add(X1, X2) -> add#(X1, X2)
        0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
        activate# n__fst(X1, X2) -> fst#(X1, X2)
        1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
        fst#(s X, cons(Y, Z)) -> activate# X
        2 + 1Z + 0Y + 1X >= 0 + 1X
        fst#(s X, cons(Y, Z)) -> activate# Z
        2 + 1Z + 0Y + 1X >= 0 + 1Z
       Weak:
        len cons(X, Z) -> s n__len activate Z
        0 + 0Z + 0X >= 1 + 0Z
        len nil() -> 0()
        0 >= 0
        len X -> n__len X
        0 + 0X >= 0 + 1X
        add(s X, Y) -> s n__add(activate X, Y)
        0 + 0Y + 0X >= 1 + 0Y + 0X
        add(0(), X) -> X
        0 + 0X >= 1X
        add(X1, X2) -> n__add(X1, X2)
        0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2
        from X -> n__from X
        0 + 0X >= 0 + 0X
        from X -> cons(X, n__from s X)
        0 + 0X >= 0 + 0X
        activate n__len X -> len X
        0 + 0X >= 0 + 0X
        activate n__add(X1, X2) -> add(X1, X2)
        0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
        activate n__from X -> from X
        0 + 0X >= 0 + 0X
        activate n__fst(X1, X2) -> fst(X1, X2)
        0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
        activate X -> X
        0 + 0X >= 1X
        fst(s X, cons(Y, Z)) -> cons(Y, n__fst(activate X, activate Z))
        0 + 0Z + 0Y + 0X >= 1 + 0Z + 0Y + 0X
        fst(0(), Z) -> nil()
        0 + 0Z >= 0
        fst(X1, X2) -> n__fst(X1, X2)
        0 + 0X1 + 0X2 >= 1 + 1X1 + 1X2
      SCCS (1):
       Scc:
        {activate# n__len X -> len# X,
            len# cons(X, Z) -> activate# Z}
       
       SCC (2):
        Strict:
         {activate# n__len X -> len# 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:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [fst](x0, x1) = x0 + x1 + 1,
          
          [cons](x0, x1) = x0 + 1,
          
          [n__fst](x0, x1) = x0 + 1,
          
          [add](x0, x1) = 0,
          
          [n__add](x0, x1) = x0 + 1,
          
          [activate](x0) = 1,
          
          [s](x0) = 0,
          
          [n__from](x0) = 0,
          
          [from](x0) = 0,
          
          [len](x0) = 0,
          
          [n__len](x0) = x0,
          
          [nil] = 0,
          
          [0] = 1,
          
          [activate#](x0) = x0,
          
          [len#](x0) = x0
         Strict:
          len# cons(X, Z) -> activate# Z
          1 + 1Z + 0X >= 0 + 1Z
          activate# n__len X -> len# X
          0 + 1X >= 0 + 1X
         Weak:
          len cons(X, Z) -> s n__len activate Z
          0 + 0Z + 0X >= 0 + 0Z
          len nil() -> 0()
          0 >= 1
          len X -> n__len X
          0 + 0X >= 0 + 1X
          add(s X, Y) -> s n__add(activate X, Y)
          0 + 0Y + 0X >= 0 + 0Y + 0X
          add(0(), X) -> X
          0 + 0X >= 1X
          add(X1, X2) -> n__add(X1, X2)
          0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2
          from X -> n__from X
          0 + 0X >= 0 + 0X
          from X -> cons(X, n__from s X)
          0 + 0X >= 1 + 0X
          activate n__len X -> len X
          1 + 0X >= 0 + 0X
          activate n__add(X1, X2) -> add(X1, X2)
          1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
          activate n__from X -> from X
          1 + 0X >= 0 + 0X
          activate n__fst(X1, X2) -> fst(X1, X2)
          1 + 0X1 + 0X2 >= 1 + 1X1 + 1X2
          activate X -> X
          1 + 0X >= 1X
          fst(s X, cons(Y, Z)) -> cons(Y, n__fst(activate X, activate Z))
          2 + 1Z + 0Y + 0X >= 3 + 0Z + 0Y + 0X
          fst(0(), Z) -> nil()
          2 + 1Z >= 0
          fst(X1, X2) -> n__fst(X1, X2)
          1 + 1X1 + 1X2 >= 1 + 1X1 + 0X2
        SCCS (0):