(ms_composition_cont
 (IMP_continuity_ms_TCC1 0
  (IMP_continuity_ms_TCC1-1 nil 3462096232
   ("" (lemma "fullset_metric_space1") (("" (propax) nil nil)) nil)
   ((fullset_metric_space1 formula-decl nil ms_composition_cont nil))
   nil))
 (IMP_continuity_ms_TCC2 0
  (IMP_continuity_ms_TCC2-1 nil 3462096232
   ("" (lemma "fullset_metric_space2") (("" (propax) nil nil)) nil)
   ((fullset_metric_space2 formula-decl nil ms_composition_cont nil))
   nil))
 (IMP_continuity_ms_TCC3 0
  (IMP_continuity_ms_TCC3-1 nil 3462096232
   ("" (lemma "fullset_metric_space3") (("" (propax) nil nil)) nil)
   ((fullset_metric_space3 formula-decl nil ms_composition_cont nil))
   nil))
 (composition_continuous 0
  (composition_continuous-1 nil 3462096289
   ("" (skosimp*)
    (("" (label "finalcont" 1)
      (("" (label "imcont" -2)
        (("" (label "firstcont" -1)
          (("" (expand "continuous?")
            (("" (skosimp*)
              (("" (inst "firstcont" "x!1")
                (("" (inst "imcont" "f!1(x!1)")
                  (("1" (expand "continuous_at?")
                    (("1" (skosimp*)
                      (("1" (inst "imcont" "epsilon!1")
                        (("1" (skosimp*)
                          (("1" (inst "firstcont" "delta!1")
                            (("1" (skosimp*)
                              (("1"
                                (inst "finalcont" "delta!2")
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (inst "firstcont" "y!1")
                                    (("1"
                                      (inst "imcont" "f!1(y!1)")
                                      (("1" (grind) nil nil)
                                       ("2"
                                        (expand "image")
                                        (("2" (inst + "y!1") nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "image") (("2" (inst + "x!1") nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((x!1 skolem-const-decl "(S!1)" ms_composition_cont nil)
    (S!1 skolem-const-decl "set[T1]" ms_composition_cont nil)
    (f!1 skolem-const-decl "[T1 -> T2]" ms_composition_cont nil)
    (image const-decl "set[R]" function_image nil)
    (T2 formal-nonempty-type-decl nil ms_composition_cont nil)
    (y!1 skolem-const-decl "(S!1)" ms_composition_cont nil)
    (ball const-decl "set[T]" metric_spaces nil)
    (member const-decl "bool" sets nil)
    (O const-decl "T3" function_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (continuous_at? const-decl "bool" continuity_ms_def 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 ms_composition_cont nil)
    (continuous? const-decl "bool" continuity_ms_def nil))
   shostak)))