products/sources/formale sprachen/PVS/lebesgue/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: orph-prfs   Sprache: Unknown

("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) +
--> --------------------

--> maximum size reached

--> --------------------

[ Dauer der Verarbeitung: 0.32 Sekunden  (vorverarbeitet)  ]