| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 181 kB |
|
Quellcode-Bibliothek fundamental_theorem.prfSprache: 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 3603195158 ("" (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 3603195158 ("" (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 3603195158 ("" (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 (t: T): f!1(t) - f!1(x0)))") (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (case "(FORALL (x,x0: T): x /= x0 IMPLIES abs((F!1(x) - F!1(x0))/(x-x0) - f!1(x0)) = abs(Integral(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(x0!1, x!3, f!1) - Integr (("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) ((derivative_fun_alt formula-decl nil derivative_props 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]" fundamental_theorem nil) (T formal-nonempty-subtype-decl nil fundamental_theorem nil) (convergence const-decl "bool" lim_of_functions nil) (continuous? const-decl "bool" continuous_functions nil) (continuity_def formula-decl nil continuous_functions nil) (adh const-decl "setof[real]" convergence_functions nil) (not_one_element formula-decl nil fundamental_theorem nil) (bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil) (connected_domain formula-decl nil fundamental_theorem nil) (connected? const-decl "bool" deriv_domain_def nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (fullset const-decl "set" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (y!1 skolem-const-decl "T" fundamental_theorem nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (e!1 skolem-const-decl "posreal" fundamental_theorem nil) (x!1 skolem-const-decl "T" fundamental_theorem nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (f!1 skolem-const-decl "[T -> real]" fundamental_theorem nil) (x!2 skolem-const-decl "{yy: T | yy /= x!1}" fundamental_theorem nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (div_cancel2 formula-decl nil real_props nil) (minus_real_is_real application-judgement "real" reals nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (Integral_bounded formula-decl nil integral nil) (abs_div formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Integral const-decl "real" integral_def nil) (Integrable_funs type-eq-decl nil integral_def nil) (- const-decl "[numfield -> numfield]" number_fields nil) (const_continuous formula-decl nil continuous_functions nil) (convergence const-decl "bool" convergence_functions nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals 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" (inst - "x!1" "x!1+delta!1/2" "x!1 + e!1/2") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "continuous?") (("2" (inst -1 "x!1") (("2" (expand "continuous?") (("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 (t: T): f!1(t) - f!1(x0)))") (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (case "(FORALL (x,x0: T): x /= x0 IMPLIES abs((F!1(x) - F!1(x0))/(x-x0) - f!1(x0)) = abs(Integral(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) (("1" (name-replace "RX" "abs(Integral(x!1, x!2, LAMBDA (t: T): f!1(t) - f!1(x!1)))") (("1" (hide -2 -3 -4 -5 -6) (("1" (div-by 1 "abs(x!2 - x!1)") (("1" (div-by -1 "abs(x!2 - x!1)") (("1" (name-replace "ABS" "abs(x!2 - x!1)") (("1" (auto-rewrite-theory "real_props") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (grind) nil nil)) nil) ("3" (hide -1 2) (("3" (grind) nil nil)) nil)) nil)) nil) ("2" (reveal -6) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) 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" (reveal -3) (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (rewrite "not_one_element") nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (reveal -3) (("2" (inst?) (("2" (assert) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (reveal -8) (("3" (assert) (("3" (hide-all-but 1) (("3" (skosimp*) (("3" (rewrite "not_one_element") nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma "connected_domain") (("4" (propax) nil nil)) nil) ("5" (hide-all-but 1) (("5" (reveal -8) (("5" (inst?) (("5" (assert) nil nil)) nil)) nil)) nil) ("6" (hide-all-but 1) (("6" (grind) nil nil)) nil) ("7" (skosimp*) (("7" (rewrite "not_one_element") nil nil)) nil) ("8" (lemma "connected_domain") (("8" (propax) nil nil)) nil) ("9" (hide-all-but 1) (("9" (reveal -7) (("9" (inst?) (("9" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "not_one_element") 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(x0!1, x!3, f!1) - Integr (("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) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("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) ("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) ("3" (hide 3) (("3" (hide-all-but 1) (("3" (lemma "continuous_Integrable?[T]") (("3" (inst?) (("3" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (reveal -14) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 3) (("4" (hide-all-but 1) (("4" (lemma "continuous_Integrable?[T]") (("4" (inst?) (("4" (assert) (("4" (hide 2) (("4" (skosimp*) (("4" (reveal -14) (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "continuous_Integrable?[T]") (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (reveal -12) (("2" (inst?) 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" (hide-all-but 1) (("2" (skosimp*) (("2" (rewrite "not_one_element") nil 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" (skosimp*) (("2" (rewrite "not_one_element") nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (rewrite "not_one_element") nil nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (lemma "connected_domain") (("4" (inst?) (("4" (inst -1 "y!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((adh const-decl "setof[real]" convergence_functions 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) (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) (convergence const-decl "bool" convergence_functions nil)) nil)) (fundamental2_TCC1 0 (fundamental2_TCC1-1 nil 3603195158 ("" (skosimp*) (("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)) nil) ((deriv_domain formula-decl nil fundamental_theorem nil)) nil)) (fundamental2 0 (fundamental2-2 nil 3257699451 ("" (skosimp*) (("" (lemma "fundamental") (("" (name "xa" "choose({x: T | true})") (("1" (case "FORALL (x: T): Integrable?[T](xa, x, f!1)") (("1" (inst + "(LAMBDA (x: T): Integral(xa,x,f!1))") (("1" (inst - "(LAMBDA (x: T): Integral(xa,x,f!1))" "xa" "f!1") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (lemma "not_one_element") (("2" (inst?) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst?) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (lemma "not_one_element") (("2" (skosimp*) nil nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "continuous_Integrable?[T]") (("1" (skosimp*) (("1" (expand "continuous?" -2) (("1" (hide -1 -2 2 3 4) (("1" (expand "continuous?" -) (("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) ("3" (skosimp*) (("3" (rewrite "not_one_element") nil nil)) nil) ("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "epsilon({x: T | TRUE})") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fundamental formula-decl nil fundamental_theorem nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (pred type-eq-decl nil defined_types nil) (epsilon const-decl "T" epsilons nil) (Integrable? const-decl "bool" integral_def nil) (connected? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (not_one_element formula-decl nil fundamental_theorem nil) (connected_domain formula-decl nil fundamental_theorem nil) (Integrable_funs type-eq-decl nil integral_def nil) (Integral const-decl "real" integral_def nil) (f!1 skolem-const-decl "[T -> real]" fundamental_theorem nil) (xa skolem-const-decl "({x: T | TRUE})" fundamental_theorem nil) (continuous_Integrable? formula-decl nil integral nil) (continuous? const-decl "bool" continuous_functions 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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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]" fundamental_theorem nil) (T formal-nonempty-subtype-decl nil fundamental_theorem nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (TRUE const-decl "bool" booleans nil)) nil) (fundamental2-1 nil 3257692741 ("" (skosimp*) (("" (lemma "fundamental[T]") (("1" (name "xa" "choose({x: T | true})") (("1" (case "FORALL (x: T): Integrable?[T](xa, x, f!1)") (("1" (inst + "(LAMBDA (x: T): Integral(xa,x,f!1))") (("1" (inst - "(LAMBDA (x: T): Integral(xa,x,f!1))" "xa" "f!1") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (lemma "not_one_element") (("2" (inst?) nil nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "continuous_Integrable?[T]") (("2" (skosimp*) (("2" (expand "continuous?" -2) (("2" (hide -1 -2 2 3 4) (("2" (expand "continuous?" -) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "epsilon({x: T | TRUE})") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "open") (("2" (inst?) nil nil)) nil)) nil)) nil) ("3" (lemma "not_one_element") (("3" (propax) nil nil)) nil) ("4" (lemma "connected_domain") (("4" (propax) nil nil)) nil)) nil)) nil) ((continuous_Integrable? formula-decl nil integral nil) (Integral const-decl "real" integral_def nil) (Integrable_funs type-eq-decl nil integral_def nil) (Integrable? const-decl "bool" integral_def nil)) nil)) (fundamental3_TCC1 0 (fundamental3_TCC1-1 nil 3603195158 ("" (lemma "deriv_domain") (("" (propax) nil nil)) nil) ((deriv_domain formula-decl nil fundamental_theorem nil)) nil)) (fundamental3 0 (fundamental3-2 nil 3603195620 ("" (skosimp*) (("" (lemma "continuous_Integrable?[T]") (("1" (inst?) (("1" (split -1) (("1" (assert) (("1" (hide -1) (("1" (case "FORALL (x): Integrable?[T](a!1, x, f!1)") (("1" (case "derivable?[T](LAMBDA x: Integral[T](a!1, x, f!1))") (("1" (case "derivable?[T](LAMBDA x: Integral[T](a!1, x, f!1) - F!1(x))") (("1" (case "FORALL (xx: T): deriv((LAMBDA x: Integral(a!1, x, f!1) -F!1(x)),xx) = 0") (("1" (lemma "null_derivative[T]") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (hide -2) (("1" (case "EXISTS (c:real): (LAMBDA x: Integral(a!1, x, f!1)) = F!1+const_fun(c)") (("1" (skosimp*) (("1" (expand "+ ") (("1" (case "(LAMBDA x: Integral(a!1, x, f!1))(a!1) = (LAMBDA (x: T): const_fun(c!1)(x) + F!1(x))(a!1)" (("1" (hide -2) (("1" (assert) (("1" (expand "Integral" -1) (("1" (expand "const_fun") (("1" (reveal -1) (("1" (case "(LAMBDA x: Integral(a!1, x, f!1))(b!1) = (LAMBDA (x: T): const_fun(c!1)(x) + F!1(x))(b!1)" (("1" (hide -2) (("1" (assert) (("1" (expand "const_fun") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil) ("3" (skosimp*) (("3" (lemma "not_one_element") (("3" (propax) nil nil)) nil)) nil) ("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil) ("5" (hide-all-but 1) (("5" (reveal -5) (("5" (skosimp*) (("5" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) (("3" (lemma "not_one_element") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil) ("5" (hide-all-but 1) (("5" (reveal -5) (("5" (skosimp*) (("5" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "const_fun") (("2" (inst + "- F!1(a!1)") (("2" (expand "+ ") (("2" (apply-extensionality 1 :hide? t) (("1" (expand "constant?") (("1" (inst -1 "a!1" "x!1") (("1" (assert) (("1" (expand "Integral" -1 1) (("1" (assert) 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) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "deriv_diff_fun[T]") (("2" (expand "-") (("2" (inst -1 "(LAMBDA x: Integral(a!1, x, f!1))" "F!1") (("1" (assert) (("1" (case "deriv((LAMBDA x: Integral(a!1, x, f!1) - F!1(x)))(xx!1) = 0") (("1" (expand "deriv" -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (replace -1) (("2" (assert) (("2" (hide -1) (("2" (hide -3) (("2" (lemma "fundamental") (("2" (inst -1 "(LAMBDA x: Integral(a!1, x, f!1))" "a!1" "f!1") (("1" (assert) 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 -7) (("4" (propax) 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) ("3" (expand "derivable?" -1) (("3" (inst?) (("3" (lemma "deriv_domain") (("3" (propax) nil nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "derivable?" -1) (("4" (inst?) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "derivable_diff[T]") (("2" (expand "-") (("2" (inst -1 "(LAMBDA x: Integral[T](a!1, x, f!1))" "F!1") (("1" (lemma "not_one_element") (("1" (propax) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "fundamental") (("2" (inst -1 "(LAMBDA x: Integral(a!1, x, f!1))" "a!1" "f!1") (("1" (assert) nil nil) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (lemma "continuous_Integrable?[T]") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (expand "continuous?" -3) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (lemma "connected_domain") (("2" (skosimp*) (("2" (hide 2) (("2" (hide -1 -2 -3 -4) (("2" (expand "continuous?" -1) (("2" (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) ((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) (Closed_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (continuous? const-decl "bool" continuous_functions nil) (Integral const-decl "real" integral_def nil) (Integrable_funs type-eq-decl nil integral_def nil) (derivable? const-decl "bool" derivatives nil) (derivable_diff judgement-tcc nil derivatives nil) (deriv const-decl "real" derivatives_def nil) (derivable? const-decl "bool" derivatives_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (deriv_domain? const-decl "bool" deriv_domain_def nil) (a!1 skolem-const-decl "T" fundamental_theorem nil) (f!1 skolem-const-decl "[T -> real]" fundamental_theorem nil) (F!1 skolem-const-decl "[T -> real]" fundamental_theorem nil) (deriv_fun type-eq-decl nil derivatives nil) (constant? const-decl "bool" real_fun_preds "reals/") (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (not_one_element formula-decl nil fundamental_theorem nil) (connected_domain formula-decl nil fundamental_theorem nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (constant_seq1 application-judgement "(convergent?)" convergence_ops nil) (derivable_const application-judgement "deriv_fun" derivatives nil) (null_derivative formula-decl nil derivative_props nil) (deriv_diff_fun formula-decl nil derivatives nil) (deriv const-decl "[T -> real]" derivatives nil) (fundamental formula-decl nil fundamental_theorem nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (deriv_domain formula-decl nil fundamental_theorem nil) (real_minus_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) (Integrable? const-decl "bool" integral_def nil)) nil) (fundamental3-1 nil 3257692741 ("" (skosimp*) (("" (lemma "continuous_Integrable?[T]") (("1" (inst?) (("1" (split -1) (("1" (assert) (("1" (hide -1) (("1" (case "FORALL (x): Integrable?[T](a!1, x, f!1)") (("1" (case "derivable?[T](LAMBDA x: Integral[T](a!1, x, f!1))") (("1" (case "derivable?[T](LAMBDA x: Integral[T](a!1, x, f!1) - F!1(x))") (("1" (case "FORALL (xx: T): deriv((LAMBDA x: Integral(a!1, x, f!1) -F!1(x)),xx) = 0") (("1" (lemma "null_derivative[T]") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (hide -2) (("1" (case "EXISTS (c:real): (LAMBDA x: Integral(a!1, x, f!1)) = F!1+const_fun(c)") (("1" (skosimp*) (("1" (expand "+ ") (("1" (case "(LAMBDA x: Integral(a!1, x, f!1))(a!1) = (LAMBDA (x: T): const_fun(c!1)(x) + F!1(x))(a!1)" (("1" (hide -2) (("1" (assert) (("1" (expand "Integral" -1) (("1" (expand "const_fun") (("1" (reveal -1) (("1" (case "(LAMBDA x: Integral(a!1, x, f!1))(b!1) = (LAMBDA (x: T): const_fun(c!1)(x) + F!1(x))(b!1)" (("1" (hide -2) (("1" (assert) (("1" (expand "const_fun") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil) ("3" (skosimp*) (("3" (lemma "not_one_element") (("3" (inst?) nil nil)) nil)) nil) ("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil) ("5" (hide-all-but 1) (("5" (reveal -5) (("5" (skosimp*) (("5" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) (("3" (lemma "not_one_element") (("3" (assert) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil) ("5" (hide-all-but 1) (("5" (reveal -5) (("5" (skosimp*) (("5" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "const_fun") (("2" (inst + "- F!1(a!1)") (("2" (expand "+ ") (("2" (apply-extensionality 1 :hide? t) (("1" (expand "constant?") (("1" (inst -1 "a!1" "x!1") (("1" (assert) (("1" (expand "Integral" -1 1) (("1" (assert) 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) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil) ("2" (lemma "deriv_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "deriv_diff_fun") (("2" (expand "-") (("2" (inst -1 "(LAMBDA x: Integral(a!1, x, f!1))" "F!1") (("1" (assert) (("1" (case "deriv((LAMBDA x: Integral(a!1, x, f!1) - F!1(x)))(xx!1) = 0") (("1" (expand "deriv" -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (replace -1) (("2" (assert) (("2" (hide -1) (("2" (hide -3) (("2" (lemma "fundamental") (("2" (inst -1 "(LAMBDA x: Integral(a!1, x, f!1))" "a!1" "f!1") (("1" (assert) 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 -7) (("4" (propax) 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) ("3" (skosimp*) (("3" (expand "derivable?" -1) (("3" (inst?) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "derivable_diff") (("2" (expand "-") (("2" (inst -1 "(LAMBDA x: Integral[T](a!1, x, f!1))" "F!1") (("1" (lemma "not_one_element") (("1" (propax) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "fundamental") (("2" (inst -1 "(LAMBDA x: Integral(a!1, x, f!1))" "a!1" "f!1") (("1" (assert) nil nil) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (lemma "continuous_Integrable?[T]") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (expand "continuous?" -3) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (lemma "connected_domain") (("2" (skosimp*) (("2" (hide 2) (("2" (hide -1 -2 -3 -4) (("2" (expand "continuous?" -1) (("2" (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) ((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) (Closed_interval type-eq-decl nil intervals_real "reals/") (Integral const-decl "real" integral_def nil) (Integrable_funs type-eq-decl nil integral_def nil) (derivable? const-decl "bool" derivatives nil) (derivable_diff judgement-tcc nil derivatives nil) (deriv const-decl "real" derivatives_def nil) (derivable? const-decl "bool" derivatives_def nil) (deriv_fun type-eq-decl nil derivatives nil) (constant? const-decl "bool" real_fun_preds "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (constant_seq1 application-judgement "(convergent?)" convergence_ops nil) (null_derivative formula-decl nil derivative_props nil) (deriv_diff_fun formula-decl nil derivatives nil) (deriv const-decl "[T -> real]" derivatives nil) (Integrable? const-decl "bool" integral_def nil)) nil)) (derivable_Integrable? 0 (derivable_Integrable?-1 nil 3319993827 ("" (skosimp*) (("" (lemma "derivable_cont[T]") (("" (inst?) (("" (assert) (("" (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)) 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) (derivable_cont judgement-tcc nil derivatives nil) (connected_domain formula-decl nil fundamental_theorem nil) (not_one_element formula-decl nil fundamental_theorem 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/") (continuous? const-decl "bool" continuous_functions nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (connected? const-decl "bool" deriv_domain_def nil) (continuous_Integrable? formula-decl nil integral nil) (deriv_fun type-eq-decl nil derivatives nil) (bool nonempty-type-eq-decl nil booleans nil) (derivable? const-decl "bool" derivatives nil) (f!1 skolem-const-decl "[T -> real]" fundamental_theorem nil)) shostak)) (fundamental3b 0 (fundamental3b-1 nil 3393933425 ("" (skosimp*) (("" (lemma "fundamental3") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((fundamental3 formula-decl nil fundamental_theorem nil) (deriv const-decl "[T -> real]" derivatives nil) (deriv_fun type-eq-decl nil derivatives nil) (derivable? const-decl "bool" derivatives nil) (bool nonempty-type-eq-decl nil booleans 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)) shostak)))
¤ 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.0.133Bemerkung: (vorverarbeitet am 2026-04-26) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26