Quelle  complete_lattices.prf

(complete_lattices
 (every_set_is_tightly_bounded 0
  (every_set_is_tightly_bounded-1 nil 3314557532
   ("" (skolem!)
    (("" (typepred "<=")
      (("" (expand* "tightly_bounded?" "complete_lattice?")
        (("" (prop)
          (("1" (expand "complete_upper_semilattice?")
            (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)
           ("2" (expand "complete_lower_semilattice?")
            (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((<= formal-const-decl "(complete_lattice?[T])" complete_lattices
        nil)
    (complete_lattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil complete_lattices nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (complete_upper_semilattice? const-decl "bool" bounded_orders nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (tightly_bounded? const-decl "bool" bounded_orders nil))
   nil)))