3.73/1.48	YES
3.73/1.48	
3.73/1.48	Problem:
3.73/1.48	isnoc(cons(y, nil())) -> tp2(nil(), y)
3.73/1.48	isnoc(cons(x, ys)) -> tp2(cons(x, xs), y) <= isnoc(ys) = tp2(xs, y)
3.73/1.48	
3.73/1.48	Proof:
3.73/1.48	This system is confluent.
3.73/1.48	By \cite{SMI95}, Corollary 4.7 or 5.3.
3.73/1.48	This system is oriented.
3.73/1.49	This system is of type 3 or smaller.
3.73/1.49	This system is right-stable.
3.73/1.49	This system is properly oriented.
3.73/1.49	This is an overlay system.
3.73/1.49	This system is left-linear.
3.73/1.49	All 2 critical pairs are trivial or infeasible.
3.73/1.49	CP: tp2(nil(), x) = tp2(cons(x, y), z') <= isnoc(nil()) = tp2(y, z'):
3.73/1.49	This critical pair is infeasible.
3.73/1.49	This critical pair is conditional.
3.73/1.49	This critical pair has some non-trivial conditions.
3.73/1.49	'tcap(conds(isnoc(nil())))' and 'conds(tp2(y, z'))' are not unifiable.
3.73/1.49	CP: tp2(cons(y, z), z') = tp2(nil(), y) <= isnoc(nil()) = tp2(z, z'):
3.73/1.49	This critical pair is infeasible.
3.73/1.49	This critical pair is conditional.
3.73/1.49	This critical pair has some non-trivial conditions.
3.73/1.49	'[\Sigma(REN(conds(isnoc(nil()))))](->^*_R_\alpha) \cap \Sigma(conds(tp2(z, z')))' is empty.
3.73/1.49	
7.96/2.41	EOF