|
(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(x0,x,(LAMBDA (t: T): f!1(t) - f!1(x0)))/(x-x0)))")
(("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) - Integral(x0!1, x!3, (LAMBDA (t: T): f!1(x0!1)))")
(("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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.109 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.
|
