You are right that the property "x <= y == x < y \/ x = y" in
DerivedOrders.lsl is not implied by the other three axioms (which define <, >=,
and > in terms of <=).

     That property was (hastily and, as you point out, erroneously) moved from
the assertions to the implications of DerivedOrders.lsl to work around
operational problems caused by the way LP oriented the axioms of DerivedOrders
into rewrite rules.  At the time, I realized that there might be problems with
this work-around, because it wasn't clear
(a) whether there was a single best orientation for all applications, 
(b) whether the user should be given means to specify a desired orientation, or
(c) whether LP should be provided with special procedures for reasoning about
    partial orders.
My current feeling is that (c) presents the best prospects for success, but
requires the most work.

     Had the property been moved to the implications of PartialOrder.lsl or
TotalOrder.lsl, where it is known that <= if reflexive, it would have followed
from reflexivity and the remaining axioms of DerivedOrders.lsl.  I will try to
figure out how to change DerivedOrders.lsl once again (possibly back to its
original form) in order to achieve both semantic correctness and operational
					Steve Garland