0.00/0.70 YES 0.00/0.70 0.00/0.70 Problem: 0.00/0.70 lt(x, 0()) -> false() 0.00/0.70 lt(0(), s(x)) -> true() 0.00/0.70 lt(s(x), s(y)) -> lt(x, y) 0.00/0.70 m(0(), s(y)) -> 0() 0.00/0.70 m(x, 0()) -> x 0.00/0.70 m(s(x), s(y)) -> m(x, y) 0.00/0.70 div(0(), s(x)) -> pair(0(), 0()) 0.00/0.70 div(s(x), s(y)) -> pair(0(), s(x)) <= lt(x, y) = true() 0.00/0.70 div(s(x), s(y)) -> pair(s(q), r) <= lt(x, y) = false(), div(m(x, y), s(y)) = pair(q, r) 0.00/0.70 0.00/0.70 Proof: 0.00/0.70 This system is confluent. 0.00/0.70 By \cite{GNG13}, Theorem 9. 0.00/0.70 This system is of type 3 or smaller. 0.00/0.70 This system is deterministic. 0.00/0.70 This system is weakly left-linear. 0.00/0.70 System R transformed to optimized U(R). 0.00/0.70 This system is orthogonal. 0.00/0.70 1.79/1.02 EOF