| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 657 kB |
|
Quelle measure_space.prfSprache: Lisp |
|||||||||||||||
|
(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) (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) (measurable_bounded_below? const-decl "bool" measure_space nil) (pointwise_bounded_def formula-decl nil pointwise_convergence nil) (measurable_bounded_above? const-decl "bool" measure_space nil)) nil)) (inf_measurable 0 (inf_measurable-1 nil 3392299935 ("" (skosimp) (("" (case "forall m: measurable_function?[T, S](u!1(m))") (("1" (rewrite "measurable_ge") (("1" (skosimp) (("1" (case-replace "{z: T | inf(u!1)(n!1)(z) >= c!1}=IIntersection(lambda m: {z: T | u!1(m+n!1)(z) >= c!1})") (("1" (hide -1) (("1" (lemma "measurable_IIntersection" ("SS" "LAMBDA m: {z: T | u!1(m + n!1)(z) >= c!1}")) (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "m!1+n!1") (("2" (rewrite "measurable_ge") (("2" (inst - "c!1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "IIntersection") (("2" (expand "inf") (("2" (typepred "inf(image[nat, real](LAMBDA m: u!1(m)(x!1), {m | m >= n!1}))") (("2" (name-replace "INF" "inf(image[nat, real](LAMBDA m: u!1(m)(x!1), {m | m >= n!1}))") (("2" (expand "image") (("2" (expand "greatest_lower_bound") (("2" (flatten) (("2" (expand "lower_bound") (("2" (case-replace "(FORALL (i: nat): u!1(i + n!1)(x!1) >= c!1)") (("1" (inst -3 "c!1") (("1" (split -3) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "z!1") (("3" (skosimp) (("3" (typepred "x!2") (("3" (inst -3 "x!2-n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (simplify 2) (("2" (skosimp) (("2" (inst - "u!1(i!1 + n!1)(x!1)") (("1" (assert) nil nil) ("2" (inst + "i!1+n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (grind) nil 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) (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) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (<= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (below_bounded const-decl "bool" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (image const-decl "set[R]" function_image nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (n!1 skolem-const-decl "nat" measure_space nil) (u!1 skolem-const-decl "measurable_bounded_below" measure_space nil) (i!1 skolem-const-decl "nat" measure_space nil) (x!1 skolem-const-decl "T" measure_space nil) (lower_bound const-decl "bool" bound_defs "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_IIntersection judgement-tcc nil measure_space_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IIntersection const-decl "set[T]" indexed_sets nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (inf const-decl "real" pointwise_convergence nil) (pointwise_bounded_below nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_bounded_below? const-decl "bool" pointwise_convergence nil) (measurable_ge formula-decl nil measure_space_def nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (sup_measurable 0 (sup_measurable-1 nil 3392309178 ("" (skosimp) (("" (rewrite "sup_inf_def") (("" (typepred "u!1") (("" (lemma "inf_measurable" ("u" "-u!1" "n" "n!1")) (("1" (lemma "opp_measurable" ("g" "inf(-u!1)(n!1)")) (("1" (expand "-" 1 1) (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (split) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (expand "measurable_bounded_above?") (("2" (expand "measurable_bounded_below?") (("2" (expand "pointwise_bounded_below?") (("2" (expand "pointwise_bounded_above?") (("2" (expand "pointwise?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "bounded_below?") (("2" (expand "bounded_above?") (("2" (skosimp) (("2" (assert) (("2" (inst + "-a!1") (("2" (skosimp) (("2" (inst - "x!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sup_inf_def formula-decl nil 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil) (pointwise_bounded_above? const-decl "bool" pointwise_convergence nil) (pointwise_bounded_above nonempty-type-eq-decl nil pointwise_convergence 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) (measurable_bounded_above? const-decl "bool" measure_space nil) (measurable_bounded_above nonempty-type-eq-decl nil measure_space nil) (T formal-type-decl nil measure_space nil) (- const-decl "sequence[[T -> real]]" pointwise_convergence nil) (measurable_bounded_below nonempty-type-eq-decl nil measure_space nil) (measurable_bounded_below? const-decl "bool" measure_space nil) (inf_measurable formula-decl nil measure_space nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (inf const-decl "real" pointwise_convergence nil) (pointwise_bounded_below nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_bounded_below? const-decl "bool" pointwise_convergence nil) (opp_measurable judgement-tcc nil measure_space_def nil) (bounded_below? const-decl "bool" real_fun_preds "reals/") (minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (bounded_above? const-decl "bool" real_fun_preds "reals/") (pointwise? const-decl "bool" pointwise_convergence nil) (opp_measurable application-judgement "measurable_function" measure_space nil) (real_minus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (pointwise_measurable 0 (pointwise_measurable-1 nil 3390466718 ("" (skosimp) (("" (lemma "pointwise_convergent_is_pointwise_bounded" ("x" "u!1")) (("1" (rewrite "pointwise_bounded_def") (("1" (flatten) (("1" (lemma "inf_pointwise_convergence_upto" ("p" "u!1" "f" "f!1")) (("1" (assert) (("1" (lemma "limsup_pointwise_convergence" ("b" "u!1")) (("1" (expand "pointwise_converges_upto?") (("1" (flatten) (("1" (lemma "sup_measurable" ("u" "inf(u!1)" "n" "0")) (("1" (case-replace "sup(inf(u!1))(0)=f!1") (("1" (apply-extensionality 1 :hide? t) (("1" (expand "pointwise_convergence?") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (lemma "hausdorff_convergence.unique_limit" ("u" "LAMBDA n: inf(u!1)(n)(x!1)" "l1" "limsup(u!1)(x!1)" "l2" "f!1(x!1)")) (("1" (assert) (("1" (expand "limsup") (("1" (expand "inf" 1) (("1" (assert) (("1" (expand "sup" 1) (("1" (expand "fullset") (("1" (case-replace "image[nat, real] (LAMBDA (m_1: nat): inf(image[nat, real] (LAMBDA m: u!1(m)(x!1), {m | m >= m_1})), {m_1: nat | TRUE})=image[nat, real](LAMBDA m: inf(u!1)(m)(x!1), {x: nat | TRUE})") (("1" (hide 2 3) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "image" 1 2) (("1" (expand "inf" 1) (("1" (expand "image" 1 3) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (split) (("1" (hide-all-but 1) (("1" (expand "image") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "u!1(m!1)(x!1)") (("1" (inst + "m!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_bounded_below?") (("2" (expand "pointwise?") (("2" (inst -7 "x!1") (("2" (hide-all-but (-7 1)) (("2" (expand "bounded_below?") (("2" (expand "image") (("2" (expand "below_bounded") (("2" (skosimp) (("2" (expand "lower_bound") (("2" (inst + "a!1") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (split) (("1" (hide-all-but 1) (("1" (expand "image") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "u!1(m!1)(x!1)") (("1" (inst + "m!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-7 1)) (("2" (expand "pointwise_bounded_below?") (("2" (expand "pointwise?") (("2" (inst - "x!1") (("2" (expand "bounded_below?") (("2" (expand "image") (("2" (expand "below_bounded") (("2" (skosimp) (("2" (expand "lower_bound") (("2" (inst + "a!1") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (inst - "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (lemma "inf_measurable" ("u" "u!1" "n" "x1!1")) (("1" (propax) nil nil) ("2" (hide-all-but (-5 1)) (("2" (expand "measurable_bounded_below?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "measurable_bounded_above?") (("2" (expand "pointwise_bounded_above?") (("2" (expand "pointwise?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "bounded_above?") (("2" (skosimp) (("2" (inst + "a!1") (("2" (skolem + ("n!1")) (("2" (expand "inf" 1) (("2" (typepred "inf(image[nat, real](LAMBDA m: u!1(m)(x!1), {m | m >= n!1}))") (("2" (expand "greatest_lower_bound") (("2" (flatten) (("2" (expand "lower_bound") (("2" (inst - "u!1(n!1)(x!1)") (("1" (inst -6 "n!1") (("1" (assert) nil nil)) nil) ("2" (expand "image") (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "pointwise_bounded_def") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "pointwise_convergent?") (("2" (inst + "f!1") nil nil)) nil)) nil)) 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) (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) (pointwise_convergent nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_convergent? const-decl "bool" pointwise_convergence nil) (sequence type-eq-decl nil sequences 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) (pointwise_convergent_is_pointwise_bounded judgement-tcc nil pointwise_convergence nil) (pointwise_converges_upto? const-decl "bool" pointwise_convergence nil) (sup_measurable formula-decl nil measure_space nil) (measurable_bounded_above? const-decl "bool" measure_space nil) (measurable_bounded_above nonempty-type-eq-decl nil measure_space nil) (inf const-decl "real" pointwise_convergence nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unique_limit formula-decl nil hausdorff_convergence "topology/") (limsup const-decl "real" pointwise_convergence nil) (nonneg_real nonempty-type-eq-decl nil real_types 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/") (fullset const-decl "set" sets nil) (bounded_below? const-decl "bool" real_fun_preds "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (pointwise? const-decl "bool" pointwise_convergence nil) (member const-decl "bool" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (u!1 skolem-const-decl "sequence[measurable_function[T, S]]" measure_space nil) (x!1 skolem-const-decl "T" measure_space nil) (set type-eq-decl nil sets nil) (image const-decl "set[R]" function_image nil) (nonempty? const-decl "bool" sets nil) (below_bounded const-decl "bool" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (pred type-eq-decl nil defined_types nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (<= const-decl "bool" reals nil) (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (TRUE const-decl "bool" booleans nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (= const-decl "[T, T -> boolean]" equalities nil) (pointwise_bounded_above? const-decl "bool" pointwise_convergence nil) (pointwise_bounded_above nonempty-type-eq-decl nil pointwise_convergence nil) (sup const-decl "real" pointwise_convergence nil) (inf_measurable formula-decl nil measure_space nil) (measurable_bounded_below? const-decl "bool" measure_space nil) (measurable_bounded_below nonempty-type-eq-decl nil measure_space nil) (bounded_above? const-decl "bool" real_fun_preds "reals/") (n!1 skolem-const-decl "nat" measure_space nil) (x!1 skolem-const-decl "T" measure_space nil) (pointwise_bounded nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_bounded? const-decl "bool" pointwise_convergence nil) (limsup_pointwise_convergence formula-decl nil pointwise_convergence nil) (pointwise_bounded_below nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_bounded_below? const-decl "bool" pointwise_convergence nil) (inf_pointwise_convergence_upto formula-decl nil pointwise_convergence nil) (pointwise_bounded_def formula-decl nil pointwise_convergence nil)) shostak)) (simple_TCC1 0 (simple_TCC1-1 nil 3390205059 ("" (expand "simple?") (("" (lemma "const_measurable" ("c" "0")) (("" (expand "const_fun") (("" (assert) (("" (hide -1) (("" (expand "fullset") (("" (expand "image") (("" (case "exists x: true") (("1" (lemma "extensionality" ("a" "{y: real | EXISTS (x_1: ({x: T | TRUE})): y = 0}" "b" "singleton(0)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (skolem - ("TT")) (("2" (skosimp) (("2" (expand "singleton") (("2" (expand "member") (("2" (case-replace "x!1=0") (("1" (assert) (("1" (inst + "TT") nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "extensionality" ("a" "{y: real | EXISTS (x_1: ({x: T | TRUE})): y = 0}" "b" "emptyset[real]")) (("2" (split -1) (("1" (assert) nil nil) ("2" (skosimp*) (("2" (expand "emptyset") (("2" (expand "member") (("2" (skosimp) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (const_measurable formula-decl nil measure_space nil) (image const-decl "set[R]" function_image nil) (emptyset const-decl "set" sets nil) (subset_algebra_emptyset name-judgement "(S)" measure_space_def nil) (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" real_topology "metric_space/") (finite_emptyset name-judgement "finite_set[real]" measure_space nil) (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (extensionality formula-decl nil sets_lemmas nil) (member const-decl "bool" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[nat]" countability "sets_aux/") (singleton_is_compact application-judgement "compact[real, metric_induced_topology]" measure_space_def nil) (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" measure_space nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (TRUE const-decl "bool" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-type-decl nil measure_space nil) (fullset const-decl "set" sets nil) (simple? const-decl "bool" measure_space nil)) nil)) (simple_is_measurable 0 (simple_is_measurable-1 nil 3426481705 ("" (skosimp) (("" (typepred "x!1") (("" (expand "simple?") (("" (flatten) nil nil)) nil)) nil)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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)) nil)) (simple_const 0 (simple_const-1 nil 3390271219 ("" (expand "simple?") (("" (skosimp) (("" (expand "fullset") (("" (expand "const_fun") (("" (expand "image") (("" (case "exists x: true") (("1" (lemma "extensionality" ("a" "{y: real | EXISTS (x_1: ({x: T | TRUE})): y = c!1}" "b" "singleton[real](c!1)")) (("1" (split -1) (("1" (replace -1) (("1" (assert) (("1" (lemma "const_measurable" ("c" "c!1")) (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (expand "member") (("2" (skosimp) (("2" (case-replace "x!1 = c!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "extensionality" ("a" "{y: real | EXISTS (x_1: ({x: T | TRUE})): y = c!1}" "b" "emptyset[real]")) (("2" (split -1) (("1" (replace -1) (("1" (assert) (("1" (lemma "const_measurable" ("c" "c!1")) (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "emptyset") (("2" (expand "member") (("2" (skolem - ("TT")) (("2" (inst + "TT") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((image const-decl "set[R]" function_image 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/") (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) (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) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (extensionality formula-decl nil sets_lemmas nil) (member const-decl "bool" sets nil) (const_measurable formula-decl nil measure_space nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" measure_space nil) (singleton_is_compact application-judgement "compact[real, metric_induced_topology]" measure_space_def nil) (T formal-type-decl nil measure_space nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (TRUE const-decl "bool" booleans nil) (fullset const-decl "set" sets nil) (simple? const-decl "bool" measure_space nil)) nil)) (nn_simple_TCC1 0 (nn_simple_TCC1-1 nil 3392524429 ("" (expand "nn_simple?") (("" (lemma "simple_const" ("c" "0")) (("" (expand "const_fun") (("" (propax) nil nil)) nil)) nil)) 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) (simple_const formula-decl nil measure_space nil) (nn_simple? const-decl "bool" measure_space nil)) nil)) (nn_simple_is_simple 0 (nn_simple_is_simple-1 nil 3392524429 ("" (skosimp) (("" (typepred "x!1") (("" (expand "nn_simple?") (("" (flatten) nil nil)) nil)) nil)) nil) ((nn_simple nonempty-type-eq-decl nil measure_space nil) (nn_simple? const-decl "bool" measure_space 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)) nil)) (simple_sq 0 (simple_sq-1 nil 3390272484 ("" (skosimp) (("" (typepred "h!1") (("" (expand "simple?") (("" (flatten) (("" (expand "sq") (("" (lemma "prod_measurable" ("g1" "h!1" "g2" "h!1")) (("" (expand "*") (("" (expand "sq") (("" (assert) (("" (hide -1 -2) (("" (lemma "finite_image[real,real]" ("f" "lambda y: y*y" "S" "image(h!1, fullset[T])")) (("" (lemma "extensionality" ("a" "image[real, real](LAMBDA y: y * y, image[T,real](h!1, fullset[T]))" "b" "image[T,real](LAMBDA (x: T): h!1(x) * h!1(x), fullset[T])")) (("" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "member") (("2" (skosimp*) (("2" (split) (("1" (skosimp*) (("1" (typepred "x!2") (("1" (skosimp) (("1" (inst + "x!3") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "h!1(x!2)") (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (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) (prod_measurable judgement-tcc nil measure_space nil) (sq const-decl "nonneg_real" sq "reals/") (extensionality formula-decl nil sets_lemmas nil) (x!2 skolem-const-decl "({x | TRUE})" measure_space nil) (h!1 skolem-const-decl "simple" measure_space nil) (= const-decl "[T, T -> boolean]" equalities nil) (TRUE const-decl "bool" booleans nil) (member const-decl "bool" sets nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (fullset const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (finite_image judgement-tcc nil function_image_aux nil) (real_times_real_is_real application-judgement "real" reals nil) (subset_algebra_fullset name-judgement "(S)" measure_space nil) (measurable_fullset name-judgement "measurable_set[T, S]" measure_space nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (sq_measurable application-judgement "measurable_function[T, S]" measure_space nil)) nil)) (simple_add 0 (simple_add-1 nil 3390205059 ("" (skosimp) (("" (typepred "h1!1") (("" (typepred "h2!1") (("" (expand "simple?") (("" (flatten) (("" (hide -1 -3) (("" (lemma "is_finite_cross[(fullset[(image(h1!1, fullset[T]))]),(fullset[(image(h2!1, fullse (("" (split -1) (("1" (lemma "finite_image[[real,real],real]" ("f" "lambda (x,y:real): x+y" "S" "fullset[[((fullset[(image(h1!1, fullset[T]))])), ((fullset[(image(h2!1, fullset[T]))]))]]")) (("1" (case "subset?(image((+[T])(h1!1, h2!1), fullset[T]),image[[real, real], real](LAMBDA extend [[real, real], [((fullset[(image[T, real](h1!1, fullset[T]))])), ((fullset[(image[T, real](h2!1, fullset[T]))]))], bool, FALSE] (fullset [[((fullset[(image(h1!1, fullset[T]))])), ((fullset[(image(h2!1, fullset[T]))]))]])))") (("1" (lemma "finite_subset[real]" ("s" "image((+[T])(h1!1, h2!1), fullset[T])" "A" "image[[real, real], real] (LAMBDA (x, y: real): x + y, extend [[real, real], [((fullset[(image[T, real](h1!1, fullset[T]))])), ((fullset[(image[T, real](h2!1, fullset[T]))]))], bool, FALSE] (fullset [[((fullset[(image(h1!1, fullset[T]))])), ((fullset[(image(h2!1, fullset[T]))]))]]))")) (("1" (assert) nil nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (inst + "(h1!1(x!2),h2!1(x!2))") (("2" (prop) (("1" (inst + "x!2") nil nil) ("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 2) (("2" (expand "extend") (("2" (expand "is_finite") (("2" (expand "is_finite_type") (("2" (skosimp*) (("2" (inst + "N!1" "g!1") (("1" (expand "restrict") (("1" (expand "injective?") (("1" (skosimp*) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "is_finite_type") (("2" (expand "is_finite") (("2" (skosimp) (("2" (inst + "N!1" "f!1") (("2" (expand "restrict") (("2" (expand "injective?") (("2" (skosimp*) (("2" (inst - "x1!1" "x2!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-1 1)) (("3" (expand "is_finite") (("3" (skosimp) (("3" (expand "is_finite_type") (("3" (inst + "N!1" "f!1") (("3" (expand "restrict") (("3" (expand "injective?") (("3" (skosimp*) (("3" (inst - "x1!1" "x2!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (sum_measurable application-judgement "measurable_function[T, S]" measure_space nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (restrict const-decl "R" restrict nil) (is_finite_type const-decl "bool" finite_sets nil) (subset? const-decl "bool" sets nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (finite_subset formula-decl nil finite_sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (TRUE const-decl "bool" booleans nil) (h2!1 skolem-const-decl "simple" measure_space nil) (x!2 skolem-const-decl "(fullset[T])" measure_space nil) (h1!1 skolem-const-decl "simple" measure_space nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (real_plus_real_is_real application-judgement "real" reals nil) (finite_image judgement-tcc nil function_image_aux nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (subset_algebra_fullset name-judgement "(S)" measure_space nil) (measurable_fullset name-judgement "measurable_set[T, S]" measure_space nil) (is_finite_cross formula-decl nil finite_cross "finite_sets/") (set type-eq-decl nil sets nil) (image const-decl "set[R]" function_image nil) (fullset const-decl "set" sets nil)) nil)) (simple_scal 0 (simple_scal-1 nil 3390205059 ("" (skosimp) (("" (typepred "h!1") (("" (expand "simple?") (("" (flatten) (("" (hide -1) (("" (lemma "finite_image[real,real]" ("f" "lambda y: c!1*y" "S" "image(h!1, fullset[T])")) (("1" (lemma "extensionality[real]" ("a" "image[real, real](LAMBDA y: c!1 * y, image[T,real](h!1, fullset[T]))" "b" "image[T,real](*[T](c!1, h!1), fullset[T])")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "member") (("2" (skosimp) (("2" (split) (("1" (skosimp*) (("1" (typepred "x!2") (("1" (skosimp) (("1" (inst + "x!3") (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "*") (("2" (inst + "h!1(x!2)") (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (fullset const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (finite_image judgement-tcc nil function_image_aux nil) (real_times_real_is_real application-judgement "real" reals nil) (measurable_fullset name-judgement "measurable_set[T, S]" measure_space nil) (subset_algebra_fullset name-judgement "(S)" measure_space nil) (member const-decl "bool" sets nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (x!2 skolem-const-decl "({x | TRUE})" measure_space nil) (h!1 skolem-const-decl "simple" measure_space nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (extensionality formula-decl nil sets_lemmas nil) (scal_measurable application-judgement "measurable_function[T, S]" measure_space nil)) nil)) (simple_neg 0 (simple_neg-1 nil 3390205059 ("" (skosimp) (("" (typepred "h!1") (("" (expand "simple?") (("" (flatten) (("" (hide -1) (("" (expand "fullset") (("" (expand "image") (("" (rewrite "is_finite_surj" -1 :dir rl) (("" (rewrite "is_finite_surj" 1 :dir rl) (("" (skosimp*) (("" (inst + "N!1" "lambda (n:below[N!1]): -f!1(n)") (("1" (expand "surjective?") (("1" (skosimp) (("1" (inst - "-y!1") (("1" (skosimp) (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "y!1") (("2" (skosimp) (("2" (expand "-") (("2" (inst + "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "f!1(n!1)") (("2" (skosimp) (("2" (inst + "x!1") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (fullset const-decl "set" sets nil) (is_finite_surj formula-decl nil finite_sets nil) (set type-eq-decl nil sets nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (surjective? const-decl "bool" functions nil) (y!1 skolem-const-decl "({y: real | EXISTS (x_1: ({x | TRUE})): y = (-h!1)(x_1)})" measure_space nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (N!1 skolem-const-decl "nat" measure_space nil) (below type-eq-decl nil nat_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (h!1 skolem-const-decl "simple" measure_space nil) (f!1 skolem-const-decl "[below[N!1] -> ({y: real | EXISTS (x_1: ({x | TRUE})): y = h!1(x_1)})]" measure_space nil) (minus_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (image const-decl "set[R]" function_image nil) (opp_measurable application-judgement "measurable_function" measure_space nil)) nil)) (simple_diff 0 (simple_diff-1 nil 3390271654 ("" (skosimp) (("" (lemma "simple_neg" ("h" "h2!1")) (("" (lemma "simple_add" ("h1" "h1!1" "h2" "-h2!1")) (("" (expand "+") (("" (expand "-") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (simple_neg judgement-tcc nil measure_space nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (minus_real_is_real application-judgement "real" reals nil) (real_plus_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) (simple_neg application-judgement "simple" measure_space nil) (simple_add judgement-tcc nil measure_space nil) (- const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (simple_abs 0 (simple_abs-1 nil 3390205059 ("" (skosimp) (("" (typepred "h!1") (("" (expand "simple?") (("" (flatten) (("" (hide -1) (("" (expand "fullset") (("" (expand "image") (("" (rewrite "is_finite_surj" -1 :dir rl) (("" (rewrite "is_finite_surj" 1 :dir rl) (("" (skosimp) (("" (inst + "N!1" "_") (("" (inst + "lambda (n:below[N!1]): abs(f!1(n))") (("1" (expand "surjective?") (("1" (skosimp) (("1" (typepred "y!1") (("1" (skosimp) (("1" (expand "abs" -1) (("1" (replace -1) (("1" (inst - "h!1(x!1)") (("1" (skosimp) (("1" (inst + "x!2") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "f!1(n!1)") (("2" (skosimp) (("2" (inst + "x!1") (("2" (assert) (("2" (expand "abs" 1 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (fullset const-decl "set" sets nil) (is_finite_surj formula-decl nil finite_sets nil) (set type-eq-decl nil sets nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (f!1 skolem-const-decl "[below[N!1] -> ({y: real | EXISTS (x_1: ({x | TRUE})): y = h!1(x_1)})]" measure_space nil) (h!1 skolem-const-decl "simple" measure_space 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) (below type-eq-decl nil nat_types nil) (N!1 skolem-const-decl "nat" measure_space nil) (< const-decl "bool" reals nil) (x!1 skolem-const-decl "({x | TRUE})" measure_space nil) (surjective? const-decl "bool" functions nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= 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/") (image const-decl "set[R]" function_image nil) (abs_measurable application-judgement "measurable_function[T, S]" measure_space nil)) nil)) (simple_min 0 (simple_min-1 nil 3390205059 ("" (skosimp) (("" (lemma "simple_add" ("h1" "h1!1" "h2" "h2!1")) (("" (lemma "simple_diff" ("h1" "h1!1" "h2" "h2!1")) (("" (lemma "simple_abs" ("h" "(-[T])(h1!1, h2!1)")) (("" (lemma "simple_diff" ("h1" "(+[T])(h1!1, h2!1)" "h2" "abs((-[T])(h1!1, h2!1))")) (("" (lemma "simple_scal" ("c" "1/2" "h" "(-[T])((+[T])(h1!1, h2!1), abs((-[T])(h1!1, h2!1)))")) (("" (expand "*") (("" (expand "-") (("" (expand "+") (("" (expand "abs" -1) (("" (expand "min") (("" (lemma "extensionality" ("f" "(LAMBDA (x: T): h1!1(x) * (1 / 2) + h2!1(x) * (1 / 2) - abs(h1!1(x) - h2!1(x)) * (1 / 2))" "g" "LAMBDA (x: T): min(h1!1(x), h2!1(x))")) (("" (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)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (simple_add judgement-tcc nil measure_space nil) (simple_diff application-judgement "simple" measure_space nil) (simple_abs judgement-tcc nil measure_space nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (simple_scal judgement-tcc nil measure_space nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (extensionality formula-decl nil functions nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (min const-decl "[T -> real]" real_fun_ops_aux "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (simple_abs application-judgement "simple" measure_space nil) (simple_add application-judgement "simple" measure_space nil) (simple_diff judgement-tcc nil measure_space nil)) nil)) (simple_max 0 (simple_max-1 nil 3390205059 ("" (skosimp) (("" (lemma "simple_neg" ("h" "h1!1")) (("" (lemma "simple_neg" ("h" "h2!1")) (("" (lemma "simple_min" ("h1" "-h1!1" "h2" "-h2!1")) (("" (lemma "simple_neg" ("h" "min(-h1!1,-h2!1)")) (("" (expand "-") (("" (expand "min") (("" (expand "max") (("" (case-replace "(LAMBDA (x_1: T): -min(-h1!1(x_1), -h2!1(x_1)))=(LAMBDA (x: T): max(h1!1(x), h2!1(x)))" (("" (apply-extensionality :hide? t) (("" (hide-all-but 1) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (simple_neg judgement-tcc nil measure_space nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (simple_min judgement-tcc nil measure_space nil) (simple_neg application-judgement "simple" measure_space nil) (max const-decl "[T -> real]" real_fun_ops_aux "reals/") (real_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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (>= const-decl "bool" reals 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) (- const-decl "[numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (min const-decl "[T -> real]" real_fun_ops_aux "reals/") (simple_min application-judgement "simple" measure_space nil)) nil)) (simple_maximum 0 (simple_maximum-1 nil 3409894810 ("" (induct "n") (("1" (expand "maximum" 1) (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (expand "maximum" 1) (("2" (inst - "v!1") (("2" (rewrite "simple_max") nil nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (maximum_measurable application-judgement "measurable_function[T, S]" measure_space nil) (simple_max judgement-tcc nil measure_space nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (max_measurable application-judgement "measurable_function[T, S]" measure_space 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) (simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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)) (simple_minimum 0 (simple_minimum-1 nil 3409894810 ("" (induct "n") (("1" (expand "minimum" 1) (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (expand "minimum" 1) (("2" (inst - "v!1") (("2" (rewrite "simple_min") nil nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (minimum_measurable application-judgement "measurable_function[T, S]" measure_space nil) (simple_min judgement-tcc nil measure_space nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (min_measurable application-judgement "measurable_function[T, S]" 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) (simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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)) (simple_plus 0 (simple_plus-1 nil 3390205059 ("" (skosimp) (("" (lemma "simple_const" ("c" "0")) (("" (expand "const_fun") (("" (lemma "simple_max" ("h1" "h!1" "h2" "LAMBDA (x: T): 0")) (("1" (expand "plus") (("1" (expand "max" -) (("1" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) 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) (simple_const formula-decl nil measure_space nil) (plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (max const-decl "[T -> real]" real_fun_ops_aux "reals/") (simple_max judgement-tcc nil measure_space nil) (T formal-type-decl nil measure_space nil) (bool nonempty-type-eq-decl nil booleans nil) (simple? const-decl "bool" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil)) nil)) (simple_minus 0 (simple_minus-1 nil 3390205059 ("" (skosimp) (("" (lemma "simple_const" ("c" "0")) (("" (expand "const_fun") (("" (lemma "simple_min" ("h1" "h!1" "h2" "LAMBDA (x: T): 0")) (("1" (expand "minus") (("1" (expand "min" -1) (("1" (lemma "simple_neg" ("h" "LAMBDA (x_1: T): min(h!1(x_1), 0)")) (("1" (expand "-") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) 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) (simple_const formula-decl nil measure_space nil) (minus_real_is_real application-judgement "real" reals nil) (minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (simple_neg judgement-tcc nil measure_space nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (min const-decl "[T -> real]" real_fun_ops_aux "reals/") (simple_min judgement-tcc nil measure_space nil) (T formal-type-decl nil measure_space nil) (bool nonempty-type-eq-decl nil booleans nil) (simple? const-decl "bool" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil)) nil)) (simple_times 0 (simple_times-1 nil 3390205059 ("" (skosimp) (("" (lemma "simple_add" ("h1" "h1!1" "h2" "h2!1")) (("" (lemma "simple_diff" ("h1" "h1!1" "h2" "h2!1")) (("" (lemma "simple_sq" ("h" "(+[T])(h1!1, h2!1)")) (("" (lemma "simple_sq" ("h" "(-[T])(h1!1, h2!1)")) (("" (lemma "simple_diff" ("h1" "sq[T]((+[T])(h1!1, h2!1))" "h2" "sq[T]((-[T])(h1!1, h2!1))")) (("" (lemma "simple_scal" ("c" "1/4" "h" "(-[T])(sq[T]((+[T])(h1!1, h2!1)), sq[T]((-[T])(h1!1, h2!1)))")) (("" (lemma "extensionality" ("f" "*[T] (1 / 4, (-[T]) (sq[T]((+[T])(h1!1, h2!1)), sq[T]((-[T])(h1!1, h2!1))))" "g" "*[T](h1!1, h2!1)")) (("" (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) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (simple_add judgement-tcc nil measure_space nil) (simple_add application-judgement "simple" measure_space nil) (simple_sq judgement-tcc nil measure_space nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (simple_sq application-judgement "simple" measure_space nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sq const-decl "[T -> nnreal]" real_fun_ops_aux "reals/") (extensionality formula-decl nil functions nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (prod_measurable application-judgement "measurable_function[T, S]" measure_space nil) (simple_scal application-judgement "simple" measure_space nil) (/ 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) (simple_scal judgement-tcc nil measure_space nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (simple_diff application-judgement "simple" measure_space nil) (simple_diff judgement-tcc nil measure_space nil)) nil)) (simple_expt_nat 0 (simple_expt_nat-1 nil 3390205059 ("" (skolem + ("h!1" "_")) (("" (induct "n") (("1" (expand "expt") (("1" (expand "expt") (("1" (rewrite "simple_const") nil nil)) nil)) nil) ("2" (skosimp) (("2" (expand "expt" 1) (("2" (lemma "simple_times" ("h1" "h!1" "h2" "expt[T](h!1, j!1)")) (("1" (expand "*" -1) (("1" (expand "expt" -1) (("1" (expand "expt" 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil measure_space nil) (simple? const-decl "bool" measure_space nil) (expt const-decl "[T -> real]" real_fun_power "power/") (simple nonempty-type-eq-decl nil measure_space nil) (nat_induction formula-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (simple_const formula-decl nil measure_space nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (simple_times judgement-tcc nil measure_space nil) (expt_nat_measurable application-judgement "measurable_function[T, S]" measure_space nil)) nil)) (simple_expt_TCC1 0 (simple_expt_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_simple? const-decl "bool" measure_space nil) (nn_simple nonempty-type-eq-decl nil measure_space nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (simple? const-decl "bool" measure_space nil) (is_finite const-decl "bool" finite_sets nil) (injective? const-decl "bool" functions 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) (subset_algebra_fullset name-judgement "(S)" measure_space nil) (measurable_fullset name-judgement "measurable_set[T, S]" 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)) (simple_expt 0 (simple_expt-1 nil 3430677936 ("" (skosimp) (("" (expand "simple?") (("" (typepred "h!1") (("" (typepred "a!1") (("" (lemma "expt_measurable" ("g" "h!1" "a" "a!1")) (("1" (replace -1) (("1" (hide -1) (("1" (expand "nn_simple?") (("1" (flatten) (("1" (expand "simple?") (("1" (flatten) (("1" (hide -4 -1) (("1" (expand "fullset") (("1" (expand "image") (("1" (lemma "finite_image[nnreal,real]" ("f" "lambda (x:nnreal): x^a!1" "S" "{y: nnreal | EXISTS (x_1: ({x: T | TRUE})): y = h!1(x_1)}")) (("1" (hide -4) (("1" (expand "image") (("1" (case-replace "{y_1: real | EXISTS (x_1: ({y: nnreal | EXISTS (x_1: ({x: T | TRUE})): y = h!1(x_1)})): y_1 = x_1 ^ a!1}={y: real | EXISTS (x_1: ({x: T | TRUE})): y = (^[T](h!1, a!1))(x_1)}") (("1" (hide -1 2) (("1" (apply-extensionality :hide? t) (("1" (case-replace "EXISTS (x_1: ({x: T | TRUE})): x!1 = ^[T](h!1, a!1)(x_1)") (("1" (skosimp) (("1" (expand "^" -1) (("1" (inst + "h!1(x!2)") (("1" (split) (("1" (inst - "x!2") (("1" (assert) nil nil)) nil) ("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "x!2") (("2" (skosimp) (("2" (replace -2) (("2" (expand "^" 1) (("2" (replace -3) (("2" (inst + "x!3") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (skosimp) (("3" (inst - "x1!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (skosimp) (("2" (inst - "x1!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (skosimp) (("2" (inst - "x1!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "is_finite") (("2" (skosimp) (("2" (inst + "N!1" "f!1") (("2" (expand "restrict") (("2" (expand "injective?") (("2" (skosimp) (("2" (inst - "x1!1" "x2!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nn_simple?") (("2" (expand "simple?") (("2" (expand "nn_measurable?") (("2" (flatten) (("2" (replace -3) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple? const-decl "bool" measure_space nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (image const-decl "set[R]" function_image nil) (injective? const-decl "bool" functions nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (restrict const-decl "R" restrict nil) (^ const-decl "[T -> nnreal]" real_fun_power "power/") (h!1 skolem-const-decl "nn_simple" measure_space nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (x!2 skolem-const-decl "({x: T | TRUE})" measure_space nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (finite_image judgement-tcc nil function_image_aux nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "nnreal" real_expt "power/") (nnreal type-eq-decl nil real_types nil) (fullset const-decl "set" sets nil) (expt_measurable judgement-tcc nil measure_space nil) (nn_measurable? const-decl "bool" measure_space nil) (nn_measurable nonempty-type-eq-decl nil 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) (nn_simple? const-decl "bool" measure_space nil) (nn_simple nonempty-type-eq-decl nil measure_space nil)) nil)) (phi_is_simple 0 (phi_is_simple-1 nil 3390786084 ("" (skosimp) (("" (expand "simple?") (("" (split) (("1" (rewrite "measurable_def2") (("1" (skosimp) (("1" (expand "phi") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (case "i!1(0)") (("1" (case "i!1(1)") (("1" (assert) (("1" (lemma "measurable_fullset") (("1" (expand "fullset") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "measurable_complement" ("a" "X!1")) (("1" (case-replace "{x_1: T | IF X!1(x_1) THEN FALSE ELSE TRUE ENDIF}=complement[T](X!1)") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "i!1(1)") (("1" (case-replace "{x_1: T | IF X!1(x_1) THEN i!1(1) ELSE i!1(0) ENDIF}= X!1") (("1" (assert) nil nil) ("2" (hide 3) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "measurable_emptyset") (("2" (expand "emptyset") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_subset[real]") (("2" (inst - "add[real](1,singleton[real](0))" "image[T,real](phi(X!1), fullset[T])") (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple? const-decl "bool" measure_space nil) (finite_subset formula-decl nil finite_sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[nat]" countability "sets_aux/") (singleton_is_compact application-judgement "compact[real, metric_induced_topology]" measure_space_def nil) (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" measure_space nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (measurable_fullset name-judgement "measurable_set[T, S]" measure_space nil) (subset_algebra_fullset name-judgement "(S)" measure_space nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (image const-decl "set[R]" function_image nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (nonempty? const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (nonempty_add_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (add_preserves_has_least application-judgement "(LAMBDA (S: set[nat]): has_least?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (add_preserves_has_greatest application-judgement "(LAMBDA (S: set[nat]): has_greatest?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (add_preserves_greatest_bounded_below application-judgement "(LAMBDA (S: set[nat]): greatest_bounded_below?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (add_preserves_least_bounded_above application-judgement "(LAMBDA (S: set[nat]): least_bounded_above?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (add_preserves_tightly_bounded application-judgement "(LAMBDA (S: set[nat]): tightly_bounded?(S, restrict[[real, real], [nat, nat], boolean](<=)))" countability "sets_aux/") (nonempty_add_finite application-judgement "non_empty_finite_set[nat]" countability "sets_aux/") (measurable_def2 formula-decl nil measure_space_def 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) (set type-eq-decl nil sets nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phi const-decl "nat" measure_space nil) (T formal-type-decl nil measure_space 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 nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" measure_space 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) (measurable_set? const-decl "bool" measure_space_def nil) (fullset const-decl "set" sets nil) (measurable_complement judgement-tcc nil measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (subset_algebra_complement application-judgement "(S)" measure_space nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (FALSE const-decl "bool" booleans nil) (TRUE const-decl "bool" booleans nil) (complement const-decl "set" sets nil) (open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (ball const-decl "set[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) (= const-decl "[T, T -> boolean]" equalities nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (inverse_image const-decl "set[D]" function_image nil)) nil)) (simple_def1 0 (simple_def1-1 nil 3390362095 ("" (expand "simple?") (("" (skosimp) (("" (case-replace "is_finite(image(f!1, fullset[T]))") (("1" (split) (("1" (flatten) (("1" (skosimp) (("1" (typepred "y!1") (("1" (expand "measurable_function?") (("1" (inst - "singleton[real](y!1)") (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (lemma "extensionality" ("a" "{x: T | f!1(x) = y!1}" "b" "{x | y!1 = f!1(x)}")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "singleton_is_borel" ("x" "y!1")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "measurable_function?") (("2" (skosimp) (("2" (typepred "B!1") (("2" (name-replace "IMAGE" "image(f!1, fullset[T])") (("2" (case "borel?[real, metric_induced_topology](IMAGE)") (("1" (lemma "intersection_is_borel" ("a" "B!1" "b" "IMAGE")) (("1" (hide -2 -3) (("1" (case-replace "inverse_image[T,real](f!1, B!1) = Union(image[real,set[T]](lambda y: inverse_image[T (("1" (hide -1) (("1" (typepred "S") (("1" (expand "sigma_algebra?") (("1" (flatten) (("1" (expand "sigma_algebra_union?") (("1" (inst - "image[real, set[T]] (LAMBDA y: inverse_image[T, real] (f!1, singleton[real](y)), intersection[real](B!1, IMAGE))") (("1" (split -3) (("1" (expand "measurable_set?") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (lemma "countable_image[real,set[T]]" ("f" "LAMBDA y: inverse_image[T, real](f!1, singleton[real](y))" "S" "intersection[real](B!1, IMAGE)")) (("2" (split -1) (("1" (name-replace "FF" "LAMBDA y: inverse_image[T, real](f!1, singleton[real](y))") (("1" (name-replace "BB" "intersection[real](B!1, IMAGE)") (("1" (expand "image" -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (lemma "finite_countable" ("x" "intersection[real](B!1, IMAGE)")) (("1" (propax) nil nil) ("2" (assert) (("2" (lemma "finite_intersection1[real]" ("s" "B!1" "A" "IMAGE")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (expand "member") (("3" (typepred "x!1") (("3" (expand "intersection") (("3" (expand "singleton") (("3" (expand "inverse_image") (("3" (expand "member") (("3" (expand "image") (("3" (skosimp*) (("3" (typepred "x!2") (("3" (inst - "x!2") (("1" (expand "measurable_set?") (("1" (lemma "extensionality" ("a" "{x_1: T | x!2 = f!1(x_1)}" "b" "{x: T | f!1(x) = x!2}")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "IMAGE") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (case-replace "inverse_image[T, real](f!1, B!1)(x!1)") (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (expand "Union") (("1" (inst + "inverse_image[T,real](f!1,singleton[real](f!1(x!1)))") (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (expand "image") (("2" (inst + "f!1(x!1)") (("2" (expand "intersection") (("2" (assert) (("2" (expand "IMAGE") (("2" (expand "fullset") (("2" (expand "image") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "singleton") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (expand "image") (("2" (skosimp) (("2" (replace -1) (("2" (assert) (("2" (hide -1) (("2" (typepred "x!2") (("2" (replace -2) (("2" (expand "intersection") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (case "forall Y,n: is_finite(Y) & card(Y) <= n => borel?[real, metric_induced_topology]( (("1" (inst - "IMAGE" "card(IMAGE)") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (induct "n") (("1" (skosimp*) (("1" (expand "<=") (("1" (split) (("1" (assert) nil nil) ("2" (rewrite "card_is_0") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "<=" -3) (("2" (split -3) (("1" (inst - "Y!1") (("1" (assert) nil nil)) nil) ("2" (lemma "nonempty_card[real]" ("S" "Y!1")) (("2" (assert) (("2" (lemma "card_rest[real]" ("S" "Y!1")) (("2" (lemma "choose_rest[real]" ("a" "Y!1")) (("2" (expand "nonempty?") (("2" (assert) (("2" (replace -1 2 rl) (("2" (replace -3 -2) (("2" (hide 1 -1 -3) (("2" (assert) (("2" (inst - "rest[real](Y!1)") (("2" (split -2) (("1" (rewrite "add_as_union") (("1" (rewrite "union_is_borel") (("1" (hide 2 -1) (("1" (rewrite "singleton_is_borel") nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "finite_rest[real]" ("A" "Y!1")) (("2" (propax) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "metric_induced_topology[real, (LAMBDA (x, y: real): abs(x - y))]") (("3" (expand "hausdorff_space?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "metric_induced_topology[real, (LAMBDA (x, y: real): abs(x - y))]") (("3" (expand "hausdorff_space?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "metric_induced_topology[real, (LAMBDA (x, y: real): abs(x - y))]") (("3" (expand "hausdorff_space?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((measurable_function? const-decl "bool" measure_space_def nil) (member const-decl "bool" sets nil) (real_minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (extensionality formula-decl nil sets_lemmas nil) (inverse_image const-decl "set[D]" function_image nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (borel nonempty-type-eq-decl nil borel nil) (borel? const-decl "sigma_algebra" borel 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) (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) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" measure_space nil) (singleton_is_compact application-judgement "compact[real, metric_induced_topology]" measure_space_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" real_topology "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[real]" real_topology "metric_space/") (TRUE const-decl "bool" booleans nil) (x!1 skolem-const-decl "T" measure_space nil) (sigma_algebra_union? const-decl "bool" subset_algebra_def nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (measurable_set? const-decl "bool" measure_space_def nil) (countable_image formula-decl nil countable_image "sets_aux/") (finite_intersection1 judgement-tcc nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (finite_countable judgement-tcc nil countable_props "sets_aux/") (image const-decl "set[R]" function_image nil) (f!1 skolem-const-decl "[T -> real]" measure_space nil) (B!1 skolem-const-decl "borel[real, metric_induced_topology]" measure_space nil) (IMAGE skolem-const-decl "set[real]" measure_space nil) (x!2 skolem-const-decl "({x | B!1(x) AND IMAGE(x)})" measure_space nil) (S formal-const-decl "sigma_algebra" measure_space nil) (Union const-decl "set" sets nil) (intersection const-decl "set" sets nil) (intersection_is_borel formula-decl nil borel nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (card_is_0 formula-decl nil finite_sets nil) (subset_algebra_emptyset name-judgement "(S)" measure_space_def nil) (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" real_topology "metric_space/") (finite_emptyset name-judgement "finite_set[real]" measure_space nil) (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty_card formula-decl nil finite_sets nil) (card_rest formula-decl nil finite_sets nil) (nonempty? const-decl "bool" sets nil) (rest const-decl "set" sets nil) (finite_rest judgement-tcc nil finite_sets nil) (choose const-decl "(p)" sets nil) (add_as_union formula-decl nil sets_lemmas nil) (nonempty_union2 application-judgement "(nonempty?)" sets nil) (union_is_borel formula-decl nil borel nil) (int_minus_int_is_int application-judgement "int" integers nil) (choose_rest formula-decl nil sets_lemmas nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (fullset const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (T formal-type-decl nil measure_space nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets 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) (measurable_fullset name-judgement "measurable_set[T, S]" measure_space nil) (subset_algebra_fullset name-judgement "(S)" measure_space nil) (simple? const-decl "bool" measure_space nil)) shostak)) (simple_def2 0 (simple_def2-1 nil 3390408417 ("" (skosimp) (("" (rewrite "simple_def1") (("" (split) (("1" (skosimp*) (("1" (name "PP" "image[real,set[T]](lambda y: inverse_image[T,real](f!1,singleton[real](y)),image[ (("1" (inst + "PP") (("1" (split 1) (("1" (expand "measurable_set?") (("1" (expand "every") (("1" (skosimp) (("1" (typepred "x!1") (("1" (replace -2 -1 rl) (("1" (expand "fullset" -1) (("1" (expand "singleton" -1) (("1" (expand "inverse_image" -1) (("1" (expand "member") (("1" (expand "image" -1) (("1" (skosimp) (("1" (typepred "x!2") (("1" (skosimp) (("1" (replace -1) (("1" (inst -5 "f!1(x!3)") (("1" (lemma "extensionality" ("a" "{x | f!1(x!3) = f!1(x)}" "b" "{x: T | f!1(x) = f!1(x!3)}")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (expand "image") (("2" (inst + "x!3") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "every") (("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "PP") (("2" (hide -2) (("2" (expand "constant_over?") (("2" (expand "fullset") (("2" (expand "singleton") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (expand "image") (("2" (skosimp*) (("2" (typepred "x!2") (("2" (skosimp) (("2" (inst + "x!2") (("2" (skosimp) (("2" (typepred "x!4") (("2" (replace -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "finite_image[real,set[T]]" ("f" "LAMBDA y: inverse_image[T, real](f!1, singleton[real](y))" "S" "image[T, real](f!1, fullset[T])")) (("1" (replace -2) (("1" (expand "finite_partition?") (("1" (assert) (("1" (expand "partition?") (("1" (split) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "fullset") (("1" (expand "Union") (("1" (name "FF" "LAMBDA y: inverse_image[T, real](f!1, singleton[real](y))") (("1" (replace -1) (("1" (inst + "FF(f!1(x!1))") (("1" (expand "FF" 1) (("1" (expand "singleton") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "PP" 1) (("2" (expand "image") (("2" (expand "FF" 1) (("2" (inst + "f!1(x!1)") (("2" (inst + "x!1") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (expand "PP") (("2" (expand "image" -1 1) (("2" (expand "image" -2 1) (("2" (skosimp*) (("2" (case-replace "x!2=x!3") (("1" (assert) nil nil) ("2" (expand "singleton") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (replace -1) (("2" (replace -2) (("2" (hide 2 -1 -2) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "P!1") (("2" (split) (("1" (expand "finite_partition?") (("1" (flatten) (("1" (expand "partition?") (("1" (flatten) (("1" (case "exists x: true") (("1" (name "PP" "{X | P!1(X) & nonempty?(X)}") (("1" (case "nonempty?(PP) & subset?(PP,P!1)") (("1" (flatten) (("1" (case "Union(PP)=fullset[T]") (("1" (case "forall (X:(PP)): singleton?(image(f!1,X))") (("1" (name "FF" "lambda (X:(PP)): choose[real](image[T,real](f!1,X))") (("1" (case-replace "image[T,real](f!1,fullset[T]) = image(FF,PP)") (("1" (hide -1) (("1" (lemma "finite_image[(PP),real]" ("f" "FF" "S" "PP")) (("1" (propax) nil nil) ("2" (hide-all-but (-5 -10 1)) (("2" (lemma "finite_subset[set[T]]" ("s" "PP" "A" "P!1")) (("1" (assert) (("1" (hide -2 -3) (("1" (expand "restrict") (("1" (expand "is_finite") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (replace -3 1 rl) (("2" (expand "restrict") (("2" (expand "image") (("2" (case-replace "EXISTS (x: (Union(PP))): x!1 = f!1(x)") (("1" (skosimp) (("1" (typepred "x!2") (("1" (expand "Union") (("1" (skosimp) (("1" (inst + "a!1") (("1" (hide -3) (("1" (expand "FF") (("1" (typepred "choose[real](image[T, real](f!1, a!1))") (("1" (name-replace "XX" "choose[real](image[T, real](f!1, a!1))") (("1" (expand "image") (("1" (skosimp) (("1" (typepred "x!3") (("1" (typepred "a!1") (("1" (expand "subset?") (("1" (inst -9 "a!1") (("1" (assert) (("1" (expand "every") (("1" (inst -16 "a!1") (("1" (expand "constant_over?") (("1" (skosimp*) (("1" (inst-cp -15 "x!2") (("1" (inst -15 "x!3") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp*) (("2" (typepred "x!2") (("2" (expand "subset?") (("2" (inst -7 "x!2") (("2" (assert) (("2" (expand "every" -13) (("2" (inst -13 "x!2") (("2" (expand "constant_over?") (("2" (skosimp) (("2" (expand "FF") (("2" (hide -3) (("2" (typepred "choose[real](image[T, real](f!1, x!2))") (("2" (replace -3 * rl) (("2" (expand "image") (("2" (skosimp) (("2" (inst + "x!4") (("2" (replace -5 1) (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "X!1") (("2" (hide-all-but (-1 1)) (("2" (expand "singleton?") (("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "every") (("2" (expand "subset?") (("2" (inst -4 "X!1") (("2" (assert) (("2" (inst -11 "X!1") (("2" (expand "constant_over?") (("2" (skolem! -11) (("2" (expand "image") (("2" (expand "singleton?") (("2" (inst + "y!1") (("1" (skosimp) (("1" (typepred "y!2") (("1" (skolem!) (("1" (typepred "x!1") (("1" (inst -13 "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "PP" -1) (("2" (expand "nonempty?") (("2" (expand "empty?" 2) (("2" (skolem! 2) (("2" (inst + "x!1") (("1" (assert) (("1" (inst -10 "x!1") nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 -1 -2 1)) (("2" (apply-extensionality 1 :hide? t) (("2" (lemma "extensionality_postulate" ("f" "Union(P!1)" "g" "fullset[T]")) (("2" (replace -1 -4 rl) (("2" (inst -4 "x!1") (("2" (expand "fullset") (("2" (expand "Union") (("2" (skosimp) (("2" (hide -1 -2) (("2" (expand "subset?") (("2" (typepred "a!1") (("2" (inst + "a!1") (("2" (expand "PP") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skosimp) (("1" (lemma "extensionality_postulate" ("f" "Union(P!1)" "g" "fullset[T]")) (("1" (replace -1 -3 rl) (("1" (inst -3 "x!1") (("1" (expand "fullset") (("1" (hide -1) (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "PP") (("1" (expand "member") (("1" (inst - "a!1") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "PP") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "fullset[T]=emptyset[T]") (("1" (lemma "extensionality" ("a" "image(f!1, emptyset[T])" "b" "emptyset[real]")) (("1" (split -1) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (expand "emptyset") (("2" (expand "member") (("2" (expand "image") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "emptyset") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "every") (("2" (expand "measurable_set?") (("2" (case-replace "{x | y!1 = f!1(x)} = Union({X:set[T] | P!1(X) & image[T,real](f!1,X) = singleton[real]( (("1" (hide -1) (("1" (case "subset?({X: set[T] | P!1(X) & image[T, real](f!1, X) = singleton[real](y!1)},P!1)") (("1" (expand "finite_partition?") (("1" (flatten) (("1" (name-replace "SS" "{X: set[T] | P!1(X) & image[T, real](f!1, X) = singleton[real](y!1)}") (("1" (typepred "S") (("1" (expand "sigma_algebra?") (("1" (flatten) (("1" (expand "sigma_algebra_union?") (("1" (inst - "SS") (("1" (split -3) (("1" (assert) nil nil) ("2" (lemma "finite_subset[set[T]]" ("s" "SS" "A" "P!1")) (("1" (assert) (("1" (lemma "finite_countable[set[T]]" ("x" "SS")) (("1" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("3" (skosimp) (("3" (expand "subset?") (("3" (inst - "x!1") (("3" (inst -6 "x!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (hide 2) (("2" (case-replace "y!1=f!1(x!1)") (("1" (expand "Union") (("1" (expand "finite_partition?") (("1" (flatten) (("1" (expand "partition?") (("1" (flatten) (("1" (lemma "extensionality_postulate" ("f" "Union(P!1)" "g" "fullset[T]")) (("1" (replace -1 -3 rl) (("1" (hide -1) (("1" (inst -2 "x!1") (("1" (expand "fullset") (("1" (expand "Union") (("1" (skosimp) (("1" (inst + "a!1") (("1" (expand "singleton") (("1" (expand "image") (("1" (apply-extensionality 1 :hide? t) (("1" (case-replace "x!2 = f!1(x!1)") (("1" (inst + "x!1") nil nil) ("2" (assert) (("2" (skosimp) (("2" (typepred "x!3") (("2" (inst -8 "a!1") (("2" (expand "constant_over?") (("2" (skosimp) (("2" (inst-cp -8 "x!1") (("2" (inst -8 "x!3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Union") (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "singleton") (("2" (lemma "extensionality_postulate" ("f" "image[T, real](f!1, a!1)" "g" "({y: real | y = y!1})")) (("2" (replace -1 -3 rl) (("2" (hide -1) (("2" (inst - "y!1") (("2" (expand "image") (("2" (skosimp) (("2" (typepred "x!2") (("2" (inst -7 "a!1") (("2" (expand "constant_over?") (("2" (skosimp) (("2" (inst-cp -7 "x!1") (("2" (inst -7 "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple_def1 formula-decl 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) (measurable_fullset name-judgement "measurable_set[T, S]" measure_space nil) (subset_algebra_fullset name-judgement "(S)" measure_space nil) (emptyset const-decl "set" sets nil) (subset_algebra_emptyset name-judgement "(S)" measure_space_def nil) (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" real_topology "metric_space/") (finite_emptyset name-judgement "finite_set[real]" measure_space nil) (finite_image application-judgement "finite_set[R]" countable_image "sets_aux/") (measurable_emptyset name-judgement "measurable_set" measure_space nil) (subset_algebra_emptyset name-judgement "(S)" measure_space nil) (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (extensionality_postulate formula-decl nil functions nil) (a!1 skolem-const-decl "(P!1)" measure_space nil) (P!1 skolem-const-decl "finite_partition[T]" measure_space nil) (restrict const-decl "R" restrict nil) (finite_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (FF skolem-const-decl "[X: (PP) -> (image[T, real](f!1, X))]" measure_space nil) (PP skolem-const-decl "[set[T] -> boolean]" measure_space nil) (x!2 skolem-const-decl "(LAMBDA (s: (PP)): TRUE)" measure_space nil) (x!4 skolem-const-decl "(x!2)" measure_space nil) (choose const-decl "(p)" sets nil) (x!1 skolem-const-decl "T" measure_space nil) (y!1 skolem-const-decl "real" measure_space nil) (X!1 skolem-const-decl "(PP)" measure_space nil) (subset? const-decl "bool" 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) (x!1 skolem-const-decl "(SS)" measure_space nil) (SS skolem-const-decl "[set[T] -> boolean]" measure_space nil) (finite_countable judgement-tcc nil countable_props "sets_aux/") (sigma_algebra_union? const-decl "bool" subset_algebra_def nil) (a!1 skolem-const-decl "({X: set[T] | P!1(X) & image[T, real](f!1, X) = singleton[real](y!1)})" measure_space nil) (y!1 skolem-const-decl "(image(f!1, fullset[T]))" measure_space nil) (a!1 skolem-const-decl "(P!1)" measure_space nil) (x!1 skolem-const-decl "T" measure_space nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (finite_partition? const-decl "bool" partitions nil) (PP skolem-const-decl "set[set[T]]" measure_space nil) (finite_partition nonempty-type-eq-decl nil partitions nil) (constant_over? const-decl "bool" measure_space nil) (measurable_set? const-decl "bool" measure_space_def nil) (member const-decl "bool" sets nil) (f!1 skolem-const-decl "[T -> real]" measure_space nil) (x!3 skolem-const-decl "({x | TRUE})" measure_space nil) (real_minus_real_is_real application-judgement "real" reals nil) (extensionality formula-decl nil sets_lemmas nil) (TRUE const-decl "bool" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (every const-decl "bool" sets nil) (FF skolem-const-decl "[real -> set[T]]" measure_space nil) (x!1 skolem-const-decl "T" measure_space nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union const-decl "set" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (singleton_is_closed application-judgement "closed[real, (metric_induced_topology)]" measure_space nil) (singleton_is_compact application-judgement "compact[real, metric_induced_topology]" measure_space_def nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (partition? const-decl "bool" partitions nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_image judgement-tcc nil function_image_aux nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (image const-decl "set[R]" function_image nil) (inverse_image const-decl "set[D]" function_image nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (fullset const-decl "set" sets nil)) shostak)) (simple_def3 0 (simple_def3-1 nil 3392345048 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (rewrite "simple_def1") (("1" (flatten) (("1" (name "NZ" "lambda f: {y| EXISTS x: f(x)=y & y/=0}") (("1" (case "forall f: subset?(NZ(f),image[T,real](f,fullset[T]))") (("1" (case "forall h: is_finite[real](NZ(h))") (("1" (case "FORALL (h: simple, n: nat): card(NZ(h)) = n => EXISTS c1, c2, h1, h2: c1 * h1 + c2 * h2 = h") (("1" (case "nonempty?(fullset[T])") (("1" (inst - "f!1" "card(NZ(f!1))") (("1" (inst - "f!1") (("1" (rewrite "simple_def1" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "simple_def1" 1) (("2" (assert) nil nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (hide-all-but (-1 1)) (("2" (inst + "0" "0" "phi(fullset[T])" "phi(fullset[T])") (("2" (expand "*") (("2" (expand "+") (("2" (lemma "extensionality[T,real]" ("f" "LAMBDA (x_1: T): 0" "g" "f!1")) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "fullset") (("2" (expand "empty?") (("2" (inst - "x!1") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (induct "n") (("1" (skosimp) (("1" (inst - "h!1") (("1" (rewrite "card_empty?" -1) (("1" (hide -2) (("1" (inst + "0" "0" "phi(emptyset[T])" "phi(emptyset[T])") (("1" (expand "*") (("1" (expand "+") (("1" (lemma "extensionality[T,real]" ("f" "LAMBDA (x_1: T): 0" "g" "h!1")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "NZ") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "h!1(x!1)") (("2" (inst + "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "nonempty_card[real]" ("S" "NZ(h!1)")) (("2" (assert) (("2" (lemma "card_rest[real]" ("S" "NZ(h!1)")) (("2" (split -1) (("1" (replace -4) (("1" (assert) (("1" (lemma "choose_rest[real]" ("a" "NZ(h!1)")) (("1" (lemma "choose_member[real]" ("a" "NZ(h!1)")) (("1" (lemma "choose_not_member[real]" ("a" "NZ(h!1)")) (("1" (name-replace "C" "choose[real](NZ(h!1))") (("1" (typepred "h!1") (("1" (rewrite "simple_def1" -1) (("1" (flatten) (("1" (hide -1) (("1" (expand "nonempty?") (("1" (replace 1 *) (("1" (expand "member" -2) (("1" (inst - "C") (("1" (name "H" "h!1-C*phi({x | C = h!1(x)})") (("1" (inst -6 "H") (("1" (split -6) (("1" (skosimp) (("1" (inst + "1" "C" "H" "phi({x | C = h!1(x)})") (("1" (assert) (("1" (replace -2 3 rl) (("1" (apply-extensionality 3 :hide? t) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "measurable_set?") (("2" (assert) (("2" (lemma "phi_is_simple" ("X" "{x | C = h!1(x)}")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (replace -1 1 rl) (("3" (hide-all-but 1) (("3" (typepred "h1!1") (("3" (typepred "h2!1") (("3" (lemma "simple_scal" ("c" "c1!1" "h" "h1!1")) (("3" (lemma "simple_scal" ("c" "c2!1" "h" "h2!1")) (("3" (lemma "simple_add" ("h1" "*[T](c1!1, h1!1)" "h2" "*[T](c2!1, h2!1)")) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "NZ(H) = rest(NZ(h!1))") (("2" (hide 5 2 -5 -6) (("2" (apply-extensionality 1 :hide? t) (("2" (lemma "extensionality_postulate[real,bool]" ("f" "add(C, rest(NZ(h!1)))" "g" "NZ(h!1)")) (("2" (replace -1 -5 rl) (("2" (hide -1) (("2" (inst -4 "x!1") (("2" (expand "add" -4) (("2" (expand "member") (("2" (case "forall x: h!1(x) = C => H(x)=0") (("1" (case "forall x: h!1(x)/=C => h!1(x)=H(x)") (("1" (case-replace "rest(NZ(h!1))(x!1)") (("1" (case-replace "x!1=C") (("1" (expand "NZ") (("1" (skolem! -7) (("1" (inst -2 "x!2") (("1" (flatten) (("1" (assert) (("1" (inst + "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (hide 2) (("2" (case-replace "x!1=C") (("1" (expand "NZ" -4) (("1" (skosimp) (("1" (inst -2 "x!2") (("1" (assert) (("1" (replace -4) (("1" (case-replace "h!1(x!2) = C") (("1" (assert) (("1" (inst -3 "x!2") (("1" (assert) nil nil)) nil)) nil) ("2" (replace 1) (("2" (inst -2 "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "NZ" -3) (("2" (skosimp) (("2" (inst -2 "x!2") (("2" (assert) (("2" (inst - "x!2") (("2" (split -1) (("1" (expand "rest" 2) (("1" (expand "remove") (("1" (expand "NZ" 2 2) (("1" (expand "member" 2) (("1" (split 2) (("1" (expand "/=" 1) (("1" (expand "C" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replace -2 2 rl) (("2" (expand "-" 2) (("2" (expand "*" 2) (("2" (expand "phi" 2) (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replace -2 1 rl) (("2" (expand "-") (("2" (replace -1) (("2" (expand "*" 1) (("2" (expand "phi" 1) (("2" (expand "member") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 1 rl) (("2" (hide-all-but (-2 1)) (("2" (expand "measurable_set?") (("2" (lemma "phi_is_simple" ("X" "{x | C = h!1(x)}")) (("1" (lemma "simple_scal" ("c" "C" "h" "phi({x | C = h!1(x)})")) (("1" (lemma "simple_diff" ("h1" "h!1" "h2" "*[T](C, phi({x | C = h!1(x)}))")) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "fullset") (("2" (expand "NZ") (("2" (expand "image") (("2" (skosimp) (("2" (inst + "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp) (("2" (typepred "h!1") (("2" (rewrite "simple_def1") (("2" (flatten) (("2" (inst -3 "h!1") (("2" (hide -2) (("2" (lemma "finite_subset[real]" ("s" "NZ(h!1)" "A" "image[T, real](h!1, fullset[T])")) (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "subset?") (("2" (skosimp) (("2" (hide-all-but (-1 1)) (("2" (expand "member") (("2" (expand "NZ") (("2" (expand "fullset") (("2" (expand "image") (("2" (skosimp) (("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "simple_scal" ("c" "c1!1" "h" "h1!1")) (("2" (lemma "simple_scal" ("c" "c2!1" "h" "h2!1")) (("2" (replace -3 1 :dir rl) (("2" (rewrite "simple_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple_def1 formula-decl 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) (measurable_fullset name-judgement "measurable_set[T, S]" measure_space nil) (subset_algebra_fullset name-judgement "(S)" measure_space nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (simple? const-decl "bool" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil) (is_finite const-decl "bool" finite_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (choose_member formula-decl nil sets_lemmas nil) (choose const-decl "(p)" sets nil) (h!1 skolem-const-decl "simple" measure_space nil) (C skolem-const-decl "(NZ(h!1))" measure_space nil) (H skolem-const-decl "[T -> real]" measure_space nil) (rest const-decl "set" sets nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (remove const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (extensionality_postulate formula-decl nil functions nil) (simple_scal judgement-tcc nil measure_space nil) (simple_add judgement-tcc nil measure_space 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) (phi_is_simple judgement-tcc nil measure_space nil) (measurable_set? const-decl "bool" measure_space_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (simple_diff judgement-tcc nil measure_space nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (TRUE const-decl "bool" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (choose_not_member formula-decl nil sets_lemmas nil) (choose_rest formula-decl nil sets_lemmas nil) (card_rest formula-decl nil finite_sets nil) (nonempty_card formula-decl nil finite_sets nil) (card_empty? formula-decl nil finite_sets nil) (emptyset const-decl "set" sets nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (nonempty? const-decl "bool" sets nil) (NZ skolem-const-decl "[[T -> real] -> [real -> boolean]]" measure_space nil) (f!1 skolem-const-decl "[T -> real]" measure_space nil) (extensionality formula-decl nil functions nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (phi const-decl "nat" measure_space nil) (phi_is_simple application-judgement "simple" measure_space nil) (simple_scal application-judgement "simple" measure_space nil) (simple_add application-judgement "simple" measure_space nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (finite_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (fullset const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (subset? const-decl "bool" sets nil) (set type-eq-decl nil sets nil)) shostak)) (bounded_measurable_TCC1 0 (bounded_measurable_TCC1-1 nil 3392437154 ("" (expand "bounded_measurable?") (("" (split) (("1" (expand "bounded?") (("1" (inst + "0") (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "const_measurable" ("c" "0")) (("2" (expand "const_fun") (("2" (propax) nil nil)) nil)) nil)) nil)) 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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_minus_real_is_real application-judgement "real" reals nil) (bounded? const-decl "bool" sup_norm nil) (const_measurable formula-decl nil measure_space nil) (bounded_measurable? const-decl "bool" measure_space nil)) nil)) (bounded_measurable_is_bounded 0 (bounded_measurable_is_bounded-1 nil 3392437154 ("" (skosimp) (("" (typepred "x!1") (("" (expand "bounded_measurable?") (("" (flatten) nil nil)) nil)) nil)) nil) ((bounded_measurable nonempty-type-eq-decl nil measure_space nil) (bounded_measurable? const-decl "bool" measure_space 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)) nil)) (bounded_measurable_is_measurable 0 (bounded_measurable_is_measurable-1 nil 3392437154 ("" (skosimp) (("" (typepred "x!1") (("" (expand "bounded_measurable?") (("" (flatten) nil nil)) nil)) nil)) nil) ((bounded_measurable nonempty-type-eq-decl nil measure_space nil) (bounded_measurable? const-decl "bool" measure_space 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)) nil)) (simple_is_bounded_measurable 0 (simple_is_bounded_measurable-1 nil 3392437154 ("" (skolem + ("F")) (("" (typepred "F") (("" (expand "bounded_measurable?") (("" (split) (("1" (expand "bounded?") (("1" (expand "simple?") (("1" (flatten) (("1" (hide -1) (("1" (name "CC" "image[T,real](abs[T](F),fullset[T])") (("1" (typepred "sup(CC)") (("1" (expand "least_upper_bound") (("1" (flatten) (("1" (case "exists x: true") (("1" (inst + "sup(CC)") (("1" (skolem! +) (("1" (expand "upper_bound") (("1" (inst - "abs(F(x!1))") (("1" (expand "CC" 1) (("1" (expand "fullset") (("1" (expand "image") (("1" (inst + "x!1") (("1" (expand "abs" 1 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "upper_bound") (("2" (skosimp) (("2" (inst - "abs(F(x!1))") (("1" (typepred "abs(F(x!1))") (("1" (assert) nil nil)) nil) ("2" (expand "CC") (("2" (expand "fullset") (("2" (expand "image") (("2" (inst + "x!1") (("2" (expand "abs" 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "0") (("2" (skosimp) (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (split 1) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (case "exists x: true") (("1" (skosimp) (("1" (inst - "abs(F(x!1))") (("1" (expand "CC") (("1" (expand "fullset") (("1" (expand "image") (("1" (inst + "x!1") (("1" (hide-all-but 1) (("1" (expand "abs" 1 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "0") (("2" (skosimp) (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "forall (X:finite_set[real]): above_bounded[real](X)") (("1" (inst - "CC") (("1" (lemma "finite_image[real,real]") (("1" (inst - "image(F, fullset[T])" "abs") (("1" (case-replace "image[real, real](abs, image(F, fullset[T]))=CC") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (expand "CC") (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "abs" 1 2) (("1" (case-replace "EXISTS (x_1: ({x: T | TRUE})): x!1 = abs(F(x_1))") (("1" (skosimp) (("1" (inst + "F(x!2)") (("1" (inst + "x!2") nil nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "x!2") (("2" (skosimp) (("2" (inst + "x!3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case " FORALL (X: finite_set[real],n:nat): card(X)=n => above_bounded[real](X)") (("1" (skosimp) (("1" (inst - "X!1" "card(X!1)") nil nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp*) (("1" (rewrite "card_empty?") (("1" (expand "above_bounded") (("1" (inst + "0") (("1" (expand "upper_bound") (("1" (skosimp) (("1" (expand "empty?") (("1" (inst - "z!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "nonempty_card[real]" ("S" "X!1")) (("2" (assert) (("2" (lemma "choose_rest[real]" ("a" "X!1")) (("2" (expand "nonempty?") (("2" (assert) (("2" (lemma "card_rest[real]" ("S" "X!1")) (("2" (replace -4) (("2" (assert) (("2" (inst - "rest[real](X!1)") (("2" (assert) (("2" (expand "above_bounded") (("2" (skosimp) (("2" (inst + "max(choose[real](X!1),n!1)") (("2" (expand "upper_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (replace -3 -1 rl) (("2" (expand "add" -1) (("2" (split -1) (("1" (replace -1) (("1" (hide-all-but 2) (("1" (grind) nil nil)) nil)) nil) ("2" (inst -4 "z!1") (("1" (name-replace "DRL1" "choose[real](X!1)") (("1" (hide-all-but (-4 2)) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "simple?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ((simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (pred type-eq-decl nil defined_types nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (<= const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (above_bounded const-decl "bool" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (CC skolem-const-decl "set[real]" measure_space nil) (nnreal type-eq-decl nil real_types nil) (upper_bound const-decl "bool" bound_defs "reals/") (x!1 skolem-const-decl "T" measure_space nil) (F skolem-const-decl "simple" measure_space 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) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x!1 skolem-const-decl "T" measure_space nil) (TRUE const-decl "bool" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (card_rest formula-decl nil finite_sets nil) (finite_rest application-judgement "finite_set[real]" measure_space nil) (nonempty_add_finite application-judgement "non_empty_finite_set[real]" measure_space nil) (add const-decl "(nonempty?)" sets nil) (X!1 skolem-const-decl "finite_set[real]" measure_space nil) (z!1 skolem-const-decl "{x: real | X!1(x)}" measure_space nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (choose const-decl "(p)" sets nil) (rest const-decl "set" sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (choose_rest formula-decl nil sets_lemmas nil) (nonempty_card formula-decl nil finite_sets nil) (card_empty? formula-decl nil finite_sets nil) (nat_induction formula-decl nil naturalnumbers nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (measurable_fullset name-judgement "measurable_set[T, S]" measure_space nil) (subset_algebra_fullset name-judgement "(S)" measure_space nil) (x!2 skolem-const-decl "({x: T | TRUE})" measure_space nil) (finite_image judgement-tcc nil function_image_aux nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (image const-decl "set[R]" function_image nil) (>= 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/") (fullset const-decl "set" sets nil) (bounded? const-decl "bool" sup_norm nil) (bounded_measurable? const-decl "bool" measure_space nil)) nil)) (nn_bounded_measurable_TCC1 0 (nn_bounded_measurable_TCC1-1 nil 3392524429 ("" (expand "nn_bounded_measurable?") (("" (lemma "bounded_measurable_TCC1") (("" (propax) nil nil)) nil)) nil) ((bounded_measurable_TCC1 subtype-tcc nil measure_space nil) (nn_bounded_measurable? const-decl "bool" measure_space nil)) nil)) (nn_bounded_measurable_is_bounded_measurable 0 (nn_bounded_measurable_is_bounded_measurable-1 nil 3392524429 ("" (skosimp) (("" (typepred "x!1") (("" (expand "nn_bounded_measurable?") (("" (flatten) nil nil)) nil)) nil)) nil) ((nn_bounded_measurable nonempty-type-eq-decl nil measure_space nil) (nn_bounded_measurable? const-decl "bool" measure_space 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)) nil)) (increasing_nn_simple_TCC1 0 (increasing_nn_simple_TCC1-1 nil 3392524429 ("" (lemma "simple_const" ("c" "0")) (("" (expand "const_fun") (("" (expand "increasing_nn_simple?") (("" (expand "nn_simple?") (("" (split) (("1" (skosimp) nil nil) ("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((increasing_nn_simple? const-decl "bool" measure_space nil) (real_minus_real_is_real application-judgement "real" reals nil) (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (T formal-type-decl nil measure_space nil) (increasing? const-decl "bool" real_fun_preds "reals/") (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nn_simple? const-decl "bool" measure_space nil) (simple_const 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)) nil)) (sup_norm_simple 0 (sup_norm_simple-1 nil 3392391734 ("" (skosimp*) (("" (name "AA" "sup_norm(p!1)/2") (("" (replace -1) (("" (typepred "p!1") (("" (expand "nn_bounded_measurable?") (("" (name "EE" "{x | p!1(x) > AA}") (("" (lemma "measurable_gt" ("f" "p!1")) (("" (assert) (("" (flatten) (("" (hide -2) (("" (assert) (("" (expand "bounded_measurable?") (("" (flatten) (("" (assert) (("" (inst - "AA") (("" (case "simple?(AA*phi(EE))") (("1" (inst + "AA * phi(EE)") (("1" (case-replace "FORALL x: 0 <= (AA * phi(EE))(x) & (AA * phi(EE))(x) <= p!1(x)") (("1" (expand "*" -1) (("1" (expand "sup_norm") (("1" (case-replace "EXISTS (x: T): TRUE") (("1" (skolem - ("XX")) (("1" (expand "extend") (("1" (typepred "sup(LAMBDA (t: real): IF t >= 0 THEN EXISTS (x_1: T): abs(p!1(x_1)) = t ELSE FALSE ENDIF)") (("1" (name-replace "NORM_P" "sup(LAMBDA (t: real): IF t >= 0 THEN EXISTS (x_1: T): abs(p!1(x_1)) = t ELSE FALSE ENDIF)") (("1" (typepred "sup(LAMBDA (t_1: real): IF t_1 >= 0 THEN EXISTS (x_2: T): abs((p!1 - AA * phi(EE))(x_2)) = t_1 ELSE FALSE ENDIF)") (("1" (name-replace "NORM_PH" "sup(LAMBDA (t_1: real): IF t_1 >= 0 THEN EXISTS (x_2: T): abs((p!1 - AA * phi(EE))(x_2)) = t_1 ELSE FALSE ENDIF)") (("1" (expand "least_upper_bound") (("1" (flatten) (("1" (hide -1) (("1" (inst - "AA") (("1" (replace 1 -1) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "upper_bound" 1) (("2" (skosimp) (("2" (typepred "z!1") (("2" (assert) (("2" (skosimp) (("2" (inst-cp -5 "x!1") (("2" (flatten) (("2" (expand "-" -1) (("2" (expand "*" -1) (("2" (expand "abs" -1) (("2" (assert) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (hide -3) (("2" (expand "upper_bound") (("2" (inst - "p!1(x!1)") (("1" (expand "phi") (("1" (expand "member") (("1" (case-replace "EE(x!1)") (("1" (expand "EE") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "EE") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "x!1") (("2" (expand "abs") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -6 -2 -2 -8)) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "p!1(XX)-AA*phi(EE)(XX)") (("1" (expand "member") (("1" (inst - "XX") (("1" (flatten) (("1" (assert) (("1" (inst + "XX") (("1" (expand "-") (("1" (expand "*") (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "above_bounded") (("2" (expand "bounded?") (("2" (skosimp) (("2" (inst + "c!1") (("2" (expand "upper_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (assert) (("2" (skosimp) (("2" (expand "-") (("2" (expand "*") (("2" (inst - "x!1") (("2" (flatten) (("2" (expand "abs" -1) (("2" (assert) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 -7 1)) (("2" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "p!1(XX)") (("1" (expand "member") (("1" (inst - "XX") (("1" (assert) (("1" (inst + "XX") (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "above_bounded") (("2" (expand "bounded?") (("2" (skosimp) (("2" (inst + "c!1") (("2" (expand "upper_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (assert) (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (replace 1 -8) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (split) (("1" (expand "*") (("1" (typepred "sup_norm(p!1)") (("1" (lemma "le_times_le_pos" ("nnx" "0" "y" "AA" "nnz" "0" "w" "phi(EE)(x!1)")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "*") (("2" (hide -1 -2 -3) (("2" (expand "phi") (("2" (expand "member") (("2" (expand "EE") (("2" (case-replace "p!1(x!1) > AA") (("1" (assert) nil nil) ("2" (assert) (("2" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "phi_is_simple" ("X" "EE")) (("1" (rewrite "simple_scal") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_bounded_measurable nonempty-type-eq-decl nil measure_space nil) (nn_bounded_measurable? const-decl "bool" measure_space nil) (sup_norm const-decl "nnreal" sup_norm nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bounded nonempty-type-eq-decl nil sup_norm nil) (bounded? const-decl "bool" sup_norm 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) (T formal-type-decl nil measure_space nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (bounded_measurable? const-decl "bool" measure_space nil) (simple? const-decl "bool" measure_space nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (set type-eq-decl nil sets nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (phi const-decl "nat" measure_space nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (pred type-eq-decl nil defined_types nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (nonempty? const-decl "bool" sets nil) (above_bounded const-decl "bool" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (FALSE const-decl "bool" booleans nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (p!1 skolem-const-decl "nn_bounded_measurable" measure_space nil) (x!1 skolem-const-decl "T" measure_space nil) (member const-decl "bool" sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (upper_bound const-decl "bool" bound_defs "reals/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (extend const-decl "R" extend nil) (TRUE const-decl "bool" booleans nil) (le_times_le_pos formula-decl nil real_props nil) (simple nonempty-type-eq-decl nil measure_space nil) (EE skolem-const-decl "[T -> bool]" measure_space nil) (AA skolem-const-decl "nnreal" measure_space nil) (phi_is_simple judgement-tcc nil measure_space nil) (simple_scal judgement-tcc nil measure_space 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) (measurable_gt formula-decl nil measure_space_def nil)) shostak)) (nn_simple_approx_TCC1 0 (nn_simple_approx_TCC1-1 nil 3394514188 ("" (skosimp) (("" (lemma "sup_norm_simple" ("p" "p!1")) (("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (inst -3 "h!1") (("" (expand "member") (("" (replace -2 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_bounded_measurable nonempty-type-eq-decl nil measure_space nil) (nn_bounded_measurable? const-decl "bool" measure_space 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) (sup_norm_simple formula-decl nil measure_space nil) (nonempty? const-decl "bool" sets nil) (simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) nil)) (nn_simple_approx_TCC2 0 (nn_simple_approx_TCC2-1 nil 3394514188 ("" (skosimp) (("" (lemma "nn_simple_approx_TCC1" ("p" "p!1")) (("" (lemma "choose_member" ("a" "{h | (FORALL x: 0 <= h(x) & h(x) <= p!1(x)) AND sup_norm[T]((-[T])(p!1, h)) <= sup_norm[T](p!1) / 2}")) (("" (expand "nonempty?") (("" (assert) (("" (expand "nn_simple?") (("" (skosimp) (("" (inst - "x!1") (("" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_bounded_measurable nonempty-type-eq-decl nil measure_space nil) (nn_bounded_measurable? const-decl "bool" measure_space 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) (nn_simple_approx_TCC1 subtype-tcc nil measure_space nil) (nonempty? const-decl "bool" sets nil) (nn_simple? const-decl "bool" measure_space nil) (member const-decl "bool" sets nil) (bounded_diff application-judgement "bounded" measure_space nil) (diff_measurable application-judgement "measurable_function[T, S]" measure_space nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (choose_member formula-decl nil sets_lemmas nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (bounded? const-decl "bool" sup_norm nil) (bounded nonempty-type-eq-decl nil sup_norm nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sup_norm const-decl "nnreal" sup_norm nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (simple? const-decl "bool" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil)) nil)) (nn_simple_sequence_TCC1 0 (nn_simple_sequence_TCC1-1 nil 3394514188 ("" (skosimp*) (("" (hide -1) (("" (expand "nn_simple_approx") (("" (case "nonempty?({h | (FORALL x: 0 <= h(x) & h(x) <= p!1(x)) AND sup_norm(p!1 - h) <= sup_norm(p!1) / 2})") (("1" (lemma "choose_member" ("a" "({h | (FORALL x: 0 <= h(x) & h(x) <= p!1(x)) AND sup_norm(p!1 - h) <= sup_norm(p!1) / 2})")) (("1" (split -1) (("1" (name-replace "HH" "choose({h | (FORALL x: 0 <= h(x) & h(x) <= p!1(x)) AND sup_norm(p!1 - h) <= sup_norm(p!1) / 2})") (("1" (expand "member") (("1" (flatten) (("1" (inst - "x!1") nil nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (lemma "sup_norm_simple" ("p" "p!1")) (("2" (skosimp) (("2" (inst -3 "h!1") (("2" (replace -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/ 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) (- const-decl "[T -> real]" real_fun_ops "reals/") (sup_norm const-decl "nnreal" sup_norm nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bounded nonempty-type-eq-decl nil sup_norm nil) (bounded? const-decl "bool" sup_norm nil) (nn_bounded_measurable nonempty-type-eq-decl nil measure_space nil) (nn_bounded_measurable? const-decl "bool" measure_space nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space 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) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (diff_measurable application-judgement "measurable_function[T, S]" measure_space nil) (bounded_diff application-judgement "bounded" measure_space nil) (member const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (choose const-decl "(p)" sets nil) (choose_member formula-decl nil sets_lemmas nil) (sup_norm_simple formula-decl nil measure_space nil) (empty? const-decl "bool" sets nil) (nn_simple_approx const-decl "nn_simple" measure_space nil)) nil)) (nn_simple_sequence_TCC2 0 (nn_simple_sequence_TCC2-1 nil 3394514188 ("" (skosimp) (("" (typepred "p!1") (("" (typepred "nn_simple_approx(p!1)") (("" (expand "nn_bounded_measurable?") (("" (lemma "simple_is_bounded_measurable") (("" (inst - "nn_simple_approx(p!1)") (("" (flatten) (("" (expand "bounded_measurable?") (("" (flatten) (("" (skosimp) (("" (expand "-" 2) (("" (name "DRL1" " nn_simple_approx(p!1)") (("" (replace -1) (("" (hide-all-but (-1 -7 1 2)) (("" (expand "nn_simple_approx") (("" (case "nonempty?({h | (FORALL x: 0 <= h(x) & h(x) <= p!1(x)) AND sup_norm(p!1 - h) <= sup_norm(p!1) / 2})") (("1" (lemma "choose_member" ("a" "{h | (FORALL x: 0 <= h(x) & h(x) <= p!1(x)) AND sup_norm(p!1 - h) <= sup_norm(p!1) / 2}")) (("1" (expand "nonempty?") (("1" (replace 1) (("1" (replace -2) (("1" (expand "member") (("1" (flatten) (("1" (hide -3 1) (("1" (inst - "x!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2 -2)) (("2" (lemma "sup_norm_simple" ("p" "p!1")) (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst -3 "h!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_bounded_measurable nonempty-type-eq-decl nil measure_space nil) (nn_bounded_measurable? const-decl "bool" measure_space 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) (bounded_diff application-judgement "bounded" measure_space nil) (diff_measurable application-judgement "measurable_function[T, S]" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space nil) (bounded_measurable? const-decl "bool" measure_space nil) (= const-decl "[T, T -> boolean]" equalities nil) (/ 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) (sup_norm const-decl "nnreal" sup_norm nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bounded nonempty-type-eq-decl nil sup_norm nil) (bounded? const-decl "bool" sup_norm nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (choose_member formula-decl nil sets_lemmas nil) (sup_norm_simple formula-decl nil measure_space nil) (empty? const-decl "bool" sets nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (simple_is_bounded_measurable judgement-tcc nil measure_space nil) (nn_simple? const-decl "bool" measure_space nil) (nn_simple nonempty-type-eq-decl nil measure_space nil) (nn_simple_approx const-decl "nn_simple" measure_space nil)) nil)) (nn_simple_sequence_TCC3 0 (nn_simple_sequence_TCC3-1 nil 3394514188 ("" (skosimp) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (nn_simple_sequence_TCC4 0 (nn_simple_sequence_TCC4-1 nil 3394514764 ("" (skosimp) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (nn_simple_sequence_TCC5 0 (nn_simple_sequence_TCC5-1 nil 3394818674 ("" (skosimp*) (("" (typepred "v!1((-[T])(p!1, nn_simple_approx(p!1)))(n!1-1)") (("1" (inst - "x!1") (("1" (flatten) (("1" (assert) (("1" (name-replace "DRL1" "v!1((-[T])(p!1, nn_simple_approx(p!1)))(n!1 - 1)(x!1)") (("1" (typepred "nn_simple_approx(p!1)") (("1" (expand "nn_simple?") (("1" (flatten) (("1" (inst - "x!1") (("1" (assert) (("1" (expand "-" -5) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "nn_simple_sequence_TCC2" ("p" "p!1" "n" "n!1")) (("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nn_simple_approx const-decl "nn_simple" measure_space nil) (nn_simple nonempty-type-eq-decl nil measure_space nil) (nn_simple? const-decl "bool" measure_space nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (simple nonempty-type-eq-decl nil measure_space nil) (< const-decl "bool" reals 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) (nn_bounded_measurable nonempty-type-eq-decl nil measure_space nil) (nn_bounded_measurable? const-decl "bool" measure_space nil) (simple? const-decl "bool" measure_space 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) (diff_measurable application-judgement "measurable_function[T, S]" measure_space nil) (bounded_diff application-judgement "bounded" measure_space nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nn_simple_sequence_TCC2 subtype-tcc nil measure_space nil)) nil)) (nn_bounded_measurable_as_increasing_simple_sequence_TCC1 0 (nn_bounded_measurable_as_increasing_simple_sequence_TCC1-1 nil 3392524429 ("" (skosimp) (("" (skosimp) (("" (typepred "w!1") (("" (expand "increasing_nn_simple?") (("" (flatten) (("" (inst - "x1!1") (("" (expand "nn_simple?") (("" (flatten) (("" (lemma "simple_is_bounded_measurable") (("" (inst - "w!1(x1!1)") (("" (expand "bounded_measurable?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((x1!1 skolem-const-decl "nat" measure_space nil) (w!1 skolem-const-decl "increasing_nn_simple" measure_space nil) (simple? const-decl "bool" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil) (bounded_measurable? const-decl "bool" measure_space nil) (simple_is_bounded_measurable judgement-tcc nil measure_space nil) (nn_simple? const-decl "bool" 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) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (measurable_function? const-decl "bool" measure_space_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (sequence type-eq-decl nil sequences nil) (increasing_nn_simple? const-decl "bool" measure_space nil) (increasing_nn_simple nonempty-type-eq-decl nil measure_space nil)) nil)) (nn_bounded_measurable_as_increasing_simple_sequence 0 (nn_bounded_measurable_as_increasing_simple_sequence-1 nil 3394603518 ("" (name "HH" "nn_simple_approx") (("" (name "GG" "nn_simple_sequence") (("" (case "forall p: (forall x: 0 <= HH(p)(x) & HH(p)(x) <= p(x)) AND sup_norm(p-HH(p)) <= sup_norm(p)/2") (("1" (case "forall p: nn_bounded_measurable?(p-HH(p))") (("1" (case "forall p: GG(p)(0)=HH(p)") (("1" (case "forall p,n: GG(p)(n+1)= GG(p-HH(p))(n)") (("1" (name "FF" "lambda p: lambda n: lambda x: sigma(0,n,lambda i: GG(p)(i)(x))") (("1" (case "forall p:FF(p)(0)= HH(p)") (("1" (case "FORALL p, n: FF(p)(n + 1) = GG(p)(n+1)+FF(p)(n)") (("1" (case "FORALL p, n: FF(p)(n + 1) = HH(p) + FF(p - HH(p))(n)") (("1" (case "FORALL p, n,x: 0<=FF(p)(n)(x)& FF(p)(n)(x)<=p(x)") (("1" (case "forall p: pointwise_increasing?(FF(p))") (("1" (case "forall p,n: nn_simple?(FF(p)(n))") (("1" (case "FORALL p,n: nn_bounded_measurable?(p - FF(p)(n))") (("1" (case "forall p,n: sup_norm(p-FF(p)(n)) <= sup_norm(p) / 2^(n+1)") (("1" (skosimp) (("1" (inst + "FF(p!1)") (("1" (expand "sup_norm_converges_to?") (("1" (skosimp) (("1" (inst - "p!1" "_") (("1" (case "exists n: sup_norm(p!1) / 2 ^ (n + 1)< epsilon!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (case-replace "FF(p!1)(i!1) - p!1 = -(p!1 - FF(p!1)(i!1))") (("1" (rewrite "sup_norm_neg") (("1" (name-replace "LHS" "sup_norm((p!1 - FF(p!1)(i!1)))") (("1" (hide -1) (("1" (case-replace "sup_norm(p!1)=0") (("1" (assert) nil nil) ("2" (lemma "both_sides_div_pos_le2" ("pz" "sup_norm(p!1)" "py" "2 ^ (n!1 + 1)" "px" "2 ^ (i!1 + 1)")) (("1" (lemma "both_sides_expt_gt1_le" ("gt1x" "2" "i" "n!1+1" "j" "i!1+1")) (("1" (assert) (("1" (hide-all-but (-1 1)) (("1" (rewrite "real_expt_int_rew") (("1" (rewrite "real_expt_int_rew") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (hide-all-but 1) (("3" (rewrite "real_expt_int_rew") (("3" (rewrite "expt_pos") nil nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (rewrite "real_expt_int_rew") (("4" (rewrite "expt_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "large_expt" ("px" "2")) (("2" (assert) (("2" (case-replace "sup_norm(p!1)=0") (("1" (inst + "0") (("1" (assert) nil nil)) nil) ("2" (inst - "sup_norm(p!1)/epsilon!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (rewrite "div_mult_pos_lt1") (("1" (rewrite "div_mult_pos_lt1") (("1" (rewrite "real_expt_int_rew") (("1" (expand "^") (("1" (expand "expt" 2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_int_rew") (("2" (rewrite "expt_pos") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "sup_norm[T](p!1)" "py" "epsilon!1")) (("1" (propax) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp) (("3" (rewrite "real_expt_int_rew") (("3" (lemma "expt_pos" ("px" "2" "i" "1+n!1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split 1) (("1" (skolem + ("n!1")) (("1" (inst -3 "p!1" "n!1") (("1" (hide-all-but (-3 1)) (("1" (expand "nn_simple?") (("1" (flatten) (("1" (assert) (("1" (lemma "simple_is_measurable" ("x" "FF(p!1)(n!1)")) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_simple?") (("2" (split) (("1" (skosimp) (("1" (inst -3 "p!1" "n!1") nil nil)) nil) ("2" (inst -4 "p!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (inst -7 "p!1") (("1" (replace -7) (("1" (inst -12 "p!1") (("1" (flatten) (("1" (rewrite "real_expt_x1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -6 "p!1" "j!1") (("2" (replace -6) (("2" (inst - "p!1-HH(p!1)") (("2" (inst -13 "p!1") (("2" (flatten) (("2" (lemma "expt_plus" ("n0x" "2" "i" "1" "j" "j!1+1")) (("2" (rewrite "expt_x1") (("2" (hide -1) (("2" (case-replace "p!1 - HH(p!1) - FF(p!1 - HH(p!1))(j!1)=p!1 - (HH(p!1) + FF(p!1 - HH(p!1))(j!1))") (("1" (hide -1) (("1" (lemma "both_sides_div_pos_le1" ("pz" "2 ^ (j!1 + 1)" "x" "sup_norm(p!1 - HH(p!1))" "y" "sup_norm(p!1) / 2")) (("1" (rewrite "div_div2") (("1" (assert) (("1" (hide-all-but (-1 -2 1)) (("1" (rewrite "real_expt_int_rew") (("1" (rewrite "real_expt_int_rew") (("1" (expand "^") (("1" (expand "expt" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "real_expt_int_rew") (("2" (rewrite "expt_pos") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "-") (("2" (expand "+") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "nn_bounded_measurable?") (("3" (expand "bounded_measurable?") (("3" (rewrite "real_expt_int_rew") (("3" (lemma "expt_pos" ("px" "2" "i" "1+n!2")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-1 1)) (("4" (skosimp) (("4" (inst - "p!1" "n!2") (("4" (expand "nn_bounded_measurable?") (("4" (expand "bounded_measurable?") (("4" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "nn_bounded_measurable?") (("3" (expand "bounded_measurable?") (("3" (rewrite "real_expt_int_rew") (("3" (lemma "expt_pos" ("px" "2" "i" "1+n!1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-1 1)) (("4" (skosimp) (("4" (inst - "p!1" "n!1") (("4" (expand "nn_bounded_measurable?") (("4" (expand "bounded_measurable?") (("4" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -3 1)) (("2" (skosimp) (("2" (typepred "p!1") (("2" (expand "nn_bounded_measurable?") (("2" (flatten) (("2" (split) (("1" (inst -3 "p!1" "n!1") (("1" (lemma "simple_is_bounded_measurable" ("x" "FF(p!1)(n!1)")) (("1" (expand "bounded_measurable?") (("1" (flatten) (("1" (split) (("1" (hide-all-but (-3 -5 -7 1)) (("1" (expand "bounded?") (("1" (skosimp) (("1" (inst + "c!1") (("1" (skosimp) (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (inst - "p!1" "n!1" "x!1") (("1" (flatten) (("1" (expand "abs") (("1" (assert) (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "diff_measurable") nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "nn_simple?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "-") (("2" (inst -4 "p!1" "n!1" "x!1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (inst -5 "p!1") (("1" (replace -5) (("1" (replace -12 1 rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -5 "p!1" "j!1") (("2" (replace -5) (("2" (inst - "p!1") (("2" (typepred "GG(p!1)(j!1 + 1)") (("2" (hide-all-but (-1 -2 -3 1)) (("2" (expand "nn_simple?") (("2" (flatten) (("2" (split) (("1" (skosimp) (("1" (expand "+") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "simple_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "increasing?") (("2" (skosimp) (("2" (case "forall n,m: FF(p!1)(m)(x!1) <= FF(p!1)(m+n)(x!1)") (("1" (inst - "y!1-x!2" "x!2") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (induct "n") (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst - "m!1+1") (("2" (case "FF(p!1)(m!1)(x!1) <= FF(p!1)(m!1 + 1)(x!1)") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (inst -3 "p!1" "m!1") (("2" (replace -3 1) (("2" (expand "+" 1) (("2" (assert) (("2" (expand "GG" 1) (("2" (typepred "nn_simple_sequence(p!1)(1 + m!1)") (("2" (inst - "x!1") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (inst - "p!1") (("1" (replace -3) (("1" (inst -8 "p!1") (("1" (flatten) (("1" (inst -8 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "p!1-HH(p!1)" "x!1") (("1" (flatten) (("1" (inst -3 "p!1" "j!1") (("1" (replace -3) (("1" (hide -3) (("1" (expand "+" 1) (("1" (name-replace "F" "FF(p!1 - HH(p!1))(j!1)(x!1)") (("1" (expand "-" -2) (("1" (assert) (("1" (inst -9 "p!1") (("1" (flatten) (("1" (inst -9 "x!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -7 "p!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (inst - "p!1" "0") (("1" (replace -1) (("1" (inst -4 "p!1" "0") (("1" (replace -4) (("1" (inst-cp - "p!1-HH(p!1)") (("1" (replace -3) (("1" (inst -6 "p!1-HH(p!1)") (("1" (replace -6) (("1" (inst -2 "p!1") (("1" (replace -2) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "+") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst-cp -2 "p!1" "j!1+1") (("2" (replace -3) (("2" (hide -3) (("2" (inst -2 "p!1-HH(p!1)" "j!1") (("2" (replace -2) (("2" (hide -2) (("2" (inst - "p!1") (("2" (replace -1) (("2" (hide -1) (("2" (inst -3 "p!1" "j!1+1") (("2" (replace -3) (("2" (hide -3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "+" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (hide-all-but 1) (("2" (expand "FF") (("2" (apply-extensionality :hide? t) (("2" (expand "+") (("2" --> -------------------- --> maximum size reached --> --------------------
¤ 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.0.805Bemerkung: (vorverarbeitet am 2026-04-26) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26