YES

Proof:
This system is quasi-decreasing.
By \cite{O02}, p. 214, Proposition 7.2.50.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to U(R).
Call external tool:
ttt2 - trs 30
Input:
  isnoc(cons(y, nil)) -> tp2(nil, y)
  ?1(tp2(xs, y), x, ys) -> tp2(cons(x, xs), y)
  isnoc(cons(x, ys)) -> ?1(isnoc(ys), x, ys)

 DP Processor:
  DPs:
   isnoc#(cons(x,ys)) -> isnoc#(ys)
   isnoc#(cons(x,ys)) -> ?1#(isnoc(ys),x,ys)
  TRS:
   isnoc(cons(y,nil())) -> tp2(nil(),y)
   ?1(tp2(xs,y),x,ys) -> tp2(cons(x,xs),y)
   isnoc(cons(x,ys)) -> ?1(isnoc(ys),x,ys)
  TDG Processor:
   DPs:
    isnoc#(cons(x,ys)) -> isnoc#(ys)
    isnoc#(cons(x,ys)) -> ?1#(isnoc(ys),x,ys)
   TRS:
    isnoc(cons(y,nil())) -> tp2(nil(),y)
    ?1(tp2(xs,y),x,ys) -> tp2(cons(x,xs),y)
    isnoc(cons(x,ys)) -> ?1(isnoc(ys),x,ys)
   graph:
    isnoc#(cons(x,ys)) -> isnoc#(ys) ->
    isnoc#(cons(x,ys)) -> ?1#(isnoc(ys),x,ys)
    isnoc#(cons(x,ys)) -> isnoc#(ys) -> isnoc#(cons(x,ys)) -> isnoc#(ys)
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 2/4
    DPs:
     isnoc#(cons(x,ys)) -> isnoc#(ys)
    TRS:
     isnoc(cons(y,nil())) -> tp2(nil(),y)
     ?1(tp2(xs,y),x,ys) -> tp2(cons(x,xs),y)
     isnoc(cons(x,ys)) -> ?1(isnoc(ys),x,ys)
    Subterm Criterion Processor:
     simple projection:
      pi(isnoc#) = 0
     problem:
      DPs:
       
      TRS:
       isnoc(cons(y,nil())) -> tp2(nil(),y)
       ?1(tp2(xs,y),x,ys) -> tp2(cons(x,xs),y)
       isnoc(cons(x,ys)) -> ?1(isnoc(ys),x,ys)
     Qed