Quelle  complete_lattices.pvs

% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Oct 2004

complete_lattices[
  T: TYPE,
  (IMPORTING bounded_orders[T])
  <=: (complete_lattice?[T])
]: THEORY

BEGIN

  IMPORTING
%    bounded_sets[T, <=],
    complete_lower_semilattices[T, <=],
    complete_upper_semilattices[T, <=]

  every_set_is_tightly_bounded: JUDGEMENT
    set[T] SUBTYPE_OF (tightly_bounded?(<=))

END complete_lattices