| products/sources/formale sprachen/PVS/lebesgue/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: finite_groups.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(lebesgue_def
(open_semi_infinite_is_cal_M 0 (open_semi_infinite_is_cal_M-1 nil 3471434094 ("" (skosimp) (("" (expand "member") (("" (expand "cal_M") (("" (lemma "outer_measurable_open_semi_infinite" ("a" "a!1")) (("" (expand "lebesgue_measurable") (("" (expand "fullset") (("" (expand "extend") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (outer_measurable_open_semi_infinite formula-decl nil real_lebesgue_scaf nil) (fullset const-decl "set" sets nil) (extend const-decl "R" extend nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue_scaf nil) (cal_M const-decl "sigma_algebra" lebesgue_def nil)) shostak)) (borel_is_cal_M 0 (borel_is_cal_M-1 nil 3471442368 ("" (expand "subset?") (("" (skosimp) (("" (expand "member") (("" (expand "cal_M") (("" (expand "lebesgue_measurable") (("" (expand "fullset") (("" (expand "extend") (("" (prop) (("" (lemma "borel_is_lebesgue_measurable") (("" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cal_M const-decl "sigma_algebra" lebesgue_def nil) (fullset const-decl "set" sets nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (>= 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) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (borel? const-decl "sigma_algebra" borel "measure_integration/") (borel nonempty-type-eq-decl nil borel "measure_integration/") (x!1 skolem-const-decl "setof[real]" lebesgue_def nil) (borel_is_lebesgue_measurable judgement-tcc nil real_lebesgue_scaf nil) (extend const-decl "R" extend nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue_scaf nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) shostak)) (open_interval_is_cal_M 0 (open_interval_is_cal_M-1 nil 3471443245 ("" (expand "subset?") (("" (skosimp) (("" (expand "member") (("" (lemma "borel_is_cal_M") (("" (expand "subset?") (("" (inst - "x!1") (("" (assert) (("" (hide 2) (("" (expand "borel?") (("" (expand "fullset") (("" (expand "extend") (("" (lemma "generated_sigma_algebra_subset1[real]") (("" (inst - "(LAMBDA (t: setof[real]): IF open?(t) THEN TRUE ELSE FALSE ENDIF)") (("" (expand "subset?") (("" (expand "member") (("" (inst - "x!1") (("" (assert) (("" (hide 2) (("" (expand "open_interval?") (("" (flatten) (("" (rewrite "metric_open_def") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((borel_is_cal_M formula-decl nil lebesgue_def nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (generated_sigma_algebra_subset1 formula-decl nil subset_algebra_def "measure_integration/") (metric_open_def formula-decl nil metric_space "metric_space/") (open_interval? const-decl "bool" real_intervals_aux nil) (FALSE const-decl "bool" booleans nil) (TRUE const-decl "bool" booleans nil) (open? 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) (>= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (setofsets type-eq-decl nil sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[real]" real_topology "metric_space/") (extend const-decl "R" extend nil) (borel? const-decl "sigma_algebra" borel "measure_integration/") (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) shostak)) (closed_interval_is_cal_M 0 (closed_interval_is_cal_M-1 nil 3471443113 ("" (lemma "borel_is_cal_M") (("" (expand "subset?") (("" (skosimp) (("" (inst - "x!1") (("" (expand "member") (("" (lemma "closed_is_borel" ("Y" "x!1")) (("1" (assert) nil nil) ("2" (expand "closed_interval?") (("2" (flatten) (("2" (expand "closed?") (("2" (expand "metric_closed?") (("2" (expand "member") (("2" (expand "metric_induced_topology") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (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) (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (closed_is_borel formula-decl nil borel "measure_integration/") (metric_closed? const-decl "bool" metric_space_def "metric_space/") (closed_interval? const-decl "bool" real_intervals_aux nil) (member const-decl "bool" sets nil) (borel_is_cal_M formula-decl nil lebesgue_def nil)) shostak)) (singleton_is_cal_M 0 (singleton_is_cal_M-1 nil 3471441879 ("" (skosimp) (("" (expand "member") (("" (expand "cal_M") (("" (expand "lebesgue_measurable") (("" (expand "fullset") (("" (expand "extend") (("" (assert) (("" (lemma "borel_is_lebesgue_measurable") (("" (inst - "singleton[real](x!1)") (("1" (assert) nil nil) ("2" (rewrite "singleton_is_borel") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_setofsets "sets_aux/") (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_compact application-judgement "compact[real, metric_induced_topology]" real_intervals nil) (member const-decl "bool" sets nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue_scaf nil) (extend const-decl "R" extend nil) (borel_is_lebesgue_measurable judgement-tcc nil real_lebesgue_scaf nil) (singleton_is_borel formula-decl nil hausdorff_borel "measure_integration/") (borel nonempty-type-eq-decl nil borel "measure_integration/") (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/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (>= 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) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (borel? const-decl "sigma_algebra" borel "measure_integration/") (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" lebesgue_def nil) (fullset const-decl "set" sets nil) (cal_M const-decl "sigma_algebra" lebesgue_def nil)) shostak)) (ball_is_cal_M 0 (ball_is_cal_M-1 nil 3471441715 ("" (skosimp) (("" (lemma "open_interval_is_cal_M") (("" (expand "subset?") (("" (inst - "ball(x!1, r!1)") (("" (assert) (("" (hide 2) (("" (expand "open_interval?") (("" (expand "interval?") (("" (skosimp) (("" (typepred "x!2") (("" (typepred "y!1") (("" (expand "ball") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((open_interval_is_cal_M formula-decl nil lebesgue_def nil) (real_minus_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) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets 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) (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/") (interval? const-decl "bool" real_topology "metric_space/") (NOT const-decl "[bool -> bool]" booleans nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (open_interval? const-decl "bool" real_intervals_aux nil) (member const-decl "bool" sets nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (subset? const-decl "bool" sets nil)) shostak)) (closed_ball_is_cal_M 0 (closed_ball_is_cal_M-1 nil 3471442240 ("" (skosimp) (("" (expand "member") (("" (expand "cal_M") (("" (expand "lebesgue_measurable") (("" (expand "fullset") (("" (expand "extend") (("" (lemma "borel_is_lebesgue_measurable") (("" (inst - "closed_ball(x!1, nnr!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "closed_is_borel" ("Y" "closed_ball(x!1, nnr!1)")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue_scaf nil) (extend const-decl "R" extend nil) (nnr!1 skolem-const-decl "nnreal" lebesgue_def nil) (x!1 skolem-const-decl "real" lebesgue_def nil) (closed_ball const-decl "closed" real_topology "metric_space/") (closed nonempty-type-eq-decl nil topology "topology/") (closed? const-decl "bool" topology "topology/") (set type-eq-decl nil sets nil) (nnreal type-eq-decl nil real_types nil) (borel? const-decl "sigma_algebra" borel "measure_integration/") (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/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (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) (borel nonempty-type-eq-decl nil borel "measure_integration/") (closed_is_borel formula-decl nil borel "measure_integration/") (borel_is_lebesgue_measurable judgement-tcc nil real_lebesgue_scaf nil) (fullset const-decl "set" sets nil) (cal_M const-decl "sigma_algebra" lebesgue_def nil)) shostak)) (lambda__TCC1 0 (lambda__TCC1-1 nil 3458582664 ("" (split) (("1" (expand "cal_M") (("1" (propax) nil nil)) nil) ("2" (typepred "lebesgue_measure") (("2" (expand "complete_sigma_finite?") (("2" (flatten) (("2" (split) (("1" (expand "measure?") (("1" (flatten) (("1" (split) (("1" (expand "measure_empty?") (("1" (propax) nil nil)) nil) ("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (inst - "X!1") (("1" (expand "o ") (("1" (expand "cal_M") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (typepred "X!1(x1!1)") (("1" (expand "cal_M") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (typepred "X!1") (("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measure_complete?") (("2" (skosimp) (("2" (inst - "x!1" "a!1") (("2" (assert) (("2" (expand "cal_M") (("2" (assert) (("2" (expand "lebesgue_measure") (("2" (assert) (("2" (split) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "measure_sigma_finite?") (("3" (skosimp) (("3" (inst + "X!1") (("1" (replace -3) (("1" (propax) nil nil)) nil) ("2" (expand "cal_M") (("2" (typepred "X!1") (("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue_scaf nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (lebesgue_measurable const-decl "sigma_algebra[real]" real_lebesgue_scaf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (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) (measure_sigma_finite? const-decl "bool" measure_def "measure_integration/") (X!1 skolem-const-decl "disjoint_indexed_measurable[real, lebesgue_measurable]" lebesgue_def nil) (measure_complete? const-decl "bool" generalized_measure_def "measure_integration/") (set type-eq-decl nil sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (measure? const-decl "bool" generalized_measure_def "measure_integration/") (measure_empty? const-decl "bool" generalized_measure_def "measure_integration/") (O const-decl "T3" function_props 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) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def "measure_integration/") (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (X!1 skolem-const-decl "disjoint_indexed_measurable[real, cal_M]" lebesgue_def nil) (measure_countably_additive? const-decl "bool" generalized_measure_def "measure_integration/") (cal_M const-decl "sigma_algebra" lebesgue_def nil)) nil)) (lambda_singleton_TCC1 0 (lambda_singleton_TCC1-1 nil 3475933087 ("" (skosimp) (("" (lemma "singleton_is_cal_M" ("x" "x!1")) (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (singleton_is_cal_M formula-decl nil lebesgue_def nil) (member const-decl "bool" sets nil)) nil)) (lambda_singleton 0 (lambda_singleton-1 nil 3475933229 ("" (skosimp) (("" (expand "lambda_") (("" (lemma "lebesgue_outer_measure_singleton" ("x" "x!1")) (("" (expand "lebesgue_measure") (("" (expand "induced_measure") (("" (expand "restrict") (("" (expand "x_eq") (("" (flatten) (("" (assert) (("" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue_scaf nil) (restrict const-decl "R" restrict nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types 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/") (outer_measure nonempty-type-eq-decl nil outer_measure_def "measure_integration/") (lebesgue_outer_measure const-decl "outer_measure" real_lebesgue_scaf nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (TRUE const-decl "bool" booleans nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_setofsets "sets_aux/") (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_compact application-judgement "compact[real, metric_induced_topology]" real_intervals nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (induced_measure const-decl "complete_measure" outer_measure_props "measure_integration/") (lebesgue_outer_measure_singleton formula-decl nil real_lebesgue_scaf 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)) shostak)) (lambda_ball_TCC1 0 (lambda_ball_TCC1-1 nil 3475932807 ("" (skosimp) (("" (lemma "ball_is_cal_M" ("x" "x1!1" "r" "r!1")) (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil) ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (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_cal_M formula-decl nil lebesgue_def nil) (member const-decl "bool" sets nil)) nil)) (lambda_ball 0 (lambda_ball-1 nil 3475932807 ("" (skosimp) (("" (lemma "lebesgue_outer_measure_bounded_interval" ("b" "ball(x!1,r!1)")) (("1" (expand "lambda_") (("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" (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) ("2" (hide 2) (("2" (expand "bounded_interval?") (("2" (split) (("1" (grind) nil nil) ("2" (expand "bounded?") (("2" (flatten) (("2" (expand "nonempty?") (("2" (assert) (("2" (hide 1) (("2" (split) (("1" (expand "above_bounded") (("1" (inst + "x!1+r!1") (("1" (grind) 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) ((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_scaf nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue_scaf nil) (restrict const-decl "R" restrict nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (length_open_rew formula-decl nil real_intervals_aux nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (TRUE const-decl "bool" booleans nil) (length const-decl "nnreal" real_intervals_aux nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (induced_measure const-decl "complete_measure" outer_measure_props "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (bounded? const-decl "bool" real_topology "metric_space/") (nonempty? const-decl "bool" sets nil) (below_bounded const-decl "bool" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (interval? const-decl "bool" real_topology "metric_space/") (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (lambda_closed_ball_TCC1 0 (lambda_closed_ball_TCC1-1 nil 3475933226 ("" (skosimp) (("" (lemma "closed_ball_is_cal_M" ("x" "x!1" "nnr" "nnr!1")) (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) 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_cal_M formula-decl nil lebesgue_def nil) (member const-decl "bool" sets nil)) nil)) (lambda_closed_ball 0 (lambda_closed_ball-1 nil 3475933366 ("" (skosimp) (("" (expand "lambda_") (("" (expand "lebesgue_measure") (("" (expand "induced_measure") (("" (expand "restrict") (("" (lemma "lebesgue_outer_measure_eq_length" ("b" "closed_ball(x!1, nnr!1)")) (("1" (case-replace "x_length(closed_ball(x!1, nnr!1))=(TRUE, 2 * nnr!1)") (("1" (hide -1) (("1" (expand "x_eq") (("1" (flatten) (("1" (assert) (("1" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "x_length") (("2" (lift-if) (("2" (assert) (("2" (prop) (("1" (lemma "length_closed_rew" ("a" "x!1-nnr!1" "b" "x!1+nnr!1")) (("1" (case-replace "closed_ball(x!1, nnr!1)={x | x!1 - nnr!1 <= x AND x <= x!1 + nnr!1}") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "closed_ball") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_interval?") (("2" (split) (("1" (grind) nil nil) ("2" (expand "bounded?") (("2" (expand "nonempty?") (("2" (flatten) (("2" (assert) (("2" (hide 1) (("2" (split) (("1" (expand "above_bounded") (("1" (inst + "x!1+nnr!1") (("1" (grind) nil nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (inst + "x!1-nnr!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded_interval?") (("2" (split) (("1" (grind) nil nil) ("2" (expand "bounded?") (("2" (expand "nonempty?") (("2" (flatten) (("2" (assert) (("2" (hide 1) (("2" (split) (("1" (expand "above_bounded") (("1" (inst + "x!1+nnr!1") (("1" (grind) nil nil)) nil)) nil) ("2" (expand "below_bounded") (("2" (inst + "x!1-nnr!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (induced_measure const-decl "complete_measure" outer_measure_props "measure_integration/") (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) (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_eq_length formula-decl nil real_lebesgue_scaf nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (length_closed_rew formula-decl nil real_intervals_aux nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (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/") (bounded? const-decl "bool" real_topology "metric_space/") (outer_measure? const-decl "bool" outer_measure_def "measure_integration/") (outer_measure nonempty-type-eq-decl nil outer_measure_def "measure_integration/") (lebesgue_outer_measure const-decl "outer_measure" real_lebesgue_scaf nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (TRUE const-decl "bool" booleans nil) (x_length const-decl "extended_nnreal" real_lebesgue_scaf nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (interval nonempty-type-eq-decl nil real_topology "metric_space/") (interval? const-decl "bool" real_topology "metric_space/") (= const-decl "[T, T -> boolean]" equalities nil) (restrict const-decl "R" restrict nil) (lebesgue_measure const-decl "complete_sigma_finite[real, lebesgue_measurable]" real_lebesgue_scaf nil)) shostak)) (integrable_phi_open 0 (integrable_phi_open-1 nil 3475932141 ("" (skosimp) (("" (rewrite "isf_is_integrable") (("" (hide 2) (("" (lemma "isf_phi[real, cal_M, lambda_]" ("E" "open(a!1, b!1)")) (("1" (propax) nil nil) ("2" (hide 2) (("2" (lemma "lambda_ball" ("x" "(b!1+a!1)/2" "r" "(b!1-a!1)/2")) (("2" (lemma "ball_is_cal_M" ("x" "(b!1+a!1)/2" "r" "(b!1-a!1)/2")) (("2" (expand "member") (("2" (expand "measurable_set?") (("2" (case-replace "open(a!1, b!1)=ball((b!1 + a!1) / 2, (b!1 - a!1) / 2)") (("1" (assert) (("1" (replace -2) (("1" (expand "mu_fin?") (("1" (replace -3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "open") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf_is_integrable judgement-tcc nil integral "measure_integration/") (isf? const-decl "bool" isf "measure_integration/") (isf nonempty-type-eq-decl nil isf "measure_integration/") (set type-eq-decl nil sets nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phi const-decl "nat" measure_space "measure_integration/") (< 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/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (isf_phi judgement-tcc nil isf "measure_integration/") (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (mu_fin? const-decl "bool" measure_props "measure_integration/") (real_div_nzreal_is_real application-judgement "real" reals nil) (lambda_ball formula-decl nil lebesgue_def nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (member const-decl "bool" sets nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (ball_is_cal_M formula-decl nil lebesgue_def nil)) shostak)) (integrable_phi_closed 0 (integrable_phi_closed-1 nil 3475934373 ("" (skosimp) (("" (case-replace "closed(a!1, b!1)=closed_ball((b!1+a!1)/2,(b!1-a!1)/2)") (("1" (hide -1) (("1" (lemma "lambda_closed_ball" ("x" "(b!1 + a!1) / 2" "nnr" "(b!1 - a!1) / 2")) (("1" (lemma "closed_ball_is_cal_M" ("x" "(b!1 + a!1) / 2" "nnr" "(b!1 - a!1) / 2")) (("1" (expand "member") (("1" (rewrite "isf_is_integrable" +) (("1" (hide 2) (("1" (rewrite "isf_phi") (("1" (hide 2) (("1" (expand "measurable_set?") (("1" (replace -1) (("1" (expand "mu_fin?") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (expand "closed") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_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) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets 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) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (lambda_closed_ball formula-decl nil lebesgue_def nil) (member const-decl "bool" sets nil) (isf_phi judgement-tcc nil isf "measure_integration/") (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (mu_fin? const-decl "bool" measure_props "measure_integration/") (real_times_real_is_real application-judgement "real" reals nil) (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (phi const-decl "nat" measure_space "measure_integration/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (isf nonempty-type-eq-decl nil isf "measure_integration/") (isf? const-decl "bool" isf "measure_integration/") (isf_is_integrable judgement-tcc nil integral "measure_integration/") (real_plus_real_is_real application-judgement "real" reals nil) (closed_ball_is_cal_M formula-decl nil lebesgue_def nil)) shostak)) (integral_phi_open_TCC1 0 (integral_phi_open_TCC1-1 nil 3475932041 ("" (skosimp) (("" (rewrite "integrable_phi_open") nil nil)) nil) ((integrable_phi_open formula-decl nil lebesgue_def nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil)) nil)) (integral_phi_open 0 (integral_phi_open-1 nil 3475934094 ("" (skosimp) (("" (case-replace "open(a!1, b!1)=ball((b!1 + a!1) / 2, (b!1 - a!1) / 2)") (("1" (hide -1) (("1" (lemma "lambda_ball" ("x" "(b!1 + a!1) / 2" "r" "(b!1 - a!1) / 2")) (("1" (lemma "ball_is_cal_M" ("x" "(b!1 + a!1) / 2" "r" "(b!1 - a!1) / 2")) (("1" (expand "member") (("1" (rewrite "integral_phi") (("1" (expand "mu") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (replace -1) (("2" (expand "mu_fin?") (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "open") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (real_minus_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) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals 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) (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/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (lambda_ball formula-decl nil lebesgue_def nil) (member const-decl "bool" sets nil) (mu const-decl "nnreal" measure_props "measure_integration/") (real_times_real_is_real application-judgement "real" reals nil) (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (mu_fin? const-decl "bool" measure_props "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (integral_phi formula-decl nil integral "measure_integration/") (real_plus_real_is_real application-judgement "real" reals nil) (ball_is_cal_M formula-decl nil lebesgue_def nil)) shostak)) (integral_phi_closed_TCC1 0 (integral_phi_closed_TCC1-1 nil 3475932041 ("" (skosimp) (("" (rewrite "integrable_phi_closed") nil nil)) nil) ((integrable_phi_closed formula-decl nil lebesgue_def nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil)) nil)) (integral_phi_closed 0 (integral_phi_closed-1 nil 3475934559 ("" (skosimp) (("" (case-replace "closed(a!1, b!1)=closed_ball((b!1+a!1)/2,(b!1-a!1)/2)") (("1" (hide -1) (("1" (lemma "lambda_closed_ball" ("x" "(b!1 + a!1) / 2" "nnr" "(b!1 - a!1) / 2")) (("1" (lemma "closed_ball_is_cal_M" ("x" "(b!1 + a!1) / 2" "nnr" "(b!1 - a!1) / 2")) (("1" (expand "member") (("1" (rewrite "integral_phi") (("1" (expand "mu") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "mu_fin?") (("2" (replace -2) (("2" (assert) (("2" (expand "measurable_set?") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (expand "closed") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_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) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets 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) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (closed? const-decl "bool" topology "topology/") (closed nonempty-type-eq-decl nil topology "topology/") (closed_ball const-decl "closed" real_topology "metric_space/") (closed_interval nonempty-type-eq-decl nil real_topology "metric_space/") (closed const-decl "closed_interval" real_topology "metric_space/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (lambda_closed_ball formula-decl nil lebesgue_def nil) (member const-decl "bool" sets nil) (mu const-decl "nnreal" measure_props "measure_integration/") (real_times_real_is_real application-judgement "real" reals nil) (lambda_ const-decl "complete_sigma_finite[real, cal_M]" lebesgue_def nil) (complete_sigma_finite type-eq-decl nil measure_def "measure_integration/") (complete_sigma_finite? const-decl "bool" measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (cal_M const-decl "sigma_algebra" lebesgue_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (mu_fin? const-decl "bool" measure_props "measure_integration/") (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (integral_phi formula-decl nil integral "measure_integration/") (real_plus_real_is_real application-judgement "real" reals nil) (closed_ball_is_cal_M formula-decl nil lebesgue_def nil)) shostak)) (I_is_measurable 0 (I_is_measurable-1 nil 3475936049 ("" (rewrite "measurable_def2") (("" (skosimp) (("" (typepred "i!1") (("" (skosimp) (("" (lemma "ball_is_cal_M" ("x" "x!1" "r" "r!1")) (("" (expand "member") (("" (case-replace "inverse_image(I[real], i!1)=i!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "inverse_image") (("2" (expand "member") (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.93 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
