Quelle  orph-prfs

("real_intervals_aux" real_intervals_aux left_closed_right_open_TCC6 0 (left_closed_right_open_TCC6-1 nil 3475907369 nil ("" (subtype-tcc) nil nil) nil nil nil nil nil nil))("real_intervals_aux" real_intervals_aux left_closed_right_open_TCC5 0 (left_closed_right_open_TCC5-1 nil 3475907369 nil ("" (subtype-tcc) nil nil) nil nil nil nil nil nil))("real_intervals_aux" real_intervals_aux left_closed_right_open_TCC4 0 (left_closed_right_open_TCC4-1 nil 3475907369 nil ("" (subtype-tcc) nil nil) nil nil nil nil nil nil))("real_intervals_aux" real_intervals_aux left_closed_right_open_TCC3 0 (left_closed_right_open_TCC3-1 nil 3475907369 nil ("" (subtype-tcc) nil nil) nil nil nil nil nil nil))("real_intervals_aux" real_intervals_aux left_closed_right_open_TCC2 0 (left_closed_right_open_TCC2-1 nil 3475907369 3475908174 ("" (skosimp) (("" (expand "left_closed_right_open_interval?") (("" (name "XX" "{x:real | inf[real](Z!1) <= x AND x < sup[real](Z!1)}") (("1" (replace -1) (("1" (typepred "Z!1") (("1" (expand "nonempty_interval?") (("1" (flatten) (("1" (case-replace "nonempty?(XX)") (("1" (case-replace "interval?(XX)") (("1" (case-replace "above_bounded(XX)") (("1" (case-replace "below_bounded(XX)") (("1" (assert) (("1" (postpone) nil nil)) nil) ("2" (hide 2) (("2" (expand "below_bounded" 1) (("2" (inst + "inf[real](Z!1)") (("1" (expand "lower_bound" 1) (("1" (skosimp) (("1" (typepred "z!1") (("1" (expand "XX") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "above_bounded" 1) (("2" (inst + "sup[real](Z!1)") (("1" (expand "upper_bound" 1) (("1" (skosimp) (("1" (typepred "z!1") (("1" (expand "XX") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -3) (("2" (expand "interval?") (("2" (skosimp) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (expand "XX") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "Z!1") (("2" (expand "nonempty_interval?") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "Z!1") (("3" (expand "nonempty_interval?") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 639369 22040 t nil))("real_intervals_aux" real_intervals_aux left_closed_right_open_TCC1 0 (left_closed_right_open_TCC1-1 nil 3475907369 3475907527 ("" (subtype-tcc) nil nil) proved ((nonempty? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (above_bounded const-decl "bool" bounded_reals "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (interval? const-decl "bool" real_topology "metric_space/") (nonempty_interval nonempty-type-eq-decl nil real_intervals_aux nil) (nonempty_interval? const-decl "bool" real_intervals_aux 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)) 140 80 t nil))("real_intervals" real_intervals inf_open_TCC1 0 (inf_open_TCC1-1 nil 3452486824 3452486960 ("" (skosimp) (("" (rewrite "metric_open_def" 1 :dir rl) (("" (expand "metric_open?") (("" (skosimp) (("" (split) (("1" (flatten) (("1" (inst + "a!1-x!1") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked ((metric_open_def formula-decl nil metric_space "metric_space/") (set type-eq-decl nil sets nil) (< const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_open? const-decl "bool" metric_space_def "metric_space/")) 35179 230 t nil))("real_intervals" real_intervals open_inf_TCC1 0 (open_inf_TCC1-1 nil 3452486824 3452486918 ("" (skosimp) (("" (rewrite "metric_open_def" 1 :dir rl) (("" (expand "metric_open?") (("" (skosimp) (("" (split) (("1" (flatten) (("1" (inst + "x!1-a!1") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((metric_open_def formula-decl nil metric_space "metric_space/") (set type-eq-decl nil sets nil) (< const-decl "bool" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_open? const-decl "bool" metric_space_def "metric_space/")) 83666 350 t nil))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measurable_intervals 0 (lebesgue_measurable_intervals-1 nil 3452409158 3475917609 ("" (skosimp) (("" (typepred "E!1") (("" (expand "mu_fin?") (("" (expand "mu") (("" (name "MU_E" "lebesgue_measure(E!1)") (("" (replace -1) (("" (expand "lebesgue_measure" -1) (("" (expand "induced_measure") (("" (expand "restrict") (("" (expand "lebesgue_outer_measure") (("" (expand "x_inf") (("" (lift-if -1) (("" (assert) (("" (prop) (("" (skosimp) (("" (typepred "glb({z_1: real |
              EXISTS (x:extended_nnreal):
                (EXISTS I:
                   x_le(x_sum(x_length o I), x) AND
                    subset?[real](E!1, IUnion(I)))
                 AND x`1 AND x`2 = z_1})") (("1" (name-replace "GLB" "glb({z_1: real |
              EXISTS (x:extended_nnreal):
                (EXISTS I:
                   x_le(x_sum(x_length o I), x) AND
                    subset?[real](E!1, IUnion(I)))
                 AND x`1 AND x`2 = z_1})") (("1" (replace -3 * rl) (("1" (assert) (("1" (hide -3 -2 -5) (("1" (expand "greatest_lower_bound?") (("1" (expand "lower_bound?") (("1" (flatten) (("1" (inst -2 "GLB+r!1/2") (("1" (assert) (("1" (skosimp) (("1" (typepred "s!1") (("1" (skosimp) (("1" (skosimp) (("1" (case "x!2`2<r!1 / 2 + GLB") (("1" (hide -5 1) (("1" (inst + "I!1") (("1" (assert) (("1" (case "x_le(lebesgue_measure(IUnion(I!1)), x_sum(lebesgue_measure o I!1))") (("1" (lemma "x_sum_le" ("S" "lebesgue_measure o I!1" "T" "x_length o I!1")) (("1" (split) (("1" (expand "x_le" (-1 -2 -4)) (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma "increasing_IUnion" ("A" "I!1")) (("1" (skosimp) (("1" (case "forall n: IUnion(n, I!1)=B!1(n)") (("1" (case "forall n: measurable_set?(B!1(n))") (("1" (replace -6 1) (("1" (case-replace "(LAMBDA n: lebesgue_measure(IUnion(n, I!1))`2)=LAMBDA n: lebesgue_measure(B!1(n))`2") (("1" (hide -1) (("1" (lemma "m_increasing_convergence" ("E" "B!1")) (("1" (assert) (("1" (expand "x_converges?" -1) (("1" (prop) (("1" (name-replace "LIMIT" "lebesgue_measure(IUnion(B!1))`2") (("1" (expand "o") (("1" (name-replace "FF" "(LAMBDA (i:nat): lebesgue_measure(B!1(i))`2)") (("1" (hide-all-but (-2 -3 1)) (("1" (lemma "convergence_sequences.limit_lemma" ("v" "FF")) (("1" (replace -3 * rl) (("1" (hide -2 -3) (("1" (rewrite "metric_convergence_def") (("1" (expand "convergence") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst - "r!2") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (expand "ball") (("1" (lemma "abs_neg" ("x" "LIMIT - FF(i!1)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -4 "i!1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("1" (inst -2 "x!3") (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (inst - "n!1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst - "n!1") (("3" (inst - "n!1") (("3" (expand "measurable_set?") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst - "n!1") (("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (inst - "n!1") (("4" (inst - "n!1") (("4" (expand "measurable_set?") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -4 1)) (("2" (induct "n") (("1" (typepred "I!1(0)") (("1" (lemma "bounded_open_interval_is_measurable") (("1" (inst - "I!1(0)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "j!1") (("2" (replace -3) (("2" (rewrite "measurable_union") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (induct "n") (("1" (expand "IUnion") (("1" (apply-extensionality :hide? t) (("1" (expand "image") (("1" (expand "Union") (("1" (case-replace "B!1(0)(x!3)") (("1" (inst + "I!1(0)") (("1" (assert) nil nil) ("2" (inst + "0") nil nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (typepred "x!4") (("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "j!1") (("2" (replace -3) (("2" (hide -3 -2) (("2" (apply-extensionality :hide? t) (("2" (expand "union") (("2" (expand "member") (("2" (case-replace "IUnion(1 + j!1, I!1)(x!3)") (("1" (expand "IUnion") (("1" (expand "image") (("1" (flatten) (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (skosimp) (("1" (typepred "x!4") (("1" (expand "<=" -1) (("1" (split) (("1" (replace -4 1 rl) (("1" (assert) (("1" (inst + "a!1") (("1" (inst + "x!4") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (split -1) (("1" (replace -2 -1 rl) (("1" (assert) (("1" (skosimp) (("1" (typepred "a!1") (("1" (skosimp) (("1" (typepred "x!4") (("1" (inst + "a!1") (("1" (inst + "x!4") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "I!1(1+j!1)") (("2" (inst + "1+j!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) ("2" (hide-all-but (-1 -2 -3 -5 1)) (("2" (skosimp) (("2" (expand "o ") (("2" (expand "lebesgue_measure") (("2" (expand "induced_measure") (("2" (expand "restrict") (("2" (lemma "lebesgue_outer_measure_le_length" ("b" "I!1(i!1)")) (("1" (propax) nil nil) ("2" (typepred "I!1(i!1)") (("2" (expand "bounded_open_interval?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "lebesgue_measure" 1) (("2" (expand "induced_measure") (("2" (expand "restrict") (("2" (expand "o" 1) (("2" (typepred "lebesgue_outer_measure") (("2" (expand "outer_measure?") (("2" (flatten) (("2" (expand "om_countably_subadditive?") (("2" (inst -3 "I!1") (("2" (expand "o ") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "I!1(x1!1)") (("3" (lemma "bounded_open_interval_is_measurable") (("3" (inst - "I!1(x1!1)") (("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma "measurable_IUnion" ("SS" "I!1")) (("4" (expand "measurable_set?") (("4" (propax) 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) ("2" (hide 2) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!1`2") (("1" (expand "member") (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (inst + "0") (("2" (expand "lower_bound?") (("2" (skosimp) (("2" (typepred "s!1") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (skosimp) (("3" (typepred "I!1(x1!1)") (("3" (expand "bounded_open_interval?") (("3" (expand "bounded_interval?") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((minus_odd_is_odd application-judgement "odd_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (restrict const-decl "R" restrict nil) (empty? const-decl "bool" sets nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (measurable_IUnion application-judgement "measurable_set[T, S]" real_lebesgue nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) nil nil nil nil nil (lebesgue_outer_measure_le_length formula-decl nil real_lebesgue nil) nil nil (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (union const-decl "set" sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (TRUE const-decl "bool" booleans nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (<= const-decl "bool" reals nil) (Union const-decl "set" sets nil) nil nil nil (limit_lemma formula-decl nil convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (minus_real_is_real application-judgement "real" reals nil) nil (ball const-decl "set[T]" metric_space_def "metric_space/") (metric_converges_to const-decl "bool" 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) (- const-decl "[numfield -> numfield]" number_fields nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (bounded_open_interval_is_measurable judgement-tcc nil real_lebesgue nil) nil (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) nil 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 "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (nonempty? const-decl "bool" sets nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (glb const-decl "{x | greatest_lower_bound?(x, SB)}" bounded_real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans 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) nil nil (sequence type-eq-decl nil sequences nil) nil nil nil nil (O const-decl "T3" function_props nil) (x_length const-decl "extended_nnreal" real_lebesgue nil) (subset? const-decl "bool" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (lebesgue_outer_measure const-decl "outer_measure" real_lebesgue nil) nil 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) (set type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) nil nil (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) nil nil (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) nil nil nil (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) nil) 2500 1600 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measurable_intervals_TCC3 0 (lebesgue_measurable_intervals_TCC3-1 nil 3452412690 3475908932 ("" (skosimp*) (("" (typepred "E!1") (("" (expand "measurable_set?") (("" (assert) nil nil)) nil)) nil)) nil) proved ((mu_fin? const-decl "bool" measure_props "measure_integration_fnd/") (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration_fnd/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration_fnd/") (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types 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) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (measurable_IUnion application-judgement "measurable_set[T, S]" real_lebesgue nil)) 149 150 t nil))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measurable_intervals_TCC2 0 (lebesgue_measurable_intervals_TCC2-1 nil 3452409043 3475908932 ("" (skosimp) (("" (typepred "E!1") (("" (assert) (("" (expand "measurable_set?") (("" (lemma "measurable_IUnion" ("SS" "I!1")) (("" (expand "measurable_set?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((mu_fin? const-decl "bool" measure_props "measure_integration_fnd/") (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration_fnd/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration_fnd/") (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types 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) (measurable_IUnion judgement-tcc nil measure_space_def "measure_integration_fnd/") (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) (sequence type-eq-decl nil sequences nil) (bounded_open_interval? const-decl "bool" real_topology "metric_space/") (bounded_open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (measurable_IUnion application-judgement "measurable_set[T, S]" real_lebesgue nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil)) 245 150 t nil))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measurable_intervals_TCC1 0 (lebesgue_measurable_intervals_TCC1-1 nil 3452344049 3475908931 ("" (skosimp) (("" (lemma "measurable_IUnion" ("SS" "I!1")) (("" (expand "measurable_set?") (("" (hide -1 -3) (("" (case "FORALL (n):
        lebesgue_measurable(IUnion[real](n, I!1))") (("1" (skosimp) (("1" (inst - "n!1") (("1" (assert) (("1" (expand "mu_fin?") (("1" (lemma "m_monotone" ("a" "IUnion[real](n!1, I!1)" "b" "IUnion(I!1)")) (("1" (split) (("1" (expand "x_le") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "IUnion") (("2" (expand "image") (("2" (expand "Union") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (typepred "a!1") (("2" (skosimp) (("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (induct "n") (("1" (rewrite "IUnion_0_def") (("1" (assert) (("1" (lemma "bounded_open_interval_is_measurable") (("1" (inst - "I!1(0)") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "IUnion_n_def") (("2" (lemma "measurable_union") (("2" (inst - "IUnion(j!1, I!1)" "I!1(1 + j!1)") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types 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) (bounded_open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_open_interval? const-decl "bool" real_topology "metric_space/") (sequence type-eq-decl nil sequences nil) (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration_fnd/") (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (set type-eq-decl nil sets nil) (nat nonempty-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) (measurable_IUnion judgement-tcc nil measure_space_def "measure_integration_fnd/") (measurable_union judgement-tcc nil measure_space_def "measure_integration_fnd/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (I!1 skolem-const-decl "sequence[bounded_open_interval]" real_lebesgue nil) (j!1 skolem-const-decl "nat" real_lebesgue nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (IUnion_n_def formula-decl nil nat_indexed_sets "sets_aux/") (IUnion_0_def formula-decl nil nat_indexed_sets "sets_aux/") (bounded_open_interval_is_measurable judgement-tcc nil real_lebesgue nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (measurable_IUnion application-judgement "measurable_set[T, S]" real_lebesgue nil) (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration_fnd/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (IUnion const-decl "set[T]" indexed_sets nil) (m_monotone formula-decl nil measure_props "measure_integration_fnd/") (image const-decl "set[R]" function_image nil) (subset? const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (Union const-decl "set" sets nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (mu_fin? const-decl "bool" measure_props "measure_integration_fnd/") (IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/")) 600 420 t nil))("real_lebesgue_scaf" real_lebesgue_scaf bounded_open_interval_is_measurable 0 (bounded_open_interval_is_measurable-1 nil 3452345860 3475908931 ("" (skolem + "b!1") (("" (lemma "nonempty_bounded_open_interval_prop" ("b" "b!1")) (("" (typepred "b!1") (("" (expand "bounded_open_interval?") (("" (expand "bounded_interval?") (("" (flatten) (("" (expand "bounded?") (("" (hide -1 -3) (("" (split) (("1" (rewrite "emptyset_is_empty?") (("1" (replace -1) (("1" (rewrite "measurable_emptyset") nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide -2 -3) (("2" (skosimp) (("2" (replace -2) (("2" (lemma "ball_is_lebesgue_measurable" ("x1" "x!1" "r" "r!1")) (("2" (expand "measurable_set?") (("2" (expand "lebesgue_measurable") (("2" (expand "fullset") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((bounded_open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_open_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (nonempty_bounded_open_interval_prop formula-decl nil real_lebesgue nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (fullset const-decl "set" sets nil) (extend const-decl "R" extend 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) (ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (emptyset_is_compact name-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" real_topology "metric_space/") (finite_emptyset name-judgement "finite_set[nat]" countability "sets_aux/") (outer_negligible_emptyset name-judgement "outer_negligible" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_borel "measure_integration_fnd/") (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (null_emptyset name-judgement "null_set" real_lebesgue nil) (finite_emptyset name-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (finite_emptyset name-judgement "finite_set[posreal]" metric_continuity "metric_space/") (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]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (measurable_emptyset judgement-tcc nil measure_space_def "measure_integration_fnd/") (bounded? const-decl "bool" real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (NOT const-decl "[bool -> bool]" booleans nil)) 271 190 t nil))("real_lebesgue_scaf" real_lebesgue_scaf nonempty_bounded_open_interval_prop 0 (nonempty_bounded_open_interval_prop-1 nil 3452348717 3475908930 ("" (skosimp) (("" (typepred "b!1") (("" (expand "bounded_open_interval?") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (assert) (("" (split) (("1" (expand "nonempty?") (("1" (propax) nil nil)) nil) ("2" (flatten) (("2" (name "SUP" "sup(b!1)") (("1" (name "INF" "inf(b!1)") (("1" (typepred "inf(b!1)") (("1" (typepred "sup(b!1)") (("1" (replace -3) (("1" (replace -4) (("1" (hide -3 -4 -5 -6) (("1" (expand "least_upper_bound") (("1" (expand "greatest_lower_bound") (("1" (flatten) (("1" (expand "lower_bound") (("1" (expand "upper_bound") (("1" (case "FORALL (z: (b!1)): z < SUP") (("1" (case "FORALL (z: (b!1)): INF<z") (("1" (case "SUP>INF") (("1" (inst + "(SUP+INF)/2" "(SUP-INF)/2") (("1" (apply-extensionality :hide? t) (("1" (case-replace "b!1(x!1)") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (hide-all-but (-1 -2 -3 -4 1)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "INF<x!1& x!1<SUP") (("1" (hide -2) (("1" (flatten) (("1" (inst -7 "x!1") (("1" (assert) (("1" (skosimp) (("1" (inst -8 "x!1") (("1" (assert) (("1" (skosimp) (("1" (expand "interval?") (("1" (inst -8 "z!2" "z!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (assert) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -4 -7)) (("2" (skosimp) (("2" (inst-cp - "z!1") (("2" (expand "<=" -2) (("2" (split -2) (("1" (propax) nil nil) ("2" (expand "metric_open?") (("2" (inst -3 "z!1") (("2" (assert) (("2" (skosimp) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "ball") (("2" (inst -3 "z!1-r!1/2") (("2" (assert) (("2" (expand "abs") (("2" (inst - "z!1-r!1/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "z!1") (("2" (inst-cp - "z!1") (("2" (expand "<=" -3) (("2" (split -3) (("1" (propax) nil nil) ("2" (hide 1 2 -5 -6) (("2" (expand "metric_open?") (("2" (inst -6 "z!1") (("2" (assert) (("2" (skosimp) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "ball") (("2" (inst -6 "z!1+r!1/2") (("2" (assert) (("2" (rewrite "abs_mult") (("2" (rewrite "abs_neg") (("2" (expand "abs") (("2" (inst - "r!1/2+z!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) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((bounded_open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_open_interval? const-decl "bool" real_topology "metric_space/") (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) (bounded_interval? const-decl "bool" real_topology "metric_space/") (nonempty? const-decl "bool" sets nil) (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (<= const-decl "bool" reals nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (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) (= const-decl "[T, T -> boolean]" equalities nil) (lower_bound const-decl "bool" bound_defs "reals/") (< const-decl "bool" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (r!1 skolem-const-decl "posreal" real_lebesgue nil) (z!1 skolem-const-decl "(b!1)" real_lebesgue nil) (subset? const-decl "bool" sets nil) (metric_open? const-decl "bool" metric_space_def "metric_space/") (> const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (real_plus_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) (interval? const-decl "bool" real_topology "metric_space/") (x!1 skolem-const-decl "real" real_lebesgue nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (INF skolem-const-decl "{x | greatest_lower_bound(<=)(x, b!1)}" real_lebesgue nil) (SUP skolem-const-decl "{x | least_upper_bound(<=)(x, b!1)}" real_lebesgue nil) (b!1 skolem-const-decl "bounded_open_interval" real_lebesgue 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 "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_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (abs_mult formula-decl nil real_props nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (z!1 skolem-const-decl "(b!1)" real_lebesgue nil) (r!1 skolem-const-decl "posreal" real_lebesgue nil) (abs_nat formula-decl nil abs_lems "reals/") (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (abs_neg formula-decl nil abs_lems "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (greatest_lower_bound const-decl "bool" bound_defs "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (bounded? const-decl "bool" real_topology "metric_space/") (minus_odd_is_odd application-judgement "odd_int" integers nil)) 1575 1180 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf countable_is_null 0 (countable_is_null-1 nil 3451333235 3475908929 ("" (skosimp) (("" (typepred "x!1") (("" (rewrite "countable_card" -1) (("" (split) (("1" (rewrite "finite_is_null") nil nil) ("2" (expand "is_countably_infinite") (("2" (skosimp) (("2" (typepred "f!1") (("2" (lemma "bijective_inverse_exists[(x!1), nat]" ("f" "f!1")) (("2" (expand "exists1") (("2" (flatten) (("2" (skolem - "g!1") (("2" (lemma "null_IUnion") (("2" (inst - "singleton[real] o g!1") (("1" (case-replace "(IUnion[nat, real](singleton[real] o g!1))=x!1") (("1" (hide -1 2) (("1" (apply-extensionality :hide? t) (("1" (expand "o") (("1" (expand "IUnion") (("1" (expand "singleton") (("1" (case-replace "x!1(x!2)") (("1" (inst + "f!1(x!2)") (("1" (rewrite "comp_inverse_left_alt[(x!1), nat]") nil nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "o") (("2" (skosimp) (("2" (lemma "singleton_is_null" ("x" "g!1(x1!1)")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (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) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_is_null judgement-tcc nil real_lebesgue nil) (bijective_inverse_exists formula-decl nil function_inverse_def nil) (null_IUnion judgement-tcc nil measure_theory "measure_integration_fnd/") (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_fnd/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue 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_fnd/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (singleton_is_null application-judgement "null_set" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_null judgement-tcc nil real_lebesgue nil) (IUnion const-decl "set[T]" indexed_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (inverse? const-decl "bool" function_inverse_def nil) (comp_inverse_left_alt formula-decl nil function_inverse_def nil) (x!2 skolem-const-decl "real" real_lebesgue nil) (null_set nonempty-type-eq-decl nil measure_theory "measure_integration_fnd/") (sequence type-eq-decl nil sequences nil) (g!1 skolem-const-decl "[nat -> ((x!1))]" real_lebesgue nil) (x!1 skolem-const-decl "countable_set[real]" real_lebesgue nil) (singleton const-decl "(singleton?)" sets nil) (O const-decl "T3" function_props nil) (singleton? const-decl "bool" sets nil) (null_set? const-decl "bool" measure_theory "measure_integration_fnd/") (exists1 const-decl "bool" exists1 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) (bijective? const-decl "bool" functions nil) (is_countably_infinite const-decl "bool" countability "sets_aux/") (countable_card formula-decl nil countable_props "sets_aux/")) 561 410 t nil))("real_lebesgue_scaf" real_lebesgue_scaf finite_is_null 0 (finite_is_null-1 nil 3451279403 3475908928 ("" (case "forall (X:finite_set[real],n:nat): card[real](X) <= n => null_set?[real, lebesgue_measurable, lebesgue_measure](X)") (("1" (skosimp) (("1" (inst - "x!1" "card(x!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (expand "<=") (("1" (split) (("1" (assert) nil nil) ("2" (rewrite "card_is_0") (("2" (replace -1) (("2" (expand "null_set?") (("2" (assert) (("2" (rewrite "measurable_emptyset") (("2" (expand "mu_fin?") (("2" (expand "mu") (("2" (typepred "lebesgue_measure") (("2" (expand "complete_sigma_finite?") (("2" (expand "measure?") (("2" (flatten) (("2" (expand "measure_empty?") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "<=" -2) (("2" (split) (("1" (inst - "X!1") (("1" (assert) nil nil)) nil) ("2" (lemma "nonempty_card[real]" ("S" "X!1")) (("2" (assert) (("2" (lemma "choose_rest[real]" ("a" "X!1")) (("2" (split -1) (("1" (rewrite "add_as_union") (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (inst - "rest[real](X!1)") (("1" (rewrite "card_rest") (("1" (replace -2) (("1" (assert) (("1" (lemma "singleton_is_null" ("x" "choose[real](X!1)")) (("1" (lemma "null_union" ("N1" "rest[real](X!1)" "N2" "singleton[real](choose[real](X!1))")) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) 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) proved ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (singleton_is_null judgement-tcc nil real_lebesgue nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (null_set nonempty-type-eq-decl nil measure_theory "measure_integration_fnd/") (null_union judgement-tcc nil measure_theory "measure_integration_fnd/") (int_minus_int_is_int application-judgement "int" integers nil) (card_rest formula-decl nil finite_sets nil) (finite_union application-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (nonempty_finite_union2 application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (finite_rest application-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_null application-judgement "null_set" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (add_as_union formula-decl nil sets_lemmas nil) (rest const-decl "set" sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (choose_rest formula-decl nil sets_lemmas nil) (nonempty_card formula-decl nil finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mu_fin? const-decl "bool" measure_props "measure_integration_fnd/") (NOT const-decl "[bool -> bool]" booleans nil) (measure? const-decl "bool" generalized_measure_def "measure_integration_fnd/") (measure_empty? const-decl "bool" generalized_measure_def "measure_integration_fnd/") (mu const-decl "nnreal" measure_props "measure_integration_fnd/") (measurable_emptyset judgement-tcc nil measure_space_def "measure_integration_fnd/") (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]" bounded_nats "orders/") (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[posreal]" metric_continuity "metric_space/") (finite_emptyset name-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (null_emptyset name-judgement "null_set" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_borel "measure_integration_fnd/") (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (outer_negligible_emptyset name-judgement "outer_negligible" real_lebesgue nil) (finite_emptyset name-judgement "finite_set[nat]" countability "sets_aux/") (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_compact name-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (card_is_0 formula-decl nil finite_sets nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (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_fnd/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue 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_fnd/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (null_set? const-decl "bool" measure_theory "measure_integration_fnd/")) 906 650 t nil))("real_lebesgue_scaf" real_lebesgue_scaf singleton_is_null 0 (singleton_is_null-1 nil 3451279403 3475908927 ("" (skosimp) (("" (expand "null_set?") (("" (rewrite "singleton_is_measurable") (("" (expand "mu") (("" (expand "mu_fin?") (("" (lemma "lebesgue_measure_singleton" ("x" "x!1")) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((singleton_is_measurable application-judgement "measurable_set" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (null_set? const-decl "bool" measure_theory "measure_integration_fnd/") (mu const-decl "nnreal" measure_props "measure_integration_fnd/") (lebesgue_measure_singleton formula-decl nil real_lebesgue nil) (mu_fin? const-decl "bool" measure_props "measure_integration_fnd/") (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) (singleton_is_measurable judgement-tcc nil real_lebesgue nil)) 164 160 t nil))("real_lebesgue_scaf" real_lebesgue_scaf integral_finite 0 (integral_finite-1 nil 3451278609 3475908927 ("" (case "forall (n:nat,X): card(X) <= n => integral(phi(X)) = 0") (("1" (skosimp) (("1" (inst - "card(X!1)" "X!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (expand "<=") (("1" (split) (("1" (assert) nil nil) ("2" (rewrite "card_is_0[real]") (("2" (replace -1) (("2" (case-replace "phi(emptyset[real])=lambda x: 0") (("1" (rewrite "integral_zero") 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" (skosimp*) (("2" (expand "<=" -2) (("2" (split) (("1" (inst - "X!1") (("1" (assert) nil nil)) nil) ("2" (lemma "nonempty_card[real]" ("S" "X!1")) (("2" (assert) (("2" (lemma "choose_rest[real]" ("a" "X!1")) (("2" (split) (("1" (lemma "card_rest[real]" ("S" "X!1")) (("1" (split) (("1" (inst - "rest[real](X!1)") (("1" (assert) (("1" (lemma "integral_singleton" ("x" "choose[real](X!1)")) (("1" (lemma "integral_add" ("f1" "phi(rest[real](X!1))" "f2" "phi(singleton[real](choose[real](X!1)))")) (("1" (expand "+" -1) (("1" (replace -4 1 rl) (("1" (case-replace "(LAMBDA (x: real):
                 phi(rest[real](X!1))(x) +
                  phi(singleton[real](choose[real](X!1)))(x))=phi(add[real](choose[real](X!1), rest[real](X!1)))") (("1" (assert) nil nil) ("2" (hide-all-but (-5 1)) (("2" (apply-extensionality :hide? t) (("2" (lemma "choose_not_member[real]" ("a" "X!1")) (("2" (split) (("1" (expand "phi") (("1" (expand "add") (("1" (expand "member") (("1" (assert) (("1" (case-replace "rest[real](X!1)(x!1)") (("1" (expand "singleton") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "singleton") (("2" (assert) (("2" (case-replace "choose[real](X!1) = x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (lemma "integrable_finite" ("X" "X!1")) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (lemma "integrable_finite" ("X" "X!1")) (("3" (propax) nil nil)) nil)) nil)) nil) proved ((integrable_finite formula-decl nil real_lebesgue nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty_add_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (int_minus_int_is_int application-judgement "int" integers nil) (singleton_is_measurable application-judgement "measurable_set" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (integral_add formula-decl nil integral "measure_integration_fnd/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (choose_not_member formula-decl nil sets_lemmas nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (add const-decl "(nonempty?)" sets nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (integral_singleton formula-decl nil real_lebesgue nil) (rest const-decl "set" sets nil) (finite_rest application-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (card_rest formula-decl nil finite_sets nil) (choose_rest formula-decl nil sets_lemmas nil) (nonempty_card formula-decl nil finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (member const-decl "bool" sets nil) (integral_zero formula-decl nil integral "measure_integration_fnd/") (phi_is_simple application-judgement "simple" real_lebesgue nil) (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]" bounded_nats "orders/") (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[posreal]" metric_continuity "metric_space/") (finite_emptyset name-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (null_emptyset name-judgement "null_set" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_borel "measure_integration_fnd/") (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (outer_negligible_emptyset name-judgement "outer_negligible" real_lebesgue nil) (finite_emptyset name-judgement "finite_set[nat]" countability "sets_aux/") (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_compact name-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (card_is_0 formula-decl nil finite_sets nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (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_fnd/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue 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_fnd/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (integrable? const-decl "bool" integral "measure_integration_fnd/") (integrable nonempty-type-eq-decl nil integral "measure_integration_fnd/") (integral const-decl "real" integral "measure_integration_fnd/") (phi const-decl "nat" measure_space "measure_integration_fnd/")) 4447 1180 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf integral_finite_TCC1 0 (integral_finite_TCC1-1 nil 3451277522 3475908922 ("" (skosimp) (("" (lemma "integrable_finite" ("X" "X!1")) (("" (propax) nil nil)) nil)) nil) proved ((finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets 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) (integrable_finite formula-decl nil real_lebesgue nil)) 178 110 t nil))("real_lebesgue_scaf" real_lebesgue_scaf integral_singleton 0 (integral_singleton-1 nil 3451276554 3475908922 ("" (skosimp) (("" (lemma "integral_phi_closed" ("a" "x!1" "b" "x!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) proved ((<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (integral_phi_closed formula-decl nil real_lebesgue nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (closed_ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (real_minus_real_is_real application-judgement "real" reals nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets 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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_measurable application-judgement "measurable_set" real_lebesgue nil) (closed_is_measurable application-judgement "measurable_set" real_lebesgue nil)) 961 810 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf integral_singleton_TCC1 0 (integral_singleton_TCC1-1 nil 3451276451 3475908921 ("" (skosimp) (("" (lemma "integrable_singleton" ("x" "x!1")) (("" (propax) nil nil)) nil)) nil) proved ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (integrable_singleton formula-decl nil real_lebesgue nil)) 103 110 t nil))("real_lebesgue_scaf" real_lebesgue_scaf integrable_finite 0 (integrable_finite-1 nil 3451277522 3475908920 ("" (case "forall (n:nat,X): card(X) <= n => integrable?(phi(X))") (("1" (skosimp) (("1" (inst - "card(X!1)" "X!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (expand "<=") (("1" (split) (("1" (assert) nil nil) ("2" (rewrite "card_is_0") (("2" (replace -1) (("2" (hide -1) (("2" (case-replace "phi(emptyset[real])=lambda x: 0") (("1" (rewrite "integrable_zero") nil nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "phi") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "<=" -2) (("2" (split) (("1" (inst - "X!1") (("1" (assert) nil nil)) nil) ("2" (lemma "nonempty_card[real]" ("S" "X!1")) (("2" (assert) (("2" (lemma "card_rest[real]" ("S" "X!1")) (("2" (split) (("1" (inst - "rest[real](X!1)") (("1" (lemma "choose_rest[real]" ("a" "X!1")) (("1" (split) (("1" (rewrite "add_as_union") (("1" (lemma "integrable_singleton" ("x" "choose[real](X!1)")) (("1" (replace -2 1 rl) (("1" (assert) (("1" (lemma "integrable_add" ("f1" "phi(rest[real](X!1))" "f2" "phi(singleton[real](choose[real](X!1)))")) (("1" (expand "+" -1) (("1" (case-replace "(LAMBDA (x: real):
                    phi(rest[real](X!1))(x) +
                     phi(singleton[real](choose[real](X!1)))(x))=phi(union[real](rest[real](X!1), singleton[real](choose[real](X!1))))") (("1" (hide -1 -2 2) (("1" (apply-extensionality :hide? t) (("1" (expand "phi") (("1" (expand "union") (("1" (expand "member") (("1" (rewrite "extensionality_postulate" -1 :dir rl) (("1" (inst - "x!1") (("1" (case-replace "rest[real](X!1)(x!1)") (("1" (lemma "choose_not_member[real]" ("a" "X!1")) (("1" (assert) (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (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)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (choose_rest formula-decl nil sets_lemmas nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (add_as_union formula-decl nil sets_lemmas nil) (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_measurable application-judgement "measurable_set" real_lebesgue nil) (nonempty_finite_union2 application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (finite_union application-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (integrable_add judgement-tcc nil integral "measure_integration_fnd/") (integrable nonempty-type-eq-decl nil integral "measure_integration_fnd/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (union const-decl "set" sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (extensionality_postulate formula-decl nil functions nil) (choose_not_member formula-decl nil sets_lemmas nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (int_minus_int_is_int application-judgement "int" integers nil) (integrable_singleton formula-decl nil real_lebesgue nil) (rest const-decl "set" sets nil) (finite_rest application-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (card_rest formula-decl nil finite_sets nil) (nonempty_card formula-decl nil finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (emptyset const-decl "set" sets nil) (phi_is_simple application-judgement "simple" real_lebesgue nil) (integrable_zero formula-decl nil integral "measure_integration_fnd/") (member const-decl "bool" 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]" bounded_nats "orders/") (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[posreal]" metric_continuity "metric_space/") (finite_emptyset name-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (null_emptyset name-judgement "null_set" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_borel "measure_integration_fnd/") (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (outer_negligible_emptyset name-judgement "outer_negligible" real_lebesgue nil) (finite_emptyset name-judgement "finite_set[nat]" countability "sets_aux/") (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_compact name-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (card_is_0 formula-decl nil finite_sets nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (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_fnd/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue 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_fnd/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (integrable? const-decl "bool" integral "measure_integration_fnd/") (phi const-decl "nat" measure_space "measure_integration_fnd/")) 1078 770 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf integrable_singleton 0 (integrable_singleton-1 nil 3451276451 3475908919 ("" (skosimp) (("" (lemma "integrable_phi_closed" ("a" "x!1" "b" "x!1")) (("" (case-replace "closed(x!1,x!1)=singleton[real](x!1)") (("" (hide-all-but 1) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (integrable_phi_closed formula-decl nil real_lebesgue nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (closed_ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets 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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_measurable application-judgement "measurable_set" real_lebesgue nil) (closed_is_measurable application-judgement "measurable_set" real_lebesgue nil)) 920 760 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf finite_is_measurable 0 (finite_is_measurable-1 nil 3451276890 3475908918 ("" (case "forall (n:nat,X:finite_set[real]): card(X) <= n =>
        measurable_set?[real, lebesgue_measurable](X)") (("1" (skosimp) (("1" (inst - "card(x!1)" "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (expand "<=" -1) (("1" (split) (("1" (assert) nil nil) ("2" (rewrite "card_is_0") (("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (rewrite "measurable_emptyset") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "<=" -2) (("2" (split) (("1" (inst - "X!1") (("1" (assert) nil nil)) nil) ("2" (lemma "nonempty_card[real]" ("S" "X!1")) (("2" (assert) (("2" (lemma "choose_rest[real]" ("a" "X!1")) (("2" (split -1) (("1" (rewrite "add_as_union") (("1" (lemma "card_rest[real]") (("1" (inst - "X!1") (("1" (split -1) (("1" (inst - "rest[real](X!1)") (("1" (assert) (("1" (lemma "singleton_is_measurable" ("x" "choose[real](X!1)")) (("1" (replace -3 1 rl) (("1" (rewrite "measurable_union" 1) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) 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) proved ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (card_rest formula-decl nil finite_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (measurable_union judgement-tcc nil measure_space_def "measure_integration_fnd/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration_fnd/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (singleton_is_measurable judgement-tcc nil real_lebesgue nil) (finite_union application-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (nonempty_finite_union2 application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (finite_rest application-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_measurable application-judgement "measurable_set" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (add_as_union formula-decl nil sets_lemmas nil) (rest const-decl "set" sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (choose_rest formula-decl nil sets_lemmas nil) (nonempty_card formula-decl nil finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (measurable_emptyset judgement-tcc nil measure_space_def "measure_integration_fnd/") (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]" bounded_nats "orders/") (finite_emptyset name-judgement "finite_set[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[posreal]" metric_continuity "metric_space/") (finite_emptyset name-judgement "finite_set[real]" measure_space "measure_integration_fnd/") (null_emptyset name-judgement "null_set" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (subset_algebra_emptyset name-judgement "(S)" real_borel "measure_integration_fnd/") (subset_algebra_emptyset name-judgement "(S)" real_lebesgue nil) (outer_negligible_emptyset name-judgement "outer_negligible" real_lebesgue nil) (finite_emptyset name-judgement "finite_set[nat]" countability "sets_aux/") (emptyset_is_clopen name-judgement "clopen[T, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_compact name-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (card_is_0 formula-decl nil finite_sets nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (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_fnd/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/")) 636 490 t nil))("real_lebesgue_scaf" real_lebesgue_scaf closed_is_measurable 0 (closed_is_measurable-1 nil 3432057715 3475908917 ("" (skosimp) (("" (lemma "closed_ball_is_lebesgue_measurable" ("x" "(a!1+b!1)/2" "nnr" "(b!1-a!1)/2")) (("" (case-replace "(closed_ball((a!1 + b!1) / 2, (b!1 - a!1) / 2))=(closed(a!1, b!1))") (("1" (expand "measurable_set?") (("1" (expand "lebesgue_measurable") (("1" (expand "fullset") (("1" (expand "extend") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) proved ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals 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) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (closed_ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue 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_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (fullset const-decl "set" sets nil) (real_plus_real_is_real application-judgement "real" reals nil) (extend const-decl "R" extend nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue 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/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (closed_ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil)) 497 430 t nil))("real_lebesgue_scaf" real_lebesgue_scaf open_is_measurable 0 (open_is_measurable-1 nil 3432057715 3475908917 ("" (skosimp) (("" (lemma "ball_is_lebesgue_measurable" ("x1" "(a!1+b!1)/2" "r" "(b!1-a!1)/2")) (("" (case-replace "(ball[real, (LAMBDA (x, y: real): abs(x - y))]
               ((a!1 + b!1) / 2, (b!1 - a!1) / 2))=(open(a!1, b!1))") (("1" (expand "measurable_set?") (("1" (expand "lebesgue_measurable") (("1" (expand "fullset") (("1" (expand "extend") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) proved ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals 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) (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) (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) (ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue 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_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (fullset const-decl "set" sets nil) (real_plus_real_is_real application-judgement "real" reals nil) (extend const-decl "R" extend nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue 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) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil)) 562 480 t nil))("real_lebesgue_scaf" real_lebesgue_scaf singleton_is_measurable 0 (singleton_is_measurable-1 nil 3432058084 3475908916 ("" (skosimp) (("" (lemma "singleton_is_outer_measurable" ("x" "x!1")) (("" (expand "measurable_set?") (("" (expand "lebesgue_measurable") (("" (expand "fullset") (("" (expand "extend") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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) (singleton_is_outer_measurable judgement-tcc nil real_lebesgue nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space "measure_integration_fnd/")) 206 130 t nil))("real_lebesgue_scaf" real_lebesgue_scaf continuous_is_measurable 0 (continuous_is_measurable-1 nil 3431904760 3475908916 ("" (skolem + "f!1") (("" (typepred "f!1") (("" (lemma "I_is_measurable") (("" (lemma "continuous_is_borel") (("" (inst - "f!1") (("" (lemma "borel_comp_measurable_is_measurable" ("phi" "f!1" "g" "I[real]")) (("1" (expand "o" -1) (("1" (expand "I" -1) (("1" (case-replace "(LAMBDA (x: real): f!1(x))=f!1") (("1" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((continuous type-eq-decl nil continuity_def "topology/") (continuous? const-decl "bool" continuity_def "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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (setofsets type-eq-decl nil sets nil) (setof 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) (continuous_is_borel judgement-tcc nil borel_functions "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (borel_function type-eq-decl nil borel_functions "measure_integration_fnd/") (borel_function? const-decl "bool" borel_functions "measure_integration_fnd/") (I const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration_fnd/") (measurable_function? const-decl "bool" measure_space_def "measure_integration_fnd/") (borel_comp_measurable_is_measurable judgement-tcc nil measure_space "measure_integration_fnd/") (I_is_continuous name-judgement "continuous[real, metric_induced_topology, real, metric_induced_topology]" real_lebesgue nil) (I_is_measurable name-judgement "measurable_function" real_lebesgue nil) (= const-decl "[T, T -> boolean]" equalities nil) (O const-decl "T3" function_props nil) (I_is_measurable judgement-tcc nil real_lebesgue nil)) 209 120 t nil))("real_lebesgue_scaf" real_lebesgue_scaf I_is_measurable 0 (I_is_measurable-1 nil 3431904402 3475908916 ("" (rewrite "measurable_def2") (("" (skosimp) (("" (typepred "i!1") (("" (skosimp) (("" (lemma "ball_is_lebesgue_measurable") (("" (inst - "r!1" "x!1") (("" (expand "lebesgue_measurable") (("" (expand "fullset") (("" (expand "extend") (("" (prop) (("" (case-replace "inverse_image(I[real], i!1)=i!1") (("1" (replace -3 * rl) (("1" (propax) nil nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((fullset const-decl "set" sets nil) (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (I_preserves application-judgement "S" identity_props nil) (member const-decl "bool" sets nil) (I_is_continuous name-judgement "continuous[real, metric_induced_topology, real, metric_induced_topology]" real_lebesgue nil) (inverse_image const-decl "set[D]" function_image nil) (extend const-decl "R" extend nil) (ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue nil) (NOT const-decl "[bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types 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) (I const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (measurable_def2 formula-decl nil measure_space_def "measure_integration_fnd/")) 487 400 t nil))("real_lebesgue_scaf" real_lebesgue_scaf integral_phi_closed 0 (integral_phi_closed-1 nil 3431903760 3475908915 ("" (skosimp) (("" (case "closed_ball((a!1+b!1)/2,(b!1-a!1)/2)=closed(a!1, b!1)") (("1" (lemma "closed_ball_is_lebesgue_measurable") (("1" (inst - "(b!1 - a!1) / 2" "(a!1 + b!1) / 2") (("1" (lemma "lebesgue_measure_closed_ball" ("x" "(a!1 + b!1) / 2" "nnr" "(b!1 - a!1) / 2")) (("1" (lemma "isf_phi" ("E" "closed(a!1, b!1)")) (("1" (rewrite "integral_phi") (("1" (expand "mu") (("1" (replace -4) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "measurable_set?") (("1" (expand "lebesgue_measurable") (("1" (expand "fullset") (("1" (expand "extend") (("1" (replace -3) (("1" (replace -2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (replace -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) proved ((closed const-decl "closed_interval" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (<= const-decl "bool" reals 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) (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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (closed_ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration_fnd/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (mu_fin? const-decl "bool" measure_props "measure_integration_fnd/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration_fnd/") (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (isf_phi judgement-tcc nil isf "measure_integration_fnd/") (mu const-decl "nnreal" measure_props "measure_integration_fnd/") (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (integral_phi formula-decl nil integral "measure_integration_fnd/") (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (lebesgue_measure_closed_ball formula-decl nil real_lebesgue nil) (closed_ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue 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)) 1005 760 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf integral_phi_closed_TCC1 0 (integral_phi_closed_TCC1-1 nil 3431902438 3475908914 ("" (lemma "integrable_phi_closed") (("" (propax) nil nil)) nil) proved ((integrable_phi_closed formula-decl nil real_lebesgue nil)) 45 50 t nil))("real_lebesgue_scaf" real_lebesgue_scaf integral_phi_open 0 (integral_phi_open-1 nil 3431903307 3475908914 ("" (skosimp) (("" (case "ball((a!1 + b!1) / 2, (b!1 - a!1) / 2) = open(a!1, b!1)") (("1" (lemma "ball_is_lebesgue_measurable") (("1" (inst - "(b!1 - a!1) / 2" "(a!1 + b!1) / 2") (("1" (lemma "lebesgue_measure_ball" ("x" "(a!1 + b!1) / 2" "r" "(b!1 - a!1) / 2")) (("1" (lemma "isf_phi" ("E" "open(a!1, b!1)")) (("1" (rewrite "integral_phi") (("1" (expand "mu") (("1" (replace -4) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "measurable_set?") (("1" (expand "lebesgue_measurable") (("1" (expand "fullset") (("1" (expand "extend") (("1" (assert) (("1" (replace -3) (("1" (assert) (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (replace -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) proved ((open const-decl "open_interval" real_topology "metric_space/") (open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (< const-decl "bool" reals 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) (ball const-decl "set[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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (real_minus_real_is_real application-judgement "real" reals nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration_fnd/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (mu_fin? const-decl "bool" measure_props "measure_integration_fnd/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration_fnd/") (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (isf_phi judgement-tcc nil isf "measure_integration_fnd/") (mu const-decl "nnreal" measure_props "measure_integration_fnd/") (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (integral_phi formula-decl nil integral "measure_integration_fnd/") (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (lebesgue_measure_ball formula-decl nil real_lebesgue nil) (ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) 990 820 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf integral_phi_open_TCC1 0 (integral_phi_open_TCC1-1 nil 3431902438 3475908912 ("" (lemma "integrable_phi_open") (("" (propax) nil nil)) nil) proved ((integrable_phi_open formula-decl nil real_lebesgue nil)) 46 50 t nil))("real_lebesgue_scaf" real_lebesgue_scaf integrable_phi_closed 0 (integrable_phi_closed-1 nil 3431902944 3475908912 ("" (skosimp) (("" (case "closed_ball((a!1+b!1)/2,(b!1-a!1)/2)=closed(a!1, b!1)") (("1" (lemma "closed_ball_is_lebesgue_measurable") (("1" (inst - "(b!1 - a!1) / 2" "(a!1 + b!1) / 2") (("1" (lemma "phi_is_simple" ("X" "closed(a!1, b!1)")) (("1" (rewrite "isf_is_integrable") (("1" (hide 2) (("1" (expand "isf?") (("1" (case-replace "nonzero_set?(phi[real, lebesgue_measurable]
                               (closed(a!1, b!1)))=closed(a!1, b!1)") (("1" (hide -1) (("1" (expand "mu_fin?") (("1" (lemma "lebesgue_measure_closed_ball" ("x" "(a!1 + b!1) / 2" "nnr" "(b!1 - a!1) / 2")) (("1" (replace -4) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "lebesgue_measurable") (("2" (expand "fullset") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) proved ((closed const-decl "closed_interval" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (<= const-decl "bool" reals 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) (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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (closed_ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (isf_is_integrable judgement-tcc nil integral "measure_integration_fnd/") (isf? const-decl "bool" isf "measure_integration_fnd/") (isf nonempty-type-eq-decl nil isf "measure_integration_fnd/") (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_fnd/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration_fnd/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (real_plus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lebesgue_measure_closed_ball formula-decl nil real_lebesgue nil) (real_times_real_is_real application-judgement "real" reals nil) (mu_fin? const-decl "bool" measure_props "measure_integration_fnd/") (nonzero_set? const-decl "set[T]" isf "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (phi_is_simple judgement-tcc nil measure_space "measure_integration_fnd/") (closed_ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue nil)) 1216 890 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf integrable_phi_open 0 (integrable_phi_open-1 nil 3431902616 3475908911 ("" (skosimp) (("" (rewrite "isf_is_integrable") (("" (hide 2) (("" (expand "isf?") (("" (rewrite "phi_is_simple") (("1" (case-replace "nonzero_set?(phi[real, lebesgue_measurable](open(a!1, b!1)))=open(a!1,b!1)") (("1" (hide -1) (("1" (expand "mu_fin?") (("1" (lemma "lebesgue_measure_ball" ("x" "(a!1 + b!1) / 2" "r" "(b!1 - a!1) / 2")) (("1" (case-replace "ball((a!1 + b!1) / 2, (b!1 - a!1) / 2)=open(a!1, b!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 2) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "lebesgue_measurable") (("2" (expand "fullset") (("2" (expand "extend") (("2" (lemma "ball_is_lebesgue_measurable" ("x1" "(b!1+a!1)/2" "r" "(b!1-a!1)/2")) (("2" (case-replace "(ball[real, (LAMBDA (x, y: real): abs(x - y))]
               ((b!1 + a!1) / 2, (b!1 - a!1) / 2))=open(a!1, b!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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((isf_is_integrable judgement-tcc nil integral "measure_integration_fnd/") (isf? const-decl "bool" isf "measure_integration_fnd/") (isf nonempty-type-eq-decl nil isf "measure_integration_fnd/") (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_fnd/") (< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (open const-decl "open_interval" real_topology "metric_space/") (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) (bool nonempty-type-eq-decl nil booleans nil) (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_fnd/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue 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_fnd/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (fullset const-decl "set" sets nil) (ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue nil) (extend const-decl "R" extend nil) (nonzero_set? const-decl "set[T]" isf "measure_integration_fnd/") (mu_fin? const-decl "bool" measure_props "measure_integration_fnd/") (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (lebesgue_measure_ball formula-decl nil real_lebesgue nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (phi_is_simple judgement-tcc nil measure_space "measure_integration_fnd/")) 1626 1240 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measure_closed_ball 0 (lebesgue_measure_closed_ball-1 nil 3421701956 3475908909 ("" (skosimp) (("" (typepred "nnr!1") (("" (expand ">=") (("" (expand "<=") (("" (split) (("1" (lemma "singleton_is_outer_measurable" ("x" "x!1-nnr!1")) (("1" (lemma "singleton_is_outer_measurable" ("x" "x!1+nnr!1")) (("1" (lemma "ball_is_lebesgue_measurable") (("1" (inst - "nnr!1" "x!1") (("1" (lemma "lebesgue_measure_singleton" ("x" "x!1-nnr!1")) (("1" (lemma "lebesgue_measure_singleton" ("x" "x!1+nnr!1")) (("1" (lemma "lebesgue_measure_ball" ("x" "x!1" "r" "nnr!1")) (("1" (lemma "m_disjoint_union" ("a" "singleton[real](x!1 - nnr!1)" "b" "singleton[real](x!1 + nnr!1)")) (("1" (split -1) (("1" (replace -3) (("1" (replace -4) (("1" (lemma "measurable_union[real, lebesgue_measurable]" ("a" "singleton[real](x!1 - nnr!1)" "b" "singleton[real](x!1 + nnr!1)")) (("1" (expand "x_add") (("1" (lemma "m_disjoint_union" ("a" "ball[real, (LAMBDA (x, y: real): abs(x - y))](x!1, nnr!1)" "b" "union[real]
                          (singleton[real](x!1 - nnr!1),
                           singleton[real](x!1 + nnr!1))")) (("1" (split -1) (("1" (case-replace "union(ball
                                      [real,
                                       (LAMBDA (x, y: real): abs(x - y))]
                                      (x!1, nnr!1),
                                  union[real]
                                      (singleton[real](x!1 - nnr!1),
                                       singleton[real](x!1 + nnr!1)))=closed_ball(x!1, nnr!1)") (("1" (hide -1) (("1" (replace -4) (("1" (hide-all-but (-1 -3 1)) (("1" (expand "x_add") (("1" (expand "x_eq") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-9 1)) (("2" (grind) nil nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil) ("3" (expand "measurable_set?") (("3" (expand "lebesgue_measurable") (("3" (expand "fullset") (("3" (expand "extend") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (expand "lebesgue_measurable") (("2" (expand "fullset") (("2" (expand "extend") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-7 1)) (("2" (expand "singleton") (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (expand "lebesgue_measurable") (("2" (expand "fullset") (("2" (expand "extend") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "measurable_set?") (("3" (expand "lebesgue_measurable") (("3" (expand "fullset") (("3" (expand "extend") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (hide -1) (("2" (lemma "lebesgue_measure_singleton" ("x" "x!1")) (("2" (case-replace "closed_ball(x!1, 0)=singleton[real](x!1)") (("1" (expand "singleton") (("1" (propax) 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)) nil)) nil)) nil) proved ((nnreal type-eq-decl nil real_types 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) (<= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (singleton_is_outer_measurable judgement-tcc nil real_lebesgue nil) (real_minus_real_is_real application-judgement "real" reals nil) (ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue nil) (lebesgue_measure_singleton formula-decl nil real_lebesgue nil) (lebesgue_measure_ball formula-decl nil real_lebesgue nil) (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (fullset const-decl "set" sets nil) (extend const-decl "R" extend nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets 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) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (TRUE const-decl "bool" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonempty_union2 application-judgement "(nonempty?)" bounded_nats "orders/") (closed_ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (= const-decl "[T, T -> boolean]" equalities 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/") (outer_measurable_intersection application-judgement "outer_measurable" real_lebesgue nil) (finite_intersection1 application-judgement "finite_set[T]" sigma_countable "sigma_set/") (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (union const-decl "set" sets nil) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (union_is_closed application-judgement "closed[real, (metric_induced_topology)]" real_topology "metric_space/") (union_is_compact application-judgement "compact[real, (metric_induced_topology)]" real_topology "metric_space/") (outer_measurable_union application-judgement "outer_measurable" real_lebesgue nil) (finite_union application-judgement "finite_set[T]" sigma_countable "sigma_set/") (nonempty_finite_union1 application-judgement "non_empty_finite_set[T]" sigma_countable "sigma_set/") (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (measurable_union judgement-tcc nil measure_space_def "measure_integration_fnd/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration_fnd/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration_fnd/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration_fnd/") (measurable_set? const-decl "bool" measure_space_def "measure_integration_fnd/") (set type-eq-decl nil sets nil) (m_disjoint_union formula-decl nil measure_props "measure_integration_fnd/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" sigma_countable "sigma_set/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnr!1 skolem-const-decl "nnreal" real_lebesgue nil) (> const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil)) 2197 1610 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measure_closed_ball_TCC1 0 (lebesgue_measure_closed_ball_TCC1-1 nil 3431866829 3475908907 ("" (subtype-tcc) nil nil) proved ((lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (fullset const-decl "set" sets nil) (extend const-decl "R" extend nil) (closed_ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil)) 208 210 nil nil))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measure_ball 0 (lebesgue_measure_ball-1 nil 3421695631 3475908907 ("" (skosimp) (("" (lemma "lebesgue_outer_measure_bounded_interval" ("b" "ball(x!1,r!1)")) (("1" (expand "lebesgue_measure") (("1" (expand "induced_measure") (("1" (expand "restrict") (("1" (replace -1) (("1" (hide -1) (("1" (decompose-equality) (("1" (expand "ball") (("1" (lemma "length_open_rew" ("a" "x!1-r!1" "b" "x!1+r!1")) (("1" (case-replace "{y: real | abs(x!1 - y) < r!1}={x | x!1 - r!1 < x AND x < x!1 + r!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)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded_interval?") (("2" (split) (("1" (expand "ball") (("1" (grind) nil nil)) nil) ("2" (expand "bounded?") (("2" (expand "nonempty?") (("2" (flatten) (("2" (assert) (("2" (hide 1) (("2" (expand "ball") (("2" (split) (("1" (expand "above_bounded") (("1" (inst + "x!1+r!1") (("1" (expand "upper_bound") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (inst + "x!1-r!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((ball const-decl "set[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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (lebesgue_outer_measure_bounded_interval formula-decl nil real_lebesgue nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (induced_measure const-decl "complete_measure" outer_measure_props "measure_integration_fnd/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (length const-decl "nnreal" real_intervals_aux nil) (TRUE const-decl "bool" booleans nil) (nnreal type-eq-decl nil real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (length_open_rew formula-decl nil real_intervals_aux nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (restrict const-decl "R" restrict nil) (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (bounded? const-decl "bool" real_topology "metric_space/") (upper_bound const-decl "bool" bound_defs "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (nonempty? const-decl "bool" sets nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (interval? const-decl "bool" real_topology "metric_space/")) 1513 1100 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measure_ball_TCC1 0 (lebesgue_measure_ball_TCC1-1 nil 3431866829 3475908905 ("" (subtype-tcc) nil nil) proved ((ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) 186 180 nil nil))("real_lebesgue_scaf" real_lebesgue_scaf closed_ball_is_lebesgue_measurable 0 (closed_ball_is_lebesgue_measurable-1 nil 3421699879 3475908905 ("" (skosimp) (("" (typepred "nnr!1") (("" (expand ">=") (("" (expand "<=") (("" (split -1) (("1" (lemma "ball_is_lebesgue_measurable") (("1" (inst - "nnr!1" "x!1") (("1" (lemma "singleton_is_outer_measurable" ("x" "x!1-nnr!1")) (("1" (lemma "singleton_is_outer_measurable" ("x" "x!1+nnr!1")) (("1" (lemma "outer_measurable_union" ("a" "singleton[real](x!1 - nnr!1)" "b" "singleton[real](x!1 + nnr!1)")) (("1" (expand "singleton") (("1" (expand "union") (("1" (expand "member") (("1" (lemma "outer_measurable_union" ("a" "{x: real | x = x!1 - nnr!1 OR x = nnr!1 + x!1}" "b" "ball[real, (LAMBDA (x, y: real): abs(x - y))](x!1, nnr!1)")) (("1" (case-replace "union[real]
                            ({x: real |
                                x = x!1 - nnr!1 OR x = nnr!1 + x!1},
                             ball[real, (LAMBDA (x, y: real): abs(x - y))]
                                 (x!1, nnr!1))=closed_ball(x!1, nnr!1)") (("1" (hide-all-but (-6 1)) (("1" (expand "closed_ball") (("1" (expand "ball") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (lemma "singleton_is_outer_measurable" ("x" "x!1")) (("2" (expand "closed_ball") (("2" (expand "singleton") (("2" (case-replace "{y: real | abs(x!1 - y) <= nnr!1}={y: real | y = x!1}") (("2" (hide -1 2) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((nnreal type-eq-decl nil real_types 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) (<= const-decl "bool" reals nil) (ball_is_lebesgue_measurable judgement-tcc nil real_lebesgue nil) (real_minus_real_is_real application-judgement "real" reals nil) (singleton_is_outer_measurable judgement-tcc nil real_lebesgue nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" sigma_countable "sigma_set/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (outer_measurable_union judgement-tcc nil outer_measure_props "measure_integration_fnd/") (outer_measurable? const-decl "bool" outer_measure_props "measure_integration_fnd/") (outer_measurable nonempty-type-eq-decl nil outer_measure_props "measure_integration_fnd/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (set type-eq-decl nil sets nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (outer_measure? const-decl "bool" outer_measure_def "measure_integration_fnd/") (outer_measure nonempty-type-eq-decl nil outer_measure_def "measure_integration_fnd/") (lebesgue_outer_measure const-decl "outer_measure" real_lebesgue nil) (union const-decl "set" sets nil) (ball_is_lebesgue_measurable application-judgement "outer_measurable" real_lebesgue nil) (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets 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/") (member const-decl "bool" sets nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnr!1 skolem-const-decl "nnreal" real_lebesgue nil) (> const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) 1346 1000 t nil))("real_lebesgue_scaf" real_lebesgue_scaf ball_is_lebesgue_measurable 0 (ball_is_lebesgue_measurable-1 nil 3421696254 3475908903 ("" (skosimp) (("" (case "borel?(ball[real, (LAMBDA (x, y: real): abs(x - y))](x1!1, r!1))") (("1" (assert) (("1" (lemma "borel_is_lebesgue_measurable") (("1" (inst - "ball[real, (LAMBDA (x, y: real): abs(x - y))](x1!1, r!1)") nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "borel?") (("2" (expand "extend") (("2" (expand "generated_sigma_algebra") (("2" (expand "Intersection") (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "fullset") (("2" (expand "subset?") (("2" (expand "member") (("2" (inst - "ball[real, (LAMBDA (x, y: real): abs(x - y))](x1!1, r!1)") (("2" (assert) (("2" (prop) (("2" (assert) (("2" (hide 2 -1) (("2" (expand "open?") (("2" (expand "member") (("2" (assert) (("2" (expand "metric_induced_topology") (("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) proved ((ball const-decl "set[T]" metric_space_def "metric_space/") (set type-eq-decl nil sets nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (borel? const-decl "sigma_algebra" borel "measure_integration_fnd/") (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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types 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) (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology "metric_space/") (metric_space_is_topology? name-judgement "(topology?)" real_topology "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff" real_topology "metric_space/") (ball_is_metric_open application-judgement "metric_open" real_topology "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (borel_is_lebesgue_measurable judgement-tcc nil real_lebesgue nil) (borel nonempty-type-eq-decl nil borel "measure_integration_fnd/") (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def "measure_integration_fnd/") (member const-decl "bool" sets nil) (FALSE const-decl "bool" booleans nil) (fullset const-decl "set" sets nil) (open nonempty-type-eq-decl nil topology "topology/") (open? const-decl "bool" topology "topology/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (Intersection const-decl "set" sets nil) (extend const-decl "R" extend nil)) 320 240 t nil))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measure_singleton 0 (lebesgue_measure_singleton-1 nil 3421365050 3475908903 ("" (skosimp) (("" (expand "lebesgue_measure") (("" (expand "induced_measure") (("" (expand "restrict") (("" (lemma "lebesgue_outer_measure_singleton" ("x" "x!1")) (("" (expand "x_eq") (("" (flatten) (("" (assert) (("" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue nil) (restrict const-decl "R" restrict nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" sigma_countable "sigma_set/") (TRUE const-decl "bool" booleans nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (lebesgue_outer_measure const-decl "outer_measure" real_lebesgue nil) (outer_measure nonempty-type-eq-decl nil outer_measure_def "measure_integration_fnd/") (outer_measure? const-decl "bool" outer_measure_def "measure_integration_fnd/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (set type-eq-decl nil sets nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (lebesgue_outer_measure_singleton formula-decl nil real_lebesgue 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) (induced_measure const-decl "complete_measure" outer_measure_props "measure_integration_fnd/")) 139 60 t shostak))("real_lebesgue_scaf" real_lebesgue_scaf lebesgue_measure_singleton_TCC1 0 (lebesgue_measure_singleton_TCC1-1 nil 3431866829 3475908903 ("" (subtype-tcc) nil nil) proved ((nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" sigma_countable "sigma_set/") (singleton_is_outer_measurable application-judgement "outer_measurable" real_lebesgue nil) (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil)) 207 210 nil nil))("real_lebesgue_scaf" real_lebesgue_scaf singleton_is_outer_measurable 0 (singleton_is_outer_measurable-1 nil 3421365379 3475908902 ("" (skosimp) (("" (lemma "singleton_is_borel" ("x" "x!1")) (("" (lemma "borel_is_lebesgue_measurable") (("" (inst - "singleton[real](x!1)") nil nil)) nil)) nil)) nil) proved ((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) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types 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) (singleton_is_borel formula-decl nil hausdorff_borel "measure_integration_fnd/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" sigma_countable "sigma_set/") (singleton_is_compact application-judgement "compact[T, (metric_induced_topology)]" real_topology "metric_space/") (singleton_is_closed application-judgement "closed[T, (metric_induced_topology)]" real_topology "metric_space/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration_fnd/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration_fnd/") (borel? const-decl "sigma_algebra" borel "measure_integration_fnd/") (borel nonempty-type-eq-decl nil borel "measure_integration_fnd/") (set type-eq-decl nil sets nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (x!1 skolem-const-decl "real" real_lebesgue nil) (borel_is_lebesgue_measurable judgement-tcc nil real_lebesgue nil)) 48 40 t nil))("ae_continuous_def" ae_continuous_def continuous_continuous? 0 (continuous_continuous?-1 nil 3452491142 3452514445 ("" (skosimp) (("" (expand "continuous") (("" (expand "continuous?") (("" (split) (("1" (skosimp*) (("1" (inst - "x!1") (("1" (rewrite "continuous_at_continuous_at?") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "x0!1") (("2" (rewrite "continuous_at_continuous_at?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((continuous const-decl "bool" continuous_functions "analysis/") (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) (continuous_at_continuous_at? formula-decl nil ae_continuous_def nil) (continuous? const-decl "bool" continuity_def "topology/")) 479 370 t shostak))("ae_continuous_def" ae_continuous_def continuous_at_continuous_at? 0 (continuous_at_continuous_at?-1 nil 3452491031 3452514444 ("" (skosimp) (("" (rewrite "continuity_def") (("" (rewrite "metric_continuous_at_def") (("" (expand "metric_continuous_at?") (("" (expand "member") (("" (expand "ball") (("" (split) (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp) (("1" (inst + "delta!1") (("1" (skosimp) (("1" (inst - "x!2") (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "epsilon!1") (("2" (skosimp) (("2" (inst + "delta!1") (("2" (skosimp) (("2" (inst - "x!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (continuity_def formula-decl nil continuous_functions "analysis/") (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) (metric_continuous_at? const-decl "bool" metric_continuity "metric_space/") (ball const-decl "set[T]" metric_space_def "metric_space/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (member const-decl "bool" sets nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (metric_continuous_at_def formula-decl nil metric_continuity "metric_space/")) 1276 1030 t shostak))("ae_continuous_def" ae_continuous_def IMP_integral_bounded_TCC2 0 (IMP_integral_bounded_TCC2-1 nil 3452512666 3452514472 ("" (skosimp) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil)) nil) proved ((real_plus_real_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) 9731 40 t nil))("ae_continuous_def" ae_continuous_def IMP_integral_bounded_TCC1 0 (IMP_integral_bounded_TCC1-1 nil 3452512666 3452514442 ("" (assuming-tcc) nil nil) proved nil 14 20 nil nil))