| products/sources/formale sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: chain_rule.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.8 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
