0.00/0.74 YES 0.00/0.74 0.00/0.74 Problem: 0.00/0.74 size(empty()) -> 0() 0.00/0.74 size(push(x, y)) -> s(size(x)) 0.00/0.74 m() -> s(s(s(s(0())))) 0.00/0.74 pop(empty()) -> empty() 0.00/0.74 pop(push(x, y)) -> x <= le(size(x), m()) = true() 0.00/0.74 top(empty()) -> eentry() 0.00/0.74 top(push(x, y)) -> y <= le(size(x), m()) = true() 0.00/0.74 le(x, 0()) -> false() 0.00/0.74 le(0(), s(x)) -> true() 0.00/0.74 le(s(x), s(y)) -> le(x, y) 0.00/0.74 0.00/0.74 Proof: 0.00/0.74 This system is confluent. 0.00/0.74 By \cite{SMI95}, Corollary 4.7 or 5.3. 0.00/0.74 This system is normal. 0.00/0.74 This system is of type 3 or smaller. 0.00/0.74 This system is right-stable. 0.00/0.74 This system is properly oriented. 0.00/0.74 This is an overlay system. 0.00/0.74 This system is left-linear. 0.00/0.74 All 0 critical pairs are trivial or infeasible. 0.00/0.74 1.98/1.09 EOF