YES

Proof:
This system is confluent.
By \cite{ALS94}, Theorem 4.1.
This system is of type 3 or smaller.
This system is strongly deterministic.
All 2 critical pairs are joinable.
tp2(nil, x) = tp2(cons(x, y), z') <= isnoc(nil) = tp2(y, z'):
This critical pair is unfeasible.
tp2(cons(y, z), z') = tp2(nil, y) <= isnoc(nil) = tp2(z, z'):
This critical pair is unfeasible.
By \cite{A14}, Theorem 11.5.9.
This system is of type 3 or smaller.
This system is deterministic.
System R transformed to V(R) + Emb.
Call external tool:
ttt2 - trs 30
Input:
  isnoc(cons(y, nil)) -> tp2(nil, y)
  isnoc(cons(x, ys)) -> tp2(cons(x, isnoc(ys)), isnoc(ys))
  isnoc(cons(x, ys)) -> isnoc(ys)
  tp2(x, y) -> x
  tp2(x, y) -> y
  cons(x, y) -> x
  cons(x, y) -> y
  isnoc(x) -> x

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