|
(piecewise_continuous
(IMP_fundamental_theorem_TCC1 0
(IMP_fundamental_theorem_TCC1-1 nil 3612529043
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil piecewise_continuous nil)) nil))
(IMP_fundamental_theorem_TCC2 0
(IMP_fundamental_theorem_TCC2-1 nil 3612529043
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil piecewise_continuous nil)) nil))
(piecewise_continuous?_TCC1 0
(piecewise_continuous?_TCC1-1 nil 3611578171
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(piecewise_continuous?_TCC2 0
(piecewise_continuous?_TCC2-1 nil 3611578171
("" (skosimp*) (("" (assert) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(piecewise_continuous?_TCC3 0
(piecewise_continuous?_TCC3-1 nil 3611578171
("" (subtype-tcc) nil nil)
((strict_increasing? const-decl "bool" real_fun_preds "reals/")
(continuous_on? const-decl "bool" continuous_functions nil) nil
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(piecewise_continuous?_TCC4 0
(piecewise_continuous?_TCC4-1 nil 3611578171
("" (skeep) (("" (assert) nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(piecewise_continuous?_TCC5 0
(piecewise_continuous?_TCC5-1 nil 3611591182 ("" (grind) nil nil)
((strict_increasing? const-decl "bool" real_fun_preds "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(continuous_on? const-decl "bool" continuous_functions nil) nil
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(piecewise_continuous?_TCC6 0
(piecewise_continuous?_TCC6-1 nil 3611591182 ("" (grind) nil nil)
((strict_increasing? const-decl "bool" real_fun_preds "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(continuous_on? const-decl "bool" continuous_functions nil) nil
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(continuous_on_integrable 0
(continuous_on_integrable-1 nil 3611681282
("" (skosimp*)
(("" (lemma "unif_cont_interval[closed_interval(a!1,b!1)]")
(("1" (inst?)
(("1" (inst -1 "f!1")
(("1" (assert)
(("1" (expand "restrict")
(("1"
(case " continuous_on?(LAMBDA (s: closed_interval[T](a!1, b!1)): f!1(s),
{xx: closed_interval[T](a!1, b!1) | TRUE})")
(("1" (assert)
(("1" (hide -1)
(("1" (rewrite "step_to_integrable")
(("1" (skosimp*)
(("1" (expand "uniformly_continuous?")
(("1" (inst -1 "(eps!1/2)/(b!1-a!1)")
(("1" (skosimp*)
(("1"
(name
"PP"
"eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1)+2)")
(("1"
(case
"step_function?(a!1, b!1, fmin(a!1, b!1, PP, f!1))")
(("1"
(case
"step_function?(a!1, b!1, fmax(a!1, b!1, PP, f!1))")
(("1"
(inst
+
"fmin(a!1,b!1,PP,f!1)"
"fmax(a!1,b!1,PP,f!1)")
(("1"
(assert)
(("1"
(case
"integrable?(a!1, b!1, fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1))")
(("1"
(assert)
(("1"
(case
" integral(a!1, b!1, fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1)) < eps!1")
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(hide-all-but
(-7 1))
(("1"
(split 1)
(("1"
(typepred
"fmin(a!1, b!1, PP, f!1)")
(("1"
(lemma
"part_induction")
(("1"
(inst
-1
"(LAMBDA x: fmin(a!1, b!1, PP, f!1)(x) <= f!1(x))"
"a!1"
"b!1"
"PP"
"xx!1")
(("1"
(assert)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(assert)
(("1"
(inst
-
"ii!1")
(("1"
(inst
-
"xx!1")
(("1"
(flatten)
(("1"
(split
-4)
(("1"
(assert)
nil
nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(replace
-3)
(("2"
(hide
-3)
(("2"
(assert)
(("2"
(typepred
"min_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)")
(("2"
(hide
-1
-2
-3)
(("2"
(inst
-1
"xx!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"fmax(a!1, b!1, PP, f!1)")
(("2"
(lemma
"part_induction")
(("2"
(inst
-1
"(LAMBDA x: fmax(a!1, b!1, PP, f!1)(x) >= f!1(x))"
"a!1"
"b!1"
"PP"
"xx!1")
(("2"
(assert)
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(inst
-
"ii!1")
(("2"
(inst
-
"xx!1")
(("2"
(flatten)
(("2"
(split
-4)
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(replace
-3)
(("2"
(hide
-3)
(("2"
(typepred
"max_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)")
(("2"
(hide
-1
-2
-3)
(("2"
(inst
-
"xx!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"width_eq_part")
(("2"
(inst?)
(("2"
(assert)
(("2"
(replace -5)
(("2"
(case
"width(a!1,b!1,PP) < delta!1")
(("1"
(hide
-2
-6)
(("1"
(lemma
"integral_bound_abs")
(("1"
(inst
-1
"eps!1/(2*(b!1-a!1))"
"a!1"
"b!1"
"fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1)")
(("1"
(name-replace
"BMA"
"b!1-a!1")
(("1"
(assert)
(("1"
(split
-1)
(("1"
(name
"III"
"integral(a!1, b!1, fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1))")
(("1"
(case
"III >= 0")
(("1"
(replace
-2)
(("1"
(expand
"abs"
-3)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(expand
"-")
(("2"
(lemma
"part_induction")
(("2"
(inst
-1
"(LAMBDA x: (fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1))(x) <= eps!1 / (2 * BMA))"
"a!1"
"b!1"
"PP"
"x!1")
(("2"
(assert)
(("2"
(expand
"-")
(("2"
(case
"fmax(a!1, b!1, PP, f!1)(x!1) - fmin(a!1, b!1, PP, f!1)(x!1) >= 0")
(("1"
(expand
"abs"
1)
(("1"
(assert)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(typepred
"fmax(a!1, b!1, PP, f!1)")
(("1"
(typepred
"fmin(a!1, b!1, PP, f!1)")
(("1"
(inst
-1
"ii!1")
(("1"
(inst
-2
"ii!1")
(("1"
(inst
-1
"x!1")
(("1"
(inst
-2
"x!1")
(("1"
(flatten)
(("1"
(case
"(seq(PP)(ii!1) = x!1 OR x!1 = seq(PP)(1 + ii!1))")
(("1"
(assert)
(("1"
(split
-1)
(("1"
(assert)
(("1"
(hide
-2
-4)
(("1"
(replace
-2)
(("1"
(replace
-3)
(("1"
(assert)
(("1"
(hide-all-but
1)
(("1"
(reveal
-21)
(("1"
(mult-by
1
"(2*BMA)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide
-2
-4)
(("2"
(replace
-2)
(("2"
(replace
-3)
(("2"
(assert)
(("2"
(hide-all-but
1)
(("2"
(reveal
-21)
(("2"
(mult-by
1
"(2*BMA)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(hide
-2
-4)
(("2"
(replace
-1)
(("2"
(hide
-1)
(("2"
(replace
-1)
(("2"
(hide
-1)
(("2"
(name
"MIN_x"
"min_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)")
(("2"
(replace
-1)
(("2"
(name
"MAX_x"
"max_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)")
(("2"
(replace
-1)
(("2"
(case
"(FORALL (x,y: closed_interval(seq(PP)(ii!1),seq(PP)(ii!1+1))): abs(x-y) <= seq(PP)(1 + ii!1) - seq(PP)(ii!1))")
(("1"
(case
"abs(MAX_x - MIN_x) <= seq(PP)(1+ii!1) - seq(PP)(ii!1)")
(("1"
(inst
-12
"MAX_x"
"MIN_x")
(("1"
(assert)
(("1"
(lemma
"width_lem")
(("1"
(expand
"finseq_appl")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(ground)
nil
nil)
("3"
(ground)
nil
nil))
nil)
("2"
(assert)
(("2"
(hide-all-but
(-2
-3
-16
1))
(("2"
(typepred
"MAX_x")
(("2"
(typepred
"MIN_x")
(("2"
(hide
-1
-4
-5
-8
-9
-10)
(("2"
(expand
"abs")
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide-all-but
1)
(("2"
(skeep)
(("2"
(typepred
"x")
(("2"
(typepred
"y")
(("2"
(expand
"abs")
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(rewrite
"fmax_ge")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.63 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.
|
