| products/Sources/formale Sprachen/PVS/vect_analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: deriv_real_vect.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(probability_space
(zero_TCC1 0 (zero_TCC1-1 nil 3424623523 ("" (lemma "constant_is_measurable") (("" (inst - "(LAMBDA t: 0)") (("" (expand "constant?") (("" (expand "const_fun") (("" (assert) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) 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) (constant? const-decl "bool" const_fun_def "structures/") (const_fun const-decl "[S -> T]" const_fun_def "structures/") (constant_is_measurable judgement-tcc nil measure_space_def "measure_integration/") (T formal-nonempty-type-decl nil probability_space 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) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil)) nil)) (one_TCC1 0 (one_TCC1-1 nil 3424623523 ("" (lemma "constant_is_measurable") (("" (inst - "(LAMBDA t: 1)") (("" (expand "constant?") (("" (expand "const_fun") (("" (inst?) nil nil)) nil)) nil)) nil)) 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) (constant? const-decl "bool" const_fun_def "structures/") (const_fun const-decl "[S -> T]" const_fun_def "structures/") (constant_is_measurable judgement-tcc nil measure_space_def "measure_integration/") (T formal-nonempty-type-decl nil probability_space 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) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil)) nil)) (lesseqp_TCC1 0 (lesseqp_TCC1-1 nil 3314025598 ("" (skosimp) (("" (typepred "X!1") (("" (lemma "measurable_le" ("f" "X!1")) (("" (assert) (("" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil) ((random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil probability_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (measurable_le formula-decl nil measure_space_def "measure_integration/")) shostak)) (lessp_TCC1 0 (lessp_TCC1-1 nil 3314191251 ("" (skosimp) (("" (typepred "X!1") (("" (lemma "measurable_gt" ("f" "X!1")) (("" (assert) (("" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil) ((random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil probability_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (measurable_gt formula-decl nil measure_space_def "measure_integration/")) shostak)) (equal_TCC1 0 (equal_TCC1-1 nil 3314190689 ("" (skosimp) (("" (typepred "X!1") (("" (lemma "measurable_ge" ("f" "X!1")) (("" (lemma "measurable_le" ("f" "X!1")) (("" (assert) (("" (inst - "x!1") (("" (inst - "x!1") (("" (lemma "measurable_intersection" ("a" "{z: T | X!1(z) <= x!1}" "b" "{z: T | X!1(z) >= x!1}")) (("1" (case-replace "(intersection[T] ({z: T | X!1(z) <= x!1}, {z: T | X!1(z) >= x!1}))={t | X!1(t) = x!1}") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil probability_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (measurable_le formula-decl nil measure_space_def "measure_integration/") (>= const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (set type-eq-decl nil sets nil) (measurable_intersection judgement-tcc nil measure_space_def "measure_integration/") (real_minus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (intersection const-decl "set" sets nil) (measurable_ge formula-decl nil measure_space_def "measure_integration/")) shostak)) (lessp_TCC2 0 (lessp_TCC2-1 nil 3314191439 ("" (skosimp) (("" (typepred "X!1") (("" (lemma "measurable_lt" ("f" "X!1")) (("" (assert) (("" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil) ((random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil probability_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (measurable_lt formula-decl nil measure_space_def "measure_integration/")) shostak)) (lesseqp_TCC2 0 (lesseqp_TCC2-1 nil 3314190689 ("" (skosimp) (("" (typepred "X!1") (("" (lemma "measurable_ge" ("f" "X!1")) (("" (assert) (("" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil) ((random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil probability_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (measurable_ge formula-decl nil measure_space_def "measure_integration/")) shostak)) (notequal_TCC1 0 (notequal_TCC1-1 nil 3314191820 ("" (skosimp) (("" (typepred "X!1") (("" (lemma "measurable_gt" ("f" "X!1")) (("" (lemma "measurable_lt" ("f" "X!1")) (("" (assert) (("" (inst - "x!1") (("" (inst - "x!1") (("" (lemma "measurable_union" ("a" "{z: T | X!1(z) < x!1}" "b" "{z: T | X!1(z) > x!1}")) (("1" (case-replace "(union[T] ({z: T | X!1(z) < x!1}, {z: T | X!1(z) > x!1}))={t | X!1(t) /= x!1}") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil) ("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil probability_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (measurable_lt formula-decl nil measure_space_def "measure_integration/") (> const-decl "bool" reals nil) (< const-decl "bool" reals nil) (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (set type-eq-decl nil sets nil) (measurable_union judgement-tcc nil measure_space_def "measure_integration/") (real_minus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (union const-decl "set" sets nil) (/= const-decl "boolean" notequal nil) (measurable_gt formula-decl nil measure_space_def "measure_integration/")) shostak)) (complement_le1 0 (complement_le1-1 nil 3321716438 ("" (skosimp) (("" (expand "<=") (("" (expand "<") (("" (expand "complement") (("" (expand "member") (("" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "(S)" probability_space nil) (complement const-decl "set" sets nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (> const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (member const-decl "bool" sets nil) (< const-decl "(S)" probability_space nil)) shostak)) (complement_lt1 0 (complement_lt1-1 nil 3321716510 ("" (skosimp) (("" (expand "<=") (("" (expand "<") (("" (expand "complement") (("" (expand "member") (("" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "(S)" probability_space nil) (complement const-decl "set" sets nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (member const-decl "bool" sets nil) (< const-decl "(S)" probability_space nil)) shostak)) (complement_eq 0 (complement_eq-1 nil 3321716535 ("" (skosimp) (("" (expand "=") (("" (expand "/=") (("" (expand "complement") (("" (expand "member") (("" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "(S)" probability_space nil) (complement const-decl "set" sets nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities 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) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (member const-decl "bool" sets nil) (/= const-decl "(S)" probability_space nil)) shostak)) (complement_lt2 0 (complement_lt2-1 nil 3321716558 ("" (skosimp) (("" (expand "<") (("" (expand "<=") (("" (expand "complement") (("" (expand "member") (("" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil) ((< const-decl "(S)" probability_space nil) (complement const-decl "set" sets nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (< const-decl "bool" reals nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (>= const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (member const-decl "bool" sets nil) (<= const-decl "(S)" probability_space nil)) shostak)) (complement_le2 0 (complement_le2-1 nil 3321716586 ("" (skosimp) (("" (expand "<=") (("" (expand "<") (("" (expand "complement") (("" (apply-extensionality :hide? t) (("" (expand "member") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "(S)" probability_space nil) (complement const-decl "set" sets nil) (T formal-nonempty-type-decl nil probability_space nil) (boolean nonempty-type-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "(S)" probability_space nil)) shostak)) (complement_ne 0 (complement_ne-1 nil 3321716617 ("" (skosimp) (("" (expand "=") (("" (expand "/=") (("" (expand "complement") (("" (expand "member") (("" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "(S)" probability_space nil) (complement const-decl "set" sets nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (/= const-decl "boolean" notequal 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) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (member const-decl "bool" sets nil) (/= const-decl "(S)" probability_space nil)) shostak)) (plus_TCC1 0 (plus_TCC1-1 nil 3322049026 ("" (skosimp) (("" (lemma "sum_measurable" ("g1" "X!1" "g2" "lambda (t:T): x!1")) (("1" (expand "+") (("1" (propax) nil nil)) nil) ("2" (lemma "constant_is_measurable") (("2" (inst - "(LAMBDA (t: T): x!1)") (("2" (expand "constant?") (("2" (expand "const_fun") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (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) (sum_measurable judgement-tcc nil measure_space_def "measure_integration/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (constant? const-decl "bool" const_fun_def "structures/") (x!1 skolem-const-decl "real" probability_space nil) (const_fun const-decl "[S -> T]" const_fun_def "structures/") (constant_is_measurable judgement-tcc nil measure_space_def "measure_integration/")) shostak)) (plus_TCC2 0 (plus_TCC2-1 nil 3351240565 ("" (skosimp) (("" (lemma "sum_measurable" ("g1" "lambda (t:T): x!1" "g2" "X!1")) (("1" (expand "+") (("1" (assert) nil nil)) nil) ("2" (lemma "constant_is_measurable") (("2" (inst - "(LAMBDA (t: T): x!1)") (("2" (expand "constant?") (("2" (expand "const_fun") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (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) (sum_measurable judgement-tcc nil measure_space_def "measure_integration/") (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (constant? const-decl "bool" const_fun_def "structures/") (x!1 skolem-const-decl "real" probability_space nil) (const_fun const-decl "[S -> T]" const_fun_def "structures/") (constant_is_measurable judgement-tcc nil measure_space_def "measure_integration/")) nil)) (difference_TCC1 0 (difference_TCC1-1 nil 3351275929 ("" (skosimp) (("" (lemma "constant_is_measurable") (("" (inst - "lambda t: x!1") (("1" (lemma "diff_measurable" ("g1" "X!1" "g2" "LAMBDA t: x!1")) (("1" (expand "-" -1) (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (expand "constant?") (("2" (expand "const_fun") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (constant_is_measurable judgement-tcc nil measure_space_def "measure_integration/") (const_fun const-decl "[S -> T]" const_fun_def "structures/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (diff_measurable judgement-tcc nil measure_space_def "measure_integration/") (- const-decl "[T -> real]" real_fun_ops "reals/") (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) (constant? const-decl "bool" const_fun_def "structures/") (x!1 skolem-const-decl "real" probability_space nil)) nil)) (difference_TCC2 0 (difference_TCC2-1 nil 3351920614 ("" (skosimp) (("" (lemma "constant_is_measurable") (("" (inst - "lambda t: x!1") (("1" (lemma "diff_measurable" ("g2" "X!1" "g1" "LAMBDA t: x!1")) (("1" (expand "-" -1) (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (expand "constant?") (("2" (expand "const_fun") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (constant_is_measurable judgement-tcc nil measure_space_def "measure_integration/") (const_fun const-decl "[S -> T]" const_fun_def "structures/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (diff_measurable judgement-tcc nil measure_space_def "measure_integration/") (- const-decl "[T -> real]" real_fun_ops "reals/") (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) (constant? const-decl "bool" const_fun_def "structures/") (x!1 skolem-const-decl "real" probability_space nil)) nil)) (divide_TCC1 0 (divide_TCC1-1 nil 3351920614 ("" (skosimp) (("" (lemma "scal_measurable" ("c" "1/n0z!1" "g" "X!1")) (("" (expand "*") (("" (assert) nil nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (nzreal nonempty-type-eq-decl nil 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) (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) (scal_measurable judgement-tcc nil measure_space_def "measure_integration/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (independent?_TCC1 0 (independent?_TCC1-1 nil 3509255376 ("" (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-nonempty-type-decl nil probability_space 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) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure 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 "measure_integration/") (borel nonempty-type-eq-decl nil borel "measure_integration/") (Intersection const-decl "set" sets nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def "measure_integration/") (open? const-decl "bool" topology "topology/") (metric_open? const-decl "bool" metric_space_def "metric_space/") (subset? const-decl "bool" sets nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (sigma_algebra_union? const-decl "bool" subset_algebra_def "measure_integration/") (is_countable const-decl "bool" countability "sets_aux/") (subset_algebra_complement? const-decl "bool" subset_algebra_def "measure_integration/") (subset_algebra_empty? const-decl "bool" subset_algebra_def "measure_integration/") (member const-decl "bool" sets nil) (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas_aux "measure_integration/") (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[real]" measure_space "measure_integration/") (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/") (subset_algebra_emptyset name-judgement "(borel?)" real_borel "measure_integration/") (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (borel_independence 0 (borel_independence-1 nil 3509204782 ("" (skosimp) (("" (typepred "X!1") (("" (typepred "Y!1") (("" (typepred "g!1") (("" (typepred "h!1") (("" (expand "independent?") (("" (skosimp) (("" (expand "borel_function?") (("" (expand "measurable_function?") (("" (inst -3 "B2!1") (("" (inst -4 "B1!1") (("" (inst -1 "B2!1") (("" (inst -2 "B1!1") (("" (inst -5 "inverse_image(g!1, B1!1)" "inverse_image(h!1, B2!1)") (("" (case-replace "inverse_image(X!1, inverse_image(g!1, B1!1))=inverse_image(g!1 o X!1, B1!1)") (("1" (case-replace "inverse_image(Y!1, inverse_image(h!1, B2!1))=inverse_image(h!1 o Y!1, B2!1)") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (expand "inverse_image") (("1" (expand "o ") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "o ") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil probability_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (borel_function type-eq-decl nil borel_functions "measure_integration/") (borel_function? const-decl "bool" borel_functions "measure_integration/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (independent? const-decl "bool" probability_space nil) (borel nonempty-type-eq-decl nil borel "measure_integration/") (borel? const-decl "sigma_algebra" borel "measure_integration/") (set type-eq-decl nil sets nil) (inverse_image const-decl "set[D]" function_image nil) (g!1 skolem-const-decl "borel_function[real, metric_induced_topology, real, metric_induced_topology]" probability_space nil) (B1!1 skolem-const-decl "borel[real, metric_induced_topology]" probability_space nil) (h!1 skolem-const-decl "borel_function[real, metric_induced_topology, real, metric_induced_topology]" probability_space nil) (B2!1 skolem-const-decl "borel[real, metric_induced_topology]" probability_space nil) (member const-decl "bool" sets nil) (borel_comp_measurable_is_measurable application-judgement "measurable_function[T, S]" probability_space nil) (= const-decl "[T, T -> boolean]" equalities nil) (O const-decl "T3" function_props nil)) shostak)) (partial_sum_is_random_variable_TCC1 0 (partial_sum_is_random_variable_TCC1-1 nil 3391354647 ("" (subtype-tcc) nil nil) nil nil)) (partial_sum_is_random_variable 0 (partial_sum_is_random_variable-1 nil 3352017383 ("" (induct "n1") (("1" (expand "sigma") (("1" (skosimp) (("1" (typepred "XS!1(0)") (("1" (expand "random_variable?") (("1" (expand "sigma") (("1" (case-replace "(LAMBDA t: XS!1(0)(t))=XS!1(0)") (("1" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "XS!1") (("2" (expand "sigma" 1) (("2" (typepred "XS!1(1 + j!1)") (("2" (expand "random_variable?") (("2" (lemma "sum_measurable" ("g1" "XS!1(1 + j!1)" "g2" "LAMBDA t: sigma(0, j!1, LAMBDA n: XS!1(n)(t))")) (("1" (expand "+") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[T -> real]" real_fun_ops "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (measurable_function nonempty-type-eq-decl nil measure_space_def "measure_integration/") (sum_measurable judgement-tcc nil measure_space_def "measure_integration/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_plus_real_is_real application-judgement "real" reals nil) (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (random_variable? const-decl "bool" probability_measure nil) (random_variable nonempty-type-eq-decl nil probability_measure nil) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-nonempty-type-decl nil probability_space 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)) shostak)) (distribution_function_TCC1 0 (distribution_function_TCC1-1 nil 3321775180 ("" (expand "distribution_function?") (("" (inst + "lambda (t:T): 0") (("1" (skosimp) (("1" (expand "<=") (("1" (case-replace "0 <= x!1") (("1" (lemma "P_fullset" ("P" "P")) (("1" (expand "fullset") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "P_emptyset" ("P" "P")) (("2" (expand "emptyset") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "constant_is_measurable") (("2" (inst - "LAMBDA (t: T): 0") (("2" (expand "constant?") (("2" (expand "const_fun") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((measurable_function? const-decl "bool" measure_space_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (T formal-nonempty-type-decl nil probability_space nil) (random_variable nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "(S)" probability_space nil) (P_emptyset formula-decl nil probability_measure nil) (emptyset const-decl "set" sets nil) (P formal-const-decl "probability_measure" probability_space nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (P_fullset formula-decl nil probability_measure nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (fullset const-decl "set" sets nil) (<= const-decl "bool" reals nil) (constant? const-decl "bool" const_fun_def "structures/") (const_fun const-decl "[S -> T]" const_fun_def "structures/") (constant_is_measurable judgement-tcc nil measure_space_def "measure_integration/") (distribution_function? const-decl "bool" probability_space nil)) shostak)) (invert_distribution 0 (invert_distribution-1 nil 3352018678 ("" (skosimp) (("" (expand "<") (("" (expand "distribution_function") (("" (expand "<=") (("" (lemma "P_complement" ("A" "{t | X!1(t) > x!1}")) (("1" (inst - "P") (("1" (expand ">") (("1" (lemma "complement_lt1" ("x" "x!1" "X" "X!1")) (("1" (expand "<" -1) (("1" (expand ">" -1) (("1" (replace -1 -2) (("1" (expand "<=" -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "x!1 (("2" (expand "<") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((< const-decl "(S)" probability_space nil) (<= const-decl "(S)" probability_space nil) (NOT const-decl "[bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" probability_space nil) (complement_lt1 formula-decl nil probability_space nil) (real_minus_real_is_real application-judgement "real" reals nil) (P_complement formula-decl nil probability_measure 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) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (T formal-nonempty-type-decl nil probability_space 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) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (distribution_function const-decl "probability" probability_space nil)) shostak)) (interval_distribution 0 (interval_distribution-1 nil 3352019023 ("" (skosimp*) (("" (assert) (("" (expand "distribution_function") (("" (skosimp) (("" (lemma "P_intersection" ("A" "x!1 < X!1" "B" "X!1 <= y!1")) (("" (inst - "P") (("" (replace -1 1) (("" (hide -1) (("" (assert) (("" (case-replace "union(x!1 < X!1, X!1 <= y!1) = fullset[T]") (("1" (hide -1) (("1" (lemma "P_fullset") (("1" (inst - "P") (("1" (replace -1) (("1" (lemma "P_complement" ("A" "x!1 < X!1")) (("1" (inst - "P") (("1" (rewrite "complement_lt1" -1) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "fullset") (("2" (expand "union") (("2" (expand "member") (("2" (expand "<") (("2" (expand "<=" 1) (("2" (expand ">" 1) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (subset_algebra_intersection application-judgement "(S)" probability_space nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (P formal-const-decl "probability_measure" probability_space nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (fullset const-decl "set" sets nil) (union const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (P_fullset formula-decl nil probability_measure nil) (subset_algebra_fullset name-judgement "(S)" probability_space nil) (measurable_fullset name-judgement "measurable_set[T, S]" probability_space nil) (real_times_real_is_real application-judgement "real" reals nil) (complement_lt1 formula-decl nil probability_space nil) (P_complement formula-decl nil probability_measure nil) (> const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (subset_algebra_union application-judgement "(S)" probability_space nil) (P_intersection formula-decl nil probability_measure 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) (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (< const-decl "(S)" probability_space nil) (<= const-decl "(S)" probability_space nil) (T formal-nonempty-type-decl nil probability_space 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) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" probability_space nil) (distribution_function const-decl "probability" probability_space nil)) shostak)) (limit_distribution_TCC1 0 (limit_distribution_TCC1-1 nil 3425001876 ("" (skosimp) (("" (expand "distribution_function") (("" (replace -1) (("" (assert) (("" (hide -1) (("" (lemma "m_increasing_convergence") (("" (inst - "lambda (n:nat): X!1 <= x!1 - 1 / (1 + n)") (("1" (split -1) (("1" (expand "x_converges?") (("1" (expand "to_measure") (("1" (expand "o") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "increasing?") (("2" (skosimp) (("2" (expand "subset?") (("2" (expand "<=" 1) (("2" (expand "member") (("2" (skosimp) (("2" (lemma "both_sides_div_pos_le2" ("py" "x!2+1" "px" "y!1+1" "pz" "1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((distribution_function const-decl "probability" probability_space nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (P formal-const-decl "probability_measure" probability_space nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (to_measure const-decl "measure_type" generalized_measure_def "measure_integration/") (measure_type nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (measure? const-decl "bool" generalized_measure_def "measure_integration/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (finite_measure nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (finite_measure? const-decl "bool" generalized_measure_def "measure_integration/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra" probability_space nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil probability_space nil) (m_increasing_convergence formula-decl nil measure_props "measure_integration/") (O const-decl "T3" function_props nil) (x_converges? const-decl "bool" extended_nnreal "extended_nnreal/") (increasing? const-decl "bool" fun_preds_partial "structures/") (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (both_sides_div_pos_le2 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sequence type-eq-decl nil sequences nil) (measurable_set nonempty-type-eq-decl nil measure_space_def "measure_integration/") (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) (set type-eq-decl nil sets nil) (measurable_set? const-decl "bool" measure_space_def "measure_integration/") (measurable_function? const-decl "bool" measure_space_def "measure_integration/") (random_variable nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "(S)" probability_space nil) (X!1 skolem-const-decl "random_variable[T, S]" probability_space nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (x!1 skolem-const-decl "real" probability_space nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) nil)) (limit_distribution 0 (limit_distribution-1 nil 3425001894 ("" (skosimp*) (("" (assert) (("" (expand "distribution_function") (("" (case-replace "P(X!1 <= x!1)=P(X!1 = x!1)+P(X!1 < x!1)") (("1" (hide -1) (("1" (assert) (("1" (lemma "P_IUnion") (("1" (inst - "P" "LAMBDA (n:nat): X!1 <= x!1 - 1 / (1 + n)") (("1" (split -1) (("1" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.80 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
