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