Impressum topology.prf

(topology
 (open_set_TCC1 0
  (open_set_TCC1-1 nil 3324957210
   ("" (expand "open?")
    (("" (typepred "S")
      (("" (expand "topology?")
        (("" (expand "topology_empty?") (("" (flatten) nil nil)) nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "topology" topology nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (topology? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (topology_empty? const-decl "bool" topology_prelim nil)
    (open? const-decl "bool" topology nil))
   shostak))
 (closed_set_TCC1 0
  (closed_set_TCC1-1 nil 3324957210
   ("" (typepred "S")
    (("" (expand "closed?")
      (("" (rewrite "complement_emptyset")
        (("" (expand "topology?")
          (("" (expand "topology_full?") (("" (flatten) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((closed? const-decl "bool" topology nil)
    (topology_full? const-decl "bool" topology_prelim nil)
    (complement_emptyset formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil topology nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (topology? const-decl "bool" topology_prelim nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (S formal-const-decl "topology" topology nil))
   shostak))
 (clopen_set_TCC1 0
  (clopen_set_TCC1-1 nil 3364196997
   ("" (expand "clopen?")
    (("" (lemma "open_set_TCC1")
      (("" (lemma "closed_set_TCC1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((open_set_TCC1 subtype-tcc nil topology nil)
    (closed_set_TCC1 subtype-tcc nil topology nil)
    (clopen? const-decl "bool" topology nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   nil))
 (compact_TCC1 0
  (compact_TCC1-1 nil 3397736514
   ("" (expand "compact?")
    (("" (expand "compact_subset?")
      (("" (skosimp)
        (("" (inst + "emptyset[set[T]]")
          (("" (hide -1)
            (("" (expand "finite_cover?")
              (("" (rewrite "subset_emptyset")
                (("" (expand "cover?")
                  (("" (rewrite "subset_emptyset") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((compact_subset? const-decl "bool" topology_prelim nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (set type-eq-decl nil sets nil)
    (emptyset const-decl "set" sets nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_cover? const-decl "bool" topology_prelim nil)
    (cover? const-decl "bool" topology_prelim nil)
    (Union const-decl "set" sets nil)
    (subset_emptyset formula-decl nil sets_lemmas nil)
    (compact? const-decl "bool" topology nil))
   nil))
 (clopen_set_is_open 0
  (clopen_set_is_open-1 nil 3364196997
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "clopen?") (("" (flatten) nil nil)) nil)) nil))
    nil)
   ((clopen_set nonempty-type-eq-decl nil topology nil)
    (clopen? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (clopen_set_is_closed 0
  (clopen_set_is_closed-1 nil 3364196997
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "clopen?") (("" (flatten) nil nil)) nil)) nil))
    nil)
   ((clopen_set nonempty-type-eq-decl nil topology nil)
    (clopen? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (open_complement 0
  (open_complement-1 nil 3300504914
   ("" (expand "closed?")
    (("" (expand "member")
      (("" (expand "open?")
        (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (open? const-decl "bool" topology nil)
    (closed? const-decl "bool" topology nil))
   shostak))
 (closed_complement 0
  (closed_complement-1 nil 3300504937
   ("" (expand "closed?")
    (("" (expand "open?")
      (("" (skosimp)
        (("" (rewrite "complement_complement") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((open? const-decl "bool" topology nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (member const-decl "bool" sets nil)
    (closed? const-decl "bool" topology nil))
   shostak))
 (open_emptyset 0
  (open_emptyset-1 nil 3301114668
   ("" (expand "open?")
    (("" (typepred "S")
      (("" (expand "topology?")
        (("" (flatten)
          (("" (expand "topology_empty?") (("" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "topology" topology nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (topology? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (topology_empty? const-decl "bool" topology_prelim nil)
    (open? const-decl "bool" topology nil))
   shostak))
 (open_fullset 0
  (open_fullset-1 nil 3301114694
   ("" (expand "open?")
    (("" (typepred "S")
      (("" (expand "topology?")
        (("" (flatten)
          (("" (expand "topology_full?") (("" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "topology" topology nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (topology? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (topology_full? const-decl "bool" topology_prelim nil)
    (open? const-decl "bool" topology nil))
   shostak))
 (open_Union 0
  (open_Union-1 nil 3301114716
   ("" (skosimp)
    (("" (typepred "S")
      (("" (expand "topology?")
        (("" (flatten)
          (("" (expand "topology_Union?")
            (("" (inst - "Y!1")
              (("" (expand "open?")
                (("" (split -3)
                  (("1" (propax) nil nil)
                   ("2" (hide-all-but (-4 1))
                    (("2" (expand "subset?")
                      (("2" (skosimp)
                        (("2" (expand "every")
                          (("2" (expand "member")
                            (("2" (inst - "x!1") nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((S formal-const-decl "topology" topology nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (topology? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (subset? const-decl "bool" sets nil)
    (every const-decl "bool" sets nil)
    (Y!1 skolem-const-decl "setofsets[T]" topology nil)
    (x!1 skolem-const-decl "setof[T]" topology nil)
    (member const-decl "bool" sets nil)
    (open? const-decl "bool" topology nil)
    (topology_Union? const-decl "bool" topology_prelim nil))
   shostak))
 (open_union 0
  (open_union-1 nil 3301285730
   ("" (skosimp)
    (("" (typepred "U1!1")
      (("" (typepred "U2!1")
        (("" (name "YY" "{a:set[T] | a = U1!1 OR a = U2!1}")
          (("" (lemma "open_Union" ("Y" "YY"))
            ((""
              (lemma "extensionality"
               ("a" "Union(YY)" "b" "union(U1!1,U2!1)"))
              (("" (split -1)
                (("1" (split -2)
                  (("1" (assert) nil nil)
                   ("2" (replace -2 1 rl)
                    (("2" (hide -1 -2 2)
                      (("2" (expand "every")
                        (("2" (skosimp)
                          (("2" (typepred "x!1")
                            (("2" (split)
                              (("1" (assert) nil nil)
                               ("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (replace -2 1 rl)
                  (("2" (hide -1 -2 2)
                    (("2" (skosimp*)
                      (("2" (expand "Union")
                        (("2" (expand "union")
                          (("2" (assert)
                            (("2" (split 1)
                              (("1"
                                (skosimp*)
                                (("1"
                                  (typepred "a!1")
                                  (("1"
                                    (split -1)
                                    (("1" (assert) nil nil)
                                     ("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (flatten)
                                (("2"
                                  (split -1)
                                  (("1" (inst + "U1!1") nil nil)
                                   ("2" (inst + "U2!1") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (extensionality formula-decl nil sets_lemmas nil)
    (Union const-decl "set" sets nil) (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (every const-decl "bool" sets nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (open_Union formula-decl nil topology nil))
   shostak))
 (open_intersection 0
  (open_intersection-1 nil 3301114844
   ("" (skosimp)
    (("" (typepred "U1!1")
      (("" (typepred "U2!1")
        (("" (expand "open?")
          (("" (typepred "S")
            (("" (expand "topology?")
              (("" (flatten)
                (("" (expand "topology_intersection?")
                  (("" (inst - "U1!1" "U2!1")
                    (("1" (assert) nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (topology_intersection? const-decl "bool" topology_prelim nil)
    (member const-decl "bool" sets nil)
    (U2!1 skolem-const-decl "open" topology nil)
    (U1!1 skolem-const-decl "open" topology nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (topology? const-decl "bool" topology_prelim nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (S formal-const-decl "topology" topology nil))
   shostak))
 (open_Intersection 0
  (open_Intersection-1 nil 3301282923
   ("" (skosimp)
    (("" (name "N" "card(Y!1)")
      (("1" (lemma "Intersection_finite" ("A" "Y!1" "P" "open?"))
        (("1" (split -1)
          (("1" (propax) nil nil)
           ("2" (rewrite "open_fullset") nil nil)
           ("3" (propax) nil nil)
           ("4" (expand "every") (("4" (propax) nil nil)) nil)
           ("5" (skosimp)
            (("5" (lemma "open_intersection" ("U1" "a!1" "U2" "b!1"))
              (("1" (propax) nil nil) ("2" (propax) nil nil)
               ("3" (propax) nil nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (propax) nil nil))
      nil))
    nil)
   ((setofsets type-eq-decl nil sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (open_fullset formula-decl nil topology nil)
    (every const-decl "bool" sets nil)
    (open_intersection formula-decl nil topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (Intersection_finite formula-decl nil prelude_sets_aux nil))
   shostak))
 (closed_emptyset 0
  (closed_emptyset-1 nil 3301114927
   ("" (rewrite "open_complement" 1 :dir rl)
    (("" (rewrite "complement_emptyset")
      (("" (rewrite "open_fullset") nil nil)) nil))
    nil)
   ((complement_emptyset formula-decl nil sets_lemmas nil)
    (open_fullset formula-decl nil topology nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (open_complement formula-decl nil topology nil))
   shostak))
 (closed_fullset 0
  (closed_fullset-1 nil 3301114973
   ("" (rewrite "open_complement" 1 :dir rl)
    (("" (rewrite "complement_fullset")
      (("" (rewrite "open_emptyset") nil nil)) nil))
    nil)
   ((complement_fullset formula-decl nil sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (open_emptyset formula-decl nil topology nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (open_complement formula-decl nil topology nil))
   shostak))
 (closed_Intersection 0
  (closed_Intersection-1 nil 3301115017
   ("" (skosimp)
    (("" (rewrite "open_complement" 1 :dir rl)
      (("" (rewrite "Demorgan2")
        (("" (lemma "open_Union" ("Y" "Complement(Y!1)"))
          (("" (split)
            (("1" (propax) nil nil)
             ("2" (hide 2)
              (("2" (expand "every")
                (("2" (skosimp)
                  (("2" (typepred "x!1")
                    (("2" (expand "Complement")
                      (("2" (skosimp)
                        (("2" (typepred "b!1")
                          (("2" (inst - "b!1")
                            (("2"
                              (rewrite "open_complement" -3 :dir rl)
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open_complement formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (Intersection const-decl "set" sets nil)
    (Intersection_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (open_Union formula-decl nil topology nil)
    (Complement const-decl "setofsets[T]" sets_lemmas nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (every const-decl "bool" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (Complement_bijective name-judgement
     "(bijective?[setofsets[T], setofsets[T]])" sets_lemmas nil)
    (Demorgan2 formula-decl nil sets_lemmas nil))
   shostak))
 (closed_intersection 0
  (closed_intersection-1 nil 3301287033
   ("" (skosimp)
    (("" (typepred "V1!1")
      (("" (typepred "V2!1")
        (("" (rewrite "open_complement" :dir rl)
          (("" (rewrite "open_complement" :dir rl)
            (("" (rewrite "open_complement" :dir rl)
              (("" (rewrite "demorgan2")
                (("" (rewrite "open_union") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((closed nonempty-type-eq-decl nil topology nil)
    (closed? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (open_complement formula-decl nil topology nil)
    (intersection const-decl "set" sets nil)
    (open_union formula-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (complement const-decl "set" sets nil)
    (demorgan2 formula-decl nil sets_lemmas nil))
   shostak))
 (closed_union 0
  (closed_union-1 nil 3301115491
   ("" (skosimp)
    (("" (rewrite "open_complement" 1 :dir rl)
      (("" (rewrite "demorgan1")
        (("" (typepred "V1!1")
          (("" (typepred "V2!1")
            (("" (rewrite "open_complement" -1 :dir rl)
              (("" (rewrite "open_complement" -2 :dir rl)
                ((""
                  (lemma "open_intersection"
                   ("U1" "complement(V1!1)" "U2" "complement(V2!1)"))
                  (("1" (propax) nil nil) ("2" (propax) nil nil)
                   ("3" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open_complement formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
    (closed? const-decl "bool" topology nil)
    (closed nonempty-type-eq-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (complement const-decl "set" sets nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (open_intersection formula-decl nil topology nil)
    (demorgan1 formula-decl nil sets_lemmas nil))
   shostak))
 (closed_Union 0
  (closed_Union-1 nil 3301283172
   ("" (skosimp)
    (("" (rewrite "open_complement" 1 :dir rl)
      (("" (rewrite "Demorgan1")
        (("" (lemma "open_Intersection" ("Y" "Complement(Y!1)"))
          (("" (rewrite "finite_Complement")
            (("" (split)
              (("1" (propax) nil nil)
               ("2" (hide -1 2)
                (("2" (expand "closed?")
                  (("2" (expand "Complement")
                    (("2" (expand "every")
                      (("2" (skosimp)
                        (("2" (typepred "x!1")
                          (("2" (skosimp)
                            (("2" (inst - "b!1")
                              (("2"
                                (expand "open?")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open_complement formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (Union const-decl "set" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (open_Intersection formula-decl nil topology nil)
    (Complement const-decl "setofsets[T]" sets_lemmas nil)
    (closed? const-decl "bool" topology nil)
    (every const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (complement const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (open? const-decl "bool" topology nil)
    (finite_Complement formula-decl nil prelude_sets_aux nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (Intersection_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (Complement_bijective name-judgement
     "(bijective?[setofsets[T], setofsets[T]])" sets_lemmas nil)
    (Demorgan1 formula-decl nil sets_lemmas nil))
   shostak))
 (complement_open_is_closed 0
  (complement_open_is_closed-1 nil 3358736741
   ("" (skosimp)
    (("" (typepred "U!1")
      (("" (rewrite "closed_complement" -1 :dir rl) nil nil)) nil))
    nil)
   ((open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (closed_complement formula-decl nil topology nil))
   nil))
 (complement_closed_is_open 0
  (complement_closed_is_open-1 nil 3358736741
   ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil topology nil)
    (set type-eq-decl nil sets nil)
    (closed? const-decl "bool" topology nil)
    (closed nonempty-type-eq-decl nil topology nil)
    (member const-decl "bool" sets nil)
    (open? const-decl "bool" topology nil))
   nil))
 (emptyset_is_open 0
  (emptyset_is_open-1 nil 3358736741
   ("" (rewrite "open_emptyset") nil nil)
   ((open_emptyset formula-decl nil topology nil)) nil))
 (fullset_is_open 0
  (fullset_is_open-1 nil 3358736741
   ("" (rewrite "open_fullset") nil nil)
   ((open_fullset formula-decl nil topology nil)) nil))
 (union_is_open 0
  (union_is_open-1 nil 3358736741
   ("" (skosimp) (("" (rewrite "open_union") nil nil)) nil)
   ((open_union formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (open? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil))
   nil))
 (intersection_is_open 0
  (intersection_is_open-1 nil 3358736741
   ("" (skosimp) (("" (rewrite "open_intersection") nil nil)) nil)
   ((open_intersection formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (open? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil))
   nil))
 (emptyset_is_closed 0
  (emptyset_is_closed-1 nil 3358736741
   ("" (rewrite "closed_emptyset") nil nil)
   ((closed_emptyset formula-decl nil topology nil)) nil))
 (fullset_is_closed 0
  (fullset_is_closed-1 nil 3358736741
   ("" (rewrite "closed_fullset") nil nil)
   ((closed_fullset formula-decl nil topology nil)) nil))
 (union_is_closed 0
  (union_is_closed-1 nil 3358736741
   ("" (skosimp) (("" (rewrite "closed_union") nil nil)) nil)
   ((closed_union formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (closed? const-decl "bool" topology nil)
    (closed nonempty-type-eq-decl nil topology nil))
   nil))
 (intersection_is_closed 0
  (intersection_is_closed-1 nil 3358736741
   ("" (skosimp) (("" (rewrite "closed_intersection") nil nil)) nil)
   ((closed_intersection formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (closed? const-decl "bool" topology nil)
    (closed nonempty-type-eq-decl nil topology nil))
   nil))
 (emptyset_is_clopen 0
  (emptyset_is_clopen-1 nil 3364196997
   ("" (expand "clopen?") (("" (propax) nil nil)) nil)
   ((clopen? const-decl "bool" topology nil)
    (emptyset_is_open name-judgement "open" topology nil)
    (emptyset_is_closed name-judgement "closed" topology nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   nil))
 (fullset_is_clopen 0
  (fullset_is_clopen-1 nil 3364196997
   ("" (expand "clopen?") (("" (propax) nil nil)) nil)
   ((clopen? const-decl "bool" topology nil)
    (fullset_is_open name-judgement "open" topology nil)
    (fullset_is_closed name-judgement "closed" topology nil))
   nil))
 (indiscrete_subset 0
  (indiscrete_subset-1 nil 3325049834
   ("" (skosimp)
    (("" (typepred "t!1")
      (("" (typepred "indiscrete_topology")
        (("" (expand "subset?")
          (("" (skosimp)
            (("" (expand "member")
              (("" (expand "indiscrete_topology")
                (("" (expand "indiscrete_topology_set")
                  (("" (split -3)
                    (("1" (hide -2)
                      (("1" (rewrite "emptyset_is_empty?")
                        (("1" (replace -1)
                          (("1" (expand "topology?")
                            (("1" (flatten)
                              (("1"
                                (expand "topology_empty?")
                                (("1"
                                  (expand "member")
                                  (("1" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (rewrite "fullset_is_full?")
                      (("2" (replace -1)
                        (("2" (hide -1 -2)
                          (("2" (expand "topology?")
                            (("2" (flatten)
                              (("2"
                                (expand "topology_full?")
                                (("2"
                                  (expand "member")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((topology nonempty-type-eq-decl nil topology_prelim nil)
    (topology? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (indiscrete_topology_set const-decl "setofsets[T]" topology_prelim
     nil)
    (fullset_is_full? formula-decl nil sets_lemmas nil)
    (fullset_is_clopen name-judgement "clopen" topology nil)
    (topology_full? const-decl "bool" topology_prelim nil)
    (topology_empty? const-decl "bool" topology_prelim nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_clopen name-judgement "clopen" topology nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (set type-eq-decl nil sets nil)
    (indiscrete_topology const-decl "topology" topology_prelim nil))
   shostak))
 (discrete_subset 0
  (discrete_subset-1 nil 3325049944
   ("" (skosimp)
    (("" (typepred "t!1")
      (("" (expand "subset?")
        (("" (skosimp*)
          (("" (expand "discrete_topology")
            (("" (expand "discrete_topology_set")
              (("" (expand "fullset")
                (("" (expand "powerset")
                  (("" (expand "member")
                    (("" (expand "subset?")
                      (("" (skosimp*)
                        (("" (expand "member") (("" (propax) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((topology nonempty-type-eq-decl nil topology_prelim nil)
    (topology? const-decl "bool" topology_prelim nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (discrete_topology_set const-decl "setofsets[T]" topology_prelim
     nil)
    (powerset const-decl "setofsets" sets nil)
    (member const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (discrete_topology const-decl "topology" topology_prelim nil)
    (subset? const-decl "bool" sets nil))
   shostak))
 (open_def 0
  (open_def-1 nil 3300477193
   ("" (skosimp)
    (("" (expand "neighbourhood?")
      (("" (expand "interior_point?")
        (("" (expand "open?")
          (("" (split)
            (("1" (skosimp*)
              (("1" (typepred "x!1")
                (("1" (inst + "A!1")
                  (("1" (rewrite "subset_reflexive")
                    (("1" (expand "member") (("1" (propax) nil nil))
                      nil))
                    nil)
                   ("2" (expand "open?") (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp*)
              (("2"
                (name "Ux"
                      "{a:set[T] | open?(a) & subset?(a,A!1) & EXISTS (x:(A!1)): a(x)}")
                (("2" (case "A!1 = Union(Ux)")
                  (("1" (lemma "open_Union" ("Y" "Ux"))
                    (("1" (split -1)
                      (("1" (expand "open?") (("1" (assert) nil nil))
                        nil)
                       ("2" (hide 2)
                        (("2" (expand "every")
                          (("2" (skosimp)
                            (("2" (typepred "x!1")
                              (("2"
                                (replace -3 -1 rl)
                                (("2"
                                  (assert)
                                  (("2" (flatten) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (rewrite "extensionality" 1)
                    (("2" (replace -1 1 rl)
                      (("2" (hide -1 2 3)
                        (("2" (skosimp)
                          (("2" (expand "Union")
                            (("2" (case-replace "A!1(x!1)")
                              (("1"
                                (inst - "x!1")
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (inst + "U!1")
                                    (("1"
                                      (assert)
                                      (("1" (inst + "x!1") nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (assert)
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (typepred "a!1")
                                    (("2"
                                      (expand "subset?")
                                      (("2"
                                        (inst - "x!1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((neighbourhood? const-decl "bool" topology nil)
    (open? const-decl "bool" topology nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (Union const-decl "set" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (every const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (open_Union formula-decl nil topology nil)
    (U!1 skolem-const-decl "open" topology nil)
    (x!1 skolem-const-decl "T" topology nil)
    (extensionality formula-decl nil functions nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subset? const-decl "bool" sets nil)
    (A!1 skolem-const-decl "set[T]" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (member const-decl "bool" sets nil)
    (subset_reflexive formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil topology nil)
    (set type-eq-decl nil sets nil)
    (interior_point? const-decl "bool" topology nil))
   shostak))
 (neighbourhood_intersection 0
  (neighbourhood_intersection-1 nil 3300507815
   ("" (expand "neighbourhood?")
    (("" (expand "interior_point?")
      (("" (skosimp*)
        (("" (expand "member")
          (("" (inst + "intersection(U!1, U!2)")
            (("1" (split)
              (("1" (expand "subset?")
                (("1" (expand "intersection")
                  (("1" (skosimp*)
                    (("1" (assert)
                      (("1" (inst - "x!2")
                        (("1" (inst - "x!2")
                          (("1" (flatten)
                            (("1" (assert) (("1" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "intersection") (("2" (assert) nil nil))
                nil))
              nil)
             ("2" (expand "open?")
              (("2" (assert)
                (("2" (typepred "U!1")
                  (("2" (typepred "U!2")
                    (("2"
                      (lemma "open_intersection"
                       ("U1" "U!1" "U2" "U!2"))
                      (("2" (expand "open?")
                        (("2" (expand "member")
                          (("2" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((interior_point? const-decl "bool" topology nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (intersection const-decl "set" sets nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (intersection_is_open application-judgement "open" topology nil)
    (neighbourhood? const-decl "bool" topology nil))
   shostak))
 (neighbourhood_subset 0
  (neighbourhood_subset-1 nil 3300508120
   ("" (skosimp)
    (("" (expand "neighbourhood?")
      (("" (expand "interior_point?")
        (("" (skosimp*)
          (("" (inst + "U!1")
            ((""
              (lemma "subset_transitive"
               ("a" "U!1" "b" "A!1" "c" "B!1"))
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((neighbourhood? const-decl "bool" topology nil)
    (subset_transitive formula-decl nil sets_lemmas nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (interior_point? const-decl "bool" topology nil))
   shostak))
 (Cl_split1 0
  (Cl_split1-1 nil 3300472637
   ("" (skosimp)
    (("" (rewrite "extensionality")
      (("" (hide 2)
        (("" (skosimp)
          (("" (expand "union")
            (("" (expand "derived_set")
              (("" (expand "limit_point?")
                (("" (assert)
                  (("" (expand "Cl")
                    (("" (case-replace "A!1(x!1)")
                      (("1" (expand "adherent_point?")
                        (("1" (skosimp)
                          (("1" (expand "neighbourhood?")
                            (("1" (expand "interior_point?")
                              (("1"
                                (skosimp)
                                (("1"
                                  (expand "nonempty?")
                                  (("1"
                                    (expand "intersection")
                                    (("1"
                                      (expand "empty?")
                                      (("1"
                                        (inst - "x!1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "subset?")
                                            (("1"
                                              (inst - "x!1")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((extensionality formula-decl nil functions nil)
    (set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
    (derived_set const-decl "set[T]" topology nil)
    (Cl const-decl "set[T]" topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (interior_point? const-decl "bool" topology nil)
    (nonempty? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (neighbourhood? const-decl "bool" topology nil)
    (adherent_point? const-decl "bool" topology nil)
    (limit_point? const-decl "bool" topology nil))
   shostak))
 (Cl_split2 0
  (Cl_split2-1 nil 3300473579
   ("" (expand "disjoint?")
    (("" (expand "intersection")
      (("" (expand "derived_set")
        (("" (expand "limit_point?")
          (("" (expand "empty?")
            (("" (skosimp*)
              (("" (assert) (("" (flatten) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((intersection const-decl "set" sets nil)
    (limit_point? const-decl "bool" topology nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (derived_set const-decl "set[T]" topology nil)
    (disjoint? const-decl "bool" sets nil))
   shostak))
 (subset_of_Cl 0
  (subset_of_Cl-1 nil 3301285013
   ("" (expand "subset?")
    (("" (expand "Cl")
      (("" (skosimp*)
        (("" (assert)
          (("" (expand "adherent_point?")
            (("" (expand "nonempty?")
              (("" (skosimp*)
                (("" (typepred "U!1")
                  (("" (expand "neighbourhood?")
                    (("" (expand "interior_point?")
                      (("" (expand "empty?")
                        (("" (skosimp)
                          (("" (typepred "U!2")
                            (("" (expand "subset?")
                              ((""
                                (inst - "x!1")
                                ((""
                                  (assert)
                                  ((""
                                    (inst - "x!1")
                                    ((""
                                      (expand "intersection")
                                      (("" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Cl const-decl "set[T]" topology nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (interior_point? const-decl "bool" topology nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (neighbourhood? const-decl "bool" topology nil)
    (adherent_point? const-decl "bool" topology nil)
    (subset? const-decl "bool" sets nil))
   shostak))
 (Cl_subset 0
  (Cl_subset-1 nil 3301285299
   ("" (expand "Cl")
    (("" (expand "subset?")
      (("" (expand "member")
        (("" (expand "adherent_point?")
          (("" (expand "nonempty?")
            (("" (expand "empty?")
              (("" (expand "member")
                (("" (skosimp*)
                  (("" (inst -2 "U!1")
                    (("" (assert)
                      (("" (skosimp)
                        (("" (inst - "x!2")
                          (("" (inst - "x!2")
                            (("" (expand "intersection")
                              ((""
                                (flatten)
                                (("" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (adherent_point? const-decl "bool" topology nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (Cl const-decl "set[T]" topology nil))
   shostak))
 (Cl_idempotent 0
  (Cl_idempotent-1 nil 3301287365
   ("" (skosimp)
    (("" (lemma "subset_of_Cl" ("A" "Cl(A!1)"))
      (("" (case "subset?(Cl(Cl(A!1)), Cl(A!1))")
        (("1"
          (lemma "subset_antisymmetric"
           ("a" "Cl(A!1)" "b" "Cl(Cl(A!1))"))
          (("1" (assert) nil nil)) nil)
         ("2" (hide 2)
          (("2" (expand "subset?")
            (("2" (expand "Cl")
              (("2" (expand "adherent_point?")
                (("2" (assert)
                  (("2" (skosimp*)
                    (("2" (inst - "U!1")
                      (("2" (expand "nonempty?")
                        (("2" (expand "empty?")
                          (("2" (expand "intersection")
                            (("2" (assert)
                              (("2"
                                (expand "neighbourhood?")
                                (("2"
                                  (expand "interior_point?")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (inst -2 "U!1")
                                        (("2"
                                          (hide -6)
                                          (("2"
                                            (split -2)
                                            (("1" (propax) nil nil)
                                             ("2"
                                              (inst + "U!1")
                                              (("2"
                                                (rewrite
                                                 "subset_reflexive")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Cl const-decl "set[T]" topology nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (subset_of_Cl formula-decl nil topology nil)
    (member const-decl "bool" sets nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (empty? const-decl "bool" sets nil)
    (interior_point? const-decl "bool" topology nil)
    (subset_reflexive formula-decl nil sets_lemmas nil)
    (neighbourhood? const-decl "bool" topology nil)
    (intersection const-decl "set" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (adherent_point? const-decl "bool" topology nil)
    (subset_antisymmetric formula-decl nil sets_lemmas nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset? const-decl "bool" sets nil))
   shostak))
 (eq_Cl_is_closed 0
  (eq_Cl_is_closed-1 nil 3301290171
   ("" (skosimp)
    (("" (lemma "subset_of_Cl" ("A" "A!1"))
      (("" (case-replace "subset?(Cl(A!1),A!1) IFF closed?(A!1)")
        (("1" (rewrite "subset_antisymmetric" 1 :dir rl)
          (("1" (assert) nil nil)) nil)
         ("2" (hide -1 2)
          (("2" (rewrite "open_complement" :dir rl)
            (("2" (rewrite "subset_complement" :dir rl)
              (("2" (lemma "open_def" ("A" "complement(A!1)"))
                (("2" (split 1)
                  (("1" (flatten 1)
                    (("1" (assert)
                      (("1" (skosimp)
                        (("1" (expand "neighbourhood?")
                          (("1" (expand "subset?")
                            (("1" (expand "Cl")
                              (("1"
                                (expand "interior_point?")
                                (("1"
                                  (inst - "x!1")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (expand "complement")
                                      (("1"
                                        (expand "member")
                                        (("1"
                                          (expand "adherent_point?")
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (inst + "U!1")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (expand
                                                   "neighbourhood?")
                                                  (("1"
                                                    (expand
                                                     "interior_point?")
                                                    (("1"
                                                      (skosimp*)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (expand
                                                           "subset?")
                                                          (("1"
                                                            (inst-cp
                                                             -
                                                             "x!1")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (skosimp)
                                                                (("1"
                                                                  (expand
                                                                   "nonempty?")
                                                                  (("1"
                                                                    (expand
                                                                     "empty?")
                                                                    (("1"
                                                                      (expand
                                                                       "intersection")
                                                                      (("1"
                                                                        (inst
                                                                         -4
                                                                         "x!2")
                                                                        (("1"
                                                                          (assert)
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (flatten 1)
                    (("2" (assert)
                      (("2" (expand "subset?")
                        (("2" (skosimp*)
                          (("2" (assert)
                            (("2" (inst - "x!1")
                              (("2"
                                (expand "Cl")
                                (("2"
                                  (expand "complement")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (expand "adherent_point?")
                                      (("2"
                                        (inst - "{x: T | NOT A!1(x)}")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (expand "nonempty?")
                                            (("2"
                                              (expand "empty?")
                                              (("2"
                                                (expand "intersection")
                                                (("2"
                                                  (skosimp*)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (flatten)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (subset_of_Cl formula-decl nil topology nil)
    (subset_complement formula-decl nil sets_lemmas nil)
    (neighbourhood? const-decl "bool" topology nil)
    (adherent_point? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (nonempty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (interior_point? const-decl "bool" topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (complement const-decl "set" sets nil)
    (open_def formula-decl nil topology nil)
    (open_complement formula-decl nil topology nil)
    (subset_antisymmetric formula-decl nil sets_lemmas nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (closed? const-decl "bool" topology nil)
    (Cl const-decl "set[T]" topology nil)
    (subset? const-decl "bool" sets nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
 (Cl_closed 0
  (Cl_closed-1 nil 3300509409
   ("" (skosimp)
    (("" (lemma "eq_Cl_is_closed" ("A" "Cl(A!1)"))
      (("" (rewrite "Cl_idempotent") (("" (flatten) nil nil)) nil))
      nil))
    nil)
   ((Cl const-decl "set[T]" topology nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (eq_Cl_is_closed formula-decl nil topology nil)
    (Cl_idempotent formula-decl nil topology nil))
   shostak))
 (Cl_subset_closed 0
  (Cl_subset_closed-1 nil 3301293173
   ("" (skosimp)
    (("" (typepred "V!1")
      (("" (rewrite "eq_Cl_is_closed" -1 :dir rl)
        (("" (lemma "Cl_subset" ("A" "A!1" "B" "V!1"))
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((closed nonempty-type-eq-decl nil topology nil)
    (closed? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Cl_subset formula-decl nil topology nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (eq_Cl_is_closed formula-decl nil topology nil))
   shostak))
 (Cl_union 0
  (Cl_union-1 nil 3301293398
   ("" (skosimp)
    (("" (lemma "subset_of_Cl" ("A" "A!1"))
      (("" (lemma "subset_of_Cl" ("A" "B!1"))
        (("" (lemma "Cl_closed" ("A" "A!1"))
          (("" (lemma "Cl_closed" ("A" "B!1"))
            (("" (lemma "closed_union" ("V1" "Cl(A!1)" "V2" "Cl(B!1)"))
              (("1"
                (lemma "union_upper_bound"
                 ("a" "A!1" "b" "B!1" "c" "union(Cl(A!1), Cl(B!1))"))
                (("1" (split -1)
                  (("1"
                    (lemma "Cl_subset_closed"
                     ("A" "union(A!1,B!1)" "V"
                      "union(Cl(A!1),Cl(B!1))"))
                    (("1" (assert)
                      (("1"
                        (lemma "subset_antisymmetric"
                         ("a" "Cl(union(A!1,B!1))" "b"
                          "union(Cl(A!1),Cl(B!1))"))
                        (("1" (assert)
                          (("1" (hide 2)
                            (("1" (expand "subset?")
                              (("1"
                                (expand "union")
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (inst - "x!1")
                                      (("1"
                                        (inst - "x!1")
                                        (("1"
                                          (split -1)
                                          (("1"
                                            (expand "Cl")
                                            (("1"
                                              (hide-all-but (-1 1))
                                              (("1"
                                                (expand
                                                 "adherent_point?")
                                                (("1"
                                                  (skosimp)
                                                  (("1"
                                                    (inst - "U!1")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (expand
                                                         "nonempty?")
                                                        (("1"
                                                          (expand
                                                           "empty?")
                                                          (("1"
                                                            (expand
                                                             "intersection")
                                                            (("1"
                                                              (skosimp*)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (flatten)
                                                                  (("1"
                                                                    (inst
                                                                     -
                                                                     "x!2")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide-all-but (-1 1))
                                            (("2"
                                              (expand "Cl")
                                              (("2"
                                                (expand
                                                 "adherent_point?")
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (inst - "U!1")
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (hide -2)
                                                        (("2"
                                                          (expand
                                                           "nonempty?")
                                                          (("2"
                                                            (expand
                                                             "empty?")
                                                            (("2"
                                                              (expand
                                                               "intersection")
                                                              (("2"
                                                                (skosimp*)
                                                                (("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (flatten)
                                                                    (("2"
                                                                      (inst
                                                                       -
                                                                       "x!2")
                                                                      (("2"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (propax) nil nil))
                    nil)
                   ("2"
                    (lemma "union_subset1"
                     ("a" "Cl(A!1)" "b" "Cl(B!1)"))
                    (("2" (assert)
                      (("2"
                        (lemma "subset_transitive"
                         ("a" "A!1" "b" "Cl(A!1)" "c"
                          "union(Cl(A!1), Cl(B!1))"))
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil)
                   ("3"
                    (lemma "subset_transitive"
                     ("a" "B!1" "b" "Cl(B!1)" "c"
                      "union(Cl(A!1), Cl(B!1))"))
                    (("3" (rewrite "union_commutative" -1)
                      (("3" (rewrite "union_subset1" -1)
                        (("3" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (propax) nil nil) ("3" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil topology nil)
    (subset_of_Cl formula-decl nil topology nil)
    (Cl_closed formula-decl nil topology nil)
    (Cl const-decl "set[T]" topology nil)
    (closed nonempty-type-eq-decl nil topology nil)
    (closed? const-decl "bool" topology nil)
    (closed_union formula-decl nil topology nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (open? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (adherent_point? const-decl "bool" topology nil)
    (member const-decl "bool" sets nil)
    (subset_antisymmetric formula-decl nil sets_lemmas nil)
    (Cl_subset_closed formula-decl nil topology nil)
    (subset_transitive formula-decl nil sets_lemmas nil)
    (union_subset1 formula-decl nil sets_lemmas nil)
    (union_commutative formula-decl nil sets_lemmas nil)
    (union const-decl "set" sets nil)
    (union_upper_bound formula-decl nil sets_lemmas nil))
   shostak))
 (Cl_Union 0
  (Cl_Union-1 nil 3301310768
   (""
    (case "FORALL (Y: setofsets[T], n: nat):
        is_finite(Y) => (card(Y) = n => Cl(Union(Y)) = Union(image(Cl, Y)))")
    (("1" (skosimp)
      (("1" (inst - "Y!1" "card(Y!1)") (("1" (assert) nil nil)) nil))
      nil)
     ("2" (hide 2)
      (("2" (induct "n")
        (("1" (skosimp)
          (("1" (rewrite "card_is_0")
            (("1" (lemma "emptyset_is_empty?" ("a" "Y!1"))
              (("1" (assert)
                (("1" (lemma "Union_empty" ("A" "Y!1"))
                  (("1" (assert)
                    (("1" (rewrite "emptyset_is_empty?" -1)
                      (("1" (replace -1)
                        (("1"
                          (lemma "eq_Cl_is_closed" ("A" "emptyset[T]"))
                          (("1" (rewrite "closed_emptyset")
                            (("1" (assert)
                              (("1"
                                (replace -1 * rl)
                                (("1"
                                  (expand "image")
                                  (("1"
                                    (apply-extensionality 1 :hide? t)
                                    (("1"
                                      (expand "Union")
                                      (("1"
                                        (expand "emptyset")
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (typepred "a!1")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (typepred "x!2")
                                                  (("1"
                                                    (expand "empty?")
                                                    (("1"
                                                      (inst - "x!2")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (lemma "nonempty_card" ("S" "Y!1"))
            (("1" (assert)
              (("1" (lemma "Union_split" ("A" "Y!1"))
                (("1" (assert)
                  (("1" (lemma "card_rest" ("S" "Y!1"))
                    (("1" (split -1)
                      (("1" (replace -6 -1)
                        (("1" (assert)
                          (("1" (inst - "rest(Y!1)")
                            (("1" (assert)
                              (("1"
                                (lemma "finite_rest" ("A" "Y!1"))
                                (("1"
                                  (assert)
                                  (("1"
                                    (replace -3 1)
                                    (("1"
                                      (rewrite "Cl_union" 1)
                                      (("1"
                                        (replace -5)
                                        (("1"
                                          (hide-all-but (-4 1))
                                          (("1"
                                            (apply-extensionality
                                             :hide?
                                             t)
                                            (("1"
                                              (expand "image")
                                              (("1"
                                                (expand "Union")
                                                (("1"
                                                  (expand "union")
                                                  (("1"
                                                    (case-replace
                                                     "EXISTS (a: ({y: set[T] | EXISTS (x: (Y!1)): y = Cl(x)})): a(x!1)")
                                                    (("1"
                                                      (skosimp*)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (typepred
                                                           "a!1")
                                                          (("1"
                                                            (skosimp)
                                                            (("1"
                                                              (case-replace
                                                               "x!2=choose(Y!1)")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (inst
                                                                 +
                                                                 "a!1")
                                                                (("2"
                                                                  (inst
                                                                   +
                                                                   "x!2")
                                                                  (("2"
                                                                    (expand
                                                                     "rest")
                                                                    (("2"
                                                                      (expand
                                                                       "nonempty?")
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (expand
                                                                           "remove")
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (replace 1 2)
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (split)
                                                          (("1"
                                                            (typepred
                                                             "choose(Y!1)")
                                                            (("1"
                                                              (inst
                                                               +
                                                               "Cl(choose(Y!1))")
                                                              (("1"
                                                                (inst
                                                                 +
                                                                 "choose(Y!1)")
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (skosimp)
                                                            (("2"
                                                              (typepred
                                                               "a!1")
                                                              (("2"
                                                                (skosimp)
                                                                (("2"
                                                                  (inst
                                                                   +
                                                                   "a!1")
                                                                  (("2"
                                                                    (inst
                                                                     +
                                                                     "x!2")
                                                                    (("2"
                                                                      (typepred
                                                                       "x!2")
                                                                      (("2"
                                                                        (expand
                                                                         "rest")
                                                                        (("2"
                                                                          (expand
                                                                           "nonempty?")
                                                                          (("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (expand
                                                                               "remove")
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (expand "nonempty?")
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (Cl_union formula-decl nil topology nil)
    (a!1 skolem-const-decl
     "({y: set[T] | EXISTS (x: (rest(Y!1))): y = Cl(x)})" topology nil)
    (x!2 skolem-const-decl "(rest(Y!1))" topology nil)
    (x!2 skolem-const-decl "(Y!1)" topology nil)
    (remove const-decl "set" sets nil)
    (a!1 skolem-const-decl
     "({y: set[T] | EXISTS (x: (Y!1)): y = Cl(x)})" topology nil)
    (Y!1 skolem-const-decl "setofsets[T]" topology nil)
    (union const-decl "set" sets nil)
    (finite_rest judgement-tcc nil finite_sets nil)
    (rest const-decl "set" sets nil)
    (card_rest formula-decl nil finite_sets nil)
    (Union_split formula-decl nil prelude_sets_aux nil)
    (nonempty_card formula-decl nil finite_sets nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (Union_empty formula-decl nil sets_lemmas nil)
    (emptyset_is_clopen name-judgement "clopen" topology nil)
    (eq_Cl_is_closed formula-decl nil topology nil)
    (emptyset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (closed_emptyset formula-decl nil topology nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (card_is_0 formula-decl nil finite_sets nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (Y!1 skolem-const-decl "setofsets[T]" topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (number nonempty-type-decl nil numbers 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Cl const-decl "set[T]" topology nil)
    (Union const-decl "set" sets nil)
    (image const-decl "set[R]" function_image nil))
   shostak))
 (Cl_Intersection 0
  (Cl_Intersection-1 nil 3301310349
   ("" (expand "Intersection")
    (("" (expand "subset?")
      (("" (skosimp*)
        (("" (expand "member")
          (("" (skosimp)
            (("" (typepred "a!1")
              (("" (expand "image")
                (("" (skosimp)
                  (("" (replace -1 1)
                    (("" (expand "Cl")
                      (("" (typepred "x!2")
                        (("" (expand "adherent_point?")
                          (("" (skosimp)
                            (("" (inst - "U!1")
                              ((""
                                (assert)
                                ((""
                                  (expand "nonempty?")
                                  ((""
                                    (expand "intersection")
                                    ((""
                                      (expand "empty?")
                                      ((""
                                        (skosimp*)
                                        ((""
                                          (inst - "x!3")
                                          ((""
                                            (assert)
                                            ((""
                                              (flatten)
                                              ((""
                                                (inst - "x!2")
                                                (("" (assert) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (Cl const-decl "set[T]" topology nil)
    (image const-decl "set[R]" function_image nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (adherent_point? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (nonempty? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (Intersection const-decl "set" sets nil))
   shostak))
 (open_difference 0
  (open_difference-1 nil 3301163217
   ("" (skosimp)
    (("" (typepred "U!1")
      (("" (typepred "V!1")
        (("" (rewrite "difference_intersection")
          (("" (rewrite "open_complement" -1 :dir rl)
            ((""
              (lemma "open_intersection"
               ("U1" "U!1" "U2" "complement(V!1)"))
              (("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (difference_intersection formula-decl nil sets_lemmas nil)
    (complement_closed_is_open application-judgement "open" topology
     nil)
    (intersection_is_open application-judgement "open" topology nil)
    (open_intersection formula-decl nil topology nil)
    (complement const-decl "set" sets nil)
    (open_complement formula-decl nil topology nil)
    (closed? const-decl "bool" topology nil)
    (closed nonempty-type-eq-decl nil topology nil))
   shostak))
 (closed_difference 0
  (closed_difference-1 nil 3301163456
   ("" (skosimp)
    (("" (rewrite "open_complement" 1 :dir rl)
      (("" (rewrite "complement_difference")
        (("" (typepred "U!1")
          (("" (typepred "V!1")
            (("" (rewrite "open_complement" -1 :dir rl)
              (("" (rewrite "open_union") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((open_complement formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (difference const-decl "set" sets nil)
    (closed? const-decl "bool" topology nil)
    (closed nonempty-type-eq-decl nil topology nil)
    (open? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (open_union formula-decl nil topology nil)
    (complement const-decl "set" sets nil)
    (union_is_open application-judgement "open" topology nil)
    (complement_closed_is_open application-judgement "open" topology
     nil)
    (complement_difference formula-decl nil prelude_sets_aux nil))
   shostak))
 (Cl_is_closed 0
  (Cl_is_closed-1 nil 3358737375
   ("" (skosimp) (("" (rewrite "Cl_closed") nil nil)) nil)
   ((Cl_closed formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil))
   nil))
 (open_diff_closed_is_open 0
  (open_diff_closed_is_open-1 nil 3358737157
   ("" (skosimp) (("" (rewrite "open_difference") nil nil)) nil)
   ((open_difference formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (open? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (closed? const-decl "bool" topology nil)
    (closed nonempty-type-eq-decl nil topology nil))
   nil))
 (closed_diff_open_is_closed 0
  (closed_diff_open_is_closed-1 nil 3358737157
   ("" (skosimp) (("" (rewrite "closed_difference") nil nil)) nil)
   ((closed_difference formula-decl nil topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (open? const-decl "bool" topology nil)
    (open nonempty-type-eq-decl nil topology nil)
    (closed? const-decl "bool" topology nil)
    (closed nonempty-type-eq-decl nil topology nil))
   nil))
 (emptyset_is_compact 0
  (emptyset_is_compact-1 nil 3397736514
   ("" (lemma "compact_TCC1") (("" (propax) nil nil)) nil)
   ((compact_TCC1 subtype-tcc nil topology nil)) nil))
 (singleton_is_compact 0
  (singleton_is_compact-1 nil 3397736514
   ("" (skosimp)
    (("" (expand "compact?")
      (("" (expand "compact_subset?")
        (("" (skosimp)
          (("" (expand "open_cover?")
            (("" (flatten)
              (("" (expand "cover?")
                (("" (expand "subset?")
                  (("" (expand "member")
                    (("" (inst -2 "x!1")
                      (("" (expand "singleton" -2)
                        (("" (hide -1)
                          (("" (expand "Union")
                            (("" (skosimp)
                              ((""
                                (typepred "a!1")
                                ((""
                                  (inst + "singleton[set[T]](a!1)")
                                  ((""
                                    (split)
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (expand "singleton")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (expand "finite_cover?")
                                      (("2"
                                        (expand "cover?")
                                        (("2"
                                          (expand "subset?")
                                          (("2"
                                            (expand "member")
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (expand "singleton")
                                                (("2"
                                                  (replace -1)
                                                  (("2"
                                                    (expand "Union")
                                                    (("2"
                                                      (inst + "a!1")
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                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 nil)
    (subset? const-decl "bool" sets nil)
    (T formal-type-decl nil topology nil)
    (singleton? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (finite_cover? const-decl "bool" topology_prelim nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Union const-decl "set" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (member const-decl "bool" sets nil)
    (cover? const-decl "bool" topology_prelim nil)
    (open_cover? const-decl "bool" topology_prelim nil)
    (compact_subset? const-decl "bool" topology_prelim nil))
   nil))
 (union_is_compact 0
  (union_is_compact-1 nil 3397736514
   ("" (skosimp)
    (("" (typepred "C1!1")
      (("" (typepred "C2!1")
        (("" (expand "compact?")
          (("" (expand "compact_subset?")
            (("" (skosimp)
              (("" (inst - "U!1")
                (("" (inst - "U!1")
                  (("" (expand "open_cover?")
                    (("" (flatten)
                      (("" (assert)
                        (("" (expand "union" -4)
                          (("" (expand "cover?")
                            (("" (expand "member")
                              ((""
                                (hide -3)
                                ((""
                                  (expand "subset?" -1 1)
                                  ((""
                                    (expand "subset?" -2 1)
                                    ((""
                                      (expand "subset?" -3 1)
                                      ((""
                                        (expand "member")
                                        ((""
                                          (split -1)
                                          (("1"
                                            (split -2)
                                            (("1"
                                              (hide -3)
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (inst
                                                   +
                                                   "union(V!1,V!2)")
                                                  (("1"
                                                    (split)
                                                    (("1"
                                                      (hide -2 -4)
                                                      (("1"
                                                        (expand
                                                         "union")
                                                        (("1"
                                                          (expand
                                                           "subset?")
                                                          (("1"
                                                            (expand
                                                             "member")
                                                            (("1"
                                                              (skosimp)
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "x!1")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "x!1")
                                                                  (("1"
                                                                    (split
                                                                     -1)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (expand
                                                       "finite_cover?")
                                                      (("2"
                                                        (flatten)
                                                        (("2"
                                                          (split)
                                                          (("1"
                                                            (rewrite
                                                             "finite_union"
                                                             1)
                                                            nil
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "cover?")
                                                            (("2"
                                                              (hide-all-but
                                                               (-3
                                                                -6
                                                                1))
                                                              (("2"
                                                                (expand
                                                                 "subset?")
                                                                (("2"
                                                                  (expand
                                                                   "union")
                                                                  (("2"
                                                                    (expand
                                                                     "member")
                                                                    (("2"
                                                                      (expand
                                                                       "Union")
                                                                      (("2"
                                                                        (skosimp)
                                                                        (("2"
                                                                          (inst
                                                                           -
                                                                           "x!1")
                                                                          (("2"
                                                                            (inst
                                                                             -
                                                                             "x!1")
                                                                            (("2"
                                                                              (split)
                                                                              (("1"
                                                                                (assert)
                                                                                (("1"
                                                                                  (skosimp)
                                                                                  (("1"
                                                                                    (inst
                                                                                     +
                                                                                     "a!1")
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (assert)
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (inst
                                                                                     +
                                                                                     "a!1")
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (skosimp)
                                              (("2"
                                                (inst - "x!1")
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (skosimp)
                                            (("2"
                                              (inst -3 "x!1")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((compact nonempty-type-eq-decl nil topology nil)
    (compact? const-decl "bool" topology nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (finite_cover? const-decl "bool" topology_prelim nil)
    (finite_union judgement-tcc nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (Union const-decl "set" sets nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (cover? const-decl "bool" topology_prelim nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (open_cover? const-decl "bool" topology_prelim nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (compact_subset? const-decl "bool" topology_prelim nil))
   nil))
 (finite_is_compact 0
  (finite_is_compact-1 nil 3397736514
   (""
    (case "forall (X:finite_set[T],n:nat): card[T](X) = n => compact?(X)")
    (("1" (skosimp) (("1" (inst - "x!1" "card[T](x!1)") nil nil)) nil)
     ("2" (hide 2)
      (("2" (induct "n")
        (("1" (skosimp)
          (("1" (rewrite "card_is_0[T]")
            (("1" (replace -1)
              (("1" (rewrite "emptyset_is_compact") nil nil)) nil))
            nil))
          nil)
         ("2" (skosimp)
          (("2" (skosimp)
            (("2" (lemma "nonempty_card[T]" ("S" "X!1"))
              (("2" (assert)
                (("2" (lemma "card_rest[T]" ("S" "X!1"))
                  (("2" (lemma "choose_rest[T]" ("a" "X!1"))
                    (("2" (expand "nonempty?")
                      (("2" (assert)
                        (("2" (replace -4)
                          (("2" (inst - "rest[T](X!1)")
                            (("2" (assert)
                              (("2"
                                (lemma
                                 "singleton_is_compact"
                                 ("x" "choose(X!1)"))
                                (("2"
                                  (rewrite "add_as_union[T]")
                                  (("2"
                                    (lemma
                                     "union_is_compact"
                                     ("C1"
                                      "rest[T](X!1)"
                                      "C2"
                                      "singleton[T](choose[T](X!1))"))
                                    (("2"
                                      (replace -3)
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty_card formula-decl nil finite_sets nil)
    (card_rest formula-decl nil finite_sets nil)
    (nonempty? const-decl "bool" sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nonempty_add_finite application-judgement "non_empty_finite_set"
     finite_sets nil)
    (add_as_union formula-decl nil sets_lemmas nil)
    (singleton_is_compact application-judgement "compact" topology nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (finite_union application-judgement "finite_set" finite_sets nil)
    (nonempty_finite_union2 application-judgement
     "non_empty_finite_set" finite_sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (compact nonempty-type-eq-decl nil topology nil)
    (union_is_compact judgement-tcc nil topology nil)
    (choose const-decl "(p)" sets nil)
    (singleton_is_compact judgement-tcc nil topology nil)
    (rest const-decl "set" sets nil)
    (finite_rest application-judgement "finite_set" finite_sets nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (choose_rest formula-decl nil sets_lemmas nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (emptyset_is_compact judgement-tcc nil topology nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_compact name-judgement "compact" topology nil)
    (emptyset_is_clopen name-judgement "clopen" topology nil)
    (card_is_0 formula-decl nil finite_sets nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (number nonempty-type-decl nil numbers 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (compact? const-decl "bool" topology nil))
   nil))
 (compact_Union 0
  (compact_Union-1 nil 3397737817
   (""
    (case "FORALL (Y: setofsets[T],n:nat):
        is_finite(Y) AND card[set[T]](Y) = n & every(compact?, Y) => compact?(Union(Y))")
    (("1" (skosimp)
      (("1" (inst - "Y!1" "card[set[T]](Y!1)") (("1" (assert) nil nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (induct "n")
        (("1" (skosimp)
          (("1" (rewrite "card_is_0[set[T]]")
            (("1" (replace -2)
              (("1"
                (case-replace "Union(emptyset[set[T]])=emptyset[T]")
                (("1" (rewrite "emptyset_is_compact") nil nil)
                 ("2" (hide-all-but 1)
                  (("2" (apply-extensionality :hide? t)
                    (("2" (expand "emptyset")
                      (("2" (expand "Union") (("2" (skosimp) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (lemma "nonempty_card[set[T]]" ("S" "Y!1"))
            (("2" (assert)
              (("2" (expand "nonempty?")
                (("2" (lemma "choose_rest[set[T]]" ("a" "Y!1"))
                  (("2" (lemma "card_rest[set[T]]" ("S" "Y!1"))
                    (("2" (assert)
                      (("2" (replace -5)
                        (("2" (assert)
                          (("2" (inst - "rest[set[T]](Y!1)")
                            (("2" (assert)
                              (("2"
                                (rewrite "finite_rest[set[T]]")
                                (("2"
                                  (split -3)
                                  (("1"
                                    (expand "every")
                                    (("1"
                                      (inst - "choose[set[T]](Y!1)")
                                      (("1"
                                        (lemma
                                         "union_is_compact"
                                         ("C1"
                                          "Union(rest[set[T]](Y!1))"
                                          "C2"
                                          "choose[set[T]](Y!1)"))
                                        (("1"
                                          (case-replace
                                           "union[T](Union(rest[set[T]](Y!1)), choose[set[T]](Y!1))=Union(Y!1)")
                                          (("1"
                                            (hide-all-but (1 2 -4))
                                            (("1"
                                              (apply-extensionality
                                               :hide?
                                               t)
                                              (("1"
                                                (expand "union")
                                                (("1"
                                                  (expand "member")
                                                  (("1"
                                                    (case-replace
                                                     "Union(Y!1)(x!1)")
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (expand
                                                         "Union")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (inst
                                                             +
                                                             "a!1")
                                                            (("1"
                                                              (expand
                                                               "rest")
                                                              (("1"
                                                                (expand
                                                                 "remove")
                                                                (("1"
                                                                  (expand
                                                                   "member")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (replace 1 2)
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (expand
                                                           "Union")
                                                          (("2"
                                                            (split)
                                                            (("1"
                                                              (skosimp)
                                                              (("1"
                                                                (inst
                                                                 +
                                                                 "a!1")
                                                                (("1"
                                                                  (typepred
                                                                   "a!1")
                                                                  (("1"
                                                                    (expand
                                                                     "rest")
                                                                    (("1"
                                                                      (expand
                                                                       "remove")
                                                                      (("1"
                                                                        (expand
                                                                         "member")
                                                                        (("1"
                                                                          (flatten)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (inst
                                                               +
                                                               "choose[set[T]](Y!1)")
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2" (propax) nil nil)
                                         ("3" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide-all-but (-5 1))
                                    (("2"
                                      (expand "every")
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (typepred "x!1")
                                          (("2"
                                            (expand "rest")
                                            (("2"
                                              (expand "remove")
                                              (("2"
                                                (expand "member")
                                                (("2"
                                                  (flatten)
                                                  (("2"
                                                    (inst - "x!1")
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (choose_rest formula-decl nil sets_lemmas nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (choose const-decl "(p)" sets nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (a!1 skolem-const-decl "(rest[set[T]](Y!1))" topology nil)
    (remove const-decl "set" sets nil)
    (a!1 skolem-const-decl "(Y!1)" topology nil)
    (Y!1 skolem-const-decl "setofsets[T]" topology nil)
    (compact nonempty-type-eq-decl nil topology nil)
    (union_is_compact judgement-tcc nil topology nil)
    (x!1 skolem-const-decl "(rest[set[T]](Y!1))" topology nil)
    (finite_rest judgement-tcc nil finite_sets nil)
    (rest const-decl "set" sets nil)
    (card_rest formula-decl nil finite_sets nil)
    (nonempty? const-decl "bool" sets nil)
    (nonempty_card formula-decl nil finite_sets nil)
    (emptyset_is_compact judgement-tcc nil topology nil)
    (emptyset_is_compact name-judgement "compact" topology nil)
    (emptyset_is_clopen name-judgement "clopen" topology nil)
    (emptyset const-decl "set" sets nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (card_is_0 formula-decl nil finite_sets nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (Y!1 skolem-const-decl "setofsets[T]" topology nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (number nonempty-type-decl nil numbers 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (PRED type-eq-decl nil defined_types nil)
    (every const-decl "bool" sets nil)
    (compact? const-decl "bool" topology nil)
    (Union const-decl "set" sets nil))
   shostak))
 (compact_def 0
  (compact_def-1 nil 3406901412
   ("" (expand "compact_space?")
    (("" (expand "compact_subset?")
      (("" (split)
        (("1" (skosimp*)
          (("1" (expand "nonempty?" 1)
            (("1" (inst - "Complement(Y!1)")
              (("1"
                (case-replace
                 "open_cover?(Complement(Y!1), Union(S), S)")
                (("1" (skosimp)
                  (("1" (inst - "Complement(V!1)")
                    (("1"
                      (case-replace
                       "subset?(Complement(V!1), Y!1) AND is_finite(Complement(V!1))")
                      (("1" (flatten)
                        (("1" (expand "nonempty?")
                          (("1" (expand "finite_cover?")
                            (("1" (expand "open_cover?")
                              (("1"
                                (flatten)
                                (("1"
                                  (rewrite "Demorgan1" 1 :dir rl)
                                  (("1"
                                    (rewrite "emptyset_is_empty?" 1)
                                    (("1"
                                      (lemma
                                       "complement_equal"
                                       ("a"
                                        "complement(Union(V!1))"
                                        "b"
                                        "emptyset[T]"))
                                      (("1"
                                        (replace -1 1 rl)
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (rewrite
                                             "complement_emptyset")
                                            (("1"
                                              (rewrite
                                               "complement_complement")
                                              (("1"
                                                (hide-all-but (-7 1))
                                                (("1"
                                                  (expand "cover?")
                                                  (("1"
                                                    (expand "subset?")
                                                    (("1"
                                                      (expand "member")
                                                      (("1"
                                                        (apply-extensionality
                                                         :hide?
                                                         t)
                                                        (("1"
                                                          (inst
                                                           -
                                                           "x!1")
                                                          (("1"
                                                            (expand
                                                             "fullset")
                                                            (("1"
                                                              (split)
                                                              (("1"
                                                                (propax)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (hide
                                                                 2)
                                                                (("2"
                                                                  (expand
                                                                   "Union")
                                                                  (("2"
                                                                    (inst
                                                                     +
                                                                     "fullset[T]")
                                                                    (("1"
                                                                      (expand
                                                                       "fullset")
                                                                      (("1"
                                                                        (propax)
                                                                        nil
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (lemma
                                                                       "fullset_is_open")
                                                                      (("2"
                                                                        (expand
                                                                         "open?")
                                                                        (("2"
                                                                          (expand
                                                                           "member")
                                                                          (("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))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (split)
                        (("1" (hide-all-but (-2 1))
                          (("1" (expand "subset?")
                            (("1" (skosimp)
                              (("1"
                                (expand "member")
                                (("1"
                                  (expand "Complement")
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (typepred "b!1")
                                      (("1"
                                        (inst - "b!1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (replace -3)
                                              (("1"
                                                (rewrite
                                                 "complement_complement")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "finite_cover?")
                          (("2" (flatten)
                            (("2" (hide-all-but (-3 1))
                              (("2"
                                (expand "is_finite")
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (inst
                                     +
                                     "N!1"
                                     "lambda (x:(Complement(V!1))): f!1(complement(x))")
                                    (("1"
                                      (expand "injective?")
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (inst
                                           -
                                           "complement(x1!1)"
                                           "complement(x2!1)")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (rewrite
                                               "complement_equal")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (skosimp)
                                      (("2"
                                        (typepred "x!1")
                                        (("2"
                                          (expand "Complement")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (replace -1)
                                              (("2"
                                                (rewrite
                                                 "complement_complement")
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide -1 -3)
                  (("2" (expand "open_cover?")
                    (("2" (rewrite "emptyset_is_empty?")
                      (("2" (lemma "Demorgan2" ("A" "Y!1"))
                        (("2" (replace -3)
                          (("2" (rewrite "complement_emptyset")
                            (("2" (split)
                              (("1"
                                (hide -1 -3)
                                (("1"
                                  (expand "subset?")
                                  (("1"
                                    (expand "every")
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (expand "Complement")
                                        (("1"
                                          (expand "member")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (typepred "b!1")
                                              (("1"
                                                (inst - "b!1")
                                                (("1"
                                                  (expand "closed?")
                                                  (("1"
                                                    (expand "member")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "cover?")
                                (("2"
                                  (replace -1 * rl)
                                  (("2"
                                    (expand "subset?")
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (expand "fullset")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (expand "open_cover?")
            (("2" (flatten)
              (("2" (inst - "Complement(U!1)")
                (("2" (case-replace "every(closed?, Complement(U!1))")
                  (("1" (split -2)
                    (("1" (expand "nonempty?")
                      (("1" (expand "empty?")
                        (("1" (skosimp)
                          (("1" (expand "member")
                            (("1" (rewrite "Demorgan1" -1 :dir rl)
                              (("1"
                                (expand "cover?")
                                (("1"
                                  (expand "subset?" -4)
                                  (("1"
                                    (inst - "x!1")
                                    (("1"
                                      (split -4)
                                      (("1"
                                        (expand "complement")
                                        (("1" (propax) nil nil))
                                        nil)
                                       ("2"
                                        (hide-all-but 1)
                                        (("2"
                                          (expand "member")
                                          (("2"
                                            (expand "Union")
                                            (("2"
                                              (inst + "fullset[T]")
                                              (("1"
                                                (expand "fullset")
                                                (("1"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil)
                                               ("2"
                                                (lemma "open_fullset")
                                                (("2"
                                                  (expand "open?")
                                                  (("2"
                                                    (expand "member")
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp)
                      (("2" (expand "nonempty?")
                        (("2" (inst + "Complement(Y1!1)")
                          (("2" (split)
                            (("1" (hide-all-but (-1 1))
                              (("1"
                                (expand "subset?")
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (expand "Complement")
                                    (("1"
                                      (expand "member")
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (replace -1)
                                          (("1"
                                            (typepred "b!1")
                                            (("1"
                                              (inst - "b!1")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (skosimp)
                                                  (("1"
                                                    (replace -3)
                                                    (("1"
                                                      (rewrite
                                                       "complement_complement")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "finite_cover?")
                              (("2"
                                (split)
                                (("1"
                                  (hide-all-but (-2 1))
                                  (("1"
                                    (expand "is_finite")
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (inst
                                         +
                                         "N!1"
                                         "lambda (x:(Complement(Y1!1))): f!1(complement(x))")
                                        (("1"
                                          (expand "injective?")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (inst
                                               -
                                               "complement(x1!1)"
                                               "complement(x2!1)")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (rewrite
                                                   "complement_equal")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (skosimp)
                                          (("2"
                                            (typepred "x!1")
                                            (("2"
                                              (expand "Complement")
                                              (("2"
                                                (skosimp)
                                                (("2"
                                                  (replace -1)
                                                  (("2"
                                                    (rewrite
                                                     "complement_complement")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "cover?")
                                  (("2"
                                    (rewrite "Demorgan2" 1 :dir rl)
                                    (("2"
                                      (expand "subset?" 1)
                                      (("2"
                                        (skosimp)
                                        (("2"
                                          (expand "member")
                                          (("2"
                                            (expand "complement")
                                            (("2"
                                              (expand "member")
                                              (("2"
                                                (expand "empty?" -5)
                                                (("2"
                                                  (inst - "x!1")
                                                  (("2"
                                                    (expand "member")
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide-all-but (-2 1))
                    (("2" (expand "every")
                      (("2" (skosimp)
                        (("2" (expand "closed?")
                          (("2" (expand "subset?")
                            (("2" (expand "member")
                              (("2"
                                (typepred "x!1")
                                (("2"
                                  (expand "Complement")
                                  (("2"
                                    (skosimp)
                                    (("2"
                                      (inst - "b!1")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (replace -1)
                                          (("2"
                                            (rewrite
                                             "complement_complement")
                                            nil
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((compact_subset? const-decl "bool" topology_prelim nil)
    (PRED type-eq-decl nil defined_types nil)
    (Y1!1 skolem-const-decl "setofsets[T]" topology nil)
    (open_fullset formula-decl nil topology nil)
    (empty? const-decl "bool" sets nil)
    (T formal-type-decl nil topology nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (Complement const-decl "setofsets[T]" sets_lemmas nil)
    (Intersection const-decl "set" sets nil)
    (Intersection_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (closed? const-decl "bool" topology nil)
    (every const-decl "bool" sets nil)
    (Demorgan2 formula-decl nil sets_lemmas nil)
    (is_finite const-decl "bool" finite_sets nil)
    (subset? const-decl "bool" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (Demorgan1 formula-decl nil sets_lemmas nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (complement_equal formula-decl nil sets_lemmas nil)
    (emptyset const-decl "set" sets nil)
    (complement_complement formula-decl nil sets_lemmas nil)
    (cover? const-decl "bool" topology_prelim nil)
    (member const-decl "bool" sets nil)
    (fullset_is_open judgement-tcc nil topology nil)
    (open? const-decl "bool" topology nil)
    (fullset const-decl "set" sets nil)
    (fullset_is_clopen name-judgement "clopen" topology nil)
    (complement_emptyset formula-decl nil sets_lemmas nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_compact name-judgement "compact" topology nil)
    (emptyset_is_clopen name-judgement "clopen" topology nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (complement const-decl "set" sets nil)
    (finite_cover? const-decl "bool" topology_prelim nil)
    (injective? const-decl "bool" functions nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (V!1 skolem-const-decl "setofsets[T]" topology nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (S formal-const-decl "topology" topology nil)
    (topology nonempty-type-eq-decl nil topology_prelim nil)
    (topology? const-decl "bool" topology_prelim nil)
    (Union const-decl "set" sets nil)
    (open_cover? const-decl "bool" topology_prelim nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (compact_space? const-decl "bool" topology_prelim nil))
   shostak)))