| products/sources/formale sprachen/PVS/Tarski/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: converse_zorn.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(derivatives
(IMP_derivatives_def_TCC1 0 (IMP_derivatives_def_TCC1-1 nil 3335530451 ("" (skosimp*) (("" (lemma "deriv_domain") (("" (expand "deriv_domain?") (("" (inst?) nil nil)) nil)) nil)) nil) ((deriv_domain formula-decl nil derivatives nil)) nil)) (IMP_derivatives_def_TCC2 0 (IMP_derivatives_def_TCC2-1 nil 3335530451 ("" (lemma "not_one_element") (("" (expand "not_one_element?") (("" (propax) nil 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_fun_def 0 (deriv_fun_def-1 nil 3297523287 ("" (skosimp*) (("" (case "derivable?(f!1)") (("1" (assert) (("1" (apply-extensionality 1 :hide? t) (("1" (lemma "deriv_def") (("1" (inst?) (("1" (expand "deriv" 1) (("1" (inst - "fp!1(x!1)" "x!1") (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "derivable?") (("2" (skosimp*) (("2" (expand "derivable?") (("2" (expand "convergent?") (("2" (inst -1 "x!1") (("2" (expand "convergence") (("2" (inst + "fp!1(x!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((derivable? const-decl "bool" derivatives nil) (bool nonempty-type-eq-decl nil booleans 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) (deriv const-decl "[T -> real]" derivatives nil) (deriv_fun type-eq-decl nil derivatives nil) (deriv_def formula-decl nil derivatives_def nil) (convergent? const-decl "bool" lim_of_functions nil) (convergence const-decl "bool" lim_of_functions nil) (derivable? const-decl "bool" derivatives_def nil)) shostak)) (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) ((nat nonempty-type-eq-decl nil naturalnumbers 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) (>= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans 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) (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions 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) (NQ const-decl "real" derivatives_def nil) (convergence const-decl "bool" convergence_functions nil) (convergence const-decl "bool" lim_of_functions nil) (convergent? const-decl "bool" lim_of_functions nil) (derivable? const-decl "bool" derivatives_def nil) (derivable? const-decl "bool" derivatives nil) (^ const-decl "real" exponentiation nil) (^ const-decl "[T -> real]" real_fun_ops "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (cnv_seq_prod_NQ formula-decl nil derivatives_def nil) (convergent? const-decl "bool" lim_of_functions nil) (both_sides_times1 formula-decl nil real_props nil) (zero_times3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (j!1 skolem-const-decl "nat" derivatives nil) (x!1 skolem-const-decl "T" derivatives nil) (/= const-decl "boolean" notequal nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (deriv_prod_fun formula-decl nil derivatives nil) (f!1 skolem-const-decl "[T -> real]" derivatives nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (const_derivable_fun formula-decl nil derivatives nil) (^ const-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv const-decl "[T -> real]" derivatives nil) (deriv_fun type-eq-decl nil derivatives 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) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.82 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
