|
(cal_L_real
(mu_TCC1 0
(mu_TCC1-1 nil 3509695580
("" (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]" 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/")
(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_real 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_real nil))
nil))
(cal_L_real_infty_TCC1 0
(cal_L_real_infty_TCC1-1 nil 3509695580
("" (skosimp)
(("" (expand "cal_L_real_infty?")
(("" (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?")
((""
(inst + "emptyset[T]")
(("1"
(skosimp)
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil)
("2"
(expand "negligible_set?")
(("2"
(inst + " emptyset[T]")
(("2"
(split)
(("1"
(expand "null_set?")
(("1"
(expand
"measurable_set?")
(("1"
(typepred "S")
(("1"
(expand
"sigma_algebra?")
(("1"
(expand
"subset_algebra_empty?")
(("1"
(expand
"member")
(("1"
(flatten)
(("1"
(expand
"mu")
(("1"
(expand
"mu_fin?")
(("1"
(typepred
"mu!1")
(("1"
(expand
"measure?")
(("1"
(flatten)
(("1"
(expand
"measure_empty?")
(("1"
(replace
-1)
(("1"
(assert)
nil
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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_real_infty? const-decl "bool" cal_L_real nil)
(essentially_bounded? const-decl "bool" essentially_bounded nil)
(ae_bounded? const-decl "bool" complex_measure_theory nil)
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(ae? const-decl "bool" measure_theory "measure_integration/")
(ae_in? const-decl "bool" measure_theory "measure_integration/")
(measurable_set? const-decl "bool" measure_space_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/")
(subset_algebra_empty? const-decl "bool" subset_algebra_def
"measure_integration/")
(NOT const-decl "[bool -> bool]" booleans nil)
(null_set? const-decl "bool" measure_theory "measure_integration/")
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(negligible nonempty-type-eq-decl nil measure_theory
"measure_integration/")
(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_real 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)
(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]" 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/")
(fullset const-decl "set" sets nil)
(pointwise_ae? const-decl "bool" measure_theory
"measure_integration/")
(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/")
(abs const-decl "nnreal" polar "complex_alt/")
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types 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_real 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_real nil)
(cal_L_complex_infty? const-decl "bool" cal_L_complex nil))
nil))
(cal_L_real_infty_TCC2 0
(cal_L_real_infty_TCC2-1 nil 3509695580
("" (skosimp)
(("" (expand "cal_L_real_infty?")
(("" (expand "cal_L_complex_infty?")
(("" (expand "essentially_bounded?")
(("" (lemma "const_measurable[T,S]" ("c" "complex_(0, 0)"))
(("" (replace -1)
(("" (expand "ae_bounded?")
(("" (inst + "0")
(("" (expand "abs")
(("" (expand "abs")
(("" (assert)
(("" (expand "sq_abs")
(("" (assert)
(("" (expand "ae_le?")
((""
(expand "pointwise_ae?")
((""
(expand "ae?")
((""
(expand "fullset")
((""
(expand "ae_in?")
((""
(inst + "emptyset[T]")
(("1"
(skosimp)
(("1"
(expand "member")
(("1" (propax) 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"
(expand
"measurable_set?")
(("1"
(expand
"to_measure")
(("1"
(typepred
"nu!1")
(("1"
(expand
"finite_measure?")
(("1"
(flatten)
(("1"
(typepred
"S")
(("1"
(expand
"sigma_algebra?")
(("1"
(expand
"subset_algebra_empty?")
(("1"
(expand
"member")
(("1"
(flatten)
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_real_infty? const-decl "bool" cal_L_real nil)
(essentially_bounded? const-decl "bool" essentially_bounded nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(abs const-decl "nnreal" polar "complex_alt/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(ae? const-decl "bool" measure_theory "measure_integration/")
(ae_in? const-decl "bool" measure_theory "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_algebra_empty? const-decl "bool" subset_algebra_def
"measure_integration/")
(mu const-decl "nnreal" measure_props "measure_integration/")
(null_set? const-decl "bool" measure_theory "measure_integration/")
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(negligible nonempty-type-eq-decl nil measure_theory
"measure_integration/")
(emptyset const-decl "set" sets nil)
(negligible_set? const-decl "bool" measure_theory
"measure_integration/")
(nu!1 skolem-const-decl "finite_measure[T, S]" cal_L_real nil)
(to_measure const-decl "measure_type" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(set type-eq-decl nil 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]" 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/")
(fullset const-decl "set" sets nil)
(pointwise_ae? const-decl "bool" measure_theory
"measure_integration/")
(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/")
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(ae_bounded? const-decl "bool" complex_measure_theory 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_real 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_real nil)
(cal_L_complex_infty? const-decl "bool" cal_L_complex nil))
nil))
(cal_L_real_TCC1 0
(cal_L_real_TCC1-1 nil 3509695580
("" (skosimp)
(("" (expand "cal_L_real?")
(("" (expand "cal_L_complex?")
(("" (expand "p_integrable?")
(("" (lemma "const_measurable[T,S]" ("c" "complex_(0, 0)"))
(("" (replace -1)
(("" (expand "^")
(("" (expand "abs")
(("" (hide -1)
(("" (expand "abs")
(("" (expand "sq_abs")
(("" (assert)
(("" (lemma "integrable_zero[T,S,mu!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))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(p_integrable? const-decl "bool" p_integrable_def nil)
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(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 "nnreal" real_expt "power/")
(> const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_expt_0x formula-decl nil 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/")
(^ const-decl "[T -> nnreal]" real_fun_power "power/")
(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_real 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_real nil)
(cal_L_complex? const-decl "bool" cal_L_complex nil))
nil))
(cal_L_real_TCC2 0
(cal_L_real_TCC2-1 nil 3509695580
("" (skosimp)
(("" (expand "cal_L_real?")
(("" (expand "cal_L_complex?")
(("" (expand "p_integrable?")
(("" (lemma "const_measurable[T,S]" ("c" "complex_(0, 0)"))
(("" (replace -1)
(("" (expand "^")
(("" (expand "abs")
(("" (expand "abs")
(("" (expand "sq_abs")
(("" (assert)
((""
(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_real? const-decl "bool" cal_L_real nil)
(p_integrable? const-decl "bool" p_integrable_def nil)
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(sq_abs const-decl "nnreal" complex_types "complex_alt/")
(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/")
(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/")
(abs const-decl "nnreal" polar "complex_alt/")
(^ const-decl "[T -> nnreal]" real_fun_power "power/")
(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_real 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_real nil)
(cal_L_complex? const-decl "bool" cal_L_complex nil))
nil))
(cal_L_real_1_def 0
(cal_L_real_1_def-1 nil 3509706438
("" (skosimp)
(("" (expand "cal_L_real?")
(("" (rewrite "cal_L_complex_1_def")
(("" (expand "integrable?" 1 1)
(("" (expand "Re")
(("" (expand "Im")
(("" (assert)
(("" (rewrite "integrable_zero[T,S,mu!1]")
(("" (rewrite "eta") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(integrable? const-decl "bool" complex_integral nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(integrable_zero formula-decl nil integral "measure_integration/")
(eta formula-decl nil functions nil)
(Im_rew formula-decl nil complex_types "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(S formal-const-decl "sigma_algebra[T]" cal_L_real 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_real 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/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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/")
(cal_L_complex_1_def formula-decl nil cal_L_complex nil))
shostak))
(scal_cal_LR 0
(scal_cal_LR-1 nil 3509696287
("" (skosimp)
(("" (expand "cal_L_real?")
(("" (expand "*")
((""
(lemma "scal_cal_L"
("mu" "mu!1" "h" "LAMBDA x: complex_(h!1(x), 0)" "p" "p!1"
"c" "complex_(c!1, 0)"))
(("" (expand "*")
(("" (assert)
(("" (expand "*") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(S formal-const-decl "sigma_algebra[T]" cal_L_real 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_real 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/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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/")
(scal_cal_L formula-decl nil cal_L_complex nil)
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(* const-decl "complex" complex_types "complex_alt/")
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(* const-decl "[T -> real]" real_fun_ops "reals/"))
shostak))
(sum_cal_LR 0
(sum_cal_LR-1 nil 3509711611
("" (skosimp)
(("" (expand "cal_L_real?")
((""
(lemma "sum_cal_L"
("mu" "mu!1" "p" "p!1" "h1" "LAMBDA x: complex_(h1!1(x), 0)"
"h2" "LAMBDA x: complex_(h2!1(x), 0)"))
(("" (assert)
((""
(expand "+
")
(("" (assert)
(("" (expand "+ ") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(+ const-decl "complex" complex_types "complex_alt/")
(+ const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(sum_cal_L formula-decl nil cal_L_complex 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/")
(>= 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/")
(T formal-type-decl nil cal_L_real 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_real nil))
shostak))
(opp_cal_LR 0
(opp_cal_LR-1 nil 3509711702
("" (skosimp)
((""
(lemma "opp_cal_L"
("mu" "mu!1" "p" "p!1" "h" "LAMBDA x: complex_(h!1(x), 0)"))
(("" (expand "cal_L_real?")
(("" (expand "-")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((S formal-const-decl "sigma_algebra[T]" cal_L_real 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_real 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/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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/")
(opp_cal_L formula-decl nil cal_L_complex nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(- const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(- const-decl "complex" complex_types "complex_alt/")
(cal_L_real? const-decl "bool" cal_L_real nil))
shostak))
(diff_cal_LR 0
(diff_cal_LR-1 nil 3509711757
("" (skosimp)
(("" (expand "cal_L_real?")
((""
(lemma "diff_cal_L"
("mu" "mu!1" "p" "p!1" "h1" "LAMBDA x: complex_(h1!1(x), 0)"
"h2" "LAMBDA x: complex_(h2!1(x), 0)"))
(("" (expand "-")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(- const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(- const-decl "complex" complex_types "complex_alt/")
(diff_cal_L formula-decl nil cal_L_complex 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/")
(>= 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/")
(T formal-type-decl nil cal_L_real 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_real nil))
shostak))
(prod_cal_LR_TCC1 0
(prod_cal_LR_TCC1-1 nil 3509695580
("" (skosimp) (("" (assert) nil nil)) nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(prod_cal_LR_TCC2 0
(prod_cal_LR_TCC2-1 nil 3509695580
("" (skosimp) (("" (assert) nil nil)) nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(prod_cal_LR 0
(prod_cal_LR-1 nil 3509711827
("" (skosimp)
(("" (expand "cal_L_real?")
((""
(lemma "prod_cal_L"
("mu" "mu!1" "p" "p!1" "h1" "LAMBDA x: complex_(h1!1(x), 0)"
"h2" "LAMBDA x: complex_(h2!1(x), 0)" "q" "q!1"))
(("" (assert)
(("" (replace -3)
(("" (expand "*")
(("" (expand "*") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types 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)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(* const-decl "complex" complex_types "complex_alt/")
(real_times_real_is_real application-judgement "real" reals nil)
(prod_cal_L formula-decl nil cal_L_complex 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/")
(>= 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/")
(T formal-type-decl nil cal_L_real 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_real nil))
shostak))
(scal_cal_L_inftyR 0
(scal_cal_L_inftyR-1 nil 3509711887
("" (skosimp)
(("" (expand "cal_L_real_infty?")
((""
(lemma "scal_cal_L_infty"
("mu" "mu!1" "h" "LAMBDA x: complex_(h!1(x), 0)" "c"
"complex_(c!1,0)"))
(("" (expand "*")
(("" (expand "*") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((cal_L_real_infty? const-decl "bool" cal_L_real nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(* const-decl "complex" complex_types "complex_alt/")
(real_times_real_is_real application-judgement "real" reals nil)
(scal_cal_L_infty formula-decl nil cal_L_complex 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/")
(>= 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/")
(T formal-type-decl nil cal_L_real 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_real nil))
shostak))
(sum_cal_L_inftyR 0
(sum_cal_L_inftyR-1 nil 3509711946
("" (skosimp)
(("" (expand "cal_L_real_infty?")
((""
(lemma "sum_cal_L_infty"
("mu" "mu!1" "h1" "LAMBDA x: complex_(h1!1(x), 0)" "h2"
"LAMBDA x: complex_(h2!1(x), 0)"))
((""
(expand "+
")
((""
(expand "+
")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((cal_L_real_infty? const-decl "bool" cal_L_real nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(+ const-decl "complex" complex_types "complex_alt/")
(sum_cal_L_infty formula-decl nil cal_L_complex 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/")
(>= 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/")
(T formal-type-decl nil cal_L_real 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_real nil))
shostak))
(opp_cal_L_inftyR 0
(opp_cal_L_inftyR-1 nil 3509712023
("" (skosimp)
(("" (expand "cal_L_real_infty?")
((""
(lemma "opp_cal_L_infty"
("mu" "mu!1" "h" "LAMBDA x: complex_(h!1(x), 0)"))
(("" (expand "-")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((cal_L_real_infty? const-decl "bool" cal_L_real nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(- const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(- const-decl "complex" complex_types "complex_alt/")
(opp_cal_L_infty formula-decl nil cal_L_complex 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/")
(>= 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/")
(T formal-type-decl nil cal_L_real 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_real nil))
shostak))
(diff_cal_L_inftyR 0
(diff_cal_L_inftyR-1 nil 3509712066
("" (skosimp)
(("" (expand "cal_L_real_infty?")
((""
(lemma "diff_cal_L_infty"
("mu" "mu!1" "h1" "LAMBDA x: complex_(h1!1(x), 0)" "h2"
"LAMBDA x: complex_(h2!1(x), 0)"))
(("" (expand "-")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((cal_L_real_infty? const-decl "bool" cal_L_real nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(- const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(- const-decl "complex" complex_types "complex_alt/")
(diff_cal_L_infty formula-decl nil cal_L_complex 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/")
(>= 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/")
(T formal-type-decl nil cal_L_real 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_real nil))
shostak))
(prod_cal_L_inftyR 0
(prod_cal_L_inftyR-1 nil 3509712098
("" (skosimp)
(("" (expand "cal_L_real_infty?")
((""
(lemma "prod_cal_L_infty"
("mu" "mu!1" "h1" "LAMBDA x: complex_(h1!1(x), 0)" "h2"
"LAMBDA x: complex_(h2!1(x), 0)"))
(("" (expand "*")
(("" (expand "*") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((cal_L_real_infty? const-decl "bool" cal_L_real nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(* const-decl "complex" complex_types "complex_alt/")
(real_times_real_is_real application-judgement "real" reals nil)
(prod_cal_L_infty formula-decl nil cal_L_complex 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/")
(>= 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/")
(T formal-type-decl nil cal_L_real 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_real nil))
shostak))
(prod_cal_L_1_inftyR 0
(prod_cal_L_1_inftyR-1 nil 3509712129
("" (skosimp)
(("" (expand "cal_L_real_infty?")
((""
(lemma "prod_cal_L_1_infty"
("mu" "mu!1" "h1" "LAMBDA x: complex_(h1!1(x), 0)" "h2"
"LAMBDA x: complex_(h2!1(x), 0)"))
(("" (expand "cal_L_real?")
(("" (expand "*")
(("" (expand "*") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((cal_L_real_infty? const-decl "bool" cal_L_real nil)
(cal_L_real? const-decl "bool" cal_L_real nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "complex" complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(prod_cal_L_1_infty formula-decl nil cal_L_complex 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/")
(>= 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/")
(T formal-type-decl nil cal_L_real 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_real nil))
shostak))
(prod_cal_L_infty_1R 0
(prod_cal_L_infty_1R-1 nil 3509712179
("" (skosimp)
(("" (expand "cal_L_real?")
(("" (expand "cal_L_real_infty?")
((""
(lemma "prod_cal_L_infty_1"
("mu" "mu!1" "h1" "LAMBDA x: complex_(h1!1(x), 0)" "h2"
"LAMBDA x: complex_(h2!1(x), 0)"))
(("" (expand "*")
(("" (expand "*") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(S formal-const-decl "sigma_algebra[T]" cal_L_real 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_real 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/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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/")
(prod_cal_L_infty_1 formula-decl nil cal_L_complex nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "complex" complex_types "complex_alt/")
(Im_rew formula-decl nil complex_types "complex_alt/")
(Re_rew formula-decl nil complex_types "complex_alt/")
(* const-decl "[T -> complex]" complex_fun_ops "complex_alt/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(cal_L_real_infty? const-decl "bool" cal_L_real nil))
shostak))
(scal_cal_L_fmR 0
(scal_cal_L_fmR-1 nil 3509712242
("" (skosimp)
(("" (expand "cal_L_real?") (("" (rewrite "scal_cal_LR") nil nil))
nil))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(to_measure const-decl "measure_type" generalized_measure_def
"measure_integration/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S formal-const-decl "sigma_algebra[T]" cal_L_real 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)
(T formal-type-decl nil cal_L_real 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)
(scal_cal_LR formula-decl nil cal_L_real nil))
shostak))
(sum_cal_L_fmR 0
(sum_cal_L_fmR-1 nil 3509712276
("" (skosimp)
(("" (expand "cal_L_real?") (("" (rewrite "sum_cal_LR") nil nil))
nil))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(to_measure const-decl "measure_type" generalized_measure_def
"measure_integration/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S formal-const-decl "sigma_algebra[T]" cal_L_real nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil cal_L_real nil)
(sum_cal_LR formula-decl nil cal_L_real nil))
shostak))
(opp_cal_L_fmR 0
(opp_cal_L_fmR-1 nil 3509712292
("" (skosimp)
(("" (expand "cal_L_real?") (("" (rewrite "opp_cal_LR") nil nil))
nil))
nil)
((cal_L_real? const-decl "bool" cal_L_real nil)
(to_measure const-decl "measure_type" generalized_measure_def
"measure_integration/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(S formal-const-decl "sigma_algebra[T]" cal_L_real nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil cal_L_real nil)
(opp_cal_LR formula-decl nil cal_L_real nil))
shostak))
(diff_cal_L_fmR 0
(diff_cal_L_fmR-1 nil 3509712306
("" (skosimp)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.102Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
