Quelle  cross_metric_uniform_continuity.prf

(cross_metric_uniform_continuity
 (IMP_cross_metric_spaces_TCC1 0
  (IMP_cross_metric_spaces_TCC1-1 nil 3460217227
   ("" (lemma "fullset_metric_space1") (("" (propax) nil nil)) nil)
   ((fullset_metric_space1 formula-decl nil
     cross_metric_uniform_continuity nil))
   nil))
 (IMP_cross_metric_spaces_TCC2 0
  (IMP_cross_metric_spaces_TCC2-1 nil 3460217227
   ("" (lemma "fullset_metric_space2") (("" (propax) nil nil)) nil)
   ((fullset_metric_space2 formula-decl nil
     cross_metric_uniform_continuity nil))
   nil))
 (IMP_continuity_ms_def_TCC1 0
  (IMP_continuity_ms_def_TCC1-1 nil 3460217227
   ("" (lemma "product_is_metric") (("" (propax) nil nil)) nil)
   ((product_is_metric formula-decl nil cross_metric_spaces nil)
    (T1 formal-nonempty-type-decl nil cross_metric_uniform_continuity
     nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (d1 formal-const-decl "[T1, T1 -> nnreal]"
     cross_metric_uniform_continuity nil)
    (T2 formal-nonempty-type-decl nil cross_metric_uniform_continuity
     nil)
    (d2 formal-const-decl "[T2, T2 -> nnreal]"
     cross_metric_uniform_continuity nil))
   nil))
 (IMP_continuity_ms_def_TCC2 0
  (IMP_continuity_ms_def_TCC2-1 nil 3460217227
   ("" (lemma "fullset_metric_space3") (("" (propax) nil nil)) nil)
   ((fullset_metric_space3 formula-decl nil
     cross_metric_uniform_continuity nil))
   nil))
 (multiary_Heine 0
  (multiary_Heine-2 nil 3565651140
   ("" (skosimp*)
    (("" (label "comp" -1)
      (("" (label "cont" -2)
        (("" (label "unif" 1)
          (("" (lemma "one_variable_unif_cont_sequence")
            (("" (label "epsq" -1)
              (("" (inst "epsq" "X!1" "Y!1" "f!1")
                (("" (assert)
                  (("" (skosimp*)
                    (("" (lemma "compact_sequence_limit[T1,d1]")
                      (("" (label "csl" -1)
                        (("" (inst "csl" "X!1")
                          (("" (assert)
                            (("" (prop)
                              (("1"
                                (inst
                                 "csl"
                                 "(LAMBDA (n: nat): IF n = 0 THEN seq!1(1)`1 ELSE seq!1(n)`1 ENDIF)")
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (lemma
                                     "product_cont_product_subset")
                                    (("1"
                                      (label "pcps" -1)
                                      (("1"
                                        (inst "pcps" "X!1" "Y!1" "f!1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (inst
                                             "pcps"
                                             "p!1"
                                             "y!1"
                                             "epsilon!1/2")
                                            (("1"
                                              (skosimp*)
                                              (("1"
                                                (lemma "archimedean")
                                                (("1"
                                                  (label "arch" -1)
                                                  (("1"
                                                    (inst
                                                     "arch"
                                                     "delta!1/2")
                                                    (("1"
                                                      (skosimp *)
                                                      (("1"
                                                        (inst
                                                         "csl"
                                                         "1/n!1"
                                                         "n!1")
                                                        (("1"
                                                          (skosimp*)
                                                          (("1"
                                                            (typepred
                                                             "n!2")
                                                            (("1"
                                                              (label
                                                               "n!2T"
                                                               -1)
                                                              (("1"
                                                                (lemma
                                                                 "fullset_metric_space1")
                                                                (("1"
                                                                  (expand
                                                                   "metric_space?")
                                                                  (("1"
                                                                    (prop)
                                                                    (("1"
                                                                      (label
                                                                       "sz1"
                                                                       -1)
                                                                      (("1"
                                                                        (label
                                                                         "sym1"
                                                                         -2)
                                                                        (("1"
                                                                          (label
                                                                           "tri1"
                                                                           -3)
                                                                          (("1"
                                                                            (lemma
                                                                             "fullset_metric_space3")
                                                                            (("1"
                                                                              (expand
                                                                               "metric_space?")
                                                                              (("1"
                                                                                (prop)
                                                                                (("1"
                                                                                  (label
                                                                                   "sz3"
                                                                                   -1)
                                                                                  (("1"
                                                                                    (label
                                                                                     "sym3"
                                                                                     -2)
                                                                                    (("1"
                                                                                      (label
                                                                                       "tri3"
                                                                                       -3)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "space_symmetric?")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "space_triangle?")
                                                                                          (("1"
                                                                                            (hide
                                                                                             "sz1"
                                                                                             "sz3")
                                                                                            (("1"
                                                                                              (lemma
                                                                                               "fullset_metric_space2")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "metric_space?")
                                                                                                (("1"
                                                                                                  (prop)
                                                                                                  (("1"
                                                                                                    (hide
                                                                                                     -2
                                                                                                     -3)
                                                                                                    (("1"
                                                                                                      (label
                                                                                                       "sz2"
                                                                                                       -1)
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "space_zero?")
                                                                                                        (("1"
                                                                                                          (copy
                                                                                                           "tri1")
                                                                                                          (("1"
                                                                                                            (hide
                                                                                                             "tri1")
                                                                                                            (("1"
                                                                                                              (inst-cp
                                                                                                               -1
                                                                                                               "seq!1(n!2)`2"
                                                                                                               "seq!1(n!2)`1"
                                                                                                               "p!1")
                                                                                                              (("1"
                                                                                                                (label
                                                                                                                 "tri1a"
                                                                                                                 -1)
                                                                                                                (("1"
                                                                                                                  (label
                                                                                                                   "tri1inst"
                                                                                                                   -2)
                                                                                                                  (("1"
                                                                                                                    (inst
                                                                                                                     "epsq"
                                                                                                                     "n!2")
                                                                                                                    (("1"
                                                                                                                      (copy
                                                                                                                       "epsq")
                                                                                                                      (("1"
                                                                                                                        (hide
                                                                                                                         "epsq")
                                                                                                                        (("1"
                                                                                                                          (prop)
                                                                                                                          (("1"
                                                                                                                            (label
                                                                                                                             "mbs1"
                                                                                                                             -1)
                                                                                                                            (("1"
                                                                                                                              (label
                                                                                                                               "mbs2"
                                                                                                                               -2)
                                                                                                                              (("1"
                                                                                                                                (label
                                                                                                                                 "mbs3"
                                                                                                                                 -3)
                                                                                                                                (("1"
                                                                                                                                  (hide
                                                                                                                                   "mbs1"
                                                                                                                                   "mbs2"
                                                                                                                                   "mbs3")
                                                                                                                                  (("1"
                                                                                                                                    (label
                                                                                                                                     "s12lt"
                                                                                                                                     -1)
                                                                                                                                    (("1"
                                                                                                                                      (label
                                                                                                                                       "s3ylt"
                                                                                                                                       -2)
                                                                                                                                      (("1"
                                                                                                                                        (label
                                                                                                                                         "d3gt"
                                                                                                                                         -3)
                                                                                                                                        (("1"
                                                                                                                                          (copy
                                                                                                                                           "csl")
                                                                                                                                          (("1"
                                                                                                                                            (label
                                                                                                                                             "cls2"
                                                                                                                                             -1)
                                                                                                                                            (("1"
                                                                                                                                              (copy
                                                                                                                                               "sym1")
                                                                                                                                              (("1"
                                                                                                                                                (inst
                                                                                                                                                 -1
                                                                                                                                                 "seq!1(n!2)`1"
                                                                                                                                                 "seq!1(n!2)`2")
                                                                                                                                                (("1"
                                                                                                                                                  (replace
                                                                                                                                                   -1
                                                                                                                                                   "s12lt")
                                                                                                                                                  (("1"
                                                                                                                                                    (hide
                                                                                                                                                     -1)
                                                                                                                                                    (("1"
                                                                                                                                                      (copy
                                                                                                                                                       "cls2")
                                                                                                                                                      (("1"
                                                                                                                                                        (label
                                                                                                                                                         "cls3"
                                                                                                                                                         -1)
                                                                                                                                                        (("1"
                                                                                                                                                          (add-formulas
                                                                                                                                                           "s12lt"
                                                                                                                                                           "cls3")
                                                                                                                                                          (("1"
                                                                                                                                                            (label
                                                                                                                                                             "tri_inst1"
                                                                                                                                                             -1)
                                                                                                                                                            (("1"
                                                                                                                                                              (add-formulas
                                                                                                                                                               "tri_inst1"
                                                                                                                                                               "tri1inst")
                                                                                                                                                              (("1"
                                                                                                                                                                (label
                                                                                                                                                                 "tri_inst2"
                                                                                                                                                                 -1)
                                                                                                                                                                (("1"
                                                                                                                                                                  (both-sides
                                                                                                                                                                   "-"
                                                                                                                                                                   "d1(seq!1(n!2)`1, p!1) + d1(seq!1(n!2)`2, seq!1(n!2)`1)"
                                                                                                                                                                   "tri_inst2")
                                                                                                                                                                  (("1"
                                                                                                                                                                    (assert)
                                                                                                                                                                    (("1"
                                                                                                                                                                      (copy
                                                                                                                                                                       "arch")
                                                                                                                                                                      (("1"
                                                                                                                                                                        (label
                                                                                                                                                                         "arch2"
                                                                                                                                                                         -1)
                                                                                                                                                                        (("1"
                                                                                                                                                                          (add-formulas
                                                                                                                                                                           "arch2"
                                                                                                                                                                           "arch2")
                                                                                                                                                                          (("1"
                                                                                                                                                                            (add-formulas
                                                                                                                                                                             -1
                                                                                                                                                                             "tri_inst2")
                                                                                                                                                                            (("1"
                                                                                                                                                                              (assert)
                                                                                                                                                                              (("1"
                                                                                                                                                                                (lemma
                                                                                                                                                                                 "both_sides_div_pos_lt2")
                                                                                                                                                                                (("1"
                                                                                                                                                                                  (label
                                                                                                                                                                                   "both_sides_div_pos_lt2"
                                                                                                                                                                                   -1)
                                                                                                                                                                                  (("1"
                                                                                                                                                                                    (inst
                                                                                                                                                                                     "both_sides_div_pos_lt2"
                                                                                                                                                                                     "n!2"
                                                                                                                                                                                     "n!1"
                                                                                                                                                                                     "1")
                                                                                                                                                                                    (("1"
                                                                                                                                                                                      (prop)
                                                                                                                                                                                      (("1"
                                                                                                                                                                                        (hide
                                                                                                                                                                                         -2)
                                                                                                                                                                                        (("1"
                                                                                                                                                                                          (add-formulas
                                                                                                                                                                                           -1
                                                                                                                                                                                           -2)
                                                                                                                                                                                          (("1"
                                                                                                                                                                                            (both-sides
                                                                                                                                                                                             "-"
                                                                                                                                                                                             "2 * (1 / n!1) + 1 / n!2"
                                                                                                                                                                                             -1)
                                                                                                                                                                                            (("1"
                                                                                                                                                                                              (assert)
                                                                                                                                                                                              (("1"
                                                                                                                                                                                                (label
                                                                                                                                                                                                 "d1sp1"
                                                                                                                                                                                                 -1)
                                                                                                                                                                                                (("1"
                                                                                                                                                                                                  (copy
                                                                                                                                                                                                   "pcps")
                                                                                                                                                                                                  (("1"
                                                                                                                                                                                                    (hide
                                                                                                                                                                                                     "pcps")
                                                                                                                                                                                                    (("1"
                                                                                                                                                                                                      (label
                                                                                                                                                                                                       "pcps2"
                                                                                                                                                                                                       -1)
                                                                                                                                                                                                      (("1"
                                                                                                                                                                                                        (copy
                                                                                                                                                                                                         "pcps2")
                                                                                                                                                                                                        (("1"
                                                                                                                                                                                                          (label
                                                                                                                                                                                                           "pcps3"
                                                                                                                                                                                                           -1)
                                                                                                                                                                                                          (("1"
                                                                                                                                                                                                            (inst
                                                                                                                                                                                                             "pcps3"
                                                                                                                                                                                                             "seq!1(n!2)`2"
                                                                                                                                                                                                             "seq!1(n!2)`3")
                                                                                                                                                                                                            (("1"
                                                                                                                                                                                                              (prop)
                                                                                                                                                                                                              (("1"
                                                                                                                                                                                                                (inst
                                                                                                                                                                                                                 "pcps2"
                                                                                                                                                                                                                 "seq!1(n!2)`1"
                                                                                                                                                                                                                 "y!1")
                                                                                                                                                                                                                (("1"
                                                                                                                                                                                                                  (inst
                                                                                                                                                                                                                   "sym1"
                                                                                                                                                                                                                   "p!1"
                                                                                                                                                                                                                   "seq!1(n!2)`1")
                                                                                                                                                                                                                  (("1"
                                                                                                                                                                                                                    (replace
                                                                                                                                                                                                                     "sym1")
                                                                                                                                                                                                                    (("1"
                                                                                                                                                                                                                      (inst
                                                                                                                                                                                                                       "sz2"
                                                                                                                                                                                                                       "y!1"
                                                                                                                                                                                                                       "y!1")
                                                                                                                                                                                                                      (("1"
                                                                                                                                                                                                                        (copy
                                                                                                                                                                                                                         "arch")
                                                                                                                                                                                                                        (("1"
                                                                                                                                                                                                                          (label
                                                                                                                                                                                                                           "arch3"
                                                                                                                                                                                                                           -1)
                                                                                                                                                                                                                          (("1"
                                                                                                                                                                                                                            (add-formulas
                                                                                                                                                                                                                             "cls2"
                                                                                                                                                                                                                             "arch")
                                                                                                                                                                                                                            (("1"
                                                                                                                                                                                                                              (assert)
                                                                                                                                                                                                                              (("1"
                                                                                                                                                                                                                                (assert)
                                                                                                                                                                                                                                (("1"
                                                                                                                                                                                                                                  (both-sides
                                                                                                                                                                                                                                   "-"
                                                                                                                                                                                                                                   "1/n!1"
                                                                                                                                                                                                                                   -1)
                                                                                                                                                                                                                                  (("1"
                                                                                                                                                                                                                                    (assert)
                                                                                                                                                                                                                                    (("1"
                                                                                                                                                                                                                                      (inst
                                                                                                                                                                                                                                       "tri3"
                                                                                                                                                                                                                                       "f!1(seq!1(n!2)`1,y!1)"
                                                                                                                                                                                                                                       "f!1(p!1,y!1)"
                                                                                                                                                                                                                                       "f!1(seq!1(n!2)`2, seq!1(n!2)`3)")
                                                                                                                                                                                                                                      (("1"
                                                                                                                                                                                                                                        (hide-all-but
                                                                                                                                                                                                                                         ("pcps3"
                                                                                                                                                                                                                                          "pcps2"
                                                                                                                                                                                                                                          "tri3"
                                                                                                                                                                                                                                          "sym3"
                                                                                                                                                                                                                                          "d3gt"
                                                                                                                                                                                                                                          "arch3"))
                                                                                                                                                                                                                                        (("1"
                                                                                                                                                                                                                                          (inst
                                                                                                                                                                                                                                           "sym3"
                                                                                                                                                                                                                                           "f!1(seq!1(n!2)`1, y!1)"
                                                                                                                                                                                                                                           "f!1(p!1, y!1)")
                                                                                                                                                                                                                                          (("1"
                                                                                                                                                                                                                                            (replace
                                                                                                                                                                                                                                             "sym3")
                                                                                                                                                                                                                                            (("1"
                                                                                                                                                                                                                                              (add-formulas
                                                                                                                                                                                                                                               "tri3"
                                                                                                                                                                                                                                               "pcps3")
                                                                                                                                                                                                                                              nil
                                                                                                                                                                                                                                              nil))
                                                                                                                                                                                                                                            nil)
                                                                                                                                                                                                                                           ("2"
                                                                                                                                                                                                                                            (expand
                                                                                                                                                                                                                                             "fullset")
                                                                                                                                                                                                                                            (("2"
                                                                                                                                                                                                                                              (propax)
                                                                                                                                                                                                                                              nil
                                                                                                                                                                                                                                              nil))
                                                                                                                                                                                                                                            nil)
                                                                                                                                                                                                                                           ("3"
                                                                                                                                                                                                                                            (expand
                                                                                                                                                                                                                                             "fullset")
                                                                                                                                                                                                                                            (("3"
                                                                                                                                                                                                                                              (propax)
                                                                                                                                                                                                                                              nil
                                                                                                                                                                                                                                              nil))
                                                                                                                                                                                                                                            nil))
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil)
                                                                                                                                                                                                                                       ("2"
                                                                                                                                                                                                                                        (expand
                                                                                                                                                                                                                                         "fullset")
                                                                                                                                                                                                                                        (("2"
                                                                                                                                                                                                                                          (propax)
                                                                                                                                                                                                                                          nil
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil)
                                                                                                                                                                                                                                       ("3"
                                                                                                                                                                                                                                        (expand
                                                                                                                                                                                                                                         "fullset")
                                                                                                                                                                                                                                        (("3"
                                                                                                                                                                                                                                          (propax)
                                                                                                                                                                                                                                          nil
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil)
                                                                                                                                                                                                                                       ("4"
                                                                                                                                                                                                                                        (expand
                                                                                                                                                                                                                                         "fullset")
                                                                                                                                                                                                                                        (("4"
                                                                                                                                                                                                                                          (propax)
                                                                                                                                                                                                                                          nil
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil))
                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                    nil)
                                                                                                                                                                                                                                   ("2"
                                                                                                                                                                                                                                    (iff)
                                                                                                                                                                                                                                    (("2"
                                                                                                                                                                                                                                      (prop)
                                                                                                                                                                                                                                      (("1"
                                                                                                                                                                                                                                        (hide-all-but
                                                                                                                                                                                                                                         (1
                                                                                                                                                                                                                                          "arch3"
                                                                                                                                                                                                                                          "csl"))
                                                                                                                                                                                                                                        (("1"
                                                                                                                                                                                                                                          (name-replace
                                                                                                                                                                                                                                           "A"
                                                                                                                                                                                                                                           "d1(seq!1(n!2)`1, p!1)")
                                                                                                                                                                                                                                          (("1"
                                                                                                                                                                                                                                            (typepred
                                                                                                                                                                                                                                             "A")
                                                                                                                                                                                                                                            (("1"
                                                                                                                                                                                                                                              (cancel-by
                                                                                                                                                                                                                                               1
                                                                                                                                                                                                                                               "n!1*n!1")
                                                                                                                                                                                                                                              nil
                                                                                                                                                                                                                                              nil))
                                                                                                                                                                                                                                            nil))
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil)
                                                                                                                                                                                                                                       ("2"
                                                                                                                                                                                                                                        (hide-all-but
                                                                                                                                                                                                                                         (1
                                                                                                                                                                                                                                          "arch3"
                                                                                                                                                                                                                                          "csl"))
                                                                                                                                                                                                                                        (("2"
                                                                                                                                                                                                                                          (name-replace
                                                                                                                                                                                                                                           "A"
                                                                                                                                                                                                                                           "d1(seq!1(n!2)`1, p!1)")
                                                                                                                                                                                                                                          (("2"
                                                                                                                                                                                                                                            (cross-mult
                                                                                                                                                                                                                                             -2)
                                                                                                                                                                                                                                            (("2"
                                                                                                                                                                                                                                              (add-formulas
                                                                                                                                                                                                                                               "csl"
                                                                                                                                                                                                                                               "csl")
                                                                                                                                                                                                                                              (("2"
                                                                                                                                                                                                                                                (add-formulas
                                                                                                                                                                                                                                                 -1
                                                                                                                                                                                                                                                 1)
                                                                                                                                                                                                                                                (("2"
                                                                                                                                                                                                                                                  (both-sides
                                                                                                                                                                                                                                                   "-"
                                                                                                                                                                                                                                                   "2 * (A * n!1)"
                                                                                                                                                                                                                                                   -1)
                                                                                                                                                                                                                                                  (("2"
                                                                                                                                                                                                                                                    (assert)
                                                                                                                                                                                                                                                    (("2"
                                                                                                                                                                                                                                                      (both-sides
                                                                                                                                                                                                                                                       "-"
                                                                                                                                                                                                                                                       "2"
                                                                                                                                                                                                                                                       -1)
                                                                                                                                                                                                                                                      (("2"
                                                                                                                                                                                                                                                        (assert)
                                                                                                                                                                                                                                                        (("2"
                                                                                                                                                                                                                                                          (case
                                                                                                                                                                                                                                                           "2 * (delta!1 / 2) / 2 = delta!1/2")
                                                                                                                                                                                                                                                          (("1"
                                                                                                                                                                                                                                                            (replace
                                                                                                                                                                                                                                                             -1)
                                                                                                                                                                                                                                                            (("1"
                                                                                                                                                                                                                                                              (mult-ineq
                                                                                                                                                                                                                                                               -2
                                                                                                                                                                                                                                                               -3)
                                                                                                                                                                                                                                                              (("1"
                                                                                                                                                                                                                                                                (assert)
                                                                                                                                                                                                                                                                nil
                                                                                                                                                                                                                                                                nil))
                                                                                                                                                                                                                                                              nil))
                                                                                                                                                                                                                                                            nil)
                                                                                                                                                                                                                                                           ("2"
                                                                                                                                                                                                                                                            (assert)
                                                                                                                                                                                                                                                            nil
                                                                                                                                                                                                                                                            nil))
                                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                                        nil))
                                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                                                nil))
                                                                                                                                                                                                                                              nil))
                                                                                                                                                                                                                                            nil))
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil))
                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                                nil))
                                                                                                                                                                                                                              nil))
                                                                                                                                                                                                                            nil))
                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                        nil)
                                                                                                                                                                                                                       ("2"
                                                                                                                                                                                                                        (expand
                                                                                                                                                                                                                         "fullset")
                                                                                                                                                                                                                        (("2"
                                                                                                                                                                                                                          (propax)
                                                                                                                                                                                                                          nil
                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                        nil))
                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                    nil)
                                                                                                                                                                                                                   ("2"
                                                                                                                                                                                                                    (expand
                                                                                                                                                                                                                     "fullset")
                                                                                                                                                                                                                    (("2"
                                                                                                                                                                                                                      (propax)
                                                                                                                                                                                                                      nil
                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                    nil)
                                                                                                                                                                                                                   ("3"
                                                                                                                                                                                                                    (expand
                                                                                                                                                                                                                     "fullset")
                                                                                                                                                                                                                    (("3"
                                                                                                                                                                                                                      (propax)
                                                                                                                                                                                                                      nil
                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil)
                                                                                                                                                                                                                 ("2"
                                                                                                                                                                                                                  (reveal
                                                                                                                                                                                                                   "mbs1")
                                                                                                                                                                                                                  (("2"
                                                                                                                                                                                                                    (propax)
                                                                                                                                                                                                                    nil
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                nil)
                                                                                                                                                                                                               ("2"
                                                                                                                                                                                                                (inst
                                                                                                                                                                                                                 "sym1"
                                                                                                                                                                                                                 "p!1"
                                                                                                                                                                                                                 "seq!1(n!2)`2")
                                                                                                                                                                                                                (("1"
                                                                                                                                                                                                                  (replace
                                                                                                                                                                                                                   "sym1")
                                                                                                                                                                                                                  (("1"
                                                                                                                                                                                                                    (reveal
                                                                                                                                                                                                                     "arch2")
                                                                                                                                                                                                                    (("1"
                                                                                                                                                                                                                      (add-formulas
                                                                                                                                                                                                                       "csl"
                                                                                                                                                                                                                       "arch2")
                                                                                                                                                                                                                      nil
                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil)
                                                                                                                                                                                                                 ("2"
                                                                                                                                                                                                                  (expand
                                                                                                                                                                                                                   "fullset")
                                                                                                                                                                                                                  (("2"
                                                                                                                                                                                                                    (propax)
                                                                                                                                                                                                                    nil
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil)
                                                                                                                                                                                                                 ("3"
                                                                                                                                                                                                                  (expand
                                                                                                                                                                                                                   "fullset")
                                                                                                                                                                                                                  (("3"
                                                                                                                                                                                                                    (propax)
                                                                                                                                                                                                                    nil
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                nil)
                                                                                                                                                                                                               ("3"
                                                                                                                                                                                                                (add-formulas
                                                                                                                                                                                                                 "cls2"
                                                                                                                                                                                                                 "arch")
                                                                                                                                                                                                                (("3"
                                                                                                                                                                                                                  (reveal
                                                                                                                                                                                                                   -)
                                                                                                                                                                                                                  (("3"
                                                                                                                                                                                                                    (assert)
                                                                                                                                                                                                                    nil
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                nil))
                                                                                                                                                                                                              nil)
                                                                                                                                                                                                             ("2"
                                                                                                                                                                                                              (reveal
                                                                                                                                                                                                               "mbs3")
                                                                                                                                                                                                              (("2"
                                                                                                                                                                                                                (propax)
                                                                                                                                                                                                                nil
                                                                                                                                                                                                                nil))
                                                                                                                                                                                                              nil)
                                                                                                                                                                                                             ("3"
                                                                                                                                                                                                              (reveal
                                                                                                                                                                                                               "mbs2")
                                                                                                                                                                                                              (("3"
                                                                                                                                                                                                                (propax)
                                                                                                                                                                                                                nil
                                                                                                                                                                                                                nil))
                                                                                                                                                                                                              nil))
                                                                                                                                                                                                            nil))
                                                                                                                                                                                                          nil))
                                                                                                                                                                                                        nil))
                                                                                                                                                                                                      nil))
                                                                                                                                                                                                    nil))
                                                                                                                                                                                                  nil))
                                                                                                                                                                                                nil))
                                                                                                                                                                                              nil)
                                                                                                                                                                                             ("2"
                                                                                                                                                                                              (assert)
                                                                                                                                                                                              nil
                                                                                                                                                                                              nil))
                                                                                                                                                                                            nil))
                                                                                                                                                                                          nil))
                                                                                                                                                                                        nil)
                                                                                                                                                                                       ("2"
                                                                                                                                                                                        (assert)
                                                                                                                                                                                        nil
                                                                                                                                                                                        nil))
                                                                                                                                                                                      nil))
                                                                                                                                                                                    nil))
                                                                                                                                                                                  nil))
                                                                                                                                                                                nil))
                                                                                                                                                                              nil))
                                                                                                                                                                            nil))
                                                                                                                                                                          nil))
                                                                                                                                                                        nil))
                                                                                                                                                                      nil))
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil))
                                                                                                                                                  nil)
                                                                                                                                                 ("2"
                                                                                                                                                  (expand
                                                                                                                                                   "fullset")
                                                                                                                                                  (("2"
                                                                                                                                                    (propax)
                                                                                                                                                    nil
                                                                                                                                                    nil))
                                                                                                                                                  nil)
                                                                                                                                                 ("3"
                                                                                                                                                  (expand
                                                                                                                                                   "fullset")
                                                                                                                                                  (("3"
                                                                                                                                                    (propax)
                                                                                                                                                    nil
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil)
                                                                                                               ("2"
                                                                                                                (expand
                                                                                                                 "fullset")
                                                                                                                (("2"
                                                                                                                  (propax)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil)
                                                                                                               ("3"
                                                                                                                (expand
                                                                                                                 "fullset")
                                                                                                                (("3"
                                                                                                                  (propax)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil)
                                                                                                               ("4"
                                                                                                                (expand
                                                                                                                 "fullset")
                                                                                                                (("4"
                                                                                                                  (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))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skosimp*)
                                  (("2"
                                    (inst "epsq" "n!1")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (skosimp*)
                                  (("3" (assert) nil nil))
                                  nil)
                                 ("4"
                                  (skosimp*)
                                  (("4"
                                    (inst "epsq" "1")
                                    (("4" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "nonempty?")
                                (("2"
                                  (expand "empty?")
                                  (("2"
                                    (expand "member")
                                    (("2"
                                      (inst "csl" "seq!1(1)`1")
                                      (("2"
                                        (inst "epsq" "1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((compact_sequence_limit formula-decl nil compactness nil)
    (metric_space? const-decl "bool" metric_spaces_def nil)
    (space_triangle? const-decl "bool" metric_spaces_def nil)
    (fullset_metric_space2 formula-decl nil
     cross_metric_uniform_continuity nil)
    (fullset const-decl "set" sets nil)
    (n!1 skolem-const-decl "posnat" cross_metric_uniform_continuity
     nil)
    (n!2 skolem-const-decl "above(n!1)" cross_metric_uniform_continuity
     nil)
    (p!1 skolem-const-decl "(X!1)" cross_metric_uniform_continuity nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (posrat_plus_nnrat_is_posrat application-judgement "posrat"
     rationals nil)
    (< const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (both_sides_minus_lt1 formula-decl nil real_props nil)
    (neg_times_lt formula-decl nil real_props nil)
    (neg_times_le formula-decl nil real_props nil)
    (add_div formula-decl nil real_props nil)
    (both_sides_plus_le2 formula-decl nil real_props nil)
    (both_sides_plus_lt2 formula-decl nil real_props nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (div_cancel1 formula-decl nil real_props nil)
    (y!1 skolem-const-decl "(Y!1)" cross_metric_uniform_continuity nil)
    (pos_times_le formula-decl nil real_props nil)
    (pos_times_lt formula-decl nil real_props nil)
    (minus_div1 formula-decl nil real_props nil)
    (div_simp formula-decl nil real_props nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (f!1 skolem-const-decl "[[T1, T2] -> T3]"
     cross_metric_uniform_continuity nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (even_minus_even_is_even application-judgement "even_int" integers
     nil)
    (even? const-decl "bool" integers nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (lt_times_lt_any1 formula-decl nil extra_real_props nil)
    (div_cancel2 formula-decl nil real_props nil)
    (Y!1 skolem-const-decl "set[T2]" cross_metric_uniform_continuity
     nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (times_div1 formula-decl nil real_props nil)
    (times_div2 formula-decl nil real_props nil)
    (both_sides_times_pos_le2 formula-decl nil real_props nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (both_sides_times_pos_lt2 formula-decl nil real_props nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (both_sides_plus_lt1 formula-decl nil real_props nil)
    (both_sides_plus_le1 formula-decl nil real_props nil)
    (both_sides_div_pos_le2 formula-decl nil real_props nil)
    (both_sides_div_pos_lt2 formula-decl nil real_props nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (space_zero? const-decl "bool" metric_spaces_def nil)
    (space_symmetric? const-decl "bool" metric_spaces_def nil)
    (fullset_metric_space3 formula-decl nil
     cross_metric_uniform_continuity nil)
    (fullset_metric_space1 formula-decl nil
     cross_metric_uniform_continuity nil)
    (above nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (archimedean formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (product_cont_product_subset formula-decl nil cross_metric_cont
     nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (X!1 skolem-const-decl "set[T1]" cross_metric_uniform_continuity
     nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (seq!1 skolem-const-decl "[posint -> [T1, T1, T2]]"
     cross_metric_uniform_continuity nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (one_variable_unif_cont_sequence formula-decl nil cross_metric_cont
     nil)
    (T1 formal-nonempty-type-decl nil cross_metric_uniform_continuity
     nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (d1 formal-const-decl "[T1, T1 -> nnreal]"
     cross_metric_uniform_continuity nil)
    (T2 formal-nonempty-type-decl nil cross_metric_uniform_continuity
     nil)
    (d2 formal-const-decl "[T2, T2 -> nnreal]"
     cross_metric_uniform_continuity nil)
    (T3 formal-nonempty-type-decl nil cross_metric_uniform_continuity
     nil)
    (d3 formal-const-decl "[T3, T3 -> nnreal]"
     cross_metric_uniform_continuity nil))
   nil)
  (multiary_Heine-1 nil 3460217255
   ("" (skosimp*)
    (("" (label "comp" -1)
      (("" (label "cont" -2)
        (("" (label "unif" 1)
          (("" (lemma "one_variable_unif_cont_sequence")
            (("" (label "epsq" -1)
              (("" (inst "epsq" "X!1" "Y!1" "f!1")
                (("" (assert)
                  (("" (skosimp*)
                    (("" (lemma "compact_sequence_limit[T1,d1]")
                      (("" (label "csl" -1)
                        (("" (inst "csl" "X!1")
                          (("" (assert)
                            (("" (prop)
                              (("1"
                                (inst
                                 "csl"
                                 "(LAMBDA (n: nat): IF n = 0 THEN seq!1(1)`1 ELSE seq!1(n)`1 ENDIF)")
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (lemma
                                     "product_cont_product_subset")
                                    (("1"
                                      (label "pcps" -1)
                                      (("1"
                                        (inst "pcps" "X!1" "Y!1" "f!1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (inst
                                             "pcps"
                                             "p!1"
                                             "y!1"
                                             "epsilon!1/2")
                                            (("1"
                                              (skosimp*)
                                              (("1"
                                                (lemma "archimedean")
                                                (("1"
                                                  (label "arch" -1)
                                                  (("1"
                                                    (inst
                                                     "arch"
                                                     "delta!1/2")
                                                    (("1"
                                                      (skosimp *)
                                                      (("1"
                                                        (inst
                                                         "csl"
                                                         "1/n!1"
                                                         "n!1")
                                                        (("1"
                                                          (skosimp*)
                                                          (("1"
                                                            (typepred
                                                             "n!2")
                                                            (("1"
                                                              (label
                                                               "n!2T"
                                                               -1)
                                                              (("1"
                                                                (lemma
                                                                 "fullset_metric_space1")
                                                                (("1"
                                                                  (expand
                                                                   "metric_space?")
                                                                  (("1"
                                                                    (prop)
                                                                    (("1"
                                                                      (label
                                                                       "sz1"
                                                                       -1)
                                                                      (("1"
                                                                        (label
                                                                         "sym1"
                                                                         -2)
                                                                        (("1"
                                                                          (label
                                                                           "tri1"
                                                                           -3)
                                                                          (("1"
                                                                            (lemma
                                                                             "fullset_metric_space3")
                                                                            (("1"
                                                                              (expand
                                                                               "metric_space?")
                                                                              (("1"
                                                                                (prop)
                                                                                (("1"
                                                                                  (label
                                                                                   "sz3"
                                                                                   -1)
                                                                                  (("1"
                                                                                    (label
                                                                                     "sym3"
                                                                                     -2)
                                                                                    (("1"
                                                                                      (label
                                                                                       "tri3"
                                                                                       -3)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "space_symmetric?")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "space_triangle?")
                                                                                          (("1"
                                                                                            (hide
                                                                                             "sz1"
                                                                                             "sz3")
                                                                                            (("1"
                                                                                              (lemma
                                                                                               "fullset_metric_space2")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "metric_space?")
                                                                                                (("1"
                                                                                                  (prop)
                                                                                                  (("1"
                                                                                                    (hide
                                                                                                     -2
                                                                                                     -3)
                                                                                                    (("1"
                                                                                                      (label
                                                                                                       "sz2"
                                                                                                       -1)
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "space_zero?")
                                                                                                        (("1"
                                                                                                          (copy
                                                                                                           "tri1")
                                                                                                          (("1"
                                                                                                            (hide
                                                                                                             "tri1")
                                                                                                            (("1"
                                                                                                              (inst-cp
                                                                                                               -1
                                                                                                               "seq!1(n!2)`2"
                                                                                                               "seq!1(n!2)`1"
                                                                                                               "p!1")
                                                                                                              (("1"
                                                                                                                (label
                                                                                                                 "tri1a"
                                                                                                                 -1)
                                                                                                                (("1"
                                                                                                                  (label
                                                                                                                   "tri1inst"
                                                                                                                   -2)
                                                                                                                  (("1"
                                                                                                                    (inst
                                                                                                                     "epsq"
                                                                                                                     "n!2")
                                                                                                                    (("1"
                                                                                                                      (copy
                                                                                                                       "epsq")
                                                                                                                      (("1"
                                                                                                                        (hide
                                                                                                                         "epsq")
                                                                                                                        (("1"
                                                                                                                          (prop)
                                                                                                                          (("1"
                                                                                                                            (label
                                                                                                                             "mbs1"
                                                                                                                             -1)
                                                                                                                            (("1"
                                                                                                                              (label
                                                                                                                               "mbs2"
                                                                                                                               -2)
                                                                                                                              (("1"
                                                                                                                                (label
                                                                                                                                 "mbs3"
                                                                                                                                 -3)
                                                                                                                                (("1"
                                                                                                                                  (hide
                                                                                                                                   "mbs1"
                                                                                                                                   "mbs2"
                                                                                                                                   "mbs3")
                                                                                                                                  (("1"
                                                                                                                                    (label
                                                                                                                                     "s12lt"
                                                                                                                                     -1)
                                                                                                                                    (("1"
                                                                                                                                      (label
                                                                                                                                       "s3ylt"
                                                                                                                                       -2)
                                                                                                                                      (("1"
                                                                                                                                        (label
                                                                                                                                         "d3gt"
                                                                                                                                         -3)
                                                                                                                                        (("1"
                                                                                                                                          (copy
                                                                                                                                           "csl")
                                                                                                                                          (("1"
                                                                                                                                            (label
                                                                                                                                             "cls2"
                                                                                                                                             -1)
                                                                                                                                            (("1"
                                                                                                                                              (copy
                                                                                                                                               "sym1")
                                                                                                                                              (("1"
                                                                                                                                                (inst
                                                                                                                                                 -1
                                                                                                                                                 "seq!1(n!2)`1"
                                                                                                                                                 "seq!1(n!2)`2")
                                                                                                                                                (("1"
                                                                                                                                                  (replace
                                                                                                                                                   -1
                                                                                                                                                   "s12lt")
                                                                                                                                                  (("1"
                                                                                                                                                    (hide
                                                                                                                                                     -1)
                                                                                                                                                    (("1"
                                                                                                                                                      (copy
                                                                                                                                                       "cls2")
                                                                                                                                                      (("1"
                                                                                                                                                        (label
                                                                                                                                                         "cls3"
                                                                                                                                                         -1)
                                                                                                                                                        (("1"
                                                                                                                                                          (add-formulas
                                                                                                                                                           "s12lt"
                                                                                                                                                           "cls3")
                                                                                                                                                          (("1"
                                                                                                                                                            (label
                                                                                                                                                             "tri_inst1"
                                                                                                                                                             -1)
                                                                                                                                                            (("1"
                                                                                                                                                              (add-formulas
                                                                                                                                                               "tri_inst1"
                                                                                                                                                               "tri1inst")
                                                                                                                                                              (("1"
                                                                                                                                                                (label
                                                                                                                                                                 "tri_inst2"
                                                                                                                                                                 -1)
                                                                                                                                                                (("1"
                                                                                                                                                                  (both-sides
                                                                                                                                                                   "-"
                                                                                                                                                                   "d1(seq!1(n!2)`1, p!1) + d1(seq!1(n!2)`2, seq!1(n!2)`1)"
                                                                                                                                                                   "tri_inst2")
                                                                                                                                                                  (("1"
                                                                                                                                                                    (assert)
                                                                                                                                                                    (("1"
                                                                                                                                                                      (copy
                                                                                                                                                                       "arch")
                                                                                                                                                                      (("1"
                                                                                                                                                                        (label
                                                                                                                                                                         "arch2"
                                                                                                                                                                         -1)
                                                                                                                                                                        (("1"
                                                                                                                                                                          (add-formulas
                                                                                                                                                                           "arch2"
                                                                                                                                                                           "arch2")
                                                                                                                                                                          (("1"
                                                                                                                                                                            (add-formulas
                                                                                                                                                                             -1
                                                                                                                                                                             "tri_inst2")
                                                                                                                                                                            (("1"
                                                                                                                                                                              (assert)
                                                                                                                                                                              (("1"
                                                                                                                                                                                (lemma
                                                                                                                                                                                 "both_sides_div_pos_lt2")
                                                                                                                                                                                (("1"
                                                                                                                                                                                  (label
                                                                                                                                                                                   "both_sides_div_pos_lt2"
                                                                                                                                                                                   -1)
                                                                                                                                                                                  (("1"
                                                                                                                                                                                    (inst
                                                                                                                                                                                     "both_sides_div_pos_lt2"
                                                                                                                                                                                     "n!2"
                                                                                                                                                                                     "n!1"
                                                                                                                                                                                     "1")
                                                                                                                                                                                    (("1"
                                                                                                                                                                                      (prop)
                                                                                                                                                                                      (("1"
                                                                                                                                                                                        (hide
                                                                                                                                                                                         -2)
                                                                                                                                                                                        (("1"
                                                                                                                                                                                          (add-formulas
                                                                                                                                                                                           -1
                                                                                                                                                                                           -2)
                                                                                                                                                                                          (("1"
                                                                                                                                                                                            (both-sides
                                                                                                                                                                                             "-"
                                                                                                                                                                                             "2 * (1 / n!1) + 1 / n!2"
                                                                                                                                                                                             -1)
                                                                                                                                                                                            (("1"
                                                                                                                                                                                              (assert)
                                                                                                                                                                                              (("1"
                                                                                                                                                                                                (label
                                                                                                                                                                                                 "d1sp1"
                                                                                                                                                                                                 -1)
                                                                                                                                                                                                (("1"
                                                                                                                                                                                                  (copy
                                                                                                                                                                                                   "pcps")
                                                                                                                                                                                                  (("1"
                                                                                                                                                                                                    (hide
                                                                                                                                                                                                     "pcps")
                                                                                                                                                                                                    (("1"
                                                                                                                                                                                                      (label
                                                                                                                                                                                                       "pcps2"
                                                                                                                                                                                                       -1)
                                                                                                                                                                                                      (("1"
                                                                                                                                                                                                        (copy
                                                                                                                                                                                                         "pcps2")
                                                                                                                                                                                                        (("1"
                                                                                                                                                                                                          (label
                                                                                                                                                                                                           "pcps3"
                                                                                                                                                                                                           -1)
                                                                                                                                                                                                          (("1"
                                                                                                                                                                                                            (inst
                                                                                                                                                                                                             "pcps3"
                                                                                                                                                                                                             "seq!1(n!2)`2"
                                                                                                                                                                                                             "seq!1(n!2)`3")
                                                                                                                                                                                                            (("1"
                                                                                                                                                                                                              (prop)
                                                                                                                                                                                                              (("1"
                                                                                                                                                                                                                (inst
                                                                                                                                                                                                                 "pcps2"
                                                                                                                                                                                                                 "seq!1(n!2)`1"
                                                                                                                                                                                                                 "y!1")
                                                                                                                                                                                                                (("1"
                                                                                                                                                                                                                  (inst
                                                                                                                                                                                                                   "sym1"
                                                                                                                                                                                                                   "p!1"
                                                                                                                                                                                                                   "seq!1(n!2)`1")
                                                                                                                                                                                                                  (("1"
                                                                                                                                                                                                                    (replace
                                                                                                                                                                                                                     "sym1")
                                                                                                                                                                                                                    (("1"
                                                                                                                                                                                                                      (inst
                                                                                                                                                                                                                       "sz2"
                                                                                                                                                                                                                       "y!1"
                                                                                                                                                                                                                       "y!1")
                                                                                                                                                                                                                      (("1"
                                                                                                                                                                                                                        (copy
                                                                                                                                                                                                                         "arch")
                                                                                                                                                                                                                        (("1"
                                                                                                                                                                                                                          (label
                                                                                                                                                                                                                           "arch3"
                                                                                                                                                                                                                           -1)
                                                                                                                                                                                                                          (("1"
                                                                                                                                                                                                                            (add-formulas
                                                                                                                                                                                                                             "cls2"
                                                                                                                                                                                                                             "arch")
                                                                                                                                                                                                                            (("1"
                                                                                                                                                                                                                              (both-sides
                                                                                                                                                                                                                               "-"
                                                                                                                                                                                                                               "1/n!1"
                                                                                                                                                                                                                               -1)
                                                                                                                                                                                                                              (("1"
                                                                                                                                                                                                                                (assert)
                                                                                                                                                                                                                                (("1"
                                                                                                                                                                                                                                  (inst
                                                                                                                                                                                                                                   "tri3"
                                                                                                                                                                                                                                   "f!1(seq!1(n!2)`1,y!1)"
                                                                                                                                                                                                                                   "f!1(p!1,y!1)"
                                                                                                                                                                                                                                   "f!1(seq!1(n!2)`2, seq!1(n!2)`3)")
                                                                                                                                                                                                                                  (("1"
                                                                                                                                                                                                                                    (hide-all-but
                                                                                                                                                                                                                                     ("pcps3"
                                                                                                                                                                                                                                      "pcps2"
                                                                                                                                                                                                                                      "tri3"
                                                                                                                                                                                                                                      "sym3"
                                                                                                                                                                                                                                      "d3gt"
                                                                                                                                                                                                                                      "arch3"))
                                                                                                                                                                                                                                    (("1"
                                                                                                                                                                                                                                      (inst
                                                                                                                                                                                                                                       "sym3"
                                                                                                                                                                                                                                       "f!1(seq!1(n!2)`1, y!1)"
                                                                                                                                                                                                                                       "f!1(p!1, y!1)")
                                                                                                                                                                                                                                      (("1"
                                                                                                                                                                                                                                        (replace
                                                                                                                                                                                                                                         "sym3")
                                                                                                                                                                                                                                        (("1"
                                                                                                                                                                                                                                          (add-formulas
                                                                                                                                                                                                                                           "tri3"
                                                                                                                                                                                                                                           "pcps3")
                                                                                                                                                                                                                                          nil
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil)
                                                                                                                                                                                                                                       ("2"
                                                                                                                                                                                                                                        (expand
                                                                                                                                                                                                                                         "fullset")
                                                                                                                                                                                                                                        (("2"
                                                                                                                                                                                                                                          (propax)
                                                                                                                                                                                                                                          nil
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil)
                                                                                                                                                                                                                                       ("3"
                                                                                                                                                                                                                                        (expand
                                                                                                                                                                                                                                         "fullset")
                                                                                                                                                                                                                                        (("3"
                                                                                                                                                                                                                                          (propax)
                                                                                                                                                                                                                                          nil
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil))
                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                    nil)
                                                                                                                                                                                                                                   ("2"
                                                                                                                                                                                                                                    (expand
                                                                                                                                                                                                                                     "fullset")
                                                                                                                                                                                                                                    (("2"
                                                                                                                                                                                                                                      (propax)
                                                                                                                                                                                                                                      nil
                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                    nil)
                                                                                                                                                                                                                                   ("3"
                                                                                                                                                                                                                                    (expand
                                                                                                                                                                                                                                     "fullset")
                                                                                                                                                                                                                                    (("3"
                                                                                                                                                                                                                                      (propax)
                                                                                                                                                                                                                                      nil
                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                    nil)
                                                                                                                                                                                                                                   ("4"
                                                                                                                                                                                                                                    (expand
                                                                                                                                                                                                                                     "fullset")
                                                                                                                                                                                                                                    (("4"
                                                                                                                                                                                                                                      (propax)
                                                                                                                                                                                                                                      nil
                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                                nil)
                                                                                                                                                                                                                               ("2"
                                                                                                                                                                                                                                (iff)
                                                                                                                                                                                                                                (("2"
                                                                                                                                                                                                                                  (prop)
                                                                                                                                                                                                                                  (("1"
                                                                                                                                                                                                                                    (hide-all-but
                                                                                                                                                                                                                                     (1
                                                                                                                                                                                                                                      "arch3"
                                                                                                                                                                                                                                      "csl"))
                                                                                                                                                                                                                                    (("1"
                                                                                                                                                                                                                                      (name-replace
                                                                                                                                                                                                                                       "A"
                                                                                                                                                                                                                                       "d1(seq!1(n!2)`1, p!1)")
                                                                                                                                                                                                                                      (("1"
                                                                                                                                                                                                                                        (typepred
                                                                                                                                                                                                                                         "A")
                                                                                                                                                                                                                                        (("1"
                                                                                                                                                                                                                                          (cancel-by
                                                                                                                                                                                                                                           1
                                                                                                                                                                                                                                           "n!1*n!1")
                                                                                                                                                                                                                                          nil
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil))
                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                    nil)
                                                                                                                                                                                                                                   ("2"
                                                                                                                                                                                                                                    (hide-all-but
                                                                                                                                                                                                                                     (1
                                                                                                                                                                                                                                      "arch3"
                                                                                                                                                                                                                                      "csl"))
                                                                                                                                                                                                                                    (("2"
                                                                                                                                                                                                                                      (name-replace
                                                                                                                                                                                                                                       "A"
                                                                                                                                                                                                                                       "d1(seq!1(n!2)`1, p!1)")
                                                                                                                                                                                                                                      (("2"
                                                                                                                                                                                                                                        (cross-mult
                                                                                                                                                                                                                                         -2)
                                                                                                                                                                                                                                        (("2"
                                                                                                                                                                                                                                          (add-formulas
                                                                                                                                                                                                                                           "csl"
                                                                                                                                                                                                                                           "csl")
                                                                                                                                                                                                                                          (("2"
                                                                                                                                                                                                                                            (add-formulas
                                                                                                                                                                                                                                             -1
                                                                                                                                                                                                                                             1)
                                                                                                                                                                                                                                            (("2"
                                                                                                                                                                                                                                              (both-sides
                                                                                                                                                                                                                                               "-"
                                                                                                                                                                                                                                               "2 * (A * n!1)"
                                                                                                                                                                                                                                               -1)
                                                                                                                                                                                                                                              (("2"
                                                                                                                                                                                                                                                (assert)
                                                                                                                                                                                                                                                (("2"
                                                                                                                                                                                                                                                  (both-sides
                                                                                                                                                                                                                                                   "-"
                                                                                                                                                                                                                                                   "2"
                                                                                                                                                                                                                                                   -1)
                                                                                                                                                                                                                                                  (("2"
                                                                                                                                                                                                                                                    (assert)
                                                                                                                                                                                                                                                    (("2"
                                                                                                                                                                                                                                                      (case
                                                                                                                                                                                                                                                       "2 * (delta!1 / 2) / 2 = delta!1/2")
                                                                                                                                                                                                                                                      (("1"
                                                                                                                                                                                                                                                        (replace
                                                                                                                                                                                                                                                         -1)
                                                                                                                                                                                                                                                        (("1"
                                                                                                                                                                                                                                                          (mult-ineq
                                                                                                                                                                                                                                                           -2
                                                                                                                                                                                                                                                           -3)
                                                                                                                                                                                                                                                          (("1"
                                                                                                                                                                                                                                                            (assert)
                                                                                                                                                                                                                                                            nil
                                                                                                                                                                                                                                                            nil))
                                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                                        nil)
                                                                                                                                                                                                                                                       ("2"
                                                                                                                                                                                                                                                        (assert)
                                                                                                                                                                                                                                                        nil
                                                                                                                                                                                                                                                        nil))
                                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                                                nil))
                                                                                                                                                                                                                                              nil))
                                                                                                                                                                                                                                            nil))
                                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                                        nil))
                                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                                nil))
                                                                                                                                                                                                                              nil))
                                                                                                                                                                                                                            nil))
                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                        nil)
                                                                                                                                                                                                                       ("2"
                                                                                                                                                                                                                        (expand
                                                                                                                                                                                                                         "fullset")
                                                                                                                                                                                                                        (("2"
                                                                                                                                                                                                                          (propax)
                                                                                                                                                                                                                          nil
                                                                                                                                                                                                                          nil))
                                                                                                                                                                                                                        nil))
                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                    nil)
                                                                                                                                                                                                                   ("2"
                                                                                                                                                                                                                    (expand
                                                                                                                                                                                                                     "fullset")
                                                                                                                                                                                                                    (("2"
                                                                                                                                                                                                                      (propax)
                                                                                                                                                                                                                      nil
                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                    nil)
                                                                                                                                                                                                                   ("3"
                                                                                                                                                                                                                    (expand
                                                                                                                                                                                                                     "fullset")
                                                                                                                                                                                                                    (("3"
                                                                                                                                                                                                                      (propax)
                                                                                                                                                                                                                      nil
                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil)
                                                                                                                                                                                                                 ("2"
                                                                                                                                                                                                                  (reveal
                                                                                                                                                                                                                   "mbs1")
                                                                                                                                                                                                                  (("2"
                                                                                                                                                                                                                    (propax)
                                                                                                                                                                                                                    nil
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                nil)
                                                                                                                                                                                                               ("2"
                                                                                                                                                                                                                (inst
                                                                                                                                                                                                                 "sym1"
                                                                                                                                                                                                                 "p!1"
                                                                                                                                                                                                                 "seq!1(n!2)`2")
                                                                                                                                                                                                                (("1"
                                                                                                                                                                                                                  (replace
                                                                                                                                                                                                                   "sym1")
                                                                                                                                                                                                                  (("1"
                                                                                                                                                                                                                    (reveal
                                                                                                                                                                                                                     "arch2")
                                                                                                                                                                                                                    (("1"
                                                                                                                                                                                                                      (add-formulas
                                                                                                                                                                                                                       "csl"
                                                                                                                                                                                                                       "arch2")
                                                                                                                                                                                                                      nil
                                                                                                                                                                                                                      nil))
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil)
                                                                                                                                                                                                                 ("2"
                                                                                                                                                                                                                  (expand
                                                                                                                                                                                                                   "fullset")
                                                                                                                                                                                                                  (("2"
                                                                                                                                                                                                                    (propax)
                                                                                                                                                                                                                    nil
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil)
                                                                                                                                                                                                                 ("3"
                                                                                                                                                                                                                  (expand
                                                                                                                                                                                                                   "fullset")
                                                                                                                                                                                                                  (("3"
                                                                                                                                                                                                                    (propax)
                                                                                                                                                                                                                    nil
                                                                                                                                                                                                                    nil))
                                                                                                                                                                                                                  nil))
                                                                                                                                                                                                                nil)
                                                                                                                                                                                                               ("3"
                                                                                                                                                                                                                (add-formulas
                                                                                                                                                                                                                 "cls2"
                                                                                                                                                                                                                 "arch")
                                                                                                                                                                                                                nil
                                                                                                                                                                                                                nil))
                                                                                                                                                                                                              nil)
                                                                                                                                                                                                             ("2"
                                                                                                                                                                                                              (reveal
                                                                                                                                                                                                               "mbs3")
                                                                                                                                                                                                              (("2"
                                                                                                                                                                                                                (propax)
                                                                                                                                                                                                                nil
                                                                                                                                                                                                                nil))
                                                                                                                                                                                                              nil)
                                                                                                                                                                                                             ("3"
                                                                                                                                                                                                              (reveal
                                                                                                                                                                                                               "mbs2")
                                                                                                                                                                                                              (("3"
                                                                                                                                                                                                                (propax)
                                                                                                                                                                                                                nil
                                                                                                                                                                                                                nil))
                                                                                                                                                                                                              nil))
                                                                                                                                                                                                            nil))
                                                                                                                                                                                                          nil))
                                                                                                                                                                                                        nil))
                                                                                                                                                                                                      nil))
                                                                                                                                                                                                    nil))
                                                                                                                                                                                                  nil))
                                                                                                                                                                                                nil))
                                                                                                                                                                                              nil)
                                                                                                                                                                                             ("2"
                                                                                                                                                                                              (assert)
                                                                                                                                                                                              nil
                                                                                                                                                                                              nil))
                                                                                                                                                                                            nil))
                                                                                                                                                                                          nil))
                                                                                                                                                                                        nil)
                                                                                                                                                                                       ("2"
                                                                                                                                                                                        (assert)
                                                                                                                                                                                        nil
                                                                                                                                                                                        nil))
                                                                                                                                                                                      nil))
                                                                                                                                                                                    nil))
                                                                                                                                                                                  nil))
                                                                                                                                                                                nil))
                                                                                                                                                                              nil))
                                                                                                                                                                            nil))
                                                                                                                                                                          nil))
                                                                                                                                                                        nil))
                                                                                                                                                                      nil))
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil))
                                                                                                                                                  nil)
                                                                                                                                                 ("2"
                                                                                                                                                  (expand
                                                                                                                                                   "fullset")
                                                                                                                                                  (("2"
                                                                                                                                                    (propax)
                                                                                                                                                    nil
                                                                                                                                                    nil))
                                                                                                                                                  nil)
                                                                                                                                                 ("3"
                                                                                                                                                  (expand
                                                                                                                                                   "fullset")
                                                                                                                                                  (("3"
                                                                                                                                                    (propax)
                                                                                                                                                    nil
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil)
                                                                                                               ("2"
                                                                                                                (expand
                                                                                                                 "fullset")
                                                                                                                (("2"
                                                                                                                  (propax)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil)
                                                                                                               ("3"
                                                                                                                (expand
                                                                                                                 "fullset")
                                                                                                                (("3"
                                                                                                                  (propax)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil)
                                                                                                               ("4"
                                                                                                                (expand
                                                                                                                 "fullset")
                                                                                                                (("4"
                                                                                                                  (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))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skosimp*)
                                  (("2"
                                    (inst "epsq" "n!1")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (skosimp*)
                                  (("3" (assert) nil nil))
                                  nil)
                                 ("4"
                                  (skosimp*)
                                  (("4"
                                    (inst "epsq" "1")
                                    (("4" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "nonempty?")
                                (("2"
                                  (expand "empty?")
                                  (("2"
                                    (expand "member")
                                    (("2"
                                      (inst "csl" "seq!1(1)`1")
                                      (("2"
                                        (inst "epsq" "1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((compact_sequence_limit formula-decl nil compactness nil)
    (metric_space? const-decl "bool" metric_spaces_def nil)
    (space_triangle? const-decl "bool" metric_spaces_def nil)
    (space_zero? const-decl "bool" metric_spaces_def nil)
    (space_symmetric? const-decl "bool" metric_spaces_def nil)
    (product_cont_product_subset formula-decl nil cross_metric_cont
     nil)
    (one_variable_unif_cont_sequence formula-decl nil cross_metric_cont
     nil))
   shostak))
 (multi_Heine_Corollary1 0
  (multi_Heine_Corollary1-1 nil 3460302464
   ("" (skosimp*)
    (("" (lemma "multiary_Heine")
      (("" (inst?)
        (("" (assert)
          (("" (expand "uniformly_continuous_in_first?")
            (("" (inst - "y1!1" "epsilon!1")
              (("" (skosimp*)
                (("" (inst + "delta!1")
                  (("" (skosimp*)
                    (("" (inst - "x!1" "x!1" "y2!1")
                      (("" (prop)
                        (("" (lemma "fullset_metric_space1")
                          (("" (expand "metric_space?")
                            (("" (expand "space_zero?")
                              ((""
                                (prop)
                                ((""
                                  (inst?)
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (expand "fullset")
                                    (("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((multiary_Heine formula-decl nil cross_metric_uniform_continuity
     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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (fullset_metric_space1 formula-decl nil
     cross_metric_uniform_continuity nil)
    (space_zero? const-decl "bool" metric_spaces_def nil)
    (fullset const-decl "set" sets nil)
    (X!1 skolem-const-decl "set[T1]" cross_metric_uniform_continuity
     nil)
    (x!1 skolem-const-decl "(X!1)" cross_metric_uniform_continuity nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (metric_space? const-decl "bool" metric_spaces_def nil)
    (uniformly_continuous_in_first? const-decl "bool" cross_metric_cont
     nil)
    (T3 formal-nonempty-type-decl nil cross_metric_uniform_continuity
     nil)
    (T2 formal-nonempty-type-decl nil cross_metric_uniform_continuity
     nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-nonempty-type-decl nil cross_metric_uniform_continuity
     nil))
   shostak)))