|
(derivatives_def
(NQ_TCC1 0
(NQ_TCC1-1 nil 3253536989 ("" (grind) 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_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(deriv_TCC 0
(deriv_TCC-3 nil 3471267100
("" (skosimp*)
(("" (lemma "deriv_domain")
(("" (expand "adh")
(("" (expand "deriv_domain?")
(("" (expand "fullset")
(("" (skosimp*)
(("" (inst - "e!1" "x!1")
(("" (skosimp*)
(("" (inst?)
(("" (expand "A") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_domain formula-decl nil derivatives_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(y!1 skolem-const-decl "{u: nzreal | T_pred(u + x!1)}"
derivatives_def nil)
(x!1 skolem-const-decl "T" derivatives_def nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(fullset const-decl "set" sets nil)
(adh const-decl "setof[real]" convergence_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)
(deriv_TCC-2 nil 3471261300
("" (skosimp*)
(("" (lemma "nearzero")
(("" (expand "adh")
(("" (expand "fullset")
(("" (skosimp*)
(("" (inst - "e!1" "x!1")
(("" (skosimp*)
(("" (inst?)
(("" (expand "A") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((adh const-decl "setof[real]" convergence_functions nil)) nil)
(deriv_TCC-1 nil 3253536989
("" (skosimp*)
(("" (expand "adh")
(("" (expand "fullset")
(("" (skosimp*) (("" (postpone) nil nil)) nil)) nil))
nil))
nil)
((adh const-decl "setof[real]" convergence_functions nil)) nil))
(adh_A_lem 0
(adh_A_lem-3 nil 3471267122
("" (skosimp*)
(("" (lemma "deriv_domain")
(("" (expand "deriv_domain?")
(("" (expand "adh")
(("" (skosimp*)
(("" (inst?)
(("" (inst - "x!1")
(("" (skosimp*)
(("" (inst + "y!1")
(("1" (expand "fullset") (("1" (propax) nil nil))
nil)
("2" (expand "A") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_domain formula-decl nil derivatives_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(adh const-decl "setof[real]" convergence_functions 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(fullset const-decl "set" sets nil)
(y!1 skolem-const-decl "{u: nzreal | T_pred(u + x!1)}"
derivatives_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(x!1 skolem-const-decl "T" derivatives_def nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil)
(adh_A_lem-2 nil 3297610627
("" (skosimp*)
(("" (lemma "nearzero")
(("" (expand "adh")
(("" (skosimp*)
(("" (inst?)
(("" (inst - "x!1")
(("" (skosimp*)
(("" (inst + "y!1")
(("1" (expand "fullset") (("1" (propax) nil nil))
nil)
("2" (expand "A") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((adh const-decl "setof[real]" convergence_functions nil)) nil)
(adh_A_lem-1 nil 3297610566
("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak))
(continuous_lim 0
(continuous_lim-1 nil 3253536989
(""
(grind :exclude ("abs" "adh") :rewrites
("deriv_TCC" "adherence_fullset[T]") :if-match nil)
(("1" (inst? -4)
(("1" (skolem!)
(("1" (inst + "delta!1")
(("1" (skosimp)
(("1" (inst - "x!2 - x!1")
(("1" (assert) nil nil)
("2" (delete -5) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst? -4)
(("2" (skolem!)
(("2" (inst + "delta!1")
(("2" (skosimp :preds? t)
(("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(x!2 skolem-const-decl "T" derivatives_def nil)
(x!1 skolem-const-decl "T" derivatives_def nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(continuous? const-decl "bool" continuous_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergence const-decl "bool" convergence_functions nil)
(fullset const-decl "set" sets nil)
(deriv_TCC formula-decl nil derivatives_def nil))
nil))
(deriv_continuous 0
(deriv_continuous-1 nil 3253536989
("" (skosimp)
(("" (rewrite "continuous_lim" :dir rl)
((""
(case-replace "(LAMBDA (h: (A(x!1))): f!1(h + x!1)) =
const_fun(f!1(x!1)) + I[(A(x!1))] * NQ(f!1, x!1)")
(("1" (delete -1)
(("1"
(auto-rewrite-theory "lim_of_functions[(A(x!1))]" :exclude
("convergence"
"convergence_def"
"convergent?"
"lim"
"lim_fun_lemma"
"lim_fun_def")
:always? t)
(("1" (auto-rewrite "deriv_TCC")
(("1" (grind :defs nil) nil nil)) nil))
nil))
nil)
("2" (delete -1 2)
(("2" (apply-extensionality :hide? t)
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
nil)
("3" (delete -1 2) (("3" (grind) nil nil)) nil))
nil))
nil))
nil)
((continuous_lim 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_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(x!1 skolem-const-decl "T" derivatives_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(lim_sum_fun formula-decl nil lim_of_functions nil)
(lim_prod_fun formula-decl nil lim_of_functions nil)
(lim_identity formula-decl nil lim_of_functions nil)
(lim_const_fun formula-decl nil lim_of_functions nil)
(prod_fun_convergent formula-decl nil lim_of_functions nil)
(lim_e_del formula-decl nil lim_of_functions nil)
(sum_fun_convergent formula-decl nil lim_of_functions nil)
(convergent_identity formula-decl nil lim_of_functions nil)
(const_fun_convergent formula-decl nil lim_of_functions nil)
(deriv_TCC formula-decl nil derivatives_def nil)
(convergence_equiv formula-decl nil lim_of_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(NQ const-decl "real" derivatives_def nil)
(I const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil)
(id_fun_continuous name-judgement "continuous_fun"
continuous_functions nil))
nil))
(derivable_continuous 0
(derivable_continuous-1 nil 3253536989
("" (expand "derivable?")
(("" (expand "convergent?")
(("" (skosimp*) (("" (forward-chain "deriv_continuous") nil nil))
nil))
nil))
nil)
((convergent? const-decl "bool" lim_of_functions nil)
(deriv_continuous 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_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil))
nil))
(sum_NQ 0
(sum_NQ-1 nil 3253536989
("" (skolem!)
(("" (apply-extensionality) (("" (grind) 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(NQ const-decl "real" derivatives_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(neg_NQ 0
(neg_NQ-1 nil 3442585851
("" (skolem!)
(("" (apply-extensionality) (("" (grind) 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(NQ const-decl "real" derivatives_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(diff_NQ 0
(diff_NQ-1 nil 3253536989
("" (skolem!)
(("" (apply-extensionality) (("" (grind) 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(NQ const-decl "real" derivatives_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(scal_NQ 0
(scal_NQ-1 nil 3253536989
("" (skolem!)
(("" (apply-extensionality) (("" (grind) 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(NQ const-decl "real" derivatives_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(const_NQ 0
(const_NQ-1 nil 3253536989
("" (skolem!)
(("" (apply-extensionality) (("" (grind) 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(NQ const-decl "real" derivatives_def nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(identity_NQ 0
(identity_NQ-1 nil 3253536989
("" (skolem!)
(("" (apply-extensionality) (("" (grind) 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(I const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(NQ const-decl "real" derivatives_def nil)
(id_fun_continuous name-judgement "continuous_fun"
continuous_functions nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(prod_NQ 0
(prod_NQ-1 nil 3253536989 ("" (grind) nil nil)
((real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(NQ const-decl "real" derivatives_def nil)
(* const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(cnv_seq_prod_NQ 0
(cnv_seq_prod_NQ-1 nil 3253536989
("" (auto-rewrite "deriv_TCC")
(("" (skosimp)
(("" (name "F" "LAMBDA (h : (A(x!1))) : f1!1(x!1 + h)")
(("1"
(case-replace
"NQ(f1!1 * f2!1, x!1) = f2!1(x!1) * NQ(f1!1, x!1) + F * NQ(f2!1, x!1)")
(("1"
(auto-rewrite-theory "lim_of_functions[(A(x!1))]" :exclude
("convergence"
"convergence_def"
"convergent?"
"lim"
"lim_fun_def"
"lim_e_del")
:always? t)
(("1" (forward-chain "deriv_continuous" -3)
(("1" (use "continuous_lim")
(("1" (replace*) (("1" (grind :defs nil) nil nil))
nil))
nil))
nil))
nil)
("2" (replace -1 + rl)
(("2" (delete -1 -2 -3 2)
(("2" (apply-extensionality :hide? t)
(("1" (grind) nil nil)
("2" (delete 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (delete -1 -2 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((NQ const-decl "real" derivatives_def nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_continuous formula-decl nil derivatives_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(convergence_equiv formula-decl nil lim_of_functions nil)
(sum_fun_convergent formula-decl nil lim_of_functions nil)
(scal_fun_convergent formula-decl nil lim_of_functions nil)
(prod_fun_convergent formula-decl nil lim_of_functions nil)
(lim_scal_fun formula-decl nil lim_of_functions nil)
(lim_prod_fun formula-decl nil lim_of_functions nil)
(lim_sum_fun formula-decl nil lim_of_functions nil)
(continuous_lim formula-decl nil derivatives_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(x!1 skolem-const-decl "T" derivatives_def 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(inv_NQ 0
(inv_NQ-1 nil 3253536989 ("" (grind) nil nil)
((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(NQ const-decl "real" derivatives_def nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(cnv_seq_inv_NQ 0
(cnv_seq_inv_NQ-2 nil 3442586093
("" (auto-rewrite "deriv_TCC")
(("" (skosimp)
(("" (name "F" "LAMBDA (h : (A(x!1))) : g!1(x!1 + h)")
(("1"
(case-replace
"NQ(1/g!1, x!1) = - NQ(g!1, x!1) / (g!1(x!1) * F)")
(("1" (rewrite "cv_div[(A(x!1))]")
(("1" (rewrite "cv_neg[(A(x!1))]") nil nil)
("2" (rewrite "cv_scal[(A(x!1))]")
(("2" (use "continuous_lim" ("f" "g!1"))
(("2" (ground)
(("2" (forward-chain "deriv_continuous") nil nil))
nil))
nil))
nil))
nil)
("2" (replace -1 + rl)
(("2" (delete -1 -2 2)
(("2" (apply-extensionality :hide? t)
(("1" (grind) nil nil)
("2" (delete 2)
(("2" (grind :rewrites "zero_times3") nil nil)) nil))
nil))
nil))
nil)
("3" (replace -1 + rl)
(("3" (delete -1 -2 2)
(("3" (grind :rewrites "zero_times3") nil nil)) nil))
nil))
nil)
("2" (delete -1 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((NQ const-decl "real" derivatives_def 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/")
(cv_scal formula-decl nil lim_of_functions nil)
(deriv_continuous formula-decl nil derivatives_def nil)
(continuous_lim formula-decl nil derivatives_def nil)
(cv_neg formula-decl nil lim_of_functions nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(cv_div formula-decl nil lim_of_functions nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(x!1 skolem-const-decl "T" derivatives_def nil)
(zero_times3 formula-decl nil real_props 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil)
(cnv_seq_inv_NQ-1 nil 3253536989
("" (auto-rewrite "deriv_TCC")
(("" (skosimp)
(("" (name "F" "LAMBDA (h : (A(x!1))) : g!1(x!1 + h)")
(("1"
(case-replace
"NQ(1/g!1, x!1) = - NQ(g!1, x!1) / (g!1(x!1) * F)")
(("1" (rewrite "cv_div[(A(x!1))]")
(("1" (rewrite "cv_opp[(A(x!1))]") nil nil)
("2" (rewrite "cv_scal[(A(x!1))]")
(("2" (use "continuous_lim" ("f" "g!1"))
(("2" (ground)
(("2" (forward-chain "deriv_continuous") nil nil))
nil))
nil))
nil)
("3" (replace -2 1 rl)
(("3" (delete -1 -2 -3 2)
(("3" (grind :rewrites "zero_times3") nil nil)) nil))
nil))
nil)
("2" (replace -1 + rl)
(("2" (delete -1 -2 2)
(("2" (apply-extensionality :hide? t)
(("1" (grind) nil nil)
("2" (delete 2)
(("2" (grind :rewrites "zero_times3") nil nil)) nil)
("3" (delete 2) (("3" (grind) nil nil)) nil))
nil))
nil))
nil)
("3" (replace -1 + rl)
(("3" (delete -1 -2 2)
(("3" (grind :rewrites "zero_times3") nil nil)) nil))
nil))
nil)
("2" (delete -1 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((cv_scal formula-decl nil lim_of_functions nil)
(cv_div formula-decl nil lim_of_functions nil))
nil))
(sum_derivable 0
(sum_derivable-1 nil 3253536989
("" (auto-rewrite "derivable?" "sum_NQ" "deriv_TCC")
(("" (skosimp)
(("" (assert)
(("" (use "sum_fun_convergent[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((sum_fun_convergent formula-decl nil lim_of_functions nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(NQ const-decl "real" derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil)
(sum_NQ formula-decl nil derivatives_def nil))
nil))
(neg_derivable 0
(neg_derivable-1 nil 3442586144
("" (auto-rewrite "derivable?" "neg_NQ" "deriv_TCC")
(("" (skosimp)
(("" (assert)
(("" (use "neg_fun_convergent[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((neg_fun_convergent formula-decl nil lim_of_functions nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(NQ const-decl "real" derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil)
(neg_NQ formula-decl nil derivatives_def nil))
nil))
(diff_derivable 0
(diff_derivable-1 nil 3253536989
("" (auto-rewrite "derivable?" "diff_NQ" "deriv_TCC")
(("" (skosimp)
(("" (assert)
(("" (use "diff_fun_convergent[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((diff_fun_convergent formula-decl nil lim_of_functions nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(NQ const-decl "real" derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil)
(diff_NQ formula-decl nil derivatives_def nil))
nil))
(prod_derivable 0
(prod_derivable-1 nil 3253536989
("" (expand "derivable?")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (use "cnv_seq_prod_NQ")
(("" (assert) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil)
((convergent? const-decl "bool" lim_of_functions nil)
(cnv_seq_prod_NQ formula-decl nil derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals 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)
(real_plus_real_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives_def nil))
nil))
(scal_derivable 0
(scal_derivable-1 nil 3253536989
("" (auto-rewrite "derivable?" "scal_NQ" "deriv_TCC")
(("" (skosimp)
(("" (assert)
(("" (use "scal_fun_convergent[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((scal_fun_convergent formula-decl nil lim_of_functions nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(NQ const-decl "real" derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil)
(scal_NQ formula-decl nil derivatives_def nil))
nil))
(const_derivable 0
(const_derivable-1 nil 3253536989
("" (skolem!)
(("" (auto-rewrite "derivable?" "const_NQ" "deriv_TCC")
(("" (assert)
(("" (lemma "const_fun_convergent[(A(x!1))]")
(("" (inst - "0" "0") nil nil)) nil))
nil))
nil))
nil)
((A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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_convergent formula-decl nil lim_of_functions nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(adh const-decl "setof[real]" convergence_functions nil)
(deriv_TCC formula-decl nil derivatives_def nil)
(const_NQ formula-decl nil derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil))
nil))
(inv_derivable 0
(inv_derivable-1 nil 3253536989
("" (expand "derivable?")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (use "cnv_seq_inv_NQ")
(("" (assert) (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil)
((convergent? const-decl "bool" lim_of_functions nil)
(cnv_seq_inv_NQ formula-decl nil derivatives_def nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(derivable? const-decl "bool" derivatives_def nil))
nil))
(div_derivable 0
(div_derivable-1 nil 3253536989
("" (skosimp)
(("" (rewrite "div_function[T]")
(("" (rewrite "prod_derivable")
(("" (rewrite "inv_derivable") nil nil)) nil))
nil))
nil)
((div_function formula-decl nil real_fun_ops "reals/")
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil 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)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(inv_derivable formula-decl nil derivatives_def nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(prod_derivable formula-decl nil derivatives_def nil))
nil))
(identity_derivable 0
(identity_derivable-1 nil 3253536989
("" (skolem!)
(("" (auto-rewrite "derivable?" "identity_NQ" "deriv_TCC")
(("" (assert)
(("" (use "const_fun_convergent[(A(x!1))]" ("b" "1" "c" "0"))
nil nil))
nil))
nil))
nil)
((deriv_TCC formula-decl nil derivatives_def nil)
(const_fun_convergent formula-decl nil lim_of_functions nil)
(adh const-decl "setof[real]" convergence_functions nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(identity_NQ formula-decl nil derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil)
(id_fun_continuous name-judgement "continuous_fun"
continuous_functions nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil))
nil))
(deriv_TCC1 0
(deriv_TCC1-1 nil 3253536989
("" (auto-rewrite "derivable?")
(("" (skosimp :preds? t) (("" (assert) nil nil)) nil)) nil)
((derivable? const-decl "bool" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" 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))
nil))
(deriv_def 0
(deriv_def-1 nil 3297521117
("" (skosimp*)
(("" (prop)
(("1" (expand "derivable?")
(("1" (expand "convergent?") (("1" (inst + "l!1") nil nil))
nil))
nil)
("2" (expand "deriv")
(("2" (rewrite "lim_fun_def")
(("2" (hide 2)
(("2" (expand "convergent?") (("2" (inst + "l!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((convergent? const-decl "bool" lim_of_functions nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(derivable? const-decl "bool" derivatives_def nil)
(lim_fun_def formula-decl nil lim_of_functions nil)
(NQ const-decl "real" derivatives_def nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(deriv const-decl "real" derivatives_def nil))
shostak))
(deriv_sum_TCC1 0
(deriv_sum_TCC1-1 nil 3253536989
("" (skosimp) (("" (rewrite "sum_derivable") nil nil)) nil)
((sum_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_def nil)
(T formal-subtype-decl nil derivatives_def nil))
nil))
(deriv_sum 0
(deriv_sum-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "sum_derivable" "derivable?" "deriv"
"sum_NQ" "lim_sum_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
((derivable? const-decl "bool" derivatives_def nil)
(sum_NQ formula-decl nil derivatives_def nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(lim_sum_fun formula-decl nil lim_of_functions nil)
(deriv const-decl "real" derivatives_def nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(deriv_neg_TCC1 0
(deriv_neg_TCC1-1 nil 3442582979
("" (lemma "neg_derivable") (("" (propax) nil nil)) nil)
((neg_derivable formula-decl nil derivatives_def nil)) shostak))
(deriv_neg 0
(deriv_neg-2 nil 3442586421
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "neg_derivable" "derivable?" "deriv"
"neg_NQ" "lim_neg_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
((derivable? const-decl "bool" derivatives_def nil)
(neg_NQ formula-decl nil derivatives_def nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(lim_neg_fun formula-decl nil lim_of_functions nil)
(deriv const-decl "real" derivatives_def nil)
(minus_real_is_real application-judgement "real" reals nil))
nil)
(deriv_neg-1 nil 3442586370
(";;; Proof for formula derivatives_def.deriv_opposite" (skosimp)
((";;; Proof for formula derivatives_def.deriv_opposite"
(auto-rewrite "deriv_TCC" "opposite_derivable" "derivable?"
"deriv" "opposite_NQ" "lim_opposite_fun[(A(x!1))]")
((";;; Proof for formula derivatives_def.deriv_opposite" (assert)
nil))))
"")
nil nil))
(deriv_diff_TCC1 0
(deriv_diff_TCC1-1 nil 3253536989
("" (skosimp) (("" (rewrite "diff_derivable") nil nil)) nil)
((diff_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_def nil)
(T formal-subtype-decl nil derivatives_def nil))
nil))
(deriv_diff 0
(deriv_diff-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "diff_derivable" "derivable?" "deriv"
"diff_NQ" "lim_diff_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
((derivable? const-decl "bool" derivatives_def nil)
(diff_NQ formula-decl nil derivatives_def nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(lim_diff_fun formula-decl nil lim_of_functions nil)
(deriv const-decl "real" derivatives_def nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(deriv_prod_TCC1 0
(deriv_prod_TCC1-1 nil 3253536989
("" (skosimp) (("" (rewrite "prod_derivable") nil nil)) nil)
((prod_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_def nil)
(T formal-subtype-decl nil derivatives_def nil))
nil))
(deriv_prod 0
(deriv_prod-1 nil 3253536989
("" (skosimp)
(("" (use "prod_derivable")
(("" (assert)
((""
(auto-rewrite "deriv" "deriv_TCC" "derivable?"
("lim_fun_def[(A(x!1))]"
"lim_fun_lemma[(A(x!1))]"))
(("" (assert)
((""
(use "cnv_seq_prod_NQ"
("l1" "lim(NQ(f1!1, x!1), 0)" "l2"
"lim(NQ(f2!1, x!1), 0)"))
(("" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((prod_derivable formula-decl nil derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(NQ const-decl "real" derivatives_def nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(cnv_seq_prod_NQ formula-decl nil derivatives_def nil)
(lim_fun_lemma formula-decl nil lim_of_functions nil)
(derivable? const-decl "bool" derivatives_def nil)
(deriv const-decl "real" derivatives_def nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(lim_fun_def formula-decl nil lim_of_functions nil))
nil))
(deriv_const_TCC1 0
(deriv_const_TCC1-1 nil 3253536989
("" (lemma "const_derivable") (("" (propax) nil nil)) nil)
((const_derivable formula-decl nil derivatives_def nil)) nil))
(deriv_const 0
(deriv_const-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "const_derivable" "derivable?" "deriv"
"const_NQ")
(("" (assert)
(("" (use "lim_const_fun[(A(x!1))]" ("b" "0" "c" "0")) nil
nil))
nil))
nil))
nil)
((deriv_TCC formula-decl nil derivatives_def nil)
(lim_const_fun formula-decl nil lim_of_functions nil)
(adh const-decl "setof[real]" convergence_functions nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(const_NQ formula-decl nil derivatives_def nil)
(deriv const-decl "real" derivatives_def nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil))
nil))
(deriv_scal_TCC1 0
(deriv_scal_TCC1-1 nil 3253536989
("" (lemma "scal_derivable") (("" (propax) nil nil)) nil)
((scal_derivable formula-decl nil derivatives_def nil)) nil))
(deriv_scal 0
(deriv_scal-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "scal_derivable" "derivable?" "deriv"
"scal_NQ" "lim_scal_fun[(A(x!1))]")
(("" (assert) nil nil)) nil))
nil)
((derivable? const-decl "bool" derivatives_def nil)
(scal_NQ formula-decl nil derivatives_def nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(lim_scal_fun formula-decl nil lim_of_functions nil)
(deriv const-decl "real" derivatives_def nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(deriv_inv_TCC1 0
(deriv_inv_TCC1-1 nil 3253536989
("" (lemma "inv_derivable") (("" (propax) nil nil)) nil)
((inv_derivable formula-decl nil derivatives_def nil)) nil))
(deriv_inv 0
(deriv_inv-1 nil 3253536989
("" (skosimp)
(("" (forward-chain "inv_derivable")
(("" (assert)
((""
(auto-rewrite "deriv" "deriv_TCC" "derivable?"
("lim_fun_def[(A(x!1))]"
"lim_fun_lemma[(A(x!1))]"))
(("" (assert)
(("" (use "cnv_seq_inv_NQ" ("l1" "lim(NQ(g!1, x!1), 0)"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((inv_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_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(NQ const-decl "real" derivatives_def nil)
(lim const-decl "{l: real | convergence(f, x0, l)}"
lim_of_functions nil)
(convergence const-decl "bool" lim_of_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(cnv_seq_inv_NQ formula-decl nil derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil)
(deriv const-decl "real" derivatives_def nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(lim_fun_def formula-decl nil lim_of_functions nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
nil))
(deriv_div_TCC1 0
(deriv_div_TCC1-1 nil 3253536989
("" (skosimp) (("" (rewrite "div_derivable") nil nil)) nil)
((div_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_def nil)
(T formal-subtype-decl nil derivatives_def nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil))
nil))
(deriv_div 0
(deriv_div-1 nil 3253536989
(""
(grind :defs nil :rewrites
("inv_derivable" "deriv_inv" "deriv_prod" "div_function[T]" "/"))
nil nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(inv_derivable formula-decl nil derivatives_def nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_inv formula-decl nil derivatives_def nil)
(deriv_prod formula-decl nil derivatives_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(div_function formula-decl nil real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil))
nil))
(deriv_identity_TCC1 0
(deriv_identity_TCC1-1 nil 3253536989
("" (lemma "identity_derivable") (("" (propax) nil nil)) nil)
((identity_derivable formula-decl nil derivatives_def nil)) nil))
(deriv_identity 0
(deriv_identity-1 nil 3253536989
("" (skosimp)
((""
(auto-rewrite "deriv_TCC" "identity_derivable" "derivable?"
"deriv" "identity_NQ")
(("" (use "lim_const_fun[(A(x!1))]" ("b" "1" "c" "0"))
(("" (assert) nil nil)) nil))
nil))
nil)
((identity_NQ formula-decl nil derivatives_def nil)
(deriv const-decl "real" derivatives_def nil)
(id_fun_continuous name-judgement "continuous_fun"
continuous_functions nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil)
(A const-decl "setof[nzreal]" derivatives_def nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil derivatives_def nil)
(T_pred const-decl "[real -> boolean]" derivatives_def nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(adh const-decl "setof[real]" convergence_functions nil)
(lim_const_fun formula-decl nil lim_of_functions nil)
(deriv_TCC formula-decl nil derivatives_def nil))
nil)))
¤ Dauer der Verarbeitung: 0.95 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.
|
