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