0.00/0.49	YES
0.00/0.49	
0.00/0.49	Problem:
0.00/0.50	sub(z, 0()) -> z
0.00/0.50	sub(s(z), s(y)) -> x <= sub(z, y) = x
0.00/0.50	
0.00/0.50	Proof:
0.00/0.50	This system is confluent.
0.00/0.50	By \cite{GNG13}, Theorem 9.
0.00/0.50	This system is of type 3 or smaller.
0.00/0.50	This system is deterministic.
0.00/0.50	This system is weakly left-linear.
0.00/0.50	System R transformed to optimized U(R).
0.00/0.50	This system is orthogonal.
0.00/0.50	
0.00/0.77	EOF