|
(cal_L_complex
(mu_TCC1 0
(mu_TCC1-1 nil 3509685164
("" (typepred "S")
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra_empty?")
(("" (expand "member") (("" (flatten) nil nil)) nil)) nil))
nil))
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]" sigma_countable
"sigma_set/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" step_fun_props
"analysis/")
(member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def
"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-type-decl nil cal_L_complex 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[T]" cal_L_complex nil))
nil))
(cal_L_complex_infty_TCC1 0
(cal_L_complex_infty_TCC1-1 nil 3509685164
("" (skosimp)
(("" (expand "cal_L_complex_infty?")
(("" (expand "essentially_bounded?")
(("" (split)
(("1" (lemma "const_measurable[T,S]" ("c" "complex_(0, 0)"))
(("1" (propax) nil nil)) nil)
("2" (expand "ae_bounded?")
(("2" (inst + "0")
(("2" (expand "ae_le?")
(("2" (expand "pointwise_ae?")
(("2" (expand "ae?")
(("2" (expand "fullset")
(("2" (expand "ae_in?")
(("2" (inst + "emptyset[T]")
(("1" (skosimp)
(("1" (expand "member")
(("1"
(expand "abs")
(("1"
(expand "abs")
(("1"
(assert)
(("1"
(expand "sq_abs")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "negligible_set?")
(("2" (inst + "emptyset[T]")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(split)
(("1"
(expand "null_set?")
(("1"
(typepred "S")
(("1"
(expand "sigma_algebra?")
(("1"
(flatten)
(("1"
(expand
"subset_algebra_empty?")
(("1"
(expand
"measurable_set?")
(("1"
(assert)
(("1"
(typepred "mu!1")
(("1"
(expand "mu")
(("1"
(expand
"mu_fin?")
(("1"
(expand
"measure?")
(("1"
(expand
"measure_empty?")
(("1"
(flatten)
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_complex_infty? const-decl "bool" cal_L_complex nil)
(const_measurable formula-decl nil complex_measurable nil)
(complex type-decl nil complex_types "complex_alt/")
(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)
(complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
"complex_alt/")
(complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
complex_types "complex_alt/")
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(pointwise_ae? const-decl "bool" measure_theory
"measure_integration/")
(fullset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set[T]" step_fun_props
"analysis/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" sigma_countable
"sigma_set/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset const-decl "set" sets nil)
(negligible_set? const-decl "bool" measure_theory
"measure_integration/")
(mu!1 skolem-const-decl "measure_type[T, S]" cal_L_complex nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(set type-eq-decl nil sets nil)
(negligible nonempty-type-eq-decl nil measure_theory
"measure_integration/")
(member const-decl "bool" sets nil)
(abs const-decl "nnreal" polar "complex_alt/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sqrt_0 formula-decl nil sqrt "reals/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(sq_0 formula-decl nil sq "reals/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(null_set? const-decl "bool" measure_theory "measure_integration/")
(subset_algebra_empty? const-decl "bool" subset_algebra_def
"measure_integration/")
(mu const-decl "nnreal" measure_props "measure_integration/")
(measure_empty? const-decl "bool" generalized_measure_def
"measure_integration/")
(mu_fin? const-decl "bool" measure_props "measure_integration/")
(measurable_set? const-decl "bool" measure_space_def
"measure_integration/")
(NOT const-decl "[bool -> bool]" booleans nil)
(subset? const-decl "bool" sets nil)
(ae_in? const-decl "bool" measure_theory "measure_integration/")
(ae? const-decl "bool" measure_theory "measure_integration/")
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(ae_bounded? const-decl "bool" complex_measure_theory nil)
(essentially_bounded? const-decl "bool" essentially_bounded nil))
nil))
(cal_L_complex_infty_TCC2 0
(cal_L_complex_infty_TCC2-1 nil 3509689393
("" (skosimp)
(("" (expand "cal_L_complex_infty?")
(("" (expand "essentially_bounded?")
(("" (lemma "const_measurable[T,S]" ("c" "complex_(0, 0)"))
(("" (replace -1)
(("" (hide -1)
(("" (expand "ae_bounded?")
(("" (inst + "0")
(("" (expand "abs")
(("" (expand "abs")
(("" (expand "sq_abs")
(("" (assert)
(("" (expand "ae_le?")
(("" (expand "pointwise_ae?")
((""
(expand "ae?")
((""
(expand "fullset")
((""
(expand "ae_in?")
((""
(expand "member")
(("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_complex_infty? const-decl "bool" cal_L_complex nil)
(S formal-const-decl "sigma_algebra[T]" cal_L_complex 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-type-decl nil cal_L_complex nil)
(complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
complex_types "complex_alt/")
(complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
"complex_alt/")
(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)
(complex type-decl nil complex_types "complex_alt/")
(const_measurable formula-decl nil complex_measurable nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(abs const-decl "nnreal" polar "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(sq_0 formula-decl nil sq "reals/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(sqrt_0 formula-decl nil sqrt "reals/")
(pointwise_ae? const-decl "bool" measure_theory
"measure_integration/")
(fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(ae_in? const-decl "bool" measure_theory "measure_integration/")
(ae? const-decl "bool" measure_theory "measure_integration/")
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(ae_bounded? const-decl "bool" complex_measure_theory nil)
(essentially_bounded? const-decl "bool" essentially_bounded nil))
nil))
(cal_L_complex_infty_is_essentially_bounded 0
(cal_L_complex_infty_is_essentially_bounded-1 nil 3509685176
("" (skosimp)
(("" (expand "cal_L_complex_infty?") (("" (propax) nil nil)) nil))
nil)
((cal_L_complex_infty? const-decl "bool" cal_L_complex nil))
shostak))
(cal_L_complex_TCC1 0
(cal_L_complex_TCC1-1 nil 3509689393
("" (skosimp)
(("" (expand "cal_L_complex?")
(("" (expand "p_integrable?")
(("" (lemma "const_measurable[T,S]" ("c" "complex_(0, 0)"))
(("" (replace -1)
(("" (hide -1)
(("" (expand "abs")
(("" (expand "abs")
(("" (expand "sq_abs")
(("" (assert)
(("" (lemma "integrable_zero[T,S,mu!1]")
(("" (expand "^")
((""
(case-replace
"(LAMBDA (x: T): 0 ^ p!1)=LAMBDA (x: T): 0")
(("" (apply-extensionality :hide? t)
(("" (rewrite "real_expt_0x") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_complex? const-decl "bool" cal_L_complex nil)
(S formal-const-decl "sigma_algebra[T]" cal_L_complex 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-type-decl nil cal_L_complex nil)
(complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
complex_types "complex_alt/")
(complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
"complex_alt/")
(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)
(complex type-decl nil complex_types "complex_alt/")
(const_measurable formula-decl nil complex_measurable nil)
(abs const-decl "nnreal" polar "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(sq_0 formula-decl nil sq "reals/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(sqrt_0 formula-decl nil sqrt "reals/")
(^ const-decl "[T -> nnreal]" real_fun_power "power/")
(real_expt_0x formula-decl nil real_expt "power/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(^ const-decl "nnreal" real_expt "power/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(integrable_zero formula-decl nil integral "measure_integration/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(p_integrable? const-decl "bool" p_integrable_def nil))
nil))
(cal_L_complex_TCC2 0
(cal_L_complex_TCC2-1 nil 3509689393
("" (skosimp)
(("" (expand "cal_L_complex?")
(("" (lemma "const_measurable[T,S]" ("c" "complex_(0, 0)"))
(("" (expand "p_integrable?")
(("" (replace -1)
(("" (hide -1)
(("" (expand "abs")
(("" (expand "abs")
(("" (expand "sq_abs")
(("" (assert)
(("" (expand "^")
((""
(lemma
"integrable_zero[T,S,to_measure(nu!1)]")
((""
(case-replace
"(LAMBDA (x: T): 0 ^ p!1)=LAMBDA (x: T): 0")
(("" (apply-extensionality :hide? t)
(("" (rewrite "real_expt_0x") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_complex? const-decl "bool" cal_L_complex nil)
(p_integrable? const-decl "bool" p_integrable_def nil)
(abs const-decl "nnreal" polar "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(sq_0 formula-decl nil sq "reals/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(sqrt_0 formula-decl nil sqrt "reals/")
(integrable_zero formula-decl nil integral "measure_integration/")
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(to_measure const-decl "measure_type" generalized_measure_def
"measure_integration/")
(real_expt_0x formula-decl nil real_expt "power/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(^ const-decl "nnreal" real_expt "power/")
(^ const-decl "[T -> nnreal]" real_fun_power "power/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(const_measurable formula-decl nil complex_measurable nil)
(complex type-decl nil complex_types "complex_alt/")
(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)
(complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
"complex_alt/")
(complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
complex_types "complex_alt/")
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex nil))
nil))
(cal_L_complex_is_p_integrable 0
(cal_L_complex_is_p_integrable-1 nil 3509689915
("" (skosimp)
(("" (expand "cal_L_complex?") (("" (propax) nil nil)) nil)) nil)
((cal_L_complex? const-decl "bool" cal_L_complex nil)) shostak))
(cal_L_complex_1_def 0
(cal_L_complex_1_def-1 nil 3509694547
("" (skosimp)
(("" (rewrite "cal_L_complex_is_p_integrable")
(("" (expand "p_integrable?")
(("" (split)
(("1" (flatten)
(("1" (expand "^")
(("1"
(case-replace
"(LAMBDA (x: T): abs(h!1)(x) ^ 1)=abs(h!1)")
(("1" (hide -1)
(("1" (expand "complex_measurable?")
(("1" (flatten)
(("1"
(lemma "integral_ae_abs[T, S, mu!1]"
("h" "Im(h!1)" "f" "abs(h!1)"))
(("1"
(lemma "integral_ae_abs[T, S, mu!1]"
("h" "Re(h!1)" "f" "abs(h!1)"))
(("1" (split)
(("1" (flatten)
(("1"
(split)
(("1"
(flatten)
(("1"
(expand "integrable?" 1)
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(expand "ae_le?")
(("2"
(expand "pointwise_ae?")
(("2"
(expand "ae?")
(("2"
(expand "fullset")
(("2"
(expand "ae_in?")
(("2"
(inst + "emptyset[T]")
(("1"
(skosimp)
(("1"
(expand "member")
(("1"
(expand "abs")
(("1"
(hide 1)
(("1"
(expand
"abs"
1
3)
(("1"
(expand
"sq_abs")
(("1"
(typepred
"sq(Re(h!1(x!1)))")
(("1"
(rewrite
"sq_le"
1
:dir
rl)
(("1"
(rewrite
"sq_sqrt")
(("1"
(assert)
(("1"
(expand
"Im")
(("1"
(expand
"Im")
(("1"
(expand
"Re")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"negligible_set?")
(("2"
(inst
+
"emptyset[T]")
(("2"
(split)
(("1"
(expand
"null_set?")
(("1"
(expand
"mu_fin?")
(("1"
(expand "mu")
(("1"
(typepred
"mu!1")
(("1"
(expand
"measure?")
(("1"
(flatten)
(("1"
(expand
"measure_empty?")
(("1"
(replace
-1)
(("1"
(typepred
"S")
(("1"
(expand
"sigma_algebra?")
(("1"
(expand
"subset_algebra_empty?")
(("1"
(flatten)
(("1"
(expand
"measurable_set?")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
("2" (hide-all-but 1)
(("2"
(expand "ae_le?")
(("2"
(expand "pointwise_ae?")
(("2"
(expand "ae?")
(("2"
(expand "fullset")
(("2"
(expand "ae_in?")
(("2"
(expand "member")
(("2"
(inst + "emptyset[T]")
(("1"
(skosimp)
(("1"
(hide 1)
(("1"
(expand "abs")
(("1"
(expand "abs" 1 3)
(("1"
(expand "sq_abs")
(("1"
(rewrite
"sq_le"
1
:dir
rl)
(("1"
(assert)
(("1"
(expand
"Re")
(("1"
(expand
"Re")
(("1"
(expand
"Im")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"negligible_set?")
(("2"
(inst + "emptyset[T]")
(("2"
(split)
(("1"
(expand
"null_set?")
(("1"
(expand
"mu_fin?")
(("1"
(expand "mu")
(("1"
(typepred
"S")
(("1"
(expand
"sigma_algebra?")
(("1"
(expand
"subset_algebra_empty?")
(("1"
(typepred
"mu!1")
(("1"
(expand
"measure?")
(("1"
(expand
"measure_empty?")
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand
"measurable_set?")
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (apply-extensionality :hide? t)
(("2" (expand "abs")
(("2" (rewrite "real_expt_x1") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "integrable_is_measurable[T, S, mu!1]")
(("2" (inst - "h!1")
(("2" (replace -1)
(("2"
(lemma "integrable_abs[T, S, mu!1]" ("f" "h!1"))
(("1" (expand "^" 1)
(("1"
(case-replace
"(LAMBDA (x: T): abs(h!1)(x) ^ 1)=abs[T](h!1)")
(("1" (apply-extensionality :hide? t)
(("1" (rewrite "real_expt_x1") nil nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_complex_is_p_integrable formula-decl nil cal_L_complex nil)
(T formal-type-decl nil cal_L_complex nil)
(complex type-decl nil complex_types "complex_alt/")
(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[T]" cal_L_complex 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(^ const-decl "[T -> nnreal]" real_fun_power "power/")
(real_expt_x1 formula-decl nil real_expt "power/")
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(Re_fun_rew formula-decl nil complex_fun_ops "complex_alt/")
(pointwise_ae? const-decl "bool" measure_theory
"measure_integration/")
(fullset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set[T]" step_fun_props
"analysis/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" sigma_countable
"sigma_set/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(set type-eq-decl nil sets nil)
(mu!1 skolem-const-decl "measure_type[T, S]" cal_L_complex nil)
(negligible_set? const-decl "bool" measure_theory
"measure_integration/")
(emptyset const-decl "set" sets nil)
(negligible nonempty-type-eq-decl nil measure_theory
"measure_integration/")
(member const-decl "bool" sets nil)
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(Im const-decl "real" complex_types "complex_alt/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(sq_le formula-decl nil sq "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Im_fun_rew formula-decl nil complex_fun_ops "complex_alt/")
(sq_abs formula-decl nil sq "reals/")
(sq_sqrt formula-decl nil sqrt "reals/")
(TRUE const-decl "bool" booleans nil)
(Re const-decl "real" complex_types "complex_alt/")
(sq const-decl "nonneg_real" sq "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(abs const-decl "nnreal" polar "complex_alt/")
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(subset? const-decl "bool" sets nil)
(null_set? const-decl "bool" measure_theory "measure_integration/")
(mu const-decl "nnreal" measure_props "measure_integration/")
(measure_empty? const-decl "bool" generalized_measure_def
"measure_integration/")
(subset_algebra_empty? const-decl "bool" subset_algebra_def
"measure_integration/")
(measurable_set? const-decl "bool" measure_space_def
"measure_integration/")
(mu_fin? const-decl "bool" measure_props "measure_integration/")
(ae_in? const-decl "bool" measure_theory "measure_integration/")
(ae? const-decl "bool" measure_theory "measure_integration/")
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(integrable? const-decl "bool" complex_integral nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(integrable nonempty-type-eq-decl nil integral
"measure_integration/")
(integrable? const-decl "bool" integral "measure_integration/")
(integral_ae_abs formula-decl nil integral "measure_integration/")
(complex_measurable? const-decl "bool" complex_measurable nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(^ const-decl "nnreal" real_expt "power/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(integrable_is_measurable judgement-tcc nil complex_integral nil)
(integrable_abs judgement-tcc nil complex_integral nil)
(integrable nonempty-type-eq-decl nil complex_integral nil)
(h!1 skolem-const-decl "[T -> complex]" cal_L_complex nil)
(p_integrable? const-decl "bool" p_integrable_def nil))
shostak))
(scal_cal_L 0
(scal_cal_L-1 nil 3509690322
("" (skosimp)
(("" (expand "cal_L_complex?")
((""
(lemma "scal_p_integrable[T, S, mu!1, p!1]"
("c" "c!1" "f" "h!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
nil))
nil)
((cal_L_complex? const-decl "bool" cal_L_complex nil)
(scal_p_integrable judgement-tcc nil p_integrable nil)
(complex type-decl nil complex_types "complex_alt/")
(p_integrable? const-decl "bool" p_integrable_def nil)
(p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/"))
shostak))
(sum_cal_L 0
(sum_cal_L-1 nil 3509690361
("" (expand "cal_L_complex?")
(("" (skosimp)
((""
(lemma "sum_p_integrable[T, S, mu!1, p!1]"
("f0" "h1!1" "f1" "h2!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)
("3" (propax) nil nil))
nil))
nil))
nil)
((sum_p_integrable judgement-tcc nil p_integrable nil)
(complex type-decl nil complex_types "complex_alt/")
(p_integrable? const-decl "bool" p_integrable_def nil)
(p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(cal_L_complex? const-decl "bool" cal_L_complex nil))
shostak))
(opp_cal_L 0
(opp_cal_L-1 nil 3509690396
("" (expand "cal_L_complex?")
(("" (skosimp)
(("" (lemma "opp_p_integrable[T, S, mu!1, p!1]" ("f" "h!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
nil))
nil)
((opp_p_integrable judgement-tcc nil p_integrable nil)
(complex type-decl nil complex_types "complex_alt/")
(p_integrable? const-decl "bool" p_integrable_def nil)
(p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(cal_L_complex? const-decl "bool" cal_L_complex nil))
shostak))
(diff_cal_L 0
(diff_cal_L-1 nil 3509690422
("" (skosimp)
(("" (expand "cal_L_complex?")
((""
(lemma "diff_p_integrable[T, S, mu!1, p!1]"
("f0" "h1!1" "f1" "h2!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)
("3" (propax) nil nil))
nil))
nil))
nil)
((cal_L_complex? const-decl "bool" cal_L_complex nil)
(diff_p_integrable judgement-tcc nil p_integrable nil)
(complex type-decl nil complex_types "complex_alt/")
(p_integrable? const-decl "bool" p_integrable_def nil)
(p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/"))
shostak))
(prod_cal_L_TCC1 0
(prod_cal_L_TCC1-1 nil 3509691141 ("" (subtype-tcc) nil nil) nil
nil))
(prod_cal_L_TCC2 0
(prod_cal_L_TCC2-1 nil 3509691141 ("" (subtype-tcc) nil nil) nil
nil))
(prod_cal_L 0
(prod_cal_L-1 nil 3509691141
("" (skosimp)
(("" (expand "cal_L_complex?")
((""
(lemma "holder_judge1[T, S, mu!1, p!1,q!1]"
("f" "h1!1" "g" "h2!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)
("3" (propax) nil nil) ("4" (propax) nil nil)
("5" (propax) nil nil))
nil))
nil))
nil)
((cal_L_complex? const-decl "bool" cal_L_complex nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_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)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(holder_judge1 judgement-tcc nil holder_scaf nil)
(complex type-decl nil complex_types "complex_alt/")
(p_integrable? const-decl "bool" p_integrable_def nil)
(p_integrable nonempty-type-eq-decl nil p_integrable_def nil)
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/"))
shostak))
(scal_cal_L_infty 0
(scal_cal_L_infty-1 nil 3509690455
("" (skosimp)
(("" (expand "cal_L_complex_infty?")
((""
(lemma "scal_essentially_bounded[T, S, mu!1]"
("c" "c!1" "f" "h!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
nil))
nil)
((cal_L_complex_infty? const-decl "bool" cal_L_complex nil)
(scal_essentially_bounded judgement-tcc nil essentially_bounded
nil)
(complex type-decl nil complex_types "complex_alt/")
(essentially_bounded? const-decl "bool" essentially_bounded nil)
(essentially_bounded nonempty-type-eq-decl nil essentially_bounded
nil)
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/"))
shostak))
(sum_cal_L_infty 0
(sum_cal_L_infty-1 nil 3509690485
("" (skosimp)
(("" (expand "cal_L_complex_infty?")
((""
(lemma "add_essentially_bounded[T, S, mu!1]"
("f0" "h1!1" "f1" "h2!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)
("3" (propax) nil nil))
nil))
nil))
nil)
((cal_L_complex_infty? const-decl "bool" cal_L_complex nil)
(add_essentially_bounded judgement-tcc nil essentially_bounded nil)
(complex type-decl nil complex_types "complex_alt/")
(essentially_bounded? const-decl "bool" essentially_bounded nil)
(essentially_bounded nonempty-type-eq-decl nil essentially_bounded
nil)
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/"))
shostak))
(opp_cal_L_infty 0
(opp_cal_L_infty-1 nil 3509690538
("" (skosimp)
(("" (expand "cal_L_complex_infty?")
(("" (lemma "opp_essentially_bounded[T, S, mu!1]" ("f" "h!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
nil))
nil)
((cal_L_complex_infty? const-decl "bool" cal_L_complex nil)
(opp_essentially_bounded judgement-tcc nil essentially_bounded nil)
(complex type-decl nil complex_types "complex_alt/")
(essentially_bounded? const-decl "bool" essentially_bounded nil)
(essentially_bounded nonempty-type-eq-decl nil essentially_bounded
nil)
(T formal-type-decl nil cal_L_complex 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[T]" cal_L_complex 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/"))
shostak))
(diff_cal_L_infty 0
(diff_cal_L_infty-1 nil 3509690562
("" (skosimp)
(("" (expand "cal_L_complex_infty?")
((""
(lemma "diff_essentially_bounded[T, S, mu!1]"
("f0" "h1!1" "f1" "h2!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)
("3" (propax) nil nil))
nil))
nil))
nil)
((cal_L_complex_infty? const-decl "bool" cal_L_complex nil)
(diff_essentially_bounded judgement-tcc nil essentially_bounded
nil)
(complex type-decl nil complex_types "complex_alt/")
(essentially_bounded? const-decl "bool" essentially_bounded nil)
(essentially_bounded nonempty-type-eq-decl nil essentially_bounded
nil)
(T formal-type-decl nil cal_L_complex 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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.83Angebot
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
|
