YES

Problem:
 a__fst(0(),Z) -> nil()
 a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
 a__from(X) -> cons(mark(X),from(s(X)))
 a__add(0(),X) -> mark(X)
 a__add(s(X),Y) -> s(add(X,Y))
 a__len(nil()) -> 0()
 a__len(cons(X,Z)) -> s(len(Z))
 mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
 mark(from(X)) -> a__from(mark(X))
 mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
 mark(len(X)) -> a__len(mark(X))
 mark(0()) -> 0()
 mark(s(X)) -> s(X)
 mark(nil()) -> nil()
 mark(cons(X1,X2)) -> cons(mark(X1),X2)
 a__fst(X1,X2) -> fst(X1,X2)
 a__from(X) -> from(X)
 a__add(X1,X2) -> add(X1,X2)
 a__len(X) -> len(X)

Proof:
 DP Processor:
  DPs:
   a__fst#(s(X),cons(Y,Z)) -> mark#(Y)
   a__from#(X) -> mark#(X)
   a__add#(0(),X) -> mark#(X)
   mark#(fst(X1,X2)) -> mark#(X2)
   mark#(fst(X1,X2)) -> mark#(X1)
   mark#(fst(X1,X2)) -> a__fst#(mark(X1),mark(X2))
   mark#(from(X)) -> mark#(X)
   mark#(from(X)) -> a__from#(mark(X))
   mark#(add(X1,X2)) -> mark#(X2)
   mark#(add(X1,X2)) -> mark#(X1)
   mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
   mark#(len(X)) -> mark#(X)
   mark#(len(X)) -> a__len#(mark(X))
   mark#(cons(X1,X2)) -> mark#(X1)
  TRS:
   a__fst(0(),Z) -> nil()
   a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
   a__from(X) -> cons(mark(X),from(s(X)))
   a__add(0(),X) -> mark(X)
   a__add(s(X),Y) -> s(add(X,Y))
   a__len(nil()) -> 0()
   a__len(cons(X,Z)) -> s(len(Z))
   mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
   mark(from(X)) -> a__from(mark(X))
   mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
   mark(len(X)) -> a__len(mark(X))
   mark(0()) -> 0()
   mark(s(X)) -> s(X)
   mark(nil()) -> nil()
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   a__fst(X1,X2) -> fst(X1,X2)
   a__from(X) -> from(X)
   a__add(X1,X2) -> add(X1,X2)
   a__len(X) -> len(X)
  TDG Processor:
   DPs:
    a__fst#(s(X),cons(Y,Z)) -> mark#(Y)
    a__from#(X) -> mark#(X)
    a__add#(0(),X) -> mark#(X)
    mark#(fst(X1,X2)) -> mark#(X2)
    mark#(fst(X1,X2)) -> mark#(X1)
    mark#(fst(X1,X2)) -> a__fst#(mark(X1),mark(X2))
    mark#(from(X)) -> mark#(X)
    mark#(from(X)) -> a__from#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    mark#(len(X)) -> mark#(X)
    mark#(len(X)) -> a__len#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1)
   TRS:
    a__fst(0(),Z) -> nil()
    a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
    a__from(X) -> cons(mark(X),from(s(X)))
    a__add(0(),X) -> mark(X)
    a__add(s(X),Y) -> s(add(X,Y))
    a__len(nil()) -> 0()
    a__len(cons(X,Z)) -> s(len(Z))
    mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
    mark(from(X)) -> a__from(mark(X))
    mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
    mark(len(X)) -> a__len(mark(X))
    mark(0()) -> 0()
    mark(s(X)) -> s(X)
    mark(nil()) -> nil()
    mark(cons(X1,X2)) -> cons(mark(X1),X2)
    a__fst(X1,X2) -> fst(X1,X2)
    a__from(X) -> from(X)
    a__add(X1,X2) -> add(X1,X2)
    a__len(X) -> len(X)
   graph:
    a__add#(0(),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#(X1)
    a__add#(0(),X) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    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)) -> a__fst#(mark(X1),mark(X2))
    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__from#(X) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__from#(X) -> mark#(X) -> mark#(len(X)) -> a__len#(mark(X))
    a__from#(X) -> mark#(X) -> mark#(len(X)) -> mark#(X)
    a__from#(X) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),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#(from(X)) -> a__from#(mark(X))
    a__from#(X) -> mark#(X) -> mark#(from(X)) -> mark#(X)
    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)
    mark#(len(X)) -> mark#(X) -> 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#(X1)
    mark#(len(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    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)) -> 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#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) ->
    a__add#(0(),X) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1)
    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#(X1)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2)
    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)) -> 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#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(len(X)) -> a__len#(mark(X))
    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#(X1)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> a__from#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
    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#(from(X)) -> a__from#(mark(X)) -> a__from#(X) -> mark#(X)
    mark#(from(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(from(X)) -> mark#(X) -> mark#(len(X)) -> a__len#(mark(X))
    mark#(from(X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
    mark#(from(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
    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#(from(X)) -> a__from#(mark(X))
    mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
    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#(fst(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(len(X)) -> a__len#(mark(X))
    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#(X1)
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(from(X)) -> a__from#(mark(X))
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(from(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#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    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#(X1)
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2)
    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)) -> 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)) -> a__fst#(mark(X1),mark(X2)) ->
    a__fst#(s(X),cons(Y,Z)) -> mark#(Y)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(len(X)) -> a__len#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> a__add#(mark(X1),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#(from(X)) -> a__from#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
    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)
    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#(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#(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#(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)) -> 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)
   SCC Processor:
    #sccs: 1
    #rules: 13
    #arcs: 113/196
    DPs:
     a__add#(0(),X) -> mark#(X)
     mark#(fst(X1,X2)) -> mark#(X2)
     mark#(fst(X1,X2)) -> mark#(X1)
     mark#(fst(X1,X2)) -> a__fst#(mark(X1),mark(X2))
     a__fst#(s(X),cons(Y,Z)) -> mark#(Y)
     mark#(from(X)) -> mark#(X)
     mark#(from(X)) -> a__from#(mark(X))
     a__from#(X) -> mark#(X)
     mark#(add(X1,X2)) -> mark#(X2)
     mark#(add(X1,X2)) -> mark#(X1)
     mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
     mark#(len(X)) -> mark#(X)
     mark#(cons(X1,X2)) -> mark#(X1)
    TRS:
     a__fst(0(),Z) -> nil()
     a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
     a__from(X) -> cons(mark(X),from(s(X)))
     a__add(0(),X) -> mark(X)
     a__add(s(X),Y) -> s(add(X,Y))
     a__len(nil()) -> 0()
     a__len(cons(X,Z)) -> s(len(Z))
     mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
     mark(from(X)) -> a__from(mark(X))
     mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
     mark(len(X)) -> a__len(mark(X))
     mark(0()) -> 0()
     mark(s(X)) -> s(X)
     mark(nil()) -> nil()
     mark(cons(X1,X2)) -> cons(mark(X1),X2)
     a__fst(X1,X2) -> fst(X1,X2)
     a__from(X) -> from(X)
     a__add(X1,X2) -> add(X1,X2)
     a__len(X) -> len(X)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [a__add#](x0, x1) = 7x1 + 0,
      
      [a__from#](x0) = 1x0 + 4,
      
      [mark#](x0) = x0 + 0,
      
      [a__fst#](x0, x1) = 2x0 + 4x1,
      
      [len](x0) = 4x0,
      
      [a__len](x0) = 4x0,
      
      [add](x0, x1) = 3x0 + 7x1,
      
      [a__add](x0, x1) = 3x0 + 7x1,
      
      [from](x0) = 2x0 + 4,
      
      [a__from](x0) = 2x0 + 4,
      
      [fst](x0, x1) = 4x0 + 4x1,
      
      [mark](x0) = x0,
      
      [cons](x0, x1) = x0 + x1 + 0,
      
      [s](x0) = x0 + 2,
      
      [nil] = 0,
      
      [a__fst](x0, x1) = 4x0 + 4x1,
      
      [0] = 0
     orientation:
      a__add#(0(),X) = 7X + 0 >= X + 0 = mark#(X)
      
      mark#(fst(X1,X2)) = 4X1 + 4X2 + 0 >= X2 + 0 = mark#(X2)
      
      mark#(fst(X1,X2)) = 4X1 + 4X2 + 0 >= X1 + 0 = mark#(X1)
      
      mark#(fst(X1,X2)) = 4X1 + 4X2 + 0 >= 2X1 + 4X2 = a__fst#(mark(X1),mark(X2))
      
      a__fst#(s(X),cons(Y,Z)) = 2X + 4Y + 4Z + 4 >= Y + 0 = mark#(Y)
      
      mark#(from(X)) = 2X + 4 >= X + 0 = mark#(X)
      
      mark#(from(X)) = 2X + 4 >= 1X + 4 = a__from#(mark(X))
      
      a__from#(X) = 1X + 4 >= X + 0 = mark#(X)
      
      mark#(add(X1,X2)) = 3X1 + 7X2 + 0 >= X2 + 0 = mark#(X2)
      
      mark#(add(X1,X2)) = 3X1 + 7X2 + 0 >= X1 + 0 = mark#(X1)
      
      mark#(add(X1,X2)) = 3X1 + 7X2 + 0 >= 7X2 + 0 = a__add#(mark(X1),mark(X2))
      
      mark#(len(X)) = 4X + 0 >= X + 0 = mark#(X)
      
      mark#(cons(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = mark#(X1)
      
      a__fst(0(),Z) = 4Z + 4 >= 0 = nil()
      
      a__fst(s(X),cons(Y,Z)) = 4X + 4Y + 4Z + 6 >= 4X + Y + 4Z + 0 = cons(mark(Y),fst(X,Z))
      
      a__from(X) = 2X + 4 >= 2X + 4 = cons(mark(X),from(s(X)))
      
      a__add(0(),X) = 7X + 3 >= X = mark(X)
      
      a__add(s(X),Y) = 3X + 7Y + 5 >= 3X + 7Y + 2 = s(add(X,Y))
      
      a__len(nil()) = 4 >= 0 = 0()
      
      a__len(cons(X,Z)) = 4X + 4Z + 4 >= 4Z + 2 = s(len(Z))
      
      mark(fst(X1,X2)) = 4X1 + 4X2 >= 4X1 + 4X2 = a__fst(mark(X1),mark(X2))
      
      mark(from(X)) = 2X + 4 >= 2X + 4 = a__from(mark(X))
      
      mark(add(X1,X2)) = 3X1 + 7X2 >= 3X1 + 7X2 = a__add(mark(X1),mark(X2))
      
      mark(len(X)) = 4X >= 4X = a__len(mark(X))
      
      mark(0()) = 0 >= 0 = 0()
      
      mark(s(X)) = X + 2 >= X + 2 = s(X)
      
      mark(nil()) = 0 >= 0 = nil()
      
      mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(mark(X1),X2)
      
      a__fst(X1,X2) = 4X1 + 4X2 >= 4X1 + 4X2 = fst(X1,X2)
      
      a__from(X) = 2X + 4 >= 2X + 4 = from(X)
      
      a__add(X1,X2) = 3X1 + 7X2 >= 3X1 + 7X2 = add(X1,X2)
      
      a__len(X) = 4X >= 4X = len(X)
     problem:
      DPs:
       a__add#(0(),X) -> mark#(X)
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(fst(X1,X2)) -> mark#(X1)
       mark#(fst(X1,X2)) -> a__fst#(mark(X1),mark(X2))
       mark#(from(X)) -> a__from#(mark(X))
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
       mark#(len(X)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1)
      TRS:
       a__fst(0(),Z) -> nil()
       a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
       a__from(X) -> cons(mark(X),from(s(X)))
       a__add(0(),X) -> mark(X)
       a__add(s(X),Y) -> s(add(X,Y))
       a__len(nil()) -> 0()
       a__len(cons(X,Z)) -> s(len(Z))
       mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
       mark(from(X)) -> a__from(mark(X))
       mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
       mark(len(X)) -> a__len(mark(X))
       mark(0()) -> 0()
       mark(s(X)) -> s(X)
       mark(nil()) -> nil()
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       a__fst(X1,X2) -> fst(X1,X2)
       a__from(X) -> from(X)
       a__add(X1,X2) -> add(X1,X2)
       a__len(X) -> len(X)
     SCC Processor:
      #sccs: 1
      #rules: 8
      #arcs: 103/100
      DPs:
       a__add#(0(),X) -> mark#(X)
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(fst(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#(len(X)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1)
      TRS:
       a__fst(0(),Z) -> nil()
       a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
       a__from(X) -> cons(mark(X),from(s(X)))
       a__add(0(),X) -> mark(X)
       a__add(s(X),Y) -> s(add(X,Y))
       a__len(nil()) -> 0()
       a__len(cons(X,Z)) -> s(len(Z))
       mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
       mark(from(X)) -> a__from(mark(X))
       mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
       mark(len(X)) -> a__len(mark(X))
       mark(0()) -> 0()
       mark(s(X)) -> s(X)
       mark(nil()) -> nil()
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       a__fst(X1,X2) -> fst(X1,X2)
       a__from(X) -> from(X)
       a__add(X1,X2) -> add(X1,X2)
       a__len(X) -> len(X)
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [a__add#](x0, x1) = x0 + x1 + 0,
        
        [mark#](x0) = x0 + 0,
        
        [len](x0) = x0 + 0,
        
        [a__len](x0) = x0 + 0,
        
        [add](x0, x1) = x0 + x1 + 0,
        
        [a__add](x0, x1) = x0 + x1 + 0,
        
        [from](x0) = 4x0 + 4,
        
        [a__from](x0) = 4x0 + 4,
        
        [fst](x0, x1) = x0 + x1 + 0,
        
        [mark](x0) = x0 + 0,
        
        [cons](x0, x1) = 2x0 + x1 + 2,
        
        [s](x0) = x0 + 0,
        
        [nil] = 0,
        
        [a__fst](x0, x1) = x0 + x1 + 0,
        
        [0] = 0
       orientation:
        a__add#(0(),X) = X + 0 >= X + 0 = mark#(X)
        
        mark#(fst(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = mark#(X2)
        
        mark#(fst(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = mark#(X1)
        
        mark#(add(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = mark#(X2)
        
        mark#(add(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = mark#(X1)
        
        mark#(add(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__add#(mark(X1),mark(X2))
        
        mark#(len(X)) = X + 0 >= X + 0 = mark#(X)
        
        mark#(cons(X1,X2)) = 2X1 + X2 + 2 >= X1 + 0 = mark#(X1)
        
        a__fst(0(),Z) = Z + 0 >= 0 = nil()
        
        a__fst(s(X),cons(Y,Z)) = X + 2Y + Z + 2 >= X + 2Y + Z + 2 = cons(mark(Y),fst(X,Z))
        
        a__from(X) = 4X + 4 >= 4X + 4 = cons(mark(X),from(s(X)))
        
        a__add(0(),X) = X + 0 >= X + 0 = mark(X)
        
        a__add(s(X),Y) = X + Y + 0 >= X + Y + 0 = s(add(X,Y))
        
        a__len(nil()) = 0 >= 0 = 0()
        
        a__len(cons(X,Z)) = 2X + Z + 2 >= Z + 0 = s(len(Z))
        
        mark(fst(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__fst(mark(X1),mark(X2))
        
        mark(from(X)) = 4X + 4 >= 4X + 4 = a__from(mark(X))
        
        mark(add(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__add(mark(X1),mark(X2))
        
        mark(len(X)) = X + 0 >= X + 0 = a__len(mark(X))
        
        mark(0()) = 0 >= 0 = 0()
        
        mark(s(X)) = X + 0 >= X + 0 = s(X)
        
        mark(nil()) = 0 >= 0 = nil()
        
        mark(cons(X1,X2)) = 2X1 + X2 + 2 >= 2X1 + X2 + 2 = cons(mark(X1),X2)
        
        a__fst(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = fst(X1,X2)
        
        a__from(X) = 4X + 4 >= 4X + 4 = from(X)
        
        a__add(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = add(X1,X2)
        
        a__len(X) = X + 0 >= X + 0 = len(X)
       problem:
        DPs:
         a__add#(0(),X) -> mark#(X)
         mark#(fst(X1,X2)) -> mark#(X2)
         mark#(fst(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#(len(X)) -> mark#(X)
        TRS:
         a__fst(0(),Z) -> nil()
         a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
         a__from(X) -> cons(mark(X),from(s(X)))
         a__add(0(),X) -> mark(X)
         a__add(s(X),Y) -> s(add(X,Y))
         a__len(nil()) -> 0()
         a__len(cons(X,Z)) -> s(len(Z))
         mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
         mark(from(X)) -> a__from(mark(X))
         mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
         mark(len(X)) -> a__len(mark(X))
         mark(0()) -> 0()
         mark(s(X)) -> s(X)
         mark(nil()) -> nil()
         mark(cons(X1,X2)) -> cons(mark(X1),X2)
         a__fst(X1,X2) -> fst(X1,X2)
         a__from(X) -> from(X)
         a__add(X1,X2) -> add(X1,X2)
         a__len(X) -> len(X)
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [a__add#](x0, x1) = x0 + x1 + 0,
         
         [mark#](x0) = x0 + 0,
         
         [len](x0) = x0,
         
         [a__len](x0) = x0 + 0,
         
         [add](x0, x1) = x0 + x1,
         
         [a__add](x0, x1) = x0 + x1 + 0,
         
         [from](x0) = 4,
         
         [a__from](x0) = 4,
         
         [fst](x0, x1) = 5x0 + 5x1 + 5,
         
         [mark](x0) = x0 + 0,
         
         [cons](x0, x1) = x1 + 0,
         
         [s](x0) = x0,
         
         [nil] = 0,
         
         [a__fst](x0, x1) = 5x0 + 5x1 + 5,
         
         [0] = 0
        orientation:
         a__add#(0(),X) = X + 0 >= X + 0 = mark#(X)
         
         mark#(fst(X1,X2)) = 5X1 + 5X2 + 5 >= X2 + 0 = mark#(X2)
         
         mark#(fst(X1,X2)) = 5X1 + 5X2 + 5 >= X1 + 0 = mark#(X1)
         
         mark#(add(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = mark#(X2)
         
         mark#(add(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = mark#(X1)
         
         mark#(add(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__add#(mark(X1),mark(X2))
         
         mark#(len(X)) = X + 0 >= X + 0 = mark#(X)
         
         a__fst(0(),Z) = 5Z + 5 >= 0 = nil()
         
         a__fst(s(X),cons(Y,Z)) = 5X + 5Z + 5 >= 5X + 5Z + 5 = cons(mark(Y),fst(X,Z))
         
         a__from(X) = 4 >= 4 = cons(mark(X),from(s(X)))
         
         a__add(0(),X) = X + 0 >= X + 0 = mark(X)
         
         a__add(s(X),Y) = X + Y + 0 >= X + Y = s(add(X,Y))
         
         a__len(nil()) = 0 >= 0 = 0()
         
         a__len(cons(X,Z)) = Z + 0 >= Z = s(len(Z))
         
         mark(fst(X1,X2)) = 5X1 + 5X2 + 5 >= 5X1 + 5X2 + 5 = a__fst(mark(X1),mark(X2))
         
         mark(from(X)) = 4 >= 4 = a__from(mark(X))
         
         mark(add(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__add(mark(X1),mark(X2))
         
         mark(len(X)) = X + 0 >= X + 0 = a__len(mark(X))
         
         mark(0()) = 0 >= 0 = 0()
         
         mark(s(X)) = X + 0 >= X = s(X)
         
         mark(nil()) = 0 >= 0 = nil()
         
         mark(cons(X1,X2)) = X2 + 0 >= X2 + 0 = cons(mark(X1),X2)
         
         a__fst(X1,X2) = 5X1 + 5X2 + 5 >= 5X1 + 5X2 + 5 = fst(X1,X2)
         
         a__from(X) = 4 >= 4 = from(X)
         
         a__add(X1,X2) = X1 + X2 + 0 >= X1 + X2 = add(X1,X2)
         
         a__len(X) = X + 0 >= X = len(X)
        problem:
         DPs:
          a__add#(0(),X) -> mark#(X)
          mark#(add(X1,X2)) -> mark#(X2)
          mark#(add(X1,X2)) -> mark#(X1)
          mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
          mark#(len(X)) -> mark#(X)
         TRS:
          a__fst(0(),Z) -> nil()
          a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
          a__from(X) -> cons(mark(X),from(s(X)))
          a__add(0(),X) -> mark(X)
          a__add(s(X),Y) -> s(add(X,Y))
          a__len(nil()) -> 0()
          a__len(cons(X,Z)) -> s(len(Z))
          mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
          mark(from(X)) -> a__from(mark(X))
          mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
          mark(len(X)) -> a__len(mark(X))
          mark(0()) -> 0()
          mark(s(X)) -> s(X)
          mark(nil()) -> nil()
          mark(cons(X1,X2)) -> cons(mark(X1),X2)
          a__fst(X1,X2) -> fst(X1,X2)
          a__from(X) -> from(X)
          a__add(X1,X2) -> add(X1,X2)
          a__len(X) -> len(X)
        Arctic Interpretation Processor:
         dimension: 1
         interpretation:
          [a__add#](x0, x1) = x1 + 0,
          
          [mark#](x0) = x0,
          
          [len](x0) = 5x0 + 6,
          
          [a__len](x0) = 5x0 + 6,
          
          [add](x0, x1) = x0 + x1 + 0,
          
          [a__add](x0, x1) = x0 + x1 + 0,
          
          [from](x0) = x0 + 1,
          
          [a__from](x0) = x0 + 1,
          
          [fst](x0, x1) = x0 + x1,
          
          [mark](x0) = x0 + 0,
          
          [cons](x0, x1) = x0 + 1,
          
          [s](x0) = 4,
          
          [nil] = 1,
          
          [a__fst](x0, x1) = x0 + x1 + 0,
          
          [0] = 1
         orientation:
          a__add#(0(),X) = X + 0 >= X = mark#(X)
          
          mark#(add(X1,X2)) = X1 + X2 + 0 >= X2 = mark#(X2)
          
          mark#(add(X1,X2)) = X1 + X2 + 0 >= X1 = mark#(X1)
          
          mark#(add(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = a__add#(mark(X1),mark(X2))
          
          mark#(len(X)) = 5X + 6 >= X = mark#(X)
          
          a__fst(0(),Z) = Z + 1 >= 1 = nil()
          
          a__fst(s(X),cons(Y,Z)) = Y + 4 >= Y + 1 = cons(mark(Y),fst(X,Z))
          
          a__from(X) = X + 1 >= X + 1 = cons(mark(X),from(s(X)))
          
          a__add(0(),X) = X + 1 >= X + 0 = mark(X)
          
          a__add(s(X),Y) = Y + 4 >= 4 = s(add(X,Y))
          
          a__len(nil()) = 6 >= 1 = 0()
          
          a__len(cons(X,Z)) = 5X + 6 >= 4 = s(len(Z))
          
          mark(fst(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__fst(mark(X1),mark(X2))
          
          mark(from(X)) = X + 1 >= X + 1 = a__from(mark(X))
          
          mark(add(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__add(mark(X1),mark(X2))
          
          mark(len(X)) = 5X + 6 >= 5X + 6 = a__len(mark(X))
          
          mark(0()) = 1 >= 1 = 0()
          
          mark(s(X)) = 4 >= 4 = s(X)
          
          mark(nil()) = 1 >= 1 = nil()
          
          mark(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(mark(X1),X2)
          
          a__fst(X1,X2) = X1 + X2 + 0 >= X1 + X2 = fst(X1,X2)
          
          a__from(X) = X + 1 >= X + 1 = from(X)
          
          a__add(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = add(X1,X2)
          
          a__len(X) = 5X + 6 >= 5X + 6 = len(X)
         problem:
          DPs:
           a__add#(0(),X) -> mark#(X)
           mark#(add(X1,X2)) -> mark#(X2)
           mark#(add(X1,X2)) -> mark#(X1)
           mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
          TRS:
           a__fst(0(),Z) -> nil()
           a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
           a__from(X) -> cons(mark(X),from(s(X)))
           a__add(0(),X) -> mark(X)
           a__add(s(X),Y) -> s(add(X,Y))
           a__len(nil()) -> 0()
           a__len(cons(X,Z)) -> s(len(Z))
           mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
           mark(from(X)) -> a__from(mark(X))
           mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
           mark(len(X)) -> a__len(mark(X))
           mark(0()) -> 0()
           mark(s(X)) -> s(X)
           mark(nil()) -> nil()
           mark(cons(X1,X2)) -> cons(mark(X1),X2)
           a__fst(X1,X2) -> fst(X1,X2)
           a__from(X) -> from(X)
           a__add(X1,X2) -> add(X1,X2)
           a__len(X) -> len(X)
         Arctic Interpretation Processor:
          dimension: 1
          interpretation:
           [a__add#](x0, x1) = 7x0 + x1 + 7,
           
           [mark#](x0) = x0,
           
           [len](x0) = x0 + 0,
           
           [a__len](x0) = x0 + 0,
           
           [add](x0, x1) = 7x0 + x1 + 7,
           
           [a__add](x0, x1) = 7x0 + x1 + 7,
           
           [from](x0) = x0 + 4,
           
           [a__from](x0) = x0 + 4,
           
           [fst](x0, x1) = x0 + x1,
           
           [mark](x0) = x0,
           
           [cons](x0, x1) = x1 + 4,
           
           [s](x0) = x0,
           
           [nil] = 0,
           
           [a__fst](x0, x1) = x0 + x1,
           
           [0] = 0
          orientation:
           a__add#(0(),X) = X + 7 >= X = mark#(X)
           
           mark#(add(X1,X2)) = 7X1 + X2 + 7 >= X2 = mark#(X2)
           
           mark#(add(X1,X2)) = 7X1 + X2 + 7 >= X1 = mark#(X1)
           
           mark#(add(X1,X2)) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = a__add#(mark(X1),mark(X2))
           
           a__fst(0(),Z) = Z + 0 >= 0 = nil()
           
           a__fst(s(X),cons(Y,Z)) = X + Z + 4 >= X + Z + 4 = cons(mark(Y),fst(X,Z))
           
           a__from(X) = X + 4 >= X + 4 = cons(mark(X),from(s(X)))
           
           a__add(0(),X) = X + 7 >= X = mark(X)
           
           a__add(s(X),Y) = 7X + Y + 7 >= 7X + Y + 7 = s(add(X,Y))
           
           a__len(nil()) = 0 >= 0 = 0()
           
           a__len(cons(X,Z)) = Z + 4 >= Z + 0 = s(len(Z))
           
           mark(fst(X1,X2)) = X1 + X2 >= X1 + X2 = a__fst(mark(X1),mark(X2))
           
           mark(from(X)) = X + 4 >= X + 4 = a__from(mark(X))
           
           mark(add(X1,X2)) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = a__add(mark(X1),mark(X2))
           
           mark(len(X)) = X + 0 >= X + 0 = a__len(mark(X))
           
           mark(0()) = 0 >= 0 = 0()
           
           mark(s(X)) = X >= X = s(X)
           
           mark(nil()) = 0 >= 0 = nil()
           
           mark(cons(X1,X2)) = X2 + 4 >= X2 + 4 = cons(mark(X1),X2)
           
           a__fst(X1,X2) = X1 + X2 >= X1 + X2 = fst(X1,X2)
           
           a__from(X) = X + 4 >= X + 4 = from(X)
           
           a__add(X1,X2) = 7X1 + X2 + 7 >= 7X1 + X2 + 7 = add(X1,X2)
           
           a__len(X) = X + 0 >= X + 0 = len(X)
          problem:
           DPs:
            a__add#(0(),X) -> mark#(X)
            mark#(add(X1,X2)) -> mark#(X2)
            mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
           TRS:
            a__fst(0(),Z) -> nil()
            a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
            a__from(X) -> cons(mark(X),from(s(X)))
            a__add(0(),X) -> mark(X)
            a__add(s(X),Y) -> s(add(X,Y))
            a__len(nil()) -> 0()
            a__len(cons(X,Z)) -> s(len(Z))
            mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
            mark(from(X)) -> a__from(mark(X))
            mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
            mark(len(X)) -> a__len(mark(X))
            mark(0()) -> 0()
            mark(s(X)) -> s(X)
            mark(nil()) -> nil()
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            a__fst(X1,X2) -> fst(X1,X2)
            a__from(X) -> from(X)
            a__add(X1,X2) -> add(X1,X2)
            a__len(X) -> len(X)
          Arctic Interpretation Processor:
           dimension: 1
           interpretation:
            [a__add#](x0, x1) = 1x0 + 6x1,
            
            [mark#](x0) = x0,
            
            [len](x0) = 4,
            
            [a__len](x0) = 4,
            
            [add](x0, x1) = 2x0 + 6x1,
            
            [a__add](x0, x1) = 2x0 + 6x1,
            
            [from](x0) = 3x0 + 2,
            
            [a__from](x0) = 3x0 + 2,
            
            [fst](x0, x1) = 4x1 + 0,
            
            [mark](x0) = x0,
            
            [cons](x0, x1) = x0 + 0,
            
            [s](x0) = x0 + 4,
            
            [nil] = 0,
            
            [a__fst](x0, x1) = 4x1 + 0,
            
            [0] = 0
           orientation:
            a__add#(0(),X) = 6X + 1 >= X = mark#(X)
            
            mark#(add(X1,X2)) = 2X1 + 6X2 >= X2 = mark#(X2)
            
            mark#(add(X1,X2)) = 2X1 + 6X2 >= 1X1 + 6X2 = a__add#(mark(X1),mark(X2))
            
            a__fst(0(),Z) = 4Z + 0 >= 0 = nil()
            
            a__fst(s(X),cons(Y,Z)) = 4Y + 4 >= Y + 0 = cons(mark(Y),fst(X,Z))
            
            a__from(X) = 3X + 2 >= X + 0 = cons(mark(X),from(s(X)))
            
            a__add(0(),X) = 6X + 2 >= X = mark(X)
            
            a__add(s(X),Y) = 2X + 6Y + 6 >= 2X + 6Y + 4 = s(add(X,Y))
            
            a__len(nil()) = 4 >= 0 = 0()
            
            a__len(cons(X,Z)) = 4 >= 4 = s(len(Z))
            
            mark(fst(X1,X2)) = 4X2 + 0 >= 4X2 + 0 = a__fst(mark(X1),mark(X2))
            
            mark(from(X)) = 3X + 2 >= 3X + 2 = a__from(mark(X))
            
            mark(add(X1,X2)) = 2X1 + 6X2 >= 2X1 + 6X2 = a__add(mark(X1),mark(X2))
            
            mark(len(X)) = 4 >= 4 = a__len(mark(X))
            
            mark(0()) = 0 >= 0 = 0()
            
            mark(s(X)) = X + 4 >= X + 4 = s(X)
            
            mark(nil()) = 0 >= 0 = nil()
            
            mark(cons(X1,X2)) = X1 + 0 >= X1 + 0 = cons(mark(X1),X2)
            
            a__fst(X1,X2) = 4X2 + 0 >= 4X2 + 0 = fst(X1,X2)
            
            a__from(X) = 3X + 2 >= 3X + 2 = from(X)
            
            a__add(X1,X2) = 2X1 + 6X2 >= 2X1 + 6X2 = add(X1,X2)
            
            a__len(X) = 4 >= 4 = len(X)
           problem:
            DPs:
             mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2))
            TRS:
             a__fst(0(),Z) -> nil()
             a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
             a__from(X) -> cons(mark(X),from(s(X)))
             a__add(0(),X) -> mark(X)
             a__add(s(X),Y) -> s(add(X,Y))
             a__len(nil()) -> 0()
             a__len(cons(X,Z)) -> s(len(Z))
             mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
             mark(from(X)) -> a__from(mark(X))
             mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
             mark(len(X)) -> a__len(mark(X))
             mark(0()) -> 0()
             mark(s(X)) -> s(X)
             mark(nil()) -> nil()
             mark(cons(X1,X2)) -> cons(mark(X1),X2)
             a__fst(X1,X2) -> fst(X1,X2)
             a__from(X) -> from(X)
             a__add(X1,X2) -> add(X1,X2)
             a__len(X) -> len(X)
           SCC Processor:
            #sccs: 0
            #rules: 0
            #arcs: 50/1