0.85/1.36	YES
0.85/1.36	
0.85/1.36	Problem:
0.85/1.36	lte(0(), n) -> true()
0.85/1.36	lte(s(m), 0()) -> false()
0.85/1.36	lte(s(m), s(n)) -> lte(m, n)
0.85/1.36	insert(nil(), m) -> cons(m, nil())
0.85/1.36	insert(cons(n, l), m) -> cons(m, cons(n, l)) <= lte(m, n) = true()
0.85/1.36	insert(cons(n, l), m) -> cons(n, insert(l, m)) <= lte(m, n) = false()
0.85/1.36	ordered(nil()) -> true()
0.85/1.36	ordered(cons(m, nil())) -> true()
0.85/1.36	ordered(cons(m, cons(n, l))) -> ordered(cons(n, l)) <= lte(m, n) = true()
0.85/1.36	ordered(cons(m, cons(n, l))) -> false() <= lte(m, n) = false()
0.85/1.36	
0.85/1.36	Proof:
0.85/1.36	This system is confluent.
0.85/1.36	By \cite{GNG13}, Theorem 9.
0.85/1.36	This system is of type 3 or smaller.
0.85/1.36	This system is deterministic.
0.85/1.36	This system is weakly left-linear.
0.85/1.36	System R transformed to optimized U(R).
0.85/1.36	This system is orthogonal.
0.85/1.36	
0.93/1.65	EOF