| products/Sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: integral_chg_var.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(integral_chg_var
(deriv_domain_T 0 (deriv_domain_T-1 nil 3472399896 ("" (expand "deriv_domain?") (("" (skosimp*) (("" (lemma "connected_domain") (("" (expand "connected?") (("" (lemma "connected_deriv_domain[T]") (("" (expand "connected?") (("" (expand "not_one_element?") (("" (expand "deriv_domain?") (("" (replace -2) (("" (lemma not_one_element) (("" (expand "not_one_element?") (("" (replace -1) (("" (hide -1) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((connected? const-decl "bool" deriv_domain_def nil) (not_one_element formula-decl nil integral_chg_var 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) (not_one_element? const-decl "bool" deriv_domain_def nil) (connected_deriv_domain formula-decl nil deriv_domain_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]" integral_chg_var nil) (T formal-nonempty-subtype-decl nil integral_chg_var nil) (connected_domain formula-decl nil integral_chg_var nil) (deriv_domain? const-decl "bool" deriv_domain_def nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (deriv_domain_U 0 (deriv_domain_U-1 nil 3472399927 ("" (expand "deriv_domain?") (("" (skosimp*) (("" (lemma "con_dom_U") (("" (lemma "connected_deriv_domain[U]") (("" (lemma not_one_U) (("" (assert) (("" (expand "deriv_domain?") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((U formal-nonempty-subtype-decl nil integral_chg_var nil) (U_pred const-decl "[real -> boolean]" integral_chg_var 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) (connected_deriv_domain formula-decl nil deriv_domain_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) (not_one_U formula-decl nil integral_chg_var nil) (con_dom_U formula-decl nil integral_chg_var nil) (deriv_domain? const-decl "bool" deriv_domain_def nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (int_chg_var_prep_TCC1 0 (int_chg_var_prep_TCC1-1 nil 3313937110 ("" (skosimp*) (("" (lemma "con_dom_U") (("" (lemma "deriv_domain_U") (("" (propax) nil nil)) nil)) nil)) nil) ((con_dom_U formula-decl nil integral_chg_var nil) (deriv_domain_U formula-decl nil integral_chg_var nil)) nil)) (int_chg_var_prep_TCC2 0 (int_chg_var_prep_TCC2-1 nil 3313937110 ("" (lemma "not_one_U") (("" (expand "not_one_element?") (("" (skosimp*) nil nil)) nil)) nil) ((not_one_element? const-decl "bool" deriv_domain_def nil) (not_one_U formula-decl nil integral_chg_var nil)) nil)) (int_chg_var_prep_TCC3 0 (int_chg_var_prep_TCC3-1 nil 3471608937 ("" (skosimp*) (("" (hide -1 -2 -3 -4) (("" (lemma "con_dom_U") (("" (inst - x!1 y!1 z!1) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((con_dom_U formula-decl nil integral_chg_var nil)) nil)) (int_chg_var_prep 0 (int_chg_var_prep-1 nil 3313937160 ("" (skosimp*) (("" (lemma "cont_fun_Integrable?[U]") (("1" (inst?) (("1" (assert) (("1" (case-replace "(LAMBDA (u: U): f!1(phi!1(u)) * deriv[U](phi!1)(u)) = (f!1 o phi!1) * deriv[U](phi!1)") (("1" (hide -1) (("1" (lemma "composition_cont_fun[U,T]") (("1" (inst - "phi!1" "f!1") (("1" (assert) (("1" (lemma "derivable_cont_fun[U]") (("1" (inst - "phi!1") (("1" (assert) (("1" (lemma "prod_fun_continuous[U]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "o ") (("2" (assert) (("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_U") (("2" (propax) nil nil)) nil) ("3" (lemma "con_dom_U") (("3" (expand "connected?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((U formal-nonempty-subtype-decl nil integral_chg_var nil) (U_pred const-decl "[real -> boolean]" integral_chg_var 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) (cont_fun_Integrable? formula-decl nil integral nil) (connected? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (bool nonempty-type-eq-decl nil booleans nil) (derivable_cont_fun formula-decl nil derivatives nil) (continuous_fun nonempty-type-eq-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (prod_fun_continuous judgement-tcc nil continuous_functions nil) (composition_cont_fun formula-decl nil composition_continuous nil) (O const-decl "T3" function_props nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (deriv const-decl "[T -> real]" derivatives nil) (deriv_fun type-eq-decl nil derivatives nil) (derivable? const-decl "bool" derivatives nil) (T formal-nonempty-subtype-decl nil integral_chg_var nil) (T_pred const-decl "[real -> boolean]" integral_chg_var nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (not_one_U formula-decl nil integral_chg_var nil) (con_dom_U formula-decl nil integral_chg_var nil)) nil)) (Int_chg_var_TCC1 0 (Int_chg_var_TCC1-1 nil 3319990294 ("" (lemma "deriv_domain_U") (("" (propax) nil nil)) nil) ((deriv_domain_U formula-decl nil integral_chg_var nil)) nil)) (Int_chg_var_TCC2 0 (Int_chg_var_TCC2-1 nil 3319990294 ("" (skosimp*) (("" (lemma "not_one_U") (("" (expand "not_one_element?") (("" (inst?) nil nil)) nil)) nil)) nil) ((not_one_U formula-decl nil integral_chg_var nil)) nil)) (Int_chg_var_TCC3 0 (Int_chg_var_TCC3-2 "" 3319993700 ("" (skosimp*) (("" (lemma "continuous_Integrable?[T]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "continuous?" -1) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (expand "connected?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral_chg_var nil) (T_pred const-decl "[real -> boolean]" integral_chg_var 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) (continuous_Integrable? formula-decl nil integral nil) (connected? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (bool nonempty-type-eq-decl nil booleans nil) (continuous? const-decl "bool" continuous_functions nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (U formal-nonempty-subtype-decl nil integral_chg_var nil) (U_pred const-decl "[real -> boolean]" integral_chg_var nil) (not_one_element formula-decl nil integral_chg_var nil) (connected_domain formula-decl nil integral_chg_var nil)) shostak) (Int_chg_var_TCC3-1 nil 3319990294 ("" (subtype-tcc) nil nil) nil nil)) (Int_chg_var_TCC4 0 (Int_chg_var_TCC4-1 nil 3319990294 ("" (lemma "connected_domain") (("" (skosimp*) nil nil)) nil) ((connected_domain formula-decl nil integral_chg_var nil)) nil)) (Int_chg_var_TCC5 0 (Int_chg_var_TCC5-1 nil 3319990294 ("" (lemma "not_one_element") (("" (skosimp*) nil nil)) nil) ((not_one_element formula-decl nil integral_chg_var nil)) nil)) (Int_chg_var_TCC6 0 (Int_chg_var_TCC6-2 nil 3319998251 ("" (skosimp*) (("" (lemma "int_chg_var_prep") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((int_chg_var_prep formula-decl nil integral_chg_var nil) (real_times_real_is_real application-judgement "real" reals nil) (T formal-nonempty-subtype-decl nil integral_chg_var nil) (T_pred const-decl "[real -> boolean]" integral_chg_var nil) (U formal-nonempty-subtype-decl nil integral_chg_var nil) (U_pred const-decl "[real -> boolean]" integral_chg_var 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) (Int_chg_var_TCC6-1 nil 3319990294 ("" (skosimp*) (("" (lemma "continuous_Integrable?[U]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil) nil nil)) (Int_chg_var_TCC7 0 (Int_chg_var_TCC7-1 nil 3471608937 ("" (skosimp*) (("" (lemma "con_dom_U") (("" (inst - x!1 y!1 z!1) (("" (assert) nil nil)) nil)) nil)) nil) ((con_dom_U formula-decl nil integral_chg_var nil)) nil)) (Int_chg_var 0 (Int_chg_var-1 nil 3319990307 ("" (skosimp*) (("" (lemma "fundamental[T]") (("1" (inst - "(LAMBDA (y: T): Integral(phi!1(a!1),y,f!1))" "phi!1(a!1)" "f!1") (("1" (name "FF" "(LAMBDA (y: T): Integral(phi!1(a!1),y,f!1))") (("1" (replace -1) (("1" (assert) (("1" (flatten) (("1" (name "GG" "FF o phi!1") (("1" (case "(LAMBDA (x:U): Integral(phi!1(a!1), phi!1(x), f!1)) = GG") (("1" (lemma "composition_derivable_fun[U,T]") (("1" (inst - "phi!1" "FF") (("1" (assert) (("1" (replace -3) (("1" (lemma "deriv_comp_fun[U,T]") (("1" (inst - "phi!1" "FF") (("1" (replace -4) (("1" (replace -7) (("1" (case-replace "Integral(phi!1(a!1), phi!1(b!1), f!1) = GG(b!1)") (("1" (lemma "fundamental3[U]") (("1" (inst - "GG" "a!1" "b!1" "(f!1 o phi!1) * deriv(phi!1)") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (case-replace "(LAMBDA (u: U): f!1(phi!1(u)) * deriv(phi!1)(u)) = (f!1 o phi!1) * deriv(phi!1) (("1" (replace -3) (("1" (case-replace "GG(a!1) = 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (replace -7 + rl) (("2" (assert) (("2" (rewrite "Integral_a_to_a[T]") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "o ") (("2" (assert) (("2" (expand "*") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "int_chg_var_prep") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "con_dom_U") (("2" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (replace -3 + rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (lemma "not_one_U") (("2" (lemma "deriv_domain_T") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (lemma "con_dom_U") (("3" (lemma not_one_U) (("3" (propax) nil nil)) nil)) nil) ("4" (lemma "deriv_domain_U") (("4" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1 + rl) (("2" (hide -1) (("2" (replace -1 + rl) (("2" (hide -1) (("2" (expand "o ") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (lemma "cont_fun_Integrable?[T]") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (skosimp*) (("2" (lemma "cont_fun_Integrable?[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (lemma "cont_fun_Integrable?[T]") (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral_chg_var nil) (T_pred const-decl "[real -> boolean]" integral_chg_var 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) (fundamental formula-decl nil fundamental_theorem nil) (connected? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_times_real_is_real application-judgement "real" reals nil) (O const-decl "T3" function_props nil) (cont_fun_Integrable? formula-decl nil integral nil) (composition_derivable_fun formula-decl nil chain_rule nil) (deriv_domain? const-decl "bool" deriv_domain_def nil) (deriv_comp_fun formula-decl nil chain_rule nil) (con_dom_U formula-decl nil integral_chg_var nil) (deriv const-decl "[T -> real]" derivatives nil) (deriv_fun type-eq-decl nil derivatives nil) (* 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) (real_minus_real_is_real application-judgement "real" reals nil) (Integral_a_to_a formula-decl nil integral nil) (int_chg_var_prep formula-decl nil integral_chg_var nil) (fundamental3 formula-decl nil fundamental_theorem nil) (derivable? const-decl "bool" derivatives nil) (not_one_U formula-decl nil integral_chg_var nil) (deriv_domain_T formula-decl nil integral_chg_var nil) (not_one_element formula-decl nil integral_chg_var nil) (deriv_domain_U formula-decl nil integral_chg_var nil) (connected_domain formula-decl nil integral_chg_var nil) (Integral const-decl "real" integral_def nil) (Integrable_funs type-eq-decl nil integral_def nil) (Integrable? const-decl "bool" integral_def nil) (U_pred const-decl "[real -> boolean]" integral_chg_var nil) (U formal-nonempty-subtype-decl nil integral_chg_var nil) (phi!1 skolem-const-decl "[U -> T]" integral_chg_var nil) (a!1 skolem-const-decl "U" integral_chg_var nil) (f!1 skolem-const-decl "[T -> real]" integral_chg_var nil)) nil)) (int_chg_var_TCC1 0 (int_chg_var_TCC1-1 nil 3319990512 ("" (skosimp*) (("" (lemma "continuous_Integrable?[T]") (("1" (inst - "phi!1(a!1)" "phi!1(b!1)" "f!1") (("1" (assert) (("1" (expand "Integrable?") (("1" (skosimp*) (("1" (expand "continuous?" -3) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (expand "connected?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral_chg_var nil) (T_pred const-decl "[real -> boolean]" integral_chg_var 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) (continuous_Integrable? formula-decl nil integral nil) (connected? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (bool nonempty-type-eq-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (continuous? const-decl "bool" continuous_functions nil) (Integrable? const-decl "bool" integral_def nil) (U formal-nonempty-subtype-decl nil integral_chg_var nil) (U_pred const-decl "[real -> boolean]" integral_chg_var nil) (not_one_element formula-decl nil integral_chg_var nil) (connected_domain formula-decl nil integral_chg_var nil)) nil)) (int_chg_var_TCC2 0 (int_chg_var_TCC2-2 nil 3319998518 ("" (skosimp*) (("" (lemma "int_chg_var_prep") (("" (inst?) (("" (assert) (("" (inst - "a!1" "b!1") (("" (flatten) (("" (expand "Integrable?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_chg_var_prep formula-decl nil integral_chg_var nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Integrable? const-decl "bool" integral_def nil) (U formal-nonempty-subtype-decl nil integral_chg_var nil) (U_pred const-decl "[real -> boolean]" integral_chg_var nil) (T formal-nonempty-subtype-decl nil integral_chg_var nil) (T_pred const-decl "[real -> boolean]" integral_chg_var 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) (int_chg_var_TCC2-1 nil 3319990512 ("" (subtype-tcc) nil nil) nil nil)) (int_chg_var 0 (int_chg_var-1 nil 3313940293 ("" (skosimp*) (("" (lemma "Int_chg_var") (("" (inst?) (("" (inst - "b!1" "_") (("" (inst?) (("" (assert) (("" (expand "Integral") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Int_chg_var formula-decl nil integral_chg_var nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Integral const-decl "real" integral_def nil) (T formal-nonempty-subtype-decl nil integral_chg_var nil) (T_pred const-decl "[real -> boolean]" integral_chg_var nil) (U formal-nonempty-subtype-decl nil integral_chg_var nil) (U_pred const-decl "[real -> boolean]" integral_chg_var 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)) shostak))) ¤ Dauer der Verarbeitung: 0.37 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 |
