|
(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: 1.17 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
