| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Sun/Oracle ©) Datei vom 28.9.2014 mit Größe 377 kB |
|
Quelle piecewise_continuous.prfSprache: Lisp |
|||||||||||||||
|
(piecewise_continuous (IMP_fundamental_theorem_TCC1 0 (IMP_fundamental_theorem_TCC1-1 nil 3612529043 ("" (lemma "connected_domain") (("" (propax) nil nil)) nil) ((connected_domain formula-decl nil piecewise_continuous nil)) nil)) (IMP_fundamental_theorem_TCC2 0 (IMP_fundamental_theorem_TCC2-1 nil 3612529043 ("" (lemma "not_one_element") (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil piecewise_continuous nil)) nil)) (piecewise_continuous?_TCC1 0 (piecewise_continuous?_TCC1-1 nil 3611578171 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (piecewise_continuous?_TCC2 0 (piecewise_continuous?_TCC2-1 nil 3611578171 ("" (skosimp*) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (piecewise_continuous?_TCC3 0 (piecewise_continuous?_TCC3-1 nil 3611578171 ("" (subtype-tcc) nil nil) ((strict_increasing? const-decl "bool" real_fun_preds "reals/") (continuous_on? const-decl "bool" continuous_functions nil) nil (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (piecewise_continuous?_TCC4 0 (piecewise_continuous?_TCC4-1 nil 3611578171 ("" (skeep) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (piecewise_continuous?_TCC5 0 (piecewise_continuous?_TCC5-1 nil 3611591182 ("" (grind) nil nil) ((strict_increasing? const-decl "bool" real_fun_preds "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (continuous_on? const-decl "bool" continuous_functions nil) nil (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (piecewise_continuous?_TCC6 0 (piecewise_continuous?_TCC6-1 nil 3611591182 ("" (grind) nil nil) ((strict_increasing? const-decl "bool" real_fun_preds "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (continuous_on? const-decl "bool" continuous_functions nil) nil (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (continuous_on_integrable 0 (continuous_on_integrable-1 nil 3611681282 ("" (skosimp*) (("" (lemma "unif_cont_interval[closed_interval(a!1,b!1)]") (("1" (inst?) (("1" (inst -1 "f!1") (("1" (assert) (("1" (expand "restrict") (("1" (case " continuous_on?(LAMBDA (s: closed_interval[T](a!1, b!1)): f!1(s), {xx: closed_interval[T](a!1, b!1) | TRUE})") (("1" (assert) (("1" (hide -1) (("1" (rewrite "step_to_integrable") (("1" (skosimp*) (("1" (expand "uniformly_continuous?") (("1" (inst -1 "(eps!1/2)/(b!1-a!1)") (("1" (skosimp*) (("1" (name "PP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1)+2)") (("1" (case "step_function?(a!1, b!1, fmin(a!1, b!1, PP, f!1))") (("1" (case "step_function?(a!1, b!1, fmax(a!1, b!1, PP, f!1))") (("1" (inst + "fmin(a!1,b!1,PP,f!1)" "fmax(a!1,b!1,PP,f!1)") (("1" (assert) (("1" (case "integrable?(a!1, b!1, fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1))") (("1" (assert) (("1" (case " integral(a!1, b!1, fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1)) < eps!1") (("1" (assert) (("1" (skosimp*) (("1" (hide-all-but (-7 1)) (("1" (split 1) (("1" (typepred "fmin(a!1, b!1, PP, f!1)") (("1" (lemma "part_induction") (("1" (inst -1 "(LAMBDA x: fmin(a!1, b!1, PP, f!1)(x) <= f!1(x))" "a!1" "b!1" "PP" "xx!1") (("1" (assert) (("1" (assert) (("1" (skosimp*) (("1" (assert) (("1" (inst - "ii!1") (("1" (inst - "xx!1") (("1" (flatten) (("1" (split -4) (("1" (assert) nil nil) ("2" (flatten) (("2" (assert) (("2" (replace -3) (("2" (hide -3) (("2" (assert) (("2" (typepred "min_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)") (("2" (hide -1 -2 -3) (("2" (inst -1 "xx!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "fmax(a!1, b!1, PP, f!1)") (("2" (lemma "part_induction") (("2" (inst -1 "(LAMBDA x: fmax(a!1, b!1, PP, f!1)(x) >= f!1(x))" "a!1" "b!1" "PP" "xx!1") (("2" (assert) (("2" (assert) (("2" (skosimp*) (("2" (inst - "ii!1") (("2" (inst - "xx!1") (("2" (flatten) (("2" (split -4) (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (assert) (("2" (replace -3) (("2" (hide -3) (("2" (typepred "max_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)") (("2" (hide -1 -2 -3) (("2" (inst - "xx!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "width_eq_part") (("2" (inst?) (("2" (assert) (("2" (replace -5) (("2" (case "width(a!1,b!1,PP) < delta!1") (("1" (hide -2 -6) (("1" (lemma "integral_bound_abs") (("1" (inst -1 "eps!1/(2*(b!1-a!1))" "a!1" "b!1" "fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1)") (("1" (name-replace "BMA" "b!1-a!1") (("1" (assert) (("1" (split -1) (("1" (name "III" "integral(a!1, b!1, fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1))") (("1" (case "III >= 0") (("1" (replace -2) (("1" (expand "abs" -3) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "-") (("2" (lemma "part_induction") (("2" (inst -1 "(LAMBDA x: (fmax(a!1, b!1, PP, f!1) - fmin(a!1, b!1, PP, f!1))(x) <= eps!1 / (2 * BMA))" "a!1" "b!1" "PP" "x!1") (("2" (assert) (("2" (expand "-") (("2" (case "fmax(a!1, b!1, PP, f!1)(x!1) - fmin(a!1, b!1, PP, f!1)(x!1) >= 0") (("1" (expand "abs" 1) (("1" (assert) (("1" (assert) (("1" (skosimp*) (("1" (typepred "fmax(a!1, b!1, PP, f!1)") (("1" (typepred "fmin(a!1, b!1, PP, f!1)") (("1" (inst -1 "ii!1") (("1" (inst -2 "ii!1") (("1" (inst -1 "x!1") (("1" (inst -2 "x!1") (("1" (flatten) (("1" (case "(seq(PP)(ii!1) = x!1 OR x!1 = seq(PP)(1 + ii!1))") (("1" (assert) (("1" (split -1) (("1" (assert) (("1" (hide -2 -4) (("1" (replace -2) (("1" (replace -3) (("1" (assert) (("1" (hide-all-but 1) (("1" (reveal -21) (("1" (mult-by 1 "(2*BMA)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -2 -4) (("2" (replace -2) (("2" (replace -3) (("2" (assert) (("2" (hide-all-but 1) (("2" (reveal -21) (("2" (mult-by 1 "(2*BMA)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide -2 -4) (("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (name "MIN_x" "min_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)") (("2" (replace -1) (("2" (name "MAX_x" "max_x(seq(PP)(ii!1), seq(PP)(1 + ii!1), f!1)") (("2" (replace -1) (("2" (case "(FORALL (x,y: closed_interval(seq(PP)(ii!1),seq(PP)(ii!1+1))): abs(x-y) <= seq(PP)(1 + (("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) (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) (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) (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) (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" piecewise_continuous 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) (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))}" piecewise_continuous nil) (ii!1 skolem-const-decl "below(length(PP) - 1)" piecewise_continuous nil) (f!1 skolem-const-decl "[T -> real]" piecewise_continuous 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))}" piecewise_continuous 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))}" piecewise_continuous 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" piecewise_continuous nil) (delta!1 skolem-const-decl "posreal" piecewise_continuous 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) (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" piecewise_continuous 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" piecewise_continuous nil) (a!1 skolem-const-decl "T" piecewise_continuous 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) ((Integrable? const-decl "bool" integral_def 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) (integrable_split formula-decl nil integral_split nil) (i skolem-const-decl "nat" piecewise_continuous nil) (piecewise_continuous? const-decl "bool" piecewise_continuous 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) (P skolem-const-decl "[upto(N) -> T]" piecewise_continuous nil) (N skolem-const-decl "posnat" piecewise_continuous nil) (= const-decl "[T, T -> boolean]" equalities nil) (f1 skolem-const-decl "[T -> real]" piecewise_continuous nil) (f2 skolem-const-decl "[T -> real]" piecewise_continuous nil) (integral_restrict_eq formula-decl nil integral_def nil) (integral_chg_one_pt formula-decl nil integral_prep nil) (below type-eq-decl nil naturalnumbers nil) (i skolem-const-decl "nat" piecewise_continuous nil) (continuous_on_integrable formula-decl nil piecewise_continuous nil) (i skolem-const-decl "nat" 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_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) (piecewise_continuous? const-decl "bool" piecewise_continuous nil) (piecewise_continuous? const-decl "bool" piecewise_continuous nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (integrable_split formula-decl nil integral_split 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) (integral_chg_one_pt formula-decl nil integral_prep 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) ((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) ((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_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*) (("" (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_TCC7 0 (piecewise_continuous_integral_TCC7-1 nil 3612186214 ("" (skosimp*) (("" (lemma "continuous_on_integrable") (("" (expand "Integrable?") (("" (assert) (("" (flatten) (("" (hide (1 3)) (("" (assert) (("" (hide -2) (("" (expand "piecewise_continuous?") (("" (flatten) (("" (expand "piecewise_continuous?") (("" (flatten) (("" (expand "strict_increasing?") (("" (inst - "k!1" "k!1+1") (("" (assert) (("" (inst?) (("" (assert) (("" (inst - "k!1") 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) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (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) (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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (T formal-nonempty-subtype-decl nil piecewise_continuous nil) (T_pred const-decl "[real -> boolean]" piecewise_continuous nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") nil nil (Integrable? const-decl "bool" integral_def nil)) nil)) (piecewise_continuous_integral_TCC8 0 (piecewise_continuous_integral_TCC8-1 nil 3612186214 ("" (skeep) (("" (skeep) (("" (assert) nil nil)) nil)) 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (piecewise_continuous_integral_TCC9 0 (piecewise_continuous_integral_TCC9-2 nil 3612187243 ("" (skosimp*) (("" (lemma "continuous_on_integrable") (("" (expand "Integrable?") (("" (assert) (("" (flatten) (("" (assert) (("" (inst - "P!1(i!1)" "x!1" "H!1(i!1)") (("" (assert) (("" (expand "piecewise_continuous?") (("" (flatten) (("" (expand "piecewise_continuous?") (("" (flatten) (("" (assert) (("" (inst - "i!1") (("" (assert) (("" (expand "continuous_on?") (("" (skeep) (("" (inst - "x0") (("" (skeep) (("" (inst - "epsilon") (("" (skeep -) (("" (inst + "delta") (("" (skeep) (("" (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) ((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) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) nil nil (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (Integrable? const-decl "bool" integral_def nil)) nil) (piecewise_continuous_integral_TCC9-1 nil 3612186214 ("" (subtype-tcc) nil nil) 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) (piecewise_continuous? const-decl "bool" piecewise_continuous nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (integral_restrict_eq formula-decl nil integral_def nil) (integral_split formula-decl nil integral_split nil) (N skolem-const-decl "posnat" piecewise_continuous nil) (a skolem-const-decl "T" piecewise_continuous nil) (P skolem-const-decl "[upto(N) -> T]" piecewise_continuous nil) (f skolem-const-decl "[T -> real]" piecewise_continuous nil) (H skolem-const-decl "[below(N) -> [T -> real]]" piecewise_continuous nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (kv!1 skolem-const-decl "nat" piecewise_continuous nil) (kv!1 skolem-const-decl "nat" piecewise_continuous nil) (kv!1 skolem-const-decl "nat" piecewise_continuous nil) (kv!1 skolem-const-decl "nat" piecewise_continuous nil) (kv!1 skolem-const-decl "nat" piecewise_continuous nil) (kv!1 skolem-const-decl "nat" piecewise_continuous nil) (kv!1 skolem-const-decl "nat" piecewise_continuous nil) (Integral_a_to_a formula-decl nil integral nil) (integral_restr_eq formula-decl nil integral_prep 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) (piecewise_continuous? const-decl "bool" piecewise_continuous nil) (piecewise_continuous? const-decl "bool" piecewise_continuous 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)))
¤ Dauer der Verarbeitung: 0.455 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26