|
(chain_rule
(chain_rule_cnvg_TCC1 0
(chain_rule_cnvg_TCC1-1 nil 3475835686
("" (lemma deriv_domain1)
(("" (expand "deriv_domain?") (("" (propax) nil nil)) nil)) nil)
((deriv_domain1 formula-decl nil chain_rule nil)) nil))
(chain_rule_cnvg_TCC2 0
(chain_rule_cnvg_TCC2-1 nil 3475835686
("" (lemma not_one_element1)
(("" (expand "not_one_element?") (("" (propax) nil nil)) nil)) nil)
((not_one_element1 formula-decl nil chain_rule nil)) nil))
(chain_rule_cnvg_TCC3 0
(chain_rule_cnvg_TCC3-1 nil 3475835686
("" (skosimp*)
(("" (lemma deriv_domain2)
(("" (expand "deriv_domain?") (("" (inst?) nil nil)) nil)) nil))
nil)
((deriv_domain2 formula-decl nil chain_rule nil)) nil))
(chain_rule_cnvg_TCC4 0
(chain_rule_cnvg_TCC4-1 nil 3475835686
("" (lemma not_one_element2)
(("" (skosimp*)
(("" (expand "not_one_element?") (("" (inst?) nil nil)) nil))
nil))
nil)
((not_one_element2 formula-decl nil chain_rule nil)) nil))
(chain_rule_cnvg 0
(chain_rule_cnvg-1 nil 3475835691
("" (skosimp)
((""
(auto-rewrite "deriv_TCC[T1]" "deriv_TCC[T2]"
"adherence_fullset[T1]" "adherence_fullset[T2]")
(("1" (use "derivative_equivalence1[T1]")
(("1" (replace -2)
(("1" (prop)
(("1" (forward-chain "derivable_continuous[T1]")
(("1" (delete -2 -3)
(("1" (rewrite continuity_def)
(("1" (rewrite "derivative_equivalence2[T1]")
(("1" (rewrite "derivative_equivalence2[T1]")
(("1" (rewrite "derivative_equivalence2[T2]")
(("1" (skosimp*)
(("1"
(inst 1
"DG!1 * phi!1 + DF!1 * (phi!2 o f!1) + phi!1 * (phi!2 o f!1)")
(("1" (prop)
(("1"
(use
"convergence_composition"
("f" "f!1" "g" "phi!2" "x" "x!1"))
(("1"
(assert)
(("1"
(delete -4 -5 -6)
(("1"
(lemma "cv_sum[T1]")
(("1"
(inst
-
"x!1"
"DG!1 * phi!1"
"DF!1 * (phi!2 o f!1) + phi!1 * (phi!2 o f!1)"
"0"
"0")
(("1"
(assert)
(("1"
(split -1)
(("1"
(expand "+")
(("1" (propax) nil nil))
nil)
("2"
(hide -1 -2 2)
(("2"
(lemma "cv_scal[T1]")
(("2"
(inst
-
"x!1"
"DG!1"
"phi!1"
"0")
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(lemma "cv_sum[T1]")
(("3"
(inst
-
"x!1"
"DF!1 * (phi!2 o f!1)"
"phi!1 * (phi!2 o f!1)"
"0"
"0")
(("3"
(assert)
(("3"
(hide 2)
(("3"
(lemma
"cv_scal[T1]")
(("3"
(inst
-
"x!1"
"DF!1"
"(phi!2 o f!1)"
"0")
(("3"
(assert)
(("3"
(lemma
"cv_prod[T1]")
(("3"
(inst
-
"x!1"
"phi!1"
"(phi!2 o f!1)"
"0"
"0")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(delete -1 -2 -4)
(("2"
(skolem!)
(("2"
(inst -1 "y!1")
(("2"
(inst -2 "f!1(y!1)")
(("2"
(expand "o ")
(("2"
(expand "*")
(("2"
(expand "+ ")
(("2"
(replace -2)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "deriv_domain2")
(("2" (lemma "not_one_element2")
(("2" (expand "not_one_element?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (lemma "not_one_element1")
(("2" (expand "not_one_element?")
(("2" (propax) nil nil)) nil))
nil)
("3" (lemma "deriv_domain1 ")
(("3" (propax) nil nil)) nil))
nil)
("2" (lemma "not_one_element1")
(("2" (expand "not_one_element?")
(("2" (propax) nil nil)) nil))
nil)
("3" (lemma "deriv_domain1 ")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element1")
(("2" (expand "not_one_element?") (("2" (propax) nil nil))
nil))
nil)
("3" (lemma "deriv_domain1 ") (("3" (propax) nil nil)) nil))
nil)
("2" (lemma "not_one_element2") (("2" (propax) nil nil)) nil)
("3" (lemma "deriv_domain2 ") (("3" (propax) nil nil)) nil))
nil))
nil)
((deriv_domain? const-decl "bool" deriv_domain_def nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(T2 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(derivable_continuous formula-decl nil derivatives_def nil)
(continuity_def formula-decl nil continuous_functions nil)
(O const-decl "T3" function_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cv_sum formula-decl nil lim_of_functions nil)
(cv_prod formula-decl nil lim_of_functions nil)
(cv_scal formula-decl nil lim_of_functions nil)
(convergence_composition formula-decl nil lim_of_composition 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/")
(not_one_element1 formula-decl nil chain_rule nil)
(deriv_domain1 formula-decl nil chain_rule nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(derivative_equivalence2 formula-decl nil derivatives_alt nil)
(real_times_real_is_real application-judgement "real" reals nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T1_pred const-decl "[real -> boolean]" chain_rule nil)
(derivative_equivalence1 formula-decl nil derivatives_alt nil)
(not_one_element2 formula-decl nil chain_rule nil)
(deriv_domain2 formula-decl nil chain_rule nil))
nil))
(composition_derivable_TCC1 0
(composition_derivable_TCC1-1 nil 3313840193
("" (skosimp)
(("" (lemma "deriv_domain2")
(("" (expand "deriv_domain?") (("" (propax) nil nil)) nil)) nil))
nil)
((deriv_domain2 formula-decl nil chain_rule nil)) nil))
(composition_derivable_TCC2 0
(composition_derivable_TCC2-1 nil 3313840193
("" (skosimp)
(("" (lemma "not_one_element2")
(("" (expand "not_one_element?") (("" (propax) nil nil)) nil))
nil))
nil)
((not_one_element2 formula-decl nil chain_rule nil)) nil))
(composition_derivable 0
(composition_derivable-3 nil 3475836001
("" (expand "derivable?")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (forward-chain "chain_rule_cnvg") (("" (inst?) nil nil))
nil))
nil))
nil))
nil)
((convergent? const-decl "bool" lim_of_functions nil)
(chain_rule_cnvg formula-decl nil chain_rule 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)
(T1_pred const-decl "[real -> boolean]" chain_rule nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule nil)
(T2 formal-subtype-decl nil chain_rule nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(derivable? const-decl "bool" derivatives_def nil))
nil)
(composition_derivable-2 nil 3445340288
("" (expand "derivable?")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (forward-chain "chain_rule") (("" (inst?) nil nil)) nil))
nil))
nil))
nil)
((convergent? const-decl "bool" lim_of_functions nil)
(derivable? const-decl "bool" derivatives_def nil))
nil)
(composition_derivable-1 nil 3313840193
("" (expand "derivable")
(("" (expand "convergent?")
(("" (skosimp*)
(("" (forward-chain "chain_rule") (("" (inst?) nil nil)) nil))
nil))
nil))
nil)
((convergent? const-decl "bool" lim_of_functions nil)) nil))
(composition_derivable_fun_TCC1 0
(composition_derivable_fun_TCC1-1 nil 3313840193
("" (skosimp*)
(("" (lemma "deriv_domain2") (("" (propax) nil nil)) nil)) nil)
((deriv_domain2 formula-decl nil chain_rule nil)) nil))
(composition_derivable_fun_TCC2 0
(composition_derivable_fun_TCC2-1 nil 3313840193
("" (skosimp*)
(("" (lemma not_one_element2) (("" (propax) nil nil)) nil)) nil)
((not_one_element2 formula-decl nil chain_rule nil)) nil))
(composition_derivable_fun 0
(composition_derivable_fun-1 nil 3313840193
("" (expand "derivable?")
(("" (skosimp*)
(("" (rewrite "composition_derivable")
(("1" (inst?) nil nil) ("2" (inst? -2) nil nil)) nil))
nil))
nil)
((T2 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T1_pred const-decl "[real -> boolean]" chain_rule 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)
(composition_derivable formula-decl nil chain_rule nil)
(derivable? const-decl "bool" derivatives nil))
nil))
(deriv_composition_TCC1 0
(deriv_composition_TCC1-1 nil 3313840193
("" (lemma "composition_derivable")
(("" (skosimp*)
(("" (inst?) (("" (expand "O") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((O const-decl "T3" function_props nil)
(T2 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T1_pred const-decl "[real -> boolean]" chain_rule 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)
(composition_derivable formula-decl nil chain_rule nil))
nil))
(deriv_composition 0
(deriv_composition-1 nil 3313840193
("" (skosimp)
(("" (forward-chain "composition_derivable")
((""
(auto-rewrite "deriv_TCC[T1]" "deriv_TCC[T2]"
("deriv[T1]" "derivable?[T1]" "deriv[T2]"
"derivable?[T2]")
("lim_fun_lemma[(A[T1](x!1))]"
"lim_fun_lemma[(A[T2](f!1(x!1)))]"))
(("1" (assert)
(("1" (rewrite "lim_fun_def[(A[T1](x!1))]")
(("1" (rewrite "chain_rule_cnvg") nil nil)) nil))
nil)
("2" (skosimp*)
(("2" (lemma "not_one_element2")
(("2" (expand "not_one_element?") (("2" (inst?) nil nil))
nil))
nil))
nil)
("3" (lemma "deriv_domain2 ")
(("3" (skosimp*)
(("3" (expand "deriv_domain?") (("3" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((composition_derivable formula-decl nil chain_rule 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)
(T1_pred const-decl "[real -> boolean]" chain_rule nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule nil)
(T2 formal-subtype-decl nil chain_rule nil)
(deriv_domain2 formula-decl nil chain_rule nil)
(not_one_element2 formula-decl nil chain_rule nil)
(real_times_real_is_real application-judgement "real" reals nil)
(deriv const-decl "real" derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil)
(lim_fun_lemma formula-decl nil lim_of_functions nil)
(chain_rule_cnvg formula-decl nil chain_rule 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)
(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)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(O const-decl "T3" function_props nil)
(NQ const-decl "real" derivatives_def nil)
(lim_fun_def formula-decl nil lim_of_functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil))
nil))
(gg_TCC1 0
(gg_TCC1-1 nil 3313840193
("" (lemma "deriv_domain2") (("" (propax) nil nil)) nil)
((deriv_domain2 formula-decl nil chain_rule nil)) nil))
(gg_TCC2 0
(gg_TCC2-1 nil 3313840193
("" (lemma "not_one_element2") (("" (propax) nil nil)) nil)
((not_one_element2 formula-decl nil chain_rule nil)) nil))
(deriv_comp_fun_TCC1 0
(deriv_comp_fun_TCC1-1 nil 3313840193
("" (skosimp) (("" (rewrite "composition_derivable_fun") nil nil))
nil)
((composition_derivable_fun formula-decl nil chain_rule 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)
(T1_pred const-decl "[real -> boolean]" chain_rule nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule nil)
(T2 formal-subtype-decl nil chain_rule nil)
(bool nonempty-type-eq-decl nil booleans nil)
(derivable? const-decl "bool" derivatives nil))
nil))
(deriv_comp_fun 0
(deriv_comp_fun-1 nil 3313840193
("" (skolem-typepred)
(("" (assert)
(("" (expand "derivable?")
(("" (auto-rewrite "composition_derivable_fun")
(("" (apply-extensionality :hide? t)
(("" (expand "*")
(("" (expand "o" 1 2)
(("" (expand "deriv")
(("" (rewrite "deriv_composition")
(("1" (inst? -1) nil nil) ("2" (inst? -2) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(deriv_composition formula-decl nil chain_rule nil)
(deriv_fun type-eq-decl nil derivatives nil)
(deriv const-decl "[T -> real]" derivatives nil)
(O const-decl "T3" function_props nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(T2 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule nil)
(derivable? const-decl "bool" derivatives nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T1_pred const-decl "[real -> boolean]" chain_rule 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))
(comp_derivable_fun 0
(comp_derivable_fun-1 nil 3475834576
("" (skosimp*)
(("" (lemma "composition_derivable_fun")
(("" (expand "o ") (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((composition_derivable_fun formula-decl nil chain_rule 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)
(T1_pred const-decl "[real -> boolean]" chain_rule nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule nil)
(T2 formal-subtype-decl nil chain_rule nil)
(O const-decl "T3" function_props nil))
shostak))
(chain_rule_TCC1 0
(chain_rule_TCC1-1 nil 3475835726
("" (skosimp*)
(("" (lemma comp_derivable_fun)
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((comp_derivable_fun formula-decl nil chain_rule nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T2 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T1_pred const-decl "[real -> boolean]" chain_rule 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))
(chain_rule 0
(chain_rule-1 nil 3475853574
("" (skosimp*)
(("" (lemma deriv_comp_fun)
(("" (expand "o ") (("" (inst?) nil nil)) nil)) nil))
nil)
((deriv_comp_fun formula-decl nil chain_rule nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T2 formal-subtype-decl nil chain_rule nil)
(T2_pred const-decl "[real -> boolean]" chain_rule nil)
(T1 formal-subtype-decl nil chain_rule nil)
(T1_pred const-decl "[real -> boolean]" chain_rule 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)
(O const-decl "T3" function_props nil))
shostak)))
¤ Dauer der Verarbeitung: 0.29 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.
|
