YES
Time: 0.003782
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}
  UR:
   {}
   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)}
    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)}
     EDG:
      {}
      EDG:
       {}
       STATUS:
        arrows: 1.000000
        SCCS (0):