| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis_ax/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quellcode-Bibliothek integral_cont.prf Sprache: unbekannt |
||||||
|
(integral_cont (IMP_integral_cont_scaf_TCC1 0 (IMP_integral_cont_scaf_TCC1-1 nil 3292324347 ("" (skosimp*) (("" (lemma "connected_domain") (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil integral_cont nil)) shostak)) (IMP_integral_cont_scaf_TCC2 0 (IMP_integral_cont_scaf_TCC2-1 nil 3292324347 ("" (skosimp*) (("" (rewrite "not_one_element") nil nil)) nil) ((not_one_element formula-decl nil integral_cont nil)) shostak)) (in_interval_TCC1 0 (in_interval_TCC1-1 nil 3262523543 ("" (subtype-tcc) nil nil) nil nil)) (in_interval_TCC2 0 (in_interval_TCC2-1 nil 3262523543 ("" (subtype-tcc) nil nil) nil nil)) (in_interval 0 (in_interval-1 nil 3262523543 ("" (skosimp*) (("" (typepred "x!1") (("" (typepred "y!1") (("" (expand "abs") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) 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) (>= 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) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_cont nil) (T_pred const-decl "[real -> boolean]" integral_cont 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (continuous_integrable 0 (continuous_integrable-3 nil 3477657179 ("" (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 + (("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" (lemma "in_interval") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (lemma "in_interval") (("2" (skosimp*) (("2" (inst?) 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)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 -4 -6 -8 2) (("2" (replace -1) (("2" (hide -1 -2 -3) (("2" (name-replace "BMA" "b!1-a!1") (("2" (mult-by 1 "(1 + floor(BMA / delta!1))") (("1" (div-by 1 "delta!1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (reveal -3) (("2" (assert) (("2" (case-replace "BMA / delta!1 >= 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (mult-by 1 "delta!1") (("2" (assert) (("2" (reveal -4) (("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) ("2" (hide 2) (("2" (lemma "integral_diff") (("2" (inst -1 "a!1" "b!1" "fmax(a!1, b!1, PP, f!1)" "fmin(a!1, b!1, PP, f!1)") (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (assert) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "step_function_integrable?") nil nil)) nil) ("3" (hide 2) (("3" (rewrite "step_function_integrable?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "fmax_step") nil nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "fmin_step") nil nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (hide -1 -2 -3) (("3" (inst?) (("3" (lemma "cont_restrict") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (case "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (mult-by 1 "delta!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (mult-by 1 "b!1-a!1") (("1" (assert) nil nil)) nil) ("2" (mult-by 1 "b!1-a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (rewrite "continuous_on_def") (("2" (skosimp*) (("2" (inst -2 "y!1") (("2" (rewrite "continuity_def") (("2" (expand "convergence") (("2" (expand "convergence") (("2" (flatten) (("2" (expand "extend") (("2" (expand "adh") (("2" (split +) (("1" (skosimp*) (("1" (inst + "y!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -3 "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (assert) (("2" (inst -4 "x!1") (("2" (expand "fullset") (("2" (propax) 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" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (typepred "x!1") (("2" (inst-cp 1 "a!1") (("2" (inst-cp 1 "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (expand "connected?") (("3" (assert) (("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (expand "connected?") (("3" (inst -1 "a!1" "b!1" "z!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil integral_cont nil) (T_pred const-decl "[real -> boolean]" integral_cont 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) (unif_cont_interval formula-decl nil unif_cont_fun nil) (connected? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (restrict const-decl "R" restrict nil) (continuity_def formula-decl nil continuous_functions nil) (extend const-decl "R" extend nil) (abs_0 formula-decl nil abs_lems "reals/") (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions nil) (convergence const-decl "bool" convergence_functions nil) (convergence const-decl "bool" lim_of_functions nil) (continuous_on_def formula-decl nil continuous_functions nil) (step_to_integrable formula-decl nil integral_step nil) (real_minus_real_is_real application-judgement "real" reals nil) (uniformly_continuous? const-decl "bool" unif_cont_fun nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (step_function? const-decl "bool" step_fun_def nil) (continuous? const-decl "bool" continuous_functions nil) (fun_cont_on type-eq-decl nil integral_cont_scaf nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (fun_cont_on type-eq-decl nil interval_minmax nil) (min_x const-decl "{mx: T | a <= mx AND mx <= b AND (FORALL (x: T): a <= x AND x <= b IMPLIES f(mx) <= f(x))}" interval_minmax nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (fmin const-decl "{ff: [T -> real] | LET xx = seq(P) IN FORALL (ii: below(length(P) - 1)): FORALL (x: T): (xx(ii) < x AND x < xx(ii + 1) IMPLIES ff(x) = f(min_x(xx(ii), xx(ii + 1), f))) AND ((xx(ii) = x OR x = xx(ii + 1)) IMPLIES ff(x) = f(x))}" integral_cont_scaf nil) (fmax_step formula-decl nil integral_cont_scaf nil) (integrable? const-decl "bool" integral_def nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (integral? const-decl "bool" integral_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (part_induction formula-decl nil integral_def nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (width_eq_part formula-decl nil integral_def nil) (width const-decl "posreal" integral_def nil) (integral_bound_abs formula-decl nil integral_prep nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (BMA skolem-const-decl "real" integral_cont nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (finite_sequence type-eq-decl nil finite_sequences nil) (partition type-eq-decl nil integral_def nil) (in_interval formula-decl nil integral_cont nil) (PP 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_cont nil) (ii!1 skolem-const-decl "below(length(PP) - 1)" integral_cont nil) (f!1 skolem-const-decl "[T -> real]" integral_cont nil) (MAX_x skolem-const-decl "{mx: T | seq(PP)(ii!1) <= mx AND mx <= seq(PP)(1 + ii!1) AND (FORALL (x: T): seq(PP)(ii!1) <= x AND x <= seq(PP)(1 + ii!1) IMPLIES f!1(mx) >= f!1(x))}" integral_cont nil) (MIN_x skolem-const-decl "{mx: T | seq(PP)(ii!1) <= mx AND mx <= seq(PP)(1 + ii!1) AND (FORALL (x: T): seq(PP)(ii!1) <= x AND x <= seq(PP)(1 + ii!1) IMPLIES f!1(mx) <= f!1(x))}" integral_cont nil) (width_lem formula-decl nil integral_def nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (fmax_ge formula-decl nil integral_cont_scaf nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (BMA skolem-const-decl "real" integral_cont nil) (delta!1 skolem-const-decl "posreal" integral_cont nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (integral_diff formula-decl nil integral_prep nil) (step_function_integrable? formula-decl nil integral_step nil) (fmax const-decl "{ff: [T -> real] | LET xx = seq(P) IN FORALL (ii: below(length(P) - 1)): FORALL (x: T): (xx(ii) < x AND x < xx(ii + 1) IMPLIES ff(x) = f(max_x(xx(ii), xx(ii + 1), f))) AND ((xx(ii) = x OR x = xx(ii + 1)) IMPLIES ff(x) = f(x))}" integral_cont_scaf nil) (max_x const-decl "{mx: T | a <= mx AND mx <= b AND (FORALL (x: T): a <= x AND x <= b IMPLIES f(mx) >= f(x))}" interval_minmax nil) (fmin_step formula-decl nil integral_cont_scaf nil) (cont_restrict formula-decl nil integral_cont_scaf 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (above nonempty-type-eq-decl nil integers 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 "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (eps!1 skolem-const-decl "posreal" integral_cont 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 "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (TRUE const-decl "bool" booleans nil) (continuous_on? const-decl "bool" continuous_functions nil) (setof type-eq-decl nil defined_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (b!1 skolem-const-decl "T" integral_cont nil) (a!1 skolem-const-decl "T" integral_cont nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected_domain formula-decl nil integral_cont nil)) nil) (continuous_integrable-2 nil 3292320666 ("" (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 + (("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" (lemma "in_interval") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (lemma "in_interval") (("2" (skosimp*) (("2" (inst?) 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)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 -4 -6 -8 2) (("2" (replace -1) (("2" (hide -1 -2 -3) (("2" (name-replace "BMA" "b!1-a!1") (("2" (mult-by 1 "(1 + floor(BMA / delta!1))") (("1" (div-by 1 "delta!1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (reveal -3) (("2" (assert) (("2" (case-replace "BMA / delta!1 >= 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (mult-by 1 "delta!1") (("2" (assert) (("2" (reveal -4) (("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) ("2" (hide 2) (("2" (lemma "integral_diff") (("2" (inst -1 "a!1" "b!1" "fmax(a!1, b!1, PP, f!1)" "fmin(a!1, b!1, PP, f!1)") (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (assert) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "step_function_integrable?") nil nil)) nil) ("3" (hide 2) (("3" (rewrite "step_function_integrable?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "fmax_step") nil nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "fmin_step") nil nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (hide -1 -2 -3) (("3" (inst?) (("3" (lemma "cont_restrict") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (case "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (mult-by 1 "delta!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (mult-by 1 "b!1-a!1") (("1" (assert) nil nil)) nil) ("2" (mult-by 1 "b!1-a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (rewrite "continuous_on_def") (("2" (skosimp*) (("2" (inst -2 "y!1") (("2" (rewrite "continuity_def") (("2" (expand "convergence") (("2" (expand "convergence") (("2" (flatten) (("2" (expand "extend") (("2" (expand "adh") (("2" (split +) (("1" (skosimp*) (("1" (inst + "y!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -3 "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (assert) (("2" (inst -4 "x!1") (("2" (expand "fullset") (("2" (propax) 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" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (typepred "x!1") (("2" (inst-cp 1 "a!1") (("2" (inst-cp 1 "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst -1 "a!1" "b!1" "z!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((closed_interval type-eq-decl nil intervals_real "reals/") (unif_cont_interval formula-decl nil unif_cont_fun nil) (continuity_def formula-decl nil continuous_functions nil) (abs_0 formula-decl nil abs_lems "reals/") (adh const-decl "setof[real]" convergence_functions nil) (convergence const-decl "bool" convergence_functions nil) (convergence const-decl "bool" lim_of_functions nil) (continuous_on_def formula-decl nil continuous_functions nil) (step_to_integrable formula-decl nil integral_step nil) (uniformly_continuous? const-decl "bool" unif_cont_fun nil) (step_function? const-decl "bool" step_fun_def nil) (fun_cont_on type-eq-decl nil integral_cont_scaf nil) (fun_cont_on type-eq-decl nil interval_minmax nil) (min_x const-decl "{mx: T | a <= mx AND mx <= b AND (FORALL (x: T): a <= x AND x <= b IMPLIES f(mx) <= f(x))}" interval_minmax nil) (fmin const-decl "{ff: [T -> real] | LET xx = seq(P) IN FORALL (ii: below(length(P) - 1)): FORALL (x: T): (xx(ii) < x AND x < xx(ii + 1) IMPLIES ff(x) = f(min_x(xx(ii), xx(ii + 1), f))) AND ((xx(ii) = x OR x = xx(ii + 1)) IMPLIES ff(x) = f(x))}" integral_cont_scaf nil) (fmax_step formula-decl nil integral_cont_scaf nil) (integrable? const-decl "bool" integral_def nil) (integral? const-decl "bool" integral_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (part_induction formula-decl nil integral_def nil) (width_eq_part formula-decl nil integral_def nil) (width const-decl "posreal" integral_def nil) (integral_bound_abs formula-decl nil integral_prep nil) (partition type-eq-decl nil integral_def nil) (width_lem formula-decl nil integral_def nil) (fmax_ge formula-decl nil integral_cont_scaf nil) (integral_diff formula-decl nil integral_prep nil) (step_function_integrable? formula-decl nil integral_step nil) (fmax const-decl "{ff: [T -> real] | LET xx = seq(P) IN FORALL (ii: below(length(P) - 1)): FORALL (x: T): (xx(ii) < x AND x < xx(ii + 1) IMPLIES ff(x) = f(max_x(xx(ii), xx(ii + 1), f))) AND ((xx(ii) = x OR x = xx(ii + 1)) IMPLIES ff(x) = f(x))}" integral_cont_scaf nil) (max_x const-decl "{mx: T | a <= mx AND mx <= b AND (FORALL (x: T): a <= x AND x <= b IMPLIES f(mx) >= f(x))}" interval_minmax nil) (fmin_step formula-decl nil integral_cont_scaf nil) (cont_restrict formula-decl nil integral_cont_scaf nil) (eq_partition const-decl "partition(a, b)" integral_def nil) (continuous_on? const-decl "bool" continuous_functions nil)) nil) (continuous_integrable-1 nil 3262523543 ("" (skosimp*) (("" (lemma "unif_cont_interval[closed_interval(a!1,b!1)]") (("1" (inst?) (("1" (inst -1 "f!1") (("1" (assert) (("1" (case "continuous[closed_interval(a!1, b!1)](restrict(f!1), extend[real, closed_inte (("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" (expand "restrict") (("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)") (("1" (hide -1 -2 -3) (("1" (inst -1 "xx!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (reveal -14) (("2" (lemma "cont_interv") (("2" (inst -1 "a!1" "b!1" "f!1" "PP" "seq(PP)") (("2" (assert) (("2" (split -1) (("1" (inst?) (("1" (expand "continuous?" -1) (("1" (inst?) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "continuous?" 1) (("2" (skosimp*) (("2" (inst?) (("2" (lemma "cont_restrict") (("2" (inst?) (("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)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (reveal -10) (("2" (inst?) (("2" (lemma "cont_restrict") (("2" (inst?) (("2" (assert) 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") (("1" (assert) (("1" (assert) (("1" (skosimp*) (("1" (inst - "ii!1") (("1" (inst - "xx!1") (("1" (flatten) (("1" (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)") (("1" (hide -1 -2 -3) (("1" (inst - "xx!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (reveal -14) (("2" (lemma "cont_interv") (("2" (inst -1 "a!1" "b!1" "f!1" "PP" "seq(PP)") (("2" (assert) (("2" (split -1) (("1" (inst?) (("1" (assert) (("1" (expand "continuous?" -1) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "continuous?" 1) (("2" (skosimp*) (("2" (inst?) (("2" (lemma "cont_restrict") (("2" (inst?) (("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)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (reveal -10) (("2" (inst?) (("2" (lemma "cont_restrict") (("2" (inst?) (("2" (assert) 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?) (("1" (assert) (("1" (replace -5) (("1" (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") (("1" (assert) (("1" (expand "-") (("1" (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)") (("1" (replace -1) (("1" (name "MAX_x" "max_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)") (("1" (replace -1) (("1" (case "(FORALL (x,y: closed_interval(seq(PP)(ii!1),seq(PP)(ii!1+1))): abs(x-y) <= seq(PP)(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" (expand "extend") (("2" (ground) nil nil)) nil) ("3" (expand "extend") (("3" (ground) nil 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" (lemma "in_interval") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (lemma "in_interval") (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-10 1)) (("2" (skosimp*) (("2" (lemma "cont_restrict") (("2" (inst?) (("2" (inst?) (("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)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "fmax_ge") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (reveal -9) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-7 1)) (("3" (skosimp*) (("3" (inst?) (("3" (lemma "cont_restrict") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-7 1)) (("2" (skosimp*) (("2" (inst?) (("2" (lemma "cont_restrict") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 -4 -6 -8 2) (("2" (replace -1) (("2" (hide -1 -2 -3) (("2" (name-replace "BMA" "b!1-a!1") (("2" (mult-by 1 "(1 + floor(BMA / delta!1))") (("1" (div-by 1 "delta!1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (reveal -3) (("2" (assert) (("2" (case-replace "BMA / delta!1 >= 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (mult-by 1 "delta!1") (("2" (assert) (("2" (reveal -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (case-replace "BMA / delta!1 >= 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (mult-by 1 "delta!1") (("2" (assert) (("2" (reveal -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (case-replace "BMA / delta!1 >= 0") (("1" (assert) nil nil) ("2" (reveal -2) (("2" (assert) (("2" (mult-by 1 "delta!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (mult-by 1 "delta!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "integral_diff") (("2" (inst -1 "a!1" "b!1" "fmax(a!1, b!1, PP, f!1)" "fmin(a!1, b!1, PP, f!1)") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (assert) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "step_function_integrable?") nil nil)) nil) ("3" (hide 2) (("3" (rewrite "step_function_integrable?") nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (hide 2) (("2" (hide-all-but (-6 1)) (("2" (inst?) (("2" (lemma "cont_restrict") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-6 1)) (("2" (skosimp*) (("2" (inst?) (("2" (lemma "cont_restrict") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "fmax_step") nil nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "fmin_step") nil nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (hide -1 -2 -3) (("3" (inst?) (("3" (lemma "cont_restrict") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (case "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (mult-by 1 "delta!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split +) (("1" (mult-by 1 "b!1-a!1") (("1" (assert) nil nil)) nil) ("2" (mult-by 1 "b!1-a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst -2 "y!1") (("1" (assert) (("1" (expand "extend") (("1" (expand "convergence") (("1" (expand "convergence") (("1" (flatten) (("1" (prop) (("1" (hide -3) (("1" (expand "adh") (("1" (skosimp*) (("1" (inst - "e!1") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (expand "extend") (("1" (ground) (("1" (case "y!1 + e!1/2 <= b!1") (("1" (inst + "y!1+e!1/2") (("1" (assert) (("1" (expand "abs" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (lemma "connected_domain") (("2" (inst -1 "y!1" "b!1" "y!1+e!1/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "b!1") (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -3 "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst -4 "x!1") (("2" (assert) (("2" (expand "restrict") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "y!1") (("2" (expand "extend") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -3 2) (("3" (expand "subset?") (("3" (skosimp*) (("3" (expand "member") (("3" (expand "extend") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (typepred "x!1") (("2" (inst-cp 1 "a!1") (("2" (inst-cp 1 "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst -1 "a!1" "b!1" "z!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((step_function? const-decl "bool" step_fun_def nil) (fmin const-decl "{ff: [T -> real] | LET xx = seq(P) IN FORALL (ii: below(length(P) - 1)): FORALL (x: T): (xx(ii) < x AND x < xx(ii + 1) IMPLIES ff(x) = f(min_x(xx(ii), xx(ii + 1), f))) AND ((xx(ii) = x OR x = xx(ii + 1)) IMPLIES ff(x) = f(x))}" integral_cont_scaf nil) (integrable? const-decl "bool" integral_def nil) (integral? const-decl "bool" integral_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (part_induction formula-decl nil integral_def nil) (cont_restrict formula-decl nil integral_cont_scaf nil) (cont_interv formula-decl nil integral_cont_scaf nil) (width_eq_part formula-decl nil integral_def nil) (width const-decl "posreal" integral_def nil) (integral_bound_abs formula-decl nil integral_prep nil) (width_lem formula-decl nil integral_def nil) (integral_diff formula-decl nil integral_prep nil) (step_function_integrable? formula-decl nil integral_step nil) (fmax const-decl "{ff: [T -> real] | LET xx = seq(P) IN FORALL (ii: below(length(P) - 1)): FORALL (x: T): (xx(ii) < x AND x < xx(ii + 1) IMPLIES ff(x) = f(max_x(xx(ii), xx(ii + 1), f))) AND ((xx(ii) = x OR x = xx(ii + 1)) IMPLIES ff(x) = f(x))}" integral_cont_scaf nil) (partition type-eq-decl nil integral_def nil) (eq_partition const-decl "partition(a, b)" integral_def nil) (step_to_integrable formula-decl nil integral_step nil) (adh const-decl "setof[real]" convergence_functions nil) (convergence const-decl "bool" convergence_functions nil)) nil)) (cont_fun_integrable 0 (cont_fun_integrable-1 nil 3313938280 ("" (skosimp*) (("" (lemma "continuous_integrable") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (expand "continuous?" -2) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_integrable formula-decl nil integral_cont nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (continuous? const-decl "bool" continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (T formal-subtype-decl nil integral_cont nil) (T_pred const-decl "[real -> boolean]" integral_cont 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)))
[0.310QuellennavigatorsProjekt 2026-04-25] |
||||||
2026-05-26