| 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 369 kB |
|
Impressum piecewise_continuous.prfSprache: Lisp |
|||||||||||||||
|
(piecewise_continuous (IMP_fundamental_theorem_TCC1 0 (IMP_fundamental_theorem_TCC1-1 nil 3612542950 ("" (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 3612542950 ("" (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) (piecewise_continuous? const-decl "bool" piecewise_continuous 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) (piecewise_continuous? const-decl "bool" piecewise_continuous 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) (piecewise_continuous? const-decl "bool" piecewise_continuous 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 + (("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)) 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" (expand "continuous_on?") (("3" (expand "continuous?") (("3" (inst - "x!1") (("3" (skeep) (("3" (inst - "epsilon") (("3" (skeep) (("3" (inst + "delta") (("3" (skeep) (("3" (inst - "x") (("3" (expand "restrict") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (mult-by 1 "delta!1") (("2" (assert) (("2" (case "floor((b!1 - a!1) / delta!1)>=0") (("1" (mult-by -1 "delta!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (mult-by -2 "1/delta!1") (("2" (assert) nil 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_on?") (("2" (propax) 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-nonempty-subtype-decl nil piecewise_continuous nil) (T_pred const-decl "[real -> boolean]" piecewise_continuous 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? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (restrict const-decl "R" restrict nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans 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) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences 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) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-decl nil integers 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) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected_domain formula-decl nil piecewise_continuous nil)) nil)) (piecewise_continuous_integrable 0 (piecewise_continuous_integrable-2 nil 3612528404 ("" (skeep) (("" (expand "Integrable?") (("" (assert) (("" (lemma "integrable_split[T]") (("" (expand "piecewise_continuous?") (("" (skeep) (("" (expand "piecewise_continuous?") (("" (flatten) (("" (case "FORALL (i:nat): i+1<=N IMPLIES integrable?(P(0),P(i+1),f)") (("1" (inst - "N-1") (("1" (assert) nil nil)) nil) ("2" (case "FORALL (i:nat): i+1<=N IMPLIES integrable?(P(i),P(i+1),f)") (("1" (induct "i") (("1" (assert) (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (inst - "1+j") (("2" (assert) (("2" (inst - "P(0)" "P(1+j)" "P(2+j)" "f") (("2" (assert) (("2" (expand "piecewise_continuous?") (("2" (flatten) (("2" (expand "strict_increasing?") (("2" (inst-cp - "0" "1+j") (("2" (inst - "1+j" "2+j") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (expand "piecewise_continuous?") (("3" (flatten) (("3" (expand "strict_increasing?") (("3" (inst - "0" "1+i") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "piecewise_continuous?") (("2" (flatten) (("2" (hide 2) (("2" (hide 2) (("2" (lemma "continuous_on_integrable") (("2" (skeep) (("2" (inst - "i") (("1" (assert) (("1" (inst - _ _ "H(i)") (("1" (assert) (("1" (inst - "P(i)" "P(i+1)") (("1" (assert) (("1" (expand "strict_increasing?") (("1" (inst? -5) (("1" (assert) (("1" (assert) (("1" (lemma "integral_chg_one_pt") (("1" (name "f1" "H(i) WITH [(P(i)):=f(P(i))]") (("1" (name "f2" "f1 WITH [(P(i+1)):=f(P(i+1))]") (("1" (inst - "P(i)" "P(i+1)" "H(i)" "f(P(i))") (("1" (assert) (("1" (inst - "P(i)") (("1" (assert) (("1" (flatten) (("1" (hide -4) (("1" (replace -2) (("1" (lemma "integral_chg_one_pt") (("1" (inst - "P(i)" "P(i+1)" "f1" "f(P(i+1))") (("1" (assert) (("1" (inst - "P(i+1)") (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (replace -2) (("1" (lemma "integral_restrict_eq") (("1" (inst - "P(i)" "P(i+1)" "f2" "f") (("1" (assert) (("1" (skeep) (("1" (expand "f2" 1) (("1" (expand "f1" 1) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (inst - "i") (("1" (inst - "x") (("1" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (skeep) (("3" (expand "piecewise_continuous?") (("3" (expand "strict_increasing?") (("3" (flatten) (("3" (inst - "i" "i+1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (assert) nil nil)) nil)) nil) ("3" (assert) (("3" (expand "piecewise_continuous?") (("3" (expand "strict_increasing?") (("3" (flatten) (("3" (skeep) (("3" (inst - "0" "i+1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (integrable? const-decl "bool" integral_def nil) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (continuous_on_integrable formula-decl nil piecewise_continuous nil) (below type-eq-decl nil naturalnumbers nil) (integral_restrict_eq formula-decl nil integral_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (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]" piecewise_continuous nil) (T formal-nonempty-subtype-decl nil piecewise_continuous nil) (Integrable? const-decl "bool" integral_def nil)) nil) (piecewise_continuous_integrable-1 nil 3611589970 ("" (skeep) (("" (lemma "integrable_split[T]") (("" (expand "piecewise_continuous?") (("" (skeep) (("" (expand "piecewise_continuous?") (("" (flatten) (("" (case "FORALL (i:nat): i+1<=N IMPLIES integrable?(P(0),P(i+1),f)") (("1" (inst - "N-1") (("1" (assert) nil nil)) nil) ("2" (case "FORALL (i:nat): i+1<=N IMPLIES integrable?(P(i),P(i+1),f)") (("1" (induct "i") (("1" (assert) (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (inst - "1+j") (("2" (assert) (("2" (inst - "P(0)" "P(1+j)" "P(2+j)" "f") (("2" (assert) (("2" (expand "piecewise_continuous?") (("2" (flatten) (("2" (expand "strict_increasing?") (("2" (inst-cp - "0" "1+j") (("2" (inst - "1+j" "2+j") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (expand "piecewise_continuous?") (("3" (flatten) (("3" (expand "strict_increasing?") (("3" (inst - "0" "1+i") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "piecewise_continuous?") (("2" (flatten) (("2" (hide 2) (("2" (hide 2) (("2" (lemma "continuous_on_integrable") (("2" (skeep) (("2" (inst - "i") (("1" (assert) (("1" (inst - _ _ "H(i)") (("1" (assert) (("1" (inst - "P(i)" "P(i+1)") (("1" (assert) (("1" (expand "strict_increasing?") (("1" (inst? -5) (("1" (assert) (("1" (assert) (("1" (lemma "integral_chg_one_pt") (("1" (name "f1" "H(i) WITH [(P(i)):=f(P(i))]") (("1" (name "f2" "f1 WITH [(P(i+1)):=f(P(i+1))]") (("1" (inst - "P(i)" "P(i+1)" "H(i)" "f(P(i))") (("1" (assert) (("1" (inst - "P(i)") (("1" (assert) (("1" (flatten) (("1" (hide -4) (("1" (replace -2) (("1" (lemma "integral_chg_one_pt") (("1" (inst - "P(i)" "P(i+1)" "f1" "f(P(i+1))") (("1" (assert) (("1" (inst - "P(i+1)") (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (replace -2) (("1" (lemma "integral_restrict_eq") (("1" (inst - "P(i)" "P(i+1)" "f2" "f") (("1" (assert) (("1" (skeep) (("1" (expand "f2" 1) (("1" (expand "f1" 1) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (inst - "i") (("1" (inst - "x") (("1" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (skeep) (("3" (expand "piecewise_continuous?") (("3" (expand "strict_increasing?") (("3" (flatten) (("3" (inst - "i" "i+1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skeep) (("4" (assert) nil nil)) nil)) nil) ("3" (assert) (("3" (expand "piecewise_continuous?") (("3" (expand "strict_increasing?") (("3" (flatten) (("3" (skeep) (("3" (inst - "0" "i+1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil piecewise_continuous nil) (T_pred const-decl "[real -> boolean]" piecewise_continuous 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) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (integral_restrict_eq formula-decl nil integral_def nil) (below type-eq-decl nil naturalnumbers nil) (continuous_on_integrable formula-decl nil piecewise_continuous nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (integrable? const-decl "bool" integral_def nil) (upto nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (piecewise_continuous_integral_TCC1 0 (piecewise_continuous_integral_TCC1-1 nil 3612186214 ("" (skosimp*) (("" (assert) nil nil)) 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)) nil)) (piecewise_continuous_integral_TCC2 0 (piecewise_continuous_integral_TCC2-1 nil 3612186214 ("" (skosimp*) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers 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)) nil)) (piecewise_continuous_integral_TCC3 0 (piecewise_continuous_integral_TCC3-1 nil 3612186214 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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)) nil)) (piecewise_continuous_integral_TCC4 0 (piecewise_continuous_integral_TCC4-1 nil 3612186214 ("" (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (piecewise_continuous_integral_TCC5 0 (piecewise_continuous_integral_TCC5-1 nil 3612186214 ("" (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (piecewise_continuous_integral_TCC6 0 (piecewise_continuous_integral_TCC6-1 nil 3612186214 ("" (skosimp*) (("" (lemma "continuous_on_integrable") (("" (inst - "P!1(k!1)" "P!1(1+k!1)" "H!1(k!1)") (("" (assert) (("" (expand "piecewise_continuous?") (("" (flatten) (("" (expand "piecewise_continuous?") (("" (flatten) (("" (inst - "k!1") (("" (assert) (("" (expand "strict_increasing?") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_on_integrable formula-decl nil piecewise_continuous nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (piecewise_continuous? const-decl "bool" piecewise_continuous nil) (piecewise_continuous? const-decl "bool" piecewise_continuous nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (T formal-nonempty-subtype-decl nil piecewise_continuous nil) (T_pred const-decl "[real -> boolean]" piecewise_continuous 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (piecewise_continuous_integral_TCC7 0 (piecewise_continuous_integral_TCC7-1 nil 3612186214 ("" (skosimp*) (("" (lemma "continuous_on_integrable") (("" (assert) (("" (inst - "P!1(i!1)" "x!1" "H!1(i!1)") (("" (assert) (("" (lemma "Integrable?_a_to_a") (("" (inst - "x!1" "H!1(i!1)") (("" (assert) (("" (expand "piecewise_continuous?") (("" (expand "piecewise_continuous?") (("" (flatten) (("" (inst - "i!1") (("" (assert) (("" (expand "continuous_on?") (("" (skosimp*) (("" (inst - "x0!1") (("" (assert) (("" (inst - "epsilon!1") (("" (skeep) (("" (inst + "delta") (("" (skosimp*) (("" (inst - "x!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) ((continuous_on_integrable formula-decl nil piecewise_continuous 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]" piecewise_continuous nil) (T formal-nonempty-subtype-decl nil piecewise_continuous nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (Integrable?_a_to_a formula-decl nil integral nil) (piecewise_continuous? const-decl "bool" piecewise_continuous nil) (real_minus_real_is_real application-judgement "real" reals nil) (continuous_on? const-decl "bool" continuous_functions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (piecewise_continuous? const-decl "bool" piecewise_continuous 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (piecewise_continuous_integral 0 (piecewise_continuous_integral-2 nil 3612273788 ("" (skeep) (("" (label "px" (-4 -5)) (("" (copy -3) (("" (label "pc1" -4) (("" (expand "piecewise_continuous?" -1) (("" (flatten) (("" (label "p0a" -2) (("" (label "PNb" -3) (("" (label "Heq" -4) (("" (copy -1) (("" (expand "piecewise_continuous?" -1) (("" (label "pc2" -2) (("" (flatten) (("" (label "si" -1) (("" (copy -2) (("" (label "cisaved" -1) (("" (hide "cisaved") (("" (label "ci" -2) (("" (copy -1) (("" (expand "strict_increasing?" -1) (("" (inst-cp - "0" "i") (("" (inst-cp - "i" "i+1") (("" (inst-cp - "i+1" "N") (("" (label "ci2" -1) (("" (label "pii" -3) (("" (assert) (("" (case "NOT (a<=P(i) AND P(i+1)<=b)") (("1" (ground) nil nil) ("2" (flatten) (("2" (label "pabz" (-1 -2)) (("2" (assert) (("2" (label "ranges" (-4 -6)) (("2" (hide "ranges") (("2" (lemma "Integrable?_inside") (("2" (label "ii4" -1) (("2" (inst-cp - "a" "b" "f" "a" "x") (("2" (assert) (("2" (lemma "piecewise_continuous_integrable") (("2" (inst - "a" "b" "f") (("2" (assert) (("2" (case "NOT piecewise_continuous?(f, a, b)") (("1" (assert) (("1" (expand "piecewise_continuous?" 1) (("1" (inst + "N" "P" "H") nil nil)) nil)) nil) ("2" (assert) (("2" (inst-cp - "a" "x" "f" _ _) (("2" (assert) (("2" (label "intss" -4) (("2" (lemma "Integral_split") (("2" (inst - "a" "P(i)" "x" "f") (("2" (assert) (("2" (inst-cp - "a" "P(i)") (("2" (inst-cp - "P(i)" "x") (("2" (assert) (("2" (assert) (("2" (lemma "integral_restrict_eq") (("2" (inst - "P(i)" "x" "f" "H(i)") (("2" (assert) (("2" (case "NOT Integral(a, P(i), f) = sigma(0, i - 1, LAMBDA (k: nat): IF k < N THEN Integral(P(k), P(1 + k), H(k)) ELSE 0 ENDIF)") (("1" (hide 2) (("1" (hide -1) (("1" (case "FORALL (kv:nat): kv<N IMPLIES Integral(a, P(kv), f) = sigma(0, kv - 1, LAMBDA (k: nat): IF k < N THEN Integral(P(k), P(1 + k), H(k)) ELSE 0 ENDIF)") (("1" (inst - "i") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "kv") (("1" (assert) (("1" (lemma "Integral_a_to_a") (("1" (inst?) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (lemma "Integral_split") (("2" (inst - "a" "P(j)" "P(j+1)" "f") (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (replaces -2 :dir rl) (("1" (assert) (("1" (expand "sigma" +) (("1" (assert) (("1" (replace -2 :dir rl) (("1" (lemma "integral_restr_eq") (("1" (inst - "P(j)" "P(1+j)" "f" "H(j)") (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (expand "Integral" 1) (("1" (assert) (("1" (copy "ci2") (("1" (inst - "j" "1+j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (copy "ci2") (("2" (inst - "j" "1+j") (("2" (assert) nil nil)) nil)) nil) ("3" (copy "Heq") (("3" (inst - "j") nil nil)) nil) ("4" (inst "ii4" "a" "b" "f" "P(j)" "P(1+j)") (("4" (assert) (("4" (copy "ci2") (("4" (inst-cp - "0" "j") (("4" (inst-cp - "j" "1+j") (("4" (inst - "1+j" "N") (("4" (ground) (("1" (expand "Integrable?" -1) (("1" (propax) nil nil)) nil) ("2" (expand "Integrable?" -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Integrable?" 1) (("2" (flatten) (("2" (copy "ci2") (("2" (inst-cp - "0" "j") (("2" (assert) (("2" (inst "ii4" "a" "b" "f" "a" "P(j)") (("2" (assert) (("2" (split "ii4") (("1" (expand "Integrable?" -1) (("1" (propax) nil nil)) nil) ("2" (inst - "j" "N") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst "ii4" "a" "b" "f" "P(j)" "P(1+j)") (("3" (assert) (("3" (expand "Integrable?" 1) (("3" (copy "ci2") (("3" (inst - "j" "1+j") (("3" (assert) (("3" (expand "Integrable?" "ii4") (("3" (copy "ci2") (("3" (inst-cp - "0" "j") (("3" (inst - "1+j" "N") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (skeep) (("4" (lemma "continuous_on_integrable") (("4" (inst - "P(k)" "P(1+k)" "H(k)") (("4" (assert) (("4" (expand "Integrable?" 1) (("4" (flatten) (("4" (assert) (("4" (reveal "cisaved") (("4" (inst - "k") (("4" (assert) (("4" (copy "ci2") (("4" (inst - "k" "1+k") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil) ("7" (skosimp*) (("7" (inst + "10") (("7" (assert) nil nil)) nil)) nil) ("8" (skeep) (("8" (assert) (("8" (inst "ii4" "a" "b" "f" "a" "P(kv)") (("8" (assert) (("8" (copy "ci2") (("8" (inst-cp - "0" "kv") (("8" (inst - "kv" "N") (("8" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("9" (skosimp*) (("9" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (hide 2) (("4" (inst "ii4" "a" "b" "f" "P(k!1)" "P(1+k!1)") (("4" (assert) (("4" (split "ii4") (("1" (lemma "integral_restr_eq") (("1" (inst - "P(k!1)" "P(1+k!1)" "f" "H(k!1)") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (expand "Integrable?" 1) (("1" (flatten) (("1" (assert) (("1" (copy "ci2") (("1" (inst - "k!1" "1+k!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (copy "ci2") (("2" (inst - "k!1" "1+k!1") (("2" (assert) nil nil)) nil)) nil) ("3" (copy "Heq") (("3" (skeep) (("3" (inst - "k!1") (("3" (inst - "x!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (expand "Integrable?" -1) (("4" (assert) (("4" (copy "ci2") (("4" (inst - "k!1" "1+k!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (copy "ci2") (("2" (inst - "0" "k!1") (("2" (assert) nil nil)) nil)) nil) ("3" (copy "ci2") (("3" (inst - "k!1" "1+k!1") (("3" (assert) nil nil)) nil)) nil) ("4" (copy "ci2") (("4" (inst - "1+k!1" "N") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil) ("7" (skosimp*) (("7" (assert) nil nil)) nil) ("8" (hide 2) (("8" (skeep) (("8" (inst "ii4" "a" "b" "f" "a" "P(kv)") (("8" (assert) (("8" (copy "ci2") (("8" (inst-cp - "0" "kv") (("8" (inst-cp - "kv" "N") (("8" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1 :dir rl) (("2" (hide -1) (("2" (assert) (("2" (lemma "integral_restr_eq") (("2" (inst - "P(i)" "x" "f" "H(i)") (("2" (split -) (("1" (flatten) (("1" (assert) (("1" (expand "Integral" +) (("1" (assert) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (replace -2) (("1" (lemma "integral_split") (("1" (inst - "a" "P(i)" "x" "f") (("1" (assert) (("1" (expand "Integrable?" -) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT x = P(i)") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (rewrite "Integral_a_to_a" 2) nil nil)) nil)) nil)) nil) ("3" (copy "Heq") (("3" (skosimp*) (("3" (inst - "i") (("3" (inst - "x!1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil) ("4" (copy -6) (("4" (expand "Integrable?" -1) (("4" (assert) (("4" (replaces -1) (("4" (assert) (("4" (rewrite "Integral_a_to_a" 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skeep) (("4" (copy "ci2") (("4" (inst-cp - "k" "1+k") (("4" (assert) (("4" (expand "Integrable?" 1) (("4" (assert) (("4" (lemma "continuous_on_integrable") (("4" (inst?) (("4" (assert) (("4" (inst "ci" "k") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (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)) 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) ((strict_increasing? const-decl "bool" real_fun_preds "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (integral_restrict_eq formula-decl nil integral_def nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (Integral_a_to_a formula-decl nil integral nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (continuous_on_integrable formula-decl nil piecewise_continuous nil) (integer nonempty-type-from-decl nil integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (Integral const-decl "real" integral_def nil) (Integrable_funs type-eq-decl nil integral_def nil) (Integrable? const-decl "bool" integral_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (Integral_split formula-decl nil integral nil) (piecewise_continuous_integrable formula-decl nil piecewise_continuous nil) (Integrable?_inside formula-decl nil integral nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-nonempty-subtype-decl nil piecewise_continuous nil) (T_pred const-decl "[real -> boolean]" piecewise_continuous nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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)) nil) (piecewise_continuous_integral-1 nil 3612260269 ("" (skeep) (("" (label "px" (-4 -5)) (("" (copy -3) (("" (label "pc1" -4) (("" (expand "piecewise_continuous?" -1) (("" (flatten) (("" (label "p0a" -2) (("" (label "PNb" -3) (("" (label "Heq" -4) (("" (copy -1) (("" (expand "piecewise_continuous?" -1) (("" (label "pc2" -2) (("" (flatten) (("" (label "si" -1) (("" (label "ci" -2) (("" (copy -1) (("" (expand "strict_increasing?" -1) (("" (inst-cp - "0" "i") (("" (inst-cp - "i" "i+1") (("" (inst-cp - "i+1" "N") (("" (label "ci2" -1) (("" (label "pii" -3) (("" (assert) (("" (case "NOT (a<=P(i) AND P(i+1)<=b)") (("1" (ground) nil nil) ("2" (flatten) (("2" (label "pabz" (-1 -2)) (("2" (assert) (("2" (label "ranges" (-4 -6)) (("2" (hide "ranges") (("2" (lemma "Integrable?_inside") (("2" (label "ii4" -1) (("2" (inst-cp - "a" "b" "f" "a" "x") (("2" (assert) (("2" (lemma "piecewise_continuous_integrable") (("2" (inst - "a" "b" "f") (("2" (assert) (("2" (case "NOT piecewise_continuous?(f, a, b)") (("1" (assert) (("1" (expand "piecewise_continuous?" 1) (("1" (inst + "N" "P" "H") nil nil)) nil)) nil) ("2" (assert) (("2" (inst-cp - "a" "x" "f" _ _) (("2" (assert) (("2" (label "intss" -4) (("2" (expand "Integrable?" -5 1) (("2" (assert) (("2" (assert) (("2" (lemma "Integral_split") (("2" (inst - "a" "P(i)" "x" "f") (("2" (assert) (("2" (inst-cp - "a" "P(i)") (("2" (inst-cp - "P(i)" "x") (("2" (assert) (("2" (assert) (("2" (lemma "integral_restrict_eq") (("2" (inst - "P(i)" "x" "f" "H(i)") (("2" (assert) (("2" (case "NOT Integral(a, P(i), f) = sigma(0, i - 1, LAMBDA (k: nat): IF k < N THEN Integral(P(k), P(1 + k), H(k)) ELSE 0 ENDIF)") (("1" (hide 2) (("1" (hide -1) (("1" (case "FORALL (kv:nat): kv<N IMPLIES Integral(a, P(kv), f) = sigma(0, kv - 1, LAMBDA (k: nat): IF k < N THEN Integral(P(k), P(1 + k), H(k)) ELSE 0 ENDIF)") (("1" (inst - "i") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "kv") (("1" (assert) (("1" (lemma "Integral_a_to_a") (("1" (inst?) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (lemma "Integral_split") (("2" (inst - "a" "P(j)" "P(j+1)" "f") (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (replaces -2 :dir rl) (("1" (assert) (("1" (expand "sigma" +) (("1" (assert) (("1" (replace -2 :dir rl) (("1" (lemma "integral_restr_eq") (("1" (inst - "P(j)" "P(1+j)" "f" "H(j)") (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (expand "Integral" 1) (("1" (assert) (("1" (copy "ci2") (("1" (inst - "j" "1+j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (copy "ci2") (("2" (inst - "j" "1+j") (("2" (assert) nil nil)) nil)) nil) ("3" (copy "Heq") (("3" (inst - "j") nil nil)) nil) ("4" (inst "ii4" "a" "b" "f" "P(j)" "P(1+j)") (("4" (assert) (("4" (copy "ci2") (("4" (inst-cp - "0" "j") (("4" (inst-cp - "j" "1+j") (("4" (inst - "1+j" "N") (("4" (ground) (("1" (expand "Integrable?" -1) (("1" (propax) nil nil)) nil) ("2" (expand "Integrable?" 1) (("2" (propax) nil nil)) nil) ("3" (expand "Integrable?" -1) (("3" (propax) nil nil)) nil) ("4" (expand "Integrable?" 1) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Integrable?" 1) (("2" (flatten) (("2" (copy "ci2") (("2" (inst-cp - "0" "j") (("2" (assert) (("2" (inst "ii4" "a" "b" "f" "a" "P(j)") (("2" (assert) (("2" (split "ii4") (("1" (expand "Integrable?" -1) (("1" (propax) nil nil)) nil) ("2" (inst - "j" "N") (("2" (assert) nil nil)) nil) ("3" (expand "Integrable?" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst "ii4" "a" "b" "f" "P(j)" "P(1+j)") (("3" (assert) (("3" (expand "Integrable?" 1) (("3" (copy "ci2") (("3" (inst - "j" "1+j") (("3" (assert) (("3" (expand "Integrable?" "ii4") (("3" (copy "ci2") (("3" (inst-cp - "0" "j") (("3" (inst - "1+j" "N") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (skeep) (("4" (lemma "continuous_on_integrable") (("4" (inst - "P(k)" "P(1+k)" "H(k)") (("4" (assert) (("4" (expand "Integrable?" 1) (("4" (flatten) (("4" (assert) (("4" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (postpone) nil nil) ("6" (postpone) nil nil) ("7" (postpone) nil nil) ("8" (postpone) nil nil) ("9" (postpone) nil nil)) nil)) nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil) ("6" (postpone) nil nil) ("7" (postpone) nil nil) ("8" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil) ("6" (postpone) 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)) 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 shostak)))
¤ 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.0.326Bemerkung: (vorverarbeitet am 2026-04-26) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26