|
(indefinite_integral
(integral_TCC1 0
(integral_TCC1-1 nil 3391140825
("" (skosimp)
(("" (typepred "f!1")
(("" (expand "integrable?" -1) (("" (propax) nil nil)) nil))
nil))
nil)
((integrable? const-decl "bool" indefinite_integral 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)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" indefinite_integral 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)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil indefinite_integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(indefinite_emptyset_TCC1 0
(indefinite_emptyset_TCC1-1 nil 3459223617
("" (skosimp)
(("" (expand "integrable?")
(("" (case-replace "phi(emptyset[T]) * g!1=lambda x: 0")
(("1" (rewrite "integrable_zero") nil nil)
("2" (apply-extensionality :hide? t)
(("2" (expand "*")
(("2" (expand "emptyset")
(("2" (expand "phi")
(("2" (expand "member") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable? const-decl "bool" indefinite_integral nil)
(member const-decl "bool" sets nil)
(real_times_real_is_real application-judgement "real" reals nil)
(m formal-const-decl "measure_type" indefinite_integral 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)
(integrable_zero formula-decl nil integral nil)
(emptyset const-decl "set" sets nil)
(phi const-decl "nat" measure_space nil)
(S formal-const-decl "sigma_algebra" indefinite_integral 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)
(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)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil indefinite_integral nil)
(phi_is_simple application-judgement "simple" indefinite_integral
nil)
(subset_algebra_emptyset name-judgement "(S)" indefinite_integral
nil)
(null_emptyset name-judgement "null_set" indefinite_integral nil)
(finite_emptyset name-judgement "finite_set[T]" sigma_countable
"sigma_set/")
(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))
(indefinite_emptyset 0
(indefinite_emptyset-1 nil 3459223725
("" (skosimp)
(("" (expand "integral")
(("" (case-replace "phi(emptyset) * g!1=lambda x: 0")
(("1" (rewrite "integral_zero") nil nil)
("2" (apply-extensionality :hide? t)
(("2" (hide 2) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((integral const-decl "real" indefinite_integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(real_times_real_is_real application-judgement "real" reals nil)
(m formal-const-decl "measure_type" indefinite_integral 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)
(integral_zero formula-decl nil integral nil)
(emptyset const-decl "set" sets nil)
(phi const-decl "nat" measure_space nil)
(S formal-const-decl "sigma_algebra" indefinite_integral 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)
(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)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil indefinite_integral nil)
(phi_is_simple application-judgement "simple" indefinite_integral
nil)
(subset_algebra_emptyset name-judgement "(S)" indefinite_integral
nil)
(null_emptyset name-judgement "null_set" indefinite_integral nil)
(finite_emptyset name-judgement "finite_set[T]" sigma_countable
"sigma_set/")
(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))
shostak))
(indefinite_fullset_TCC1 0
(indefinite_fullset_TCC1-1 nil 3459223617
("" (skosimp)
(("" (expand "integrable?")
(("" (rewrite "indefinite_integrable") nil nil)) nil))
nil)
((prod_measurable application-judgement "measurable_function[T, S]"
indefinite_integral nil)
(integrable? const-decl "bool" indefinite_integral nil)
(m formal-const-decl "measure_type" indefinite_integral 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" indefinite_integral 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 indefinite_integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(fullset 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)
(indefinite_integrable formula-decl nil integral nil)
(subset_algebra_fullset name-judgement "(S)" indefinite_integral
nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
indefinite_integral nil))
nil))
(indefinite_fullset 0
(indefinite_fullset-1 nil 3459223764
("" (skosimp)
(("" (expand "integral" 1 1)
(("" (case-replace "phi(fullset) * f!1=f!1")
(("" (hide 2)
(("" (apply-extensionality :hide? t) (("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
((integral const-decl "real" indefinite_integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(real_times_real_is_real application-judgement "real" reals nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(m formal-const-decl "measure_type" indefinite_integral 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)
(fullset const-decl "set" sets nil)
(phi const-decl "nat" measure_space nil)
(S formal-const-decl "sigma_algebra" indefinite_integral 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)
(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)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil indefinite_integral nil)
(prod_measurable application-judgement "measurable_function[T, S]"
indefinite_integral nil)
(phi_is_simple application-judgement "simple" indefinite_integral
nil)
(subset_algebra_fullset name-judgement "(S)" indefinite_integral
nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
indefinite_integral nil))
shostak))
(indefinite_eq_0_TCC1 0
(indefinite_eq_0_TCC1-1 nil 3395207138
("" (skosimp)
(("" (typepred "E!1")
(("" (expand "measurable_set?") (("" (propax) nil nil)) nil))
nil))
nil)
((measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" indefinite_integral 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)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil indefinite_integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(indefinite_eq_0 0
(indefinite_eq_0-1 nil 3395604081
("" (skosimp)
(("" (lemma "integral_ae_ge_0" ("f" "phi(E!1) * f!1"))
(("" (replace -3)
(("" (split -1)
(("1" (hide -3)
(("1" (expand "ae_in?")
(("1" (skosimp)
(("1" (typepred "E!2")
(("1" (expand "negligible_set?")
(("1" (skosimp)
(("1" (expand "ae_0?")
(("1" (expand "restrict")
(("1" (expand "pointwise_ae?")
(("1" (expand "ae?")
(("1"
(expand "fullset")
(("1"
(expand "ae_in?")
(("1"
(skosimp)
(("1"
(typepred "E!3")
(("1"
(expand "negligible_set?")
(("1"
(skosimp)
(("1"
(name-replace "FF" "X!1")
(("1"
(case
"forall x: difference(E!1,FF)(x) => f!1(x)>0")
(("1"
(hide -5 -7)
(("1"
(name-replace
"GG"
"X!2")
(("1"
(case
"FORALL x: difference(E!1, GG)(x) => f!1(x) = 0")
(("1"
(hide -4 -6)
(("1"
(lemma
"null_union"
("N1"
"FF"
"N2"
"GG"))
(("1"
(lemma
"m_monotone"
("a"
"E!1"
"b"
"union(FF,GG)"))
(("1"
(split -1)
(("1"
(hide-all-but
(-1
-2
1))
(("1"
(expand
"null_set?")
(("1"
(expand
"x_le")
(("1"
(expand
"mu_fin?")
(("1"
(expand
"mu")
(("1"
(flatten)
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-1
-4
-5
2)
(("2"
(expand
"subset?")
(("2"
(skosimp)
(("2"
(expand
"member")
(("2"
(inst
-
"x!1")
(("2"
(inst
-
"x!1")
(("2"
(expand
"union")
(("2"
(flatten)
(("2"
(expand
"member")
(("2"
(expand
"difference")
(("2"
(expand
"member")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"null_set?")
(("2"
(flatten)
nil
nil))
nil))
nil)
("2"
(propax)
nil
nil)
("3"
(propax)
nil
nil))
nil))
nil)
("2"
(hide -1 -4 2)
(("2"
(skosimp)
(("2"
(expand
"difference")
(("2"
(expand
"member")
(("2"
(flatten)
(("2"
(expand
"subset?")
(("2"
(inst
-
"x!1")
(("2"
(expand
"member")
(("2"
(assert)
(("2"
(inst
-
"x!1")
(("2"
(assert)
(("2"
(expand
"*")
(("2"
(expand
"phi")
(("2"
(expand
"member")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand "difference")
(("2"
(expand "member")
(("2"
(flatten)
(("2"
(inst -7 "x!1")
(("2"
(expand
"subset?")
(("2"
(inst
-5
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2)
(("2" (expand "ae_nonneg?")
(("2" (expand "pointwise_ae?")
(("2" (expand "ae?")
(("2" (expand "fullset")
(("2" (expand "ae_in?")
(("2" (skosimp)
(("2" (typepred "E!2")
(("2" (expand "*")
(("2" (inst + "intersection(E!1,E!2)")
(("1"
(skosimp)
(("1"
(expand "intersection")
(("1"
(assert)
(("1"
(expand "phi")
(("1"
(assert)
(("1"
(case-replace "E!1(x!1)")
(("1"
(inst - "x!1")
(("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"negligible_subset"
("E"
"E!2"
"X"
"intersection[T](E!1, E!2)"))
(("2"
(split -1)
(("1" (propax) nil nil)
("2"
(hide-all-but 1)
(("2"
(expand "intersection")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2" (skosimp*) 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" indefinite_integral 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" indefinite_integral 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 indefinite_integral nil)
(integrable? const-decl "bool" indefinite_integral nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(phi const-decl "nat" measure_space 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)
(set type-eq-decl nil sets nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(integral_ae_ge_0 formula-decl nil integral nil)
(ae_in? const-decl "bool" measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(negligible_set? const-decl "bool" measure_theory nil)
(negligible nonempty-type-eq-decl nil measure_theory nil)
(restrict const-decl "R" restrict nil)
(ae? const-decl "bool" measure_theory nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(difference const-decl "set" sets nil)
(> const-decl "bool" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(TRUE const-decl "bool" booleans nil)
(m_monotone formula-decl nil measure_props nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets 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)
(mu_fin? const-decl "bool" measure_props nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(null_union judgement-tcc nil measure_theory nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(x!1 skolem-const-decl "T" indefinite_integral nil)
(E!1 skolem-const-decl "measurable_set[T, S]" indefinite_integral
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(fullset const-decl "set" sets nil)
(pointwise_ae? const-decl "bool" measure_theory nil)
(ae_0? const-decl "bool" measure_theory nil)
(ae_nonneg? const-decl "bool" measure_theory nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
indefinite_integral nil)
(subset_algebra_fullset name-judgement "(S)" indefinite_integral
nil)
(intersection const-decl "set" sets nil)
(E!2 skolem-const-decl "negligible[T, S, m]" indefinite_integral
nil)
(x!1 skolem-const-decl "({x | TRUE})" indefinite_integral nil)
(negligible_subset formula-decl nil measure_theory nil))
shostak))
(indefinite_eq_TCC1 0
(indefinite_eq_TCC1-1 nil 3431893575
("" (skosimp)
(("" (expand "integrable?")
(("" (rewrite "indefinite_integrable") nil nil)) nil))
nil)
((integrable? const-decl "bool" indefinite_integral nil)
(m formal-const-decl "measure_type" indefinite_integral 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" indefinite_integral 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 indefinite_integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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)
(indefinite_integrable formula-decl nil integral nil))
nil))
(indefinite_eq 0
(indefinite_eq-1 nil 3391226280
("" (skosimp)
(("" (expand "integral")
(("" (name "H" "f1!1-f2!1")
(("" (lemma "integrable_diff" ("f1" "f1!1" "f2" "f2!1"))
(("" (replace -2)
(("" (lemma "integrable_is_measurable" ("x" "H"))
(("" (lemma "measurable_gt" ("f" "H"))
(("" (lemma "measurable_lt" ("f" "H"))
(("" (assert)
(("" (inst - "0")
(("" (inst - "0")
(("" (inst-cp - "{z: T | H(z) > 0}")
(("1" (inst - "{z: T | H(z) < 0}")
(("1"
(lemma "indefinite_eq_0"
("E" "{z: T | H(z) > 0}" "f" "H"))
(("1"
(split -1)
(("1"
(lemma
"indefinite_eq_0"
("E" "{z: T | H(z) < 0}" "f" "-H"))
(("1"
(split -1)
(("1"
(skosimp)
(("1"
(hide -10 -11 -8 -9)
(("1"
(lemma
"m_disjoint_union"
("a"
"{z: T | H(z) < 0}"
"b"
"{z: T | H(z) > 0}"))
(("1"
(split -1)
(("1"
(expand "x_eq")
(("1"
(expand "mu_fin?")
(("1"
(expand "mu")
(("1"
(assert)
(("1"
(flatten)
(("1"
(expand
"x_add")
(("1"
(assert)
(("1"
(replace
-4)
(("1"
(replace
-6)
(("1"
(hide
-3
-4
-5
-6)
(("1"
(expand
"ae_eq?")
(("1"
(expand
"restrict")
(("1"
(expand
"pointwise_ae?")
(("1"
(expand
"ae?")
(("1"
(expand
"fullset")
(("1"
(expand
"ae_in?")
(("1"
(inst
+
"union({z: T | H(z) < 0}, {z: T | H(z) > 0})")
(("1"
(skosimp)
(("1"
(expand
"H")
(("1"
(expand
"union")
(("1"
(expand
"member")
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand
"-")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"negligible_set?")
(("2"
(inst
+
"union({z: T | H(z) < 0}, {z: T | H(z) > 0})")
(("2"
(split)
(("1"
(expand
"null_set?")
(("1"
(rewrite
"measurable_union")
(("1"
(expand
"mu_fin?")
(("1"
(expand
"mu")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"subset?")
(("2"
(skosimp)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(expand "disjoint?")
(("2"
(expand
"intersection")
(("2"
(expand "empty?")
(("2"
(skosimp)
(("2"
(expand
"member")
(("2"
(flatten)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "ae_in?")
(("2"
(flatten)
(("2"
(inst
+
"{z: T | H(z) > 0}")
(("1"
(skosimp)
(("1"
(expand "-")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"negligible_set?")
(("2"
(inst
+
"{z: T | H(z) > 0}")
(("2"
(split)
(("1"
(expand
"null_set?")
(("1"
(expand
"measurable_set?")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand "subset?")
(("2"
(skosimp)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but (-5 -4 1 -7))
(("3"
(expand "H" 1 2)
(("3"
(case-replace
"phi({z: T | H(z) < 0}) * -(f1!1 - f2!1) = phi({z: T | H(z) < 0}) * f2!1-phi({z: T | H(z) < 0}) * f1!1")
(("1"
(rewrite "integral_diff")
(("1" (assert) nil nil))
nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality
:hide?
t)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "integrable?")
(("2"
(rewrite "indefinite_integrable")
(("2"
(expand "measurable_set?")
(("2" (propax) nil nil))
nil))
nil))
nil)
("3"
(expand "measurable_set?")
(("3" (propax) nil nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "ae_in?")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(expand "H" 1 2)
(("3"
(expand "-" 1)
(("3"
(expand "*" 1)
(("3"
(lemma
"integral_diff"
("f1"
"phi({z: T | H(z) > 0}) * f1!1"
"f2"
"phi({z: T | H(z) > 0}) * f2!1"))
(("3"
(expand "-" -1)
(("3"
(expand "*" -1)
(("3"
(replace -1 1)
(("3"
(assert)
(("3"
(expand "*" -8)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "integrable?")
(("2"
(rewrite "indefinite_integrable")
(("2"
(expand "measurable_set?")
(("2" (propax) nil nil))
nil))
nil))
nil)
("3"
(expand "measurable_set?")
(("3" (propax) nil nil))
nil))
nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integral const-decl "real" indefinite_integral nil)
(integrable_diff judgement-tcc nil integral nil)
(integrable_is_measurable judgement-tcc nil integral nil)
(measurable_lt formula-decl nil measure_space_def nil)
(set type-eq-decl nil sets nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(> const-decl "bool" reals nil)
(H skolem-const-decl "integrable[T, S, m]" indefinite_integral nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(indefinite_eq_0 formula-decl nil indefinite_integral nil)
(integrable? const-decl "bool" indefinite_integral nil)
(integrable_opp application-judgement "integrable"
indefinite_integral nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(phi const-decl "nat" measure_space 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)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(integral_diff formula-decl nil integral nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(m_disjoint_union formula-decl nil measure_props nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(mu const-decl "nnreal" measure_props nil)
(ae_eq? const-decl "bool" measure_theory nil)
(pointwise_ae? const-decl "bool" measure_theory nil)
(fullset const-decl "set" sets nil)
(negligible_set? const-decl "bool" measure_theory nil)
(union const-decl "set" sets nil)
(negligible nonempty-type-eq-decl nil measure_theory nil)
(member const-decl "bool" sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.146 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.
|
