real_orders : THEORY
BEGIN

  rel       : VAR [[real,real]->bool]

  realorder?(rel) : bool = (rel = (<=)) OR (rel = (<)) OR (rel = (>=)) OR (rel = (>))
  RealOrder       : TYPE = (realorder?)
  relreal         : VAR RealOrder

  le_realorder    : JUDGEMENT <= HAS_TYPE RealOrder
  lt_realorder    : JUDGEMENT <  HAS_TYPE RealOrder
  ge_realorder    : JUDGEMENT >= HAS_TYPE RealOrder
  gt_realorder    : JUDGEMENT >  HAS_TYPE RealOrder

  neg_rel(relreal)(x,y:real): bool = 
    NOT relreal(x,y)

  neg_rel_le_gt : LEMMA
    neg_rel(<=) = >

  neg_rel_lt_ge : LEMMA
    neg_rel(<) = >=

  neg_rel_ge_lt : LEMMA
    neg_rel(>=) = <

  neg_rel_gt_le : LEMMA
    neg_rel(>) = <=

  neg_rel_order : JUDGEMENT
    neg_rel(relreal) HAS_TYPE RealOrder

  le_ne_lt : LEMMA
    NOT ((reals.<=) = (reals.<))

  le_ne_ge : LEMMA
    NOT ((reals.<=) = (reals.>=))

  le_ne_gt : LEMMA
    NOT ((reals.<=) = (reals.>))

  lt_ne_le : LEMMA
    NOT ((reals.<) = (reals.<=))

  lt_ne_ge : LEMMA
    NOT ((reals.<) = (reals.>=))

  lt_ne_gt : LEMMA
    NOT ((reals.<) = (reals.>))

  ge_ne_gt : LEMMA
    NOT ((reals.>=) = (reals.>))

  ge_ne_le : LEMMA
    NOT ((reals.>=) = (reals.<=))

  ge_ne_lt : LEMMA
    NOT ((reals.>=) = (reals.<))

  gt_ne_ge : LEMMA
    NOT ((reals.>) = (reals.>=))

  gt_ne_le : LEMMA
    NOT ((reals.>) = (reals.<=))

  gt_ne_lt : LEMMA
    NOT ((reals.>) = (reals.<))

END real_orders