| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 638 kB |
|
Quelle integral_split_scaf.prfSprache: Lisp |
|||||||||||||||
|
(integral_split_scaf (IMP_step_fun_def_TCC1 0 (IMP_step_fun_def_TCC1-1 nil 3292238135 ("" (skosimp*) (("" (lemma "connected_domain") (("" (expand "connected?") (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil integral_split_scaf nil)) shostak)) (IMP_step_fun_def_TCC2 0 (IMP_step_fun_def_TCC2-1 nil 3292238135 ("" (skosimp*) (("" (lemma "not_one_element") (("" (expand "not_one_element?") (("" (inst?) nil nil)) nil)) nil)) nil) ((not_one_element formula-decl nil integral_split_scaf nil)) shostak)) (diff_step_is_step_on 0 (diff_step_is_step_on-1 nil 3292237292 ("" (skosimp*) (("" (expand "step_function_on?") (("" (skosimp*) (("" (inst - "ii!1") (("" (inst - "ii!1") (("" (skosimp*) (("" (inst + "fv!1-fv!2") (("" (skosimp*) (("" (inst - "x!1") (("" (inst - "x!1") (("" (expand "-") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((step_function_on? const-decl "bool" step_fun_def 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil nat_types nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (open_interval type-eq-decl nil intervals_real "reals/") (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (se_not_on_TCC1 0 (se_not_on_TCC1-1 nil 3282569216 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (se_not_on 0 (se_not_on-1 nil 3282569138 ("" (skosimp*) (("" (typepred "x!1") (("" (case "ii!1 = jj!1") (("1" (assert) nil nil) ("2" (lemma "parts_order[T]") (("2" (inst - "a!1" "b!1" "P!1" "ii!1+1" "jj!1") (("2" (assert) (("2" (case "ii!1 + 1 = jj!1") (("1" (assert) nil nil) ("2" (assert) (("2" (replace -4) (("2" (hide -4) (("2" (lemma "parts_order[T]") (("2" (inst - "a!1" "b!1" "P!1" "jj!1" "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((open_interval type-eq-decl nil intervals_real "reals/") (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (parts_order formula-decl nil integral_def nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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)) nil)) (find_P_sec_TCC1 0 (find_P_sec_TCC1-1 nil 3282569216 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (find_P_sec_TCC2 0 (find_P_sec_TCC2-1 nil 3282569216 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (find_P_sec_TCC3 0 (find_P_sec_TCC3-1 nil 3282569216 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, partition[T](a, b), (LAMBDA (x: T): a <= x AND x <= b)]): choose({ii: below(length(d`3) - 1) | seq(d`3)(ii) <= d`4 AND d`4 <= seq(d`3)(1 + ii)}))") (("1" (skosimp*) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "part_in[T]") (("1" (inst - "d!1`1" "d!1`2" "d!1`4" "d!1`3") (("1" (assert) (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (part_in formula-decl nil integral_def 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (find_P_sec_TCC4 0 (find_P_sec_TCC4-1 nil 3610725744 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, partition[T](a, b), (LAMBDA (x: T): a <= x AND x <= b)]): choose({ii: below(length(d`3) - 1) | seq(d`3)(ii) <= d`4 AND d`4 <= seq(d`3)(1 + ii)}))") (("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (lemma "part_in[T]") (("" (inst - "d!1`1" "d!1`2" "d!1`4" "d!1`3") (("" (assert) (("" (assert) (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (part_in formula-decl nil integral_def 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) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (T formal-subtype-decl nil integral_split_scaf nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (find_P_sec_lem_TCC1 0 (find_P_sec_lem_TCC1-1 nil 3282569216 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (find_P_sec_lem_TCC2 0 (find_P_sec_lem_TCC2-1 nil 3282569216 ("" (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)) shostak)) (find_P_sec_lem 0 (find_P_sec_lem-1 nil 3282569175 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (find_P_sec_in_TCC1 0 (find_P_sec_in_TCC1-1 nil 3282569217 ("" (skosimp*) (("" (assert) (("" (typepred "x!1") (("" (assert) nil nil)) 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (open_interval type-eq-decl nil intervals_real "reals/")) shostak)) (find_P_sec_in 0 (find_P_sec_in-1 nil 3282569204 ("" (skosimp*) (("" (typepred "find_P_sec(a!1, b!1, P!1, x!1)") (("1" (name-replace "FP" "find_P_sec(a!1, b!1, P!1, x!1)") (("1" (typepred "x!1") (("1" (case-replace "x!1 = seq(P!1)(FP) ") (("1" (hide -1) (("1" (hide -5) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "b!1" "P!1" "ii!1+1" "FP") (("1" (assert) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "b!1" "P!1" "FP" "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "x!1 = seq(P!1)(FP+1) ") (("1" (hide -7) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "b!1" "P!1" "FP+1" "ii!1") (("1" (assert) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "b!1" "P!1" "ii!1+1" "FP") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "parts_disjoint[T]") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil) ((open_interval type-eq-decl nil intervals_real "reals/") (find_P_sec const-decl "{ii: below(length(P) - 1) | seq(P)(ii) <= xx AND xx <= seq(P)(ii + 1)}" integral_split_scaf nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (parts_disjoint formula-decl nil integral_def nil) (parts_order formula-decl nil integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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)) nil)) (F1_TCC1 0 (F1_TCC1-1 nil 3280167871 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (F1_TCC2 0 (F1_TCC2-1 nil 3280167872 ("" (skosimp*) (("" (lemma "connected_domain") (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil integral_split_scaf nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (F1_TCC3 0 (F1_TCC3-1 nil 3280167872 ("" (skosimp*) (("" (assert) nil nil)) nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (F1_TCC4 0 (F1_TCC4-1 nil 3280230046 ("" (skosimp*) (("" (assert) (("" (typepred "f!1") (("" (expand "bnded_on?") (("" (expand "bounded_on_all?") (("" (assert) (("" (expand "bounded_on?") (("" (skosimp*) (("" (inst + "B!1") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (typepred "x!2") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (a!1 skolem-const-decl "T" integral_split_scaf nil) (b!1 skolem-const-decl "{x: T | a!1 < x}" integral_split_scaf nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split_scaf nil) (j!1 skolem-const-decl "below(P!1`length - 1)" integral_split_scaf nil) (x!2 skolem-const-decl "closed_interval[T](P!1`seq(j!1), P!1`seq(1 + j!1))" integral_split_scaf nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bounded_on? const-decl "bool" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (< const-decl "bool" reals nil) (bnded_on? const-decl "bool" integral_bounded nil)) shostak)) (F1_TCC5 0 (F1_TCC5-1 nil 3280230046 ("" (skosimp*) (("" (typepred "f!1") (("" (expand "bnded_on?") (("" (expand "bounded_on?") (("" (expand "bounded_on_all?") (("" (skosimp*) (("" (expand "bounded_on?") (("" (assert) (("" (inst + "B!1") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (typepred "x!2") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bnded_on? const-decl "bool" integral_bounded nil) (< const-decl "bool" reals nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (bounded_on? const-decl "bool" integral_bounded nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (a!1 skolem-const-decl "T" integral_split_scaf nil) (b!1 skolem-const-decl "{x: T | a!1 < x}" integral_split_scaf nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split_scaf nil) (j!1 skolem-const-decl "below(P!1`length - 1)" integral_split_scaf nil) (x!2 skolem-const-decl "closed_interval[T](finseq_appl[closed_interval[T](a!1, b!1)](P!1)(j!1), finseq_appl[closed_interval[T](a!1, b!1)](P!1)(1 + j!1))" integral_split_scaf nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bounded_on_all? const-decl "bool" integral_bounded nil)) shostak)) (F1_F2_lem_TCC1 0 (F1_F2_lem_TCC1-1 nil 3280838608 ("" (skosimp*) (("" (expand "bnded_on?") (("" (lemma "integrable_bounded[T]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((bnded_on? const-decl "bool" integral_bounded nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integrable_bounded formula-decl nil integral_bounded 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]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil)) shostak)) (F1_F2_lem 0 (F1_F2_lem-3 nil 3306071410 ("" (skosimp*) (("" (prop) (("1" (expand "step_function_on?") (("1" (skosimp*) (("1" (expand "F1") (("1" (assert) (("1" (inst + "MINj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "se_not_on") (("2" (inst?) (("2" (inst -1 "ii!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "find_P_sec_in") (("3" (inst - "a!1" "b!1") (("3" (assert) (("3" (inst - "P!1") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (lemma "bnd_on_lem[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (expand "F2") (("2" (assert) (("2" (inst + "MAXj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "se_not_on") (("2" (inst?) (("2" (inst -1 "ii!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "find_P_sec_in") (("3" (inst - "a!1" "b!1") (("3" (assert) (("3" (inst - "P!1") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "bnd_on_lem[T]") (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (prop) (("1" (expand "F1") (("1" (assert) (("1" (lift-if) (("1" (lemma "MIN_ALL_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (ground) (("1" (lemma "MINj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (lemma "connected_domain") (("1" (lemma "integrable_bounded_on_all[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "F2") (("2" (assert) (("2" (lemma "MAX_ALL_lem[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("1" (inst?) (("1" (lift-if) (("1" (ground) (("1" (lemma "MAXj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (connected_domain formula-decl nil integral_split_scaf nil) (bnd_on_lem formula-decl nil integral_bounded nil) (integrable_bounded formula-decl nil integral_bounded nil) (NOT const-decl "[bool -> bool]" booleans nil) (open_interval type-eq-decl nil intervals_real "reals/") (find_P_sec_in formula-decl nil integral_split_scaf nil) (int_minus_int_is_int application-judgement "int" integers nil) (se_not_on formula-decl nil integral_split_scaf nil) (find_P_sec const-decl "{ii: below(length(P) - 1) | seq(P)(ii) <= xx AND xx <= seq(P)(ii + 1)}" integral_split_scaf nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (MINj const-decl "real" integral_bounded 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]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (a!1 skolem-const-decl "T" integral_split_scaf nil) (b!1 skolem-const-decl "T" integral_split_scaf nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (partition type-eq-decl nil integral_def nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split_scaf nil) (f!1 skolem-const-decl "[T -> real]" integral_split_scaf nil) (F1 const-decl "real" integral_split_scaf nil) (step_function_on? const-decl "bool" step_fun_def nil) (MAXj const-decl "real" integral_bounded nil) (F2 const-decl "real" integral_split_scaf nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (MIN_ALL_lem formula-decl nil integral_bounded nil) (integrable_bounded_on_all formula-decl nil integral_bounded nil) (MINj_lem formula-decl nil integral_bounded nil) (MAX_ALL_lem formula-decl nil integral_bounded nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (MAXj_lem formula-decl nil integral_bounded nil)) nil) (F1_F2_lem-2 nil 3282501343 ("" (skosimp*) (("" (prop) (("1" (expand "step_function_on?") (("1" (skosimp*) (("1" (expand "F1") (("1" (assert) (("1" (inst + "MINj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "se_not_on[T]") (("2" (inst?) (("2" (inst -1 "ii!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "find_P_sec_in[T]") (("3" (inst - "a!1" "b!1") (("3" (assert) (("3" (inst - "P!1") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (lemma "bnd_on_lem[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (expand "F2") (("2" (assert) (("2" (inst + "MAXj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "se_not_on[T]") (("2" (inst?) (("2" (inst -1 "ii!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "find_P_sec_in[T]") (("3" (inst - "a!1" "b!1") (("3" (assert) (("3" (inst - "P!1") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "bnd_on_lem[T]") (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (prop) (("1" (expand "F1") (("1" (assert) (("1" (lift-if) (("1" (lemma "MIN_ALL_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (ground) (("1" (lemma "MINj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (lemma "connected_domain") (("1" (lemma "integrable_bounded_on_all[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "F2") (("2" (assert) (("2" (lemma "MAX_ALL_lem[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("1" (inst?) (("1" (lift-if) (("1" (ground) (("1" (lemma "MAXj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bnd_on_lem formula-decl nil integral_bounded nil) (integrable_bounded formula-decl nil integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (partition type-eq-decl nil integral_def nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (step_function_on? const-decl "bool" step_fun_def nil) (MAXj const-decl "real" integral_bounded nil) (MIN_ALL_lem formula-decl nil integral_bounded nil) (integrable_bounded_on_all formula-decl nil integral_bounded nil) (MINj_lem formula-decl nil integral_bounded nil) (MAX_ALL_lem formula-decl nil integral_bounded nil) (MAXj_lem formula-decl nil integral_bounded nil)) nil) (F1_F2_lem-1 nil 3280168909 ("" (skosimp*) (("" (prop) (("1" (expand "step_function_on?") (("1" (skosimp*) (("1" (expand "F1") (("1" (assert) (("1" (inst + "MINj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("3" (lemma "find_P_sec_in[T]") (("1" (inst - "a!1" "b!1") (("1" (assert) (("1" (inst - "P!1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil) ("3" (lemma "integrable_bounded[T]") (("1" (inst?) (("1" (assert) (("1" (lemma "bnd_on_lem") (("1" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (expand "F2") (("2" (assert) (("2" (inst + "MAXj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("3" (lemma "find_P_sec_in[T]") (("1" (inst - "a!1" "b!1") (("1" (assert) (("1" (inst - "P!1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil) ("3" (lemma "bnd_on_lem") (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) (("3" (hide 2) (("3" (lemma "integrable_bounded[T]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (prop) (("1" (expand "F1") (("1" (assert) (("1" (lift-if) (("1" (lemma "MIN_ALL_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (ground) (("1" (lemma "MINj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (lemma "connected_domain") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "integrable_bounded_on_all") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "F2") (("2" (assert) (("2" (lemma "MAX_ALL_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (lift-if) (("1" (ground) (("1" (lemma "MAXj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil) ("3" (lemma "integrable_bounded_on_all") (("3" (inst?) (("3" (assert) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable_bounded formula-decl nil integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (partition type-eq-decl nil integral_def nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (step_function_on? const-decl "bool" step_fun_def nil) (MAXj const-decl "real" integral_bounded nil) (MIN_ALL_lem formula-decl nil integral_bounded nil) (MINj_lem formula-decl nil integral_bounded nil) (MAX_ALL_lem formula-decl nil integral_bounded nil) (MAXj_lem formula-decl nil integral_bounded nil)) shostak)) (epsilon_is_0 0 (epsilon_is_0-2 nil 3276521074 ("" (skosimp*) (("" (inst - "abs(xv!1)/2") (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (xv!1 skolem-const-decl "real" integral_split_scaf nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil) (epsilon_is_0-1 nil 3276519779 ("" (skosimp*) (("" (inst - "abs(x!1)/2") (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) nil shostak)) (F2_F1_step_function_on 0 (F2_F1_step_function_on-2 nil 3306071464 ("" (skosimp*) (("" (assert) (("" (lemma "F1_F2_lem") (("" (inst?) (("" (assert) (("" (inst?) (("" (flatten) (("" (lemma "diff_step_is_step_on") (("" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (inst - "P!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (expand "bnded_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers 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) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (diff_step_is_step_on formula-decl nil integral_split_scaf nil) (bnded_on? const-decl "bool" integral_bounded nil) (F2 const-decl "real" integral_split_scaf nil) (F1 const-decl "real" integral_split_scaf nil) (F1_F2_lem formula-decl nil integral_split_scaf nil)) nil) (F2_F1_step_function_on-1 nil 3280836351 ("" (skosimp*) (("" (assert) (("" (lemma "F1_F2_lem") (("" (inst?) (("" (assert) (("" (inst?) (("" (flatten) (("" (lemma "diff_step_is_step_on[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (inst - "P!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (expand "bnded_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def nil) (integrable_bounded formula-decl nil integral_bounded nil) (bnded_on? const-decl "bool" integral_bounded nil)) shostak)) (integrable_F2_F1 0 (integrable_F2_F1-1 nil 3280247387 ("" (skosimp*) (("" (assert) (("" (case "bnded_on?(a!1, b!1)(f!1)") (("1" (lemma "F2_F1_step_function_on") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (lemma "step_function_integrable?[T]") (("1" (inst - "a!1" "b!1" "F2(a!1, b!1, P!1, f!1) - F1(a!1, b!1, P!1, f!1)") (("1" (assert) (("1" (hide 2) (("1" (expand "step_function?") (("1" (inst + "P!1") (("1" (expand "step_function_on?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (expand "bnded_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integrable_bounded formula-decl nil integral_bounded nil) (F2_F1_step_function_on formula-decl nil integral_split_scaf nil) (F1 const-decl "real" integral_split_scaf nil) (F2 const-decl "real" integral_split_scaf nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (step_function? const-decl "bool" step_fun_def nil) (step_function_integrable? formula-decl nil integral_step nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers 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]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (bnded_on? const-decl "bool" integral_bounded nil)) shostak)) (integral_F2_F1_TCC1 0 (integral_F2_F1_TCC1-1 nil 3280246825 ("" (skosimp*) (("" (lemma "integrable_F2_F1") (("" (inst?) (("" (assert) (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((integrable_F2_F1 formula-decl nil integral_split_scaf nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (integral_F2_F1_TCC2 0 (integral_F2_F1_TCC2-1 nil 3280246831 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (width const-decl "posreal" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (integral_F2_F1_TCC3 0 (integral_F2_F1_TCC3-1 nil 3280246855 ("" (subtype-tcc) (("" (postpone) nil nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real_ge_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) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (width const-decl "posreal" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (integral_F2_F1_TCC4 0 (integral_F2_F1_TCC4-1 nil 3280246861 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (width const-decl "posreal" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (integral_F2_F1_TCC5 0 (integral_F2_F1_TCC5-1 nil 3280246866 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (integral_F2_F1_TCC6 0 (integral_F2_F1_TCC6-1 nil 3280246873 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (width const-decl "posreal" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (integral_F2_F1_TCC7 0 (integral_F2_F1_TCC7-1 nil 3280576649 ("" (skosimp*) (("" (lemma "integrable_bounded_on_all[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil) ((T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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_bounded_on_all formula-decl nil integral_bounded nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil)) shostak)) (integral_F2_F1_TCC8 0 (integral_F2_F1_TCC8-1 nil 3280576649 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (integral_F2_F1 0 (integral_F2_F1-3 nil 3306071727 ("" (skosimp*) (("" (assert) (("" (lemma "connected_domain") (("" (case "bnded_on?(a!1, b!1)(f!1)") (("1" (lemma "step_function_on_integral[T]") (("1" (assert) (("1" (inst - "a!1" "b!1" "F2(a!1, b!1, P!1, f!1) - F1(a!1, b!1, P!1, f!1)") (("1" (assert) (("1" (inst - "P!1") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_restrict_eq[below(length(P!1)-1)]") (("1" (hide 2) (("1" (expand "restrict") (("1" (apply-extensionality 1 :hide? t) (("1" (expand "val_in") (("1" (typepred "pick(a!1, b!1, P!1, x!1)") (("1" (case "bounded_on_all?[T](a!1, b!1, P!1)(f!1)") (("1" (case-replace "(F2(a!1, b!1, P!1, f!1) - F1(a!1, b!1, P!1, f!1)) (pick(a!1, b!1, P!1, x!1)) = MAXj(a!1, b!1, P!1, x!1, f!1) - MINj(a!1, b!1, P!1, x!1, f!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (name-replace "MM" "pick(a!1, b!1, P!1, x!1)") (("2" (expand "-") (("2" (expand "F2") (("2" (expand "F1") (("2" (assert) (("2" (case "MM /= P!1`seq(find_P_sec(a!1, b!1, P!1, MM))") (("1" (case "MM /= P!1`seq(1 + find_P_sec(a!1, b!1, P!1, MM))") (("1" (flatten) (("1" (assert) (("1" (case "find_P_sec(a!1, b!1, P!1, MM) = x!1") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 4) (("2" (typepred "find_P_sec(a!1, b!1, P!1, MM)") (("2" (name-replace "IM" "find_P_sec(a!1, b!1, P!1, MM)") (("2" (lemma "part_not_in[T]") (("2" (inst - "a!1" "b!1" "MM") (("2" (assert) (("2" (inst?) (("2" (inst - "IM") (("2" (lemma "parts_disjoint[T]") (("2" (inst - "a!1" "b!1" "MM" "P!1" "x!1" "IM") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (hide 1) (("2" (typepred "MM") (("2" (hide -5) (("2" (name-replace "IM" "find_P_sec(a!1, b!1, P!1, MM)") (("2" (assert) (("2" (lemma "part_not_in[T]") (("2" (inst - "a!1" "b!1" "MM") (("2" (assert) (("2" (inst - "P!1" "x!1" "1+IM") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (lemma "part_not_in[T]") (("2" (inst - "a!1" "b!1" "MM") (("2" (assert) (("2" (inst - "P!1" "x!1" "find_P_sec(a!1, b!1, P!1, MM)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "F2_F1_step_function_on") (("2" (inst - "a!1" "b!1" "f!1") (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (expand "bnded_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (bnded_on? const-decl "bool" integral_bounded nil) (f!1 skolem-const-decl "[T -> real]" integral_split_scaf nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split_scaf nil) (b!1 skolem-const-decl "T" integral_split_scaf nil) (a!1 skolem-const-decl "T" integral_split_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (pick const-decl "{t: T | seq(P)(j) < t AND t < seq(P)(j + 1)}" integral_step nil) (integrable_bounded_on_all formula-decl nil integral_bounded nil) (parts_disjoint formula-decl nil integral_def nil) (part_not_in formula-decl nil integral_def nil) (find_P_sec const-decl "{ii: below(length(P) - 1) | seq(P)(ii) <= xx AND xx <= seq(P)(ii + 1)}" integral_split_scaf nil) (/= const-decl "boolean" notequal nil) (restrict const-decl "[T -> real]" sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_restrict_eq formula-decl nil sigma "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (val_in const-decl "real" integral_step nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (MAXj const-decl "real" integral_bounded nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (F2_F1_step_function_on formula-decl nil integral_split_scaf nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (F2 const-decl "real" integral_split_scaf nil) (F1 const-decl "real" integral_split_scaf nil) (step_function_on_integral formula-decl nil integral_step nil) (integrable_bounded formula-decl nil integral_bounded nil) (connected_domain formula-decl nil integral_split_scaf nil)) nil) (integral_F2_F1-2 nil 3280831713 ("" (skosimp*) (("" (assert) (("" (lemma "connected_domain") (("" (case "bnded_on?(a!1, b!1)(f!1)") (("1" (lemma "step_function_on_integral[T]") (("1" (assert) (("1" (inst - "a!1" "b!1" "F2(a!1, b!1, P!1, f!1) - F1(a!1, b!1, P!1, f!1)") (("1" (assert) (("1" (inst - "P!1") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_restrict_eq[below(length(P!1)-1)]") (("1" (hide 2) (("1" (expand "restrict") (("1" (apply-extensionality 1 :hide? t) (("1" (expand "val_in") (("1" (typepred "pick(a!1, b!1, P!1, x!1)") (("1" (case "bounded_on_all?[T](a!1, b!1, P!1)(f!1)") (("1" (case-replace "(F2(a!1, b!1, P!1, f!1) - F1(a!1, b!1, P!1, f!1)) (pick(a!1, b!1, P!1, x!1)) = MAXj(a!1, b!1, P!1, x!1, f!1) - MINj(a!1, b!1, P!1, x!1, f!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (name-replace "MM" "pick(a!1, b!1, P!1, x!1)") (("2" (expand "-") (("2" (expand "F2") (("2" (expand "F1") (("2" (assert) (("2" (case "MM /= P!1`seq(find_P_sec(a!1, b!1, P!1, MM))") (("1" (case "MM /= P!1`seq(1 + find_P_sec(a!1, b!1, P!1, MM))") (("1" (flatten) (("1" (assert) (("1" (case "find_P_sec[T](a!1, b!1, P!1, MM) = x!1") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 4) (("2" (typepred "find_P_sec[T](a!1, b!1, P!1, MM)") (("2" (name-replace "IM" "find_P_sec[T](a!1, b!1, P!1, MM)") (("2" (lemma "part_not_in[T]") (("2" (inst - "a!1" "b!1" "MM") (("2" (assert) (("2" (inst?) (("2" (inst - "IM") (("2" (lemma "parts_disjoint[T]") (("2" (inst - "a!1" "b!1" "MM" "P!1" "x!1" "IM") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (hide 1) (("2" (typepred "MM") (("2" (hide -5) (("2" (name-replace "IM" "find_P_sec[T](a!1, b!1, P!1, MM)") (("2" (assert) (("2" (lemma "part_not_in[T]") (("2" (inst - "a!1" "b!1" "MM") (("2" (assert) (("2" (inst - "P!1" "x!1" "1+IM") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (lemma "part_not_in[T]") (("2" (inst - "a!1" "b!1" "MM") (("2" (assert) (("2" (inst - "P!1" "x!1" "find_P_sec(a!1, b!1, P!1, MM)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "F2_F1_step_function_on") (("2" (inst - "a!1" "b!1" "f!1") (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (expand "bnded_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable_bounded formula-decl nil integral_bounded nil) (step_function_on_integral formula-decl nil integral_step nil) (partition type-eq-decl nil integral_def nil) (sigma_restrict_eq formula-decl nil sigma "reals/") (val_in const-decl "real" integral_step nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (MAXj const-decl "real" integral_bounded nil) (restrict const-decl "[T -> real]" sigma "reals/") (part_not_in formula-decl nil integral_def nil) (parts_disjoint formula-decl nil integral_def nil) (integrable_bounded_on_all formula-decl nil integral_bounded nil) (pick const-decl "{t: T | seq(P)(j) < t AND t < seq(P)(j + 1)}" integral_step nil) (bnded_on? const-decl "bool" integral_bounded nil)) nil) (integral_F2_F1-1 nil 3280768358 ("" (skosimp*) (("" (assert) (("" (lemma "connected_domain") (("" (case "bnded_on?(a!1, b!1)(f!1)") (("1" (lemma "step_function_on_integral[T]") (("1" (assert) (("1" (inst - "a!1" "b!1" "F2(a!1, b!1, P!1, f!1) - F1(a!1, b!1, P!1, f!1)") (("1" (assert) (("1" (inst - "P!1") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_restrict_eq[below(length(P!1)-1)]") (("1" (hide 2) (("1" (expand "restrict") (("1" (apply-extensionality 1 :hide? t) (("1" (expand "val_in") (("1" (typepred "pick(a!1, b!1, P!1, x!1)") (("1" (case "bounded_on_all?[T](a!1, b!1, P!1)(f!1)") (("1" (case-replace "(F2(a!1, b!1, P!1, f!1) - F1(a!1, b!1, P!1, f!1)) (pick(a!1, b!1, P!1, x!1)) = MAXj(a!1, b!1, P!1, x!1, f!1) - MINj(a!1, b!1, P!1, x!1, f!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (name-replace "MM" "pick(a!1, b!1, P!1, x!1)") (("2" (expand "-") (("2" (expand "F2") (("2" (expand "F1") (("2" (assert) (("2" (case "MM /= P!1`seq(find_P_sec(a!1, b!1, P!1, MM))") (("1" (case "MM /= P!1`seq(1 + find_P_sec(a!1, b!1, P!1, MM))") (("1" (flatten) (("1" (assert) (("1" (case "find_P_sec[T](a!1, b!1, P!1, MM) = x!1") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide 4) (("2" (typepred "find_P_sec[T](a!1, b!1, P!1, MM)") (("2" (name-replace "IM" "find_P_sec[T](a!1, b!1, P!1, MM)") (("2" (lemma "part_not_in[T]") (("2" (inst - "a!1" "b!1" "MM") (("2" (assert) (("2" (inst?) (("2" (inst - "IM") (("2" (lemma "parts_disjoint[T]") (("2" (inst - "a!1" "b!1" "MM" "P!1" "x!1" "IM") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (hide 1) (("2" (typepred "MM") (("2" (hide -5) (("2" (name-replace "IM" "find_P_sec[T](a!1, b!1, P!1, MM)") (("2" (assert) (("2" (lemma "part_not_in[T]") (("2" (inst - "a!1" "b!1" "MM") (("2" (assert) (("2" (inst - "P!1" "x!1" "1+IM") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (lemma "part_not_in[T]") (("2" (inst - "a!1" "b!1" "MM") (("2" (assert) (("2" (inst - "P!1" "x!1" "find_P_sec(a!1, b!1, P!1, MM)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (hide 2) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "F2_F1_step_function_on") (("2" (inst - "a!1" "b!1" "f!1") (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_bounded[T]") (("1" (inst?) (("1" (assert) (("1" (expand "bnded_on?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((parts_disjoint formula-decl nil integral_def nil) (part_not_in formula-decl nil integral_def nil) (restrict const-decl "[T -> real]" sigma "reals/") (sigma_restrict_eq formula-decl nil sigma "reals/") (partition type-eq-decl nil integral_def nil)) shostak)) (se_prep 0 (se_prep-1 nil 3280588756 ("" (skosimp*) (("" (prop) (("1" (expand "MINj") (("1" (name-replace "GLB" " glb({fx: real | EXISTS (xx: T): P!1`seq(j!1) <= xx AND xx <= P!1`seq(1 + j!1) AND fx = f!1(xx)})") (("1" (typepred "GLB") (("1" (expand "greatest_lower_bound?") (("1" (flatten) (("1" (inst -2 "GLB+nu!1") (("1" (assert) (("1" (expand "lower_bound?") (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (replace -3) (("1" (hide -3) (("1" (inst + "xx!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "f!1(P!1`seq(j!1))") (("1" (inst?) (("1" (assert) (("1" (typepred "P!1") (("1" (assert) (("1" (inst - "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "f!1") (("2" (lemma "bounded_on_all_is[T]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (split -1) (("1" (hide -2) (("1" (expand "bounded_on?") (("1" (skosimp*) (("1" (expand "bounded_below?") (("1" (inst + "-B!1") (("1" (expand "lower_bound?") (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (inst - "xx!1") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "MAXj") (("2" (name-replace "LUB" " lub({fx: real | EXISTS (xx: T): P!1`seq(j!1) <= xx AND xx <= P!1`seq(1 + j!1) AND fx = f!1(xx)}) ") (("1" (typepred "LUB") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst -2 "LUB-nu!1") (("1" (assert) (("1" (expand "upper_bound?") (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (replace -3) (("1" (hide -3) (("1" (inst + "xx!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "f!1(P!1`seq(j!1))") (("1" (inst?) (("1" (assert) (("1" (typepred "P!1") (("1" (assert) (("1" (inst - "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "f!1") (("2" (lemma "bounded_on_all_is[T]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (split -1) (("1" (hide -2) (("1" (expand "bounded_on?") (("1" (skosimp*) (("1" (expand "bounded_above?") (("1" (inst + "B!1") (("1" (expand "upper_bound?") (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (inst - "xx!1") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (greatest_lower_bound? const-decl "bool" bounded_real_defs nil) (glb const-decl "{x | greatest_lower_bound?(x, SB)}" bounded_real_defs nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (lower_bound? const-decl "bool" bounded_real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (a!1 skolem-const-decl "T" integral_split_scaf nil) (b!1 skolem-const-decl "T" integral_split_scaf nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split_scaf nil) (j!1 skolem-const-decl "below(length(P!1) - 1)" integral_split_scaf nil) (xx!1 skolem-const-decl "T" integral_split_scaf nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (bounded_on_all_is formula-decl nil integral_bounded nil) (bounded_on? const-decl "bool" integral_bounded nil) (xx!1 skolem-const-decl "T" integral_split_scaf nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (MINj const-decl "real" integral_bounded nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (xx!1 skolem-const-decl "T" integral_split_scaf nil) (xx!1 skolem-const-decl "T" integral_split_scaf nil) (MAXj const-decl "real" integral_bounded nil)) shostak)) (get_xp_TCC1 0 (get_xp_TCC1-1 nil 3280255370 ("" (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)) shostak)) (get_xp_TCC2 0 (get_xp_TCC2-1 nil 3280255370 ("" (skosimp*) (("" (assert) (("" (typepred "P!1") (("" (inst?) nil nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (get_xp_TCC3 0 (get_xp_TCC3-3 nil 3374402052 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, P: partition[T](a, b), (bounded_on_all?[T](a, b, P)), below(length(P) - 1), posreal]): choose({xp: closed_interval[T](d`3`seq(d`5), d`3`seq(1 + d`5)) | d`4(xp) < MINj[T](d`1, d`2, d`3, d`5, d`4) + d`6}))") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (grind :if-match nil) (("3" (lemma "se_prep") (("3" (inst - "d!1`1" "d!1`2") (("3" (assert) (("3" (assert) (("3" (typepred "d!1`2") (("3" (inst?) (("3" (inst - "d!1`6") (("3" (flatten) (("3" (skosimp*) (("3" (hide -4) (("3" (inst - "xp!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (se_prep formula-decl nil integral_split_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (MINj const-decl "real" integral_bounded nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (bounded_on_all? const-decl "bool" integral_bounded nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil integral_def nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (T formal-subtype-decl nil integral_split_scaf nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil) (get_xp_TCC3-2 "GET PAST PVS3.2 bug" 3308650227 ("" (name "A" "1") (("" (postpone) nil nil)) nil) nil shostak) (get_xp_TCC3-1 nil 3280255370 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, P: partition[T](a, b), (bounded_on_all?[T](a, b, P)), below(length(P) - 1), posreal]): choose({xp: closed_interval[T](d`3`seq(d`5), d`3`seq(1 + d`5)) | d`4(xp) < MINj[T](d`1, d`2, d`3, d`5, d`4) + d`6}))") (("1" (skosimp*) (("1" (lemma "se_prep") (("1" (inst - "d!1`1" "d!1`2") (("1" (assert) (("1" (typepred "d!1`2") (("1" (assert) (("1" (inst?) (("1" (inst - "d!1`6") (("1" (flatten) (("1" (skosimp*) (("1" (hide -4) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "xp!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (skosimp*) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ((MINj const-decl "real" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (partition type-eq-decl nil integral_def nil)) shostak)) (get_xpp_TCC1 0 (get_xpp_TCC1-5 nil 3374402219 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, P: partition[T](a, b), (bounded_on_all?[T](a, b, P)), below(length(P) - 1), posreal]): choose({xpp: closed_interval[T](d`3`seq(d`5), d`3`seq(1 + d`5)) | d`4(xpp) > MAXj[T](d`1, d`2, d`3, d`5, d`4) - d`6}))") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (lemma "se_prep") (("3" (inst - "d!1`1" "d!1`2") (("3" (assert) (("3" (assert) (("3" (typepred "d!1`2") (("3" (inst?) (("3" (flatten) (("3" (skosimp*) (("3" (hide -3) (("3" (expand "nonempty?") (("3" (expand "empty?") (("3" (expand "member") (("3" (inst - "xpp!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (se_prep formula-decl nil integral_split_scaf 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (MAXj const-decl "real" integral_bounded nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (bounded_on_all? const-decl "bool" integral_bounded nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (partition type-eq-decl nil integral_def nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (T formal-subtype-decl nil integral_split_scaf nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (get_xpp_TCC1-4 "GET PAST PVS3.2 bug" 3308650295 ("" (name "A" "1") (("" (postpone) nil nil)) nil) nil shostak) (get_xpp_TCC1-3 nil 3280591908 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, P: partition[T](a, b), (bounded_on_all?[T](a, b, P)), below(length(P) - 1), posreal]): choose({xpp: closed_interval[T](d`3`seq(d`5), d`3`seq(1 + d`5)) | d`4(xpp) > MAXj[T](d`1, d`2, d`3, d`5, d`4) - d`6}))") (("1" (skosimp*) (("1" (lemma "se_prep") (("1" (inst - "d!1`1" "d!1`2") (("1" (assert) (("1" (typepred "d!1`2") (("1" (assert) (("1" (inst?) (("1" (flatten) (("1" (skosimp*) (("1" (hide -3) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "xpp!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ((MAXj const-decl "real" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (partition type-eq-decl nil integral_def nil)) nil) (get_xpp_TCC1-2 nil 3280590849 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, P: partition[T](a, b), (bounded_on_all?[T](a, b, P)), below(length(P) - 1), posreal]): choose({xpp: closed_interval[T](d`3`seq(d`5), d`3`seq(1 + d`5)) | d`4(xpp) > MAXj[T](d`1, d`2, d`3, d`5, d`4) + d`6}))") (("1" (skosimp*) (("1" (lemma "se_prep") (("1" (inst - "d!1`1" "d!1`2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (skosimp*) (("2" (hide -1) (("2" (lemma "se_prep") (("2" (inst - "d!1`1" "d!1`2") (("2" (typepred "d!1`2") (("2" (assert) (("2" (inst?) (("2" (inst - "d!1`6") (("2" (flatten) (("2" (skosimp*) (("2" (hide -3) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "xpp!1") (("2" (assert) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil) nil nil) (get_xpp_TCC1-1 nil 3280255370 ("" (postpone) nil nil) nil shostak)) (lt_via_epsi 0 (lt_via_epsi-1 nil 3280256580 ("" (skosimp*) (("" (inst - "x!1-a!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (> const-decl "bool" reals nil) (a!1 skolem-const-decl "real" integral_split_scaf nil) (x!1 skolem-const-decl "real" integral_split_scaf nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_all_parts_TCC1 0 (sigma_all_parts_TCC1-1 nil 3280576649 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_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)) shostak)) (sigma_all_parts_TCC2 0 (sigma_all_parts_TCC2-1 nil 3280576649 ("" (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sigma_all_parts_TCC3 0 (sigma_all_parts_TCC3-1 nil 3280576649 ("" (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)) shostak)) (sigma_all_parts_TCC4 0 (sigma_all_parts_TCC4-1 nil 3280576649 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sigma_all_parts_TCC5 0 (sigma_all_parts_TCC5-1 nil 3280576649 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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)) shostak)) (sigma_all_parts 0 (sigma_all_parts-1 nil 3280592990 ("" (skosimp*) (("" (case "FORALL (n: below(length(P!1) - 1)): sigma(0, n, LAMBDA (j: below(length(P!1) - 1)): P!1`seq(1 + j) - P!1`seq(j)) = P!1`seq(1+n) - a!1 ") (("1" (inst - "length(P!1) - 2") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (assert) (("1" (expand "sigma") (("1" (assert) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) 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) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (below type-eq-decl nil nat_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_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) (a!1 skolem-const-decl "T" integral_split_scaf nil) (b!1 skolem-const-decl "T" integral_split_scaf nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split_scaf nil) (pred type-eq-decl nil defined_types nil) (below_induction formula-decl nil bounded_nat_inductions nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_0_neg formula-decl nil sigma_below "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (steps_exist 0 (steps_exist-5 nil 3306071816 ("" (auto-rewrite "xis?") (("" (auto-rewrite "xis_lem") (("" (skosimp*) (("" (lemma "connected_domain") (("" (lemma "Lemma_1[T]") (("" (inst?) (("" (assert) (("" (inst - "eps!1/2") (("" (skosimp*) (("" (name "EP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)") (("1" (case "bnded_on?(a!1, b!1)(f!1)") (("1" (inst + "F1(a!1,b!1,EP,f!1)" "F2(a!1,b!1,EP,f!1)") (("1" (lemma "F1_F2_lem") (("1" (inst?) (("1" (assert) (("1" (inst - "EP") (("1" (flatten) (("1" (case-replace " step_function?(a!1, b!1, F1(a!1, b!1, EP, f!1)) AND step_function?(a!1, b!1, F2(a!1, b!1, EP, f!1))") (("1" (flatten) (("1" (hide -3 -4) (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (lemma "integrable_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (case-replace "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) <= eps!1/2") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "lt_via_epsi") (("2" (inst - "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1))" "eps!1 / 2") (("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (name "NU" "epsi!1/(2*(b!1 - a!1))") (("2" (case "NU > 0") (("1" (case "bounded_on_all?[T](a!1, b!1, EP)(f!1)") (("1" (name "XP" "(LAMBDA (j: below(length(EP) - 1)): get_xp(a!1,b!1,EP,f!1,j,NU))") (("1" (name "XPP" "(LAMBDA (j: below(length(EP) - 1)): get_xpp(a!1,b!1,EP,f!1,j,NU))") (("1" (inst - "EP" "EP" "XPP" "XP") (("1" (assert) (("1" (case "width(a!1, b!1, EP) < delta!1") (("1" (assert) (("1" (expand "Rie_sum") (("1" (assert) (("1" (lemma "integral_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (rewrite "sigma_minus[below(length(EP) - 1)]") (("1" (case "sigma(0, length(EP) - 2, LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XP(i)) + EP`seq(1 + i) * f!1(XPP(i)) - EP`seq(i) * f!1(XPP(i)) - EP`seq(1 + i) * f!1(XP(i))) > sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2*NU) * (EP`seq(j+1) - EP`seq(j)))") (("1" (case-replace "sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j))) = integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1) (("1" (hide -1) (("1" (case "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) - 2 * NU * (b!1 - a!1) < eps!1 / 2") (("1" (assert) (("1" (cross-mult -9) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (hide -1 2) (("2" (replace -1) (("2" (hide-all-but 1) (("2" (lemma "sigma_sum[below(length(EP) - 1)]") (("2" (inst - "(LAMBDA (j: below(length(EP) - 1)): 2 * (EP`seq(j) * NU) - 2 * (EP`seq(1 + j) * NU))" "(LAMBDA (j: below(length(EP) - 1)): (EP`seq(j) * MINj(a!1, b!1, EP, j, f!1) - EP`seq(1 + j) * MINj(a!1, b!1, EP, j, f!1)) + (EP`seq(1 + j) * MAXj(a!1, b!1, EP, j, f!1) - EP`seq(j) * MAXj(a!1, b!1, EP, j, f!1)))" "length(EP) - 2" "0") (("2" (replace -1 * rl) (("2" (hide -1) (("2" (assert) (("2" (lemma "sigma_all_parts") (("2" (inst - "a!1" "b!1") (("2" (assert) (("2" (inst?) (("2" (lemma "sigma_scal[below(length(EP) - 1)]") (("2" (inst?) (("2" (inst - "-2*NU") (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (case "FORALL (i: below(length(EP) - 1)): f!1(XP(i)) < MINj(a!1, b!1, EP, i, f!1) + NU") (("1" (case "FORALL (i: below(length(EP) - 1)): f!1(XPP(i)) > MAXj(a!1, b!1, EP, i, f!1) - NU") (("1" (hide -4 -5) (("1" (hide -3 -5 -6 -7 -8) (("1" (lemma "sigma_lt[below(length(EP) -1)]") (("1" (inst - "(LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j)))" "(LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XP(i)) + EP`seq(1 + i) * f!1(XPP(i)) - EP`seq(i) * f!1(XPP(i)) - EP`seq(1 + i) * f!1(XP(i)))" "length(EP) - 2" "0") (("1" (assert) (("1" (hide 2) (("1" (case "length(EP) > 2") (("1" (assert) (("1" (skosimp*) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (case "f!1(XPP(n!1)) - f!1(XP(n!1)) > MAXj(a!1, b!1, EP, n!1, f!1) - MINj(a!1, b!1, EP, n!1, f!1) - 2*N (("1" (mult-by -1 "EP`seq(n!1+1) - EP`seq(n!1)") (("1" (assert) nil nil) ("2" (typepred "EP") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal 2) (("2" (typepred "EP") (("2" (rewrite "sigma_rew" 1) (("2" (lemma "sigma_rew[below(length(EP) - 1)]") (("2" (inst - "(LAMBDA (j: below(length(EP) - 1)): 2 * (EP`seq(j) * NU) - 2 * (EP`seq(1 + j) * NU) + (EP`seq(j) * MINj(a!1, b!1, EP, j, f!1) - EP`seq(1 + j) * MINj(a!1, b!1, EP, j, f!1)) + (EP`seq(1 + j) * MAXj(a!1, b!1, EP, j, f!1) - EP`seq(j) * MAXj(a!1, b!1, EP, j, f!1)))" "length(EP) - 2" "0") (("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (inst - "0") (("2" (inst - "0") (("2" (case "f!1(XPP(0)) - f!1(XP(0)) > MAXj(a!1, b!1, EP, 0, f!1) - MINj(a!1, b!1, EP, 0, f!1) - 2*NU ") (("1" (mult-by -1 "EP`seq(1) - EP`seq(0)") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -3 * rl) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -9 2) (("2" (replace -3 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma " N_from_delta[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (hide -1 -2) (("2" (prop) (("1" (skosimp*) (("1" (typepred "get_xpp(a!1, b!1, EP, f!1, x1!1, NU)") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "get_xp(a!1, b!1, EP, f!1, ii!1, NU)") (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide 2) (("3" (assert) (("3" (hide -1 -2) (("3" (prop) (("1" (skosimp*) (("1" (typepred "get_xp(a!1, b!1, EP, f!1, x1!1, NU)") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (typepred "get_xp(a!1, b!1, EP, f!1, ii!1, NU)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) nil nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (replace -1 * rl) (("2" (cross-mult 1) 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) (("2" (hide 2) (("2" (hide -3 -4 -5 -6 -7 -8 -9) (("2" (split +) (("1" (expand "step_function?") (("1" (inst?) nil nil)) nil) ("2" (expand "step_function?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bnded_on?") (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case-replace "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil integral_split_scaf nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integrable_bounded formula-decl nil integral_bounded nil) (a!1 skolem-const-decl "T" integral_split_scaf nil) (b!1 skolem-const-decl "T" integral_split_scaf nil) (f!1 skolem-const-decl "[T -> real]" integral_split_scaf nil) (F2 const-decl "real" integral_split_scaf nil) (F1 const-decl "real" integral_split_scaf nil) (partition type-eq-decl nil integral_def nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (step_function? const-decl "bool" step_fun_def nil) (integrable_F2_F1 formula-decl nil integral_split_scaf nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_via_epsi formula-decl nil integral_split_scaf nil) (integrable_bounded_on_all formula-decl nil integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (get_xp const-decl "{xp: closed_interval[T](P`seq(j), P`seq(j + 1)) | f(xp) < MINj(a, b, P, j, f) + nu}" integral_split_scaf nil) (EP skolem-const-decl "{fs: finite_sequence[{x | a!1 <= x AND x <= b!1}] | length(fs) > 1 AND seq(fs)(0) = a!1 AND seq(fs)(length(fs) - 1) = b!1 AND (FORALL (ii: below(length(fs) - 1)): seq(fs)(ii) < seq(fs)(1 + ii))}" integral_split_scaf nil) (NU skolem-const-decl "nzreal" integral_split_scaf nil) (XPP skolem-const-decl "[j: below(length(EP) - 1) -> {xpp: closed_interval[T](EP`seq(j), EP`seq(1 + j)) | f!1(xpp) > MAXj(a!1, b!1, EP, j, f!1) - NU}]" integral_split_scaf nil) (XP skolem-const-decl "[j: below(length(EP) - 1) -> {xp: closed_interval[T](EP`seq(j), EP`seq(1 + j)) | f!1(xp) < MINj(a!1, b!1, EP, j, f!1) + NU}]" integral_split_scaf nil) (xis? const-decl "bool" integral_def nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (width const-decl "posreal" integral_def nil) (Rie_sum const-decl "real" integral_def nil) (integral_F2_F1 formula-decl nil integral_split_scaf nil) (real_plus_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma_minus formula-decl nil sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_lt formula-decl nil sigma "reals/") (subrange type-eq-decl nil integers nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (n!1 skolem-const-decl "subrange(0, length(EP) - 2)" integral_split_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (sigma_rew formula-decl nil sigma "reals/") (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (sigma_all_parts formula-decl nil integral_split_scaf nil) (sigma_scal formula-decl nil sigma "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (sigma_sum formula-decl nil sigma "reals/") (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (sigma def-decl "real" sigma "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (N_from_delta formula-decl nil integral_def nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (get_xpp const-decl "{xpp: closed_interval[T](P`seq(j), P`seq(j + 1)) | f(xpp) > MAXj(a, b, P, j, f) - nu}" integral_split_scaf nil) (MAXj const-decl "real" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (F1_F2_lem formula-decl nil integral_split_scaf nil) (bnded_on? const-decl "bool" integral_bounded nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (Lemma_1 formula-decl nil integral_prep 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]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil)) nil) (debug3p2 "Debug PVS 3.2" 3303221484 ("" (skosimp*) (("" (lemma "connected_domain") (("" (lemma "Lemma_1[T]") (("" (inst?) (("" (assert) (("" (inst - "eps!1/2") (("" (skosimp*) (("" (name "EP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)") (("1" (case "bnded_on?(a!1, b!1)(f!1)") (("1" (inst + "F1(a!1,b!1,EP,f!1)" "F2(a!1,b!1,EP,f!1)") (("1" (lemma "F1_F2_lem") (("1" (inst?) (("1" (assert) (("1" (inst - "EP") (("1" (flatten) (("1" (case-replace " step_function?(a!1, b!1, F1(a!1, b!1, EP, f!1)) AND step_function?(a!1, b!1, F2(a!1, b!1, EP, f!1))") (("1" (flatten) (("1" (hide -3 -4) (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (lemma "integrable_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (case-replace "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) <= eps!1/2") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "lt_via_epsi[T]") (("2" (inst - "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1))" "eps!1 / 2") (("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (name "NU" "epsi!1/(2*(b!1 - a!1))") (("2" (case "NU > 0") (("1" (case "bounded_on_all?[T](a!1, b!1, EP)(f!1)") (("1" (name "XP" "(LAMBDA (j: below(length(EP) - 1)): get_xp(a!1,b!1,EP,f!1,j,NU))") (("1" (name "XPP" "(LAMBDA (j: below(length(EP) - 1)): get_xpp(a!1,b!1,EP,f!1,j,NU))") (("1" (inst - "EP" "EP" "XPP" "XP") (("1" (assert) (("1" (case "width(a!1, b!1, EP) < delta!1") (("1" (assert) (("1" (expand "Rie_sum") (("1" (assert) (("1" (assert) (("1" (lemma "integral_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (rewrite "sigma_minus[below(length(EP) - 1)]") (("1" (case "sigma(0, length(EP) - 2, LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XP(i)) + EP`seq(1 + i) * f!1(XPP(i)) - EP`seq(i) * f!1(XPP(i)) - EP`seq(1 + i) * f!1(XP(i))) > sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2*NU) * (EP`seq(j+1) - EP`seq(j)))") (("1" (case-replace "sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j))) = integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1) (("1" (hide -1) (("1" (case "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) - 2 * NU * (b!1 - a!1) < eps!1 / 2") (("1" (assert) (("1" (cross-mult -9) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (hide -1 2) (("2" (replace -1) (("2" (hide-all-but 1) (("2" (lemma "sigma_sum[below(length(EP) - 1)]") (("2" (inst - "(LAMBDA (j: below(length(EP) - 1)): 2 * (EP`seq(j) * NU) - 2 * (EP`seq(1 + j) * NU))" "(LAMBDA (j: below(length(EP) - 1)): (EP`seq(j) * MINj(a!1, b!1, EP, j, f!1) - EP`seq(1 + j) * MINj(a!1, b!1, EP, j, f!1)) + (EP`seq(1 + j) * MAXj(a!1, b!1, EP, j, f!1) - EP`seq(j) * MAXj(a!1, b!1, EP, j, f!1)))" "length(EP) - 2" "0") (("2" (replace -1 * rl) (("2" (hide -1) (("2" (assert) (("2" (lemma "sigma_all_parts") (("2" (inst - "a!1" "b!1") (("2" (assert) (("2" (inst?) (("2" (lemma "sigma_scal[below(length(EP) - 1)]") (("2" (inst?) (("2" (inst - "-2*NU") (("2" (assert) (("2" (replace -2) (("2" (assert) 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" (hide -1) (("2" (case "FORALL (i: below(length(EP) - 1)): f!1(XP(i)) < MINj(a!1, b!1, EP, i, f!1) + NU") (("1" (case "FORALL (i: below(length(EP) - 1)): f!1(XPP(i)) > MAXj(a!1, b!1, EP, i, f!1) - NU") (("1" (hide -4 -5) (("1" (hide -3 -5 -6 -7 -8) (("1" (lemma "sigma_lt[below(length(EP) -1)]") (("1" (inst - "(LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j)))" "(LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XP(i)) + EP`seq(1 + i) * f!1(XPP(i)) - EP`seq(i) * f!1(XPP(i)) - EP`seq(1 + i) * f!1(XP(i)))" "length(EP) - 2" "0") (("1" (assert) (("1" (hide 2) (("1" (case "length(EP) > 2") (("1" (assert) (("1" (skosimp*) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (case "f!1(XPP(n!1)) - f!1(XP(n!1)) > MAXj(a!1, b!1, EP, n!1, f!1) - MINj(a!1, b!1, EP, n!1, f!1) - 2*N (("1" (assert) (("1" (mult-by -1 "EP(n!1+1) - EP(n!1)") (("1" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("3" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma " N_from_delta[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (hide -1 -2) (("2" (prop) (("1" (skosimp*) (("1" (typepred "get_xpp(a!1, b!1, EP, f!1, x1!1, NU)") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "get_xp(a!1, b!1, EP, f!1, ii!1, NU)") (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide 2) (("3" (assert) (("3" (hide -1 -2) (("3" (prop) (("1" (skosimp*) (("1" (typepred "get_xp(a!1, b!1, EP, f!1, x1!1, NU)") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (typepred "get_xp(a!1, b!1, EP, f!1, ii!1, NU)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) nil nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (replace -1 * rl) (("2" (cross-mult 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)) nil)) nil) ("2" (hide 2) (("2" (hide -3 -4 -5 -6 -7 -8 -9) (("2" (split +) (("1" (expand "step_function?") (("1" (inst?) nil nil)) nil) ("2" (expand "step_function?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bnded_on?") (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case-replace "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (steps_exist-4 nil 3280570585 ("" (skosimp*) (("" (lemma "connected_domain") (("" (lemma "Lemma_1[T]") (("" (inst?) (("" (assert) (("" (inst - "eps!1/2") (("" (skosimp*) (("" (name "EP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)") (("1" (case "bnded_on?(a!1, b!1)(f!1)") (("1" (inst + "F1(a!1,b!1,EP,f!1)" "F2(a!1,b!1,EP,f!1)") (("1" (lemma "F1_F2_lem") (("1" (inst?) (("1" (assert) (("1" (inst - "EP") (("1" (flatten) (("1" (case-replace " step_function?(a!1, b!1, F1(a!1, b!1, EP, f!1)) AND step_function?(a!1, b!1, F2(a!1, b!1, EP, f!1))") (("1" (flatten) (("1" (hide -3 -4) (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (lemma "integrable_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (case-replace "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) <= eps!1/2") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "lt_via_epsi[T]") (("2" (inst - "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1))" "eps!1 / 2") (("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (name "NU" "epsi!1/(2*(b!1 - a!1))") (("2" (case "NU > 0") (("1" (case "bounded_on_all?[T](a!1, b!1, EP)(f!1)") (("1" (name "XP" "(LAMBDA (j: below(length(EP) - 1)): get_xp(a!1,b!1,EP,f!1,j,NU))") (("1" (name "XPP" "(LAMBDA (j: below(length(EP) - 1)): get_xpp(a!1,b!1,EP,f!1,j,NU))") (("1" (inst - "EP" "EP" "XPP" "XP") (("1" (assert) (("1" (case "width(a!1, b!1, EP) < delta!1") (("1" (assert) (("1" (expand "Rie_sum") (("1" (assert) (("1" (lemma "integral_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (rewrite "sigma_minus[below(length(EP) - 1)]") (("1" (case "sigma(0, length(EP) - 2, LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XP(i)) + EP`seq(1 + i) * f!1(XPP(i)) - EP`seq(i) * f!1(XPP(i)) - EP`seq(1 + i) * f!1(XP(i))) > sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2*NU) * (EP`seq(j+1) - EP`seq(j)))") (("1" (case-replace "sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j))) = integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1) (("1" (hide -1) (("1" (case "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) - 2 * NU * (b!1 - a!1) < eps!1 / 2") (("1" (assert) (("1" (cross-mult -9) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (hide -1 2) (("2" (replace -1) (("2" (hide-all-but 1) (("2" (lemma "sigma_sum[below(length(EP) - 1)]") (("2" (inst - "(LAMBDA (j: below(length(EP) - 1)): 2 * (EP`seq(j) * NU) - 2 * (EP`seq(1 + j) * NU))" "(LAMBDA (j: below(length(EP) - 1)): (EP`seq(j) * MINj(a!1, b!1, EP, j, f!1) - EP`seq(1 + j) * MINj(a!1, b!1, EP, j, f!1)) + (EP`seq(1 + j) * MAXj(a!1, b!1, EP, j, f!1) - EP`seq(j) * MAXj(a!1, b!1, EP, j, f!1)))" "length(EP) - 2" "0") (("2" (replace -1 * rl) (("2" (hide -1) (("2" (assert) (("2" (lemma "sigma_all_parts") (("2" (inst - "a!1" "b!1") (("2" (assert) (("2" (inst?) (("2" (lemma "sigma_scal[below(length(EP) - 1)]") (("2" (inst?) (("2" (inst - "-2*NU") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (case "FORALL (i: below(length(EP) - 1)): f!1(XP(i)) < MINj(a!1, b!1, EP, i, f!1) + NU") (("1" (case "FORALL (i: below(length(EP) - 1)): f!1(XPP(i)) > MAXj(a!1, b!1, EP, i, f!1) - NU") (("1" (hide -4 -5) (("1" (hide -3 -5 -6 -7 -8) (("1" (lemma "sigma_lt[below(length(EP) -1)]") (("1" (inst - "(LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j)))" "(LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XP(i)) + EP`seq(1 + i) * f!1(XPP(i)) - EP`seq(i) * f!1(XPP(i)) - EP`seq(1 + i) * f!1(XP(i)))" "length(EP) - 2" "0") (("1" (assert) (("1" (hide 2) (("1" (case "length(EP) > 2") (("1" (assert) (("1" (skosimp*) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (case "f!1(XPP(n!1)) - f!1(XP(n!1)) > MAXj(a!1, b!1, EP, n!1, f!1) - MINj(a!1, b!1, EP, n!1, f!1) - 2*N (("1" (mult-by -1 "EP(n!1+1) - EP(n!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (typepred "EP") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal 2) (("2" (expand "sigma") (("2" (assert) (("2" (inst - "0") (("2" (inst - "0") (("2" (case "f!1(XPP(0)) - f!1(XP(0)) > MAXj(a!1, b!1, EP, 0, f!1) - MINj(a!1, b!1, EP, 0, f!1) - 2*NU ") (("1" (mult-by -1 "EP(1) - EP(0)") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -3 * rl) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -9 2) (("2" (replace -3 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma " N_from_delta[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (hide -1 -2) (("2" (prop) (("1" (skosimp*) (("1" (typepred "get_xpp(a!1, b!1, EP, f!1, x1!1, NU)") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "get_xp(a!1, b!1, EP, f!1, ii!1, NU)") (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide 2) (("3" (assert) (("3" (hide -1 -2) (("3" (prop) (("1" (skosimp*) (("1" (typepred "get_xp(a!1, b!1, EP, f!1, x1!1, NU)") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (typepred "get_xp(a!1, b!1, EP, f!1, ii!1, NU)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) nil nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (replace -1 * rl) (("2" (cross-mult 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)) nil)) nil) ("2" (hide 2) (("2" (hide -3 -4 -5 -6 -7 -8 -9) (("2" (split +) (("1" (expand "step_function?") (("1" (inst?) (("1" (expand "step_function_on?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "step_function?") (("2" (inst?) (("2" (expand "step_function_on?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bnded_on?") (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case-replace "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((eq_partition const-decl "partition(a, b)" integral_def nil) (partition type-eq-decl nil integral_def nil) (integrable_bounded formula-decl nil integral_bounded nil) (step_function? const-decl "bool" step_fun_def nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def nil) (integral? const-decl "bool" integral_def nil) (integrable? const-decl "bool" integral_def nil) (integrable_bounded_on_all formula-decl nil integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (xis? const-decl "bool" integral_def nil) (width const-decl "posreal" integral_def nil) (Rie_sum const-decl "real" integral_def nil) (sigma_minus formula-decl nil sigma "reals/") (sigma_lt formula-decl nil sigma "reals/") (sigma_scal formula-decl nil sigma "reals/") (sigma_sum formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (N_from_delta formula-decl nil integral_def nil) (MAXj const-decl "real" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (bnded_on? const-decl "bool" integral_bounded nil) (Lemma_1 formula-decl nil integral_prep nil)) nil) (steps_exist-3 nil 3280570227 ("" (skosimp*) (("" (lemma "Lemma_1[T]") (("1" (inst?) (("1" (assert) (("1" (inst - "eps!1/2") (("1" (skosimp*) (("1" (name "EP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)") (("1" (inst + "F1(a!1,b!1,EP,f!1)" "F2(a!1,b!1,EP,f!1)") (("1" (lemma "F1_F2_lem") (("1" (inst?) (("1" (assert) (("1" (inst - "EP") (("1" (flatten) (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (lemma "integrable_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (case-replace "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) <= eps!1/2") (("1" (assert) nil) ("2" (hide 2) (("2" (lemma "lt_via_epsi[T]") (("2" (inst - "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1))" "eps!1 / 2") (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (lemma "integral_F2_F1") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (name "NU" "epsi!1/(2*(b!1 - a!1))") (("1" (case "NU > 0") (("1" (name "XP" "(LAMBDA (j: below(length(EP) - 1)): get_xp(a!1,b!1,EP,f!1,j,NU))") (("1" (name "XPP" "(LAMBDA (j: below(length(EP) - 1)): get_xpp(a!1,b!1,EP,f!1,j,NU))") (("1" (hide -5) (("1" (inst - "EP" "EP" "XPP" "XP") (("1" (assert) (("1" (case "width(a!1, b!1, EP) < delta!1") (("1" (assert) (("1" (expand "Rie_sum") (("1" (assert) (("1" (lemma "integral_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (rewrite "sigma_minus[below(length(EP) - 1)]") (("1" (case "sigma(0, length(EP) - 2, LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XPP(i)) + EP`seq(1 + i) * f!1(XP(i)) - EP`seq(i) * f!1(XP(i)) - EP`seq(1 + i) * f!1(XPP(i))) > sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2*NU) * (EP`seq(j+1) - EP`seq(j)))") (("1" (case-replace "sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j))) = integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1) (("1" (hide -1) (("1" (case "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) - 2 * NU * (b!1 - a!1) < eps!1 / 2") (("1" (assert) (("1" (cross-mult -8) nil))) ("2" (cross-mult -7) (("2" (assert) nil))) ("3" (expand "bnded_on?") (("3" (assert) (("3" (lemma "integrable_bounded[T]") (("3" (inst?) (("3" (assert) nil))))))))))))) ("2" (assert) (("2" (hide -1) (("2" (replace -1) (("2" (hide-all-but 1) (("2" (assert) (("2" (lemma "sigma_sum[below(length(EP) - 1)]") (("2" (inst - "(LAMBDA (j: below(length(EP) - 1)): 2 * (EP`seq(j) * NU) - 2 * (EP`seq(1 + j) * NU))" "(LAMBDA (j: below(length(EP) - 1)): (EP`seq(j) * MINj(a!1, b!1, EP, j, f!1) - EP`seq(1 + j) * MINj(a!1, b!1, EP, j, f!1)) + (EP`seq(1 + j) * MAXj(a!1, b!1, EP, j, f!1) - EP`seq(j) * MAXj(a!1, b!1, EP, j, f!1)))" "length(EP) - 2" "0") (("1" (replace -1 * rl) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_all_parts") (("1" (inst - "a!1" "b!1") (("1" (assert) (("1" (inst?) (("1" (lemma "sigma_scal[below(length(EP) - 1)]") (("1" (inst?) (("1" (inst - "-2*NU") (("1" (assert) nil))))))))))))))))))))) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (skosimp*) nil))))) ("3" (hide 2) (("3" (reveal -10) (("3" (skosimp*) (("3" (lemma "integrable_bounded_on_all[T]") (("3" (inst?) (("3" (assert) (("3" (inst?) nil))))))))))))))))))))))))))) ("3" (assert) (("3" (expand "bnded_on?") (("3" (assert) (("3" (lemma "integrable_bounded[T]") (("3" (assert) (("3" (inst?) (("3" (assert) nil))))))))))))))) ("2" (hide 2) (("2" (hide -1) (("2" (case "FORALL (i: below(length(EP) - 1)): f!1(XP(i)) < MINj(a!1, b!1, EP, i, f!1) + NU") (("1" (case "FORALL (i: below(length(EP) - 1)): f!1(XPP(i)) > MAXj(a!1, b!1, EP, i, f!1) - NU") (("1" (hide -4 -5) (("1" (hide -3 -5 -6 -7) (("1" (lemma "sigma_lt[below(length(EP) -1)]") (("1" (inst - "(LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j)))" "(LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XPP(i)) + EP`seq(1 + i) * f!1(XP(i)) - EP`seq(i) * f!1(XP(i)) - EP`seq(1 + i) * f!1(XPP(i)))" "length(EP) - 2" "0") (("1" (assert) (("1" (hide 2) (("1" (assert) (("1" (case "length(EP) > 2") (("1" (assert) (("1" (skosimp*) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (case "f!1(XPP(n!1)) - f!1(XP(n!1)) > MAXj(a!1, b!1, EP, n!1, f!1) - MINj(a!1, b!1, EP, n!1, f!1) - 2*N (("1" (assert) (("1" (mult-by -1 "EP(n!1+1) - EP(n!1)") (("1" (assert) (("1" (postpone) nil))) ("2" (postpone) nil) ("3" (postpone) nil) ("4" (postpone) nil))))) ("2" (postpone) nil) ("3" (postpone) nil))))))))))))))) ("2" (postpone) nil))))))))) ("2" (postpone) nil) ("3" (postpone) nil))))))))) ("2" (hide -7 -8 2) (("2" (skosimp*) (("2" (replace -3 * rl) (("2" (assert) nil))))))))) ("2" (hide -7 -8 2) (("2" (skosimp*) (("2" (replace -3 * rl) (("2" (assert) nil))))))))))))) ("3" (hide-all-but 1) (("3" (lemma "connected_domain") (("3" (skosimp*) nil))))) ("4" (skosimp*) (("4" (assert) nil))))) ("2" (skosimp*) (("2" (assert) nil))))))))))))))))))) ("2" (hide 2) (("2" (lemma " N_from_delta[T]") (("2" (inst?) (("2" (assert) nil))))))))))) ("2" (hide 2) (("2" (replace -1 * rl) (("2" (assert) (("2" (hide -1 -2) (("2" (prop) (("1" (skosimp*) (("1" (typepred "get_xpp(a!1, b!1, EP, f!1, x1!1, NU)") (("1" (assert) nil) ("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil))))))))))) ("2" (skosimp*) (("2" (typepred "get_xpp(a!1, b!1, EP, f!1, ii!1, NU)") (("1" (assert) nil) ("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil))))))))))))))))))))) ("3" (assert) (("3" (hide 2) (("3" (replace -2 * rl) (("3" (assert) (("3" (hide -1 -2) (("3" (prop) (("1" (skosimp*) (("1" (typepred "get_xp(a!1, b!1, EP, f!1, x1!1, NU)") (("1" (assert) nil) ("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil))))))))))) ("2" (assert) (("2" (skosimp*) (("2" (assert) (("2" (typepred "get_xp(a!1, b!1, EP, f!1, ii!1, NU)") (("1" (assert) nil) ("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) nil))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (assert) nil))) ("3" (skosimp*) (("3" (lemma "integrable_bounded_on_all[T]") (("3" (inst?) (("3" (assert) (("3" (inst?) nil))))))))))) ("2" (replace -1 * rl) (("2" (cross-mult 1) (("2" (assert) nil))))))))))))))))))))))))) ("2" (inst?) (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (expand "bnded_on?") (("2" (propax) nil))))))))))))))))) ("3" (expand "bnded_on?") (("3" (lemma "integrable_bounded[T]") (("3" (inst?) (("3" (assert) nil))))))))))))))))))))))))))))))))))))) ("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (expand "bnded_on?") (("2" (propax) nil))))))))))) ("2" (hide 2) (("2" (case-replace "(b!1 - a!1) / delta!1 > 0") (("1" (assert) nil) ("2" (cross-mult 1) nil))))))))))))))) ("2" (lemma "connected_domain") (("2" (propax) nil)))))) nil) nil nil) (steps_exist-2 nil 3280513421 ("" (skosimp*) (("" (lemma "Lemma_1[T]") (("1" (inst?) (("1" (assert) (("1" (inst - "eps!1/2") (("1" (skosimp*) (("1" (name "EP" "eq_partition(a!1,b!1,floor((b!1-a!1)/delta!1) + 2)") (("1" (inst + "F1(a!1,b!1,EP,f!1)" "F2(a!1,b!1,EP,f!1)") (("1" (lemma "F1_F2_lem") (("1" (inst?) (("1" (assert) (("1" (inst - "EP") (("1" (flatten) (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (lemma "integrable_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (hide -1 -2 -3) (("1" (case-replace "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) <= eps!1/2") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "lt_via_epsi[T]") (("2" (inst - "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1))" "eps!1 / 2") (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (lemma "integral_F2_F1") (("1" (inst - "a!1" "b!1" "f!1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (name "NU" "epsi!1/(2*(b!1 - a!1))") (("1" (case "NU > 0") (("1" (name "XP" "(LAMBDA (j: below(length(EP) - 1)): get_xp(a!1,b!1,EP,f!1,j,NU))") (("1" (name "XPP" "(LAMBDA (j: below(length(EP) - 1)): get_xpp(a!1,b!1,EP,f!1,j,NU))") (("1" (hide -5) (("1" (inst - "EP" "EP" "XP" "XPP") (("1" (assert) (("1" (case "width(a!1, b!1, EP) < delta!1") (("1" (assert) (("1" (expand "Rie_sum") (("1" (assert) (("1" (lemma "integral_F2_F1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (rewrite "sigma_minus[below(length(EP) - 1)]") (("1" (case "sigma(0, length(EP) - 2, LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XPP(i)) + EP`seq(1 + i) * f!1(XP(i)) - EP`seq(i) * f!1(XP(i)) - EP`seq(1 + i) * f!1(XPP(i))) > sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2*NU) * (EP`seq(j+1) - EP`seq(j)))") (("1" (case-replace "sigma(0, length(EP) - 2, LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j))) = integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1) (("1" (hide -1) (("1" (case "integral(a!1, b!1, F2(a!1, b!1, EP, f!1) - F1(a!1, b!1, EP, f!1)) - 2 * NU * (b!1 - a!1) < eps!1 / 2") (("1" (assert) (("1" (cross-mult -8) nil nil)) nil) ("2" (cross-mult -7) (("2" (assert) nil nil)) nil) ("3" (expand "bnded_on?") (("3" (assert) (("3" (lemma "integrable_bounded[T]") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -1) (("2" (replace -1) (("2" (hide-all-but 1) (("2" (assert) (("2" (lemma "sigma_sum[below(length(EP) - 1)]") (("2" (inst - "(LAMBDA (j: below(length(EP) - 1)): 2 * (EP`seq(j) * NU) - 2 * (EP`seq(1 + j) * NU))" "(LAMBDA (j: below(length(EP) - 1)): (EP`seq(j) * MINj(a!1, b!1, EP, j, f!1) - EP`seq(1 + j) * MINj(a!1, b!1, EP, j, f!1)) + (EP`seq(1 + j) * MAXj(a!1, b!1, EP, j, f!1) - EP`seq(j) * MAXj(a!1, b!1, EP, j, f!1)))" "length(EP) - 2" "0") (("1" (replace -1 * rl) (("1" (hide -1) (("1" (assert) (("1" (lemma "sigma_all_parts") (("1" (inst - "a!1" "b!1") (("1" (assert) (("1" (inst?) (("1" (lemma "sigma_scal[below(length(EP) - 1)]") (("1" (inst?) (("1" (inst - "-2*NU") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (skosimp*) nil nil)) nil)) nil) ("3" (hide 2) (("3" (reveal -10) (("3" (skosimp*) (("3" (lemma "integrable_bounded_on_all[T]") (("3" (inst?) (("3" (assert) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand "bnded_on?") (("3" (assert) (("3" (lemma "integrable_bounded[T]") (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (case "FORALL (i: below(length(EP) - 1)): f!1(XP(i)) < MINj(a!1, b!1, EP, i, f!1) + NU") (("1" (case "FORALL (i: below(length(EP) - 1)): f!1(XPP(i)) > MAXj(a!1, b!1, EP, i, f!1) - NU") (("1" (hide -4 -5) (("1" (hide -3 -5 -6 -7) (("1" (lemma "sigma_lt[below(length(EP) -1)]") (("1" (inst - "(LAMBDA (j: below(length(EP) - 1)): (MAXj(a!1, b!1, EP, j, f!1) - MINj(a!1, b!1, EP, j, f!1) - 2 * NU) * (EP`seq(j + 1) - EP`seq(j)))" "(LAMBDA (i: below(length(EP) - 1)): EP`seq(i) * f!1(XPP(i)) + EP`seq(1 + i) * f!1(XP(i)) - EP`seq(i) * f!1(XP(i)) - EP`seq(1 + i) * f!1(XPP(i))) " "length(EP) - 2" "0") (("1" (assert) (("1" (hide 2) (("1" (assert) (("1" (case "length(EP) > 2") (("1" (assert) (("1" (skosimp*) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (case "f!1(XPP(n!1)) - f!1(XP(n!1)) > MAXj(a!1, b!1, EP, n!1, f!1) - MINj(a!1, b!1, EP, n!1, f!1) - 2*N (("1" (assert) (("1" (mult-by -1 "EP(n!1+1) - EP(n!1)") (("1" (assert) (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.934 Sekunden (vorverarbeitet am 2026-04-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26