products/Sources/formale Sprachen/PVS/analysis_ax/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: top.pvs   Sprache: PVS

Original von: PVS©
(derivatives
 (IMP_derivatives_def_TCC1 0
  (IMP_derivatives_def_TCC1-1 nil 3601998467
   ("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)
   ((deriv_domain formula-decl nil derivatives nil)) nil))
 (IMP_derivatives_def_TCC2 0
  (IMP_derivatives_def_TCC2-1 nil 3601998467
   ("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
   ((not_one_element formula-decl nil derivatives nil)) nil))
 (deriv_TCC1 0
  (deriv_TCC1-1 nil 3253536989
   ("" (auto-rewrite "derivable")
    (("" (skosimp :preds? t)
      (("" (expand "derivable?" -1) (("" (inst?) nil 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)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil))
   nil))
 (derivable_cont_fun 0
  (derivable_cont_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (expand "continuous?")
      (("" (grind :defs nil :rewrites "derivable_continuous") nil nil))
      nil))
    nil)
   ((continuous? const-decl "bool" continuous_functions nil)
    (derivable_continuous formula-decl nil derivatives_def nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (sum_derivable_fun 0
  (sum_derivable_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (grind :defs nil :rewrites "sum_derivable") 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)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (sum_derivable formula-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (neg_derivable_fun 0
  (neg_derivable_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (grind :defs nil :rewrites "neg_derivable") 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)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (neg_derivable formula-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (diff_derivable_fun 0
  (diff_derivable_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (grind :defs nil :rewrites "diff_derivable") 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)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (diff_derivable formula-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (prod_derivable_fun 0
  (prod_derivable_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (grind :defs nil :rewrites "prod_derivable") 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)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (prod_derivable formula-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (scal_derivable_fun 0
  (scal_derivable_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (grind :defs nil :rewrites "scal_derivable") nil nil)) nil)
   ((T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (scal_derivable formula-decl nil derivatives_def nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (const_derivable_fun 0
  (const_derivable_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (skosimp*)
      (("" (lemma "const_derivable")
        (("" (expand "const_fun") (("" (inst?) nil nil)) nil)) nil))
      nil))
    nil)
   ((const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (const_derivable formula-decl nil derivatives_def nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (inv_derivable_fun 0
  (inv_derivable_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (grind :defs nil :rewrites "inv_derivable") 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)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (inv_derivable formula-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (div_derivable_fun 0
  (div_derivable_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (grind :defs nil :rewrites "div_derivable") 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)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (div_derivable formula-decl nil derivatives_def nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (identity_derivable_fun 0
  (identity_derivable_fun-1 nil 3253536989
   ("" (expand "derivable?")
    (("" (grind :defs nil :rewrites "identity_derivable") nil nil))
    nil)
   ((identity_derivable formula-decl nil derivatives_def nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (id_derivable_fun 0
  (id_derivable_fun-1 nil 3474728116
   ("" (lemma identity_derivable_fun)
    (("" (expand "I") (("" (propax) nil nil)) nil)) nil)
   ((I const-decl "(bijective?[T, T])" identity nil)
    (identity_derivable_fun formula-decl nil derivatives nil))
   nil))
 (derivable_cont 0
  (derivable_cont-1 nil 3253536989
   ("" (skolem!) (("" (rewrite "derivable_cont_fun") nil nil)) nil)
   ((derivable_cont_fun formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil))
   nil))
 (nz_derivable_cont 0
  (nz_derivable_cont-1 nil 3253536989
   ("" (skolem!) (("" (rewrite "derivable_cont_fun") nil nil)) nil)
   ((derivable_cont_fun formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (nz_deriv_fun type-eq-decl nil derivatives nil))
   nil))
 (derivable_sum 0
  (derivable_sum-1 nil 3253536989
   ("" (skolem!) (("" (rewrite "sum_derivable_fun") nil nil)) nil)
   ((sum_derivable_fun formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil))
   nil))
 (derivable_diff 0
  (derivable_diff-1 nil 3253536989
   ("" (skolem!) (("" (rewrite "diff_derivable_fun") nil nil)) nil)
   ((diff_derivable_fun formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil))
   nil))
 (derivable_prod 0
  (derivable_prod-1 nil 3253536989
   ("" (skolem!) (("" (rewrite "prod_derivable_fun") nil nil)) nil)
   ((prod_derivable_fun formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil))
   nil))
 (derivable_scal 0
  (derivable_scal-1 nil 3253536989
   ("" (skolem!) (("" (rewrite "scal_derivable_fun") nil nil)) nil)
   ((scal_derivable_fun formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil))
   nil))
 (derivable_neg 0
  (derivable_neg-1 nil 3253536989
   ("" (skolem!) (("" (rewrite "neg_derivable_fun") nil nil)) nil)
   ((neg_derivable_fun formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil))
   nil))
 (derivable_div 0
  (derivable_div-1 nil 3253536989
   ("" (skolem!) (("" (rewrite "div_derivable_fun") nil nil)) nil)
   ((div_derivable_fun formula-decl nil derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nz_deriv_fun type-eq-decl nil derivatives nil))
   nil))
 (derivable_inv 0
  (derivable_inv-1 nil 3253536989
   ("" (skolem!)
    (("" (case-replace "b!1 / gg!1 = b!1 * (1 / gg!1)")
      (("1" (rewrite "scal_derivable_fun")
        (("1" (rewrite "inv_derivable_fun") nil nil)) nil)
       ("2" (delete 2)
        (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (nz_deriv_fun type-eq-decl nil derivatives nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (inv_derivable_fun formula-decl nil derivatives nil)
    (scal_derivable_fun formula-decl nil derivatives nil)
    (real_div_nzreal_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))
   nil))
 (derivable_const 0
  (derivable_const-1 nil 3253536989
   ("" (skosimp*)
    (("" (expand "const_fun")
      (("" (rewrite "const_derivable_fun") nil nil)) nil))
    nil)
   ((const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (const_derivable_fun formula-decl nil derivatives nil))
   nil))
 (derivable_id 0
  (derivable_id-1 nil 3253536989
   ("" (lemma "identity_derivable_fun") (("" (propax) nil nil)) nil)
   ((identity_derivable_fun formula-decl nil derivatives nil)) nil))
 (deriv_sum_fun 0
  (deriv_sum_fun-1 nil 3253536989
   ("" (skolem-typepred)
    (("" (expand "derivable?")
      (("" (apply-extensionality :hide? t)
        (("" (expand "+" 1 2)
          (("" (expand "deriv")
            (("" (rewrite "deriv_sum")
              (("1" (inst?) nil nil) ("2" (inst? -2) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_sum formula-decl nil derivatives_def nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (derivable_sum application-judgement "deriv_fun" derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (deriv_neg_fun 0
  (deriv_neg_fun-1 nil 3253536989
   ("" (skolem-typepred)
    (("" (expand "derivable?")
      (("" (apply-extensionality :hide? t)
        (("" (expand "-" 1 2)
          (("" (expand "deriv")
            (("" (rewrite "deriv_neg") (("" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_neg formula-decl nil derivatives_def nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (derivable_neg application-judgement "deriv_fun" derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (deriv_diff_fun 0
  (deriv_diff_fun-1 nil 3253536989
   ("" (skolem-typepred)
    (("" (expand "derivable?")
      (("" (apply-extensionality :hide? t)
        (("" (expand "-" 1 2)
          (("" (expand "deriv")
            (("" (rewrite "deriv_diff")
              (("1" (inst?) nil nil) ("2" (inst? -2) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_diff formula-decl nil derivatives_def nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (derivable_diff application-judgement "deriv_fun" derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (deriv_prod_fun 0
  (deriv_prod_fun-1 nil 3253536989
   ("" (skolem-typepred)
    (("" (expand "derivable?")
      (("" (apply-extensionality :hide? t)
        (("" (expand "+" +)
          (("" (expand "*" 1 2)
            (("" (expand "*" 1 2)
              (("" (expand "deriv")
                (("" (rewrite "deriv_prod")
                  (("1" (inst?) nil nil) ("2" (inst? -2) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_prod formula-decl nil derivatives_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (derivable_prod application-judgement "deriv_fun" derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (deriv_scal_fun 0
  (deriv_scal_fun-1 nil 3253536989
   ("" (skolem-typepred)
    (("" (expand "derivable?")
      (("" (apply-extensionality :hide? t)
        (("" (expand "*" 1 2)
          (("" (expand "deriv")
            (("" (rewrite "deriv_scal") (("" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_scal formula-decl nil derivatives_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (derivable_scal application-judgement "deriv_fun" derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (deriv_inv_fun_TCC1 0
  (deriv_inv_fun_TCC1-1 nil 3253536989
   ("" (skosimp)
    (("" (expand "*")
      (("" (rewrite "zero_times3") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((* const-decl "[T -> real]" real_fun_ops "reals/")
    (nz_deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives 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)
    (zero_times3 formula-decl nil real_props nil))
   nil))
 (deriv_inv_fun 0
  (deriv_inv_fun-1 nil 3253536989
   ("" (skolem-typepred)
    (("" (expand "derivable?")
      (("" (apply-extensionality :hide? t)
        (("1" (expand "/" 1 2)
          (("1" (expand "-" +)
            (("1" (expand "*" +)
              (("1" (expand "deriv")
                (("1" (rewrite "deriv_inv") (("1" (inst?) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (delete -)
          (("2" (grind :rewrites "zero_times3") nil nil)) nil))
        nil))
      nil))
    nil)
   ((deriv_inv formula-decl nil derivatives_def nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (derivable_prod application-judgement "deriv_fun" derivatives nil)
    (derivable_inv application-judgement "deriv_fun" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (deriv const-decl "[T -> real]" derivatives 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/")
    (nz_deriv_fun type-eq-decl nil derivatives nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (derivable? const-decl "bool" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (deriv_scaldiv_fun 0
  (deriv_scaldiv_fun-1 nil 3253536989
   ("" (skolem!)
    (("" (case-replace "b!1 / gg!1 = b!1 * (1/gg!1)")
      (("1" (rewrite "deriv_scal_fun")
        (("1" (rewrite "deriv_inv_fun")
          (("1" (delete -)
            (("1" (apply-extensionality :hide? t)
              (("1" (expand "/")
                (("1" (expand "*")
                  (("1" (expand "-") (("1" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (assert)
          (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivable_inv application-judgement "deriv_fun" derivatives nil)
    (derivable_scal application-judgement "deriv_fun" derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (nz_deriv_fun type-eq-decl nil derivatives nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_inv_fun formula-decl nil derivatives nil)
    (derivable_prod application-judgement "deriv_fun" derivatives nil)
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv const-decl "[T -> real]" derivatives nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (deriv_scal_fun formula-decl nil derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil))
   nil))
 (deriv_div_fun 0
  (deriv_div_fun-1 nil 3253536989
   ("" (skolem-typepred)
    (("" (expand "derivable?")
      (("" (apply-extensionality :hide? t)
        (("1" (inst?)
          (("1" (inst?)
            (("1" (expand "/" 1 2)
              (("1" (expand "-" +)
                (("1" (expand "*")
                  (("1" (expand "deriv")
                    (("1" (rewrite "deriv_div") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (delete -)
          (("2" (grind :rewrites "zero_times3") nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (deriv_div formula-decl nil derivatives_def nil)
    (derivable_prod application-judgement "deriv_fun" derivatives nil)
    (derivable_div application-judgement "deriv_fun" derivatives nil)
    (deriv const-decl "[T -> real]" derivatives 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/")
    (nz_deriv_fun type-eq-decl nil derivatives nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (deriv_const_fun_TCC1 0
  (deriv_const_fun_TCC1-1 nil 3475585951
   ("" (skosimp*) (("" (rewrite "const_derivable_fun") nil nil)) nil)
   ((const_derivable_fun formula-decl nil derivatives 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))
   nil))
 (deriv_const_fun 0
  (deriv_const_fun-1 nil 3253536989
   ("" (skosimp*)
    (("" (expand "deriv" 1)
      (("" (assert)
        (("" (apply-extensionality 1 :hide? t)
          (("1" (lemma "deriv_const")
            (("1" (expand "const_fun") (("1" (inst?) nil nil)) nil))
            nil)
           ("2" (skosimp*)
            (("2" (lemma "const_derivable_fun")
              (("2" (expand "const_fun")
                (("2" (inst?)
                  (("2" (expand "derivable?" -1)
                    (("2" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv const-decl "[T -> real]" derivatives nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (deriv const-decl "real" derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (b!1 skolem-const-decl "real" derivatives nil)
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_const formula-decl nil derivatives_def nil)
    (const_derivable_fun formula-decl nil derivatives nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (deriv_const_func 0
  (deriv_const_func-1 nil 3475596664
   ("" (skosimp*)
    (("" (lemma "deriv_const_fun")
      (("" (expand "const_fun") (("" (inst?) nil nil)) nil)) nil))
    nil)
   ((deriv_const_fun formula-decl nil derivatives nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/"))
   shostak))
 (deriv_id_fun_TCC1 0
  (deriv_id_fun_TCC1-1 nil 3475576474
   ("" (lemma "id_derivable_fun") (("" (propax) nil nil)) nil)
   ((id_derivable_fun formula-decl nil derivatives nil)) nil))
 (deriv_id_fun 0
  (deriv_id_fun-1 nil 3253536989
   (""
    (auto-rewrite "I" "const_fun" "deriv_identity"
                  "identity_derivable")
    (("" (expand "deriv")
      (("" (apply-extensionality :hide? t)
        (("1" (lemma "deriv_identity")
          (("1" (inst?)
            (("1" (expand "I") (("1" (propax) nil nil)) nil)) nil))
          nil)
         ("2" (skosimp*)
          (("2" (lemma "id_derivable_fun")
            (("2" (expand "derivable?" -1) (("2" (inst?) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv const-decl "[T -> real]" derivatives nil)
    (derivable? const-decl "bool" derivatives nil)
    (id_derivable_fun formula-decl nil derivatives nil)
    (deriv_identity formula-decl nil derivatives_def nil)
    (I const-decl "(bijective?[T, T])" identity nil)
    (derivable? const-decl "bool" derivatives_def nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (deriv const-decl "real" derivatives_def nil)
    (T formal-subtype-decl nil derivatives nil)
    (T_pred const-decl "[real -> boolean]" derivatives 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))
 (deriv_I_fun 0
  (deriv_I_fun-1 nil 3475596599
   ("" (lemma deriv_id_fun)
    (("" (expand "I") (("" (propax) nil nil)) nil)) nil)
   ((I const-decl "(bijective?[T, T])" identity nil)
    (deriv_id_fun formula-decl nil derivatives nil))
   shostak))
 (deriv_linear_fun 0
  (deriv_linear_fun-1 nil 3320142862
   ("" (skosimp*)
    (("" (assert)
      (("" (lemma "const_derivable_fun[T]")
        (("" (expand "const_fun")
          (("" (inst - "b!1")
            (("" (lemma "id_derivable_fun")
              (("" (lemma "scal_derivable_fun[T]")
                (("" (inst - "m!1" "(LAMBDA x: x)")
                  (("" (assert)
                    (("" (expand "*" -1)
                      (("" (case "derivable?(LAMBDA x: m!1 * x + b!1)")
                        (("1" (assert)
                          (("1" (lemma "deriv_sum_fun[T]")
                            (("1"
                              (inst - "(LAMBDA x: m!1 * x)"
                               "(LAMBDA x: b!1)")
                              (("1"
                                (assert)
                                (("1"
                                  (expand "+ " -1)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (replace -1)
                                      (("1"
                                        (hide -1)
                                        (("1"
                                          (apply-extensionality
                                           1
                                           :hide?
                                           t)
                                          (("1"
                                            (lemma "deriv_scal_fun[T]")
                                            (("1"
                                              (inst
                                               -
                                               "m!1"
                                               "(LAMBDA x: x)")
                                              (("1"
                                                (expand "*" -1)
                                                (("1"
                                                  (replace -1)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (hide -1)
                                                      (("1"
                                                        (lemma
                                                         "deriv_const_fun[T]")
                                                        (("1"
                                                          (expand
                                                           "const_fun")
                                                          (("1"
                                                            (inst?)
                                                            (("1"
                                                              (replace
                                                               -1)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lemma
                                                                   "deriv_id_fun[T]")
                                                                  (("1"
                                                                    (replace
                                                                     -1)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide 2)
                          (("2" (lemma "sum_derivable_fun[T]")
                            (("2"
                              (inst - "(LAMBDA x: m!1 * x)"
                               "(LAMBDA x: b!1)")
                              (("2"
                                (assert)
                                (("2"
                                  (expand "+ " -1)
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (scal_derivable_fun formula-decl nil derivatives nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (derivable? const-decl "bool" derivatives nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (deriv_sum_fun formula-decl nil derivatives nil)
    (deriv_scal_fun formula-decl nil derivatives nil)
    (deriv_const_fun formula-decl nil derivatives nil)
    (deriv_id_fun formula-decl nil derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_fun type-eq-decl nil derivatives nil)
    (sum_derivable_fun formula-decl nil derivatives nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (id_derivable_fun formula-decl nil derivatives nil)
    (const_derivable_fun formula-decl nil derivatives nil))
   shostak))
 (deriv_exp_fun_TCC1 0
  (deriv_exp_fun_TCC1-1 nil 3253536989 ("" (subtype-tcc) 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)
    (>= 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (derivable? const-decl "bool" derivatives nil))
   nil))
 (deriv_exp_fun 0
  (deriv_exp_fun-1 nil 3253536989
   ("" (induct "n")
    (("1" (skosimp*)
      (("1" (split)
        (("1" (expand "^")
          (("1" (expand "^")
            (("1" (expand "expt")
              (("1" (lemma "const_derivable_fun")
                (("1" (inst?)
                  (("1" (expand "const_fun") (("1" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (apply-extensionality 1 :hide? t) nil nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (inst?)
        (("2" (assert)
          (("2" (case-replace "j!1 = 0")
            (("1" (hide -2)
              (("1" (expand "^")
                (("1" (expand "^")
                  (("1" (expand "expt")
                    (("1" (expand "expt")
                      (("1" (split +)
                        (("1"
                          (case-replace
                           "(LAMBDA (t: T): f!1(t)) = f!1")
                          (("1" (hide 2)
                            (("1" (apply-extensionality + :hide? t) nil
                              nil))
                            nil))
                          nil)
                         ("2" (apply-extensionality 1 :hide? t)
                          (("1" (expand "*")
                            (("1"
                              (case-replace
                               "(LAMBDA (t: T): f!1(t)) = f!1")
                              (("1" (assert) nil nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (apply-extensionality 1 :hide? t)
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2"
                            (case-replace
                             "(LAMBDA (t: T): f!1(t)) = f!1")
                            (("2" (hide 2)
                              (("2"
                                (apply-extensionality 1 :hide? t)
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (flatten)
                (("2" (split +)
                  (("1" (hide -2)
                    (("1" (expand "derivable?")
                      (("1" (skosimp*)
                        (("1" (expand "derivable?")
                          (("1" (expand "convergent?")
                            (("1" (inst - "x!1")
                              (("1"
                                (inst - "x!1")
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (lemma "cnv_seq_prod_NQ")
                                    (("1"
                                      (inst
                                       -1
                                       "f!1^j!1"
                                       "f!1"
                                       "l!1"
                                       "l!2"
                                       "x!1")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (inst
                                           +
                                           "(f!1 ^ j!1)(x!1) * l!2 + f!1(x!1) * l!1")
                                          (("1"
                                            (case-replace
                                             "f!1 ^ (1 + j!1) = f!1 ^ j!1 * f!1")
                                            (("1"
                                              (hide -1 -2 -3 2)
                                              (("1"
                                                (expand "^")
                                                (("1"
                                                  (expand "^")
                                                  (("1"
                                                    (expand "expt" 1 1)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (apply-extensionality
                                                         1
                                                         :hide?
                                                         t)
                                                        (("1"
                                                          (expand "*")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2"
                    (case-replace "f!1 ^ (1 + j!1) = f!1 ^ j!1 * f!1")
                    (("1" (hide -1)
                      (("1" (lemma "deriv_prod_fun")
                        (("1" (inst?)
                          (("1" (replace -1)
                            (("1" (hide -1)
                              (("1"
                                (replace -2)
                                (("1"
                                  (hide -2)
                                  (("1"
                                    (case-replace
                                     "j!1 * f!1 ^ (j!1 - 1) * deriv(f!1) * f!1 = j!1 * f!1 ^ j!1 * deriv(f!1) ")
                                    (("1"
                                      (apply-extensionality 1 :hide? t)
                                      (("1"
                                        (hide -1)
                                        (("1"
                                          (expand "+ ")
                                          (("1"
                                            (expand "*")
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide 2)
                                      (("2"
                                        (apply-extensionality
                                         1
                                         :hide?
                                         t)
                                        (("2"
                                          (expand "*")
                                          (("2"
                                            (case
                                             "deriv(f!1)(x!1) = 0")
                                            (("1" (assert) nil nil)
                                             ("2"
                                              (lemma
                                               "both_sides_times1")
                                              (("2"
                                                (inst
                                                 -1
                                                 "deriv(f!1)(x!1)*j!1 "
                                                 "(f!1 ^ (j!1 - 1))(x!1) * f!1(x!1)"
                                                 "(f!1 ^ j!1)(x!1)")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (hide -1)
                                                    (("1"
                                                      (split -1)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide
                                                         -1
                                                         -2
                                                         2
                                                         3)
                                                        (("2"
                                                          (expand "^")
                                                          (("2"
                                                            (expand
                                                             "^")
                                                            (("2"
                                                              (expand
                                                               "expt"
                                                               1
                                                               2)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide -1 -2 3)
                                                  (("2"
                                                    (flatten)
                                                    (("2"
                                                      (mult-cases -1)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide -1 -2 -3 2)
                      (("2" (apply-extensionality 1 :hide? t)
                        (("2" (expand "^")
                          (("2" (expand "^")
                            (("2" (expand "*")
                              (("2"
                                (expand "expt" 1 1)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil))
      nil))
    nil)
   ((derivable? const-decl "bool" derivatives_def nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (^ const-decl "[T -> real]" real_fun_ops "reals/"))
   nil))
 (deriv_x_n_TCC1 0
  (deriv_x_n_TCC1-1 nil 3297592656 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) shostak))
 (deriv_x_n_TCC2 0
  (deriv_x_n_TCC2-1 nil 3297592656 ("" (subtype-tcc) 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)
    (>= 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (T_pred const-decl "[real -> boolean]" derivatives nil)
    (T formal-subtype-decl nil derivatives nil)
    (^ const-decl "real" exponentiation nil)
    (derivable? const-decl "bool" derivatives nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (deriv_x_n 0
  (deriv_x_n-1 nil 3297592562
   ("" (skosimp*)
    (("" (lemma "deriv_exp_fun")
      (("" (inst - "I" "n!1")
        (("" (assert)
          (("" (flatten)
            (("" (expand "I")
              (("" (expand "^" -1)
                (("" (assert)
                  (("" (replace -4 * rl)
                    (("" (expand "^" -2)
                      (("" (case-replace "(LAMBDA (x: T): x) = I")
                        (("1" (hide -1)
                          (("1" (replace -4 * rl)
                            (("1" (hide -4)
                              (("1"
                                (replace -2)
                                (("1"
                                  (hide -2)
                                  (("1"
                                    (expand "*")
                                    (("1"
                                      (apply-extensionality 1 :hide? t)
                                      (("1"
                                        (lemma "deriv_identity")
                                        (("1"
                                          (inst?)
                                          (("1"
                                            (expand "deriv" 1)
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "I") (("2" (propax) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deriv_exp_fun formula-decl nil derivatives nil)
    (derivable_id name-judgement "deriv_fun" derivatives nil)
    (id_fun_continuous name-judgement "continuous_fun"
     continuous_functions nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (derivable? const-decl "bool" derivatives nil)
    (deriv_fun type-eq-decl nil derivatives nil)
    (deriv const-decl "[T -> real]" derivatives nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (deriv_identity formula-decl nil derivatives_def nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.143 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

Eigene Datei ansehen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff