SSL directed_order_props.pvs

directed_order_props[T:TYPE,(IMPORTING directed_orders[T])
                     <=:(directed_complete_partial_order?[T])]: THEORY

BEGIN

  IMPORTING partial_order_props[T,<=],
            bounded_order_props[T,<=]

  S: VAR (nonempty?[T])

  directed?(S):bool = directed?(<=)(S)

  directed: TYPE    = (directed?)

  x,y,z:   VAR T
  D:       VAR directed
  U:       VAR upper_set
  L,L1,L2: VAR lower_set

  directed_is_lub_set: JUDGEMENT directed     SUBTYPE_OF (lub_set?)
  directed_singleton:  JUDGEMENT singleton(x) HAS_TYPE directed

  intersection_directed_upper:
       LEMMA nonempty?(intersection(U,D)) IMPLIES directed?(intersection(U,D))

  split_directed_lower: LEMMA
       member(x,D) AND member(y,D) AND member(x,L) AND NOT member(y,L) IMPLIES
          EXISTS z: x <= z AND y <= z AND member(z,D) AND NOT member(z,L)

  directed_union_lower: LEMMA
    subset?(D,union(L1,L2)) IMPLIES (subset?(D,L1) OR subset?(D,L2))


END directed_order_props