Quelle interval_deriv.prf Sprache: Lisp

(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
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.