0.80/1.36	YES
0.80/1.36	
0.80/1.36	Problem:
0.80/1.36	size(empty()) -> 0()
0.80/1.36	size(push(x, y)) -> s(size(x))
0.80/1.36	m() -> s(s(s(s(0()))))
0.80/1.36	pop(empty()) -> empty()
0.80/1.36	pop(push(x, y)) -> x <= le(size(x), m()) = true()
0.80/1.36	top(empty()) -> eentry()
0.80/1.36	top(push(x, y)) -> y <= le(size(x), m()) = true()
0.80/1.36	le(x, 0()) -> false()
0.80/1.36	le(0(), s(x)) -> true()
0.80/1.36	le(s(x), s(y)) -> le(x, y)
0.80/1.36	
0.80/1.37	Proof:
0.80/1.37	This system is confluent.
0.80/1.37	By \cite{GNG13}, Theorem 9.
0.80/1.37	This system is of type 3 or smaller.
0.80/1.37	This system is deterministic.
0.80/1.37	This system is weakly left-linear.
0.80/1.37	System R transformed to optimized U(R).
0.80/1.37	This system is orthogonal.
0.80/1.37	
0.88/1.71	EOF