YES Proof: This system is confluent. By \cite{SMI95}, Corollary 4.7 or 5.3. This system is not normal. This system is oriented. This system is of type 3 or smaller. This system is right-stable. This system is properly oriented. This is an overlay system. This system is left-linear. All 2 critical pairs are trivial or infeasible. tp2(nil, x) = tp2(cons(x, y), z') <= isnoc(nil) = tp2(y, z'): This critical pair is not trivial. This critical pair is conditional. This critical pair has some non-trivial conditions. 'tcap(?1(isnoc(nil)))' is not unifiable with '?1(tp2(y, z'))'. tp2(cons(y, z), z') = tp2(nil, y) <= isnoc(nil) = tp2(z, z'): This critical pair is not trivial. This critical pair is conditional. This critical pair has some non-trivial conditions. 'tcap(?1(isnoc(nil)))' is not unifiable with '?1(tp2(z, z'))'.