YES
TRS:
 {          a__fst(X1, X2) -> fst(X1, X2),
            a__fst(0(), Z) -> nil(),
  a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
               mark(nil()) -> nil(),
                 mark(0()) -> 0(),
        mark(cons(X1, X2)) -> cons(mark(X1), X2),
         mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                mark(s(X)) -> s(X),
             mark(from(X)) -> a__from(mark(X)),
         mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
              mark(len(X)) -> a__len(mark(X)),
                a__from(X) -> cons(mark(X), from(s(X))),
                a__from(X) -> from(X),
            a__add(X1, X2) -> add(X1, X2),
            a__add(0(), X) -> mark(X),
           a__add(s(X), Y) -> s(add(X, Y)),
                 a__len(X) -> len(X),
             a__len(nil()) -> 0(),
        a__len(cons(X, Z)) -> s(len(Z))}
 DP:
  Strict:
   {a__fst#(s(X), cons(Y, Z)) -> mark#(Y),
          mark#(cons(X1, X2)) -> mark#(X1),
           mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)),
           mark#(fst(X1, X2)) -> mark#(X1),
           mark#(fst(X1, X2)) -> mark#(X2),
               mark#(from(X)) -> mark#(X),
               mark#(from(X)) -> a__from#(mark(X)),
           mark#(add(X1, X2)) -> mark#(X1),
           mark#(add(X1, X2)) -> mark#(X2),
           mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                mark#(len(X)) -> mark#(X),
                mark#(len(X)) -> a__len#(mark(X)),
                  a__from#(X) -> mark#(X),
              a__add#(0(), X) -> mark#(X)}
  Weak:
  {          a__fst(X1, X2) -> fst(X1, X2),
             a__fst(0(), Z) -> nil(),
   a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                mark(nil()) -> nil(),
                  mark(0()) -> 0(),
         mark(cons(X1, X2)) -> cons(mark(X1), X2),
          mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                 mark(s(X)) -> s(X),
              mark(from(X)) -> a__from(mark(X)),
          mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
               mark(len(X)) -> a__len(mark(X)),
                 a__from(X) -> cons(mark(X), from(s(X))),
                 a__from(X) -> from(X),
             a__add(X1, X2) -> add(X1, X2),
             a__add(0(), X) -> mark(X),
            a__add(s(X), Y) -> s(add(X, Y)),
                  a__len(X) -> len(X),
              a__len(nil()) -> 0(),
         a__len(cons(X, Z)) -> s(len(Z))}
  EDG:
   {(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> a__len#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(len(X)) -> mark#(X), mark#(len(X)) -> a__len#(mark(X)))
    (mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))
    (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(len(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(len(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
    (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
    (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
    (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (mark#(len(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> a__len#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)))
    (a__add#(0(), X) -> mark#(X), mark#(from(X)) -> mark#(X))
    (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
    (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
    (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (a__add#(0(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> a__len#(mark(X)))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(len(X)) -> a__len#(mark(X)))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(len(X)) -> mark#(X))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(from(X)) -> a__from#(mark(X)))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(from(X)) -> mark#(X))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> mark#(X2))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> mark#(X1))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> a__len#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> a__len#(mark(X)))
    (mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), a__fst#(s(X), cons(Y, Z)) -> mark#(Y))
    (mark#(from(X)) -> a__from#(mark(X)), a__from#(X) -> mark#(X))
    (a__from#(X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
    (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
    (a__from#(X) -> mark#(X), mark#(from(X)) -> mark#(X))
    (a__from#(X) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)))
    (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (a__from#(X) -> mark#(X), mark#(len(X)) -> mark#(X))
    (a__from#(X) -> mark#(X), mark#(len(X)) -> a__len#(mark(X)))
    (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
    (mark#(from(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
    (mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
    (mark#(from(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(from(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(from(X)) -> mark#(X), mark#(len(X)) -> mark#(X))
    (mark#(from(X)) -> mark#(X), mark#(len(X)) -> a__len#(mark(X)))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))
    (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> a__len#(mark(X)))}
   SCCS:
    Scc:
     {a__fst#(s(X), cons(Y, Z)) -> mark#(Y),
            mark#(cons(X1, X2)) -> mark#(X1),
             mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)),
             mark#(fst(X1, X2)) -> mark#(X1),
             mark#(fst(X1, X2)) -> mark#(X2),
                 mark#(from(X)) -> mark#(X),
                 mark#(from(X)) -> a__from#(mark(X)),
             mark#(add(X1, X2)) -> mark#(X1),
             mark#(add(X1, X2)) -> mark#(X2),
             mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                  mark#(len(X)) -> mark#(X),
                    a__from#(X) -> mark#(X),
                a__add#(0(), X) -> mark#(X)}
    SCC:
     Strict:
      {a__fst#(s(X), cons(Y, Z)) -> mark#(Y),
             mark#(cons(X1, X2)) -> mark#(X1),
              mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)),
              mark#(fst(X1, X2)) -> mark#(X1),
              mark#(fst(X1, X2)) -> mark#(X2),
                  mark#(from(X)) -> mark#(X),
                  mark#(from(X)) -> a__from#(mark(X)),
              mark#(add(X1, X2)) -> mark#(X1),
              mark#(add(X1, X2)) -> mark#(X2),
              mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                   mark#(len(X)) -> mark#(X),
                     a__from#(X) -> mark#(X),
                 a__add#(0(), X) -> mark#(X)}
     Weak:
     {          a__fst(X1, X2) -> fst(X1, X2),
                a__fst(0(), Z) -> nil(),
      a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                   mark(nil()) -> nil(),
                     mark(0()) -> 0(),
            mark(cons(X1, X2)) -> cons(mark(X1), X2),
             mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                    mark(s(X)) -> s(X),
                 mark(from(X)) -> a__from(mark(X)),
             mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                  mark(len(X)) -> a__len(mark(X)),
                    a__from(X) -> cons(mark(X), from(s(X))),
                    a__from(X) -> from(X),
                a__add(X1, X2) -> add(X1, X2),
                a__add(0(), X) -> mark(X),
               a__add(s(X), Y) -> s(add(X, Y)),
                     a__len(X) -> len(X),
                 a__len(nil()) -> 0(),
            a__len(cons(X, Z)) -> s(len(Z))}
     POLY:
      Argument Filtering:
       pi(len) = 0, pi(a__len) = 0, pi(add) = [0,1], pi(a__add#) = 1, pi(a__add) = [0,1], pi(a__from#) = 0, pi(a__from) = [0], pi(from) = [0], pi(s) = [], pi(fst) = [0,1], pi(mark#) = 0, pi(mark) = 0, pi(cons) = 0, pi(0) = [], pi(a__fst#) = 1, pi(a__fst) = [0,1], pi(nil) = []
      Usable Rules:
       {}
      Interpretation:
       [add](x0, x1) = x0 + x1,
       [fst](x0, x1) = x0 + x1,
       [from](x0) = x0 + 1
      Strict:
       {a__fst#(s(X), cons(Y, Z)) -> mark#(Y),
              mark#(cons(X1, X2)) -> mark#(X1),
               mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)),
               mark#(fst(X1, X2)) -> mark#(X1),
               mark#(fst(X1, X2)) -> mark#(X2),
               mark#(add(X1, X2)) -> mark#(X1),
               mark#(add(X1, X2)) -> mark#(X2),
               mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                    mark#(len(X)) -> mark#(X),
                      a__from#(X) -> mark#(X),
                  a__add#(0(), X) -> mark#(X)}
      Weak:
       {          a__fst(X1, X2) -> fst(X1, X2),
                  a__fst(0(), Z) -> nil(),
        a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                     mark(nil()) -> nil(),
                       mark(0()) -> 0(),
              mark(cons(X1, X2)) -> cons(mark(X1), X2),
               mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                      mark(s(X)) -> s(X),
                   mark(from(X)) -> a__from(mark(X)),
               mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                    mark(len(X)) -> a__len(mark(X)),
                      a__from(X) -> cons(mark(X), from(s(X))),
                      a__from(X) -> from(X),
                  a__add(X1, X2) -> add(X1, X2),
                  a__add(0(), X) -> mark(X),
                 a__add(s(X), Y) -> s(add(X, Y)),
                       a__len(X) -> len(X),
                   a__len(nil()) -> 0(),
              a__len(cons(X, Z)) -> s(len(Z))}
      EDG:
       {(mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X))
        (mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))
        (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
        (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
        (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
        (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
        (mark#(len(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> mark#(X))
        (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
        (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
        (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
        (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
        (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
        (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
        (a__add#(0(), X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
        (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
        (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
        (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
        (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
        (mark#(fst(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))
        (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
        (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
        (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
        (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
        (mark#(fst(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
        (a__from#(X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
        (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
        (a__from#(X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
        (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
        (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
        (a__from#(X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
        (a__from#(X) -> mark#(X), mark#(len(X)) -> mark#(X))
        (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
        (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
        (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> mark#(X1))
        (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(fst(X1, X2)) -> mark#(X2))
        (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X1))
        (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> mark#(X2))
        (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
        (a__fst#(s(X), cons(Y, Z)) -> mark#(Y), mark#(len(X)) -> mark#(X))
        (mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)), a__fst#(s(X), cons(Y, Z)) -> mark#(Y))}
       SCCS:
        Scc:
         {a__fst#(s(X), cons(Y, Z)) -> mark#(Y),
                mark#(cons(X1, X2)) -> mark#(X1),
                 mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)),
                 mark#(fst(X1, X2)) -> mark#(X1),
                 mark#(fst(X1, X2)) -> mark#(X2),
                 mark#(add(X1, X2)) -> mark#(X1),
                 mark#(add(X1, X2)) -> mark#(X2),
                 mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                      mark#(len(X)) -> mark#(X),
                    a__add#(0(), X) -> mark#(X)}
        SCC:
         Strict:
          {a__fst#(s(X), cons(Y, Z)) -> mark#(Y),
                 mark#(cons(X1, X2)) -> mark#(X1),
                  mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)),
                  mark#(fst(X1, X2)) -> mark#(X1),
                  mark#(fst(X1, X2)) -> mark#(X2),
                  mark#(add(X1, X2)) -> mark#(X1),
                  mark#(add(X1, X2)) -> mark#(X2),
                  mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                       mark#(len(X)) -> mark#(X),
                     a__add#(0(), X) -> mark#(X)}
         Weak:
         {          a__fst(X1, X2) -> fst(X1, X2),
                    a__fst(0(), Z) -> nil(),
          a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                       mark(nil()) -> nil(),
                         mark(0()) -> 0(),
                mark(cons(X1, X2)) -> cons(mark(X1), X2),
                 mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                        mark(s(X)) -> s(X),
                     mark(from(X)) -> a__from(mark(X)),
                 mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                      mark(len(X)) -> a__len(mark(X)),
                        a__from(X) -> cons(mark(X), from(s(X))),
                        a__from(X) -> from(X),
                    a__add(X1, X2) -> add(X1, X2),
                    a__add(0(), X) -> mark(X),
                   a__add(s(X), Y) -> s(add(X, Y)),
                         a__len(X) -> len(X),
                     a__len(nil()) -> 0(),
                a__len(cons(X, Z)) -> s(len(Z))}
         POLY:
          Argument Filtering:
           pi(len) = 0, pi(a__len) = 0, pi(add) = [0,1], pi(a__add#) = 1, pi(a__add) = [0,1], pi(a__from) = [0], pi(from) = [0], pi(s) = [], pi(fst) = [0,1], pi(mark#) = 0, pi(mark) = 0, pi(cons) = [0], pi(0) = [], pi(a__fst#) = 1, pi(a__fst) = [0,1], pi(nil) = []
          Usable Rules:
           {}
          Interpretation:
           [add](x0, x1) = x0 + x1,
           [fst](x0, x1) = x0 + x1,
           [cons](x0) = x0 + 1
          Strict:
           {mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)),
            mark#(fst(X1, X2)) -> mark#(X1),
            mark#(fst(X1, X2)) -> mark#(X2),
            mark#(add(X1, X2)) -> mark#(X1),
            mark#(add(X1, X2)) -> mark#(X2),
            mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                 mark#(len(X)) -> mark#(X),
               a__add#(0(), X) -> mark#(X)}
          Weak:
           {          a__fst(X1, X2) -> fst(X1, X2),
                      a__fst(0(), Z) -> nil(),
            a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                         mark(nil()) -> nil(),
                           mark(0()) -> 0(),
                  mark(cons(X1, X2)) -> cons(mark(X1), X2),
                   mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                          mark(s(X)) -> s(X),
                       mark(from(X)) -> a__from(mark(X)),
                   mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                        mark(len(X)) -> a__len(mark(X)),
                          a__from(X) -> cons(mark(X), from(s(X))),
                          a__from(X) -> from(X),
                      a__add(X1, X2) -> add(X1, X2),
                      a__add(0(), X) -> mark(X),
                     a__add(s(X), Y) -> s(add(X, Y)),
                           a__len(X) -> len(X),
                       a__len(nil()) -> 0(),
                  a__len(cons(X, Z)) -> s(len(Z))}
          EDG:
           {(mark#(add(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))
            (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
            (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
            (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
            (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
            (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
            (mark#(add(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
            (mark#(add(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
            (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
            (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
            (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
            (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
            (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
            (mark#(add(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
            (mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)), a__add#(0(), X) -> mark#(X))
            (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> mark#(X))
            (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
            (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
            (a__add#(0(), X) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
            (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
            (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
            (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
            (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
            (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
            (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
            (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
            (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
            (mark#(len(X)) -> mark#(X), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
            (mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))
            (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
            (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
            (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
            (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
            (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
            (mark#(fst(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
            (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
            (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> a__fst#(mark(X1), mark(X2)))
            (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
            (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
            (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
            (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
            (mark#(fst(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)))
            (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))}
           SCCS:
            Scc:
             {mark#(fst(X1, X2)) -> mark#(X1),
              mark#(fst(X1, X2)) -> mark#(X2),
              mark#(add(X1, X2)) -> mark#(X1),
              mark#(add(X1, X2)) -> mark#(X2),
              mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                   mark#(len(X)) -> mark#(X),
                 a__add#(0(), X) -> mark#(X)}
            SCC:
             Strict:
              {mark#(fst(X1, X2)) -> mark#(X1),
               mark#(fst(X1, X2)) -> mark#(X2),
               mark#(add(X1, X2)) -> mark#(X1),
               mark#(add(X1, X2)) -> mark#(X2),
               mark#(add(X1, X2)) -> a__add#(mark(X1), mark(X2)),
                    mark#(len(X)) -> mark#(X),
                  a__add#(0(), X) -> mark#(X)}
             Weak:
             {          a__fst(X1, X2) -> fst(X1, X2),
                        a__fst(0(), Z) -> nil(),
              a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                           mark(nil()) -> nil(),
                             mark(0()) -> 0(),
                    mark(cons(X1, X2)) -> cons(mark(X1), X2),
                     mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                            mark(s(X)) -> s(X),
                         mark(from(X)) -> a__from(mark(X)),
                     mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                          mark(len(X)) -> a__len(mark(X)),
                            a__from(X) -> cons(mark(X), from(s(X))),
                            a__from(X) -> from(X),
                        a__add(X1, X2) -> add(X1, X2),
                        a__add(0(), X) -> mark(X),
                       a__add(s(X), Y) -> s(add(X, Y)),
                             a__len(X) -> len(X),
                         a__len(nil()) -> 0(),
                    a__len(cons(X, Z)) -> s(len(Z))}
             POLY:
              Argument Filtering:
               pi(len) = 0, pi(a__len) = 0, pi(add) = [0,1], pi(a__add#) = 1, pi(a__add) = [0,1], pi(a__from) = [], pi(from) = [], pi(s) = [], pi(fst) = [0,1], pi(mark#) = 0, pi(mark) = 0, pi(cons) = [], pi(0) = [], pi(a__fst) = [0,1], pi(nil) = []
              Usable Rules:
               {}
              Interpretation:
               [add](x0, x1) = x0 + x1 + 1,
               [fst](x0, x1) = x0 + x1
              Strict:
               {mark#(fst(X1, X2)) -> mark#(X1),
                mark#(fst(X1, X2)) -> mark#(X2),
                     mark#(len(X)) -> mark#(X),
                   a__add#(0(), X) -> mark#(X)}
              Weak:
               {          a__fst(X1, X2) -> fst(X1, X2),
                          a__fst(0(), Z) -> nil(),
                a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                             mark(nil()) -> nil(),
                               mark(0()) -> 0(),
                      mark(cons(X1, X2)) -> cons(mark(X1), X2),
                       mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                              mark(s(X)) -> s(X),
                           mark(from(X)) -> a__from(mark(X)),
                       mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                            mark(len(X)) -> a__len(mark(X)),
                              a__from(X) -> cons(mark(X), from(s(X))),
                              a__from(X) -> from(X),
                          a__add(X1, X2) -> add(X1, X2),
                          a__add(0(), X) -> mark(X),
                         a__add(s(X), Y) -> s(add(X, Y)),
                               a__len(X) -> len(X),
                           a__len(nil()) -> 0(),
                      a__len(cons(X, Z)) -> s(len(Z))}
              EDG:
               {(mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))
                (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
                (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
                (mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
                (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X2))
                (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
                (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
                (a__add#(0(), X) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X2))
                (a__add#(0(), X) -> mark#(X), mark#(len(X)) -> mark#(X))
                (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X1))
                (mark#(fst(X1, X2)) -> mark#(X2), mark#(fst(X1, X2)) -> mark#(X2))
                (mark#(fst(X1, X2)) -> mark#(X2), mark#(len(X)) -> mark#(X))}
               SCCS:
                Scc:
                 {mark#(fst(X1, X2)) -> mark#(X1),
                  mark#(fst(X1, X2)) -> mark#(X2),
                       mark#(len(X)) -> mark#(X)}
                SCC:
                 Strict:
                  {mark#(fst(X1, X2)) -> mark#(X1),
                   mark#(fst(X1, X2)) -> mark#(X2),
                        mark#(len(X)) -> mark#(X)}
                 Weak:
                 {          a__fst(X1, X2) -> fst(X1, X2),
                            a__fst(0(), Z) -> nil(),
                  a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                               mark(nil()) -> nil(),
                                 mark(0()) -> 0(),
                        mark(cons(X1, X2)) -> cons(mark(X1), X2),
                         mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                                mark(s(X)) -> s(X),
                             mark(from(X)) -> a__from(mark(X)),
                         mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                              mark(len(X)) -> a__len(mark(X)),
                                a__from(X) -> cons(mark(X), from(s(X))),
                                a__from(X) -> from(X),
                            a__add(X1, X2) -> add(X1, X2),
                            a__add(0(), X) -> mark(X),
                           a__add(s(X), Y) -> s(add(X, Y)),
                                 a__len(X) -> len(X),
                             a__len(nil()) -> 0(),
                        a__len(cons(X, Z)) -> s(len(Z))}
                 SPSC:
                  Simple Projection:
                   pi(mark#) = 0
                  Strict:
                   {mark#(fst(X1, X2)) -> mark#(X1),
                         mark#(len(X)) -> mark#(X)}
                  EDG:
                   {(mark#(fst(X1, X2)) -> mark#(X1), mark#(len(X)) -> mark#(X))
                    (mark#(fst(X1, X2)) -> mark#(X1), mark#(fst(X1, X2)) -> mark#(X1))
                    (mark#(len(X)) -> mark#(X), mark#(fst(X1, X2)) -> mark#(X1))
                    (mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))}
                   SCCS:
                    Scc:
                     {mark#(fst(X1, X2)) -> mark#(X1),
                           mark#(len(X)) -> mark#(X)}
                    SCC:
                     Strict:
                      {mark#(fst(X1, X2)) -> mark#(X1),
                            mark#(len(X)) -> mark#(X)}
                     Weak:
                     {          a__fst(X1, X2) -> fst(X1, X2),
                                a__fst(0(), Z) -> nil(),
                      a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                                   mark(nil()) -> nil(),
                                     mark(0()) -> 0(),
                            mark(cons(X1, X2)) -> cons(mark(X1), X2),
                             mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                                    mark(s(X)) -> s(X),
                                 mark(from(X)) -> a__from(mark(X)),
                             mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                                  mark(len(X)) -> a__len(mark(X)),
                                    a__from(X) -> cons(mark(X), from(s(X))),
                                    a__from(X) -> from(X),
                                a__add(X1, X2) -> add(X1, X2),
                                a__add(0(), X) -> mark(X),
                               a__add(s(X), Y) -> s(add(X, Y)),
                                     a__len(X) -> len(X),
                                 a__len(nil()) -> 0(),
                            a__len(cons(X, Z)) -> s(len(Z))}
                     SPSC:
                      Simple Projection:
                       pi(mark#) = 0
                      Strict:
                       {mark#(len(X)) -> mark#(X)}
                      EDG:
                       {(mark#(len(X)) -> mark#(X), mark#(len(X)) -> mark#(X))}
                       SCCS:
                        Scc:
                         {mark#(len(X)) -> mark#(X)}
                        SCC:
                         Strict:
                          {mark#(len(X)) -> mark#(X)}
                         Weak:
                         {          a__fst(X1, X2) -> fst(X1, X2),
                                    a__fst(0(), Z) -> nil(),
                          a__fst(s(X), cons(Y, Z)) -> cons(mark(Y), fst(X, Z)),
                                       mark(nil()) -> nil(),
                                         mark(0()) -> 0(),
                                mark(cons(X1, X2)) -> cons(mark(X1), X2),
                                 mark(fst(X1, X2)) -> a__fst(mark(X1), mark(X2)),
                                        mark(s(X)) -> s(X),
                                     mark(from(X)) -> a__from(mark(X)),
                                 mark(add(X1, X2)) -> a__add(mark(X1), mark(X2)),
                                      mark(len(X)) -> a__len(mark(X)),
                                        a__from(X) -> cons(mark(X), from(s(X))),
                                        a__from(X) -> from(X),
                                    a__add(X1, X2) -> add(X1, X2),
                                    a__add(0(), X) -> mark(X),
                                   a__add(s(X), Y) -> s(add(X, Y)),
                                         a__len(X) -> len(X),
                                     a__len(nil()) -> 0(),
                                a__len(cons(X, Z)) -> s(len(Z))}
                         SPSC:
                          Simple Projection:
                           pi(mark#) = 0
                          Strict:
                           {}
                          Qed