|
(probability_measure
(trivial_probability_measure_TCC1 0
(trivial_probability_measure_TCC1-1 nil 3424438960
("" (skosimp)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (expand "fullset") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(empty? const-decl "bool" sets nil))
nil))
(probability_measure_TCC1 0
(probability_measure_TCC1-1 nil 3424438960
("" (expand "probability_measure?")
(("" (expand "finite_measure?")
(("" (split)
(("1" (expand "probability_measure_full?")
(("1" (expand "trivial_probability_measure")
(("1" (lift-if) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (expand "trivial_probability_measure")
(("2" (expand "emptyset")
(("2" (expand "member") (("2" (propax) nil nil)) nil))
nil))
nil)
("3" (skosimp*)
(("3" (expand "trivial_probability_measure")
(("3" (expand "o ")
(("3" (expand "member")
(("3" (typepred "X!1")
(("3"
(case-replace "IUnion(X!1)(choose(fullset[T]))")
(("1" (name-replace "CC" "choose(fullset[T])")
(("1" (expand "IUnion")
(("1" (skosimp)
(("1" (expand "disjoint_indexed_measurable?")
(("1" (expand "disjoint?")
(("1"
(inst - "i!1" "_")
(("1"
(lemma
"single_nz_series"
("a"
"LAMBDA (x: nat):
IF X!1(x)(CC) THEN 1 ELSE 0 ENDIF"
"n"
"i!1"))
(("1"
(assert)
(("1"
(hide 2)
(("1"
(skosimp)
(("1"
(inst - "m!1")
(("1"
(assert)
(("1"
(expand "disjoint?")
(("1"
(expand "empty?")
(("1"
(expand
"intersection")
(("1"
(expand "member")
(("1"
(inst - "CC")
(("1"
(assert)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2)
(("2"
(case-replace "(LAMBDA (x: nat):
IF X!1(x)(choose(fullset[T])) THEN 1
ELSE 0
ENDIF)=(lambda (x:nat): 0)")
(("1" (hide-all-but 2)
(("1" (expand "convergence")
(("1" (skosimp)
(("1"
(inst + "0")
(("1"
(skosimp)
(("1"
(expand "series")
(("1"
(lemma
"sigma_zero[nat]"
("low" "0" "high" "i!1"))
(("1"
(replace -1)
(("1"
(expand "abs")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (apply-extensionality :hide? t)
(("2" (lift-if)
(("2"
(assert)
(("2"
(prop)
(("2"
(expand "IUnion")
(("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide-all-but 1)
(("3" (expand "fullset")
(("3" (expand "nonempty?")
(("3" (expand "empty?")
(("3" (expand "member")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sigma_algebra_IUnion_rew application-judgement "(S)"
probability_measure nil)
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(O const-decl "T3" function_props nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def "measure_integration/")
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def "measure_integration/")
(S formal-const-decl "sigma_algebra" probability_measure 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_measure nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sigma_zero formula-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(series const-decl "sequence[real]" series "series/")
(sigma_nat application-judgement "nat" sigma_nat "reals/")
(sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
(convergence const-decl "bool" convergence_sequences "analysis/")
(= const-decl "[T, T -> boolean]" equalities nil)
(disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
(single_nz_series formula-decl nil series_aux "series/")
(sequence type-eq-decl nil sequences nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(disjoint? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(fullset const-decl "set" sets nil)
(emptyset const-decl "set" sets nil)
(probability_measure_full? const-decl "bool" probability_measure
nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
probability_measure nil)
(subset_algebra_fullset name-judgement "(S)" probability_measure
nil)
(member const-decl "bool" sets nil)
(trivial_probability_measure const-decl "probability"
probability_measure nil)
(probability_measure? const-decl "bool" probability_measure nil))
nil))
(probability_measure_is_finite_measure 0
(probability_measure_is_finite_measure-1 nil 3424499703
("" (judgement-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_measure 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_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)
(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)
(probability_measure_full? const-decl "bool" probability_measure
nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
probability_measure nil)
(subset_algebra_fullset name-judgement "(S)" probability_measure
nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(measurable_emptyset name-judgement "measurable_set[T, S]"
probability_measure nil)
(subset_algebra_emptyset name-judgement "(S)" probability_measure
nil)
(series const-decl "sequence[real]" series "series/")
(convergence const-decl "bool" convergence_sequences "analysis/")
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(sigma_algebra_IUnion_rew application-judgement "(S)"
probability_measure nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sigma_nnreal application-judgement "nnreal" sigma_nat "reals/"))
nil))
(random_variable_TCC1 0
(random_variable_TCC1-1 nil 3424499077
("" (lemma "constant_is_measurable")
(("" (inst - "(LAMBDA (x: T): 0)")
(("" (hide 2)
(("" (expand "constant?")
(("" (inst + "0")
(("" (apply-extensionality :hide? t)
(("" (expand "const_fun") (("" (propax) nil nil)) 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_measure 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_measure nil))
nil))
(P_fullset 0
(P_fullset-1 nil 3424499713
("" (skosimp)
(("" (typepred "P!1")
(("" (expand "probability_measure?")
(("" (expand "probability_measure_full?")
(("" (flatten) nil nil)) nil))
nil))
nil))
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)
(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_measure 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_measure nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(probability_measure_full? const-decl "bool" probability_measure
nil))
shostak))
(P_convergence 0
(P_convergence-1 nil 3424499739
("" (skosimp)
(("" (typepred "P!1")
(("" (expand "probability_measure?")
(("" (expand "finite_measure?")
(("" (flatten)
(("" (typepred "SS!1")
(("" (inst - "SS!1")
(("1" (assert)
(("1" (expand "o ") (("1" (propax) nil nil)) nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (expand "disjoint_indexed_measurable?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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_measure 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_measure nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
probability_measure nil)
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def "measure_integration/")
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def "measure_integration/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(subset_algebra_emptyset name-judgement "(S)" probability_measure
nil)
(measurable_emptyset name-judgement "measurable_set[T, S]"
probability_measure nil)
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(O const-decl "T3" function_props nil))
shostak))
(P_emptyset 0
(P_emptyset-1 nil 3424499803
("" (skosimp)
(("" (typepred "P!1")
(("" (expand "probability_measure?")
(("" (expand "finite_measure?") (("" (flatten) nil nil)) nil))
nil))
nil))
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)
(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_measure 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_measure nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
probability_measure nil)
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/"))
shostak))
(P_disjointunion 0
(P_disjointunion-1 nil 3424499882
("" (skosimp)
(("" (assert)
(("" (typepred "P!1")
(("" (expand "probability_measure?")
(("" (flatten)
((""
(lemma "fm_disjointunion[T,S,P!1]" ("A" "A!1" "B" "B!1"))
(("1" (assert) nil nil) ("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(subset_algebra_union application-judgement "(S)"
probability_measure nil)
(fm_disjointunion formula-decl nil finite_measure
"measure_integration/")
(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_measure 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_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)
(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))
shostak))
(P_complement 0
(P_complement-1 nil 3424583049
("" (skosimp)
((""
(lemma "P_disjointunion"
("P" "P!1" "A" "A!1" "B" "complement(A!1)"))
(("" (case-replace "union(A!1, complement(A!1))=fullset[T]")
(("1" (rewrite "P_fullset")
(("1" (split -2)
(("1" (assert) nil nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality :hide? t) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
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)
(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)
(complement const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(S formal-const-decl "sigma_algebra" probability_measure 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_measure nil)
(P_disjointunion formula-decl nil probability_measure nil)
(subset_algebra_complement application-judgement "(S)"
probability_measure nil)
(P_fullset formula-decl nil probability_measure nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(subset_algebra_intersection application-judgement "(S)"
probability_measure nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(subset_algebra_fullset name-judgement "(S)" probability_measure
nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
probability_measure nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(subset_algebra_union application-judgement "(S)"
probability_measure nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(union const-decl "set" sets nil)
(fullset const-decl "set" sets nil))
shostak))
(P_union 0
(P_union-1 nil 3424956361
("" (skosimp)
((""
(lemma "P_disjointunion"
("A" "A!1" "B" "difference(B!1,A!1)" "P" "P!1"))
((""
(lemma "P_disjointunion"
("A" "B!1" "B" "difference(A!1,B!1)" "P" "P!1"))
(("" (rewrite "difference_disjoint")
(("" (rewrite "difference_disjoint")
((""
(case-replace
"union(B!1, difference(A!1, B!1))=union(A!1,B!1)")
(("1" (hide -1)
(("1" (replace -1)
(("1" (assert)
(("1" (hide -1)
(("1" (hide -1)
(("1" (rewrite "difference_intersection")
(("1"
(lemma "P_disjointunion"
("P" "P!1" "A"
"intersection(A!1, complement(B!1))" "B"
"intersection(A!1, B!1)"))
(("1"
(case-replace
"union(intersection(A!1, complement(B!1)),
intersection(A!1, B!1))=A!1")
(("1"
(split -2)
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality :hide? t)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality :hide? t)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(S formal-const-decl "sigma_algebra" probability_measure 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_measure nil)
(P_disjointunion formula-decl nil probability_measure nil)
(subset_algebra_difference application-judgement "(S)"
probability_measure nil)
(difference_disjoint formula-decl nil sets_lemmas nil)
(union const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(subset_algebra_union application-judgement "(S)"
probability_measure nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(difference_intersection formula-decl nil sets_lemmas nil)
(subset_algebra_complement application-judgement "(S)"
probability_measure nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(complement const-decl "set" sets nil)
(intersection const-decl "set" sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(subset_algebra_intersection application-judgement "(S)"
probability_measure nil))
shostak))
(P_intersection 0
(P_intersection-1 nil 3424693483
("" (skosimp)
(("" (lemma "P_union" ("A" "A!1" "B" "B!1" "P" "P!1"))
(("" (assert) nil nil)) nil))
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)
(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_measure 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_measure nil)
(P_union formula-decl nil probability_measure nil)
(subset_algebra_union application-judgement "(S)"
probability_measure nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(subset_algebra_intersection application-judgement "(S)"
probability_measure nil))
shostak))
(P_difference 0
(P_difference-1 nil 3424693520
("" (skosimp)
(("" (lemma "fm_difference[T,S,P!1]" ("A" "A!1" "B" "B!1"))
(("1" (propax) nil nil) ("2" (postpone) nil nil)) nil))
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)
(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_measure 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_measure nil)
(fm_difference formula-decl nil finite_measure
"measure_integration/"))
shostak))
(P_subset 0
(P_subset-1 nil 3424957252
("" (skosimp)
(("" (lemma "P_difference" ("P" "P!1" "A" "A!1" "B" "B!1"))
(("" (lemma "difference_subset2" ("a" "A!1" "b" "B!1"))
(("" (assert)
(("" (replace -1)
(("" (rewrite "P_emptyset") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
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)
(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_measure 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_measure nil)
(P_difference formula-decl nil probability_measure nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas_aux "measure_integration/")
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(subset_algebra_difference application-judgement "(S)"
probability_measure nil)
(P_emptyset formula-decl nil probability_measure nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(measurable_emptyset name-judgement "measurable_set[T, S]"
probability_measure nil)
(subset_algebra_emptyset name-judgement "(S)" probability_measure
nil)
(set type-eq-decl nil sets nil)
(difference_subset2 formula-decl nil sets_lemmas nil))
shostak))
(P_subset_le 0
(P_subset_le-1 nil 3424957345
("" (skosimp)
(("" (lemma "P_subset" ("A" "A!1" "B" "B!1" "P" "P!1"))
(("" (assert)
(("" (typepred "P!1(difference(B!1, A!1))")
(("" (assert) nil nil)) nil))
nil))
nil))
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)
(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_measure 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_measure nil)
(P_subset formula-decl nil probability_measure nil)
(subset_algebra_difference application-judgement "(S)"
probability_measure nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(difference const-decl "set" sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas_aux "measure_integration/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(P_IUnion 0
(P_IUnion-1 nil 3424958483
("" (skosimp)
(("" (lemma "fm_IUnion[T,S,P!1]" ("X" "X!1"))
(("" (assert)
(("" (expand "convergence")
(("" (expand "o ") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
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)
(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_measure 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_measure nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(fm_IUnion formula-decl nil finite_measure "measure_integration/")
(real_minus_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_sequences "analysis/")
(O const-decl "T3" function_props nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
probability_measure nil))
shostak))
(P_IIntersection 0
(P_IIntersection-1 nil 3424958571
("" (skosimp)
(("" (lemma "fm_IIntersection[T,S,P!1]" ("X" "X!1"))
(("" (expand "o ") (("" (assert) nil nil)) nil)) nil))
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)
(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_measure 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_measure nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(fm_IIntersection formula-decl nil finite_measure
"measure_integration/")
(sigma_algebra_IIntersection_rew application-judgement "(S)"
probability_measure nil)
(O const-decl "T3" function_props nil))
shostak))
(P0_intersection 0
(P0_intersection-1 nil 3424957493
("" (skosimp)
((""
(lemma "P_subset_le"
("P" "P!1" "A" "intersection(A!1,B!1)" "B" "A!1"))
(("" (rewrite "intersection_subset1") (("" (assert) nil nil))
nil))
nil))
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)
(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)
(intersection const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(S formal-const-decl "sigma_algebra" probability_measure 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_measure nil)
(P_subset_le formula-decl nil probability_measure nil)
(subset_algebra_intersection application-judgement "(S)"
probability_measure nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(intersection_subset1 formula-decl nil sets_lemmas nil))
shostak))
(P0_union 0
(P0_union-1 nil 3424957599
("" (skosimp)
(("" (rewrite "P_union")
(("" (lemma "P0_intersection" ("P" "P!1" "A" "A!1" "B" "B!1"))
(("" (assert) nil nil)) nil))
nil))
nil)
((P_union formula-decl nil probability_measure nil)
(T formal-nonempty-type-decl nil probability_measure 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_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)
(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)
(subset_algebra_intersection application-judgement "(S)"
probability_measure nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(P0_intersection formula-decl nil probability_measure nil))
shostak))
(P1_intersection 0
(P1_intersection-1 nil 3424957828
("" (skosimp)
((""
(lemma "P_disjointunion"
("P" "P!1" "A" "intersection(B!1, A!1)" "B"
"intersection(B!1, complement(A!1))"))
(("" (split -1)
(("1"
(case-replace "union(intersection(B!1, A!1),
intersection(B!1, complement(A!1)))=B!1")
(("1" (hide -1)
(("1"
(lemma "P0_intersection"
("P" "P!1" "B" "B!1" "A" "complement(A!1)"))
(("1" (rewrite "P_complement")
(("1" (replace -3)
(("1" (assert)
(("1" (rewrite "intersection_commutative")
(("1" (replace -1)
(("1" (hide -1 -3)
(("1" (rewrite "intersection_commutative")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality :hide? t)
(("2" (grind) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
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)
(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)
(complement const-decl "set" sets nil)
(intersection const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(S formal-const-decl "sigma_algebra" probability_measure 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_measure nil)
(P_disjointunion formula-decl nil probability_measure nil)
(subset_algebra_intersection application-judgement "(S)"
probability_measure nil)
(subset_algebra_complement application-judgement "(S)"
probability_measure nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(subset_algebra_union application-judgement "(S)"
probability_measure nil)
(P0_intersection formula-decl nil probability_measure nil)
(intersection_commutative formula-decl nil sets_lemmas nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(P_complement formula-decl nil probability_measure nil)
(member const-decl "bool" sets nil))
shostak))
(P1_union 0
(P1_union-1 nil 3424958254
("" (skosimp)
(("" (lemma "P1_intersection" ("P" "P!1" "A" "A!1" "B" "B!1"))
(("" (assert)
(("" (rewrite "P_union") (("" (assert) nil nil)) nil)) nil))
nil))
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)
(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_measure 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_measure nil)
(P1_intersection formula-decl nil probability_measure nil)
(P_union formula-decl nil probability_measure nil)
(subset_algebra_intersection application-judgement "(S)"
probability_measure nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(subset_algebra_union application-judgement "(S)"
probability_measure nil))
shostak))
(measure_to_df_TCC1 0
(measure_to_df_TCC1-1 nil 3425001461
("" (skosimp)
(("" (typepred "Y!1")
(("" (rewrite "measurable_le") (("" (inst - "x!1") 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_measure 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_measure 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/"))
nil)))
¤ Dauer der Verarbeitung: 0.64 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.
|
