2.61/1.76	YES
2.61/1.76	
2.61/1.76	Proof:
2.61/1.76	This system is confluent.
2.61/1.76	By \cite{SMI95}, Corollary 4.7 or 5.3.
2.61/1.76	This system is oriented.
2.61/1.76	This system is of type 3 or smaller.
2.61/1.76	This system is right-stable.
2.61/1.76	This system is properly oriented.
2.61/1.76	This is an overlay system.
2.61/1.76	This system is left-linear.
2.61/1.77	All 2 critical pairs are trivial or infeasible.
2.61/1.77	Overlap: (rule1: pos(s(y)) -> true <= pos(y) = true, rule2: pos(s(0)) -> true, pos: ε, mgu: {(y,0)})
2.61/1.77	CP: true = true <= pos(0) = true
2.61/1.77	This critical pair is trivial.
2.61/1.77	Overlap: (rule1: pos(s(0)) -> true, rule2: pos(s(y)) -> true <= pos(y) = true, pos: ε, mgu: {(y,0)})
2.61/1.77	CP: true = true <= pos(0) = true
2.61/1.77	This critical pair is trivial.
2.61/1.77	
4.93/2.18	EOF