| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis_ax/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 156 kB |
|
Quelle fundamental_theorem.prf Sprache: Lisp |
|||||||||
|
(fundamental_theorem
(deriv_domain 0 (deriv_domain-2 nil 3472399705 ("" (lemma "connected_domain") (("" (lemma "connected_deriv_domain[T]") (("" (lemma not_one_element) (("" (assert) nil nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil fundamental_theorem nil) (T_pred const-decl "[real -> boolean]" fundamental_theorem 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) (not_one_element formula-decl nil fundamental_theorem nil) (connected_domain formula-decl nil fundamental_theorem nil)) nil) (deriv_domain-1 nil 3471610571 ("" (skosimp*) (("" (lemma "connected_domain") (("" (lemma "connected_deriv_domain[T]") (("1" (replace -2) (("1" (inst?) nil nil)) nil) ("2" (lemma not_one_element) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) nil shostak)) (IMP_derivative_props_TCC1 0 (IMP_derivative_props_TCC1-1 nil 3610702394 ("" (lemma "connected_domain") (("" (propax) nil nil)) nil) ((connected_domain formula-decl nil fundamental_theorem nil)) nil)) (IMP_derivative_props_TCC2 0 (IMP_derivative_props_TCC2-1 nil 3610702394 ("" (lemma "not_one_element") (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil fundamental_theorem nil)) nil)) (fundamental_TCC1 0 (fundamental_TCC1-1 nil 3257699428 ("" (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" (propax) nil nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil fundamental_theorem nil) (T_pred const-decl "[real -> boolean]" fundamental_theorem 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/") (not_one_element formula-decl nil fundamental_theorem nil) (connected_domain formula-decl nil fundamental_theorem nil)) shostak)) (fundamental_TCC2 0 (fundamental_TCC2-1 nil 3610702232 ("" (skosimp*) (("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)) nil) ((deriv_domain formula-decl nil fundamental_theorem nil)) nil)) (fundamental 0 (fundamental-2 nil 3257787730 ("" (skosimp*) (("" (rewrite "derivative_fun_alt") (("" (skosimp*) (("" (expand "convergence") (("" (expand "convergence") (("" (prop) (("1" (hide -2) (("1" (expand "continuous?") (("1" (inst?) (("1" (rewrite continuity_def) (("1" (expand "convergence") (("1" (expand "convergence") (("1" (flatten) (("1" (hide -2) (("1" (hide -1) (("1" (expand "adh") (("1" (skosimp*) (("1" (lemma "not_one_element") (("1" (expand "not_one_element?") (("1" (inst -1 "x!1") (("1" (skosimp*) (("1" (case "x!1 <= y!1") (("1" (inst + "min(y!1,x!1+e!1/2)") (("1" (grind) nil nil) ("2" (expand "min") (("2" (ground) (("1" (lemma "connected_domain") (("1" (expand "connected?") (("1" (inst -1 "x!1" "y!1" "x!1 + e!1 / 2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "max(y!1,x!1-e!1/2)") (("1" (grind) nil nil) ("2" (expand "max") (("2" (ground) (("1" (lemma "connected_domain") (("1" (expand "connected?") (("1" (inst -1 "y!1" "x!1" "x!1 - e!1 / 2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "continuous?") (("2" (inst -1 "x!1") (("2" (rewrite continuity_def) (("2" (expand "convergence") (("2" (expand "convergence") (("2" (flatten) (("2" (inst -2 "epsilon!1/2") (("2" (skosimp*) (("2" (case "FORALL (x, x0: T): x /= x0 IMPLIES Integrable?[T](x0, x, (LAMBDA (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (case "(FORALL (x,x0: T): x /= x0 IMPLIES abs((F!1(x) - F!1(x0))/(x- (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (rewrite "abs_div") (("1" (mult-by 1 "abs(x!2 - x!1)") (("1" (inst -4 "x!2") (("1" (assert) (("1" (lemma "Integral_bounded[T]") (("1" (inst?) (("1" (assert) (("1" (inst -1 "epsilon!1/2") (("1" (split -1) (("1" (assert) nil nil) ("2" (reveal -6) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (reveal -3) (("3" (hide 2) (("3" (inst -1 "x!3") (("3" (assert) (("3" (hide -3 -4 2) (("3" (hide -3) (("3" (expand "fullset") (("3" (typepred "x!3") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) 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)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (hide-all-but 1) (("4" (reveal -8) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (lemma "not_one_element") (("5" (propax) nil nil)) nil) ("6" (lemma "connected_domain") (("6" (propax) nil nil)) nil) ("7" (hide-all-but 1) (("7" (reveal -7) (("7" (inst?) (("7" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (reveal -6) (("2" (inst?) (("2" (assert) (("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil) ("4" (hide-all-but 1) (("4" (reveal -6) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (hide -1 -2 -3 -4 -5) (("2" (inst-cp -1 "x!3") (("2" (inst -1 "x0!1") (("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "Integral_split[T]") (("1" (inst -1 "x0!1" "a!1" "x!3" "f!1") (("1" (split -1) (("1" (flatten) (("1" (case-replace "Integral(x0!1, a!1, f!1) = -Integral(a!1,x0!1, f!1)") (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (case-replace "Integral(x0!1, x!3, (LAMBDA (t: T): f!1(t) - f!1(x0!1))) = Integral (("1" (hide -1 -2 -3) (("1" (lemma "Integral_const_fun[T]") (("1" (inst?) (("1" (name-replace "MTT" "(x!3 - x0!1)") (("1" (expand "const_fun") (("1" (inst?) (("1" (flatten) (("1" (replace -2) (("1" (assert) (("1" (hide -1 -2) (("1" (name-replace "II" "Integral(x0!1, x!3, f!1)") (("1" (reveal -5) (("1" (case-replace "(II - f!1(x0!1) * MTT) / MTT = II/MTT - f!1(x0!1) ") (("1" (hide 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (lemma "Integral_diff[T]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (lemma "Integral_const_fun[T]") (("2" (expand "const_fun") (("2" (inst?) (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "Integral_const_fun[T]") (("3" (expand "const_fun") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (reveal -8) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "Integral_rev[T]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (reveal -14) (("2" (lemma "continuous_Integrable?[T]") (("2" (inst?) (("2" (split -1) (("1" (propax) nil nil) ("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (hide-all-but 1) (("2" (lemma "continuous_Integrable?[T]") (("2" (inst?) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lemma "continuous_Integrable?[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (lemma "continuous_Integrable?[T]") (("2" (inst?) (("2" (assert) (("2" (reveal -12) (("2" (reveal -13) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 3) (("3" (lemma "continuous_Integrable?[T]") (("3" (inst?) (("3" (assert) (("3" (skosimp*) (("3" (reveal -12) (("3" (inst?) nil 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (hide -1 -2 -3) (("2" (reveal -5) (("2" (lemma "Integral_diff[T]") (("1" (inst?) (("1" (assert) (("1" (hide 3) (("1" (prop) (("1" (lemma "continuous_Integrable?[T]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "continuous_Integrable?[T]") (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (assert) (("2" (hide-all-but 1) (("2" (lemma "const_continuous[T]") (("2" (expand "const_fun") (("2" (inst?) nil nil)) nil)) nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "not_one_element") (("3" (skosimp*) nil nil)) nil) ("4" (skosimp*) (("4" (lemma "connected_domain") (("4" (propax) nil nil)) nil)) nil)) nil)) 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? const-decl "bool" deriv_domain_def nil) (Integrable? const-decl "bool" integral_def nil) (continuous_Integrable? formula-decl nil integral nil) (Integral_rev formula-decl nil integral nil) (Integral_diff formula-decl nil integral nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (Integral_const_fun formula-decl nil integral nil) (Integral_split formula-decl nil integral nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (Integral_bounded formula-decl nil integral nil) (Integral const-decl "real" integral_def nil) (Integrable_funs type-eq-decl nil integral_def nil) (const_continuous formula-decl nil continuous_functions nil)) nil) (fundamental-1 nil 3257698051 ("" (skosimp*) (("" (rewrite "derivative_fun_alt") (("" (skosimp*) (("" (expand "convergence") (("" (expand "convergence") (("" (prop) (("1" (hide -1 -2) (("1" (lemma "open") (("1" (inst?) (("1" (skosimp*) (("1" (expand "adh") (("1" (skosimp*) (("1" (inst -1 "x!1 + delta!1/2") (("1" (split -1) (("1" (case "delta!1/2 < e!1") (("1" (inst + "x!1 + delta!1/2") (("1" (expand "fullset") (("1" (grind) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst + "x!1+e!1/2") (("1" (expand "fullset") (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.33 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28