|
(integral_bounded
(IMP_integral_prep_TCC1 0
(IMP_integral_prep_TCC1-1 nil 3282561874
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil integral_bounded nil)) shostak))
(IMP_integral_prep_TCC2 0
(IMP_integral_prep_TCC2-1 nil 3282561874
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil integral_bounded nil)) shostak))
(int_to_bnd_TCC1 0
(int_to_bnd_TCC1-1 nil 3282561874
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(int_to_bnd_TCC2 0
(int_to_bnd_TCC2-1 nil 3282561874
("" (skosimp*) (("" (assert) nil nil)) nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(int_to_bnd 0
(int_to_bnd-2 nil 3477651374
("" (skosimp*)
((""
(case "(FORALL (eps: posreal):
(EXISTS (EP: partition[T](a!1,b!1)):
(FORALL (j: below(length(EP)-1)):
FORALL (xx: real): (EP(j) <= xx AND xx <= EP(j+1))
IMPLIES
abs(f!1(xx) - f!1(EP(j))) < eps/abs(EP(j+1) - EP(j)))))")
(("1" (assert)
(("1" (inst - "1000")
(("1" (skosimp*)
(("1" (inst + "EP!1")
(("1" (skosimp*)
(("1" (inst - "j!1")
(("1" (expand "bounded_on?")
(("1"
(inst +
"1000 / abs(EP!1`seq(1 + j!1) - EP!1`seq(j!1)) + abs(f!1(EP!1`seq(j!1)))")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert)
(("1" (lemma "abs_diff")
(("1"
(inst
-
"f!1(x!1)"
"f!1(EP!1`seq(j!1))")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "EP!1")
(("2" (inst - "j!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (assert)
(("2" (lemma "Lemma_1[T]")
(("2" (inst?)
(("2" (assert)
(("2" (inst -1 "eps!1")
(("2" (skosimp*)
(("2"
(name "EP"
"eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)")
(("1" (inst + "EP")
(("1" (skosimp*)
(("1" (case "T_pred(xx!1)")
(("1"
(case
"abs(EP`seq(1 + j!1) - EP`seq(j!1)) > 0")
(("1"
(cross-mult 1)
(("1"
(hide -1)
(("1"
(name
"SecJ"
"(EP`seq(1 + j!1) - EP`seq(j!1))")
(("1"
(name
"F_DIF"
"(f!1((EP)(j!1)) - f!1(xx!1))")
(("1"
(assert)
(("1"
(rewrite
"abs_mult"
:dir
rl)
(("1"
(case-replace
"EP`seq(1 + j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(xx!1) +
(EP`seq(j!1) * f!1(EP`seq(j!1))-
EP`seq(1 + j!1) * f!1(EP`seq(j!1))) = -SecJ*F_DIF")
(("1"
(hide -1)
(("1"
(lemma "abs_neg")
(("1"
(inst
-
"SecJ * F_DIF")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(inst
-
"EP"
"EP"
"gxis(a!1,b!1,EP,j!1,true,xx!1)"
"gxis(a!1,b!1,EP,j!1,false,xx!1)")
(("1"
(split -5)
(("1"
(expand
"Rie_sum")
(("1"
(assert)
(("1"
(assert)
(("1"
(rewrite
"sigma_minus[below[length(EP)-1]]")
(("1"
(case-replace
"(LAMBDA (i: below(length(EP) - 1)):
EP`seq(i) *
f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i))
+
EP`seq(1 + i) *
f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i))
-
EP`seq(i) *
f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i))
-
EP`seq(1 + i) *
f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i)))
= (LAMBDA (i: below(length(EP) - 1)):
IF i = j!1 THEN
(EP`seq(1 + j!1) - EP`seq(j!1)) * (f!1(EP(j!1)) - f!1(xx!1))
ELSE 0
ENDIF)")
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(case-replace
"EP`seq(1 + j!1) * f!1(EP`seq(j!1)) -
EP`seq(1 + j!1) * f!1(xx!1)
+
(EP`seq(j!1) * f!1(xx!1) -
EP`seq(j!1) * f!1(EP`seq(j!1)))
= SecJ*F_DIF")
(("1"
(hide
-1)
(("1"
(case
"j!1 < length(EP) - 2")
(("1"
(lemma
"sigma_below[length(EP)-1].sigma_split_ge")
(("1"
(inst
-
"_"
"length(EP) - 2"
"0"
"j!1")
(("1"
(assert)
(("1"
(inst?)
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(case-replace
"sigma(1 + j!1, length(EP) - 2,
(LAMBDA (i: below(length(EP) - 1)):
IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0")
(("1"
(hide
-1)
(("1"
(rewrite
"sigma_last_ge")
(("1"
(assert)
(("1"
(case
"sigma(0, j!1 - 1,
(LAMBDA (i: below(length(EP) - 1)):
IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0")
(("1"
(assert)
nil
nil)
("2"
(lemma
"sigma_restrict_eq[below(length(EP)-1)]")
(("2"
(inst?)
(("2"
(inst
-
"(LAMBDA (i: below(length(EP) - 1)): 0)")
(("2"
(expand
"restrict")
(("2"
(replace
-1)
(("2"
(hide
-1)
(("2"
(lemma
"sigma_const[below(length(EP)-1)]")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(lemma
"sigma_restrict_eq[below(length(EP)-1)]")
(("1"
(inst?)
(("1"
(inst
-
"(LAMBDA (i: below(length(EP) - 1)): 0)")
(("1"
(expand
"restrict")
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(lemma
"sigma_const[below(length(EP)-1)]")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"j!1 = length(EP) - 2")
(("1"
(rewrite
"sigma_last_ge")
(("1"
(case-replace
"sigma(0, length(EP) - 3,
(LAMBDA (i: below(length(EP) - 1)):
IF i = j!1 THEN SecJ * F_DIF ELSE 0 ENDIF)) = 0")
(("1"
(assert)
nil
nil)
("2"
(lemma
"sigma_restrict_eq[below(length(EP)-1)]")
(("1"
(inst?)
(("1"
(inst
-
"(LAMBDA (i: below(length(EP) - 1)): 0)")
(("1"
(expand
"restrict")
(("1"
(assert)
(("1"
(lemma
"sigma_const[below(length(EP)-1)]")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide
-1
2)
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(expand
"gxis")
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"gxis")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"N_from_delta")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil)
("3"
(lemma
"N_from_delta")
(("3"
(inst?)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(typepred "EP")
(("2"
(inst - "j!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma "connected_domain")
(("2"
(expand "connected?")
(("2"
(inst?)
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (case "(b!1 - a!1) / delta!1 > 0")
(("1" (assert) nil nil)
("2" (cross-mult 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp*)
(("3" (typepred "EP!1")
(("3" (inst - "j!1") (("3" (assert) nil nil)) nil)) nil))
nil))
nil)
("4" (hide 2)
(("4" (skosimp*)
(("4" (lemma "connected_domain")
(("4" (expand "connected?")
(("4" (inst - "_" "_" "xx!1")
(("4" (inst?)
(("4" (inst?) (("4" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(finseq type-eq-decl nil finite_sequences nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(partition type-eq-decl nil integral_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-subtype-decl nil integral_bounded nil)
(T_pred const-decl "[real -> boolean]" integral_bounded nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(a!1 skolem-const-decl "T" integral_bounded nil)
(b!1 skolem-const-decl "T" integral_bounded nil)
(EP!1 skolem-const-decl "partition[T](a!1, b!1)" integral_bounded
nil)
(j!1 skolem-const-decl "below(length(EP!1) - 1)" integral_bounded
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(abs_diff formula-decl nil abs_lems "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(bounded_on? const-decl "bool" integral_bounded nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Lemma_1 formula-decl nil integral_prep nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(j!1 skolem-const-decl "below(length(EP) - 1)" integral_bounded
nil)
(EP skolem-const-decl
"{fs: finite_sequence[{x | a!1 <= x AND x <= b!1}] |
length(fs) > 1 AND
seq(fs)(0) = a!1 AND
seq(fs)(length(fs) - 1) = b!1 AND
(FORALL (ii: below(length(fs) - 1)):
seq(fs)(ii) < seq(fs)(1 + ii))}" integral_bounded nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_real_is_real application-judgement "real" reals nil)
(abs_neg formula-decl nil abs_lems "reals/")
(FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(gxis const-decl "(xis?(a, b, P))" integral_prep nil)
(xis? const-decl "bool" integral_def nil)
(N_from_delta formula-decl nil integral_def nil)
(Rie_sum const-decl "real" integral_def nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(sigma_split_ge formula-decl nil sigma_below "reals/")
(sigma_restrict_eq formula-decl nil sigma "reals/")
(sigma_nat application-judgement "nat" sigma_below "reals/")
(sigma_const formula-decl nil sigma "reals/")
(int_times_even_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(restrict const-decl "[T -> real]" sigma "reals/")
(sigma_last_ge formula-decl nil sigma_below "reals/")
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sigma def-decl "real" sigma "reals/")
(int_below type-eq-decl nil sigma_below "reals/")
(sigma_minus formula-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(abs_mult formula-decl nil real_props nil)
(connected_domain formula-decl nil integral_bounded nil)
(connected? const-decl "bool" deriv_domain_def nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(integer nonempty-type-from-decl nil integers nil)
(eq_partition const-decl "partition(a, b)" integral_def nil)
(above nonempty-type-eq-decl nil integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(int_plus_int_is_int application-judgement "int" integers nil))
nil)
(int_to_bnd-1 nil 3282561219
("" (skosimp*)
((""
(case "(FORALL (eps: posreal):
(EXISTS (EP: partition[T](a!1,b!1)):
(FORALL (j: below(length(EP)-1)):
FORALL (xx: real): (EP(j) <= xx AND xx <= EP(j+1))
IMPLIES
abs(f!1(xx) - f!1(EP(j))) < eps/abs(EP(j+1) - EP(j)))))")
(("1" (assert)
(("1" (inst - "1000")
(("1" (skosimp*)
(("1" (inst + "EP!1")
(("1" (skosimp*)
(("1" (inst - "j!1")
(("1" (expand "bounded_on?")
(("1"
(inst +
"1000 / abs(EP!1`seq(1 + j!1) - EP!1`seq(j!1)) + abs(f!1(EP!1`seq(j!1)))")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert)
(("1" (lemma "abs_diff")
(("1"
(inst
-
"f!1(x!1)"
"f!1(EP!1`seq(j!1))")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "EP!1")
(("2" (inst - "j!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (assert)
(("2" (lemma "Lemma_1[T]")
(("2" (inst?)
(("2" (assert)
(("2" (inst -1 "eps!1")
(("2" (skosimp*)
(("2"
(name "EP"
"eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)")
(("1" (inst + "EP")
(("1" (skosimp*)
(("1" (case "T_pred(xx!1)")
(("1"
(case
"abs(EP`seq(1 + j!1) - EP`seq(j!1)) > 0")
(("1"
(cross-mult 1)
(("1"
(hide -1)
(("1"
(name
"SecJ"
"(EP`seq(1 + j!1) - EP`seq(j!1))")
(("1"
(name
"F_DIF"
"(f!1((EP)(j!1)) - f!1(xx!1))")
(("1"
(assert)
(("1"
(rewrite
"abs_mult"
:dir
rl)
(("1"
(case-replace
"EP`seq(1 + j!1) * f!1(xx!1) - EP`seq(j!1) * f!1(xx!1) +
(EP`seq(j!1) * f!1(EP`seq(j!1))-
EP`seq(1 + j!1) * f!1(EP`seq(j!1))) = -SecJ*F_DIF")
(("1"
(hide -1)
(("1"
(lemma "abs_neg")
(("1"
(inst
-
"SecJ * F_DIF")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(inst
-
"EP"
"EP"
"gxis(a!1,b!1,EP,j!1,true,xx!1)"
"gxis(a!1,b!1,EP,j!1,false,xx!1)")
(("1"
(split -5)
(("1"
(expand
"Rie_sum")
(("1"
(assert)
(("1"
(assert)
(("1"
(rewrite
"sigma_minus[below[length(EP)-1]]")
(("1"
(case-replace
"(LAMBDA (i: below(length(EP) - 1)):
EP`seq(i) *
f!1(gxis(a!1, b!1, EP, j!1, FALSE, xx!1)(i))
+
EP`seq(1 + i) *
f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i))
-
EP`seq(i) *
f!1(gxis(a!1, b!1, EP, j!1, TRUE, xx!1)(i))
-
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.66 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.
|
