|
(measure_theory
(null_set?_TCC1 0
(null_set?_TCC1-1 nil 3390731916 ("" (subtype-tcc) nil nil)
((m formal-const-decl "measure_type" measure_theory nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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" measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil measure_theory nil)
(mu_fin? const-decl "bool" measure_props nil)
(measurable_set? const-decl "bool" measure_space_def nil))
nil))
(null_set_TCC1 0
(null_set_TCC1-1 nil 3390722475
("" (expand "null_set?")
(("" (typepred "m")
(("" (expand "measure?")
(("" (flatten)
(("" (expand "mu_fin?")
(("" (expand "mu")
(("" (assert)
(("" (expand "measure_empty?")
(("" (replace -1)
(("" (assert)
(("" (typepred "S")
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra_empty?")
(("" (flatten)
((""
(expand "measurable_set?")
(("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((m formal-const-decl "measure_type" measure_theory nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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" measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(mu const-decl "nnreal" measure_props nil)
(measure_empty? const-decl "bool" generalized_measure_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(mu_fin? const-decl "bool" measure_props nil)
(null_set? const-decl "bool" measure_theory nil)
(subset_algebra_emptyset name-judgement "(S)" measure_theory 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))
nil))
(negligible_TCC1 0
(negligible_TCC1-1 nil 3390722475
("" (expand "negligible_set?")
(("" (inst + "emptyset[T]")
(("" (rewrite "null_set_TCC1") (("" (grind) nil nil)) nil)) nil))
nil)
((T formal-type-decl nil measure_theory nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(subset_algebra_emptyset name-judgement "(S)" measure_theory 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)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(null_set_TCC1 subtype-tcc nil measure_theory nil)
(negligible_set? const-decl "bool" measure_theory nil))
nil))
(negligible_iff_measurable_null 0
(negligible_iff_measurable_null-1 nil 3390726086
("" (expand "negligible_set?")
(("" (skosimp*)
(("" (split)
(("1" (skosimp*)
(("1" (expand "null_set?")
(("1" (flatten)
(("1" (assert)
(("1" (lemma "m_monotone" ("a" "X!1" "b" "X!2"))
(("1" (assert)
(("1" (assert)
(("1" (expand "x_le")
(("1" (expand "mu_fin?")
(("1" (expand "mu")
(("1" (replace -3)
(("1"
(replace -4)
(("1"
(flatten)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "null_set?")
(("2" (flatten)
(("2" (assert)
(("2" (inst + "X!1")
(("2" (assert)
(("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(m formal-const-decl "measure_type" measure_theory nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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" measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil measure_theory nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(set type-eq-decl nil sets nil)
(m_monotone formula-decl nil measure_props nil)
(mu_fin? const-decl "bool" measure_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(mu const-decl "nnreal" measure_props nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(null_set? const-decl "bool" measure_theory nil)
(negligible_set? const-decl "bool" measure_theory nil))
shostak))
(null_set_is_measurable 0
(null_set_is_measurable-1 nil 3391144602
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "null_set?") (("" (flatten) nil nil)) nil)) nil))
nil)
((null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(null_is_negligible 0
(null_is_negligible-1 nil 3390722475 ("" (judgement-tcc) nil nil)
((null_set nonempty-type-eq-decl nil measure_theory nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(S formal-const-decl "sigma_algebra" measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil measure_theory nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(m formal-const-decl "measure_type" measure_theory nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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)
(mu_fin? const-decl "bool" measure_props nil)
(mu const-decl "nnreal" measure_props nil)
(null_set? const-decl "bool" measure_theory nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(negligible_set? const-decl "bool" measure_theory nil))
nil))
(null_emptyset 0
(null_emptyset-1 nil 3395639293
("" (expand "null_set?")
(("" (typepred "m")
(("" (typepred "S")
(("" (expand "measure?")
(("" (expand "sigma_algebra?")
(("" (flatten)
(("" (expand "subset_algebra_empty?")
(("" (expand "measure_empty?")
(("" (expand "mu_fin?")
(("" (expand "mu")
(("" (replace -4)
(("" (expand "measurable_set?")
(("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((m formal-const-decl "measure_type" measure_theory nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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" measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(measure_empty? const-decl "bool" generalized_measure_def nil)
(mu const-decl "nnreal" measure_props nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(mu_fin? const-decl "bool" measure_props nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(null_set? const-decl "bool" measure_theory nil)
(subset_algebra_emptyset name-judgement "(S)" measure_theory 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))
nil))
(null_union 0
(null_union-1 nil 3509948281
("" (skosimp)
(("" (typepred "N2!1")
(("" (typepred "N1!1")
(("" (expand "null_set?")
(("" (flatten)
(("" (lemma "m_union" ("a" "N1!1" "b" "N2!1"))
(("" (expand "x_add")
(("" (expand "x_le")
(("" (expand "mu_fin?")
(("" (expand "mu")
(("" (assert)
(("" (flatten) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(measurable_union application-judgement "measurable_set[T, S]"
measure_theory nil)
(m formal-const-decl "measure_type" measure_theory nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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" measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(m_union formula-decl nil measure_props nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(mu const-decl "nnreal" measure_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(mu_fin? const-decl "bool" measure_props nil)
(x_add const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/"))
nil))
(null_intersection 0
(null_intersection-1 nil 3509948281
("" (skosimp)
(("" (typepred "N2!1")
(("" (typepred "N1!1")
(("" (expand "null_set?")
(("" (flatten)
(("" (expand "mu")
(("" (expand "mu_fin?")
((""
(lemma "m_monotone"
("a" "intersection[T](N1!1, N2!1)" "b" "N1!1"))
(("" (split)
(("1" (expand "x_le")
(("1" (assert)
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(measurable_intersection application-judgement "measurable_set"
measure_theory nil)
(mu const-decl "nnreal" measure_props nil)
(m formal-const-decl "measure_type" measure_theory nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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" measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(intersection const-decl "set" sets nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(m_monotone formula-decl nil measure_props nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(mu_fin? const-decl "bool" measure_props nil))
nil))
(null_difference 0
(null_difference-1 nil 3509948281
("" (skosimp)
((""
(lemma "m_monotone" ("a" "difference[T](N1!1, N2!1)" "b" "N1!1"))
(("" (typepred "N1!1")
(("" (typepred "N2!1")
(("" (split)
(("1" (expand "null_set?")
(("1" (expand "x_le")
(("1" (flatten)
(("1" (assert)
(("1" (expand "mu_fin?")
(("1" (expand "mu")
(("1" (assert)
(("1" (flatten) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((m formal-const-decl "measure_type" measure_theory nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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" measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(difference const-decl "set" sets nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(set type-eq-decl nil sets nil)
(m_monotone formula-decl nil measure_props nil)
(measurable_difference application-judgement "measurable_set[T, S]"
measure_theory nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(mu_fin? const-decl "bool" measure_props nil)
(mu const-decl "nnreal" measure_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(null_IUnion 0
(null_IUnion-1 nil 3509948281
("" (skosimp)
(("" (typepred "m")
(("" (lemma "disjoint_IUnion[T]" ("A" "NS!1"))
(("" (skosimp)
(("" (replace -5)
(("" (case "forall (n:nat): null_set?(B!1(n))")
(("1" (hide -3 -4 -5 -6)
(("1" (expand "measure?")
(("1" (flatten)
(("1" (expand "measure_countably_additive?")
(("1" (expand "null_set?")
(("1" (expand "mu_fin?")
(("1" (expand "mu")
(("1" (assert)
(("1"
(rewrite "measurable_IUnion")
(("1"
(inst -4 "B!1")
(("1"
(expand "x_eq")
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand "o ")
(("1"
(expand "x_sum")
(("1"
(case-replace
"FORALL (i:nat): m(B!1(i))`1")
(("1"
(case-replace
"series(LAMBDA i: m(B!1(i))`2)=lambda (n:nat): 0")
(("1"
(hide -1 -2 -3 -4 -5)
(("1"
(case-replace
"convergence_sequences.convergent?(LAMBDA (n: nat): 0)")
(("1"
(assert)
(("1"
(lemma
"convergence_sequences.limit_lemma"
("v"
"LAMBDA (n: nat): 0"))
(("1"
(replace -4)
(("1"
(hide-all-but
(-1 1))
(("1"
(expand
"convergence")
(("1"
(typepred
"m(IUnion(B!1))`2")
(("1"
(name-replace
"BB"
"m(IUnion(B!1))`2")
(("1"
(expand
">="
-1)
(("1"
(expand
"<="
-1)
(("1"
(split)
(("1"
(inst
-
"BB")
(("1"
(skosimp)
(("1"
(inst
-
"n!1")
(("1"
(assert)
(("1"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(expand
"convergent?")
(("2"
(inst + "0")
(("2"
(expand
"convergence")
(("2"
(skosimp)
(("2"
(inst
+
"0")
(("2"
(skosimp)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1 -2 1))
(("2"
(apply-extensionality
:hide?
t)
(("1"
(expand "series")
(("1"
(case-replace
"(LAMBDA (i:nat): m(B!1(i))`2) = lambda (i:nat): 0")
(("1"
(rewrite
"sigma_zero[nat]")
nil
nil)
("2"
(apply-extensionality
:hide?
t)
(("1"
(inst
-2
"x!2")
(("1"
(flatten)
nil
nil))
nil)
("2"
(skosimp)
(("2"
(inst
-2
"i!1")
(("2"
(flatten)
(("2"
(expand
"measurable_set?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(inst
-2
"i!1")
(("3"
(flatten)
(("3"
(expand
"measurable_set?")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(inst -2 "i!1")
(("2"
(expand
"measurable_set?")
(("2"
(flatten)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(inst -2 "i!1")
(("3"
(flatten)
(("3"
(expand
"measurable_set?")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace 1)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst - "i!1")
(("2"
(flatten)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(inst - "i!1")
(("3"
(flatten)
(("3"
(expand
"measurable_set?")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"disjoint_indexed_measurable?")
(("2"
(skolem + "n!1")
(("2"
(inst - "n!1")
(("2"
(flatten)
(("2"
(assert)
(("2"
(expand
"measurable_set?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skolem + "n!1")
(("2"
(inst - "n!1")
(("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2 -5)
(("2" (induct "n")
(("1" (replace -3) (("1" (assert) nil nil)) nil)
("2" (skosimp)
(("2" (inst -5 "j!1")
(("2" (inst -3 "j!1")
(("2" (replace -3 * rl)
(("2"
(lemma "null_difference"
("N1" "NS!1(j!1+1)" "N2"
"IUnion(j!1, B!1)"))
(("1" (replace -6 -1 rl)
(("1" (propax) nil nil)) nil)
("2" (replace -3)
(("2"
(hide-all-but 1)
(("2"
(case
"forall (n:nat): null_set?(IUnion(n, NS!1))")
(("1" (inst - "j!1") nil nil)
("2"
(hide 2)
(("2"
(induct "n")
(("1"
(rewrite "IUnion_0_def")
(("1" (assert) nil nil))
nil)
("2"
(skosimp)
(("2"
(rewrite "IUnion_n_def" 1)
(("2"
(rewrite "null_union")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((m formal-const-decl "measure_type" measure_theory nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(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" measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_theory 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)"
measure_theory nil)
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil)
(mu_fin? const-decl "bool" measure_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(B!1 skolem-const-decl "sequence[set[T]]" measure_theory nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(O const-decl "T3" function_props nil)
(sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sigma_zero formula-decl nil sigma "reals/")
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_times_real_is_real application-judgement "real" reals nil)
(convergence const-decl "bool" convergence_sequences "analysis/")
(<= const-decl "bool" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(BB skolem-const-decl "nnreal" measure_theory nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(limit_lemma formula-decl nil convergence_sequences "analysis/")
(convergent? const-decl "bool" convergence_sequences "analysis/")
(= const-decl "[T, T -> boolean]" equalities nil)
(series const-decl "sequence[real]" series "series/")
(x_sum const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/")
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(measurable_IUnion judgement-tcc nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(mu const-decl "nnreal" measure_props nil)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(IUnion_0_def formula-decl nil nat_indexed_sets "sets_aux/")
(IUnion_n_def formula-decl nil nat_indexed_sets "sets_aux/")
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(null_union judgement-tcc nil measure_theory nil)
(IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(null_difference judgement-tcc nil measure_theory nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(sequence type-eq-decl nil sequences nil)
(set type-eq-decl nil sets 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)
(disjoint_IUnion formula-decl nil nat_indexed_sets "sets_aux/"))
nil))
(null_Union 0
(null_Union-1 nil 3423545392
("" (skosimp)
(("" (lemma "Union_IUnion" ("XS" "Z!1"))
(("" (assert)
(("" (skosimp)
(("" (replace -1)
(("" (rewrite "null_IUnion")
(("" (hide -1 -4 2)
(("" (skolem + ("n!1"))
(("" (inst - "n!1")
(("" (split -1)
(("1" (rewrite "emptyset_is_empty?")
(("1" (replace -1)
(("1" (rewrite "null_emptyset") nil nil))
nil))
nil)
("2" (expand "every")
(("2" (inst - "YS!1(n!1)") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil measure_theory nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Union_IUnion formula-decl nil countable_indexed_sets "sets_aux/")
(null_IUnion judgement-tcc nil measure_theory nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(sequence type-eq-decl nil sequences nil)
(null_emptyset judgement-tcc nil measure_theory nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(null_emptyset name-judgement "null_set" measure_theory nil)
(subset_algebra_emptyset name-judgement "(S)" measure_theory nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(Z!1 skolem-const-decl "setofsets[T]" measure_theory nil)
(YS!1 skolem-const-decl "sequence[set[T]]" measure_theory nil)
(n!1 skolem-const-decl "nat" measure_theory nil)
(every const-decl "bool" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil))
shostak))
(negligible_union 0
(negligible_union-1 nil 3509948281
("" (skosimp)
(("" (typepred "E2!1")
(("" (typepred "E1!1")
(("" (expand "negligible_set?")
(("" (skosimp*)
(("" (inst + "union(X!1,X!2)")
(("" (rewrite "null_union")
(("" (hide -1 -3)
(("" (expand "subset?")
(("" (skosimp)
(("" (inst - "x!1")
(("" (inst - "x!1") (("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((negligible nonempty-type-eq-decl nil measure_theory nil)
(negligible_set? const-decl "bool" measure_theory nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(null_union judgement-tcc nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil))
nil))
(negligible_intersection 0
(negligible_intersection-1 nil 3509948281
("" (skosimp)
(("" (typepred "E2!1")
(("" (typepred "E1!1")
(("" (expand "negligible_set?")
(("" (skosimp*)
(("" (inst + "X!1")
(("" (assert)
(("" (hide -1 -3)
(("" (expand "subset?")
(("" (skosimp)
(("" (inst - "x!1")
(("" (inst - "x!1") (("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((negligible nonempty-type-eq-decl nil measure_theory nil)
(negligible_set? const-decl "bool" measure_theory nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
nil))
(negligible_IUnion 0
(negligible_IUnion-1 nil 3509948281
("" (skosimp)
(("" (case "forall (n:nat): exists N: subset?(ES!1(n),N)")
(("1" (expand "negligible_set?")
(("1"
(name "NNS"
"lambda (n:nat): choose[null_set]({ N | subset?(ES!1(n),N)})")
(("1" (lemma "null_IUnion" ("NS" "NNS"))
(("1" (inst + "IUnion(NNS)")
(("1" (assert)
(("1" (hide -2)
(("1" (expand "subset?" 1)
(("1" (skosimp)
(("1" (expand "member")
(("1" (expand "IUnion")
(("1" (hide -1)
(("1" (skosimp)
(("1"
(inst + "i!1")
(("1"
(expand "NNS")
(("1"
(lemma
"choose_member[null_set]"
("a"
"{N | subset?(ES!1(i!1), N)}"))
(("1"
(split)
(("1"
(expand "member")
(("1"
(expand "subset?" -1 1)
(("1"
(expand "member")
(("1"
(inst - "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 1)
(("2"
(expand "empty?")
(("2"
(inst -2 "i!1")
(("2"
(skosimp)
(("2"
(inst - "N!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (inst - "n!1")
(("2" (skosimp)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (inst - "N!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (typepred "ES!1(n!1)")
(("2" (expand "negligible_set?")
(("2" (skosimp) (("2" (inst + "X!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sequence type-eq-decl nil sequences nil)
(negligible nonempty-type-eq-decl nil measure_theory nil)
(negligible_set? const-decl "bool" measure_theory nil)
(subset? const-decl "bool" sets nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil measure_theory 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)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(NNS skolem-const-decl "[n: nat -> ({N | subset?(ES!1(n), N)})]"
measure_theory nil)
(empty? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(choose_member formula-decl nil sets_lemmas nil)
(member const-decl "bool" sets nil)
(null_IUnion application-judgement "null_set" measure_theory nil)
(null_IUnion judgement-tcc nil measure_theory nil)
(X!1 skolem-const-decl "set[T]" measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(negligible_Union 0
(negligible_Union-1 nil 3423653542
("" (skosimp)
(("" (lemma "Union_IUnion" ("XS" "Z!1"))
(("" (assert)
(("" (skosimp)
(("" (replace -1)
(("" (rewrite "negligible_IUnion")
(("" (hide -1 -4 2)
(("" (skolem + ("n!1"))
(("" (inst - "n!1")
(("" (split -1)
(("1" (rewrite "emptyset_is_empty?")
(("1" (replace -1)
(("1" (hide -1 -2)
(("1" (expand "negligible_set?")
(("1"
(inst + "emptyset[T]")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "every")
(("2" (inst - "YS!1(n!1)") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil measure_theory nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Union_IUnion formula-decl nil countable_indexed_sets "sets_aux/")
(negligible_IUnion judgement-tcc nil measure_theory nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(negligible_set? const-decl "bool" measure_theory nil)
(negligible nonempty-type-eq-decl nil measure_theory nil)
(sequence type-eq-decl nil sequences nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(null_emptyset name-judgement "null_set" measure_theory nil)
(subset_algebra_emptyset name-judgement "(S)" measure_theory nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(Z!1 skolem-const-decl "setofsets[T]" measure_theory nil)
(YS!1 skolem-const-decl "sequence[set[T]]" measure_theory nil)
(n!1 skolem-const-decl "nat" measure_theory nil)
(every const-decl "bool" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil))
shostak))
(negligible_subset 0
(negligible_subset-1 nil 3395735108
("" (skosimp)
(("" (typepred "E!1")
(("" (expand "negligible_set?")
(("" (skosimp)
(("" (inst + "X!2")
(("" (assert)
(("" (hide -1)
(("" (expand "subset?")
(("" (skosimp)
(("" (inst - "x!1")
(("" (inst - "x!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.95Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
