(continuous_functions_props
 (intermediate1 0
  (intermediate1-1 nil 3473169490
   ("" (skosimp)
    (("" (assert)
      (("" (auto-rewrite "sub_interval")
        (("" (lemma "intermediate_value2[a!1, b!1]")
          (("" (inst -1 "R(g!1, a!1, b!1)" "x!1")
            (("" (rewrite "continuous_in_subintervals")
              (("" (expand "R")
                (("" (skolem!)
                  (("" (inst 1 "c!1")
                    (("" (assert) nil))))))))))))))))))
    nil)
   nil nil))
 (intermediate2 0
  (intermediate2-1 nil 3473169490
   ("" (skosimp)
    (("" (assert)
      (("" (auto-rewrite "sub_interval")
        (("" (lemma "intermediate_value4[a!1, b!1]")
          (("" (inst -1 "R(g!1, a!1, b!1)" "x!1")
            (("" (rewrite "continuous_in_subintervals")
              (("" (expand "R")
                (("" (skolem!)
                  (("" (inst 1 "c!1")
                    (("" (assert) nil))))))))))))))))))
    nil)
   nil nil))
 (max_in_interval 0
  (max_in_interval-1 nil 3473169490
   ("" (skosimp)
    (("" (assert)
      (("" (auto-rewrite "sub_interval")
        (("" (lemma "maximum_exists[a!1, b!1]")
          (("" (inst -1 "R(g!1, a!1, b!1)")
            (("" (split)
              (("1" (grind :if-match nil)
                (("1" (inst 1 "c!1")
                  (("1" (assert)
                    (("1" (skosimp)
                      (("1" (inst?) (("1" (assert) nil)))))))))))
               ("2" (rewrite "continuous_in_subintervals")
                nil))))))))))))
    nil)
   ((is_maximum? const-decl "bool" real_fun_preds "reals/")) nil))
 (min_in_interval 0
  (min_in_interval-1 nil 3473169490
   ("" (skosimp)
    (("" (assert)
      (("" (auto-rewrite "sub_interval")
        (("" (lemma "minimum_exists[a!1, b!1]")
          (("" (inst -1 "R(g!1, a!1, b!1)")
            (("" (split)
              (("1" (grind :if-match nil)
                (("1" (inst 1 "c!1")
                  (("1" (assert)
                    (("1" (skosimp)
                      (("1" (inst?) (("1" (assert) nil)))))))))))
               ("2" (rewrite "continuous_in_subintervals")
                nil))))))))))))
    nil)
   ((is_minimum? const-decl "bool" real_fun_preds "reals/")) nil))
 (inj_continuous 0
  (inj_continuous-1 nil 3473169490
   ("" (skosimp)
    (("" (expand "injective?")
      (("" (assert)
        (("" (case "g!1(a!1) <= g!1(c!1)")
          (("1" (ground)
            (("1"
              (lemma "intermediate1"
               ("g" "g!1" "a" "b!1" "b" "c!1" "x" "g!1(a!1)"))
              (("1" (assert)
                (("1" (skosimp)
                  (("1" (inst -5 "a!1" "c!2")
                    (("1" (assert) nil)))))))))
             ("2"
              (lemma "intermediate1"
               ("g" "g!1" "a" "a!1" "b" "b!1" "x" "g!1(c!1)"))
              (("2" (assert)
                (("2" (skosimp)
                  (("2" (inst -5 "c!1" "c!2")
                    (("2" (assert) nil)))))))))))
           ("2" (ground)
            (("1"
              (lemma "intermediate2"
               ("g" "g!1" "a" "a!1" "b" "b!1" "x" "g!1(c!1)"))
              (("1" (assert)
                (("1" (skosimp)
                  (("1" (inst -4 "c!1" "c!2")
                    (("1" (assert) nil)))))))))
             ("2"
              (lemma "intermediate2"
               ("g" "g!1" "a" "b!1" "b" "c!1" "x" "g!1(a!1)"))
              (("2" (assert)
                (("2" (skosimp)
                  (("2" (inst -4 "c!2" "a!1")
                    (("2" (assert) nil))))))))))))))))))
    nil)
   ((injective? const-decl "bool" functions nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (T formal-subtype-decl nil continuous_functions_props nil)
    (T_pred const-decl "[real -> boolean]" continuous_functions_props
     nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (intermediate1 formula-decl nil continuous_functions_props nil)
    (intermediate2 formula-decl nil continuous_functions_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (inj_monotone 0
  (inj_monotone-1 nil 3473169490
   ("" (skolem!)
    (("" (prop)
      (("1" (expand "strict_increasing?")
        (("1" (expand "strict_decreasing?")
          (("1" (skosimp*)
            (("1" (assert)
              (("1" (expand "injective?")
                (("1" (inst-cp -1 "x!1" "y!1")
                  (("1" (inst -1 "x!2" "y!2")
                    (("1" (assert)
                      (("1" (case "x!1 <= x!2")
                        (("1"
                          (lemma "inj_continuous"
                           ("g" "g!1" "a" "x!1" "b" "x!2" "c" "y!2"))
                          (("1" (assert)
                            (("1"
                              (lemma "inj_continuous"
                               ("g"
                                "g!1"
                                "a"
                                "x!1"
                                "b"
                                "y!1"
                                "c"
                                "y!2"))
                              (("1"
                                (lemma
                                 "inj_continuous"
                                 ("g"
                                  "g!1"
                                  "a"
                                  "x!1"
                                  "b"
                                  "y!2"
                                  "c"
                                  "y!1"))
                                (("1" (assert) nil)))))))))
                         ("2"
                          (lemma "inj_continuous"
                           ("g" "g!1" "a" "x!2" "b" "x!1" "c" "y!1"))
                          (("2" (assert)
                            (("2"
                              (lemma "inj_continuous"
                               ("g"
                                "g!1"
                                "a"
                                "x!2"
                                "b"
                                "y!2"
                                "c"
                                "y!1"))
                              (("2"
                                (lemma
                                 "inj_continuous"
                                 ("g"
                                  "g!1"
                                  "a"
                                  "x!2"
                                  "b"
                                  "y!1"
                                  "c"
                                  "y!2"))
                                (("2"
                                  (assert)
                                  nil)))))))))))))))))))))))))))
       ("2" (grind :if-match nil)
        (("2" (inst-cp -3 "x1!1" "x2!1")
          (("2" (inst -3 "x2!1" "x1!1") (("2" (assert) nil)))))))
       ("3" (grind :if-match nil)
        (("3" (inst-cp -3 "x1!1" "x2!1")
          (("3" (inst -3 "x2!1" "x1!1") (("3" (assert) nil))))))))))
    nil)
   ((strict_decreasing? const-decl "bool" real_fun_preds "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (T_pred const-decl "[real -> boolean]" continuous_functions_props
     nil)
    (T formal-subtype-decl nil continuous_functions_props nil)
    (inj_continuous formula-decl nil continuous_functions_props nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil)))