| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lebesgue/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 MB |
|
Quelle riemann_scaf.prfSprache: Lisp |
|||||||||||||||
|
(riemann_scaf (IMP_integral_def_TCC1 0 (IMP_integral_def_TCC1-1 nil 3420183209 ("" (expand "connected?") (("" (propax) nil nil)) nil) ((connected? const-decl "bool" deriv_domain_def "analysis/")) nil)) (IMP_integral_def_TCC2 0 (IMP_integral_def_TCC2-1 nil 3420183209 ("" (expand "not_one_element?") (("" (skosimp) (("" (case-replace "x!1=0") (("1" (inst + "1") (("1" (assert) nil nil)) nil) ("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) nil)) (step_TCC1 0 (step_TCC1-1 nil 3450779708 ("" (expand "step?") (("" (expand "step_function?") (("" (expand "zeroed?") (("" (inst + "(# length := 2, seq := (LAMBDA (ii: below(2)): if ii = 0 then a else b endif) #)") (("1" (expand "step_function_on?") (("1" (skosimp) (("1" (inst + "0") (("1" (skosimp) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((step_function? const-decl "bool" step_fun_def "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (a formal-const-decl "real" riemann_scaf nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers 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) (NOT const-decl "[bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def "analysis/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (step_function_on? const-decl "bool" step_fun_def "analysis/") (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) (zeroed? const-decl "bool" riemann_scaf nil) (step? const-decl "bool" riemann_scaf nil)) nil)) (bounded_TCC1 0 (bounded_TCC1-1 nil 3450779708 ("" (expand "zeroed_bounded?") (("" (expand "bounded?") (("" (expand "zeroed?") (("" (expand "abs") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((bounded? const-decl "bool" sup_norm "measure_integration/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (zeroed? const-decl "bool" riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf nil)) nil)) (IMP_fun_preds_partial_TCC1 0 (IMP_fun_preds_partial_TCC1-1 nil 3450779708 ("" (expand "partial_order?") (("" (expand "preorder?") (("" (expand "restrict") (("" (split) (("1" (expand "reflexive?") (("1" (skosimp) (("1" (expand "<=") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "transitive?") (("2" (expand "<=") (("2" (skosimp*) (("2" (inst - "x!2") (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "antisymmetric?") (("3" (expand "<=") (("3" (skosimp) (("3" (apply-extensionality 1 :hide? t) (("3" (inst - "x!2") (("3" (inst - "x!2") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((preorder? const-decl "bool" orders nil) (<= const-decl "bool" real_fun_orders "reals/") (reflexive? const-decl "bool" relations 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (transitive? const-decl "bool" relations nil) (bool nonempty-type-eq-decl nil booleans nil) (step? const-decl "bool" riemann_scaf nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (antisymmetric? const-decl "bool" relations nil) (restrict const-decl "R" restrict nil) (partial_order? const-decl "bool" orders nil)) nil)) (partition_to_finite_partition_TCC1 0 (partition_to_finite_partition_TCC1-1 nil 3420272748 ("" (grind) nil nil) nil nil)) (partition_to_finite_partition_TCC2 0 (partition_to_finite_partition_TCC2-1 nil 3420272748 ("" (grind) nil nil) nil nil)) (partition_to_finite_partition_TCC3 0 (partition_to_finite_partition_TCC3-1 nil 3420272748 ("" (skosimp) (("" (expand "finite_partition?") (("" (split) (("1" (expand "singleton" 1 1) (("1" (expand "singleton" 1 1) (("1" (expand "union") (("1" (expand "member") (("1" (expand "fullset") (("1" (expand "partition?") (("1" (split) (("1" (apply-extensionality :hide? t) (("1" (expand "Union") (("1" (case "x!1<a OR b <x!1") (("1" (split) (("1" (inst + "{x | x < a}") nil nil) ("2" (inst + "{x | b<x}") nil nil)) nil) ("2" (flatten) (("2" (case "a<=x!1") (("1" (case "x!1<=b") (("1" (hide 1 2) (("1" (lemma "part_in" ("P" "P!1" "a" "a" "b" "b" "x" "x!1")) (("1" (assert) (("1" (skosimp) (("1" (expand "<=" (-1 -2)) (("1" (split -1) (("1" (split -2) (("1" (inst + "{x | seq(P!1)(ii!1) < x AND x < seq(P!1)(1 + ii!1)}") (("1" (assert) nil nil) ("2" (flatten) (("2" (assert) (("2" (inst 4 "ii!1") nil nil)) nil)) nil)) nil) ("2" (inst + "singleton[closed_interval[real](a, b)] (seq(P!1)(1+ii!1))") (("1" (expand "extend") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (flatten) (("2" (inst 3 "1+ii!1") (("2" (expand "extend") (("2" (hide 1 2 4) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "singleton") (("1" (lift-if 1) (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "singleton[closed_interval[real](a, b)] (seq(P!1)(ii!1))") (("1" (expand "extend") (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (hide 1 2 4) (("2" (inst + "ii!1") (("2" (apply-extensionality 1 :hide? t) (("2" (expand "extend") (("2" (expand "singleton") (("2" (lift-if 1) (("2" (assert) (("2" (case-replace "x!2 = seq(P!1)(ii!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (split) (("1" (split) (("1" (assert) nil nil) ("2" (grind) nil nil) ("3" (skosimp) (("3" (grind) nil nil)) nil) ("4" (grind) nil nil)) nil) ("2" (split -2) (("1" (grind) nil nil) ("2" (assert) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil) ("3" (skosimp) (("3" (split -2) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (skosimp) (("4" (replace -1) (("4" (replace -2) (("4" (hide-all-but 2) (("4" (expand "disjoint?") (("4" (expand "intersection") (("4" (expand "empty?") (("4" (expand "member") (("4" (skosimp) (("4" (expand "singleton") (("4" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!2")) (("4" (assert) (("4" (inst - "P!1") (("4" (inst - "i!2" "i!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (split) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (skosimp*) (("3" (replace -1) (("3" (replace -2) (("3" (hide-all-but 2) (("3" (expand "disjoint?") (("3" (expand "intersection") (("3" (expand "empty?") (("3" (expand "member") (("3" (skosimp) (("3" (expand "singleton") (("3" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!2")) (("3" (assert) (("3" (inst - "P!1") (("3" (inst - "i!2" "i!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma "parts_disjoint" ("a" "a" "b" "b")) (("4" (inst - "_" "P!1" "i!1" "i!2") (("4" (replace -2) (("4" (replace -3) (("4" (hide -2 -3) (("4" (expand "disjoint?") (("4" (expand "intersection") (("4" (expand "empty?") (("4" (expand "member") (("4" (skosimp) (("4" (inst - "x!2") (("4" (assert) (("4" (replace -1) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "finite_union") (("2" (hide 2) (("2" (rewrite "finite_union") (("1" (hide 2) (("1" (rewrite "is_finite_surj" + :dir rl) (("1" (inst + "length(P!1)-1" "lambda (i: below(length(P!1) - 1)): {x | seq(P!1)(i) < x AND x < seq(P!1)(1 + i)}") (("1" (expand "surjective?") (("1" (skosimp) (("1" (typepred "y!1") (("1" (skosimp) (("1" (inst + "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "is_finite_surj" + :dir rl) (("2" (inst + "length(P!1)" "lambda (i: below(length(P!1))):singleton[closed_interval[real](a, b)] (seq(P!1)(i))") (("1" (expand "surjective?") (("1" (skosimp) (("1" (typepred "y!1") (("1" (skosimp) (("1" (inst + "i!1") (("1" (expand "extend") (("1" (apply-extensionality :hide? t) (("1" (replace -1 1 rl) (("1" (lift-if 1) (("1" (prop) (("1" (assert) (("1" (replace -2) (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -2) (("2" (expand "singleton") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst + "i!1") (("2" (expand "extend") (("2" (apply-extensionality :hide? t) (("1" (expand "singleton") (("1" (case-replace "x!1 = seq(P!1)(i!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty_union1 application-judgement "(nonempty?)" bounded_nats "orders/") (finite_partition? const-decl "bool" partitions "measure_integration/") (nonempty_finite_union1 application-judgement "non_empty_finite_set[T]" sigma_countable "sigma_set/") (finite_union judgement-tcc nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite_surj formula-decl nil finite_sets nil) (surjective? const-decl "bool" functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (singleton const-decl "(singleton?)" sets nil) (union const-decl "set" sets nil) (fullset const-decl "set" sets nil) (part_in formula-decl nil integral_def "analysis/") (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (nonempty_extend application-judgement "(nonempty?[T])" extend_set_props nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil) (ii!1 skolem-const-decl "below(length(P!1) - 1)" riemann_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) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_compact application-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" integral_def "analysis/") (singleton_is_null application-judgement "null_set" lebesgue_def nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" sigma_countable "sigma_set/") (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (set type-eq-decl nil sets nil) (Union const-decl "set" sets nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf nil) (b formal-const-decl "{x: real | a < x}" riemann_scaf 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) (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) (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) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def "analysis/") (singleton? const-decl "bool" sets nil) (TRUE const-decl "bool" booleans 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) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (part_not_in formula-decl nil integral_def "analysis/") (finite_intersection1 application-judgement "finite_set[real]" integral_def "analysis/") (intersection2_preserves_bounded application-judgement "(LAMBDA (S: set[T]): bounded?(S, restrict[[real, real], [T, T], boolean](<=)))" bounded_nats "orders/") (parts_disjoint formula-decl nil integral_def "analysis/") (intersection1_preserves_bounded application-judgement "(LAMBDA (S: set[T]): bounded?(S, restrict[[real, real], [T, T], boolean](<=)))" bounded_nats "orders/") (finite_intersection2 application-judgement "finite_set[real]" integral_def "analysis/") (partition? const-decl "bool" partitions "measure_integration/") (member const-decl "bool" sets nil)) nil)) (riemann_lebesgue_step_isf 0 (riemann_lebesgue_step_isf-1 nil 3450826554 ("" (skosimp) (("" (typepred "phi!1") (("" (expand "step?") (("" (flatten) (("" (lemma "step_function_integrable?" ("a" "a" "b" "b" "f" "phi!1")) (("" (expand "Integrable?") (("" (assert) (("" (hide -1) (("" (expand "Integral") (("" (lemma "step_function_on_integral" ("a" "a" "b" "b" "f" "phi!1")) (("" (assert) (("" (expand "step_function?") (("" (skosimp) (("" (inst - "P!1") (("" (assert) (("" (replace -1) (("" (hide -1) (("" (expand "step_function_on?") (("" (typepred "P!1") (("" (case "forall (x:real): isf?(*[real](phi(singleton[real](x)),phi!1)) & isf_integral(*[ (("1" (case "forall (ii: below(length(P!1) - 1)): isf?(*[real]( val_in(a, b, P!1, ii, phi!1),phi(open( P!1`seq(ii) * val_in(a, b, P!1, ii, phi!1)") (("1" (name "FF" "LAMBDA (ii: below(length(P!1) - 1)): P!1`seq(1 + ii) * val_in(a, b, P!1, ii, phi!1) - P!1`seq(ii) * val_in(a, b, P!1, ii, phi!1)") (("1" (replace -1) (("1" (case "FORALL (ii: below(length(P!1) - 1)): isf?(*[real] (val_in(a, b, P!1, ii, phi!1), phi(open(seq(P!1)(ii), seq(P!1)(1 + ii))))) & isf_integral(*[real] (val_in(a, b, P!1, ii, phi!1), phi(open(seq(P!1)(ii), seq(P!1)(1 + ii))))) = FF(ii)") (("1" (case "forall (n:nat): n <= length(P!1) - 2 => isf?(*[real](phi({x:real | a <= x & x < seq(P!1)(n+1)}) (("1" (inst - "length(P!1)-2") (("1" (assert) (("1" (replace -8) (("1" (flatten) (("1" (replace -2) (("1" (hide -3 -4 -5 -2) (("1" (inst -2 "b") (("1" (flatten) (("1" (lemma "isf_add" ("i1" "(*[real](phi({x: real | a <= x & x < b}), phi!1))" "i2" "(*[real](phi(singleton[real](b)), phi!1))")) (("1" (lemma "isf_integral_add" ("i1" "(*[real](phi({x: real | a <= x & x < b}), phi!1))" "i2" "(*[real](phi(singleton[real](b)), phi!1))")) (("1" (case-replace "((*[real](phi({x: real | a <= x & x < b}), phi!1)) + (*[real](phi(singleton[real](b)), phi!1)))=phi!1") (("1" (replace -3) (("1" (replace -2 1) (("1" (replace -6) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-11 1)) (("2" (apply-extensionality :hide? t) (("2" (expand "zeroed?") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name "GG" "lambda (n: below(length(P!1) - 1)): (*[real] (phi({x: real | a <= x & x < seq(P!1)(n + 1)}), phi!1))") (("2" (case "FORALL (n: nat): n <= length(P!1) - 2 => isf?(GG(n)) & sigma(0, n, FF) = isf_integral(GG(n))") (("1" (skosimp) (("1" (inst - "n!1") (("1" (expand "GG") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (induct "n") (("1" (flatten) (("1" (expand "sigma") (("1" (assert) (("1" (expand "GG") (("1" (inst -2 "0") (("1" (inst -5 "a") (("1" (flatten) (("1" (lemma "isf_add" ("i1" "(*[real](phi(singleton[real](a)), phi!1))" "i2" "(*[real] (val_in(a, b, P!1, 0, phi!1), phi(open(seq(P!1)(0), seq(P!1)(1 + 0)))))")) (("1" (lemma "isf_integral_add" ("i1" "(*[real](phi(singleton[real](a)), phi!1))" "i2" "(*[real] (val_in(a, b, P!1, 0, phi!1), phi(open(seq(P!1)(0), seq(P!1)(1 + 0)))))")) (("1" (replace -9) (("1" (replace -5) (("1" (expand "+ ") (("1" (expand "*") (("1" (case-replace "(LAMBDA (x: real): phi(singleton[real](a))(x) * phi!1(x) + val_in(a, b, P!1, 0, phi!1) * phi(open(seq(P!1)(0), seq(P!1)(1)))(x))=(LAMBDA (x_1: real): phi({x: real | a <= x & x < seq(P!1)(1)})(x_1) * phi!1(x_1))") (("1" (replace -3) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil) ("2" (hide 2 -7) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "singleton") (("1" (expand "phi") (("1" (expand "member") (("1" (case-replace "x!1=a") (("1" (assert) (("1" (replace -11) (("1" (inst -13 "0") (("1" (assert) (("1" (expand "val_in") (("1" (inst -14 "0") (("1" (skosimp) (("1" (case-replace "open(a, seq(P!1)(1))(a)") (("1" (hide-all-but (-12 -14 -1)) (("1" (grind) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "a <= x!1 & x!1 < seq(P!1)(1)") (("1" (flatten) (("1" (case-replace "open(seq(P!1)(0), seq(P!1)(1))(x!1)") (("1" (inst -16 "0") (("1" (skosimp) (("1" (inst-cp -16 "x!1") (("1" (expand "val_in") (("1" (inst -16 "pick(a,b,P!1,0)") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1 2)) (("2" (grind) nil nil)) nil) ("3" (inst -14 "0") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1 3) (("2" (inst -12 "0") (("2" (case-replace "open(seq(P!1)(0), seq(P!1)(1))(x!1)") (("1" (hide-all-but (-1 -13 -11 1 2)) (("1" (grind) nil nil)) nil) ("2" (replace 1 4) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -12 "0") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (inst -13 "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "sigma" 1) (("2" (flatten) (("2" (replace -2) (("2" (hide -2) (("2" (inst -3 "1+j!1") (("2" (inst -6 "seq(P!1)(1 + j!1)") (("2" (flatten) (("2" (hide -5 -6) (("2" (lemma "isf_add" ("i2" "(*[real] (val_in(a, b, P!1, 1 + j!1, phi!1), phi(open(seq(P!1)(1 + j!1), seq(P!1)(1 + (1 + j!1))))))" "i1" "(*[real](phi(singleton[real](seq(P!1)(1 + j!1))), phi!1))")) (("2" (lemma "isf_integral_add" ("i2" "(*[real] (val_in(a, b, P!1, 1 + j!1, phi!1), phi(open(seq(P!1)(1 + j!1), seq(P!1)(1 + (1 + j!1))))))" "i1" "(*[real](phi(singleton[real](seq(P!1)(1 + j!1))), phi!1))")) (("2" (replace -6) (("2" (replace -8) (("2" (hide -5 -6 -7 -8) (("2" (name-replace "HH" "((*[real] (phi(singleton[real](seq(P!1)(1 + j!1))), phi!1)) + (*[real] (val_in(a, b, P!1, 1 + j!1, phi!1), phi(open(seq(P!1)(1 + j!1), seq(P!1)(1 + (1 + j!1)))))))") (("2" (lemma "isf_add" ("i1" "GG(j!1)" "i2" "HH")) (("1" (lemma "isf_integral_add" ("i1" "GG(j!1)" "i2" "HH")) (("1" (case-replace "GG(j!1) + HH=GG(1+j!1)") (("1" (replace -2 1) (("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 2) (("2" (apply-extensionality :hide? t) (("2" (expand "HH") (("2" (expand "GG") (("2" (expand "singleton") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "*") (("2" (expand "+") (("2" (expand "open") (("2" (expand "ball") (("2" (case-replace "abs((seq(P!1)(1 + j!1) + seq(P!1)(2 + j!1)) / 2 - x!1) < (seq(P!1)(2 + j!1) - seq(P!1)(1 + j!1)) / 2 IFF (seq(P!1)(1 + j!1) < x!1 & x!1 < seq(P!1)(2 + j!1) (("1" (hide -1) (("1" (inst - "1+j!1") (("1" (case-replace "a<= x!1") (("1" (case-replace "x!1 < seq(P!1)(1 + j!1)") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "x!1 = seq(P!1)(1 + j!1)") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "x!1 < seq(P!1)(2 + j!1)") (("1" (expand "val_in") (("1" (inst -8 "1+j!1") (("1" (skosimp) (("1" (inst-cp -8 "x!1") (("1" (inst -8 "pick(a, b, P!1, 1 + j!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil) ("5" (skosimp) (("5" (assert) nil nil)) nil) ("6" (skosimp) (("6" (assert) nil nil)) nil) ("7" (skosimp) (("7" (skosimp) (("7" (assert) nil nil)) nil)) nil) ("8" (skosimp) (("8" (skosimp) (("8" (assert) nil nil)) nil)) nil) ("9" (skosimp) (("9" (skosimp) (("9" (assert) nil nil)) nil)) nil) ("10" (assert) nil nil) ("11" (skosimp) (("11" (assert) nil nil)) nil) ("12" (skosimp) (("12" (assert) nil nil)) nil) ("13" (assert) nil nil) ("14" (assert) nil nil) ("15" (skosimp) (("15" (assert) nil nil)) nil) ("16" (skosimp) (("16" (assert) nil nil)) nil) ("17" (skosimp) (("17" (assert) nil nil)) nil) ("18" (skosimp) (("18" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil) ("5" (skosimp) (("5" (assert) nil nil)) nil) ("6" (skosimp) (("6" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp) (("4" (skosimp) (("4" (assert) nil nil)) nil)) nil) ("5" (skosimp) (("5" (assert) nil nil)) nil) ("6" (skosimp) (("6" (skosimp) (("6" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -2 "ii!1") (("2" (expand "FF") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst -5 "ii!1") (("2" (lemma "isf_phi" ("E" "(ball[real, (LAMBDA (x, y: real): abs(x - y))] ((seq(P!1)(1 + ii!1) + seq(P!1)(ii!1)) / 2, (seq(P!1)(1 + ii!1) - seq(P!1)(ii!1)) / 2))")) (("1" (lemma "isf_integral_phi" ("E" "(ball[real, (LAMBDA (x, y: real): abs(x - y))] ((seq(P!1)(1 + ii!1) + seq(P!1)(ii!1)) / 2, (seq(P!1)(1 + ii!1) - seq(P!1)(ii!1)) / 2))")) (("1" (expand "mu" -1) (("1" (assert) (("1" (case-replace "2 * ((seq(P!1)(1 + ii!1) - seq(P!1)(ii!1)) / 2)= seq(P!1)(1 + ii!1) - seq(P!1)(ii!1)") (("1" (hide -1) (("1" (case-replace "((ball[real, (LAMBDA (x, y: real): abs(x - y))] ((seq(P!1)(1 + ii!1) + seq(P!1)(ii!1)) / 2, (seq(P!1)(1 + ii!1) - seq(P!1)(ii!1)) / 2)))=open(seq(P!1)(ii!1), seq(P!1)(1 + ii!1))") (("1" (hide -1) (("1" (hide -3) (("1" (lemma "isf_scal" ("c" "val_in(a, b, P!1, ii!1, phi!1)" "i" "phi(open(seq(P!1)(ii!1), seq(P!1)(1 + ii!1)))")) (("1" (replace -1) (("1" (lemma "isf_integral_scal" ("c" "val_in(a, b, P!1, ii!1, phi!1)" "i" "phi(open(seq(P!1)(ii!1), seq(P!1)(1 + ii!1)))")) (("1" (replace -1) (("1" (replace -3) (("1" (assert) (("1" (case-replace "lambda_(open(seq(P!1)(ii!1), seq(P!1)(1 + ii!1)))`2=P!1`seq(1 + ii!1)-P!1`seq(ii!1)" (("1" (assert) nil nil) ("2" (case-replace "open(seq(P!1)(ii!1), seq(P!1)(1 + ii!1))=ball((seq(P!1)(1 + ii!1) + seq(P!1)(ii!1)) / 2, (seq(P!1)(1 + ii!1) - seq(P!1)(ii!1)) / 2)") (("1" (rewrite "lambda_ball") (("1" (assert) nil nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "open") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-9 1)) (("2" (apply-extensionality :hide? t) (("2" (expand "open") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (expand "measurable_set?") (("2" (assert) (("2" (expand "mu_fin?") (("2" (split) (("1" (lemma "ball_is_cal_M" ("x" "(seq(P!1)(1 + ii!1) + seq(P!1)(ii!1)) / 2" "r" "(seq(P!1)(1 + ii!1) - seq(P!1)(ii!1)) / 2")) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (rewrite "lambda_ball") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) (("3" (typepred "P!1") (("3" (inst - "ii!1") nil nil)) nil)) nil)) nil) ("4" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (lemma "phi_is_simple") (("2" (inst - "singleton[real](x!1)") (("1" (lemma "isf_scal" ("c" "phi!1(x!1)" "i" "phi(singleton[real](x!1))")) (("1" (split 1) (("1" (expand "*" (-1 1)) (("1" (case-replace "(LAMBDA (x: real): phi!1(x!1) * phi(singleton[real](x!1))(x))=(LAMBDA (x: real): phi(si (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (expand "singleton") (("1" (expand "phi") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "isf_integral" ("i" "*[real](phi!1(x!1), phi(singleton[real](x!1)))")) (("1" (lemma "integral_scal" ("c" "phi!1(x!1)" "f" "phi(singleton[real](x!1))")) (("1" (replace -1) (("1" (expand "*" (-2 1)) (("1" (case-replace "(LAMBDA (x: real): phi!1(x!1) * phi(singleton[real](x!1))(x))=(LAMBDA (x: real): phi(singleton[real](x!1))(x) * phi!1(x))") (("1" (replace -3 1 rl) (("1" (hide -1 -2 -3 -4) (("1" (lemma "integral_phi_closed" ("a" "x!1" "b" "x!1")) (("1" (case-replace "closed(x!1, x!1)=singleton[real](x!1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "singleton") (("2" (expand "phi") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "integrable_phi_closed" ("a" "x!1" "b" "x!1")) (("2" (case-replace "closed(x!1, x!1)=singleton[real](x!1)") (("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "isf_phi" ("E" "singleton[real](x!1)")) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "mu_fin?") (("2" (case-replace "closed_ball(x!1, 0)=singleton[real](x!1)") (("1" (assert) (("1" (rewrite "lambda_singleton") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "singleton_is_cal_M" ("x" "x!1")) (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((step nonempty-type-eq-decl nil riemann_scaf nil) (step? const-decl "bool" riemann_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) (Integrable? const-decl "bool" integral_def "analysis/") (step_function_on_integral formula-decl nil integral_step "analysis/") (step_function? const-decl "bool" step_fun_def "analysis/") (step_function_on? const-decl "bool" step_fun_def "analysis/") (singleton_is_null application-judgement "null_set" lebesgue_def nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" integral_def "analysis/") (singleton_is_compact application-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (isf? const-decl "bool" isf "measure_integration/") (* const-decl "[T -> real]" real_fun_ops "reals/") (set type-eq-decl nil sets nil) (phi const-decl "nat" measure_space "measure_integration/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (isf nonempty-type-eq-decl nil isf "measure_integration/") (isf_integral const-decl "real" isf "measure_integration/") (ball_is_cal_M formula-decl nil lebesgue_def nil) (isf_integral_phi formula-decl nil isf "measure_integration/") (isf_scal judgement-tcc nil isf "measure_integration/") (isf_integral_scal formula-decl nil isf "measure_integration/") (lambda_ball formula-decl nil lebesgue_def nil) (mu const-decl "nnreal" measure_props "measure_integration/") (mu_fin? const-decl "bool" measure_props "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (isf_phi judgement-tcc nil isf "measure_integration/") (GG skolem-const-decl "[below(length(P!1) - 1) -> [real -> real]]" riemann_scaf nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (x!1 skolem-const-decl "real" riemann_scaf nil) (j!1 skolem-const-decl "nat" riemann_scaf nil) (HH skolem-const-decl "[real -> real]" riemann_scaf nil) (sigma_0_neg formula-decl nil sigma_below "reals/") (minus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "real" riemann_scaf nil) (open_interval type-eq-decl nil intervals_real "reals/") (pick const-decl "{t: T | seq(P)(j) < t AND t < seq(P)(j + 1)}" integral_step "analysis/") (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (real_div_nzreal_is_real application-judgement "real" reals nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (n!1 skolem-const-decl "nat" riemann_scaf nil) (n!1 skolem-const-decl "nat" riemann_scaf nil) (n!1 skolem-const-decl "nat" riemann_scaf nil) (n!1 skolem-const-decl "nat" riemann_scaf nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil) (isf_add judgement-tcc nil isf "measure_integration/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (zeroed? const-decl "bool" riemann_scaf nil) (isf_integral_add formula-decl nil isf "measure_integration/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (integer nonempty-type-from-decl nil integers 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (FF skolem-const-decl "[below(length(P!1) - 1) -> real]" riemann_scaf nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (open const-decl "open_interval" real_topology "metric_space/") (open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (ball const-decl "set[T]" metric_space_def "metric_space/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (val_in const-decl "real" integral_step "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (open_is_measurable application-judgement "measurable_set" lebesgue_def nil) (x!1 skolem-const-decl "real" riemann_scaf nil) (lambda_singleton formula-decl nil lebesgue_def nil) (integral_scal formula-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integral_phi_closed formula-decl nil lebesgue_def nil) (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/") (integrable_phi_closed formula-decl nil lebesgue_def nil) (isf_integral formula-decl nil integral "measure_integration/") (singleton_is_cal_M formula-decl nil lebesgue_def nil) (phi_is_simple judgement-tcc nil measure_space "measure_integration/") (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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_times_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) (partition type-eq-decl nil integral_def "analysis/") (+ 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) (Integral const-decl "real" integral_def "analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (step_function_integrable? formula-decl nil integral_step "analysis/") (a formal-const-decl "real" riemann_scaf nil) (< const-decl "bool" reals nil) (b formal-const-decl "{x: real | a < x}" riemann_scaf nil)) shostak)) (riemann_lebesgue_step_integrable 0 (riemann_lebesgue_step_integrable-1 nil 3420256049 ("" (skosimp) (("" (lemma "riemann_lebesgue_step_isf" ("phi" "phi!1")) (("" (flatten) (("" (assert) (("" (hide -1) (("" (lemma "isf_is_integrable") (("" (inst - "phi!1") (("" (assert) (("" (replace -3) (("" (rewrite "isf_integral") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((step nonempty-type-eq-decl nil riemann_scaf nil) (step? const-decl "bool" riemann_scaf 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) (riemann_lebesgue_step_isf formula-decl nil riemann_scaf nil) (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (isf_is_integrable judgement-tcc nil integral "measure_integration/") (isf_integral formula-decl nil integral "measure_integration/") (isf nonempty-type-eq-decl nil isf "measure_integration/") (isf? const-decl "bool" isf "measure_integration/")) shostak)) (step_function_is_simple 0 (step_function_is_simple-1 nil 3420258089 ("" (skosimp) (("" (typepred "x!1") (("" (lemma "riemann_lebesgue_step_isf" ("phi" "x!1")) (("" (flatten) (("" (expand "isf?") (("" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((step nonempty-type-eq-decl nil riemann_scaf nil) (step? const-decl "bool" riemann_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) (isf? const-decl "bool" isf "measure_integration/") (riemann_lebesgue_step_isf formula-decl nil riemann_scaf nil)) shostak)) (step_function_is_bounded 0 (step_function_is_bounded-1 nil 3450584200 ("" (skolem + "phi!1") (("" (typepred "phi!1") (("" (expand "zeroed_bounded?") (("" (expand "step?") (("" (flatten) (("" (assert) (("" (lemma "step_function_is_simple") (("" (inst - "phi!1") (("" (lemma "simple_is_bounded_measurable") (("" (inst - "phi!1") (("" (expand "bounded_measurable?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((step nonempty-type-eq-decl nil riemann_scaf nil) (step? const-decl "bool" riemann_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) (simple nonempty-type-eq-decl nil measure_space "measure_integration/") (simple? const-decl "bool" measure_space "measure_integration/") (bounded_measurable? const-decl "bool" measure_space "measure_integration/") (simple_is_bounded_measurable judgement-tcc nil measure_space "measure_integration/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (step_function_is_simple judgement-tcc nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf nil)) shostak)) (lower_step_exists 0 (lower_step_exists-1 nil 3450706122 ("" (skosimp) (("" (typepred "f!1") (("" (expand "zeroed_bounded?") (("" (expand "bounded?") (("" (flatten) (("" (skosimp*) (("" (lemma "integrable_phi_closed" ("a" "a" "b" "b")) (("1" (lemma "integrable_scal" ("c" "-c!1" "f" "phi(closed(a, b))")) (("1" (inst + "*[real](-c!1, phi(closed(a, b)))") (("1" (hide-all-but (-3 -4 1)) (("1" (expand "<=" 1) (("1" (skosimp) (("1" (expand "zeroed?") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step?") (("2" (split) (("1" (expand "step_function?") (("1" (inst + "(# length := 2, seq := (LAMBDA (ii: below(2)): if ii = 0 then a else b endif) #)") (("1" (expand "step_function_on?") (("1" (skosimp) (("1" (inst + "-c!1") (("1" (skosimp) (("1" (hide-all-but 1) (("1" (typepred "x!1") (("1" (expand "phi") (("1" (expand "member") (("1" (expand "closed") (("1" (expand "closed_ball") (("1" (expand "*") (("1" (case-replace "abs((a + b) / 2 - x!1) <= (b - a) / 2") (("1" (assert) nil nil) ("2" (hide 2) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil) ("4" (skosimp) (("4" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "zeroed?" 1) (("2" (skosimp) (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_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? const-decl "bool" sup_norm "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (closed const-decl "closed_interval" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (phi const-decl "nat" measure_space "measure_integration/") (nat nonempty-type-eq-decl nil naturalnumbers 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) (set type-eq-decl nil sets nil) (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (integrable_scal judgement-tcc nil integral "measure_integration/") (minus_real_is_real application-judgement "real" reals nil) (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (step_function? const-decl "bool" step_fun_def "analysis/") (step_function_on? const-decl "bool" step_fun_def "analysis/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (open_interval type-eq-decl nil intervals_real "reals/") (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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def "analysis/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_even_is_even application-judgement "even_int" integers nil) (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (zeroed? const-decl "bool" riemann_scaf nil) (<= const-decl "bool" real_fun_orders "reals/") (step nonempty-type-eq-decl nil riemann_scaf nil) (c!1 skolem-const-decl "nnreal" riemann_scaf nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (step? const-decl "bool" riemann_scaf nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (integrable_phi_closed formula-decl nil lebesgue_def nil) (a formal-const-decl "real" riemann_scaf nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (b formal-const-decl "{x: real | a < x}" riemann_scaf nil)) shostak)) (upper_step_exists 0 (upper_step_exists-1 nil 3450706482 ("" (skosimp) (("" (lemma "lower_step_exists" ("f" "-f!1")) (("1" (skosimp) (("1" (inst + "-phi!1") (("1" (expand "<=") (("1" (skosimp) (("1" (inst - "x!1") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (typepred "phi!1") (("2" (hide -2) (("2" (expand "step?") (("2" (flatten) (("2" (split) (("1" (hide -2) (("1" (expand "step_function?") (("1" (skosimp) (("1" (inst + "P!1") (("1" (expand "step_function_on?") (("1" (skosimp) (("1" (inst - "ii!1") (("1" (skosimp) (("1" (inst + "-fv!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "zeroed?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "f!1") (("2" (expand "zeroed_bounded?") (("2" (flatten) (("2" (split) (("1" (expand "bounded?") (("1" (skosimp) (("1" (inst + "c!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "zeroed?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[T -> real]" real_fun_ops "reals/") (bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf 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) (lower_step_exists formula-decl nil riemann_scaf nil) (simple_neg application-judgement "simple[real, cal_M]" lebesgue_def nil) (opp_measurable application-judgement "measurable_function[real, cal_M]" lebesgue_def nil) (step? const-decl "bool" riemann_scaf nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (phi!1 skolem-const-decl "step" riemann_scaf nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" real_fun_orders "reals/") (zeroed? const-decl "bool" riemann_scaf nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (step_function_on? const-decl "bool" step_fun_def "analysis/") (- const-decl "[numfield -> numfield]" number_fields nil) (open_interval type-eq-decl nil intervals_real "reals/") (partition type-eq-decl nil integral_def "analysis/") (+ 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/") (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf 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) (step_function? const-decl "bool" step_fun_def "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (bounded? const-decl "bool" sup_norm "measure_integration/") (nnreal type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) shostak)) (lower_riemann_integral_TCC1 0 (lower_riemann_integral_TCC1-1 nil 3450707160 ("" (skosimp) (("" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!1")) (("" (flatten) nil nil)) nil)) nil) ((step nonempty-type-eq-decl nil riemann_scaf nil) (step? const-decl "bool" riemann_scaf 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) (riemann_lebesgue_step_integrable formula-decl nil riemann_scaf nil)) nil)) (lower_riemann_integral_TCC2 0 (lower_riemann_integral_TCC2-1 nil 3450707160 ("" (skosimp) (("" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "lower_step_exists" ("f" "f!1")) (("1" (skosimp) (("1" (inst - "Integral(a,b,phi!1)") (("1" (inst + "phi!1") (("1" (assert) (("1" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!1")) (("1" (flatten) nil nil)) nil)) nil)) nil) ("2" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!1")) (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "above_bounded") (("2" (typepred "f!1") (("2" (expand "zeroed_bounded?") (("2" (flatten) (("2" (expand "bounded?") (("2" (skosimp) (("2" (inst + "(b-a)*c!1") (("2" (expand "upper_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (expand "<=" -1) (("2" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!1")) (("2" (flatten) (("2" (replace -5) (("2" (hide -1 -3 -5) (("2" (lemma "integrable_phi_closed" ("a" "a" "b" "b")) (("1" (lemma "integral_phi_closed" ("a" "a" "b" "b")) (("1" (lemma "integrable_scal" ("c" "c!1" "f" "phi(closed(a, b))")) (("1" (lemma "integral_scal" ("c" "c!1" "f" "phi(closed(a, b))")) (("1" (replace -3) (("1" (lemma "integral_ae_le" ("f1" "phi!1" "f2" "*[real](c!1, phi(closed(a, b)))")) (("1" (split -1) (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (1 -6 -7 -8)) (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "emptyset[real]") (("2" (expand "emptyset") (("2" (skosimp) (("2" (expand "phi") (("2" (expand "member") (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "zeroed?") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf 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) (lower_step_exists formula-decl nil riemann_scaf nil) (phi!1 skolem-const-decl "step" riemann_scaf nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (step? const-decl "bool" riemann_scaf nil) (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf nil) (Integrable? const-decl "bool" integral_def "analysis/") (Integrable_funs type-eq-decl nil integral_def "analysis/") (Integral const-decl "real" integral_def "analysis/") (riemann_lebesgue_step_integrable formula-decl nil riemann_scaf nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (upper_bound const-decl "bool" bound_defs "reals/") (integral const-decl "real" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" real_fun_orders "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (integral_phi_closed formula-decl nil lebesgue_def nil) (integral_scal formula-decl nil integral "measure_integration/") (integral_ae_le formula-decl nil integral "measure_integration/") (* const-decl "[T -> real]" real_fun_ops "reals/") (pointwise_ae? const-decl "bool" measure_theory "measure_integration/") (fullset const-decl "set" sets nil) (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (finite_emptyset name-judgement "finite_set[real]" integral_def "analysis/") (subset_algebra_emptyset name-judgement "(cal_M)" lebesgue_def nil) (outer_negligible_emptyset name-judgement "outer_negligible[real, lebesgue_outer_measure]" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(induced_sigma_algebra)" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(lebesgue_measurable)" real_lebesgue_scaf nil) (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[T]" bounded_nats "orders/") (finite_emptyset name-judgement "finite_set[T]" step_fun_props "analysis/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (negligible nonempty-type-eq-decl nil measure_theory "measure_integration/") (negligible_set? const-decl "bool" measure_theory "measure_integration/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (zeroed? const-decl "bool" riemann_scaf nil) (TRUE const-decl "bool" booleans nil) (ae_in? const-decl "bool" measure_theory "measure_integration/") (ae? const-decl "bool" measure_theory "measure_integration/") (fullset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (measurable_fullset name-judgement "measurable_set[real, cal_M]" lebesgue_def nil) (subset_algebra_fullset name-judgement "(cal_M)" lebesgue_def nil) (real_is_complete name-judgement "metric_complete" real_topology "metric_space/") (subset_algebra_fullset name-judgement "(induced_sigma_algebra)" real_lebesgue_scaf nil) (subset_algebra_fullset name-judgement "(lebesgue_measurable)" real_lebesgue_scaf nil) (ae_le? const-decl "bool" measure_theory "measure_integration/") (real_minus_real_is_real application-judgement "real" reals nil) (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (integrable_scal judgement-tcc nil integral "measure_integration/") (set type-eq-decl nil sets 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phi const-decl "nat" measure_space "measure_integration/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (integrable_phi_closed formula-decl nil lebesgue_def nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (bounded? const-decl "bool" sup_norm "measure_integration/") (above_bounded const-decl "bool" bounded_reals "reals/")) nil)) (upper_riemann_integral_TCC1 0 (upper_riemann_integral_TCC1-1 nil 3450716455 ("" (skosimp) (("" (lemma "riemann_lebesgue_step_integrable" ("phi" "psi!1")) (("" (flatten) nil nil)) nil)) nil) ((step nonempty-type-eq-decl nil riemann_scaf nil) (step? const-decl "bool" riemann_scaf 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) (riemann_lebesgue_step_integrable formula-decl nil riemann_scaf nil)) nil)) (upper_riemann_integral_TCC2 0 (upper_riemann_integral_TCC2-1 nil 3450716455 ("" (skosimp) (("" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "upper_step_exists" ("f" "f!1")) (("1" (skosimp) (("1" (lemma "riemann_lebesgue_step_integrable" ("phi" "psi!1")) (("1" (flatten) (("1" (inst - "Integral[real](a, b, psi!1)") (("1" (inst + "psi!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (typepred "f!1") (("2" (expand "zeroed_bounded?") (("2" (flatten) (("2" (expand "bounded?") (("2" (skosimp) (("2" (inst + "(-c!1)*(b-a)") (("2" (expand "lower_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (lemma "riemann_lebesgue_step_integrable" ("phi" "psi!1")) (("2" (flatten) (("2" (lemma "integrable_phi_closed" ("a" "a" "b" "b")) (("1" (lemma "integral_phi_closed" ("a" "a" "b" "b")) (("1" (lemma "integrable_scal" ("c" "(-c!1)" "f" "phi(closed(a, b))")) (("1" (lemma "integral_scal" ("c" "(-c!1)" "f" "phi(closed(a, b))")) (("1" (replace -3) (("1" (lemma "integral_ae_le" ("f2" "psi!1" "f1" "*[real]((-c!1), phi(closed(a, b)))")) (("1" (split -1) (("1" (replace -2) (("1" (replace -10) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (1 -11 -10 -8)) (("2" (expand "<=") (("2" (expand "ae_le?") (("2" (expand "pointwise_ae?") (("2" (expand "ae?") (("2" (expand "fullset") (("2" (expand "ae_in?") (("2" (inst + "emptyset[real]") (("2" (skosimp) (("2" (expand "emptyset") (("2" (expand "*") (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "zeroed?") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf 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) (upper_step_exists formula-decl nil riemann_scaf nil) (riemann_lebesgue_step_integrable formula-decl nil riemann_scaf nil) (step? const-decl "bool" riemann_scaf nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf nil) (Integral const-decl "real" integral_def "analysis/") (Integrable_funs type-eq-decl nil integral_def "analysis/") (Integrable? const-decl "bool" integral_def "analysis/") (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_real_is_real application-judgement "real" reals nil) (lower_bound const-decl "bool" bound_defs "reals/") (integral const-decl "real" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" real_fun_orders "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (integrable_phi_closed formula-decl nil lebesgue_def nil) (<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (closed_is_measurable application-judgement "measurable_set" lebesgue_def nil) (integrable_scal judgement-tcc nil integral "measure_integration/") (set type-eq-decl nil sets 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phi const-decl "nat" measure_space "measure_integration/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (pointwise_ae? const-decl "bool" measure_theory "measure_integration/") (fullset const-decl "set" sets nil) (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (finite_emptyset name-judgement "finite_set[real]" integral_def "analysis/") (subset_algebra_emptyset name-judgement "(cal_M)" lebesgue_def nil) (outer_negligible_emptyset name-judgement "outer_negligible[real, lebesgue_outer_measure]" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(induced_sigma_algebra)" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(lebesgue_measurable)" real_lebesgue_scaf nil) (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[T]" bounded_nats "orders/") (finite_emptyset name-judgement "finite_set[T]" step_fun_props "analysis/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (negligible nonempty-type-eq-decl nil measure_theory "measure_integration/") (negligible_set? const-decl "bool" measure_theory "measure_integration/") (TRUE const-decl "bool" booleans nil) (zeroed? const-decl "bool" riemann_scaf nil) (minus_even_is_even application-judgement "even_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ae_in? const-decl "bool" measure_theory "measure_integration/") (ae? const-decl "bool" measure_theory "measure_integration/") (fullset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (measurable_fullset name-judgement "measurable_set[real, cal_M]" lebesgue_def nil) (subset_algebra_fullset name-judgement "(cal_M)" lebesgue_def nil) (real_is_complete name-judgement "metric_complete" real_topology "metric_space/") (subset_algebra_fullset name-judgement "(induced_sigma_algebra)" real_lebesgue_scaf nil) (subset_algebra_fullset name-judgement "(lebesgue_measurable)" real_lebesgue_scaf nil) (ae_le? const-decl "bool" measure_theory "measure_integration/") (* const-decl "[T -> real]" real_fun_ops "reals/") (integral_ae_le formula-decl nil integral "measure_integration/") (integral_scal formula-decl nil integral "measure_integration/") (integral_phi_closed formula-decl nil lebesgue_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (bounded? const-decl "bool" sup_norm "measure_integration/") (below_bounded const-decl "bool" bounded_reals "reals/")) nil)) (lower_riemann_prop1 0 (lower_riemann_prop1-1 nil 3450818440 ("" (skosimp) (("" (name "RHS" "lower_riemann_integral(f!1) - epsilon!1") (("" (replace -1) (("" (expand "lower_riemann_integral") (("" (typepred "sup({z | EXISTS phi: phi <= f!1 AND z = integral(phi)})") (("1" (name-replace "SUP" "sup({z | EXISTS phi: phi <= f!1 AND z = integral(phi)})") (("1" (expand "least_upper_bound") (("1" (flatten) (("1" (expand "upper_bound") (("1" (inst -2 "SUP-epsilon!1") (("1" (assert) (("1" (skosimp) (("1" (typepred "z!1") (("1" (skosimp) (("1" (replace -2) (("1" (inst + "phi!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "lower_riemann_integral_TCC2" ("f" "f!1")) (("2" (propax) nil nil)) nil) ("3" (skosimp) (("3" (lemma "lower_riemann_integral_TCC1" ("f" "f!1")) (("3" (inst - "phi!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (lower_riemann_integral const-decl "real" riemann_scaf nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil) (lower_riemann_integral_TCC1 subtype-tcc nil riemann_scaf nil) (lower_riemann_integral_TCC2 subtype-tcc nil riemann_scaf nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (upper_bound const-decl "bool" bound_defs "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (above_bounded const-decl "bool" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (step? const-decl "bool" riemann_scaf nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" real_fun_orders "reals/") (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integral const-decl "real" integral "measure_integration/")) shostak)) (upper_riemann_prop1 0 (upper_riemann_prop1-1 nil 3450819321 ("" (skosimp) (("" (name "RHS" "upper_riemann_integral(f!1) + epsilon!1") (("" (replace -1) (("" (expand "upper_riemann_integral") (("" (typepred "inf({z | EXISTS psi: f!1 <= psi AND z = integral(psi)})") (("1" (name-replace "INF" "inf({z | EXISTS psi: f!1 <= psi AND z = integral(psi)})") (("1" (expand "greatest_lower_bound") (("1" (flatten) (("1" (expand "lower_bound") (("1" (inst -2 "INF+epsilon!1") (("1" (assert) (("1" (skosimp) (("1" (typepred "z!1") (("1" (skosimp) (("1" (replace -2) (("1" (replace -4) (("1" (inst + "psi!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "upper_riemann_integral_TCC2" ("f" "f!1")) (("2" (propax) nil nil)) nil) ("3" (lemma "upper_riemann_integral_TCC1" ("f" "f!1")) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (upper_riemann_integral const-decl "real" riemann_scaf nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_plus_real_is_real application-judgement "real" reals nil) (upper_riemann_integral_TCC1 subtype-tcc nil riemann_scaf nil) (upper_riemann_integral_TCC2 subtype-tcc nil riemann_scaf nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lower_bound const-decl "bool" bound_defs "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (below_bounded const-decl "bool" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (step? const-decl "bool" riemann_scaf nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" real_fun_orders "reals/") (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integral const-decl "real" integral "measure_integration/")) shostak)) (lower_riemann_prop2 0 (lower_riemann_prop2-1 nil 3450823935 ("" (skosimp) (("" (expand "lower_riemann_integral") (("" (typepred "sup({z | EXISTS phi: phi <= f!1 AND z = integral(phi)})") (("1" (name-replace "RHS" "sup({z | EXISTS phi: phi <= f!1 AND z = integral(phi)})") (("1" (expand "least_upper_bound") (("1" (expand "upper_bound") (("1" (flatten) (("1" (inst - "integral(phi!1)") (("1" (inst + "phi!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "lower_riemann_integral_TCC2" ("f" "f!1")) (("2" (propax) nil nil)) nil) ("3" (lemma "lower_riemann_integral_TCC1" ("f" "f!1")) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((lower_riemann_integral const-decl "real" riemann_scaf nil) (lower_riemann_integral_TCC1 subtype-tcc nil riemann_scaf nil) (lower_riemann_integral_TCC2 subtype-tcc nil riemann_scaf nil) (upper_bound const-decl "bool" bound_defs "reals/") (f!1 skolem-const-decl "bounded" riemann_scaf nil) (phi!1 skolem-const-decl "step" riemann_scaf nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (pred type-eq-decl nil defined_types nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (above_bounded const-decl "bool" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (step? const-decl "bool" riemann_scaf nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" real_fun_orders "reals/") (zeroed_bounded? const-decl "bool" riemann_scaf nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (= const-decl "[T, T -> boolean]" equalities nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integral const-decl "real" integral "measure_integration/")) shostak)) (upper_riemann_prop2 0 (upper_riemann_prop2-1 nil 3450823809 ("" (skosimp) (("" (expand "upper_riemann_integral") (("" (typepred "inf({z | EXISTS psi: f!1 <= psi AND z = integral(psi)})") (("1" (name-replace "LHS" "inf({z | EXISTS psi: f!1 <= psi AND z = integral(psi)})") (("1" (expand "greatest_lower_bound") (("1" (flatten) (("1" (expand "lower_bound") (("1" (inst -1 "integral(psi!1)") (("1" (inst + "psi!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "upper_riemann_integral_TCC2" ("f" "f!1")) (("2" (propax) nil nil)) nil) ("3" (lemma "upper_riemann_integral_TCC1" ("f" "f!1")) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((upper_riemann_integral const-decl "real" riemann_scaf nil) (upper_riemann_integral_TCC1 subtype-tcc nil riemann_scaf nil) (upper_riemann_integral_TCC2 subtype-tcc nil riemann_scaf nil) (f!1 skolem-const-decl "bounded" riemann_scaf nil) (psi!1 skolem-const-decl "step" riemann_scaf nil) (lower_bound const-decl "bool" bound_defs "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (pred type-eq-decl nil defined_types nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (below_bounded const-decl "bool" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (step? const-decl "bool" riemann_scaf nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" real_fun_orders "reals/") (zeroed_bounded? const-decl "bool" riemann_scaf nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (= const-decl "[T, T -> boolean]" equalities nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (integrable? const-decl "bool" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integral const-decl "real" integral "measure_integration/")) shostak)) (lower_upper_riemann_prop 0 (lower_upper_riemann_prop-1 nil 3450793358 ("" (skosimp) (("" (expand "upper_riemann_integral") (("" (expand "lower_riemann_integral") (("" (typepred "sup({z | EXISTS phi: phi <= f!1 AND z = integral(phi)})") (("1" (name-replace "LOW" "sup({z | EXISTS phi: phi <= f!1 AND z = integral(phi)})") (("1" (typepred "inf({z | EXISTS psi: f!1 <= psi AND z = integral(psi)})") (("1" (name-replace "HIGH" "inf({z | EXISTS psi: f!1 <= psi AND z = integral(psi)})") (("1" (expand "greatest_lower_bound") (("1" (expand "least_upper_bound") (("1" (flatten) (("1" (inst -4 "HIGH") (("1" (split -4) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (expand "upper_bound" 1) (("3" (skosimp) (("3" (typepred "z!1") (("3" (skosimp) (("3" (inst -4 "z!1") (("3" (split -4) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (expand "lower_bound" 1) (("3" (skosimp) (("3" (typepred "z!2") (("3" (skosimp) (("3" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!1")) (("3" (lemma "riemann_lebesgue_step_integrable" ("phi" "psi!1")) (("3" (flatten) (("3" (replace -3) (("3" (replace -6) (("3" (hide -1 -3 -4 -6 -11 -12) (("3" (replace -4) (("3" (replace -6) (("3" (hide -4 -6 2 3) (("3" (lemma "integral_ae_le" ("f1" "phi!1" "f2" "psi!1")) (("3" (assert) (("3" (hide -1 -2 2) (("3" (expand "<=") (("3" (expand "ae_le?") (("3" (expand "pointwise_ae?") (("3" (expand "ae?") (("3" (expand "fullset") (("3" (expand "ae_in?") (("3" (inst + "emptyset[real]") (("3" (skosimp) (("3" (inst - "x!1") (("3" (inst - "x!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "upper_riemann_integral_TCC2" ("f" "f!1")) (("2" (propax) nil nil)) nil) ("3" (skosimp) (("3" (lemma "riemann_lebesgue_step_integrable" ("phi" "psi!1")) (("3" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "lower_riemann_integral_TCC2" ("f" "f!1")) (("2" (propax) nil nil)) nil) ("3" (skosimp) (("3" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!1")) (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((upper_riemann_integral const-decl "real" riemann_scaf nil) (integral const-decl "real" integral "measure_integration/") (integrable nonempty-type-eq-decl nil integral "measure_integration/") (integrable? const-decl "bool" integral "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf nil) (<= const-decl "bool" real_fun_orders "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (step? const-decl "bool" riemann_scaf nil) (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (setof type-eq-decl nil defined_types nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (integral_ae_le formula-decl nil integral "measure_integration/") (ae_le? const-decl "bool" measure_theory "measure_integration/") (subset_algebra_fullset name-judgement "(lebesgue_measurable)" real_lebesgue_scaf nil) (subset_algebra_fullset name-judgement "(induced_sigma_algebra)" real_lebesgue_scaf nil) (real_is_complete name-judgement "metric_complete" real_topology "metric_space/") (subset_algebra_fullset name-judgement "(cal_M)" lebesgue_def nil) (measurable_fullset name-judgement "measurable_set[real, cal_M]" lebesgue_def nil) (fullset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (ae? const-decl "bool" measure_theory "measure_integration/") (ae_in? const-decl "bool" measure_theory "measure_integration/") (member const-decl "bool" sets nil) (TRUE const-decl "bool" booleans nil) (negligible_set? const-decl "bool" measure_theory "measure_integration/") (negligible nonempty-type-eq-decl nil measure_theory "measure_integration/") (emptyset const-decl "set" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" step_fun_props "analysis/") (finite_emptyset name-judgement "finite_set[T]" bounded_nats "orders/") (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (subset_algebra_emptyset name-judgement "(lebesgue_measurable)" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(induced_sigma_algebra)" real_lebesgue_scaf nil) (outer_negligible_emptyset name-judgement "outer_negligible[real, lebesgue_outer_measure]" real_lebesgue_scaf nil) (subset_algebra_emptyset name-judgement "(cal_M)" lebesgue_def nil) (finite_emptyset name-judgement "finite_set[real]" integral_def "analysis/") (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (fullset const-decl "set" sets nil) (pointwise_ae? const-decl "bool" measure_theory "measure_integration/") (riemann_lebesgue_step_integrable formula-decl nil riemann_scaf nil) (lower_bound const-decl "bool" bound_defs "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (upper_riemann_integral_TCC2 subtype-tcc nil riemann_scaf nil) (lower_riemann_integral_TCC2 subtype-tcc nil riemann_scaf nil) (lower_riemann_integral const-decl "real" riemann_scaf nil)) shostak)) (riemann_integrable_def1 0 (riemann_integrable_def1-1 nil 3450803522 ("" (skosimp) (("" (lemma "lower_upper_riemann_prop" ("f" "f!1")) (("" (expand "<=") (("" (split) (("1" (assert) (("1" (name "EPS" "(upper_riemann_integral(f!1)-lower_riemann_integral(f!1))/2") (("1" (case "EPS>0") (("1" (lemma "steps_exist[real]" ("a" "a" "b" "b" "f" "f!1")) (("1" (expand "Integrable?") (("1" (assert) (("1" (inst - "EPS") (("1" (skolem - ("phi!1" "psi!1")) (("1" (flatten) (("1" (hide -9) (("1" (name "phi!2" "lambda x: if a <= x AND x <= b then phi!1(x) else 0 endif") (("1" (name "psi!2" "lambda x: if a <= x AND x <= b then psi!1(x) else 0 endif") (("1" (case "step?(phi!2)") (("1" (case "step?(psi!2)") (("1" (hide -3 -4 -5 -6) (("1" (case "phi!2<=f!1 & f!1 <= psi!2") (("1" (lemma "lower_riemann_prop2" ("phi" "phi!2" "f" "f!1")) (("1" (lemma "upper_riemann_prop2" ("psi" "psi!2" "f" "f!1")) (("1" (flatten -3) (("1" (assert) (("1" (hide -7) (("1" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!2")) (("1" (lemma "riemann_lebesgue_step_integrable" ("phi" "psi!2")) (("1" (flatten) (("1" (lemma "Integral_diff[real]" ("a" "a" "b" "b" "f" "psi!2" "g" "phi!2")) (("1" (assert) (("1" (flatten) (("1" (expand "-" (-15 -16)) (("1" (lemma "integral_restrict_eq" ("a" "a" "b" "b" "f" "LAMBDA (x: real): psi!2(x) - phi!2(x)" "g" "LAMBDA (x: real): psi!1(x) - phi!1(x)")) (("1" (assert) (("1" (split -1) (("1" (replace -1) (("1" (expand "Integral" -3) (("1" (replace -3) (("1" (expand "Integral") (("1" (replace -6) (("1" (replace -9) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "psi!2") (("2" (expand "phi!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "Integrable?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "<=" 1) (("2" (typepred "f!1") (("2" (expand "zeroed_bounded?") (("2" (flatten) (("2" (hide -1) (("2" (expand "zeroed?") (("2" (split 1) (("1" (skosimp) (("1" (inst - "x!1") (("1" (expand "phi!2") (("1" (case "a <= x!1 AND x!1 <= b") (("1" (inst -3 "x!1") (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (replace 1 2) (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "psi!2") (("2" (case-replace "a <= x!1 AND x!1 <= b") (("1" (inst -3 "x!1") (("1" (grind) nil nil)) nil) ("2" (replace 1 2) (("2" (inst -1 "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (expand "step?") (("2" (expand "psi!2") (("2" (split) (("1" (expand "step_function?") (("1" (skosimp) (("1" (inst + "P!1") (("1" (expand "step_function_on?") (("1" (skosimp) (("1" (inst - "ii!1") (("1" (skosimp) (("1" (inst + "fv!1") (("1" (skosimp) (("1" (typepred "x!1") (("1" (typepred "P!1") (("1" (assert) (("1" (inst -7 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "zeroed?") (("2" (skosimp) (("2" (split) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "phi!2") (("2" (expand "step?") (("2" (split) (("1" (expand "step_function?") (("1" (skosimp) (("1" (inst + "P!1") (("1" (expand "step_function_on?") (("1" (skosimp) (("1" (inst - "ii!1") (("1" (skosimp) (("1" (inst + "fv!1") (("1" (skosimp) (("1" (typepred "x!1") (("1" (typepred "P!1") (("1" (inst -7 "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "zeroed?") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "step_to_integrable[real]" ("a" "a" "b" "b" "f" "f!1")) (("2" (expand "Integrable?") (("2" (assert) (("2" (hide 2) (("2" (skosimp) (("2" (lemma "lower_riemann_prop1" ("f" "f!1" "epsilon" "eps!1/2")) (("2" (lemma "upper_riemann_prop1" ("f" "f!1" "epsilon" "eps!1/2")) (("2" (skosimp*) (("2" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!1")) (("2" (lemma "riemann_lebesgue_step_integrable" ("phi" "psi!1")) (("2" (flatten) (("2" (inst + "phi!1" "psi!1") (("2" (assert) (("2" (typepred "phi!1") (("2" (typepred "psi!1") (("2" (expand "step?") (("2" (flatten) (("2" (replace -1) (("2" (replace -3) (("2" (lemma "integral_diff[real]" ("a" "a" "b" "b" "f" "psi!1" "g" "phi!1")) (("2" (expand "-" 1) (("2" (assert) (("2" (expand "Integrable?") (("2" (expand "Integral") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (hide-all-but (-13 -15 1)) (("2" (skosimp) (("2" (expand "<=" (-1 -2)) (("2" (inst - "xx!1") (("2" (inst - "xx!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf 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) (lower_upper_riemann_prop formula-decl nil riemann_scaf nil) (lower_riemann_integral const-decl "real" riemann_scaf nil) (upper_riemann_integral const-decl "real" riemann_scaf nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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 "[T, T -> boolean]" equalities nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (steps_exist formula-decl nil integral_split_scaf "analysis/") (a formal-const-decl "real" riemann_scaf nil) (< const-decl "bool" reals nil) (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (<= const-decl "bool" real_fun_orders "reals/") (upper_riemann_prop2 formula-decl nil riemann_scaf nil) (riemann_lebesgue_step_integrable formula-decl nil riemann_scaf nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (psi!2 skolem-const-decl "[real -> real]" riemann_scaf nil) (phi!2 skolem-const-decl "[real -> real]" riemann_scaf nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Integral const-decl "real" integral_def "analysis/") (integral_restrict_eq formula-decl nil integral_def "analysis/") (Integral_diff formula-decl nil integral "analysis/") (step nonempty-type-eq-decl nil riemann_scaf nil) (lower_riemann_prop2 formula-decl nil riemann_scaf nil) (closed_interval type-eq-decl nil intervals_real "reals/") (x!1 skolem-const-decl "real" riemann_scaf nil) (x!1 skolem-const-decl "real" riemann_scaf nil) (zeroed? const-decl "bool" riemann_scaf nil) (NOT const-decl "[bool -> bool]" booleans nil) (step_function_on? const-decl "bool" step_fun_def "analysis/") (open_interval type-eq-decl nil intervals_real "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences 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) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def "analysis/") (step_function? const-decl "bool" step_fun_def "analysis/") (step? const-decl "bool" riemann_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Integrable? const-decl "bool" integral_def "analysis/") (> const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (step_to_integrable formula-decl nil integral_step "analysis/") (upper_riemann_prop1 formula-decl nil riemann_scaf nil) (real_plus_real_is_real application-judgement "real" reals nil) (integral_diff formula-decl nil integral_prep "analysis/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (lower_riemann_prop1 formula-decl nil riemann_scaf nil) (<= const-decl "bool" reals nil)) shostak)) (riemann_integrable_def2 0 (riemann_integrable_def2-1 nil 3450865321 ("" (skosimp) (("" (lemma "riemann_integrable_def1" ("f" "f!1")) (("" (assert) (("" (expand "Integrable?") (("" (expand "Integral") (("" (lemma "steps_exist" ("a" "a" "b" "b" "f" "f!1")) (("" (assert) (("" (name "EPS" "integral(a, b, f!1) - lower_riemann_integral(f!1)") (("" (lemma "trichotomy" ("x" "EPS")) (("" (split) (("1" (inst - "EPS/2") (("1" (skosimp) (("1" (name "phi!1" "lambda x: if a <=x&x<=b then f1!1(x) else 0 endif") (("1" (name "psi!1" "lambda x: if a <=x&x<=b then f2!1(x) else 0 endif") (("1" (case "step?(psi!1)") (("1" (case "step?(phi!1)") (("1" (case "f!1<=psi!1") (("1" (case "phi!1<=f!1") (("1" (lemma "step_function_integrable?" ("a" "a" "b" "b" "f" "f1!1")) (("1" (lemma "step_function_integrable?" ("a" "a" "b" "b" "f" "f2!1")) (("1" (assert) (("1" (lemma "integral_restr_eq" ("a" "a" "b" "b" "f" "f1!1" "g" "phi!1")) (("1" (lemma "integral_restr_eq" ("a" "a" "b" "b" "f" "f2!1" "g" "psi!1")) (("1" (assert) (("1" (split -1) (("1" (split -2) (("1" (flatten) (("1" (hide -11 -12 -15 -16 -17) (("1" (lemma "integral_diff[real]" ("a" "a" "b" "b" "f" "psi!1" "g" "phi!1")) (("1" (assert) (("1" (flatten) (("1" (lemma "integral_diff[real]" ("a" "a" "b" "b" "f" "f2!1" "g" "f1!1")) (("1" (assert) (("1" (flatten) (("1" (hide -1) (("1" (expand "-" -17) (("1" (replace -1) (("1" (replace -5 * :dir rl) (("1" (replace -7 * :dir rl) (("1" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9) (("1" (hide -7) (("1" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!1")) (("1" (lemma "riemann_lebesgue_step_integrable" ("phi" "psi!1")) (("1" (flatten) (("1" (expand "Integral") (("1" (replace -3) (("1" (replace -6) (("1" (hide -1 -3 -4 -6) (("1" (replace -10) (("1" (lemma "upper_riemann_prop1" ("f" "f!1" "epsilon" "EPS")) (("1" (skosimp) (("1" (lemma "Integral_le" ("a" "a" "b" "b" "f" "f!1" "g" "psi!2")) (("1" (lemma "riemann_lebesgue_step_integrable" ("phi" "psi!2")) (("1" (flatten) (("1" (assert) (("1" (replace -3) (("1" (expand "Integral") (("1" (hide-all-but (-4 1)) (("1" (skosimp) (("1" (expand "<=" -1) (("1" (inst - "x!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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -6)) (("2" (expand "step?") (("2" (flatten) (("2" (hide -1) (("2" (expand "zeroed?") (("2" (expand "phi!1") (("2" (skosimp) (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-7 1)) (("2" (expand "step?") (("2" (expand "zeroed?") (("2" (expand "psi!1") (("2" (skosimp) (("2" (inst - "x!1") (("2" (hide -3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -10 -2)) (("2" (typepred "f!1") (("2" (expand "zeroed_bounded?") (("2" (expand "step?") (("2" (flatten) (("2" (hide -1 -3) (("2" (expand "<=" 1) (("2" (skosimp) (("2" (expand "zeroed?") (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (inst - "x!1") (("1" (expand "phi!1") (("1" (grind) nil nil)) nil) ("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1 -9)) (("2" (typepred "f!1") (("2" (expand "zeroed_bounded?") (("2" (expand "step?") (("2" (flatten) (("2" (hide -1 -3) (("2" (expand "<=" 1) (("2" (skosimp) (("2" (expand "zeroed?") (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (inst - "x!1") (("1" (expand "psi!1") (("1" (grind) nil nil)) nil) ("2" (expand "psi!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "step?") (("2" (hide-all-but (-6 1)) (("2" (expand "phi!1") (("2" (split) (("1" (expand "step_function?") (("1" (skosimp) (("1" (inst + "P!1") (("1" (expand "step_function_on?") (("1" (skosimp) (("1" (inst - "ii!1") (("1" (skosimp) (("1" (inst + "fv!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (assert) (("1" (typepred "x!1") (("1" (typepred "P!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "zeroed?") (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -6)) (("2" (expand "step?") (("2" (expand "psi!1") (("2" (split) (("1" (expand "step_function?") (("1" (expand "step_function_on?") (("1" (skosimp) (("1" (inst + "P!1") (("1" (skosimp) (("1" (inst - "ii!1") (("1" (skosimp) (("1" (inst + "fv!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (typepred "x!1") (("1" (typepred "P!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "zeroed?") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil) ("3" (hide-all-but (-1 -2 -4 -5 1)) (("3" (lemma "lower_riemann_prop1" ("f" "f!1" "epsilon" "-EPS")) (("1" (skosimp) (("1" (replace -4 -2 rl) (("1" (assert) (("1" (case-replace "lower_riemann_integral(f!1) - -(integral(a, b, f!1) - lower_riemann_integral(f!1)) = integral(a, b, f!1)") (("1" (hide -1) (("1" (hide-all-but (-1 -2 -5)) (("1" (lemma "integral_le" ("a" "a" "b" "b" "f" "phi!1" "g" "f!1")) (("1" (lemma "riemann_lebesgue_step_integrable" ("phi" "phi!1")) (("1" (flatten) (("1" (assert) (("1" (expand "Integrable?" -1) (("1" (assert) (("1" (split -4) (("1" (expand "Integral") (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (expand "<=" -4) (("2" (inst -4 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf 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) (riemann_integrable_def1 formula-decl nil riemann_scaf nil) (Integrable? const-decl "bool" integral_def "analysis/") (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf nil) (steps_exist formula-decl nil integral_split_scaf "analysis/") (lower_riemann_integral const-decl "real" riemann_scaf nil) (integral const-decl "{S: real | integral?(a, b, ff, S)}" integral_def "analysis/") (integral? const-decl "bool" integral_def "analysis/") (integrable? const-decl "bool" integral_def "analysis/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "real" riemann_scaf nil) (integral_restr_eq formula-decl nil integral_prep "analysis/") (psi!1 skolem-const-decl "[real -> real]" riemann_scaf nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (riemann_lebesgue_step_integrable formula-decl nil riemann_scaf nil) (step nonempty-type-eq-decl nil riemann_scaf nil) (upper_riemann_prop1 formula-decl nil riemann_scaf nil) (Integral_le formula-decl nil integral "analysis/") (closed_interval type-eq-decl nil intervals_real "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (integral_diff formula-decl nil integral_prep "analysis/") (phi!1 skolem-const-decl "[real -> real]" riemann_scaf nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (zeroed? const-decl "bool" riemann_scaf nil) (step_function_integrable? formula-decl nil integral_step "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (x!1 skolem-const-decl "real" riemann_scaf nil) (<= const-decl "bool" real_fun_orders "reals/") (step_function? const-decl "bool" step_fun_def "analysis/") (partition type-eq-decl nil integral_def "analysis/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers 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) (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) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (open_interval type-eq-decl nil intervals_real "reals/") (step_function_on? const-decl "bool" step_fun_def "analysis/") (step? const-decl "bool" riemann_scaf nil) (<= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (EPS skolem-const-decl "real" riemann_scaf nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (minus_real_is_real application-judgement "real" reals nil) (lower_riemann_prop1 formula-decl nil riemann_scaf nil) (- const-decl "[numfield -> numfield]" number_fields nil) (integral_le formula-decl nil integral_prep "analysis/") (trichotomy formula-decl nil real_axioms nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Integral const-decl "real" integral_def "analysis/")) shostak)) (ii_of_x_TCC1 0 (ii_of_x_TCC1-1 nil 3450935427 ("" (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)) nil)) (ii_of_x_TCC2 0 (ii_of_x_TCC2-1 nil 3450935427 ("" (skosimp) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (ii_of_x_TCC3 0 (ii_of_x_TCC3-1 nil 3450935427 ("" (skosimp) (("" (typepred "x!1") (("" (lemma "part_in" ("a" "a" "b" "b" "P" "P!1" "x" "x!1")) (("" (assert) (("" (skosimp) (("" (expand "<=" -2) (("" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "ii!1") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "P!1") (("2" (typepred "ii!1") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst -10 "ii!1+1") (("1" (expand "member") (("1" (assert) (("1" (assert) (("1" (inst -5 "ii!1+1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (a formal-const-decl "real" riemann_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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil) (ii!1 skolem-const-decl "below(length(P!1) - 1)" riemann_scaf nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty? const-decl "bool" sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (part_in formula-decl nil integral_def "analysis/") (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) (= 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 "analysis/")) nil)) (ii_of_x_def 0 (ii_of_x_def-1 nil 3451310505 ("" (skosimp) (("" (expand "ii_of_x") (("" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)}")) (("" (case "nonempty?({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (split -2) (("1" (split 1) (("1" (flatten) (("1" (replace -1) (("1" (hide -1) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (name-replace "CC" "choose[below(length(P!1) - 1)] ({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("2" (expand "member") (("2" (flatten) (("2" (hide -5) (("2" (expand "<=" -1) (("2" (split) (("1" (expand "<=" -3) (("1" (split) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b" "P" "P!1" "ii" "ii!1" "jj" "CC" "x" "x!1")) (("1" (assert) nil nil)) nil) ("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "ii!1" "CC") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "<=" -3) (("2" (split) (("1" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("1" (assert) (("1" (inst - "P!1") (("1" (inst - "CC" "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -3 -4) (("2" (lemma "trich_lt" ("x" "CC" "y" "ii!1")) (("2" (split) (("1" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "ii" "CC" "jj" "ii!1")) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "jj" "CC" "ii" "ii!1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (lemma "part_in" ("a" "a" "b" "b" "P" "P!1" "x" "x!1")) (("2" (assert) (("2" (skosimp) (("2" (expand "<=" -2) (("2" (split) (("1" (inst - "ii!2") (("1" (assert) nil nil)) nil) ("2" (typepred "x!1") (("2" (typepred "P!1") (("2" (typepred "ii!2") (("2" (case-replace "ii!2=length(P!1)-2") (("1" (assert) nil nil) ("2" (inst -10 "ii!2+1") (("1" (assert) (("1" (assert) (("1" (inst - "ii!2+1") (("1" (assert) nil nil)) 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) ((ii_of_x const-decl "below(length(P) - 1)" riemann_scaf nil) (int_minus_int_is_int application-judgement "int" integers nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (trich_lt formula-decl nil real_props nil) (parts_order formula-decl nil integral_def "analysis/") (part_not_in formula-decl nil integral_def "analysis/") (parts_disjoint formula-decl nil integral_def "analysis/") (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) (NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil) (ii!2 skolem-const-decl "below(length(P!1) - 1)" riemann_scaf 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) (part_in formula-decl nil integral_def "analysis/") (empty? const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (choose_member formula-decl nil sets_lemmas nil) (set type-eq-decl nil sets 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf nil) (b formal-const-decl "{x: real | a < x}" riemann_scaf 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 "analysis/")) shostak)) (ii_of_x_prop 0 (ii_of_x_prop-1 nil 3451018544 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (lemma "part_in" ("a" "a" "b" "b" "P" "P!1" "x" "x!1")) (("1" (assert) (("1" (skolem - "II_X") (("1" (flatten) (("1" (typepred "x!1") (("1" (typepred "II_X") (("1" (expand "<=" -5) (("1" (split -5) (("1" (case-replace "ii_of_x(P!1)(x!1)=II_X") (("1" (hide -1) (("1" (inst + "II_X") (("1" (assert) (("1" (hide -1 -2 -3 -4 -5) (("1" (expand "ii_of_x") (("1" (typepred "y!1") (("1" (lemma "part_in" ("a" "a" "b" "b" "P" "P!1" "x" "y!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -6) (("2" (expand "ii_of_x") (("2" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)}")) (("2" (name-replace "LHS" "choose[below(length(P!1) - 1)] ({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (expand "member") (("1" (split) (("1" (flatten) (("1" (expand "<=" (-1 -7)) (("1" (split) (("1" (split -7) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b" "P" "P!1" "x" "x!1" "ii" "LHS" "jj" "II_X")) (("1" (assert) nil nil)) nil) ("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "LHS" "II_X") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("1" (assert) (("1" (inst - "P!1") (("1" (inst - "II_X" "LHS") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (lemma "trich_lt" ("x" "LHS" "y" "II_X")) (("2" (split) (("1" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "ii" "LHS" "jj" "II_X")) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "jj" "LHS" "ii" "II_X")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (inst - "II_X") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (hide 1 -2) (("2" (expand "empty?") (("2" (inst - "II_X") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "II_X=length(P!1)-2") (("1" (typepred "P!1") (("1" (assert) nil nil)) nil) ("2" (case "II_X < length(P!1)-2") (("1" (hide -3 1) (("1" (inst + "II_X+1") (("1" (assert) (("1" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "ii" "1+II_X" "jj" "2+II_X")) (("1" (assert) (("1" (case-replace "ii_of_x(P!1)(x!1)=II_X+1") (("1" (hide -1 -2 -4 -5 -6 -7) (("1" (expand "ii_of_x") (("1" (typepred "y!1") (("1" (lemma "part_in" ("a" "a" "b" "b" "P" "P!1" "x" "y!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -7) (("2" (expand "ii_of_x") (("2" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)}")) (("2" (case "nonempty?[below(length(P!1) - 1)]({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (split -2) (("1" (name-replace "LHS" "choose[below(length(P!1) - 1)] ({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (expand "member") (("1" (flatten) (("1" (expand "<=" -1) (("1" (split) (("1" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("1" (assert) (("1" (inst - "P!1") (("1" (inst - "LHS" "1+II_X") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -6 1)) (("2" (lemma "trich_lt" ("x" "LHS" "y" "1+II_X")) (("2" (split) (("1" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "ii" "LHS" "jj" "1+II_X")) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "jj" "LHS" "ii" "1+II_X")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "1+II_X") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "ii_of_x") (("2" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)}")) (("2" (case "nonempty?({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (split -2) (("1" (name-replace "LHS" "choose[below(length(P!1) - 1)]({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (expand "member") (("1" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= y!1 AND y!1 < seq(P!1)(1 + ii)}")) (("1" (name-replace "RHS" "choose[below(length(P!1) - 1)]({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= y!1 AND y!1 < seq(P!1)(1 + ii)})") (("1" (split -1) (("1" (expand "member") (("1" (hide -3) (("1" (flatten) (("1" (expand "<=") (("1" (split) (("1" (split) (("1" (split) (("1" (split) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b" "P" "P!1" "ii" "ii!1" "jj" "LHS" "x" "x!1")) (("1" (assert) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b" "P" "P!1" "ii" "ii!1" "jj" "RHS" "x" "y!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "y!1")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "RHS" "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "LHS" "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (split -5) (("1" (hide -3 -4 -8 1 -7) (("1" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("1" (assert) (("1" (inst - "P!1") (("1" (inst - "ii!1" "LHS") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "LHS=ii!1") (("1" (hide -1 -2 -3 -7) (("1" (split -4) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b" "P" "P!1" "ii" "ii!1" "jj" "RHS")) (("1" (inst - "y!1") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "y!1")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "RHS" "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (lemma "trich_lt" ("x" "ii!1" "y" "LHS")) (("2" (split) (("1" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "ii" "ii!1" "jj" "LHS")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "jj" "ii!1" "ii" "LHS")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split -7) (("1" (lemma "part_not_in" ("a" "a" "b" "b" "x" "y!1")) (("1" (assert) (("1" (inst - "P!1") (("1" (inst - "ii!1" "RHS") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "RHS=ii!1") (("1" (hide -1 -2 -9) (("1" (hide -1 -2) (("1" (split) (("1" (split) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b" "P" "P!1" "x" "x!1" "ii" "ii!1" "jj" "LHS")) (("1" (assert) nil nil)) nil) ("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "LHS" "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("1" (assert) (("1" (inst - "P!1") (("1" (inst - "ii!1" "LHS") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -3 -4) (("2" (lemma "trich_lt" ("x" "ii!1" "y" "LHS")) (("2" (split) (("1" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "ii" "ii!1" "jj" "LHS")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "jj" "ii!1" "ii" "LHS")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "trich_lt" ("x" "RHS" "y" "ii!1")) (("2" (split) (("1" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "ii" "RHS" "jj" "ii!1")) (("1" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (lemma "parts_order" ("a" "a" "b" "b" "P" "P!1" "jj" "RHS" "ii" "ii!1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (inst - "ii!1") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (replace -1) (("2" (hide 1) (("2" (expand "empty?") (("2" (inst - "ii!1") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil) ("2" (hide 2 -1) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (partition type-eq-decl nil integral_def "analysis/") (+ 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/") (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) (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (a formal-const-decl "real" riemann_scaf nil) (part_in formula-decl nil integral_def "analysis/") (NOT const-decl "[bool -> bool]" booleans 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) (II_X skolem-const-decl "below(length(P!1) - 1)" riemann_scaf nil) (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (ii_of_x const-decl "below(length(P) - 1)" riemann_scaf nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (trich_lt formula-decl nil real_props nil) (parts_order formula-decl nil integral_def "analysis/") (parts_disjoint formula-decl nil integral_def "analysis/") (part_not_in formula-decl nil integral_def "analysis/") (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (choose_member formula-decl nil sets_lemmas 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)) (part_set_of_TCC1 0 (part_set_of_TCC1-1 nil 3450936937 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (part_set_of_TCC2 0 (part_set_of_TCC2-1 nil 3450936937 ("" (skosimp) (("" (typepred "x!1") (("" (typepred "ii_of_x(P!1)(x!1)") (("" (assert) nil nil)) nil)) nil)) nil) ((b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (a formal-const-decl "real" riemann_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) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (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) (= 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 "analysis/") (ii_of_x const-decl "below(length(P) - 1)" riemann_scaf nil)) nil)) (part_set_of_TCC3 0 (part_set_of_TCC3-1 nil 3450937652 ("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (typepred "ii_of_x(P!1)(x!1)") (("" (inst - "(seq(P!1)(1 + ii_of_x(P!1)(x!1))+seq(P!1)(ii_of_x(P!1)(x!1)))/2") (("1" (assert) (("1" (typepred "P!1") (("1" (inst - "ii_of_x(P!1)(x!1)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil) (x!1 skolem-const-decl "{x | a <= x AND x < b}" riemann_scaf nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals 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) (< 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) (a formal-const-decl "real" riemann_scaf nil) (b formal-const-decl "{x: real | a < x}" riemann_scaf 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 "analysis/") (ii_of_x const-decl "below(length(P) - 1)" riemann_scaf nil) (empty? const-decl "bool" sets nil)) nil)) (part_set_of_prop_TCC1 0 (part_set_of_prop_TCC1-1 nil 3450944091 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (part_set_of_prop 0 (part_set_of_prop-1 nil 3450944888 ("" (skosimp) (("" (typepred "part_set_of(P!1)(x!1)") (("" (expand "restrict") (("" (expand "member") (("" (expand "part_set_of") (("" (expand "ii_of_x") (("" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)}")) (("" (case-replace "empty?({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (hide -2 2) (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "part_in" ("a" "a" "b" "b" "x" "x!1")) (("1" (inst - "P!1") (("1" (assert) (("1" (skosimp) (("1" (expand "<=" -1) (("1" (split) (("1" (expand "<=" -2) (("1" (split) (("1" (inst - "ii!1") (("1" (assert) nil nil)) nil) ("2" (typepred "ii!1") (("2" (typepred "P!1") (("2" (assert) (("2" (inst + "ii!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (name-replace "II" "choose[below(length(P!1) - 1)] ({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (expand "member") (("1" (flatten) (("1" (typepred "II") (("1" (hide -2 -3) (("1" (expand "<=" -2) (("1" (split -2) (("1" (assert) nil nil) ("2" (inst 2 "II") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((part_set_of const-decl "(nonempty?[real])" riemann_scaf nil) (partition type-eq-decl nil integral_def "analysis/") (+ 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/") (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf 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) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (choose_member formula-decl nil sets_lemmas nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (choose const-decl "(p)" sets 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_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) (part_in formula-decl nil integral_def "analysis/") (int_minus_int_is_int application-judgement "int" integers nil) (empty? const-decl "bool" sets nil) (ii_of_x const-decl "below(length(P) - 1)" riemann_scaf nil) (member const-decl "bool" sets nil)) shostak)) (lower_step_TCC1 0 (lower_step_TCC1-1 nil 3450936937 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (lower_step_TCC2 0 (lower_step_TCC2-1 nil 3450936937 ("" (skosimp) (("" (case "a < x!1 & x!1 < b") (("1" (hide 1 2) (("1" (flatten) (("1" (split) (("1" (typepred "part_set_of(P!1)(x!1)") (("1" (hide 2) (("1" (name-replace "DRL" "part_set_of(P!1)(x!1)") (("1" (expand "image") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp) (("1" (expand "member") (("1" (inst - "f!1(x!2)") (("1" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "f!1") (("2" (expand "zeroed_bounded?") (("2" (expand "bounded?") (("2" (flatten) (("2" (skosimp) (("2" (expand "below_bounded") (("2" (inst 1 "-c!1") (("2" (expand "image") (("2" (expand "lower_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (replace -1) (("2" (inst - "x!2") (("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (inst + "0") (("2" (typepred "P!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (a formal-const-decl "real" riemann_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) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (bounded? const-decl "bool" sup_norm "measure_integration/") (minus_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (lower_bound const-decl "bool" bound_defs "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs 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) (below_bounded const-decl "bool" bounded_reals "reals/") (part_set_of const-decl "(nonempty?[real])" riemann_scaf nil) (partition type-eq-decl nil integral_def "analysis/") (+ 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) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf nil) (x!2 skolem-const-decl "real" riemann_scaf nil) (DRL skolem-const-decl "(nonempty?[real])" riemann_scaf nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (image const-decl "set[R]" function_image nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (lower_step_TCC3 0 (lower_step_TCC3-1 nil 3450936937 ("" (skosimp) (("" (lemma "lower_step_TCC2" ("P" "P!1" "f" "f!1")) (("" (expand "step?") (("" (split) (("1" (expand "step_function?") (("1" (inst + "P!1") (("1" (expand "step_function_on?") (("1" (skosimp) (("1" (name "MID" "(seq(P!1)(ii!1)+ seq(P!1)(1 + ii!1))/2") (("1" (inst - "MID") (("1" (assert) (("1" (assert) (("1" (typepred "P!1") (("1" (inst - "ii!1") (("1" (assert) (("1" (split -6) (("1" (flatten) (("1" (inst + "inf[real](image[real, real](f!1, part_set_of(P!1)(MID)))") (("1" (skosimp) (("1" (typepred "x!1") (("1" (lift-if 1) (("1" (prop) (("1" (skosimp) (("1" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("1" (assert) (("1" (inst - "P!1") (("1" (inst - "ii!1" "ii!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (case-replace "part_set_of(P!1)(x!1)=part_set_of(P!1)(MID)") (("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "part_set_of") (("2" (case-replace "ii_of_x(P!1)(x!1)=ii_of_x(P!1)(MID)") (("2" (hide 2) (("2" (hide -4) (("2" (expand "ii_of_x") (("2" (hide -3) (("2" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)}")) (("2" (case-replace "empty?({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (name-replace "II_LEFT" "choose[below(length(P!1) - 1)] ({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (expand "member") (("1" (flatten) (("1" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("1" (assert) (("1" (inst - "P!1") (("1" (inst - "ii!1" "II_LEFT") (("1" (expand "<=" -2) (("1" (replace -4) (("1" (replace -5) (("1" (expand "/=" -1) (("1" (split -1) (("1" (hide 1) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b")) (("1" (inst - "x!1" "P!1" "ii!1" "II_LEFT") (("1" (assert) (("1" (replace -1) (("1" (hide -1 -2 -3 -4 -5 1) (("1" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= MID AND MID < seq(P!1)(1 + ii)}")) (("1" (case-replace "empty?({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= MID AND MID < seq(P!1)(1 + ii)})") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (name-replace "II_RIGHT" "choose[below(length(P!1) - 1)] ({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= MID AND MID < seq(P!1)(1 + ii)})") (("1" (expand "member") (("1" (flatten) (("1" (expand "<=" -1) (("1" (split) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b" "P" "P!1" "x" "MID" "ii" "ii!1" "jj" "II_RIGHT")) (("1" (assert) nil nil)) nil) ("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "MID")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "ii!1" "II_RIGHT") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (lemma "part_not_in" ("a" "a" "b" "b")) (("2" (inst - "MID") (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "ii!1" "ii!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" (expand "zeroed?") (("2" (skosimp) (("2" (split) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partition type-eq-decl nil integral_def "analysis/") (+ 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/") (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf 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) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf 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) (lower_step_TCC2 subtype-tcc nil riemann_scaf nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (image const-decl "set[R]" function_image nil) (f!1 skolem-const-decl "bounded" riemann_scaf nil) (part_set_of const-decl "(nonempty?[real])" riemann_scaf nil) (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil) (MID skolem-const-decl "real" riemann_scaf nil) (setof type-eq-decl nil defined_types nil) (below_bounded const-decl "bool" bounded_reals "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (greatest_lower_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (inf_set type-eq-decl nil bounded_reals "reals/") (open_interval type-eq-decl nil intervals_real "reals/") (part_not_in formula-decl nil integral_def "analysis/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (ii_of_x const-decl "below(length(P) - 1)" riemann_scaf nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (parts_disjoint formula-decl nil integral_def "analysis/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (choose_member formula-decl nil sets_lemmas nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (step_function_on? const-decl "bool" step_fun_def "analysis/") (step_function? const-decl "bool" step_fun_def "analysis/") (zeroed? const-decl "bool" riemann_scaf nil) (step? const-decl "bool" riemann_scaf nil)) nil)) (upper_step_TCC1 0 (upper_step_TCC1-1 nil 3450936937 ("" (skosimp) (("" (typepred "part_set_of(P!1)(x!1)") (("1" (split) (("1" (expand "nonempty?") (("1" (expand "image") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp) (("1" (inst - "f!1(x!2)") (("1" (inst 1 "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "f!1") (("2" (expand "zeroed_bounded?") (("2" (flatten) (("2" (expand "above_bounded") (("2" (expand "bounded?") (("2" (skosimp) (("2" (inst + "c!1") (("2" (hide -2) (("2" (expand "image") (("2" (expand "upper_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (inst - "x!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((part_set_of const-decl "(nonempty?[real])" riemann_scaf nil) (partition type-eq-decl nil integral_def "analysis/") (+ 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/") (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf 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) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets 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) (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) (above_bounded const-decl "bool" bounded_reals "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nnreal type-eq-decl nil real_types nil) (bounded? const-decl "bool" sup_norm "measure_integration/") (empty? const-decl "bool" sets nil) (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil) (x!1 skolem-const-decl "real" riemann_scaf nil) (x!2 skolem-const-decl "real" riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (member const-decl "bool" sets nil) (image const-decl "set[R]" function_image nil)) nil)) (upper_step_TCC2 0 (upper_step_TCC2-1 nil 3450936937 ("" (skosimp) (("" (expand "step?") (("" (split) (("1" (expand "step_function?") (("1" (inst + "P!1") (("1" (expand "step_function_on?") (("1" (skosimp) (("1" (name "MID" "(seq(P!1)(ii!1)+ seq(P!1)(1 + ii!1))/2") (("1" (lemma "upper_step_TCC1" ("P" "P!1" "f" "f!1" "x" "MID")) (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (inst + "sup[real] (image[real, real](f!1, part_set_of(P!1)(MID)))") (("1" (skosimp) (("1" (typepred "x!1") (("1" (lift-if 1) (("1" (prop) (("1" (skosimp) (("1" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("1" (assert) (("1" (inst - "P!1") (("1" (inst - "ii!1" "ii!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (expand "part_set_of") (("2" (case-replace "ii_of_x(P!1)(x!1)=ii_of_x(P!1)(MID)") (("2" (hide -3 -4 2) (("2" (expand "ii_of_x") (("2" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)}")) (("2" (case-replace "empty?({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (expand "empty?") (("1" (inst - "ii!1") (("1" (assert) nil nil)) nil)) nil) ("2" (replace 1 -1) (("2" (name-replace "II_LEFT" "choose[below(length(P!1) - 1)] ({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= x!1 AND x!1 < seq(P!1)(1 + ii)})") (("1" (expand "member") (("1" (flatten) (("1" (expand "<=" -1) (("1" (split) (("1" (hide 1) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b" "P" "P!1" "ii" "ii!1" "jj" "II_LEFT" "x" "x!1")) (("1" (assert) (("1" (replace -1) (("1" (hide -1 -2 -3) (("1" (lemma "choose_member[below(length(P!1) - 1)]" ("a" "{ii: below(length(P!1) - 1) | seq(P!1)(ii) <= MID AND MID < seq(P!1)(1 + ii)}")) (("1" (case-replace "empty?({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= MID AND MID < seq(P!1)(1 + ii)})") (("1" (expand "empty?") (("1" (inst - "ii!1") (("1" (typepred "P!1") (("1" (inst - "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1 -1) (("2" (name-replace "II_RIGHT" "choose[below(length(P!1) - 1)] ({ii: below(length(P!1) - 1) | seq(P!1)(ii) <= MID AND MID < seq(P!1)(1 + ii)})") (("1" (hide 1) (("1" (expand "member") (("1" (flatten) (("1" (expand "<=" -1) (("1" (split) (("1" (lemma "parts_disjoint" ("a" "a" "b" "b" "P" "P!1" "x" "MID" "ii" "II_RIGHT" "jj" "ii!1")) (("1" (typepred "P!1") (("1" (inst - "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "MID")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "ii!1" "II_RIGHT") (("2" (typepred "P!1") (("2" (inst - "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "x!1")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "ii!1" "II_LEFT") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 1) (("2" (skosimp) (("2" (lemma "part_not_in" ("a" "a" "b" "b" "x" "MID")) (("2" (assert) (("2" (inst - "P!1") (("2" (inst - "ii!1" "ii!2") (("2" (assert) (("2" (typepred "P!1") (("2" (inst - "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 1) (("3" (typepred "P!1") (("3" (inst - "ii!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "zeroed?") (("2" (skosimp) (("2" (split) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((step? const-decl "bool" riemann_scaf nil) (zeroed? const-decl "bool" riemann_scaf nil) (step_function? const-decl "bool" step_fun_def "analysis/") (step_function_on? const-decl "bool" step_fun_def "analysis/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (ii_of_x const-decl "below(length(P) - 1)" riemann_scaf nil) (empty? const-decl "bool" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (parts_disjoint formula-decl nil integral_def "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (choose_member formula-decl nil sets_lemmas nil) (part_not_in formula-decl nil integral_def "analysis/") (open_interval type-eq-decl nil intervals_real "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (sup_set type-eq-decl nil bounded_reals "reals/") (pred type-eq-decl nil defined_types nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (setof type-eq-decl nil defined_types nil) (MID skolem-const-decl "real" riemann_scaf nil) (P!1 skolem-const-decl "partition[real](a, b)" riemann_scaf nil) (part_set_of const-decl "(nonempty?[real])" riemann_scaf nil) (f!1 skolem-const-decl "bounded" riemann_scaf nil) (image const-decl "set[R]" function_image nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (bounded nonempty-type-eq-decl nil riemann_scaf nil) (zeroed_bounded? const-decl "bool" riemann_scaf nil) (upper_step_TCC1 subtype-tcc nil riemann_scaf nil) (partition type-eq-decl nil integral_def "analysis/") (+ 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/") (b formal-const-decl "{x: real | a < x}" riemann_scaf nil) (< const-decl "bool" reals nil) (a formal-const-decl "real" riemann_scaf nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (lower_step_prop 0 (lower_step_prop-1 nil 3450943549 ("" (skosimp) (("" (expand "<=") (("" (skosimp) (("" (expand "lower_step") (("" (lift-if) (("" (assert) (("" (typepred "f!1") (("" (expand "zeroed_bounded?") (("" (flatten) (("" (hide -1) (("" (split) (("1" (expand "zeroed?") (("1" (inst - "x!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (prop) (("2" (lemma "lower_step_TCC2" ("P" "P!1" "f" "f!1" "x" "x!1")) (("2" (replace 1 -1) (("2" (replace 4 -1) (("2" (replace 5 -1) (("2" (replace 2 -1) (("2" (flatten) (("2" (typepred "inf(image(f!1, part_set_of(P!1)(x!1)))") (("2" (name-replace --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.1.1Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26