|
(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
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.41Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
