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