Impressum interval_deriv.prf

(interval_deriv
 (deriv_domain_Xt 0
  (deriv_domain_Xt-2 nil 3545779310
   ("" (typepred "X")
    (("" (expand "StrictInterval?")
      (("" (lemma "deriv_domain_closed")
        (("" (inst - "lb(X)" "ub(X)")
          (("" (assert)
            (("" (expand "deriv_domain?")
              (("" (skosimp*)
                (("" (inst - "e!1" "x!1")
                  (("1" (skosimp*)
                    (("1" (inst + "y!1") (("1" (grind) nil nil)) nil))
                    nil)
                   ("2" (assert)
                    (("2" (hide 2)
                      (("2" (typepred "x!1")
                        (("2" (expand "##") (("2" (propax) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (|##| const-decl "bool" interval nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (x!1 skolem-const-decl "Xt" interval_deriv 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)
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (y!1 skolem-const-decl
     "{u: nzreal | lb(X) <= u + x!1 AND u + x!1 <= ub(X)}"
     interval_deriv nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (deriv_domain_closed formula-decl nil deriv_domain "analysis/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil))
   nil)
  (deriv_domain_Xt-1 nil 3472488588
   ("" (typepred "X")
    (("" (expand "StrictlyProper?")
      (("" (lemma "deriv_domain_closed")
        (("" (inst - "lb(X)" "ub(X)")
          (("" (assert)
            (("" (expand "deriv_domain?")
              (("" (skosimp*)
                (("" (inst - "e!1" "x!1")
                  (("1" (skosimp*)
                    (("1" (inst + "y!1") (("1" (grind) nil nil)) nil))
                    nil)
                   ("2" (assert)
                    (("2" (hide 2)
                      (("2" (typepred "x!1")
                        (("2" (expand "##") (("2" (propax) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (closed_interval type-eq-decl nil intervals_real "reals/")
    (deriv_domain_closed formula-decl nil deriv_domain "analysis/")
    (Interval type-eq-decl nil interval nil))
   nil))
 (IMP_derivatives_TCC1 0
  (IMP_derivatives_TCC1-1 nil 3301761309
   ("" (lemma "deriv_domain_Xt") (("" (propax) nil nil)) nil)
   ((deriv_domain_Xt formula-decl nil interval_deriv nil)) shostak))
 (IMP_derivatives_TCC2 0
  (IMP_derivatives_TCC2-1 nil 3301761489
   ("" (expand "not_one_element?")
    (("" (skeep)
      (("" (typepred "x")
        (("" (typepred "X")
          (("" (inst 1 "if x=lb(X) then ub(X) else lb(X) endif")
            (("1" (grind) nil nil) ("2" (grind) nil nil)
             ("3" (grind) nil nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (/= const-decl "boolean" notequal nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (x skolem-const-decl "Xt" interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
   shostak))
 (D_TCC1 0
  (D_TCC1-1 nil 3304700431
   ("" (skosimp :preds? t)
    (("" (expand "Diff?") (("" (propax) nil nil)) 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (Diffn?_TCC1 0
  (Diffn?_TCC1-1 nil 3321368055
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (Diffn?_TCC2 0
  (Diffn?_TCC2-1 nil 3321368055
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (Diffn_derivn 0
  (Diffn_derivn-2 nil 3445354344
   ("" (induct "n")
    (("1" (grind) nil nil)
     ("2" (skeep)
      (("2" (skeep)
        (("2" (expand "Diffn?" 1)
          (("2" (expand "derivable_n_times?" 1)
            (("2" (expand "Diff?")
              (("2" (inst -1 "D(f)")
                (("1" (expand "D" -1 2) (("1" (replaces -1) nil nil))
                  nil)
                 ("2" (expand "Diff?") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Diff? const-decl "bool" interval_deriv nil)
    (D const-decl "[Xt -> real]" interval_deriv nil)
    (f skolem-const-decl "[Xt -> real]" interval_deriv nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
    (Diffn? def-decl "bool" interval_deriv nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil)
  (Diffn_derivn-1 nil 3321368515
   ("" (induct "n")
    (("1" (grind) nil nil)
     ("2" (skeep)
      (("2" (skeep)
        (("2" (expand "Diffn?" 1)
          (("2" (expand "derivable_n_times" 1)
            (("2" (expand "Diff?")
              (("2" (inst -1 "D(f)")
                (("1" (expand "D" -1 2) (("1" (replaces -1) nil nil))
                  nil)
                 ("2" (expand "Diff?") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Interval type-eq-decl nil interval nil)) shostak))
 (Dn_TCC1 0
  (Dn_TCC1-1 nil 3321368055 ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (Dn_TCC2 0
  (Dn_TCC2-1 nil 3321368055
   ("" (skosimp* :preds? t)
    (("" (expand "Diffn?") (("" (assert) nil nil)) nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diffn? def-decl "bool" interval_deriv nil))
   nil))
 (Dn_TCC3 0
  (Dn_TCC3-1 nil 3321368055
   ("" (skosimp* :preds? t)
    (("" (expand "Diffn?" -2) (("" (assert) nil nil)) nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diffn? def-decl "bool" interval_deriv nil))
   nil))
 (Dn_TCC4 0
  (Dn_TCC4-1 nil 3321368055 ("" (skosimp) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (Dn_nderiv_TCC1 0
  (Dn_nderiv_TCC1-1 nil 3321368411
   ("" (skosimp* :preds? t)
    (("" (lemma "Diffn_derivn")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((Diffn_derivn formula-decl nil interval_deriv nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diffn? def-decl "bool" interval_deriv nil))
   nil))
 (Dn_nderiv 0
  (Dn_nderiv-1 nil 3321368706
   ("" (induct "n")
    (("1" (grind) nil nil)
     ("2" (skeep)
      (("2" (skeep :preds? t)
        (("2" (expand "Dn" 1)
          (("2" (expand "nderiv" 1)
            (("2" (expand "Diffn?" -1)
              (("2" (flatten)
                (("2" (inst -3 "D(f)")
                  (("2" (expand "D" -3 2) (("2" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2)
      (("3" (skeep :preds? t) (("3" (rewrite "Diffn_derivn") nil nil))
        nil))
      nil))
    nil)
   ((Diffn_derivn formula-decl nil interval_deriv nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (D const-decl "[Xt -> real]" interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
    (nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
    (Dn def-decl "[Xt -> real]" interval_deriv nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diffn? def-decl "bool" interval_deriv nil)
    (derivable_n_times? def-decl "bool" nth_derivatives "analysis/"))
   shostak))
 (Diff_id 0
  (Diff_id-1 nil 3304425174
   ("" (expand "Diff?")
    (("" (lemma "derivable_id")
      (("" (expand "I") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval 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_id judgement-tcc nil derivatives "analysis/")
    (I const-decl "(bijective?[T, T])" identity nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_id_TCC1 0
  (D_id_TCC1-1 nil 3304424118 ("" (rewrite "Diff_id") nil nil)
   ((Diff_id formula-decl nil interval_deriv nil)) shostak))
 (D_id 0
  (D_id-1 nil 3304429116
   ("" (expand "D")
    (("" (lemma "deriv_id_fun")
      (("" (expand "I")
        (("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval 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)
    (deriv_id_fun formula-decl nil derivatives "analysis/")
    (D const-decl "[Xt -> real]" interval_deriv nil))
   shostak))
 (Diff_const 0
  (Diff_const-1 nil 3304425582
   ("" (skosimp)
    (("" (expand "Diff?")
      (("" (lemma "derivable_const")
        (("" (inst?)
          (("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((Diff? const-decl "bool" interval_deriv nil)
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable_const judgement-tcc nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil))
   shostak))
 (D_const_TCC1 0
  (D_const_TCC1-1 nil 3304424144
   ("" (skosimp) (("" (rewrite "Diff_const") nil nil)) nil)
   ((Diff_const formula-decl nil interval_deriv 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))
   shostak))
 (D_const 0
  (D_const-1 nil 3304430079
   ("" (skosimp)
    (("" (expand "D")
      (("" (lemma "deriv_const_fun")
        (("" (inst -1 "a!1")
          (("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (deriv_const_fun formula-decl nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil))
   shostak))
 (Diff_add 0
  (Diff_add-1 nil 3304429143
   ("" (skosimp :preds? t)
    (("" (expand "Diff?")
      (("" (lemma "derivable_sum")
        (("" (inst -1 "f!1" "g!1")
          (("" (expand "+") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable_sum judgement-tcc nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   nil))
 (D_add_TCC1 0
  (D_add_TCC1-1 nil 3304424494
   ("" (skosimp) (("" (rewrite "Diff_add") nil nil)) nil)
   ((Diff_add formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_add 0
  (D_add-1 nil 3304430121
   ("" (skosimp :preds? t)
    (("" (expand* "Diff?" "D")
      (("" (lemma "deriv_sum_fun")
        (("" (inst -1 "f!1" "g!1")
          (("" (expand "+") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_sum_fun formula-decl nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (Diff_mult 0
  (Diff_mult-1 nil 3304429240
   ("" (skosimp :preds? t)
    (("" (expand "Diff?")
      (("" (lemma "derivable_prod")
        (("" (inst -1 "f!1" "g!1")
          (("" (expand "*") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable_prod judgement-tcc nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_mult_TCC1 0
  (D_mult_TCC1-1 nil 3304424503
   ("" (skosimp) (("" (rewrite "Diff_mult") nil nil)) nil)
   ((Diff_mult formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_mult 0
  (D_mult-1 nil 3304430162
   ("" (skosimp :preds? t)
    (("" (expand* "Diff?" "D")
      (("" (lemma "deriv_prod_fun")
        (("" (inst -1 "f!1" "g!1")
          (("" (expand "*")
            (("" (expand "+") (("" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_prod_fun formula-decl nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (Diff_pow_TCC1 0
  (Diff_pow_TCC1-1 nil 3305042267 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) shostak))
 (Diff_pow 0
  (Diff_pow-1 nil 3305042471
   ("" (skeep)
    (("" (case "n=0")
      (("1" (replaces)
        (("1" (expand "^")
          (("1" (expand "expt") (("1" (rewrite "Diff_const") nil nil))
            nil))
          nil))
        nil)
       ("2" (expand "Diff?")
        (("2" (lemma "deriv_x_to_n")
          (("2" (inst -1 "n" "1")
            (("1" (beta) (("1" (flatten) (("1" (assert) nil nil)) nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (^ const-decl "real" exponentiation nil)
    (Diff_const formula-decl nil interval_deriv nil)
    (expt def-decl "real" exponentiation nil)
    (deriv_x_to_n formula-decl nil derivatives "analysis/")
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (n skolem-const-decl "nat" interval_deriv nil)
    (> const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_pow_TCC1 0
  (D_pow_TCC1-1 nil 3305042277 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) shostak))
 (D_pow_TCC2 0
  (D_pow_TCC2-1 nil 3305042285
   ("" (skosimp) (("" (rewrite "Diff_pow") nil nil)) nil)
   ((Diff_pow formula-decl nil interval_deriv 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil))
   shostak))
 (D_pow_TCC3 0
  (D_pow_TCC3-1 nil 3305042306 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) shostak))
 (D_pow 0
  (D_pow-1 nil 3305042697
   ("" (skeep)
    (("" (expand "D")
      (("" (lemma "deriv_x_to_n")
        (("" (inst -1 "m" "1")
          (("" (beta) (("" (flatten) (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (deriv_x_to_n formula-decl nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil))
   shostak))
 (Diff_scal1 0
  (Diff_scal1-2 nil 3304699767
   ("" (skosimp :preds? t)
    (("" (expand "Diff?")
      (("" (lemma "derivable_scal")
        (("" (inst -1 "a!1" "f!1")
          (("" (expand "*") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable_scal judgement-tcc nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   nil))
 (D_scal1_TCC1 0
  (D_scal1_TCC1-2 nil 3304431213
   ("" (skosimp) (("" (rewrite "Diff_scal1") nil nil)) nil)
   ((Diff_scal1 formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   nil))
 (D_scal1 0
  (D_scal1-1 nil 3304431129
   ("" (skosimp :preds? t)
    (("" (expand* "Diff?" "D")
      (("" (lemma "deriv_scal_fun")
        (("" (inst -1 "a!1" "f!1")
          (("" (expand "*") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_scal_fun formula-decl nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   nil))
 (Diff_scal2 0
  (Diff_scal2-1 nil 3304431294
   ("" (skosimp :preds? t)
    (("" (lemma "Diff_scal1")
      (("" (inst -1 "a!1" "f!1") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((Diff_scal1 formula-decl nil interval_deriv nil)
    (real_times_real_is_real application-judgement "real" 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_scal2_TCC1 0
  (D_scal2_TCC1-2 nil 3304431448
   ("" (skosimp) (("" (rewrite "Diff_scal2") nil nil)) nil)
   ((Diff_scal2 formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   nil))
 (D_scal2 0
  (D_scal2-1 nil 3304431330
   ("" (skosimp :preds? t)
    (("" (lemma "D_scal1")
      (("" (inst -1 "a!1" "f!1") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((D_scal1 formula-decl nil interval_deriv nil)
    (real_times_real_is_real application-judgement "real" 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (Diff_neg 0
  (Diff_neg-2 nil 3442593099
   ("" (skosimp :preds? t)
    (("" (expand "Diff?")
      (("" (lemma "derivable_neg")
        (("" (inst -1 "g!1")
          (("" (expand "-") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable_neg judgement-tcc nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   nil)
  (Diff_neg-1 nil 3304429291
   ("" (skosimp :preds? t)
    (("" (expand "Diff?")
      (("" (lemma "derivable_opp")
        (("" (inst -1 "g!1")
          (("" (expand "-") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((deriv_fun type-eq-decl nil derivatives "analysis/")
    (Interval type-eq-decl nil interval nil))
   shostak))
 (D_neg_TCC1 0
  (D_neg_TCC1-1 nil 3304424526
   ("" (skosimp) (("" (rewrite "Diff_neg") nil nil)) nil)
   ((Diff_neg formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_neg 0
  (D_neg-2 nil 3442592991
   ("" (skosimp :preds? t)
    (("" (expand* "Diff?" "D")
      (("" (lemma "deriv_neg_fun")
        (("" (inst -1 "g!1")
          (("" (expand "-") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_neg_fun formula-decl nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   nil)
  (D_neg-1 nil 3304430224
   ("" (skosimp :preds? t)
    (("" (expand* "Diff?" "D")
      (("" (lemma "deriv_opp_fun")
        (("" (inst -1 "g!1")
          (("" (expand "-") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((deriv_fun type-eq-decl nil derivatives "analysis/")
    (Interval type-eq-decl nil interval nil))
   shostak))
 (Diff_sub 0
  (Diff_sub-1 nil 3304429323
   ("" (skosimp :preds? t)
    (("" (expand "Diff?")
      (("" (lemma "derivable_diff")
        (("" (inst -1 "f!1" "g!1")
          (("" (expand "-") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable_diff judgement-tcc nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_sub_TCC1 0
  (D_sub_TCC1-1 nil 3304424618
   ("" (skosimp) (("" (rewrite "Diff_sub") nil nil)) nil)
   ((Diff_sub formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_sub 0
  (D_sub-1 nil 3304430250
   ("" (skosimp :preds? t)
    (("" (expand* "Diff?" "D")
      (("" (lemma "deriv_diff_fun")
        (("" (inst -1 "f!1" "g!1")
          (("" (expand "-") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (g!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_diff_fun formula-decl nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (Diff_sq 0
  (Diff_sq-1 nil 3304429366
   ("" (expand "sq")
    (("" (rewrite "Diff_mult") (("" (rewrite "Diff_id") nil nil)) nil))
    nil)
   ((Diff_mult formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (Diff_id formula-decl nil interval_deriv nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (D_sq_TCC1 0
  (D_sq_TCC1-1 nil 3304424624 ("" (rewrite "Diff_sq") nil nil)
   ((Diff_sq formula-decl nil interval_deriv nil)) shostak))
 (D_sq 0
  (D_sq-1 nil 3304430266
   ("" (expand "sq")
    (("" (rewrite "D_mult")
      (("1" (rewrite "D_id") (("1" (assert) nil nil)) nil)
       ("2" (rewrite "Diff_id") nil nil))
      nil))
    nil)
   ((D_mult formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (D_id formula-decl nil interval_deriv nil)
    (Diff_id formula-decl nil interval_deriv nil)
    (sq const-decl "nonneg_real" sq "reals/"))
   shostak))
 (Diff_div_TCC1 0
  (Diff_div_TCC1-1 nil 3304431499
   ("" (skosimp :preds? t)
    (("" (inst -2 "t!1") (("" (assert) nil nil)) 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (Diff_div 0
  (Diff_div-1 nil 3304431982
   ("" (skosimp :preds? t)
    (("" (expand "Diff?")
      (("" (lemma "derivable_div")
        (("" (inst -1 "f!1" "k!1")
          (("1" (expand "/") (("1" (propax) nil nil)) nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (k!1 skolem-const-decl "(LAMBDA (f): FORALL (t: Xt): f(t) /= 0)"
     interval_deriv nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nz_deriv_fun type-eq-decl nil derivatives "analysis/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable_div judgement-tcc nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (D_div_TCC1 0
  (D_div_TCC1-1 nil 3304431524
   ("" (skosimp :preds? t) (("" (rewrite "Diff_div") nil nil)) nil)
   ((Diff_div formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (D_div_TCC2 0
  (D_div_TCC2-1 nil 3304431579
   ("" (skosimp :preds? t)
    (("" (inst -2 "t!1")
      (("" (hide -1 -3)
        (("" (expand "sq") (("" (grind-reals) nil nil)) nil)) nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (nonzero_times3 formula-decl nil real_props 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (D_div 0
  (D_div-1 nil 3304432155
   ("" (skosimp :preds? t)
    (("" (expand* "Diff?" "D")
      (("" (lemma "deriv_div_fun")
        (("" (inst -1 "f!1" "k!1")
          (("1" (expand "/")
            (("1" (expand "sq")
              (("1" (expand "*")
                (("1" (assert)
                  (("1" (expand "-") (("1" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (f!1 skolem-const-decl "(Diff?)" interval_deriv nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (k!1 skolem-const-decl "(LAMBDA (f): FORALL (t: Xt): f(t) /= 0)"
     interval_deriv nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nz_deriv_fun type-eq-decl nil derivatives "analysis/")
    (sq const-decl "nonneg_real" sq "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals 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_div_fun formula-decl nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (Diff_scald1 0
  (Diff_scald1-1 nil 3304432031
   ("" (skosimp :preds? t)
    (("" (expand "Diff?")
      (("" (lemma "derivable_div")
        (("" (inst -1 "LAMBDA(t):a!1" "k!1")
          (("1" (expand "/") (("1" (propax) nil nil)) nil)
           ("2" (assert) nil nil)
           ("3" (hide 2)
            (("3" (lemma "derivable_const")
              (("3" (expand "const_fun") (("3" (inst?) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (a!1 skolem-const-decl "real" interval_deriv nil)
    (k!1 skolem-const-decl "(LAMBDA (f): FORALL (t: Xt): f(t) /= 0)"
     interval_deriv nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nz_deriv_fun type-eq-decl nil derivatives "analysis/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable_const judgement-tcc nil derivatives "analysis/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (derivable_div judgement-tcc nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (D_scald1_TCC1 0
  (D_scald1_TCC1-1 nil 3304431707
   ("" (skosimp :preds? t) (("" (rewrite "Diff_scald1") nil nil)) nil)
   ((Diff_scald1 formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (D_scald1 0
  (D_scald1-1 nil 3304432324
   ("" (skosimp :preds? t)
    (("" (expand* "Diff?" "D")
      (("" (lemma "deriv_scaldiv_fun")
        (("" (inst -1 "a!1" "k!1")
          (("1" (expand "/")
            (("1" (expand "-")
              (("1" (expand "*")
                (("1" (expand "sq") (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((D const-decl "[Xt -> real]" interval_deriv nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (k!1 skolem-const-decl "(LAMBDA (f): FORALL (t: Xt): f(t) /= 0)"
     interval_deriv nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nz_deriv_fun type-eq-decl nil derivatives "analysis/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals 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/")
    (deriv_scaldiv_fun formula-decl nil derivatives "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (Diff_scald2 0
  (Diff_scald2-1 nil 3304432497
   ("" (skosimp)
    (("" (lemma "Diff_scal1")
      (("" (inst -1 "1/b!1" "f!1") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((Diff_scal1 formula-decl nil interval_deriv nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil))
   shostak))
 (D_scald2_TCC1 0
  (D_scald2_TCC1-1 nil 3304432644
   ("" (skosimp) (("" (rewrite "Diff_scald2") nil nil)) nil)
   ((Diff_scald2 formula-decl nil interval_deriv 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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_scald2 0
  (D_scald2-1 nil 3304432554
   ("" (skosimp)
    (("" (lemma "D_scal1")
      (("" (inst -1 "1/b!1" "f!1") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((D_scal1 formula-decl nil interval_deriv nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil))
   shostak))
 (Diff_sin 0
  (Diff_sin-2 nil 3425718979
   ("" (expand "Diff?")
    (("" (lemma "sin_derivable_fun")
      (("" (lemma "IMP_derivatives_TCC1")
        (("" (lemma "IMP_derivatives_TCC2")
          (("" (lemma "restrict2_derivable[Xt,real]")
            (("1" (hide -2 -3)
              (("1" (inst -1 "sin")
                (("1" (expand "restrict2") (("1" (propax) nil nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but 1)
              (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
             ("3" (hide-all-but 1)
              (("3" (assert)
                (("3" (expand "not_one_element?")
                  (("3" (skeep)
                    (("3" (inst + "x+1") (("3" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("4" (propax) nil nil)
             ("5" (lemma "deriv_domain_real") (("5" (propax) nil nil))
              nil)
             ("6" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sin_derivable_fun formula-decl nil sincos "trig_fnd/")
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (IMP_derivatives_TCC1 assuming-tcc nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/"))
   nil)
  (Diff_sin-1 nil 3304438429
   ("" (expand "Diff?")
    (("" (lemma "sin_derivable2")
      (("" (lemma "IMP_derivatives_TCC1")
        (("" (lemma "IMP_derivatives_TCC2")
          (("" (lemma "restrict2_derivable[Xt,real]")
            (("1" (hide -2 -3)
              (("1" (inst -1 "sin")
                (("1" (expand "restrict2") (("1" (propax) nil nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but 1)
              (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
             ("3" (hide-all-but 1)
              (("3" (skeep)
                (("3" (inst 1 "x+1") (("3" (assert) nil nil)) nil))
                nil))
              nil)
             ("4" (propax) nil nil) ("5" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
    (Interval type-eq-decl nil interval nil))
   shostak))
 (D_sin_TCC1 0
  (D_sin_TCC1-1 nil 3304438388 ("" (rewrite "Diff_sin") nil nil)
   ((Diff_sin formula-decl nil interval_deriv nil)) shostak))
 (D_sin 1
  (D_sin-1 nil 3350430186
   ("" (expand "D")
    (("" (lemma "deriv_exp_fun")
      (("" (lemma "IMP_derivatives_TCC1")
        (("" (lemma "IMP_derivatives_TCC2")
          (("" (lemma "restrict2_deriv[Xt,real]")
            (("1" (hide -2 -3)
              (("1" (decompose-equality 1)
                (("1" (inst -1 "x!1" "exp")
                  (("1" (expand "restrict2")
                    (("1" (replaces -2) (("1" (assert) nil)))))))
                 ("2" (lemma "Diff_exp")
                  (("2" (expand "Diff?") (("2" (propax) nil)))))))))
             ("2" (hide-all-but 1)
              (("2" (skeep) (("2" (inst 1 "x") nil)))))
             ("3" (hide-all-but 1)
              (("3" (skeep)
                (("3" (inst 1 "x+1") (("3" (assert) nil)))))))
             ("4" (propax) nil) ("5" (propax) nil))))))))))
    nil)
   nil nil)
  (D_sin-2 nil 3304438984
   ("" (expand "D")
    (("" (lemma "deriv_sin_fun")
      (("" (lemma "IMP_derivatives_TCC1")
        (("" (lemma "IMP_derivatives_TCC2")
          (("" (lemma "restrict2_deriv[Xt,real]")
            (("1" (hide -2 -3)
              (("1" (decompose-equality 1)
                (("1" (inst -1 "x!1" "sin")
                  (("1" (expand "restrict2")
                    (("1" (replaces -2) (("1" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (lemma "Diff_sin")
                  (("2" (expand "Diff?") (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but 1)
              (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
             ("3" (expand "not_one_element?")
              (("3" (skosimp*)
                (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil))
                nil))
              nil)
             ("4" (propax) nil nil)
             ("5" (lemma "deriv_domain_real") (("5" (propax) nil nil))
              nil)
             ("6" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_sin_fun formula-decl nil sincos "trig_fnd/")
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (Diff_sin formula-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (IMP_derivatives_TCC1 assuming-tcc nil interval_deriv nil)
    (D const-decl "[Xt -> real]" interval_deriv nil))
   nil))
 (Diff_cos 0
  (Diff_cos-2 nil 3425719011
   ("" (expand "Diff?")
    (("" (lemma "cos_derivable_fun")
      (("" (lemma "IMP_derivatives_TCC1")
        (("" (lemma "IMP_derivatives_TCC2")
          (("" (lemma "restrict2_derivable[Xt,real]")
            (("1" (hide -2 -3)
              (("1" (inst -1 "cos")
                (("1" (expand "restrict2") (("1" (propax) nil nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but 1)
              (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
             ("3" (hide-all-but 1)
              (("3" (assert)
                (("3" (expand "not_one_element?")
                  (("3" (skosimp*)
                    (("3" (inst + "x!1+1") (("3" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("4" (propax) nil nil)
             ("5" (lemma "deriv_domain_real") (("5" (propax) nil nil))
              nil)
             ("6" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cos_derivable_fun formula-decl nil sincos "trig_fnd/")
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (IMP_derivatives_TCC1 assuming-tcc nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/"))
   nil)
  (Diff_cos-1 nil 3304438688
   ("" (expand "Diff?")
    (("" (lemma "cos_derivable2")
      (("" (lemma "IMP_derivatives_TCC1")
        (("" (lemma "IMP_derivatives_TCC2")
          (("" (lemma "restrict2_derivable[Xt,real]")
            (("1" (hide -2 -3)
              (("1" (inst -1 "cos")
                (("1" (expand "restrict2") (("1" (propax) nil nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but 1)
              (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
             ("3" (hide-all-but 1)
              (("3" (skeep)
                (("3" (inst 1 "x+1") (("3" (assert) nil nil)) nil))
                nil))
              nil)
             ("4" (propax) nil nil) ("5" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
    (Interval type-eq-decl nil interval nil))
   nil))
 (D_cos_TCC1 0
  (D_cos_TCC1-1 nil 3304438400 ("" (rewrite "Diff_cos") nil nil)
   ((Diff_cos formula-decl nil interval_deriv nil)) shostak))
 (D_cos 0
  (D_cos-3 "" 3555948645
   ("" (expand "D")
    (("" (lemma "deriv_cos_fun")
      (("" (lemma "restrict2_deriv[Xt,real]")
        (("1" (decompose-equality 1)
          (("1" (inst -1 "x!1" "cos")
            (("1" (expand "restrict2")
              (("1" (replaces -2)
                (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil))
              nil))
            nil)
           ("2" (lemma "Diff_cos")
            (("2" (expand "Diff?") (("2" (propax) nil nil)) nil)) nil))
          nil)
         ("2" (hide-all-but 1)
          (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
         ("3" (hide-all-but 1)
          (("3" (assert)
            (("3" (expand "not_one_element?")
              (("3" (skosimp*)
                (("3" (typepred "x!1")
                  (("3" (typepred "X")
                    (("3" (expand "StrictInterval?")
                      (("3" (inst-cp + "lb(X)")
                        (("1" (inst-cp + "ub(X)")
                          (("1" (flatten) (("1" (assert) nil nil)) nil)
                           ("2" (grind) nil nil))
                          nil)
                         ("2" (grind) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("4" (lemma "deriv_domain_Xt") (("4" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((deriv_cos_fun formula-decl nil sincos "trig_fnd/")
    (deriv_domain_Xt formula-decl nil interval_deriv nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (minus_real_is_real application-judgement "real" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (Diff? const-decl "bool" interval_deriv nil)
    (Diff_cos formula-decl nil interval_deriv nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (D const-decl "[Xt -> real]" interval_deriv nil))
   shostak)
  (D_cos-2 nil 3545779380
   ("" (expand "D")
    (("" (lemma "deriv_cos_fun")
      (("" (lemma "restrict2_deriv[Xt,real]")
        (("1" (decompose-equality 1)
          (("1" (inst -1 "x!1" "cos")
            (("1" (expand "restrict2")
              (("1" (replaces -2)
                (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil))
              nil))
            nil)
           ("2" (lemma "Diff_cos")
            (("2" (expand "Diff?") (("2" (propax) nil nil)) nil)) nil))
          nil)
         ("2" (hide-all-but 1)
          (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
         ("3" (hide-all-but 1)
          (("3" (assert)
            (("3" (expand "not_one_element?")
              (("3" (skosimp*)
                (("3" (typepred "x!1")
                  (("3" (typepred "X")
                    (("3" (inst-cp + "lb(X)")
                      (("1" (inst-cp + "ub(X)")
                        (("1" (flatten)
                          (("1" (assert) (("1" (grind) nil nil)) nil))
                          nil)
                         ("2" (assert) (("2" (grind) nil nil)) nil))
                        nil)
                       ("2" (assert) (("2" (grind) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("4" (lemma "deriv_domain_Xt") (("4" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (deriv_cos_fun formula-decl nil sincos "trig_fnd/"))
   nil)
  (D_cos-1 nil 3304438720
   ("" (expand "D")
    (("" (lemma "deriv_cos_fun")
      (("" (lemma "restrict2_deriv[Xt,real]")
        (("1" (decompose-equality 1)
          (("1" (inst -1 "x!1" "cos")
            (("1" (expand "restrict2")
              (("1" (replaces -2)
                (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil))
              nil))
            nil)
           ("2" (lemma "Diff_cos")
            (("2" (expand "Diff?") (("2" (propax) nil nil)) nil)) nil))
          nil)
         ("2" (hide-all-but 1)
          (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
         ("3" (hide-all-but 1)
          (("3" (assert)
            (("3" (expand "not_one_element?")
              (("3" (skosimp*)
                (("3" (typepred "x!1")
                  (("3" (expand "##")
                    (("3" (typepred "X")
                      (("3" (expand "StrictlyProper?")
                        (("3" (inst-cp + "lb(X)")
                          (("1" (inst-cp + "ub(X)")
                            (("1" (flatten) (("1" (assert) nil nil))
                              nil)
                             ("2" (expand "##")
                              (("2" (assert) nil nil)) nil))
                            nil)
                           ("2" (expand "##") (("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("4" (lemma "deriv_domain_Xt") (("4" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((deriv_cos_fun formula-decl nil sincos "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
    (Interval type-eq-decl nil interval nil))
   nil))
 (Diff_tan_TCC1 0
  (Diff_tan_TCC1-1 nil 3304442382 ("" (subtype-tcc) nil nil) nil
   shostak))
 (Diff_tan_TCC2 0
  (Diff_tan_TCC2-1 nil 3393001518
   ("" (skeep)
    (("" (skosimp)
      (("" (use "Tan_pi2_def")
        (("" (typepred "t!1")
          (("" (expand "##") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pi_lb_pos application-judgement "posreal" atan_approx "trig_fnd/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (|##| const-decl "bool" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Tan_pi2_def formula-decl nil interval_trig nil))
   nil))
 (Diff_tan 0
  (Diff_tan-1 nil 3304442448
   ("" (skeep)
    (("" (expand "tan")
      (("" (rewrite "Diff_div")
        (("1" (split)
          (("1" (hide 2) (("1" (rewrite "Diff_cos") nil nil)) nil)
           ("2" (hide 2)
            (("2" (skeep :preds? t)
              (("2" (lemma "Tan_pi2_def")
                (("2" (inst -1 "X" "5+n" "t_1")
                  (("2" (expand "Tan?") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (rewrite "Diff_sin") nil nil))
        nil))
      nil))
    nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (tan const-decl "real" sincos_def "trig_fnd/")
    (Diff_sin formula-decl nil interval_deriv nil)
    (Diff_cos formula-decl nil interval_deriv nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (Tan? const-decl "bool" sincos_def "trig_fnd/")
    (Tan_pi2_def formula-decl nil interval_trig nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (pi_lb_pos application-judgement "posreal" atan_approx "trig_fnd/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (Diff? const-decl "bool" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval 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)
    (Diff_div formula-decl nil interval_deriv nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
 (D_tan_TCC1 0
  (D_tan_TCC1-1 nil 3304442394
   ("" (skeep)
    (("" (lemma "Diff_tan") (("" (inst?) (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((Diff_tan formula-decl nil interval_deriv nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (pi_lb_pos application-judgement "posreal" atan_approx "trig_fnd/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (D_tan_TCC2 0
  (D_tan_TCC2-1 nil 3304442404
   ("" (skeep)
    (("" (skeep :preds? t)
      (("" (lemma "Tan_pi2_def")
        (("" (inst -1 "X" _ "t")
          (("" (inst?)
            (("" (assert)
              (("" (expand "Tan?")
                (("" (rewrite "sq_eq_0")
                  (("" (expand "##") (("" (flatten) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv 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)
    (|##| const-decl "bool" interval nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi_lb_pos application-judgement "posreal" atan_approx "trig_fnd/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (sq_eq_0 formula-decl nil sq "reals/")
    (Tan? const-decl "bool" sincos_def "trig_fnd/")
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Tan_pi2_def formula-decl nil interval_trig nil))
   shostak))
 (D_tan 0
  (D_tan-1 nil 3304442607
   ("" (skeep)
    (("" (expand "tan")
      (("" (rewrite "D_div")
        (("1" (rewrite "D_sin")
          (("1" (rewrite "D_cos")
            (("1" (beta)
              (("1" (decompose-equality 1)
                (("1" (lemma "sin2_cos2")
                  (("1" (inst -1 "x!1")
                    (("1" (expand "sq") (("1" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (skeep :preds? t)
                  (("2" (lemma "Tan_pi2_def")
                    (("2" (inst -1 "X" _ "t_1")
                      (("2" (inst?)
                        (("2" (expand "Tan?")
                          (("2" (rewrite "sq_eq_0")
                            (("2" (expand "##")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (split)
            (("1" (rewrite "Diff_cos") nil nil)
             ("2" (skeep :preds? t)
              (("2" (lemma "Tan_pi2_def")
                (("2" (inst -1 "X" _ "t_1")
                  (("2" (inst?)
                    (("2" (expand "Tan?")
                      (("2" (expand "##") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (hide 2) (("3" (rewrite "Diff_sin") nil nil)) nil))
        nil))
      nil))
    nil)
   ((tan const-decl "real" sincos_def "trig_fnd/")
    (Diff_sin formula-decl nil interval_deriv nil)
    (Diff_cos formula-decl nil interval_deriv nil)
    (D_sin formula-decl nil interval_deriv nil)
    (Tan? const-decl "bool" sincos_def "trig_fnd/")
    (sq_eq_0 formula-decl nil sq "reals/")
    (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)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Tan_pi2_def formula-decl nil interval_trig nil)
    (sin2_cos2 formula-decl nil trig_basic "trig_fnd/")
    (real_plus_real_is_real application-judgement "real" reals 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 -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (D_cos formula-decl nil interval_deriv nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (pi_lb_pos application-judgement "posreal" atan_approx "trig_fnd/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (/= const-decl "boolean" notequal nil)
    (sin const-decl "real" sincos_def "trig_fnd/")
    (Diff? const-decl "bool" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval 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)
    (D_div formula-decl nil interval_deriv nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
 (Diff_atan 0
  (Diff_atan-1 nil 3393000322
   ("" (expand "Diff?")
    (("" (lemma "deriv_atan_fun")
      (("" (flatten)
        (("" (hide -2)
          (("" (lemma "IMP_derivatives_TCC1")
            (("" (lemma "IMP_derivatives_TCC2")
              (("" (lemma "restrict2_derivable[Xt,real]")
                (("1" (hide -2 -3)
                  (("1" (inst -1 "atan")
                    (("1" (expand "restrict2") (("1" (propax) nil nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but 1)
                  (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
                 ("3" (hide-all-but 1)
                  (("3" (assert)
                    (("3" (expand "not_one_element?")
                      (("3" (skeep)
                        (("3" (inst 1 "x+1") (("3" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("4" (propax) nil nil)
                 ("5" (lemma "deriv_domain_real")
                  (("5" (propax) nil nil)) nil)
                 ("6" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_atan_fun formula-decl nil atan "trig_fnd/")
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals 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)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (pi const-decl "posreal" atan "trig_fnd/")
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig_fnd/")
    (atan const-decl "real_abs_lt_pi2" atan "trig_fnd/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (IMP_derivatives_TCC1 assuming-tcc nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_atan_TCC1 0
  (D_atan_TCC1-1 nil 3393000230 ("" (rewrite "Diff_atan") nil nil)
   ((Diff_atan formula-decl nil interval_deriv nil)) nil))
 (D_atan 0
  (D_atan-1 nil 3393000770
   ("" (expand "D")
    (("" (lemma "deriv_atan_fun")
      (("" (flatten)
        (("" (lemma "IMP_derivatives_TCC1")
          (("" (lemma "IMP_derivatives_TCC2")
            (("" (lemma "restrict2_deriv[Xt,real]")
              (("1" (hide -2 -3)
                (("1" (decompose-equality 1)
                  (("1" (inst -1 "x!1" "atan")
                    (("1" (expand "restrict2")
                      (("1" (expand "sq")
                        (("1" (replaces -3) (("1" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (lemma "Diff_atan")
                    (("2" (expand "Diff?") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide-all-but 1)
                (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
               ("3" (hide-all-but 1)
                (("3" (assert)
                  (("3" (expand "not_one_element?")
                    (("3" (skeep)
                      (("3" (inst + "x+1") (("3" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("4" (propax) nil nil)
               ("5" (lemma "deriv_domain_real")
                (("5" (propax) nil nil)) nil)
               ("6" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_atan_fun formula-decl nil atan "trig_fnd/")
    (IMP_derivatives_TCC1 assuming-tcc nil interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval 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)
    (restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (atan const-decl "real_abs_lt_pi2" atan "trig_fnd/")
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig_fnd/")
    (pi const-decl "posreal" atan "trig_fnd/")
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (Diff? const-decl "bool" interval_deriv nil)
    (Diff_atan formula-decl nil interval_deriv nil)
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (D const-decl "[Xt -> real]" interval_deriv nil))
   shostak))
 (Diff_sqrt_TCC1 0
  (Diff_sqrt_TCC1-1 nil 3304436172
   ("" (flatten) (("" (grind) nil nil)) nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Gt const-decl "bool" interval 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (Diff_sqrt 0
  (Diff_sqrt-1 nil 3304435882
   ("" (expand "Diff?")
    (("" (flatten)
      (("" (lemma "sqrt_derivable_fun")
        (("" (lemma "IMP_derivatives_TCC2")
          (("" (lemma "restrict2_derivable[Xt,posreal]")
            (("1" (inst -1 "sqrt")
              (("1" (expand "restrict2")
                (("1" (expand "restrict") (("1" (propax) nil nil))
                  nil))
                nil))
              nil)
             ("2" (skeep :preds? t)
              (("2" (inst 1 "x")
                (("2" (hide-all-but (-1 -4 1)) (("2" (grind) nil nil))
                  nil))
                nil))
              nil)
             ("3" (propax) nil nil)
             ("4" (hide-all-but 1)
              (("4" (lemma "deriv_domain_Xt") (("4" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (deriv_domain_Xt formula-decl nil interval_deriv nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Gt const-decl "bool" interval nil)
    (x skolem-const-decl "Xt" interval_deriv nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (restrict const-decl "R" restrict nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv 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)
    (sqrt_derivable_fun formula-decl nil sqrt_derivative "analysis/")
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_sqrt_TCC1 0
  (D_sqrt_TCC1-1 nil 3304436226
   ("" (flatten) (("" (rewrite "Diff_sqrt") nil nil)) nil)
   ((Diff_sqrt formula-decl nil interval_deriv nil)) shostak))
 (D_sqrt_TCC2 0
  (D_sqrt_TCC2-1 nil 3304436241
   ("" (flatten) (("" (skeep :preds? t) (("" (grind) nil nil)) nil))
    nil)
   ((Gt const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   shostak))
 (D_sqrt 0
  (D_sqrt-1 nil 3304437850
   ("" (expand "D")
    (("" (flatten)
      (("" (lemma "IMP_derivatives_TCC2")
        (("" (lemma "deriv_sqrt")
          (("" (flatten)
            (("" (lemma "restrict2_deriv[Xt,posreal]")
              (("1" (decompose-equality 1)
                (("1" (inst -1 "x!1" "sqrt")
                  (("1" (expand "restrict2")
                    (("1" (expand "restrict")
                      (("1" (replaces -1 :dir rl)
                        (("1" (replaces -2)
                          (("1" (beta) (("1" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skeep :preds? t)
                  (("2" (hide-all-but (-1 -2 -7))
                    (("2" (grind) nil nil)) nil))
                  nil)
                 ("3" (lemma "Diff_sqrt")
                  (("3" (expand "Diff?") (("3" (propax) nil nil)) nil))
                  nil)
                 ("4" (skeep :preds? t)
                  (("4" (hide-all-but (-1 -6 1))
                    (("4" (grind) nil nil)) nil))
                  nil))
                nil)
               ("2" (skeep :preds? t)
                (("2" (inst 1 "x")
                  (("2" (hide-all-but (-1 -5 1))
                    (("2" (grind) nil nil)) nil))
                  nil))
                nil)
               ("3" (propax) nil nil)
               ("4" (lemma "deriv_domain_Xt") (("4" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_sqrt formula-decl nil sqrt_derivative "analysis/")
    (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)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval 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)
    (restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Diff_sqrt formula-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Gt const-decl "bool" interval nil)
    (restrict const-decl "R" restrict nil)
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (/= const-decl "boolean" notequal nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (x skolem-const-decl "Xt" interval_deriv nil)
    (deriv_domain_Xt formula-decl nil interval_deriv nil)
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (D const-decl "[Xt -> real]" interval_deriv nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   shostak))
 (Diff_exp 0
  (Diff_exp-2 nil 3350429197
   ("" (expand "Diff?")
    (("" (lemma "IMP_derivatives_TCC1")
      (("" (lemma "IMP_derivatives_TCC2")
        (("" (lemma "restrict2_derivable[Xt,real]")
          (("1" (hide -2 -3)
            (("1" (inst -1 "exp")
              (("1" (expand "restrict2") (("1" (propax) nil nil)) nil)
               ("2" (lemma "exp_deriv") (("2" (assert) nil nil)) nil))
              nil))
            nil)
           ("2" (hide-all-but 1)
            (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
           ("3" (hide-all-but 1)
            (("3" (assert)
              (("3" (expand "not_one_element?")
                (("3" (skeep)
                  (("3" (inst 1 "x+1") (("3" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("4" (propax) nil nil)
           ("5" (lemma "deriv_domain_real") (("5" (propax) nil nil))
            nil)
           ("6" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((IMP_derivatives_TCC1 assuming-tcc nil interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval 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)
    (restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (>= 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)
    (ln const-decl "real" ln_exp "lnexp_fnd/")
    (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (exp_deriv formula-decl nil ln_exp "lnexp_fnd/")
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   nil)
  (Diff_exp-1 nil 3350429081
   ("" (expand "Diff?")
    (("" (lemma "sin_derivable2")
      (("" (lemma "IMP_derivatives_TCC1")
        (("" (lemma "IMP_derivatives_TCC2")
          (("" (lemma "restrict2_derivable[Xt,real]")
            (("1" (hide -2 -3)
              (("1" (inst -1 "sin")
                (("1" (expand "restrict2") (("1" (propax) nil)))))))
             ("2" (hide-all-but 1)
              (("2" (skeep) (("2" (inst 1 "x") nil)))))
             ("3" (hide-all-but 1)
              (("3" (skeep)
                (("3" (inst 1 "x+1") (("3" (assert) nil)))))))
             ("4" (propax) nil) ("5" (propax) nil))))))))))
    nil)
   nil nil))
 (D_exp_TCC1 0
  (D_exp_TCC1-1 nil 3350428120 ("" (rewrite "Diff_exp") nil nil)
   ((Diff_exp formula-decl nil interval_deriv nil)) nil))
 (D_exp 0
  (D_exp-1 nil 3350430351
   ("" (expand "D")
    (("" (lemma "exp_deriv")
      (("" (lemma "IMP_derivatives_TCC1")
        (("" (lemma "IMP_derivatives_TCC2")
          (("" (lemma "restrict2_deriv[Xt,real]")
            (("1" (hide -2 -3)
              (("1" (decompose-equality 1)
                (("1" (flatten)
                  (("1" (inst -1 "x!1" "exp")
                    (("1" (expand "restrict2")
                      (("1" (replaces -1 :dir rl)
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (lemma "Diff_exp")
                  (("2" (expand "Diff?") (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)
             ("3" (assert)
              (("3" (hide-all-but 1)
                (("3" (expand "not_one_element?")
                  (("3" (skeep)
                    (("3" (inst + "x+1") (("3" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("4" (propax) nil nil)
             ("5" (lemma "deriv_domain_real") (("5" (propax) nil nil))
              nil)
             ("6" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exp_deriv formula-decl nil ln_exp "lnexp_fnd/")
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (Diff_exp formula-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (>= 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)
    (ln const-decl "real" ln_exp "lnexp_fnd/")
    (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
    (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)
    (Interval type-eq-decl nil interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (IMP_derivatives_TCC1 assuming-tcc nil interval_deriv nil)
    (D const-decl "[Xt -> real]" interval_deriv nil))
   nil))
 (Diff_ln_TCC1 0
  (Diff_ln_TCC1-1 nil 3350428120 ("" (subtype-tcc) nil nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Gt const-decl "bool" interval 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (Diff_ln 0
  (Diff_ln-4 "Fixed, and shorter proof w.r.t. Diff_ln-3." 3555950105
   ("" (expand "Diff?")
    (("" (lemma "IMP_derivatives_TCC1")
      (("" (lemma "IMP_derivatives_TCC2")
        (("" (lemma "restrict2_derivable[Xt,posreal]")
          (("1" (hide -2 -3)
            (("1" (inst -1 "ln")
              (("1" (expand "restrict2") (("1" (flatten) nil nil)) nil)
               ("2" (lemma "ln_derivable") (("2" (assert) nil nil))
                nil))
              nil))
            nil)
           ("2" (flatten)
            (("2" (skeep)
              (("2" (inst 1 "x")
                (("2" (typepred "x")
                  (("2" (hide-all-but (-1 -4 1))
                    (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (propax) nil nil) ("4" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((IMP_derivatives_TCC1 assuming-tcc nil interval_deriv 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)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval 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)
    (restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (ln const-decl "real" ln_exp "lnexp_fnd/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (ln_derivable formula-decl nil ln_exp "lnexp_fnd/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Gt const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (x skolem-const-decl "Xt" interval_deriv nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak)
  (Diff_ln-3 nil 3350429811
   ("" (expand "Diff?")
    (("" (lemma "IMP_derivatives_TCC1")
      (("" (lemma "IMP_derivatives_TCC2")
        (("" (lemma "restrict2_derivable[Xt,posreal]")
          (("1" (hide -2 -3)
            (("1" (inst -1 "ln")
              (("1" (expand "restrict2") (("1" (flatten) nil nil)) nil)
               ("2" (lemma "ln_derivable") (("2" (assert) nil nil))
                nil))
              nil))
            nil)
           ("2" (flatten)
            (("2" (skeep)
              (("2" (inst 1 "x")
                (("2" (typepred "x")
                  (("2" (hide-all-but (-1 -4 1))
                    (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (hide-all-but 1)
            (("3" (expand "not_one_element?")
              (("3" (skeep)
                (("3" (inst + "x+1") (("3" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("4" (propax) nil nil)
           ("5" (flatten)
            (("5" (hide-all-but 1)
              (("5" (lemma "deriv_domain_posreal")
                (("5" (propax) nil nil)) nil))
              nil))
            nil)
           ("6" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (restrict2_derivable formula-decl nil restrict2_deriv "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (ln const-decl "real" ln_exp "lnexp_fnd/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (ln_derivable formula-decl nil ln_exp "lnexp_fnd/")
    (Gt const-decl "bool" interval nil))
   nil)
  (Diff_ln-2 nil 3350429454
   ("" (expand "Diff?")
    (("" (lemma "IMP_derivatives_TCC1")
      (("" (lemma "IMP_derivatives_TCC2")
        (("" (lemma "restrict2_derivable[Xt,real]")
          (("1" (hide -2 -3)
            (("1" (inst -1 "ln")
              (("1" (expand "restrict2") (("1" (flatten) nil nil)) nil)
               ("2" (postpone) nil nil))
              nil))
            nil)
           ("2" (hide-all-but 1)
            (("2" (skeep) (("2" (inst 1 "x") nil nil)) nil)) nil)
           ("3" (hide-all-but 1)
            (("3" (skeep)
              (("3" (inst 1 "x+1") (("3" (assert) nil nil)) nil)) nil))
            nil)
           ("4" (propax) nil nil) ("5" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   nil nil)
  (Diff_ln-1 nil 3350429435
   ("" (expand "Diff?")
    (("" (lemma "IMP_derivatives_TCC1")
      (("" (lemma "IMP_derivatives_TCC2")
        (("" (lemma "restrict2_derivable[Xt,real]")
          (("1" (hide -2 -3)
            (("1" (inst -1 "exp")
              (("1" (expand "restrict2") (("1" (propax) nil)))
               ("2" (postpone) nil)))))
           ("2" (hide-all-but 1)
            (("2" (skeep) (("2" (inst 1 "x") nil)))))
           ("3" (hide-all-but 1)
            (("3" (skeep)
              (("3" (inst 1 "x+1") (("3" (assert) nil)))))))
           ("4" (propax) nil) ("5" (propax) nil))))))))
    nil)
   nil nil))
 (D_ln_TCC1 0
  (D_ln_TCC1-1 nil 3350428120
   ("" (flatten) (("" (rewrite "Diff_ln") nil nil)) nil)
   ((Diff_ln formula-decl nil interval_deriv nil)) nil))
 (D_ln_TCC2 0
  (D_ln_TCC2-1 nil 3350428120 ("" (subtype-tcc) nil nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil)
    (Gt const-decl "bool" interval 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (D_ln 0
  (D_ln-2 nil 3350430791
   ("" (expand "D")
    (("" (flatten)
      (("" (lemma "IMP_derivatives_TCC2")
        (("" (lemma "ln_derivable")
          (("" (flatten)
            (("" (lemma "restrict2_deriv[Xt,posreal]")
              (("1" (decompose-equality 1)
                (("1" (inst -1 "x!1" "ln")
                  (("1" (expand "restrict2")
                    (("1" (replaces -1 :dir rl)
                      (("1" (replaces -2)
                        (("1" (beta) (("1" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (skeep :preds? t)
                  (("2" (hide-all-but (-1 -2 -7))
                    (("2" (grind) nil nil)) nil))
                  nil)
                 ("3" (lemma "Diff_ln")
                  (("3" (expand "Diff?") (("3" (propax) nil nil)) nil))
                  nil)
                 ("4" (skeep :preds? t)
                  (("4" (hide-all-but (-1 -6 1))
                    (("4" (grind) nil nil)) nil))
                  nil))
                nil)
               ("2" (skeep :preds? t)
                (("2" (inst 1 "x")
                  (("2" (hide-all-but (-1 -5 1))
                    (("2" (grind) nil nil)) nil))
                  nil))
                nil)
               ("3" (propax) nil nil)
               ("4" (lemma "deriv_domain_Xt") (("4" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((ln_derivable formula-decl nil ln_exp "lnexp_fnd/")
    (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)
    (Xt type-eq-decl nil interval_deriv nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (StrictInterval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Interval type-eq-decl nil interval 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)
    (restrict2_deriv formula-decl nil restrict2_deriv "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Diff_ln formula-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Gt const-decl "bool" interval nil)
    (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (/= const-decl "boolean" notequal nil)
    (ln const-decl "real" ln_exp "lnexp_fnd/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (x skolem-const-decl "Xt" interval_deriv nil)
    (deriv_domain_Xt formula-decl nil interval_deriv nil)
    (IMP_derivatives_TCC2 assuming-tcc nil interval_deriv nil)
    (D const-decl "[Xt -> real]" interval_deriv nil))
   nil)
  (D_ln-1 nil 3350430749
   ("" (expand "D")
    (("" (flatten)
      (("" (lemma "IMP_derivatives_TCC2")
        (("" (lemma "deriv_sqrt")
          (("" (flatten)
            (("" (lemma "restrict2_deriv[Xt,posreal]")
              (("1" (decompose-equality 1)
                (("1" (inst -1 "x!1" "sqrt")
                  (("1" (expand "restrict2")
                    (("1" (expand "restrict")
                      (("1" (replaces -1 :dir rl)
                        (("1" (replaces -2)
                          (("1" (beta) (("1" (propax) nil)))))))))))))
                 ("2" (skeep :preds? t)
                  (("2" (hide-all-but (-1 -2 -7))
                    (("2" (grind) nil)))))
                 ("3" (lemma "Diff_sqrt")
                  (("3" (expand "Diff?") (("3" (propax) nil)))))
                 ("4" (skeep :preds? t)
                  (("4" (hide-all-but (-1 -6 1))
                    (("4" (grind) nil)))))))
               ("2" (skeep :preds? t)
                (("2" (inst 1 "x")
                  (("2" (hide-all-but (-1 -5 1))
                    (("2" (grind) nil)))))))
               ("3" (hide-all-but 1)
                (("3" (skeep)
                  (("3" (inst 1 "x+1") (("3" (assert) nil)))))))
               ("4" (propax) nil)
               ("5" (hide-all-but 1) (("5" (grind) nil)))
               ("6" (hide-all-but 1) (("6" (grind) nil))))))))))))))
    nil)
   nil nil))
 (Diff_I 0
  (Diff_I-1 nil 3304781158
   ("" (expand "id") (("" (propax) nil nil)) nil)
   ((id const-decl "(bijective?[T, T])" identity nil)) shostak))
 (D_I_TCC1 0
  (D_I_TCC1-1 nil 3304781247
   ("" (skosimp :preds? t)
    (("" (expand "id")
      (("" (case "f!1 = LAMBDA(t):f!1(t)")
        (("1" (assert) nil nil) ("2" (decompose-equality) nil nil))
        nil))
      nil))
    nil)
   ((id const-decl "(bijective?[T, T])" identity nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_I_TCC2 0
  (D_I_TCC2-1 nil 3304781295
   ("" (skosimp :preds? t)
    (("" (case "f!1 = LAMBDA(t):f!1(t)")
      (("1" (assert) nil nil) ("2" (decompose-equality) nil nil)) nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities 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)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (X formal-const-decl "StrictInterval" interval_deriv nil)
    (Xt type-eq-decl nil interval_deriv nil)
    (Diff? const-decl "bool" interval_deriv nil))
   shostak))
 (D_I 0
  (D_I-1 nil 3304781168 ("" (expand "id") (("" (propax) nil nil)) nil)
   ((id const-decl "(bijective?[T, T])" identity nil)) shostak)))