NO

Problem:
 from(x) -> :(x,from(x))
 nat() -> from(0())
 inc(:(x,y)) -> :(s(x),inc(y))
 hd(:(x,y)) -> x
 tl(:(x,y)) -> y
 inc(tl(nat())) -> tl(inc(nat()))
 d(:(x,y)) -> :(x,:(x,d(y)))

Proof:
 Containment Processor: loop length: 1
                        terms:
                         from(x)
                        context: :(x,[])
                        substitution:
                         x -> x
  Qed