| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 MB |
|
Quellcode-Bibliothek isf.prfSprache: Lisp |
|||||||||||||||
|
(isf (nonzero_measurable 0 (nonzero_measurable-1 nil 3390787726 ("" (skosimp) (("" (typepred "g!1") (("" (expand "measurable_function?") (("" (lemma "singleton_is_borel" ("x" "0")) (("" (lemma "fullset_is_borel[real,metric_induced_topology]") (("" (lemma "difference_is_borel[real,metric_induced_topology]" ("a" "fullset[real]" "b" "singleton[real](0)")) (("1" (inst - "difference[real](fullset[real], singleton[real](0))") (("1" (expand "measurable_set?") (("1" (case-replace "inverse_image(g!1, difference[real](fullset[real], singleton[real](0))) = nonzero_set?(g!1)") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (expand "nonzero_set?") (("1" (expand "singleton") (("1" (expand "fullset") (("1" (expand "difference") (("1" (expand "member") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (expand "/=") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (S formal-const-decl "sigma_algebra" isf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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) (singleton_is_borel formula-decl nil hausdorff_borel nil) (real_is_complete name-judgement "metric_complete" real_topology "metric_space/") (fullset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (singleton_is_compact application-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[nat]" countability "sets_aux/") (difference_is_borel formula-decl nil borel nil) (borel? const-decl "sigma_algebra" borel nil) (borel nonempty-type-eq-decl nil borel nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (measurable_set? const-decl "bool" measure_space_def nil) (member const-decl "bool" sets nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (inverse_image const-decl "set[D]" function_image nil) (nonzero_set? const-decl "set[T]" isf nil) (difference const-decl "set" sets nil) (open_diff_closed_is_open application-judgement "open[real, (metric_induced_topology)]" convergence_aux "metric_space/") (fullset_is_borel formula-decl nil borel nil)) shostak)) (nonzero_set_phi 0 (nonzero_set_phi-1 nil 3390785835 ("" (skosimp) (("" (typepred "X!1") (("" (apply-extensionality 1 :hide? t) (("" (expand "nonzero_set?") (("" (expand "phi") (("" (expand "member") (("" (case-replace "X!1(x!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" isf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (phi_is_simple application-judgement "simple" isf 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) (nonzero_set? const-decl "set[T]" isf 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) (phi const-decl "nat" measure_space nil)) shostak)) (isf?_TCC1 0 (isf?_TCC1-1 nil 3390785367 ("" (skosimp*) (("" (expand "simple?") (("" (flatten) (("" (lemma "nonzero_measurable" ("g" "f!1")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((simple? const-decl "bool" measure_space nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (S formal-const-decl "sigma_algebra" isf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil isf nil) (nonzero_measurable formula-decl nil isf nil)) nil)) (isf_zero 0 (isf_zero-1 nil 3395229959 ("" (expand "isf?") (("" (lemma "simple_const" ("c" "0")) (("" (replace -1) (("" (hide -1) (("" (expand "nonzero_set?") (("" (expand "mu_fin?") (("" (lemma "m_emptyset") (("" (expand "emptyset") (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" isf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil isf 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) (simple_const formula-decl nil measure_space nil) (mu_fin? const-decl "bool" measure_props nil) (emptyset const-decl "set" sets nil) (m_emptyset formula-decl nil measure_props 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/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" isf nil) (nonzero_set? const-decl "set[T]" isf nil) (isf? const-decl "bool" isf nil)) shostak)) (isf_TCC1 0 (isf_TCC1-1 nil 3390785367 ("" (expand "isf?") (("" (split) (("1" (expand "simple?") (("1" (split) (("1" (expand "measurable_function?") (("1" (skosimp) (("1" (case "B!1(0)") (("1" (case-replace "inverse_image(LAMBDA (x: T): 0, B!1)=fullset[T]") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "fullset") (("2" (expand "inverse_image") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "inverse_image(LAMBDA (x: T): 0, B!1)=emptyset[T]") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (hide 3) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "inverse_image") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "empty?(fullset[T])") (("1" (case-replace "image(LAMBDA (x: T): 0, fullset[T]) = emptyset[real]") (("1" (assert) nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "fullset") (("2" (hide 1) (("2" (expand "image") (("2" (skolem - ("TT")) (("2" (expand "empty?") (("2" (inst - "TT") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "image[T,real](LAMBDA (x: T): 0, fullset[T]) = singleton[real](0)") (("1" (assert) nil nil) ("2" (hide 3) (("2" (expand "singleton") (("2" (apply-extensionality :hide? t) (("2" (case-replace "x!1=0") (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "empty?") (("1" (skosimp) (("1" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "fullset") (("2" (expand "image") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonzero_set?") (("2" (typepred "m") (("2" (expand "measure?") (("2" (flatten) (("2" (expand "mu_fin?") (("2" (assert) (("2" (expand "measure_empty?") (("2" (expand "emptyset") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((emptyset const-decl "set" sets nil) (subset_algebra_emptyset name-judgement "(S)" isf nil) (null_emptyset name-judgement "null_set" isf 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" finite_sets nil) (measurable_fullset name-judgement "measurable_set[T, S]" isf nil) (subset_algebra_fullset name-judgement "(S)" isf nil) (T formal-type-decl nil isf nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (inverse_image const-decl "set[D]" function_image nil) (fullset const-decl "set" sets nil) (measurable_set? const-decl "bool" measure_space_def nil) (member 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) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def 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) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (borel? const-decl "sigma_algebra" borel nil) (borel nonempty-type-eq-decl nil borel nil) (measurable_function? const-decl "bool" measure_space_def nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (singleton_is_compact application-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[nat]" countability "sets_aux/") (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (image const-decl "set[R]" function_image nil) (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (finite_emptyset name-judgement "finite_set[real]" measure_space nil) (TRUE const-decl "bool" booleans nil) (empty? const-decl "bool" sets nil) (simple? const-decl "bool" measure_space nil) (m formal-const-decl "measure_type" isf nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (S formal-const-decl "sigma_algebra" isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (mu_fin? const-decl "bool" measure_props nil) (nonzero_set? const-decl "set[T]" isf nil) (isf? const-decl "bool" isf nil)) nil)) (isf_is_simple 0 (isf_is_simple-1 nil 3390790021 ("" (skosimp) (("" (typepred "x!1") (("" (expand "isf?") (("" (flatten) nil nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (isf_add 0 (isf_add-1 nil 3390785367 ("" (skosimp) (("" (typepred "i1!1") (("" (typepred "i2!1") (("" (expand "isf?") (("" (flatten) (("" (lemma "simple_add" ("h1" "i1!1" "h2" "i2!1")) (("" (assert) (("" (expand "+") (("" (expand "simple?") (("" (flatten) (("" (hide-all-but (-5 -8 1)) (("" (lemma "union_difference" ("a" "nonzero_set?(i1!1)" "b" "nonzero_set?(i2!1)")) (("" (lemma "difference_disjoint" ("a" "nonzero_set?(i1!1)" "b" "nonzero_set?(i2!1)")) (("" (lemma "m_disjoint_union" ("a" "nonzero_set?(i1!1)" "b" "difference(nonzero_set?(i2!1), nonzero_set?(i1!1))")) (("1" (replace -2 -1) (("1" (replace -3 -1 rl) (("1" (expand "mu_fin?") (("1" (expand "x_eq") (("1" (expand "x_add") (("1" (replace -5) (("1" (flatten) (("1" (hide -2) (("1" (lemma "m_monotone" ("a" "difference(nonzero_set?(i2!1), nonzero_set?(i1!1))" "b" "nonzero_set?(i2!1)")) (("1" (split -1) (("1" (expand "x_le") (("1" (replace -5) (("1" (flatten) (("1" (replace -1) (("1" (hide -2) (("1" (hide-all-but (-2 1)) (("1" (lemma "m_monotone" ("a" "nonzero_set?(LAMBDA (x: T): i1!1(x) + i2!1(x))" "b" "union(nonzero_set?(i1!1), nonzero_set?(i2!1))")) (("1" (split -1) (("1" (expand "x_le") (("1" (replace -2) (("1" (flatten) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "nonzero_set?") (("2" (expand "union") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "nonzero_measurable" ("g" "i1!1")) (("2" (lemma "nonzero_measurable" ("g" "i2!1")) (("2" (expand "measurable_set?") (("2" (lemma "sigma_algebra_union" ("x" "nonzero_set?(i1!1)" "y" "nonzero_set?(i2!1)")) (("1" (assert) nil nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "nonzero_measurable" ("g" "LAMBDA (x: T): i1!1(x) + i2!1(x)")) (("1" (propax) nil nil) ("2" (hide 2) (("2" (lemma "sum_measurable" ("g1" "i1!1" "g2" "i2!1")) (("2" (expand "+") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "nonzero_set?") (("2" (expand "difference") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "nonzero_measurable" ("g" "i2!1")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_algebra_difference" ("x" "nonzero_set?(i2!1)" "y" "nonzero_set?(i1!1)")) (("1" (expand "measurable_set?") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "nonzero_measurable" ("g" "i1!1")) (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil) ("3" (lemma "nonzero_measurable" ("g" "i2!1")) (("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (sum_measurable application-judgement "measurable_function[T, S]" isf nil) (simple_add application-judgement "simple" isf nil) (S formal-const-decl "sigma_algebra" isf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space nil) (simple_add judgement-tcc nil measure_space nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (union_difference formula-decl nil sets_lemmas nil) (set type-eq-decl nil sets nil) (nonzero_set? const-decl "set[T]" isf nil) (m formal-const-decl "measure_type" isf nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (difference const-decl "set" sets nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (m_disjoint_union formula-decl nil measure_props nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (sum_measurable judgement-tcc nil measure_space_def nil) (sigma_algebra_union formula-decl nil sigma_algebra nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (nonzero_measurable formula-decl nil isf nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (union const-decl "set" sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (m_monotone formula-decl nil measure_props nil) (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (mu_fin? const-decl "bool" measure_props nil) (sigma_algebra_difference formula-decl nil sigma_algebra nil) (difference_disjoint formula-decl nil sets_lemmas nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (isf_scal 0 (isf_scal-1 nil 3390785367 ("" (skosimp) (("" (typepred "i!1") (("" (expand "*") (("" (expand "isf?") (("" (flatten) (("" (lemma "simple_scal" ("c" "c!1" "h" "i!1")) (("" (expand "*") (("" (split) (("1" (propax) nil nil) ("2" (hide -1 -2) (("2" (case-replace "c!1=0") (("1" (case-replace "nonzero_set?(LAMBDA (x: T): 0 * i!1(x)) = emptyset[T]") (("1" (expand "mu_fin?") (("1" (typepred "m") (("1" (expand "measure?") (("1" (flatten) (("1" (assert) (("1" (expand "measure_empty?") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "emptyset") (("2" (expand "nonzero_set?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "nonzero_set?(LAMBDA (x: T): c!1 * i!1(x)) = nonzero_set?(i!1)") (("2" (hide-all-but (1 2)) (("2" (apply-extensionality :hide? t) (("2" (expand "nonzero_set?") (("2" (expand "/=") (("2" (assert) (("2" (case-replace "i!1(x!1) = 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (S formal-const-decl "sigma_algebra" isf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space nil) (simple_scal judgement-tcc nil measure_space nil) (= const-decl "[T, T -> boolean]" equalities nil) (mu_fin? const-decl "bool" measure_props nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (m formal-const-decl "measure_type" isf nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (null_emptyset name-judgement "null_set" isf nil) (subset_algebra_emptyset name-judgement "(S)" isf nil) (set type-eq-decl nil sets nil) (nonzero_set? const-decl "set[T]" isf nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (emptyset const-decl "set" sets nil) (/= const-decl "boolean" notequal nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil)) nil)) (isf_opp 0 (isf_opp-1 nil 3390790565 ("" (skosimp) (("" (typepred "i!1") (("" (lemma "isf_scal" ("c" "-1" "i" "i!1")) (("" (expand "*") (("" (expand "-" 1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (isf_scal judgement-tcc nil isf nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil)) nil)) (isf_diff 0 (isf_diff-1 nil 3390790565 ("" (skosimp) (("" (lemma "isf_opp" ("i" "i2!1")) (("" (lemma "isf_add" ("i1" "i1!1" "i2" "-i2!1")) (("" (expand "-") (("" (expand "+") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (isf_opp judgement-tcc nil isf nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (isf_opp application-judgement "isf" isf nil) (isf_add judgement-tcc nil isf nil) (- const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (isf_abs 0 (isf_abs-1 nil 3390785367 ("" (skosimp) (("" (typepred "i!1") (("" (expand "isf?") (("" (flatten) (("" (lemma "simple_abs" ("h" "i!1")) (("" (expand "simple?") (("" (flatten) (("" (lemma "m_monotone" ("a" "nonzero_set?(abs[T](i!1))" "b" "nonzero_set?(i!1)")) (("" (split -1) (("1" (expand "x_le") (("1" (expand "mu_fin?") (("1" (replace -6) (("1" (flatten) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "nonzero_set?") (("2" (expand "abs") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (replace -1) (("2" (expand "abs") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (m formal-const-decl "measure_type" isf nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (nonzero_set? const-decl "set[T]" isf nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (set type-eq-decl nil sets nil) (m_monotone formula-decl nil measure_props nil) (member const-decl "bool" sets nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (subset? const-decl "bool" sets nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (mu_fin? const-decl "bool" measure_props nil) (simple_abs judgement-tcc nil measure_space nil) (simple? const-decl "bool" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" isf nil) (simple_abs application-judgement "simple" isf nil) (abs_measurable application-judgement "measurable_function[T, S]" isf nil)) nil)) (isf_min 0 (isf_min-1 nil 3390785367 ("" (skosimp) (("" (typepred "i1!1") (("" (typepred "i2!1") (("" (expand "isf?") (("" (flatten) (("" (lemma "simple_min" ("h1" "i1!1" "h2" "i2!1")) (("" (expand "min") (("" (hide -1 -2 -4) (("" (expand "mu_fin?") (("" (case "subset?(nonzero_set?(LAMBDA (x: T): min(i1!1(x), i2!1(x))),union(nonzero_set?( (("1" (lemma "m_union" ("a" "nonzero_set?(i1!1)" "b" "nonzero_set?(i2!1)")) (("1" (lemma "m_monotone" ("a" "nonzero_set?(LAMBDA (x: T): min(i1!1(x), i2!1(x)))" "b" "union(nonzero_set?(i1!1), nonzero_set?(i2!1))")) (("1" (replace -3 -1 LR) (("1" (name-replace "NZM" "nonzero_set?(LAMBDA (x: T): min(i1!1(x), i2!1(x)))") (("1" (hide -3) (("1" (expand "x_le") (("1" (assert) (("1" (expand "x_add") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (lemma "sigma_algebra_union" ("x" "nonzero_set?(i1!1)" "y" "nonzero_set?(i2!1)")) (("2" (assert) nil nil)) nil)) nil) ("3" (rewrite "nonzero_measurable") (("3" (lemma "min_measurable" ("g1" "i1!1" "g2" "i2!1")) (("3" (expand "min" -1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "nonzero_measurable" ("g" "i2!1")) (("2" (propax) nil nil)) nil) ("3" (lemma "nonzero_measurable" ("g" "i1!1")) (("3" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (min_measurable application-judgement "measurable_function[T, S]" isf nil) (simple_min application-judgement "simple" isf nil) (S formal-const-decl "sigma_algebra" isf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space nil) (simple_min judgement-tcc nil measure_space nil) (set type-eq-decl nil sets nil) (subset? const-decl "bool" sets nil) (nonzero_set? const-decl "set[T]" isf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (union const-decl "set" sets nil) (m_monotone formula-decl nil measure_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_algebra_union formula-decl nil sigma_algebra nil) (member const-decl "bool" sets nil) (min_measurable judgement-tcc nil measure_space nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (nonzero_measurable formula-decl nil isf nil) (measurable_function? const-decl "bool" measure_space_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (m formal-const-decl "measure_type" isf nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (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 nil) (measurable_set? const-decl "bool" measure_space_def nil) (m_union formula-decl nil measure_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mu_fin? const-decl "bool" measure_props nil) (min const-decl "[T -> real]" real_fun_ops_aux "reals/")) nil)) (isf_max 0 (isf_max-1 nil 3390785367 ("" (skosimp) (("" (typepred "i1!1") (("" (typepred "i2!1") (("" (lemma "isf_scal" ("c" "-1" "i" "i1!1")) (("" (lemma "isf_scal" ("c" "-1" "i" "i2!1")) (("" (lemma "isf_min" ("i1" "*[T](-1, i1!1)" "i2" "*[T](-1, i2!1)")) (("" (expand "*") (("" (expand "min") (("" (lemma "isf_scal" ("c" "-1" "i" "LAMBDA (x_1: T): min(-1 * i1!1(x_1), -1 * i2!1(x_1))")) (("1" (expand "*" -1) (("1" (expand "min") (("1" (expand "max") (("1" (expand "max") (("1" (case-replace "(LAMBDA (x: T): -1 * IF -1 * i1!1(x) > -1 * i2!1(x) THEN -1 * i2!1(x) ELSE -1 * i1!1(x) ENDIF)=(LAMBDA (x: T): IF i1!1(x) < i2!1(x) THEN i2!1(x) ELSE i1!1(x) ENDIF)") (("1" (apply-extensionality :hide? t) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (isf_scal judgement-tcc nil isf nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (isf_scal application-judgement "isf" isf nil) (isf_min judgement-tcc nil isf nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (min const-decl "[T -> real]" real_fun_ops_aux "reals/") (max const-decl "[T -> real]" real_fun_ops_aux "reals/") (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (isf_minimum 0 (isf_minimum-1 nil 3409635960 ("" (induct "n") (("1" (expand "minimum") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (inst - "w!1") (("2" (expand "minimum" 1) (("2" (assert) (("2" (rewrite "isf_min") nil nil)) nil)) nil)) nil)) nil)) nil) ((min_measurable application-judgement "measurable_function[T, S]" isf nil) (simple_min application-judgement "simple" isf nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (isf_min judgement-tcc nil isf nil) (minimum_measurable application-judgement "measurable_function[T, S]" isf nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (minimum def-decl "[T -> real]" real_fun_ops_aux "reals/") (sequence type-eq-decl nil sequences nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (T formal-type-decl nil isf nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (isf_maximum 0 (isf_maximum-1 nil 3409635960 ("" (induct "n") (("1" (expand "maximum") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (inst - "w!1") (("2" (expand "maximum" 1) (("2" (rewrite "isf_max") nil nil)) nil)) nil)) nil)) nil) ((max_measurable application-judgement "measurable_function[T, S]" isf nil) (simple_max application-judgement "simple" isf nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (maximum_measurable application-judgement "measurable_function[T, S]" isf nil) (isf_max judgement-tcc nil isf nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat_induction formula-decl nil naturalnumbers nil) (maximum def-decl "[T -> real]" real_fun_ops_aux "reals/") (sequence type-eq-decl nil sequences nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (T formal-type-decl nil isf nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (isf_plus 0 (isf_plus-1 nil 3390785367 ("" (skosimp) (("" (typepred "i!1") (("" (lemma "isf_max" ("i1" "i!1" "i2" "lambda x: 0")) (("1" (expand "max") (("1" (expand "plus") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "isf_zero") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (isf_zero formula-decl nil isf nil) (max const-decl "[T -> real]" real_fun_ops_aux "reals/") (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (isf_max judgement-tcc nil isf nil)) nil)) (isf_minus 0 (isf_minus-1 nil 3390785367 ("" (skosimp) (("" (lemma "isf_min" ("i1" "i!1" "i2" "lambda x: 0")) (("1" (expand "min") (("1" (lemma "isf_scal" ("c" "-1" "i" "LAMBDA (x_1: T): min(i!1(x_1), 0)")) (("1" (expand "*") (("1" (expand "minus") (("1" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (lemma "isf_zero") (("2" (propax) nil nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (isf_min judgement-tcc nil isf nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (isf_scal judgement-tcc nil isf nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (min const-decl "[T -> real]" real_fun_ops_aux "reals/") (isf_zero formula-decl nil isf nil)) nil)) (isf_sq 0 (isf_sq-1 nil 3390790771 ("" (skosimp) (("" (typepred "i!1") (("" (expand "sq") (("" (expand "isf?") (("" (flatten) (("" (split) (("1" (hide -2) (("1" (expand "simple?") (("1" (flatten) (("1" (split) (("1" (hide -2) (("1" (lemma "prod_measurable" ("g1" "i!1" "g2" "i!1")) (("1" (expand "sq") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "finite_image[real,real]") (("2" (inst - "image(i!1, fullset[T])" "lambda (x:real): x*x") (("2" (case-replace "image[real, real] (LAMBDA (x: real): x * x, image[T,real](i!1, fullset[T]))=image[T,real](LAMBDA (x: T): sq( (("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "fullset") (("2" (expand "sq") (("2" (expand "image") (("2" (case-replace "(EXISTS (x_1: ({x: T | TRUE})): x!1 = i!1(x_1) * i!1(x_1))") (("1" (skosimp) (("1" (inst + "i!1(x!2)") (("1" (inst + "x!2") nil nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp*) (("2" (typepred "x!2") (("2" (skosimp) (("2" (inst + "x!3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (case-replace "nonzero_set?(LAMBDA (x: T): sq(i!1(x))) = nonzero_set?(i!1)") (("2" (hide-all-but 1) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "sq") (("2" (expand "nonzero_set?") (("2" (case-replace "i!1(x!1)=0") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "/=") (("2" (rewrite "sq_eq_0" 1 :dir rl) (("2" (expand "sq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (simple? const-decl "bool" measure_space nil) (S formal-const-decl "sigma_algebra" isf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (prod_measurable judgement-tcc nil measure_space nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sq const-decl "nonneg_real" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (finite_image judgement-tcc nil function_image_aux nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (TRUE const-decl "bool" booleans nil) (x!2 skolem-const-decl "({x: T | TRUE})" isf nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (finite_set type-eq-decl nil finite_sets nil) (fullset const-decl "set" sets nil) (i!1 skolem-const-decl "isf" isf nil) (image const-decl "set[R]" function_image nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (measurable_fullset name-judgement "measurable_set[T, S]" isf nil) (subset_algebra_fullset name-judgement "(S)" isf nil) (nonzero_set? const-decl "set[T]" isf nil) (sq_eq_0 formula-decl nil sq "reals/") (/= const-decl "boolean" notequal nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")) nil)) (isf_prod 0 (isf_prod-1 nil 3390785367 ("" (skosimp) (("" (lemma "isf_add" ("i1" "i1!1" "i2" "i2!1")) (("" (lemma "isf_diff" ("i1" "i1!1" "i2" "i2!1")) (("" (lemma "isf_sq" ("i" "(+[T])(i1!1, i2!1)")) (("" (lemma "isf_sq" ("i" "(-[T])(i1!1, i2!1)")) (("" (lemma "isf_diff" ("i1" "sq[T]((+[T])(i1!1, i2!1))" "i2" "sq[T]((-[T])(i1!1, i2!1))")) (("" (lemma "isf_scal" ("c" "1/4" "i" "(-[T])(sq[T]((+[T])(i1!1, i2!1)), sq[T]((-[T])(i1!1, i2!1)))")) (("" (case-replace "*[T] (1 / 4, (-[T]) (sq[T]((+[T])(i1!1, i2!1)), sq[T]((-[T])(i1!1, i2!1)))) = *[T](i1!1, i2!1)") (("" (hide-all-but 1) (("" (apply-extensionality :hide? t) (("" (expand "sq") (("" (expand "*") (("" (expand "-") (("" (expand "+") (("" (expand "sq") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (isf_add judgement-tcc nil isf nil) (isf_add application-judgement "isf" isf nil) (isf_sq judgement-tcc nil isf nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (isf_sq application-judgement "isf" isf nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (simple_times application-judgement "simple[T, S]" isf nil) (prod_measurable application-judgement "measurable_function[T, S]" isf nil) (isf_scal application-judgement "isf" isf nil) (real_plus_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (isf_scal judgement-tcc nil isf nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (isf_diff application-judgement "isf" isf nil) (isf_diff judgement-tcc nil isf nil)) nil)) (isf_phi 0 (isf_phi-1 nil 3390785367 ("" (skosimp) (("" (expand "isf?") (("" (typepred "E!1") (("" (expand "measurable_set?") (("" (rewrite "nonzero_set_phi") (("" (assert) (("" (lemma "phi_is_simple") (("" (inst - "E!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf? const-decl "bool" isf nil) (phi_is_simple judgement-tcc nil measure_space nil) (nonzero_set_phi formula-decl nil isf nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil isf nil) (set type-eq-decl nil 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 nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" isf nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" isf nil) (mu_fin? const-decl "bool" measure_props nil)) nil)) (isf_expt 0 (isf_expt-1 nil 3409636311 ("" (skolem + ("i!1" "_")) (("" (induct "pn") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case-replace "j!1=0") (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (typepred "i!1") (("1" (rewrite "eta") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "expt") (("2" (expand "expt" 2) (("2" (lemma "isf_prod" ("i1" "i!1" "i2" "LAMBDA (x: T): expt(i!1(x), j!1)")) (("1" (expand "*") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (T formal-type-decl nil isf nil) (isf? const-decl "bool" isf nil) (expt const-decl "[T -> real]" real_fun_power "power/") (isf nonempty-type-eq-decl nil isf nil) (nat_induction formula-decl nil naturalnumbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt_nat_measurable application-judgement "measurable_function[T, S]" isf nil) (simple_expt_nat application-judgement "simple[T, S]" isf nil) (= const-decl "[T, T -> boolean]" equalities nil) (expt def-decl "real" exponentiation nil) (NOT const-decl "[bool -> bool]" booleans nil) (eta formula-decl nil functions nil) (isf_prod judgement-tcc nil isf nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (isf_times_simple_is_isf 0 (isf_times_simple_is_isf-1 nil 3390785367 ("" (skosimp) (("" (typepred "i!1") (("" (typepred "h!1") (("" (expand "isf?") (("" (flatten) (("" (hide -1 -2) (("" (case "subset?(nonzero_set?(*[T](i!1, h!1)),nonzero_set?(i!1))") (("1" (lemma "m_monotone" ("a" "nonzero_set?(*[T](i!1, h!1))" "b" "nonzero_set?(i!1)")) (("1" (assert) (("1" (expand "mu_fin?") (("1" (expand "x_le") (("1" (replace -3) (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (prod_measurable application-judgement "measurable_function[T, S]" isf nil) (simple_times application-judgement "simple[T, S]" isf nil) (real_times_real_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil) (member const-decl "bool" sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (m formal-const-decl "measure_type" isf nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (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 nil) (measurable_set? const-decl "bool" measure_space_def nil) (m_monotone formula-decl nil measure_props nil) (mu_fin? const-decl "bool" measure_props nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (set type-eq-decl nil sets nil) (subset? const-decl "bool" sets nil) (nonzero_set? const-decl "set[T]" isf nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" isf nil) (simple? const-decl "bool" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil)) nil)) (isf_induction 0 (isf_induction-1 nil 3390968503 ("" (case "FORALL (P: pred[isf], i1: isf, n:nat): card[real](image[T,real](i1,nonzero_set?( (P(lambda x: 0) AND (FORALL c, E, i: P(i) IMPLIES P(c * phi(E) + i))) IMPLIES P(i1)") (("1" (skosimp) (("1" (inst - "P!1" "i1!1" "card[real](image[T,real](i1!1,nonzero_set?(i1!1)))") (("1" (assert) nil nil) ("2" (typepred "i1!1") (("2" (expand "isf?") (("2" (expand "simple?") (("2" (flatten) (("2" (lemma "finite_subset[real]" ("s" "image[T, real](i1!1, nonzero_set?(i1!1))" "A" "image(i1!1, fullset[T])")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide-all-but 1) (("2" (expand "nonzero_set?") (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (typepred "x!2") (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp*) (("1" (rewrite "card_empty?[real]") (("1" (case "empty?(nonzero_set?(i1!1))") (("1" (case-replace "i1!1=lambda x: 0") (("1" (apply-extensionality 1 :hide? t) (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (expand "nonzero_set?") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (inst - "i1!1(x!1)") (("2" (expand "nonzero_set?") (("2" (expand "image") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "P!1" "_") (("2" (replace -3) (("2" (replace -4 -1) (("2" (lemma "nonempty_card[real]" ("S" "image[T, real](i1!1, nonzero_set?(i1!1))")) (("2" (assert) (("2" (lemma "choose_rest[real]" ("a" "image[T, real](i1!1, nonzero_set?(i1!1))")) (("2" (lemma "choose_member[real]" ("a" "image[T, real](i1!1, nonzero_set?(i1!1))")) (("2" (name-replace "CC" "choose[real](image[T, real](i1!1, nonzero_set?(i1!1)))") (("2" (expand "nonempty?") (("2" (replace 1 *) (("2" (expand "member" -1) (("2" (copy -1) (("2" (expand "nonzero_set?" -1) (("2" (expand "image" -1) (("2" (skosimp) (("2" (typepred "x!1") (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (name "EE" "inverse_image[T,real](i1!1,singleton[real](CC))") (("2" (typepred "i1!1") (("2" (expand "isf?") (("2" (expand "simple?") (("2" (flatten) (("2" (expand "measurable_function?") (("2" (lemma "singleton_is_borel[real,metric_induced_topology]" ("x" "CC")) (("2" (inst - "singleton[real](CC)") (("2" (replace -5) (("2" (lemma "card_rest[real]" ("S" "image[T, real](i1!1, nonzero_set?(i1!1))")) (("2" (replace -10) (("2" (assert) (("2" (name "EEC" "difference(nonzero_set?(i1!1),EE)") (("2" (case "measurable_set?(EEC)") (("1" (case "subset?(EE,nonzero_set?(i1!1))") (("1" (case "mu_fin?(EE)") (("1" (case "mu_fin?(EEC)") (("1" (lemma "isf_phi" ("E" "EE")) (("1" (lemma "isf_phi" ("E" "EEC")) (("1" (lemma "isf_prod" ("i1" "phi(EEC)" "i2" "i1!1")) (("1" (lemma "isf_scal" ("c" "CC" "i" "phi(EE)")) (("1" (lemma "isf_add" ("i1" "*[T](CC, phi(EE))" "i2" "*[T](phi(EEC), i1!1)")) (("1" (lemma "extensionality" ("f" "i1!1" "g" "(+[T])(*[T](CC, phi(EE)), *[T](phi(EEC), i1!1))")) (("1" (expand "phi" -1 1) (("1" (expand "phi" -1 1) (("1" (expand "+" -1 1) (("1" (expand "*" -1 1) (("1" (expand "*" -1 2) (("1" (expand "member") (("1" (split -1) (("1" (inst -20 "*[T](phi(EEC), i1!1)") (("1" (split -20) (("1" (inst -23 "CC" "EE" "*[T](phi(EEC), i1!1)") (("1" (assert) nil nil)) nil) ("2" (case-replace "image[T, real] (*[T](phi(EEC), i1!1), nonzero_set?(*[T](phi(EEC), i1!1))) = rest[real](image[T, real] (("2" (hide 2 5 -21 -22) (("2" (expand "rest" 1) (("2" (reveal -6) (("2" (replace -1) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "remove") (("2" (expand "EEC") (("2" (expand "phi") (("2" (expand "*" 1) (("2" (expand "difference") (("2" (expand "member") (("2" (expand "nonzero_set?") (("2" (expand "image") (("2" (case-replace "x!2=CC") (("1" (assert) (("1" (skosimp*) (("1" (typepred "x!3") (("1" (case-replace "i1!1(x!3)=0") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "EE(x!3)") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "EE") (("2" (expand "singleton") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "EXISTS (x_1: ({x | i1!1(x) /= 0})): x!2 = i1!1(x_1)") (("1" (hide -3 -4 -5-6 -7 -8 -9 -10 -20 -21) (("1" (skosimp) (("1" (typepred "x!3") (("1" (inst + "x!3") (("1" (assert) (("1" (case-replace "EE(x!3)") (("1" (expand "EE") (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "EE") (("2" (expand "singleton") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 3) (("2" (assert) (("2" (hide -3 -4 -5 -6 -7 -8 -9 -10 -13 -14 -15 -17 -21 -22) (("2" (skosimp*) (("2" (hide -2 -8) (("2" (case-replace "EE(x!3)") (("1" (expand "EE") (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (typepred "x!3") (("1" (assert) (("1" (expand "EE") (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "EE") (("2" (expand "singleton") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (typepred "x!3") (("2" (expand "EE") (("2" (assert) (("2" (case-replace "i1!1(x!3)=0") (("1" (assert) nil nil) ("2" (assert) (("2" (inst + "x!3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (case-replace "EE(x!2)") (("1" (expand "EEC") (("1" (expand "nonzero_set?") (("1" (expand "difference") (("1" (expand "member") (("1" (assert) (("1" (hide-all-but (-1 1 2)) (("1" (expand "EE") (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "EEC") (("2" (expand "nonzero_set?") (("2" (expand "difference") (("2" (expand "member") (("2" (case-replace "i1!1(x!2) = 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (lemma "m_monotone" ("a" "EEC" "b" "nonzero_set?(i1!1)")) (("2" (split -1) (("1" (expand "x_le") (("1" (expand "mu_fin?") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "EEC") (("2" (rewrite "difference_subset") nil nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (lemma "m_monotone" ("a" "EE" "b" "nonzero_set?(i1!1)")) (("2" (assert) (("2" (expand "x_le") (("2" (expand "mu_fin?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -8 2)) (("2" (expand "nonzero_set?") (("2" (expand "EE") (("2" (hide -1) (("2" (expand "singleton") (("2" (expand "inverse_image") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -5 -6 1 -1)) (("2" (lemma "nonzero_measurable" ("g" "i1!1")) (("2" (expand "measurable_set?") (("2" (lemma "sigma_algebra_difference" ("x" "nonzero_set?(i1!1)" "y" "EE")) (("1" (assert) nil nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (rewrite "isf_zero") nil nil)) nil) ("4" (skosimp*) (("4" (typepred "i1!1") (("4" (expand "isf?") (("4" (expand "simple?") (("4" (flatten) (("4" (lemma "finite_subset[real]" ("s" "image[T, real](i1!1, nonzero_set?(i1!1))" "A" "image(i1!1, fullset[T])")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide-all-but 1) (("2" (expand "fullset") (("2" (expand "nonzero_set?") (("2" (expand "image") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (rewrite "isf_zero") nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (typepred "i1!1") (("4" (expand "isf?") (("4" (expand "simple?") (("4" (flatten) (("4" (lemma "finite_subset[real]" ("s" "image[T, real](i1!1, nonzero_set?(i1!1))" "A" "image(i1!1, fullset[T])")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide-all-but 1) (("2" (expand "fullset") (("2" (expand "nonzero_set?") (("2" (expand "image") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf_zero formula-decl nil isf nil) (nonempty_card formula-decl nil finite_sets nil) (choose_rest formula-decl nil sets_lemmas nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (measurable_function? const-decl "bool" measure_space_def nil) (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_compact application-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (borel nonempty-type-eq-decl nil borel nil) (borel? const-decl "sigma_algebra" borel nil) (card_rest formula-decl nil finite_sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (m_monotone formula-decl nil measure_props nil) (difference_subset formula-decl nil sets_lemmas nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (isf_phi judgement-tcc nil isf nil) (isf_prod judgement-tcc nil isf nil) (isf_add judgement-tcc nil isf nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (EE skolem-const-decl "set[T]" isf nil) (remove const-decl "set" sets nil) (x!3 skolem-const-decl "({x | i1!1(x) /= 0})" isf nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (real_times_real_is_real application-judgement "real" reals nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (rest const-decl "set" sets nil) (i1!1 skolem-const-decl "isf" isf nil) (EEC skolem-const-decl "set[T]" isf nil) (real_plus_real_is_real application-judgement "real" reals nil) (extensionality formula-decl nil functions nil) (isf_scal judgement-tcc nil isf nil) (nonzero_measurable formula-decl nil isf nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (sigma_algebra_difference formula-decl nil sigma_algebra nil) (difference const-decl "set" 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (singleton_is_borel formula-decl nil hausdorff_borel nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (inverse_image const-decl "set[D]" function_image nil) (choose_member formula-decl nil sets_lemmas nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (x!1 skolem-const-decl "T" isf nil) (i1!1 skolem-const-decl "isf" isf nil) (card_empty? formula-decl nil finite_sets nil) (nat_induction formula-decl nil naturalnumbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (simple? const-decl "bool" measure_space nil) (measurable_fullset name-judgement "measurable_set[T, S]" isf nil) (subset_algebra_fullset name-judgement "(S)" isf nil) (finite_subset formula-decl nil finite_sets nil) (fullset const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (TRUE const-decl "bool" booleans nil) (/= const-decl "boolean" notequal nil) (member const-decl "bool" sets nil) (i1!1 skolem-const-decl "isf" isf nil) (isf_phi application-judgement "isf" isf nil) (isf_scal application-judgement "isf" isf nil) (isf_add application-judgement "isf" isf nil) (T formal-type-decl nil isf 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) (isf? const-decl "bool" isf nil) (isf nonempty-type-eq-decl nil isf nil) (pred type-eq-decl nil defined_types 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 "[T, T -> boolean]" equalities 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) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (image const-decl "set[R]" function_image nil) (nonzero_set? const-decl "set[T]" isf nil) (AND const-decl "[bool, bool -> bool]" 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 nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" isf nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" isf nil) (mu_fin? const-decl "bool" measure_props nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (phi const-decl "nat" measure_space nil)) shostak)) (finite_partition_of?_TCC1 0 (finite_partition_of?_TCC1-1 nil 3395073229 ("" (skosimp) (("" (expand "nonempty?") (("" (propax) nil nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil)) nil)) (finite_partition_of?_TCC2 0 (finite_partition_of?_TCC2-1 nil 3395073229 ("" (skosimp*) (("" (expand "measurable_set?") (("" (propax) nil nil)) nil)) nil) ((measurable_set? const-decl "bool" measure_space_def nil)) nil)) (isf_def 0 (isf_def-1 nil 3395074092 ("" (skosimp) (("" (expand "isf?") (("" (split) (("1" (flatten) (("1" (rewrite "simple_def2") (("1" (skosimp) (("1" (inst + "P!1") (("1" (expand "finite_partition_of?") (("1" (skosimp) (("1" (typepred "E!1") (("1" (expand "every") (("1" (inst - "E!1") (("1" (inst - "E!1") (("1" (replace -2) (("1" (replace -3) (("1" (flatten) (("1" (lemma "m_monotone" ("a" "E!1" "b" "nonzero_set?(f!1)")) (("1" (split -1) (("1" (expand "mu_fin?") (("1" (expand "x_le") (("1" (replace -5) (("1" (replace 3) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (expand "nonzero_set?") (("2" (expand "constant_over?") (("2" (skosimp) (("2" (inst-cp - "choose(E!1)") (("2" (inst - "x!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) ("2" (skosimp*) (("2" (typepred "p!1") (("2" (case-replace "simple?(f!1)") (("1" (expand "finite_partition_of?") (("1" (name "PP" "{x: set[T] | S(x)& p!1(x) & nonempty?(x) & f!1(choose(x)) /= 0}") (("1" (case "forall (x:(PP)): S(x) & p!1(x)& nonempty?(x) & f!1(choose(x)) /= 0") (("1" (hide -2) (("1" (case "forall (p:setofsets[T],n:nat): subset?(p,PP) & card(p) = n => mu_fin?(Union(p)) (("1" (inst - "PP" "card(PP)") (("1" (split -1) (("1" (case-replace "Union(PP)=nonzero_set?(f!1)") (("1" (hide -1 2) (("1" (apply-extensionality :hide? t) (("1" (expand "nonzero_set?") (("1" (case-replace "f!1(x!1)=0") (("1" (assert) (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "PP") (("1" (flatten) (("1" (inst -9 "a!1") (("1" (flatten) (("1" (expand "constant_over?") (("1" (skosimp) (("1" (inst-cp -10 "x!1") (("1" (inst -10 "choose(a!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Union") (("2" (expand "finite_partition?") (("2" (expand "fullset") (("2" (expand "partition?") (("2" (flatten) (("2" (lemma "extensionality_postulate" ("f" "Union(p!1)" "g" "({x: T | TRUE})")) (("2" (replace -1 -4 rl) (("2" (hide -1) (("2" (inst -3 "x!1") (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (inst -7 "a!1") (("2" (flatten) (("2" (inst + "a!1") (("2" (expand "PP") (("2" (assert) (("2" (case-replace "nonempty?(a!1)") (("1" (assert) (("1" (expand "/=") (("1" (expand "constant_over?") (("1" (skosimp) (("1" (inst-cp -10 "x!1") (("1" (inst -10 "choose(a!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "x!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) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (expand "finite_partition?") (("2" (flatten) (("2" (lemma "finite_subset[set[T]]" ("s" "PP" "A" "p!1")) (("1" (assert) (("1" (expand "subset?") (("1" (skosimp) (("1" (expand "member") (("1" (inst - "x!1") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (rewrite "card_is_0[set[T]]") (("1" (replace -2) (("1" (lemma "Union_empty" ("A" "emptyset[set[T]]")) (("1" (expand "emptyset" -1 2) (("1" (expand "empty?" -1 2) (("1" (expand "member") (("1" (rewrite "emptyset_is_empty?" -1) (("1" (replace -1) (("1" (lemma "m_emptyset") (("1" (expand "mu_fin?") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "nonempty_card[set[T]]" ("S" "p!2")) (("2" (assert) (("2" (expand "nonempty?") (("2" (lemma "choose_rest[set[T]]" ("a" "p!2")) (("2" (assert) (("2" (lemma "card_rest[set[T]]" ("S" "p!2")) (("2" (assert) (("2" (replace -5) (("2" (assert) (("2" (inst - "rest(p!2)") (("2" (assert) (("2" (split -3) (("1" (case-replace "Union(p!2)=union(choose(p!2),Union(rest(p!2)))") (("1" (hide -1) (("1" (expand "subset?") (("1" (inst - "choose(p!2)") (("1" (assert) (("1" (inst - "choose(p!2)") (("1" (flatten) (("1" (inst - "choose(p!2)") (("1" (flatten) (("1" (replace 4) (("1" (replace 3) (("1" (lemma "m_union" ("a" "choose(p!2)" "b" "Union(rest(p!2))")) (("1" (expand "x_add") (("1" (expand "x_le") (("1" (expand "mu_fin?") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3 -1) (("2" (apply-extensionality 1 :hide? t) (("2" (case-replace "Union(p!2)(x!1)") (("1" (expand "union") (("1" (expand "member") (("1" (flatten) (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (replace -4 -1 rl) (("1" (expand "add") (("1" (expand "member") (("1" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (inst + "a!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (expand "union") (("2" (expand "member") (("2" (expand "Union") (("2" (split -1) (("1" (inst + "choose(p!2)") nil nil) ("2" (skosimp) (("2" (inst + "a!1") (("2" (typepred "a!1") (("2" (lemma "rest_subset" ("a" "p!2")) (("2" (expand "subset?") (("2" (inst - "a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (lemma "rest_subset" ("a" "p!2")) (("2" (expand "subset?") (("2" (inst - "x!1") (("2" (assert) (("2" (inst - "x!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) ("3" (skosimp) (("3" (hide 2) (("3" (rewrite "measurable_Union") (("3" (split) (("1" (skosimp) (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (assert) (("1" (inst - "x!1") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_countable[set[T]]" ("x" "p!2")) (("2" (expand "is_countable") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (lemma "finite_subset[set[T]]" ("s" "p!2" "A" "p!1")) (("1" (assert) (("1" (expand "subset?") (("1" (skosimp) (("1" (expand "member") (("1" (inst - "x!1") (("1" (assert) (("1" (inst - "x!1") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "finite_partition?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (lemma "measurable_Union" ("M" "p!2")) (("1" (expand "restrict") (("1" (expand "Union") (("1" (case-replace "{x: T | EXISTS (a: (LAMBDA (s: (S)): p!2(s))): a(x)}={x: T | EXISTS (a: (p!2)): a(x)}") (("1" (hide -1 2 3) (("1" (apply-extensionality 1 :hide? t) (("1" (case-replace "EXISTS (a: (p!2)): a(x!1)") (("1" (skosimp) (("1" (inst + "a!1") (("1" (typepred "a!1") (("1" (expand "subset?") (("1" (inst - "a!1") (("1" (assert) (("1" (inst - "a!1") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (inst + "a!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3) (("2" (expand "finite_partition?") (("2" (flatten) (("2" (expand "restrict") (("2" (case "is_countable[set[T]](p!2)") (("1" (expand "is_countable") (("1" (skosimp) (("1" (inst + "f!2") nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "finite_countable[set[T]]" ("x" "p!2")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (hide 2) (("4" (expand "finite_partition?") (("4" (flatten) (("4" (lemma "finite_subset[set[T]]" ("s" "p!2" "A" "p!1")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (inst - "x!1") (("2" (inst - "x!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "PP") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "simple_def2") (("2" (inst + "p!1") (("2" (expand "finite_partition_of?") (("2" (split) (("1" (expand "every") (("1" (skosimp) (("1" (inst - "x!1") (("1" (flatten) nil nil)) nil)) nil)) nil) ("2" (expand "every") (("2" (skosimp) (("2" (inst - "x!1") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf? const-decl "bool" isf nil) (simple? const-decl "bool" measure_space nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (x!1 skolem-const-decl "set[T]" isf nil) (injective? const-decl "bool" functions nil) (restrict_of_inj_is_inj application-judgement "(injective?[S, R])" restrict nil) (a!1 skolem-const-decl "(p!2)" isf nil) (p!2 skolem-const-decl "setofsets[T]" isf nil) (restrict const-decl "R" restrict nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (measurable_Union judgement-tcc nil measure_space_def nil) (finite_countable judgement-tcc nil countable_props "sets_aux/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (choose_rest formula-decl nil sets_lemmas nil) (card_rest formula-decl nil finite_sets nil) (rest const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (a!1 skolem-const-decl "(p!2)" isf nil) (a!1 skolem-const-decl "(rest(p!2))" isf nil) (rest_subset formula-decl nil sets_lemmas nil) (p!2 skolem-const-decl "setofsets[T]" isf nil) (m_union formula-decl nil measure_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (union const-decl "set" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nonempty_card formula-decl nil finite_sets nil) (m_emptyset formula-decl nil measure_props nil) (null_emptyset name-judgement "null_set" isf nil) (subset_algebra_emptyset name-judgement "(S)" isf nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (emptyset const-decl "set" sets nil) (Union_empty formula-decl nil sets_lemmas nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[finite_set[T]]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[set[T]]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (card_is_0 formula-decl nil finite_sets nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (PP skolem-const-decl "[set[T] -> boolean]" isf nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (real_minus_real_is_real application-judgement "real" reals nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (measurable_fullset name-judgement "measurable_set[T, S]" isf nil) (subset_algebra_fullset name-judgement "(S)" isf nil) (x!1 skolem-const-decl "T" isf nil) (a!1 skolem-const-decl "(PP)" isf nil) (p!1 skolem-const-decl "(finite_partition_of?(f!1))" isf nil) (a!1 skolem-const-decl "(p!1)" isf nil) (empty? const-decl "bool" sets nil) (TRUE const-decl "bool" booleans nil) (extensionality_postulate formula-decl nil functions nil) (partition? const-decl "bool" partitions nil) (x!1 skolem-const-decl "set[T]" isf nil) (finite_subset formula-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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Union const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (mu_fin? const-decl "bool" measure_props nil) (E!1 skolem-const-decl "(P!1)" isf nil) (x!1 skolem-const-decl "T" isf nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (constant_over? const-decl "bool" measure_space nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (m_monotone formula-decl nil measure_props nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (nonzero_set? const-decl "set[T]" isf 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/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" isf nil) (every const-decl "bool" sets nil) (f!1 skolem-const-decl "[T -> real]" isf nil) (P!1 skolem-const-decl "finite_partition[T]" isf nil) (finite_partition_of? const-decl "bool" isf nil) (finite_partition nonempty-type-eq-decl nil partitions nil) (fullset const-decl "set" sets nil) (finite_partition? const-decl "bool" partitions nil) (set type-eq-decl nil sets nil) (S formal-const-decl "sigma_algebra" isf nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil isf 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) (simple_def2 formula-decl nil measure_space nil)) shostak)) (isf_integral_TCC1 0 (isf_integral_TCC1-1 nil 3390789911 ("" (skosimp) (("" (typepred "i!1") (("" (expand "isf?") (("" (flatten) (("" (expand "simple?") (("" (flatten) (("" (lemma "finite_countable[real]" ("x" "image[T, real](i!1, fullset[T])")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_algebra_fullset name-judgement "(S)" isf nil) (measurable_fullset name-judgement "measurable_set[T, S]" isf nil) (finite_countable judgement-tcc nil countable_props "sets_aux/") (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (image const-decl "set[R]" function_image nil) (fullset const-decl "set" sets nil) (simple? const-decl "bool" measure_space nil)) nil)) (isf_integral_TCC2 0 (isf_integral_TCC2-1 nil 3390789911 ("" (skosimp*) (("" (typepred "i!1") (("" (split) (("1" (expand "isf?") (("1" (flatten) (("1" (expand "simple?") (("1" (flatten) (("1" (expand "measurable_function?") (("1" (lemma "singleton_is_borel[real,metric_induced_topology]" ("x" "c!1")) (("1" (inst - " singleton[real](c!1)") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "isf?") (("2" (flatten) (("2" (case "subset?(inverse_image[T, real](i!1, singleton[real](c!1)),nonzero_set?(i!1)) (("1" (lemma "m_monotone" ("a" "inverse_image[T, real](i!1, singleton[real](c!1))" "b" "nonzero_set?(i!1)")) (("1" (assert) (("1" (expand "x_le") (("1" (expand "mu_fin?") (("1" (replace -4) (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nonzero_set? const-decl "set[T]" isf nil) (inverse_image const-decl "set[D]" function_image nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (mu_fin? const-decl "bool" measure_props nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (m_monotone formula-decl nil measure_props nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (S formal-const-decl "sigma_algebra" isf nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" isf nil) (real_minus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (/= const-decl "boolean" notequal nil) (simple? const-decl "bool" measure_space nil) (measurable_function? const-decl "bool" measure_space_def nil) (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_compact application-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (borel nonempty-type-eq-decl nil borel nil) (borel? const-decl "sigma_algebra" borel nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (singleton_is_borel formula-decl nil hausdorff_borel nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets 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) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/")) nil)) (isf_integral_TCC3 0 (isf_integral_TCC3-1 nil 3390789911 ("" (skosimp) (("" (typepred "i!1") (("" (expand "convergent?") (("" (expand "isf?") (("" (expand "simple?") (("" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (simple? const-decl "bool" measure_space nil) (convergent? const-decl "bool" countable_convergence "sigma_set/")) nil)) (isf_integral_phi_TCC1 0 (isf_integral_phi_TCC1-1 nil 3390837470 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil isf nil) (set type-eq-decl nil 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 nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" isf nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" isf nil) (mu_fin? const-decl "bool" measure_props nil)) nil)) (isf_integral_phi 0 (isf_integral_phi-1 nil 3390842272 ("" (skosimp) (("" (expand "isf_integral") (("" (case "empty?(fullset[T])") (("1" (case-replace "image[T, real](phi(E!1), fullset[T]) = emptyset[real]") (("1" (rewrite "sigma_empty") (("1" (typepred "E!1") (("1" (rewrite "extensionality_postulate" -3 :dir rl) (("1" (expand "emptyset") (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "phi") (("1" (expand "member") (("1" (expand "empty?") (("1" (expand "member") (("1" (case-replace "E!1=emptyset[T]") (("1" (typepred "m") (("1" (expand "measure?") (("1" (flatten) (("1" (expand "emptyset") (("1" (expand "mu") (("1" (assert) (("1" (expand "measure_empty?") (("1" (expand "emptyset") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (inst -4 "1") (("2" (inst + "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "singleton") (("2" (expand "phi") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (rewrite "extensionality_postulate" -1 :dir rl) (("2" (expand "emptyset") (("2" (expand "fullset") (("2" (expand "image") (("2" (case "empty?(E!1)") (("1" (case-replace "c!1=1") (("1" (assert) (("1" (case-replace "{x_2: T | IF E!1(x_2) THEN 1 ELSE 0 ENDIF = 1}=E!1") (("1" (lemma "emptyset_is_empty?[T]") (("1" (inst - "E!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "{x_2: T | IF E!1(x_2) THEN 1 ELSE 0 ENDIF = c!1}=emptyset[T]") (("1" (expand "mu_fin?") (("1" (typepred "m") (("1" (expand "measure?") (("1" (flatten) (("1" (assert) (("1" (expand "measure_empty?") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -3 1 2 3)) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (lift-if -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "c!1=1") (("1" (case-replace "{x_2: T | IF E!1(x_2) THEN 1 ELSE 0 ENDIF = 1}=E!1") (("1" (assert) (("1" (typepred "E!1") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (lift-if 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case-replace "{x_2: T | IF E!1(x_2) THEN 1 ELSE 0 ENDIF = c!1}=emptyset[T]") (("1" (expand "mu_fin?") (("1" (typepred "m") (("1" (expand "measure?") (("1" (flatten) (("1" (assert) (("1" (expand "measure_empty?") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (lift-if -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (expand "fullset") (("2" (expand "image") (("2" (skosimp) (("2" (expand "phi") (("2" (expand "member") (("2" (expand "empty?") (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "E!1=emptyset[T]") (("1" (case-replace "image[T, real](phi(emptyset[T]), fullset[T]) = singleton[real](0)") (("1" (rewrite "sigma_singleton") (("1" (typepred "m") (("1" (expand "measure?") (("1" (flatten) (("1" (expand "mu") (("1" (assert) (("1" (expand "measure_empty?") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp) (("2" (expand "singleton") (("2" (expand "emptyset") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (case-replace "{x: T | 0 = c!1}=emptyset[T]") (("1" (expand "mu_fin?") (("1" (typepred "m") (("1" (expand "measure?") (("1" (flatten) (("1" (assert) (("1" (expand "measure_empty?") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 3) (("2" (expand "singleton") (("2" (expand "fullset") (("2" (expand "emptyset") (("2" (expand "phi") (("2" (expand "image") (("2" (apply-extensionality 1 :hide? t) (("2" (case-replace "x!1=0") (("1" (expand "empty?") (("1" (skosimp) (("1" (inst + "x!2") nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "E!1=fullset[T]") (("1" (case-replace "image[T, real](phi(fullset[T]), fullset[T]) = singleton[real](1)") (("1" (rewrite "sigma_singleton") (("1" (expand "singleton" 3) (("1" (expand "phi") (("1" (expand "member") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (case-replace "{x_1: T | IF fullset[T](x_1) THEN 1 ELSE 0 ENDIF = 1}=fullset[T]") (("1" (assert) nil nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (skosimp*) (("2" (expand "singleton") (("2" (expand "phi") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (expand "fullset") (("2" (case-replace "1=c!1") (("1" (assert) nil nil) ("2" (replace 1 3) (("2" (assert) (("2" (typepred "m") (("2" (expand "measure?") (("2" (flatten) (("2" (expand "mu_fin?") (("2" (expand "emptyset") (("2" (assert) (("2" (typepred "S") (("2" (expand "sigma_algebra?") (("2" (flatten) (("2" (expand "subset_algebra_empty?") (("2" (expand "emptyset") (("2" (expand "member") (("2" (replace -1) (("2" (assert) (("2" (expand "measure_empty?") (("2" (expand "emptyset") (("2" (replace -4) (("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) ("2" (hide-all-but (1 3)) (("2" (expand "singleton") (("2" (apply-extensionality :hide? t) (("2" (case-replace "x!1=1") (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "empty?") (("1" (skosimp) (("1" (inst + "x!2") (("1" (expand "phi") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "phi") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "image[T, real](phi(E!1), fullset[T]) = add[real](1,singleton[real](0))") (("1" (hide -1) (("1" (case "FORALL (c:real): NOT c = 0 IMPLIES measurable_set?(inverse_image[T, real](phi[T, S](E!1), singleton[real](c))) AND S(inv mu_fin?[T, S, m] (inverse_image[T, real](phi[T, S](E!1), singleton[real](c)))") (("1" (rewrite "sigma_add" 4) (("1" (expand "singleton" 4 1) (("1" (case-replace "inverse_image[T, real](phi(E!1), singleton[real](1)) = E!1") (("1" (hide -1) (("1" (rewrite "sigma_singleton") (("1" (assert) nil nil) ("2" (skosimp) (("2" (inst - "c!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "singleton") (("2" (expand "phi") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (lift-if 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "convergent_singleton" 1) (("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (inst - "c!1") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (inst - "c!1") (("3" (assert) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (lemma "finite_countable[real]" ("x" "singleton[real](0)")) (("4" (propax) nil nil)) nil)) nil) ("2" (hide 5) (("2" (skosimp) (("2" (case-replace "inverse_image[T, real] (phi[T, S](E!1), singleton[real](c!1)) = if c!1=1 then E!1 else emptyset[T] endif") (("1" (hide -1) (("1" (case-replace "c!1=1") (("1" (assert) (("1" (typepred "E!1") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "mu_fin?") (("2" (expand "measurable_set?") (("2" (typepred "m") (("2" (expand "measure?") (("2" (flatten) (("2" (assert) (("2" (expand "measure_empty?") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (expand "singleton") (("2" (expand "phi") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (case-replace "E!1(x!1)") (("1" (assert) (("1" (case-replace "c!1=1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 5) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "singleton") (("2" (expand "add") (("2" (expand "fullset") (("2" (expand "phi") (("2" (expand "member") (("2" (expand "image") (("2" (case-replace "x!1=0") (("1" (lemma "fullset_is_full?[T]") (("1" (inst - "E!1") (("1" (expand "fullset" -1) (("1" (replace -1 2 rl) (("1" (hide -1) (("1" (expand "full?") (("1" (skosimp) (("1" (expand "member") (("1" (inst + "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "x!1=1") (("1" (hide 1 3 5 -1) (("1" (rewrite "emptyset_is_empty?" 2 :dir rl) (("1" (expand "empty?") (("1" (skosimp) (("1" (inst + "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((isf_integral const-decl "real" isf nil) (FALSE const-decl "bool" booleans nil) (sigma_singleton formula-decl nil sigma_countable "sigma_set/") (phi_is_simple application-judgement "simple" isf nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (singleton_is_compact application-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" convergence_aux "metric_space/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[nat]" countability "sets_aux/") (add const-decl "(nonempty?)" sets nil) (nonempty? const-decl "bool" sets nil) (nonempty_add_finite application-judgement "non_empty_finite_set[nat]" countability "sets_aux/") (add_preserves_tightly_bounded application-judgement "(LAMBDA (S: set[nat]): tightly_bounded?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (add_preserves_least_bounded_above application-judgement "(LAMBDA (S: set[nat]): least_bounded_above?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (add_preserves_greatest_bounded_below application-judgement "(LAMBDA (S: set[nat]): greatest_bounded_below?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (add_preserves_has_greatest application-judgement "(LAMBDA (S: set[nat]): has_greatest?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (add_preserves_has_least application-judgement "(LAMBDA (S: set[nat]): has_least?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (nonempty_add_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (convergent_singleton formula-decl nil countable_convergence "sigma_set/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_add formula-decl nil sigma_countable "sigma_set/") (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (convergent? const-decl "bool" countable_convergence "sigma_set/") (fullset_is_full? formula-decl nil sets_lemmas nil) (full? const-decl "bool" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[posreal]" metric_continuity "metric_space/") (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (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[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[real]" measure_space nil) (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (image const-decl "set[R]" function_image 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) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" isf nil) (phi const-decl "nat" measure_space nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" isf nil) (mu_fin? const-decl "bool" measure_props nil) (emptyset const-decl "set" sets nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (member const-decl "bool" sets nil) (TRUE const-decl "bool" booleans nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (null_emptyset name-judgement "null_set" isf nil) (subset_algebra_emptyset name-judgement "(S)" isf nil) (extensionality_postulate formula-decl nil functions nil) (isf_phi application-judgement "isf" isf nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_empty formula-decl nil sigma_countable "sigma_set/") (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (mu const-decl "nnreal" measure_props nil) (inverse_image const-decl "set[D]" function_image nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (measurable_fullset name-judgement "measurable_set[T, S]" isf nil) (subset_algebra_fullset name-judgement "(S)" isf nil) (T formal-type-decl nil isf nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (empty? const-decl "bool" sets nil) (fullset const-decl "set" sets nil)) shostak)) (isf_integral_zero 0 (isf_integral_zero-1 nil 3390876205 ("" (expand "isf_integral") (("" (case "empty?(fullset[T])") (("1" (case-replace "image[T, real](LAMBDA (x: T): 0, fullset[T])=emptyset[real]") (("1" (rewrite "sigma_empty") (("1" (hide -1 2) (("1" (skosimp) (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (case-replace "{x: T | 0 = c!1}=emptyset[T]") (("1" (expand "mu_fin?") (("1" (typepred "m") (("1" (expand "measure?") (("1" (flatten) (("1" (assert) (("1" (expand "measure_empty?") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (expand "fullset") (("2" (expand "image") (("2" (skosimp) (("2" (expand "empty?") (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "image[T, real](LAMBDA (x: T): 0, fullset[T])=singleton[real](0)") (("1" (rewrite "sigma_singleton") (("1" (hide 3) (("1" (skosimp) (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (expand "mu_fin?") (("1" (typepred "m") (("1" (expand "measure?") (("1" (flatten) (("1" (case-replace "{x: T | 0 = c!1}=emptyset[T]") (("1" (assert) (("1" (expand "measure_empty?") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "singleton") (("2" (expand "fullset") (("2" (expand "image") (("2" (case-replace "x!1=0") (("1" (expand "empty?") (("1" (skosimp) (("1" (inst + "x!2") nil nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil isf nil) (subset_algebra_fullset name-judgement "(S)" isf nil) (measurable_fullset name-judgement "measurable_set[T, S]" isf nil) (TRUE const-decl "bool" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_empty formula-decl nil sigma_countable "sigma_set/") (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" isf nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_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/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" isf nil) (mu_fin? const-decl "bool" measure_props nil) (mu const-decl "nnreal" measure_props nil) (inverse_image const-decl "set[D]" function_image nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (subset_algebra_emptyset name-judgement "(S)" isf nil) (null_emptyset name-judgement "null_set" isf nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (member const-decl "bool" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (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[T]" sigma_countable "sigma_set/") (finite_emptyset name-judgement "finite_set[real]" measure_space nil) (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" convergence_aux "metric_space/") (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" convergence_aux "metric_space/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (image const-decl "set[R]" function_image nil) (emptyset const-decl "set" sets nil) (sigma_singleton formula-decl nil sigma_countable "sigma_set/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[nat]" countability "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)]" convergence_aux "metric_space/") (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (isf_integral const-decl "real" isf nil)) shostak)) (isf_integral_def_TCC1 0 (isf_integral_def_TCC1-1 nil 3394999213 ("" (skosimp*) (("" (expand "nonempty?") (("" (propax) nil nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil)) nil)) (isf_integral_def_TCC2 0 (isf_integral_def_TCC2-1 nil 3394999213 ("" (skosimp*) (("" (expand "finite_partition_of?") (("" (inst - "Y!1") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((finite_partition_of? const-decl "bool" isf nil) (T formal-type-decl nil isf nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (set type-eq-decl nil sets nil) (finite_partition? const-decl "bool" partitions nil) (fullset const-decl "set" sets nil) (finite_partition nonempty-type-eq-decl nil partitions nil) (p!1 skolem-const-decl "finite_partition[T]" isf nil) (Y!1 skolem-const-decl "set[T]" isf nil)) nil)) (isf_integral_def_TCC3 0 (isf_integral_def_TCC3-1 nil 3394999213 ("" (skosimp*) (("" (typepred "p!1") (("" (expand "fullset") (("" (expand "finite_partition?") (("" (flatten) (("" (hide-all-but (-2 1)) (("" (expand "is_countable") (("" (expand "is_finite") (("" (skosimp) (("" (inst + "f!2") (("" (expand "injective?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_partition nonempty-type-eq-decl nil partitions nil) (fullset const-decl "set" sets nil) (finite_partition? const-decl "bool" partitions nil) (set type-eq-decl nil sets nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (is_finite const-decl "bool" finite_sets 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) (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) (injective? const-decl "bool" functions nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (f!2 skolem-const-decl "[(p!1) -> below[N!1]]" isf nil) (N!1 skolem-const-decl "nat" isf nil) (p!1 skolem-const-decl "finite_partition[T]" isf nil) (is_countable const-decl "bool" countability "sets_aux/")) nil)) (isf_integral_def_TCC4 0 (isf_integral_def_TCC4-1 nil 3394999213 ("" (skosimp*) (("" (expand "convergent?") (("" (typepred "p!1") (("" (expand "fullset") (("" (expand "finite_partition?") (("" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((convergent? const-decl "bool" countable_convergence "sigma_set/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil isf nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (set type-eq-decl nil sets nil) (finite_partition? const-decl "bool" partitions nil) (fullset const-decl "set" sets nil) (finite_partition nonempty-type-eq-decl nil partitions nil)) nil)) (isf_integral_def 0 (isf_integral_def-1 nil 3407610741 ("" (assert) (("" (skolem + ("_" "p!1")) (("" (case "FORALL (n:nat,i: isf): finite_partition_of?(i)(p!1) & card({c | c /= 0 and image(i,fullset[T])(c)}) = n IMPLIE isf_integral(i) = sigma[set[T]] (p!1, LAMBDA Y: IF (NOT p!1(Y)) OR empty?(Y) OR i(choose[T](Y)) = 0 THEN 0 ELSE i(choose[T](Y)) * mu(Y) ENDIF)") (("1" (skosimp) (("1" (inst - "card({c | c /= 0 AND image(i!1, fullset[T])(c)})" "i!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "i!1") (("2" (expand "isf?") (("2" (expand "simple?") (("2" (flatten) (("2" (lemma "finite_subset[real]" ("s" "{c | c /= 0 AND image[T, real](i!1, fullset[T])(c)}" "A" "image(i!1, fullset[T])")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide-all-but 1) (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (lemma "card_is_0[real]" ("S" "{c | c /= 0 AND image(i!1, fullset[T])(c)}")) (("1" (assert) (("1" (replace -3) (("1" (expand "isf_integral") (("1" (case "nonempty?(image[T, real](i!1, fullset[T]))") (("1" (case-replace "image[T, real](i!1, fullset[T])=singleton[real](0)") (("1" (rewrite "sigma_singleton" 1) (("1" (case "forall x: i!1(x) = 0") (("1" (lemma "sigma_eq" ("X" "p!1" "f" "LAMBDA (Y:set[T]): IF (NOT p!1(Y)) OR empty?(Y) OR i!1(choose[T](Y)) = 0 THEN 0 ELSE i!1(choose[T](Y)) * mu(Y) ENDIF" "g" "lambda (Y:set[T]):0")) (("1" (split -1) (("1" (replace -1) (("1" (rewrite "sigma_zero" 1) nil nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (lift-if) (("2" (prop) (("2" (inst - "choose[T](t!1)") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "p!1") (("2" (expand "finite_partition?") (("2" (expand "convergent?") (("2" (flatten) nil nil)) nil)) nil)) nil) ("3" (typepred "p!1") (("3" (expand "convergent?") (("3" (expand "finite_partition?") (("3" (flatten) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (expand "finite_partition_of?") (("4" (inst -6 "Y!1") (("4" (flatten) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (expand "nonempty?") (("5" (propax) nil nil)) nil)) nil) ("6" (skosimp) (("6" (expand "nonempty?") (("6" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (lemma "extensionality_postulate" ("f" "image[T, real](i!1, fullset[T])" "g" "singleton[real](0)")) (("2" (replace -1 -2 rl) (("2" (inst - "i!1(x!1)") (("2" (expand "singleton") (("2" (replace -2 1 rl) (("2" (expand "fullset") (("2" (expand "image") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (case-replace "inverse_image[T, real](i!1, singleton[real](c!1))=emptyset[T]") (("1" (lemma "m_emptyset") (("1" (expand "mu_fin?") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (expand "singleton") (("2" (lemma "extensionality_postulate" ("f" "image[T, real](i!1, fullset[T])" "g" "{y: real | y = 0}")) (("2" (replace -1 -3 rl) (("2" (hide -1) (("2" (inst - "i!1(x!1)") (("2" (replace -1 * rl) (("2" (replace -2 1 rl) (("2" (expand "fullset") (("2" (expand "image") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "singleton") (("2" (case-replace "x!1=0") (("1" (hide -5) (("1" (lemma "extensionality_postulate" ("f" "{c | c /= 0 AND image(i!1, fullset[T])(c)}" "g" "emptyset[real]")) (("1" (replace -1 -4 rl) (("1" (hide -1) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp) (("1" (expand "member") (("1" (inst - "x!2") (("1" (replace -2) (("1" (expand "emptyset") (("1" (expand "image") (("1" (skosimp) (("1" (inst + "x!3") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "extensionality_postulate" ("f" "{c | c /= 0 AND image(i!1, fullset[T])(c)}" "g" "emptyset[real]")) (("2" (replace -1 -4 rl) (("2" (hide -1) (("2" (inst - "x!1") (("2" (assert) (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (hide -2 -4) (("2" (rewrite "emptyset_is_empty?") (("2" (replace -1) (("2" (rewrite "sigma_empty" 1) (("1" (lemma "extensionality_postulate[real,bool]" ("f" "image[T, real](i!1, fullset[T])" "g" "emptyset[real]")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (lemma "sigma_countable.sigma_eq" ("X" "p!1" "f" "LAMBDA (Y:set[T]): IF (NOT p!1(Y)) OR empty?(Y) OR i!1(choose[T](Y)) = 0 THEN 0 ELSE i!1(choose[T](Y)) * mu(Y) ENDIF" "g" "lambda(Y:set[T]):0")) (("1" (split -1) (("1" (replace -1) (("1" (rewrite "sigma_zero" 1) nil nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "t!1") (("2" (assert) (("2" (lift-if) (("2" (prop) (("2" (inst - "i!1(choose[T](t!1))") (("2" (expand "emptyset") (("2" (expand "fullset") (("2" (expand "image") (("2" (inst + "choose[T](t!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (typepred "p!1") (("2" (expand "finite_partition?") (("2" (flatten) nil nil)) nil)) nil)) nil) ("3" (typepred "p!1") (("3" (expand "finite_partition?") (("3" (expand "convergent?") (("3" (flatten) nil nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (expand "finite_partition_of?") (("4" (inst -3 "Y!1") (("4" (flatten) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (skosimp) (("5" (expand "nonempty?") (("5" (propax) nil nil)) nil)) nil) ("6" (skosimp) (("6" (expand "nonempty?") (("6" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (case-replace "inverse_image[T, real](i!1, singleton[real](c!1))=emptyset[T]") (("1" (lemma "m_emptyset") (("1" (expand "mu_fin?") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (expand "inverse_image") (("2" (expand "singleton") (("2" (expand "member") (("2" (lemma "extensionality_postulate" ("f" "image[T, real](i!1, fullset[T])" "g" "{x: real | FALSE}")) (("2" (replace -1 -3 rl) (("2" (inst - "c!1") (("2" (expand "fullset") (("2" (expand "image") (("2" (inst + "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "i!1") (("2" (expand "isf?") (("2" (expand "simple?") (("2" (flatten) (("2" (lemma "finite_subset[real]" ("s" "{c | c /= 0 AND image[T, real](i!1, fullset[T])(c)}" "A" "image(i!1, fullset[T])")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide-all-but 1) (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (name-replace "NZ_IMAGE" "{c | c /= 0 AND image(i!1, fullset[T])(c)}") (("2" (lemma "nonempty_card[real]" ("S" "NZ_IMAGE")) (("2" (assert) (("2" (lemma "card_rest[real]" ("S" "NZ_IMAGE")) (("2" (replace -5) (("2" (simplify -1) (("2" (lemma "choose_member[real]" ("a" "NZ_IMAGE")) (("2" (expand "nonempty?") (("2" (replace 1) (("2" (expand "NZ_IMAGE" -1 2) (("2" (expand "member" -1) (("2" (flatten) (("2" (name-replace "CC" "choose[real](NZ_IMAGE)") (("2" (name "P1" "{a:set[T] | p!1(a) & forall (x:(a)): i!1(x) = CC}") (("2" (case "subset?(P1,p!1)") (("1" (case "is_finite[set[T]](P1)") (("1" (lemma "measurable_Union" ("M" "P1")) (("1" (expand "restrict" -1) (("1" (expand "Union" -1) (("1" (name-replace "CC_SET" "{x: T | EXISTS (a: (LAMBDA (s: ((S))): P1(s))): a(x)}") (("1" (case "forall x: CC_SET(x) => i!1(x)=CC & exists (a:(P1)): a(x)") (("1" (name "II" "i!1-CC*phi(CC_SET)") (("1" (copy -3) (("1" (expand "measurable_set?" -1) (("1" (case "mu_fin?(CC_SET)") (("1" (lemma "isf_phi" ("E" "CC_SET")) (("1" (lemma "isf_scal" ("c" "CC" "i" "phi[T, S](CC_SET)")) (("1" (lemma "isf_diff" ("i1" "i!1" "i2" "*[T](CC, phi[T, S](CC_SET))")) (("1" (replace -6) (("1" (inst -14 "II") (("1" (case-replace "{c | c /= 0 AND image(II, fullset[T])(c)}=rest(NZ_IMAGE)") (("1" (replace -14) (("1" (hide -3 -14 -17) (("1" (hide -1) (("1" (case "finite_partition_of?(II)(p!1)") (("1" (replace -1) (("1" (case-replace "isf_integral(i!1) = isf_integral(II) + CC*mu(CC_SET)") (("1" (hide -1) (("1" (name-replace "LHS" "isf_integral(II)") (("1" (name "P2" "difference(p!1,P1)") (("1" (lemma "difference_subset" ("a" "p!1" "b" "P1")) (("1" (lemma "difference_disjoint" ("b" "p!1" "a" "P1")) (("1" (replace -3) (("1" (case "union(P1,P2)=p!1") (("1" (case "is_finite(P2)") (("1" (case "is_finite(p!1)") (("1" (lemma "sigma_disjoint_union" ("f" "LAMBDA Y: IF (NOT p!1(Y)) OR empty?(Y) OR i!1(choose[T](Y)) = 0 THEN 0 ELSE i!1(choose[T](Y)) * mu(Y) ENDIF" "X" "P1" "Y" "P2")) (("1" (replace -4) (("1" (replace -5) (("1" (replace -1 3) (("1" (hide -1) (("1" (lemma "sigma_eq" ("X" "P1" "f" "LAMBDA Y: IF (NOT p!1(Y)) OR empty?(Y) OR i!1(choose[T](Y)) = 0 THEN 0 ELSE i!1(choose[T](Y)) * mu(Y) ENDIF" "g" "LAMBDA Y: if not P1(Y) then 0 else CC*mu(Y) endif")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (case "forall (c:real,f:(convergent?(P1))): (forall (x:(P1)): f(x) = c*mu(x)) => sigma(P1, f) = c* (("1" (inst-cp - "CC" "LAMBDA Y: IF NOT P1(Y) THEN 0 ELSE CC * mu(Y) ENDIF") (("1" (split -2) (("1" (replace -1) (("1" (assert) (("1" (hide -1) (("1" (lemma "sigma_disjoint_union" ("X" "P1" "Y" "P2" "f" " LAMBDA Y: IF (NOT p!1(Y)) OR empty?(Y) OR II(choose[T](Y)) = 0 THEN 0 ELSE II(choose[T](Y)) * mu(Y) ENDIF")) (("1" (replace -6) (("1" (replace -5) (("1" (replace -1) (("1" (hide -1) (("1" (inst - "0" "LAMBDA Y: IF (NOT p!1(Y)) OR empty?(Y) OR II(choose[T](Y)) = 0 THEN 0 ELSE II(choose[T](Y)) * mu(Y) ENDIF") (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (replace -19) (("1" (hide -19) (("1" (lemma "sigma_eq" ("X" "P2" "f" "LAMBDA Y: IF (NOT p!1(Y)) OR empty?(Y) OR II(choose[T](Y)) = 0 THEN 0 ELSE II(choose[T](Y)) * mu(Y) ENDIF" "g" "LAMBDA Y: IF (NOT p!1(Y)) OR empty?(Y) OR i!1(choose[T](Y)) = 0 THEN 0 ELSE i!1(choose[T](Y)) * mu(Y) ENDIF")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 4) (("2" (skosimp) (("2" (typepred "t!1") (("2" (expand "subset?" -6) (("2" (inst - "t!1") (("2" (assert) (("2" (assert) (("2" (case-replace "empty?(t!1)") (("2" (assert) (("2" (case-replace "i!1(choose[T](t!1)) = 0") (("1" (expand "II" 2) (("1" (expand "-" 2) (("1" (replace -1) (("1" (expand "*" 2) (("1" (expand "phi") (("1" (expand "member") (("1" (case-replace "CC_SET(choose[T](t!1))") (("1" (inst -16 "choose[T](t!1)") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (expand "II" 3) (("2" (expand "-" 3) (("2" (expand "*" 3) (("2" (expand "P2" -1) (("2" (expand "difference" -1) (("2" (expand "member") (("2" (expand "phi" 4) (("2" (expand "member") (("2" (case-replace "CC_SET(choose[T](t!1))") (("1" (inst -14 "choose[T](t!1)") (("1" (assert) (("1" (flatten) (("1" (skosimp) (("1" (expand "P1" 3) (("1" (skosimp) (("1" (typepred "x!1") (("1" (typepred "t!1") (("1" (expand "finite_partition_of?" -23) (("1" (inst -23 "t!1") (("1" (flatten) (("1" (assert) (("1" (expand "constant_over?") (("1" (skosimp) (("1" (inst-cp -24 "choose[T](t!1)") (("1" (inst -24 "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (replace 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "nonempty?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (propax) nil nil)) nil) ("3" (expand "convergent?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide -19 4) (("2" (typepred "x!1") (("2" (expand "subset?" -17) (("2" (inst -17 "x!1") (("2" (assert) (("2" (assert) (("2" (case-replace "empty?(x!1)") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "II(choose[T](x!1)) = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (hide 3) (("2" (expand "II" 1) (("2" (expand "-" 1) (("2" (expand "*" 1) (("2" (expand "phi") (("2" (expand "member") (("2" (case-replace "CC_SET(choose[T](x!1))") (("1" (inst -15 "choose[T](x!1)") (("1" (assert) nil nil)) nil) ("2" (replace 1 2) (("2" (typepred "p!1") (("2" (expand "finite_partition?") (("2" (expand "partition?") (("2" (flatten) (("2" (lemma "extensionality_postulate" ("f" "Union(p!1)" "g" "fullset[T]")) (("2" (replace -1 -2 rl) (("2" (hide -1) (("2" (expand "CC_SET" 1) (("2" (inst + "x!1") (("1" (assert) nil nil) ("2" (expand "finite_partition_of?" -22) (("2" (inst -22 "x!1") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "nonempty?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (propax) nil nil)) nil) ("3" (skosimp) (("3" (expand "finite_partition_of?" -8) (("3" (inst -8 "Y!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (expand "nonempty?") (("4" (propax) nil nil)) nil)) nil) ("5" (skosimp) (("5" (expand "nonempty?") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4) (("2" (expand "convergent?") (("2" (propax) nil nil)) nil)) nil) ("3" (skosimp) (("3" (expand "finite_partition_of?" -9) (("3" (inst -9 "Y!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (skosimp) (("4" (expand "nonempty?") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (flatten) nil nil)) nil) ("3" (hide 4 -19) (("3" (skosimp) (("3" (expand "subset?" -17) (("3" (inst -17 "Y!1") (("3" (expand "member") (("3" (assert) (("3" (expand "finite_partition_of?" -20) (("3" (inst -20 "Y!1") (("3" (flatten) (("3" (assert) (("3" (expand "P1" -1) (("3" (split -22) (("1" (rewrite "emptyset_is_empty?") (("1" (replace -1) (("1" (expand "mu_fin?") (("1" (rewrite "m_emptyset") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "choose(Y!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4 -19) (("2" (hide-all-but (1 2 3 -19 -18 -16 -15 -14 -11 -1)) (("2" (skosimp) (("2" (case "forall (n:nat,X:setofsets[T]): subset?(X,P1) & card(X)=n => sigma(X,f!1)=c!1*mu(Un (("1" (inst - "card(P1)" "P1") (("1" (split -1) (("1" (case-replace "Union(P1)=CC_SET") (("1" (hide -1 2) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "CC_SET") (("1" (case-replace "Union(P1)(x!1)") (("1" (expand "Union" -1) (("1" (skosimp) (("1" (inst + "a!1") (("1" (expand "subset?") (("1" (inst -7 "a!1") (("1" (expand "member") (("1" (expand "finite_partition_of?") (("1" (inst -9 "a!1") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "Union") (("2" (inst + "a!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil) ("2" (induct "n") (("1" (skosimp) (("1" (lemma "card_is_0" ("S" "X!1")) (("1" (assert) (("1" (replace -3) (("1" (replace -1) (("1" (rewrite "Union_emptyset_rew") (("1" (rewrite "sigma_empty") (("1" (expand "mu") (("1" (rewrite "m_emptyset") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 2) (("2" (lemma "nonempty_card" ("S" "X!1")) (("2" (assert) (("2" (rewrite "sigma_choose_rest" 1) --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.704Bemerkung: (vorverarbeitet am 2026-05-06) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26