|
(measure_space
(IMP_metric_continuity_TCC1 0
(IMP_metric_continuity_TCC1-1 nil 3426480897 ("" (grind) nil nil)
((minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(metric_zero? const-decl "bool" metric_def "metric_space/")
(metric_symmetric? const-decl "bool" metric_def "metric_space/")
(metric_triangle? const-decl "bool" metric_def "metric_space/")
(metric? const-decl "bool" metric_def "metric_space/"))
nil))
(borel_comp_measurable_is_measurable 0
(borel_comp_measurable_is_measurable-1 nil 3358646357
("" (skosimp)
(("" (typepred "g!1")
(("" (typepred "phi!1")
(("" (expand "measurable_function?")
(("" (skosimp)
(("" (expand "borel_function?")
(("" (inst - "B!1")
(("" (inst - "inverse_image(phi!1, B!1)")
(("" (expand "measurable_set?")
((""
(lemma "extensionality"
("a"
"inverse_image(g!1, inverse_image(phi!1, B!1))"
"b"
"inverse_image(o[T, real, real](phi!1, g!1), B!1)"))
(("" (split -1)
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (skosimp*)
(("2" (expand "o")
(("2"
(expand "inverse_image")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space 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)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil measure_space nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(inverse_image const-decl "set[D]" function_image nil)
(phi!1 skolem-const-decl
"borel_function[real, metric_induced_topology, real, metric_induced_topology]"
measure_space nil)
(B!1 skolem-const-decl "borel[real, metric_induced_topology]"
measure_space nil)
(extensionality formula-decl nil sets_lemmas nil)
(O const-decl "T3" function_props nil)
(member const-decl "bool" sets nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(borel? const-decl "sigma_algebra" borel nil)
(borel nonempty-type-eq-decl nil borel nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(borel_function? const-decl "bool" borel_functions nil)
(borel_function type-eq-decl nil borel_functions nil))
shostak))
(const_measurable 0
(const_measurable-1 nil 3390270932
("" (skosimp)
(("" (expand "const_fun")
(("" (expand "measurable_function?")
(("" (skosimp)
(("" (expand "measurable_set?")
(("" (expand "inverse_image")
(("" (expand "member")
(("" (typepred "S")
(("" (expand "sigma_algebra?")
(("" (flatten)
(("" (expand "subset_algebra_empty?")
(("" (expand "subset_algebra_complement?")
(("" (expand "member")
(("" (inst - "emptyset[T]")
((""
(rewrite "complement_emptyset")
((""
(case-replace "B!1(c!1)")
(("1"
(assert)
(("1"
(lemma
"extensionality"
("a"
"fullset[T]"
"b"
"{x_1: T | TRUE}"))
(("1"
(split -1)
(("1" (assert) nil nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"extensionality"
("a"
"emptyset[T]"
"b"
"{x_1: T | FALSE}"))
(("2"
(split -1)
(("1" (assert) nil nil)
("2"
(expand "emptyset")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((measurable_function? const-decl "bool" measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(subset_algebra_complement application-judgement "(S)"
measure_space nil)
(complement_emptyset formula-decl nil sets_lemmas nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
measure_space nil)
(subset_algebra_fullset name-judgement "(S)" measure_space nil)
(FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(fullset const-decl "set" sets nil)
(extensionality formula-decl nil sets_lemmas 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(borel? const-decl "sigma_algebra" borel nil)
(borel nonempty-type-eq-decl nil borel nil)
(set type-eq-decl nil sets nil)
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(subset_algebra_emptyset name-judgement "(S)" measure_space nil)
(measurable_emptyset name-judgement "measurable_set" measure_space
nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil measure_space nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(inverse_image const-decl "set[D]" function_image nil))
nil))
(nn_measurable_TCC1 0
(nn_measurable_TCC1-1 nil 3431068678
("" (expand "nn_measurable?")
(("" (rewrite "const_measurable") nil nil)) nil)
((const_measurable formula-decl nil measure_space nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(nn_measurable? const-decl "bool" measure_space nil))
nil))
(nn_measurable_is_measurable 0
(nn_measurable_is_measurable-1 nil 3431068678
("" (judgement-tcc) nil nil)
((NOT const-decl "[bool -> bool]" booleans 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)
(nn_measurable? const-decl "bool" measure_space nil)
(nn_measurable nonempty-type-eq-decl nil measure_space nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(borel? const-decl "sigma_algebra" borel nil)
(borel nonempty-type-eq-decl nil borel nil)
(Intersection const-decl "set" sets nil)
(generated_sigma_algebra const-decl "sigma_algebra"
subset_algebra_def nil)
(open? const-decl "bool" topology "topology/")
(metric_open? const-decl "bool" metric_space_def "metric_space/")
(subset? const-decl "bool" sets nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
(is_countable const-decl "bool" countability "sets_aux/")
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(member const-decl "bool" sets nil)
(Intersection_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[real]" measure_space
nil)
(emptyset_is_compact name-judgement
"compact[real, (metric_induced_topology)]" real_topology
"metric_space/")
(emptyset_is_clopen name-judgement
"clopen[real, (metric_induced_topology)]" real_topology
"metric_space/")
(subset_algebra_emptyset name-judgement "(S)" measure_space_def
nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil measure_space nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(abs_measurable 0
(abs_measurable-1 nil 3358676725
("" (skosimp)
(("" (typepred "g!1")
((""
(lemma "borel_comp_measurable_is_measurable"
("phi" "lambda (x:real): abs(x)" "g" "g!1"))
(("1" (expand "o")
(("1" (expand "abs" 1) (("1" (propax) nil nil)) nil)) nil)
("2" (hide-all-but 1)
(("2"
(lemma "continuous_is_borel"
("x" "LAMBDA (x: real): abs(x)"))
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (rewrite "metric_continuous_def")
(("2" (expand "metric_continuous?")
(("2" (expand "metric_continuous_at?")
(("2" (expand "member")
(("2" (expand "ball")
(("2" (skosimp*)
(("2" (inst + "epsilon!1")
(("2" (skosimp) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space 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)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil measure_space nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(metric_continuous? const-decl "bool" metric_continuity
"metric_space/")
(member const-decl "bool" sets nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(real_minus_real_is_real application-judgement "real" reals nil)
(metric_continuous_at? const-decl "bool" metric_continuity
"metric_space/")
(metric_continuous_def formula-decl nil metric_continuity
"metric_space/")
(continuous type-eq-decl nil continuity_def "topology/")
(continuous? const-decl "bool" continuity_def "topology/")
(continuous_is_borel judgement-tcc nil borel_functions nil)
(O const-decl "T3" function_props nil)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(borel_comp_measurable_is_measurable judgement-tcc nil
measure_space nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(borel_function? const-decl "bool" borel_functions nil)
(borel_function type-eq-decl nil borel_functions nil))
nil))
(expt_nat_measurable 0
(expt_nat_measurable-1 nil 3358677209
("" (skosimp)
((""
(lemma "borel_comp_measurable_is_measurable"
("g" "g!1" "phi" "lambda (x:real): expt(x,n!1)"))
(("1" (expand "o")
(("1" (expand "expt" 1) (("1" (propax) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (lemma "continuous_is_borel")
(("2" (inst - "LAMBDA (x: real): expt(x, n!1)")
(("2" (hide 2)
(("2"
(lemma "expt_nat_continuous"
("g" "lambda (x:real): x" "n" "n!1"))
(("1" (expand "expt" -1)
(("1" (rewrite "metric_continuous_def") nil nil))
nil)
("2" (hide 2)
(("2" (expand "metric_continuous?")
(("2" (skosimp)
(("2" (expand "metric_continuous_at?")
(("2" (skosimp)
(("2" (inst + "epsilon!1")
(("2" (skosimp) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((expt def-decl "real" exponentiation 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)
(borel_function type-eq-decl nil borel_functions nil)
(borel_function? const-decl "bool" borel_functions nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space 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)
(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 measure_space nil)
(borel_comp_measurable_is_measurable judgement-tcc nil
measure_space nil)
(expt const-decl "[T -> real]" real_fun_power "power/")
(O const-decl "T3" function_props nil)
(continuous_is_borel judgement-tcc nil borel_functions nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(metric_continuous_at? const-decl "bool" metric_continuity
"metric_space/")
(metric_continuous_def formula-decl nil metric_continuity
"metric_space/")
(metric_continuous type-eq-decl nil metric_continuity
"metric_space/")
(metric_continuous? const-decl "bool" metric_continuity
"metric_space/")
(expt_nat_continuous judgement-tcc nil real_continuity
"metric_space/")
(n!1 skolem-const-decl "nat" measure_space nil)
(continuous? const-decl "bool" continuity_def "topology/")
(continuous type-eq-decl nil continuity_def "topology/"))
nil))
(sq_measurable 0
(sq_measurable-1 nil 3430584720
("" (skosimp)
(("" (lemma "expt_nat_measurable" ("g" "g!1" "n" "2"))
(("" (expand "expt")
(("" (expand "sq")
(("" (expand "sq")
(("" (expand "expt")
(("" (expand "expt")
(("" (expand "expt") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space 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)
(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 measure_space nil)
(expt_nat_measurable judgement-tcc nil measure_space nil)
(sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(expt def-decl "real" exponentiation nil)
(sq const-decl "nonneg_real" sq "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(expt const-decl "[T -> real]" real_fun_power "power/"))
nil))
(min_measurable 0
(min_measurable-1 nil 3358676725
("" (skosimp)
(("" (lemma "sum_measurable" ("g1" "g1!1" "g2" "g2!1"))
(("" (lemma "diff_measurable" ("g1" "g1!1" "g2" "g2!1"))
(("" (lemma "abs_measurable" ("g" "(-[T])(g1!1, g2!1)"))
(("" (rewrite "min_def" 1)
((""
(lemma "diff_measurable"
("g1" "+[T](g1!1, g2!1)" "g2"
"abs[T]((-[T])(g1!1, g2!1))"))
((""
(lemma "scal_measurable"
("c" "1/2" "g" "(-[T])
(+[T](g1!1, g2!1),
abs[T]((-[T])(g1!1, g2!1)))"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((S formal-const-decl "sigma_algebra" measure_space nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil measure_space nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def 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)
(sum_measurable judgement-tcc nil measure_space_def nil)
(diff_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(abs_measurable judgement-tcc nil measure_space nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(scal_measurable judgement-tcc nil measure_space_def nil)
(scal_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(sum_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(abs_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(min_def formula-decl nil real_fun_ops_aux "reals/")
(diff_measurable judgement-tcc nil measure_space_def nil))
nil))
(max_measurable 0
(max_measurable-1 nil 3358676014
("" (skosimp)
(("" (rewrite "max_def")
(("" (typepred "g1!1")
(("" (typepred "g2!1")
(("" (lemma "diff_measurable" ("g1" "g1!1" "g2" "g2!1"))
(("" (lemma "sum_measurable" ("g1" "g1!1" "g2" "g2!1"))
(("" (lemma "abs_measurable" ("g" "(-[T])(g1!1, g2!1)"))
((""
(lemma "sum_measurable"
("g1" "+[T](g1!1, g2!1)" "g2"
"abs[T]((-[T])(g1!1, g2!1))"))
((""
(lemma "scal_measurable"
("c" "1/2" "g" "+[T]
(+[T](g1!1, g2!1),
abs[T]((-[T])(g1!1, g2!1)))"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((max_def formula-decl nil real_fun_ops_aux "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(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 nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(T formal-type-decl nil measure_space nil)
(diff_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(abs_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(sum_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(scal_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(sum_measurable judgement-tcc nil measure_space_def nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(scal_measurable judgement-tcc nil measure_space_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(abs_measurable judgement-tcc nil measure_space nil)
(diff_measurable judgement-tcc nil measure_space_def nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(minimum_measurable 0
(minimum_measurable-1 nil 3409894810
("" (induct "n")
(("1" (skosimp)
(("1" (expand "minimum") (("1" (propax) nil nil)) nil)) nil)
("2" (skosimp)
(("2" (skosimp)
(("2" (inst - "u!1")
(("2" (expand "minimum" 1)
(("2" (assert) (("2" (rewrite "min_measurable") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(min_measurable judgement-tcc nil measure_space nil)
(nat_induction formula-decl nil naturalnumbers nil)
(minimum def-decl "[T -> real]" real_fun_ops_aux "reals/")
(sequence type-eq-decl nil sequences nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_space nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(maximum_measurable 0
(maximum_measurable-1 nil 3409894810
("" (induct "n")
(("1" (skosimp)
(("1" (expand "maximum") (("1" (propax) nil nil)) nil)) nil)
("2" (skosimp)
(("2" (skosimp)
(("2" (inst - "u!1")
(("2" (expand "maximum" 1)
(("2" (rewrite "max_measurable") nil nil)) nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(max_measurable judgement-tcc nil measure_space nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nat_induction formula-decl nil naturalnumbers nil)
(maximum def-decl "[T -> real]" real_fun_ops_aux "reals/")
(sequence type-eq-decl nil sequences nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_space nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(plus_measurable 0
(plus_measurable-1 nil 3358680519
("" (skosimp)
(("" (expand "plus")
(("" (typepred "g!1")
(("" (lemma "scal_measurable" ("c" "0" "g" "g!1"))
(("" (lemma "max_measurable" ("g1" "g!1" "g2" "*[T](0,g!1)"))
(("" (expand "max" -1)
(("" (expand "*" -1)
((""
(lemma "extensionality[T,real]"
("f" "LAMBDA (x: T): max(g!1(x), 0 * g!1(x))" "g"
"LAMBDA (x: T): max(g!1(x), 0)"))
(("" (split -1)
(("1" (assert) nil nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(scal_measurable judgement-tcc nil measure_space_def nil)
(max const-decl "[T -> real]" real_fun_ops_aux "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(extensionality formula-decl nil functions nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(max_measurable judgement-tcc nil measure_space nil)
(scal_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil measure_space 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)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil))
nil))
(minus_measurable 0
(minus_measurable-1 nil 3358680519
("" (skosimp)
(("" (expand "minus")
(("" (typepred "g!1")
(("" (lemma "scal_measurable" ("c" "0" "g" "g!1"))
((""
(lemma "min_measurable" ("g1" "g!1" "g2" "*[T](0, g!1)"))
(("" (expand "*")
(("" (expand "min" -1)
(("" (assert)
((""
(lemma "opp_measurable"
("g" "LAMBDA (x:T): min(g!1(x),0*g!1(x))"))
(("" (expand "-" -1)
((""
(lemma "extensionality"
("f"
"LAMBDA (x_1: T): -min(g!1(x_1), 0 * g!1(x_1))"
"g" "LAMBDA (x: T): -min(g!1(x), 0)"))
(("" (split -1)
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_real_is_real application-judgement "real" reals nil)
(minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(scal_measurable judgement-tcc nil measure_space_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(real_minus_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 "[numfield -> numfield]" number_fields nil)
(extensionality formula-decl nil functions nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(opp_measurable judgement-tcc nil measure_space_def nil)
(min const-decl "[T -> real]" real_fun_ops_aux "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(min_measurable judgement-tcc nil measure_space nil)
(scal_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil measure_space 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)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil))
nil))
(prod_measurable 0
(prod_measurable-1 nil 3358679440
("" (skosimp)
(("" (rewrite "prod_def")
(("" (lemma "sum_measurable" ("g1" "g1!1" "g2" "g2!1"))
(("" (lemma "diff_measurable" ("g1" "g1!1" "g2" "g2!1"))
(("" (lemma "sq_measurable" ("g" "(+[T])(g1!1, g2!1)"))
(("" (lemma "sq_measurable" ("g" "(-[T])(g1!1, g2!1)"))
((""
(lemma "diff_measurable"
("g1" "sq[T]((+[T])(g1!1, g2!1))" "g2"
"sq[T]((-[T])(g1!1, g2!1))"))
(("" (rewrite "scal_measurable") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((prod_def formula-decl nil real_fun_ops_aux "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(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 nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(T formal-type-decl nil measure_space nil)
(sum_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(sq_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(diff_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(scal_measurable application-judgement "measurable_function[T, S]"
measure_space nil)
(diff_measurable judgement-tcc nil measure_space_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(scal_measurable judgement-tcc nil measure_space_def nil)
(sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(sq_measurable judgement-tcc nil measure_space nil)
(sum_measurable judgement-tcc nil measure_space_def nil))
nil))
(expt_measurable_TCC1 0
(expt_measurable_TCC1-1 nil 3433774225 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil measure_space 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)
(nn_measurable? const-decl "bool" measure_space nil)
(nn_measurable nonempty-type-eq-decl nil measure_space nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(expt_measurable 0
(expt_measurable-1 nil 3430677297
("" (skosimp)
((""
(lemma "borel_comp_measurable_is_measurable"
("phi" "(abs)^a!1" "g" "g!1"))
(("1" (expand "o")
(("1" (expand "^" -1)
(("1"
(case-replace
"(LAMBDA (x: T): (abs)(g!1(x)) ^ a!1)=(^[T](g!1, a!1))")
(("1" (hide-all-but 1)
(("1" (apply-extensionality :hide? t)
(("1" (expand "^" 1 2)
(("1" (typepred "g!1")
(("1" (expand "nn_measurable?")
(("1" (flatten)
(("1" (inst - "x!1")
(("1" (expand "abs") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "continuous_is_borel")
(("2" (inst - "(^[real]((abs), a!1))")
(("2" (hide 2)
(("2" (lemma "expt_real_continuous")
(("2" (inst - "a!1" "abs")
(("1" (rewrite "metric_continuous_def") nil nil)
("2" (hide 2)
(("2" (split)
(("1" (expand "metric_continuous?")
(("1" (expand "metric_continuous_at?")
(("1" (skosimp*)
(("1" (inst + "epsilon!1")
(("1" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "[T -> nnreal]" real_fun_power "power/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(borel_function type-eq-decl nil borel_functions nil)
(borel_function? const-decl "bool" borel_functions nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(nn_measurable nonempty-type-eq-decl nil measure_space nil)
(nn_measurable? const-decl "bool" measure_space nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space 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)
(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 measure_space nil)
(borel_comp_measurable_is_measurable judgement-tcc nil
measure_space nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "nnreal" real_expt "power/")
(O const-decl "T3" function_props nil)
(continuous_is_borel judgement-tcc nil borel_functions nil)
(metric_continuous? const-decl "bool" metric_continuity
"metric_space/")
(metric_continuous type-eq-decl nil metric_continuity
"metric_space/")
(metric_continuous_def formula-decl nil metric_continuity
"metric_space/")
(metric_continuous_at? const-decl "bool" metric_continuity
"metric_space/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(real_minus_real_is_real application-judgement "real" reals nil)
(expt_real_continuous judgement-tcc nil real_continuity
"metric_space/")
(a!1 skolem-const-decl "posreal" measure_space nil)
(continuous? const-decl "bool" continuity_def "topology/")
(continuous type-eq-decl nil continuity_def "topology/"))
nil))
(measurable_plus_minus 0
(measurable_plus_minus-1 nil 3358680295
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (assert)
(("1" (lemma "plus_measurable" ("g" "f!1"))
(("1" (lemma "minus_measurable" ("g" "f!1"))
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2"
(lemma "diff_measurable"
("g1" "plus(f!1)" "g2" "minus(f!1)"))
(("1" (rewrite "plus_minus_def" -1 :dir rl) nil nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil)
((minus_measurable judgement-tcc nil measure_space nil)
(plus_measurable judgement-tcc nil measure_space nil)
(T formal-type-decl nil measure_space nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(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 nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(diff_measurable judgement-tcc nil measure_space_def nil)
(plus_minus_def formula-decl nil real_fun_ops_aux "reals/"))
shostak))
(measurable_bounded_above_TCC1 0
(measurable_bounded_above_TCC1-1 nil 3391663705
("" (expand "measurable_function?")
(("" (skosimp)
(("" (expand "inverse_image")
(("" (expand "member")
(("" (case "B!1(0)")
(("1" (lemma "measurable_fullset")
(("1" (expand "fullset") (("1" (assert) nil nil)) nil))
nil)
("2" (lemma "measurable_emptyset")
(("2" (expand "emptyset") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(measurable_emptyset judgement-tcc nil measure_space_def nil)
(emptyset const-decl "set" sets nil)
(measurable_fullset judgement-tcc nil measure_space_def nil)
(T formal-type-decl nil measure_space nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(fullset const-decl "set" sets nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(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 nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(borel? const-decl "sigma_algebra" borel nil)
(borel nonempty-type-eq-decl nil borel nil)
(inverse_image const-decl "set[D]" function_image nil)
(measurable_function? const-decl "bool" measure_space_def nil))
nil))
(measurable_bounded_above_TCC2 0
(measurable_bounded_above_TCC2-1 nil 3391663705
("" (expand "measurable_bounded_above?")
(("" (expand "pointwise_bounded_above?")
(("" (expand "pointwise?")
(("" (expand "bounded_above?")
(("" (skosimp) (("" (inst + "0") (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((pointwise_bounded_above? const-decl "bool" pointwise_convergence
nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(pointwise? const-decl "bool" pointwise_convergence nil)
(measurable_bounded_above? const-decl "bool" measure_space nil))
nil))
(measurable_bounded_below_TCC1 0
(measurable_bounded_below_TCC1-1 nil 3391663705
("" (expand "measurable_bounded_below?")
(("" (expand "pointwise_bounded_below?")
(("" (expand "pointwise?")
(("" (skosimp)
(("" (expand "bounded_below?")
(("" (inst + "0") (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((pointwise_bounded_below? const-decl "bool" pointwise_convergence
nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(pointwise? const-decl "bool" pointwise_convergence nil)
(measurable_bounded_below? const-decl "bool" measure_space nil))
nil))
(measurable_bounded_TCC1 0
(measurable_bounded_TCC1-1 nil 3391665943
("" (expand "measurable_bounded?")
(("" (rewrite "measurable_bounded_above_TCC2")
(("" (rewrite "measurable_bounded_below_TCC1") nil nil)) nil))
nil)
((measurable_bounded_above_TCC2 subtype-tcc nil measure_space nil)
(measurable_bounded_below_TCC1 subtype-tcc nil measure_space nil)
(measurable_bounded? const-decl "bool" measure_space nil))
nil))
(measurable_bounded_above_is_bounded_above 0
(measurable_bounded_above_is_bounded_above-1 nil 3391663705
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "measurable_bounded_above?") (("" (propax) nil nil))
nil))
nil))
nil)
((measurable_bounded_above nonempty-type-eq-decl nil measure_space
nil)
(measurable_bounded_above? const-decl "bool" measure_space nil)
(sequence type-eq-decl nil sequences nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_space nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(measurable_bounded_below_is_bounded_below 0
(measurable_bounded_below_is_bounded_below-1 nil 3391663705
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "measurable_bounded_below?") (("" (propax) nil nil))
nil))
nil))
nil)
((measurable_bounded_below nonempty-type-eq-decl nil measure_space
nil)
(measurable_bounded_below? const-decl "bool" measure_space nil)
(sequence type-eq-decl nil sequences nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_space nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(measurable_bounded_is_measurable_bounded_above 0
(measurable_bounded_is_measurable_bounded_above-1 nil 3391665943
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "measurable_bounded?") (("" (flatten) nil nil))
nil))
nil))
nil)
((measurable_bounded nonempty-type-eq-decl nil measure_space nil)
(measurable_bounded? const-decl "bool" measure_space nil)
(sequence type-eq-decl nil sequences nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_space nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(measurable_bounded_is_measurable_bounded_below 0
(measurable_bounded_is_measurable_bounded_below-1 nil 3391665943
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "measurable_bounded?") (("" (flatten) nil nil))
nil))
nil))
nil)
((measurable_bounded nonempty-type-eq-decl nil measure_space nil)
(measurable_bounded? const-decl "bool" measure_space nil)
(sequence type-eq-decl nil sequences nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_space nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(measurable_bounded_is_bounded 0
(measurable_bounded_is_bounded-1 nil 3391666175
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "measurable_bounded?")
(("" (flatten)
(("" (expand "measurable_bounded_above?")
(("" (expand "measurable_bounded_below?")
(("" (rewrite "pointwise_bounded_def")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((measurable_bounded nonempty-type-eq-decl nil measure_space nil)
(measurable_bounded? const-decl "bool" measure_space nil)
(sequence type-eq-decl nil sequences nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" measure_space nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil measure_space nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.89 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.
|
