YES

We show the termination of the TRS R:

  fst(|0|(),Z) -> nil()
  fst(s(),cons(Y)) -> cons(Y)
  from(X) -> cons(X)
  add(|0|(),X) -> X
  add(s(),Y) -> s()
  len(nil()) -> |0|()
  len(cons(X)) -> s()

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

  (no rules)

and R consists of:

r1: fst(|0|(),Z) -> nil()
r2: fst(s(),cons(Y)) -> cons(Y)
r3: from(X) -> cons(X)
r4: add(|0|(),X) -> X
r5: add(s(),Y) -> s()
r6: len(nil()) -> |0|()
r7: len(cons(X)) -> s()

The estimated dependency graph contains the following SCCs:

  (no SCCs)