YES

Problem:
 from(x) -> :(x,from(s(x)))
 sel(0(),:(y,z)) -> y
 sel(s(x),:(y,z)) -> sel(x,z)

Proof:
 Church Rosser Transformation Processor:
  strict:
   from(x) -> :(x,from(s(x)))
   sel(0(),:(y,z)) -> y
   sel(s(x),:(y,z)) -> sel(x,z)
  weak:
   
  critical peaks: 0
  Closedness Processor (*parallel*):
   strict:
    
   weak:
    
   Qed