Quelle  heine_borel.prf   Sprache: Lisp

(heine_borel
 (real_heine_borel 0
  (real_heine_borel-1 nil 3397538876
   ("" (skosimp)
    (("" (expand "compact?")
      (("" (expand "compact_subset?")
        (("" (skosimp)
          ((""
            (lemma "heine_borel_aux" ("a" "a!1" "b" "b!1" "C" "U!1"))
            (("" (replace -2)
              (("" (replace -3)
                (("" (expand "open_cover?" -3)
                  (("" (flatten)
                    (("" (split -1)
                      (("1" (skosimp)
                        (("1" (inst + "U!2")
                          (("1" (assert)
                            (("1" (expand "finite_cover?")
                              (("1"
                                (hide -1 -2 -5 -6)
                                (("1"
                                  (expand "cover?")
                                  (("1" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide 2 -3)
                        (("2" (expand "every")
                          (("2" (skosimp)
                            (("2" (typepred "x!1")
                              (("2"
                                (expand "subset?")
                                (("2"
                                  (inst - "x!1")
                                  (("2"
                                    (expand "member")
                                    (("2"
                                      (expand
                                       "metric_induced_topology")
                                      (("2"
                                        (expand "open?")
                                        (("2"
                                          (expand "member")
                                          (("2"
                                            (expand
                                             "metric_induced_topology")
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((compact? const-decl "bool" topology "topology/")
    (open_cover? const-decl "bool" topology_prelim "topology/")
    (finite_cover? const-decl "bool" topology_prelim "topology/")
    (cover? const-decl "bool" topology_prelim "topology/")
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (metric_induced_topology_is_second_countable name-judgement
     "second_countable" real_topology nil)
    (metric_space_is_hausdorff? name-judgement "(hausdorff?)"
     real_topology nil)
    (metric_space_is_hausdorff name-judgement "hausdorff" real_topology
     nil)
    (every const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (metric_induced_topology const-decl "setofsets[T]" metric_space_def
     nil)
    (open? const-decl "bool" topology "topology/")
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (heine_borel_aux formula-decl nil heine_borel_scaf nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (compact_subset? const-decl "bool" topology_prelim "topology/"))
   shostak)))