0.00/0.80 YES 0.00/0.80 0.00/0.80 Problem: 0.00/0.80 le(0(), x) -> true() 0.00/0.80 le(s(x), 0()) -> false() 0.00/0.80 le(s(x), s(y)) -> le(x, y) 0.00/0.80 app(nil(), x) -> x 0.00/0.80 app(cons(x, xs), ys) -> cons(x, app(xs, ys)) 0.00/0.80 split(x, nil()) -> pair(nil(), nil()) 0.00/0.80 qsort(nil()) -> nil() 0.00/0.81 split(x, cons(y, ys)) -> pair(xs, cons(y, zs)) <= split(x, ys) = pair(xs, zs), le(x, y) = true() 0.00/0.81 split(x, cons(y, ys)) -> pair(cons(y, xs), zs) <= split(x, ys) = pair(xs, zs), le(x, y) = false() 0.00/0.81 qsort(cons(x, xs)) -> app(qsort(ys), cons(x, qsort(zs))) <= split(x, xs) = pair(ys, zs) 0.00/0.81 0.00/0.81 Proof: 0.00/0.81 This system is confluent. 0.00/0.81 By \cite{GNG13}, Theorem 9. 0.00/0.81 This system is of type 3 or smaller. 0.00/0.81 This system is deterministic. 0.00/0.81 This system is weakly left-linear. 0.00/0.81 System R transformed to optimized U(R). 0.00/0.81 This system is orthogonal. 0.00/0.81 1.51/1.12 EOF