(derivatives_def
 (NQ_TCC1 0
  (NQ_TCC1-1 nil 3253536989 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (deriv_TCC 0
  (deriv_TCC-3 nil 3471267100
   ("" (skosimp*)
    (("" (lemma "deriv_domain")
      (("" (expand "adh")
        (("" (expand "deriv_domain?")
          (("" (expand "fullset")
            (("" (skosimp*)
              (("" (inst - "e!1" "x!1")
                (("" (skosimp*)
                  (("" (inst?)
                    (("" (expand "A") (("" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_domain formula-decl nil derivatives_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (y!1 skolem-const-decl "{u: nzreal | T_pred(u + x!1)}"
     derivatives_def nil)
    (x!1 skolem-const-decl "T" derivatives_def nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def 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)
    (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)
    (fullset const-decl "set" sets nil)
    (adh const-decl "setof[real]" convergence_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)
  (deriv_TCC-2 nil 3471261300
   ("" (skosimp*)
    (("" (lemma "nearzero")
      (("" (expand "adh")
        (("" (expand "fullset")
          (("" (skosimp*)
            (("" (inst - "e!1" "x!1")
              (("" (skosimp*)
                (("" (inst?)
                  (("" (expand "A") (("" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((adh const-decl "setof[real]" convergence_functions nil)) nil)
  (deriv_TCC-1 nil 3253536989
   ("" (skosimp*)
    (("" (expand "adh")
      (("" (expand "fullset")
        (("" (skosimp*) (("" (postpone) nil nil)) nil)) nil))
      nil))
    nil)
   ((adh const-decl "setof[real]" convergence_functions nil)) nil))
 (adh_A_lem 0
  (adh_A_lem-3 nil 3471267122
   ("" (skosimp*)
    (("" (lemma "deriv_domain")
      (("" (expand "deriv_domain?")
        (("" (expand "adh")
          (("" (skosimp*)
            (("" (inst?)
              (("" (inst - "x!1")
                (("" (skosimp*)
                  (("" (inst + "y!1")
                    (("1" (expand "fullset") (("1" (propax) nil nil))
                      nil)
                     ("2" (expand "A") (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_domain formula-decl nil derivatives_def nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (adh const-decl "setof[real]" convergence_functions 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)
    (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 const-decl "set" sets nil)
    (y!1 skolem-const-decl "{u: nzreal | T_pred(u + x!1)}"
     derivatives_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (x!1 skolem-const-decl "T" derivatives_def nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (deriv_domain? const-decl "bool" deriv_domain_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil)
  (adh_A_lem-2 nil 3297610627
   ("" (skosimp*)
    (("" (lemma "nearzero")
      (("" (expand "adh")
        (("" (skosimp*)
          (("" (inst?)
            (("" (inst - "x!1")
              (("" (skosimp*)
                (("" (inst + "y!1")
                  (("1" (expand "fullset") (("1" (propax) nil nil))
                    nil)
                   ("2" (expand "A") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((adh const-decl "setof[real]" convergence_functions nil)) nil)
  (adh_A_lem-1 nil 3297610566
   ("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak))
 (continuous_lim 0
  (continuous_lim-1 nil 3253536989
   (""
    (grind :exclude ("abs" "adh") :rewrites
     ("deriv_TCC" "adherence_fullset[T]") :if-match nil)
    (("1" (inst? -4)
      (("1" (skolem!)
        (("1" (inst + "delta!1")
          (("1" (skosimp)
            (("1" (inst - "x!2 - x!1")
              (("1" (assert) nil nil)
               ("2" (delete -5) (("2" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (inst? -4)
      (("2" (skolem!)
        (("2" (inst + "delta!1")
          (("2" (skosimp :preds? t)
            (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (x!2 skolem-const-decl "T" derivatives_def nil)
    (x!1 skolem-const-decl "T" derivatives_def nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(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)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions nil)
    (convergence const-decl "bool" lim_of_functions nil)
    (convergence const-decl "bool" convergence_functions nil)
    (fullset const-decl "set" sets nil)
    (deriv_TCC formula-decl nil derivatives_def nil))
   nil))
 (deriv_continuous 0
  (deriv_continuous-1 nil 3253536989
   ("" (skosimp)
    (("" (rewrite "continuous_lim" :dir rl)
      ((""
        (case-replace "(LAMBDA (h: (A(x!1))): f!1(h + x!1)) =
           const_fun(f!1(x!1)) + I[(A(x!1))] * NQ(f!1, x!1)")
        (("1" (delete -1)
          (("1"
            (auto-rewrite-theory "lim_of_functions[(A(x!1))]" :exclude
                                 ("convergence"
                                  "convergence_def"
                                  "convergent?"
                                  "lim"
                                  "lim_fun_lemma"
                                  "lim_fun_def")
                                 :always? t)
            (("1" (auto-rewrite "deriv_TCC")
              (("1" (grind :defs nil) nil nil)) nil))
            nil))
          nil)
         ("2" (delete -1 2)
          (("2" (apply-extensionality :hide? t)
            (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
          nil)
         ("3" (delete -1 2) (("3" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((continuous_lim formula-decl nil derivatives_def 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]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (x!1 skolem-const-decl "T" derivatives_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (lim_sum_fun formula-decl nil lim_of_functions nil)
    (lim_prod_fun formula-decl nil lim_of_functions nil)
    (lim_identity formula-decl nil lim_of_functions nil)
    (lim_const_fun formula-decl nil lim_of_functions nil)
    (prod_fun_convergent formula-decl nil lim_of_functions nil)
    (lim_e_del formula-decl nil lim_of_functions nil)
    (sum_fun_convergent formula-decl nil lim_of_functions nil)
    (convergent_identity formula-decl nil lim_of_functions nil)
    (const_fun_convergent formula-decl nil lim_of_functions nil)
    (deriv_TCC formula-decl nil derivatives_def nil)
    (convergence_equiv formula-decl nil lim_of_functions nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (NQ const-decl "real" derivatives_def nil)
    (I const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (const_fun_continuous application-judgement "continuous_fun"
     continuous_functions nil)
    (id_fun_continuous name-judgement "continuous_fun"
     continuous_functions nil))
   nil))
 (derivable_continuous 0
  (derivable_continuous-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (expand "convergent?")
      (("" (skosimp*) (("" (forward-chain "deriv_continuous") nil nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" lim_of_functions nil)
    (deriv_continuous formula-decl nil derivatives_def 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]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives_def nil))
   nil))
 (sum_NQ 0
  (sum_NQ-1 nil 3253536989
   ("" (skolem!)
    (("" (apply-extensionality) (("" (grind) nil nil)) nil)) 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (NQ const-decl "real" derivatives_def nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (neg_NQ 0
  (neg_NQ-1 nil 3442585851
   ("" (skolem!)
    (("" (apply-extensionality) (("" (grind) nil nil)) nil)) 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (NQ const-decl "real" derivatives_def nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (diff_NQ 0
  (diff_NQ-1 nil 3253536989
   ("" (skolem!)
    (("" (apply-extensionality) (("" (grind) nil nil)) nil)) 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (NQ const-decl "real" derivatives_def nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (scal_NQ 0
  (scal_NQ-1 nil 3253536989
   ("" (skolem!)
    (("" (apply-extensionality) (("" (grind) nil nil)) nil)) 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (NQ const-decl "real" derivatives_def nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (const_NQ 0
  (const_NQ-1 nil 3253536989
   ("" (skolem!)
    (("" (apply-extensionality) (("" (grind) nil nil)) nil)) 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (NQ const-decl "real" derivatives_def nil)
    (const_fun_continuous application-judgement "continuous_fun"
     continuous_functions nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (identity_NQ 0
  (identity_NQ-1 nil 3253536989
   ("" (skolem!)
    (("" (apply-extensionality) (("" (grind) nil nil)) nil)) 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (I const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (NQ const-decl "real" derivatives_def nil)
    (id_fun_continuous name-judgement "continuous_fun"
     continuous_functions nil)
    (const_fun_continuous application-judgement "continuous_fun"
     continuous_functions nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (prod_NQ 0
  (prod_NQ-1 nil 3253536989 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (NQ const-decl "real" derivatives_def nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/"))
   nil))
 (cnv_seq_prod_NQ 0
  (cnv_seq_prod_NQ-1 nil 3253536989
   ("" (auto-rewrite "deriv_TCC")
    (("" (skosimp)
      (("" (name "F" "LAMBDA (h : (A(x!1))) : f1!1(x!1 + h)")
        (("1"
          (case-replace
           "NQ(f1!1 * f2!1, x!1) = f2!1(x!1) * NQ(f1!1, x!1) + F * NQ(f2!1, x!1)")
          (("1"
            (auto-rewrite-theory "lim_of_functions[(A(x!1))]" :exclude
                                 ("convergence"
                                  "convergence_def"
                                  "convergent?"
                                  "lim"
                                  "lim_fun_def"
                                  "lim_e_del")
                                 :always? t)
            (("1" (forward-chain "deriv_continuous" -3)
              (("1" (use "continuous_lim")
                (("1" (replace*) (("1" (grind :defs nil) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (replace -1 + rl)
            (("2" (delete -1 -2 -3 2)
              (("2" (apply-extensionality :hide? t)
                (("1" (grind) nil nil)
                 ("2" (delete 2) (("2" (grind) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (delete -1 -2 2) (("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((NQ const-decl "real" derivatives_def nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_continuous formula-decl nil derivatives_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (convergence_equiv formula-decl nil lim_of_functions nil)
    (sum_fun_convergent formula-decl nil lim_of_functions nil)
    (scal_fun_convergent formula-decl nil lim_of_functions nil)
    (prod_fun_convergent formula-decl nil lim_of_functions nil)
    (lim_scal_fun formula-decl nil lim_of_functions nil)
    (lim_prod_fun formula-decl nil lim_of_functions nil)
    (lim_sum_fun formula-decl nil lim_of_functions nil)
    (continuous_lim formula-decl nil derivatives_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (x!1 skolem-const-decl "T" derivatives_def nil)
    (real_plus_real_is_real application-judgement "real" reals 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   nil))
 (inv_NQ 0
  (inv_NQ-1 nil 3253536989 ("" (grind) nil nil)
   ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (NQ const-decl "real" derivatives_def nil)
    (/ const-decl "[T -> real]" real_fun_ops "reals/"))
   nil))
 (cnv_seq_inv_NQ 0
  (cnv_seq_inv_NQ-2 nil 3442586093
   ("" (auto-rewrite "deriv_TCC")
    (("" (skosimp)
      (("" (name "F" "LAMBDA (h : (A(x!1))) : g!1(x!1 + h)")
        (("1"
          (case-replace
           "NQ(1/g!1, x!1) = - NQ(g!1, x!1) / (g!1(x!1) * F)")
          (("1" (rewrite "cv_div[(A(x!1))]")
            (("1" (rewrite "cv_neg[(A(x!1))]") nil nil)
             ("2" (rewrite "cv_scal[(A(x!1))]")
              (("2" (use "continuous_lim" ("f" "g!1"))
                (("2" (ground)
                  (("2" (forward-chain "deriv_continuous") nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (replace -1 + rl)
            (("2" (delete -1 -2 2)
              (("2" (apply-extensionality :hide? t)
                (("1" (grind) nil nil)
                 ("2" (delete 2)
                  (("2" (grind :rewrites "zero_times3") nil nil)) nil))
                nil))
              nil))
            nil)
           ("3" (replace -1 + rl)
            (("3" (delete -1 -2 2)
              (("3" (grind :rewrites "zero_times3") nil nil)) nil))
            nil))
          nil)
         ("2" (delete -1 2) (("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((NQ const-decl "real" derivatives_def nil)
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (cv_scal formula-decl nil lim_of_functions nil)
    (deriv_continuous formula-decl nil derivatives_def nil)
    (continuous_lim formula-decl nil derivatives_def nil)
    (cv_neg formula-decl nil lim_of_functions nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (cv_div formula-decl nil lim_of_functions nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (x!1 skolem-const-decl "T" derivatives_def nil)
    (zero_times3 formula-decl nil real_props nil)
    (real_plus_real_is_real application-judgement "real" reals 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   nil)
  (cnv_seq_inv_NQ-1 nil 3253536989
   ("" (auto-rewrite "deriv_TCC")
    (("" (skosimp)
      (("" (name "F" "LAMBDA (h : (A(x!1))) : g!1(x!1 + h)")
        (("1"
          (case-replace
           "NQ(1/g!1, x!1) = - NQ(g!1, x!1) / (g!1(x!1) * F)")
          (("1" (rewrite "cv_div[(A(x!1))]")
            (("1" (rewrite "cv_opp[(A(x!1))]") nil nil)
             ("2" (rewrite "cv_scal[(A(x!1))]")
              (("2" (use "continuous_lim" ("f" "g!1"))
                (("2" (ground)
                  (("2" (forward-chain "deriv_continuous") nil nil))
                  nil))
                nil))
              nil)
             ("3" (replace -2 1 rl)
              (("3" (delete -1 -2 -3 2)
                (("3" (grind :rewrites "zero_times3") nil nil)) nil))
              nil))
            nil)
           ("2" (replace -1 + rl)
            (("2" (delete -1 -2 2)
              (("2" (apply-extensionality :hide? t)
                (("1" (grind) nil nil)
                 ("2" (delete 2)
                  (("2" (grind :rewrites "zero_times3") nil nil)) nil)
                 ("3" (delete 2) (("3" (grind) nil nil)) nil))
                nil))
              nil))
            nil)
           ("3" (replace -1 + rl)
            (("3" (delete -1 -2 2)
              (("3" (grind :rewrites "zero_times3") nil nil)) nil))
            nil))
          nil)
         ("2" (delete -1 2) (("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((cv_scal formula-decl nil lim_of_functions nil)
    (cv_div formula-decl nil lim_of_functions nil))
   nil))
 (sum_derivable 0
  (sum_derivable-1 nil 3253536989
   ("" (auto-rewrite "derivable?" "sum_NQ" "deriv_TCC")
    (("" (skosimp)
      (("" (assert)
        (("" (use "sum_fun_convergent[(A(x!1))]")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((sum_fun_convergent formula-decl nil lim_of_functions 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (NQ const-decl "real" derivatives_def nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (sum_NQ formula-decl nil derivatives_def nil))
   nil))
 (neg_derivable 0
  (neg_derivable-1 nil 3442586144
   ("" (auto-rewrite "derivable?" "neg_NQ" "deriv_TCC")
    (("" (skosimp)
      (("" (assert)
        (("" (use "neg_fun_convergent[(A(x!1))]")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((neg_fun_convergent formula-decl nil lim_of_functions 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (NQ const-decl "real" derivatives_def nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (neg_NQ formula-decl nil derivatives_def nil))
   nil))
 (diff_derivable 0
  (diff_derivable-1 nil 3253536989
   ("" (auto-rewrite "derivable?" "diff_NQ" "deriv_TCC")
    (("" (skosimp)
      (("" (assert)
        (("" (use "diff_fun_convergent[(A(x!1))]")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((diff_fun_convergent formula-decl nil lim_of_functions 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (NQ const-decl "real" derivatives_def nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (diff_NQ formula-decl nil derivatives_def nil))
   nil))
 (prod_derivable 0
  (prod_derivable-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (expand "convergent?")
      (("" (skosimp*)
        (("" (use "cnv_seq_prod_NQ")
          (("" (assert) (("" (inst?) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" lim_of_functions nil)
    (cnv_seq_prod_NQ formula-decl nil derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives_def nil))
   nil))
 (scal_derivable 0
  (scal_derivable-1 nil 3253536989
   ("" (auto-rewrite "derivable?" "scal_NQ" "deriv_TCC")
    (("" (skosimp)
      (("" (assert)
        (("" (use "scal_fun_convergent[(A(x!1))]")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((scal_fun_convergent formula-decl nil lim_of_functions 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (NQ const-decl "real" derivatives_def nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (scal_NQ formula-decl nil derivatives_def nil))
   nil))
 (const_derivable 0
  (const_derivable-1 nil 3253536989
   ("" (skolem!)
    (("" (auto-rewrite "derivable?" "const_NQ" "deriv_TCC")
      (("" (assert)
        (("" (lemma "const_fun_convergent[(A(x!1))]")
          (("" (inst - "0" "0") nil nil)) nil))
        nil))
      nil))
    nil)
   ((A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (const_fun_convergent formula-decl nil lim_of_functions nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (adh const-decl "setof[real]" convergence_functions nil)
    (deriv_TCC formula-decl nil derivatives_def nil)
    (const_NQ formula-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (const_fun_continuous application-judgement "continuous_fun"
     continuous_functions nil))
   nil))
 (inv_derivable 0
  (inv_derivable-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (expand "convergent?")
      (("" (skosimp*)
        (("" (use "cnv_seq_inv_NQ")
          (("" (assert) (("" (inst?) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" lim_of_functions nil)
    (cnv_seq_inv_NQ formula-decl nil derivatives_def nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives_def nil))
   nil))
 (div_derivable 0
  (div_derivable-1 nil 3253536989
   ("" (skosimp)
    (("" (rewrite "div_function[T]")
      (("" (rewrite "prod_derivable")
        (("" (rewrite "inv_derivable") nil nil)) nil))
      nil))
    nil)
   ((div_function formula-decl nil real_fun_ops "reals/")
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals 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]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (inv_derivable formula-decl nil derivatives_def nil)
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (prod_derivable formula-decl nil derivatives_def nil))
   nil))
 (identity_derivable 0
  (identity_derivable-1 nil 3253536989
   ("" (skolem!)
    (("" (auto-rewrite "derivable?" "identity_NQ" "deriv_TCC")
      (("" (assert)
        (("" (use "const_fun_convergent[(A(x!1))]" ("b" "1" "c" "0"))
          nil nil))
        nil))
      nil))
    nil)
   ((deriv_TCC formula-decl nil derivatives_def nil)
    (const_fun_convergent formula-decl nil lim_of_functions nil)
    (adh const-decl "setof[real]" convergence_functions nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (identity_NQ formula-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (id_fun_continuous name-judgement "continuous_fun"
     continuous_functions nil)
    (const_fun_continuous application-judgement "continuous_fun"
     continuous_functions nil))
   nil))
 (deriv_TCC1 0
  (deriv_TCC1-1 nil 3253536989
   ("" (auto-rewrite "derivable?")
    (("" (skosimp :preds? t) (("" (assert) nil nil)) nil)) nil)
   ((derivable? const-decl "bool" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (deriv_def 0
  (deriv_def-1 nil 3297521117
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "derivable?")
        (("1" (expand "convergent?") (("1" (inst + "l!1") nil nil))
          nil))
        nil)
       ("2" (expand "deriv")
        (("2" (rewrite "lim_fun_def")
          (("2" (hide 2)
            (("2" (expand "convergent?") (("2" (inst + "l!1") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" lim_of_functions 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)
    (derivable? const-decl "bool" derivatives_def nil)
    (lim_fun_def formula-decl nil lim_of_functions nil)
    (NQ const-decl "real" derivatives_def nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (deriv const-decl "real" derivatives_def nil))
   shostak))
 (deriv_sum_TCC1 0
  (deriv_sum_TCC1-1 nil 3253536989
   ("" (skosimp) (("" (rewrite "sum_derivable") nil nil)) nil)
   ((sum_derivable formula-decl nil derivatives_def 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]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil))
   nil))
 (deriv_sum 0
  (deriv_sum-1 nil 3253536989
   ("" (skosimp)
    ((""
      (auto-rewrite "deriv_TCC" "sum_derivable" "derivable?" "deriv"
                    "sum_NQ" "lim_sum_fun[(A(x!1))]")
      (("" (assert) nil nil)) nil))
    nil)
   ((derivable? const-decl "bool" derivatives_def nil)
    (sum_NQ formula-decl nil derivatives_def nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (lim_sum_fun formula-decl nil lim_of_functions nil)
    (deriv const-decl "real" derivatives_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (deriv_neg_TCC1 0
  (deriv_neg_TCC1-1 nil 3442582979
   ("" (lemma "neg_derivable") (("" (propax) nil nil)) nil)
   ((neg_derivable formula-decl nil derivatives_def nil)) shostak))
 (deriv_neg 0
  (deriv_neg-2 nil 3442586421
   ("" (skosimp)
    ((""
      (auto-rewrite "deriv_TCC" "neg_derivable" "derivable?" "deriv"
                    "neg_NQ" "lim_neg_fun[(A(x!1))]")
      (("" (assert) nil nil)) nil))
    nil)
   ((derivable? const-decl "bool" derivatives_def nil)
    (neg_NQ formula-decl nil derivatives_def nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (lim_neg_fun formula-decl nil lim_of_functions nil)
    (deriv const-decl "real" derivatives_def nil)
    (minus_real_is_real application-judgement "real" reals nil))
   nil)
  (deriv_neg-1 nil 3442586370
   (";;; Proof for formula derivatives_def.deriv_opposite" (skosimp)
    ((";;; Proof for formula derivatives_def.deriv_opposite"
      (auto-rewrite "deriv_TCC" "opposite_derivable" "derivable?"
                    "deriv" "opposite_NQ" "lim_opposite_fun[(A(x!1))]")
      ((";;; Proof for formula derivatives_def.deriv_opposite" (assert)
        nil))))
    "")
   nil nil))
 (deriv_diff_TCC1 0
  (deriv_diff_TCC1-1 nil 3253536989
   ("" (skosimp) (("" (rewrite "diff_derivable") nil nil)) nil)
   ((diff_derivable formula-decl nil derivatives_def 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]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil))
   nil))
 (deriv_diff 0
  (deriv_diff-1 nil 3253536989
   ("" (skosimp)
    ((""
      (auto-rewrite "deriv_TCC" "diff_derivable" "derivable?" "deriv"
                    "diff_NQ" "lim_diff_fun[(A(x!1))]")
      (("" (assert) nil nil)) nil))
    nil)
   ((derivable? const-decl "bool" derivatives_def nil)
    (diff_NQ formula-decl nil derivatives_def nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (lim_diff_fun formula-decl nil lim_of_functions nil)
    (deriv const-decl "real" derivatives_def nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (deriv_prod_TCC1 0
  (deriv_prod_TCC1-1 nil 3253536989
   ("" (skosimp) (("" (rewrite "prod_derivable") nil nil)) nil)
   ((prod_derivable formula-decl nil derivatives_def 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]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil))
   nil))
 (deriv_prod 0
  (deriv_prod-1 nil 3253536989
   ("" (skosimp)
    (("" (use "prod_derivable")
      (("" (assert)
        ((""
          (auto-rewrite "deriv" "deriv_TCC" "derivable?"
                        ("lim_fun_def[(A(x!1))]"
                         "lim_fun_lemma[(A(x!1))]"))
          (("" (assert)
            ((""
              (use "cnv_seq_prod_NQ"
                   ("l1" "lim(NQ(f1!1, x!1), 0)" "l2"
                    "lim(NQ(f2!1, x!1), 0)"))
              (("" (ground) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((prod_derivable formula-decl nil derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def 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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (NQ const-decl "real" derivatives_def nil)
    (lim const-decl "{l: real | convergence(f, x0, l)}"
     lim_of_functions nil)
    (convergence const-decl "bool" lim_of_functions nil)
    (convergent? const-decl "bool" lim_of_functions nil)
    (cnv_seq_prod_NQ formula-decl nil derivatives_def nil)
    (lim_fun_lemma formula-decl nil lim_of_functions nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (deriv const-decl "real" derivatives_def nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (lim_fun_def formula-decl nil lim_of_functions nil))
   nil))
 (deriv_const_TCC1 0
  (deriv_const_TCC1-1 nil 3253536989
   ("" (lemma "const_derivable") (("" (propax) nil nil)) nil)
   ((const_derivable formula-decl nil derivatives_def nil)) nil))
 (deriv_const 0
  (deriv_const-1 nil 3253536989
   ("" (skosimp)
    ((""
      (auto-rewrite "deriv_TCC" "const_derivable" "derivable?" "deriv"
                    "const_NQ")
      (("" (assert)
        (("" (use "lim_const_fun[(A(x!1))]" ("b" "0" "c" "0")) nil
          nil))
        nil))
      nil))
    nil)
   ((deriv_TCC formula-decl nil derivatives_def nil)
    (lim_const_fun formula-decl nil lim_of_functions nil)
    (adh const-decl "setof[real]" convergence_functions nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (const_NQ formula-decl nil derivatives_def nil)
    (deriv const-decl "real" derivatives_def nil)
    (const_fun_continuous application-judgement "continuous_fun"
     continuous_functions nil))
   nil))
 (deriv_scal_TCC1 0
  (deriv_scal_TCC1-1 nil 3253536989
   ("" (lemma "scal_derivable") (("" (propax) nil nil)) nil)
   ((scal_derivable formula-decl nil derivatives_def nil)) nil))
 (deriv_scal 0
  (deriv_scal-1 nil 3253536989
   ("" (skosimp)
    ((""
      (auto-rewrite "deriv_TCC" "scal_derivable" "derivable?" "deriv"
                    "scal_NQ" "lim_scal_fun[(A(x!1))]")
      (("" (assert) nil nil)) nil))
    nil)
   ((derivable? const-decl "bool" derivatives_def nil)
    (scal_NQ formula-decl nil derivatives_def nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (lim_scal_fun formula-decl nil lim_of_functions nil)
    (deriv const-decl "real" derivatives_def nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (deriv_inv_TCC1 0
  (deriv_inv_TCC1-1 nil 3253536989
   ("" (lemma "inv_derivable") (("" (propax) nil nil)) nil)
   ((inv_derivable formula-decl nil derivatives_def nil)) nil))
 (deriv_inv 0
  (deriv_inv-1 nil 3253536989
   ("" (skosimp)
    (("" (forward-chain "inv_derivable")
      (("" (assert)
        ((""
          (auto-rewrite "deriv" "deriv_TCC" "derivable?"
                        ("lim_fun_def[(A(x!1))]"
                         "lim_fun_lemma[(A(x!1))]"))
          (("" (assert)
            (("" (use "cnv_seq_inv_NQ" ("l1" "lim(NQ(g!1, x!1), 0)"))
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inv_derivable formula-decl nil derivatives_def 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]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (NQ const-decl "real" derivatives_def nil)
    (lim const-decl "{l: real | convergence(f, x0, l)}"
     lim_of_functions nil)
    (convergence const-decl "bool" lim_of_functions nil)
    (convergent? const-decl "bool" lim_of_functions nil)
    (cnv_seq_inv_NQ formula-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (deriv const-decl "real" derivatives_def nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (lim_fun_def formula-decl nil lim_of_functions nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil))
   nil))
 (deriv_div_TCC1 0
  (deriv_div_TCC1-1 nil 3253536989
   ("" (skosimp) (("" (rewrite "div_derivable") nil nil)) nil)
   ((div_derivable formula-decl nil derivatives_def 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]" derivatives_def nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil))
   nil))
 (deriv_div 0
  (deriv_div-1 nil 3253536989
   (""
    (grind :defs nil :rewrites
     ("inv_derivable" "deriv_inv" "deriv_prod" "div_function[T]" "/"))
    nil nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (inv_derivable formula-decl nil derivatives_def nil)
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_inv formula-decl nil derivatives_def nil)
    (deriv_prod formula-decl nil derivatives_def nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def 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)
    (div_function formula-decl nil real_fun_ops "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil))
   nil))
 (deriv_identity_TCC1 0
  (deriv_identity_TCC1-1 nil 3253536989
   ("" (lemma "identity_derivable") (("" (propax) nil nil)) nil)
   ((identity_derivable formula-decl nil derivatives_def nil)) nil))
 (deriv_identity 0
  (deriv_identity-1 nil 3253536989
   ("" (skosimp)
    ((""
      (auto-rewrite "deriv_TCC" "identity_derivable" "derivable?"
                    "deriv" "identity_NQ")
      (("" (use "lim_const_fun[(A(x!1))]" ("b" "1" "c" "0"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((identity_NQ formula-decl nil derivatives_def nil)
    (deriv const-decl "real" derivatives_def nil)
    (id_fun_continuous name-judgement "continuous_fun"
     continuous_functions nil)
    (const_fun_continuous application-judgement "continuous_fun"
     continuous_functions nil)
    (A const-decl "setof[nzreal]" derivatives_def nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil derivatives_def nil)
    (T_pred const-decl "[real -> boolean]" derivatives_def nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (adh const-decl "setof[real]" convergence_functions nil)
    (lim_const_fun formula-decl nil lim_of_functions nil)
    (deriv_TCC formula-decl nil derivatives_def nil))
   nil)))