| 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 448 kB |
|
Quelle nn_integral.prfSprache: Lisp |
|||||||||||||||
|
(nn_integral (nn_isf_TCC1 0 (nn_isf_TCC1-1 nil 3395153333 ("" (lemma "isf_zero") (("" (assert) (("" (expand "nn_isf?") (("" (propax) nil nil)) nil)) nil)) nil) ((nn_isf? const-decl "bool" nn_integral nil) (isf_zero formula-decl nil isf nil) (T formal-type-decl nil nn_integral 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" nn_integral nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil)) nil)) (increasing_nn_isf_TCC1 0 (increasing_nn_isf_TCC1-1 nil 3395150698 ("" (expand "increasing_nn_isf?") (("" (expand "pointwise_increasing?") (("" (skosimp) (("" (expand "increasing?") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((pointwise_increasing? const-decl "bool" pointwise_convergence nil) (increasing? const-decl "bool" real_fun_preds "reals/") (increasing_nn_isf? const-decl "bool" nn_integral nil)) nil)) (nn_integrable_zero 0 (nn_integrable_zero-1 nil 3394683734 ("" (expand "nn_integrable?") (("" (inst + "lambda n: lambda x: 0") (("1" (split) (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (expand "convergence?") (("1" (skosimp) (("1" (inst + "0") (("1" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (inst + "0") (("2" (expand "o ") (("2" (expand "convergence?") (("2" (skosimp) (("2" (inst + "0") (("2" (skosimp) (("2" (lemma "isf_integral_zero") (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "increasing?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "isf_zero") (("3" (assert) (("3" (expand "nn_isf?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (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 nn_integral nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (sequence type-eq-decl nil sequences nil) (nn_isf nonempty-type-eq-decl nil nn_integral 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) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (convergent? const-decl "bool" topological_convergence "topology/") (O const-decl "T3" function_props nil) (isf_integral_zero formula-decl nil isf nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (convergence? const-decl "bool" topological_convergence "topology/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (increasing? const-decl "bool" real_fun_preds "reals/") (isf_zero formula-decl nil isf nil) (nn_integrable? const-decl "bool" nn_integral nil)) shostak)) (nn_integrable_TCC1 0 (nn_integrable_TCC1-1 nil 3390818142 ("" (rewrite "nn_integrable_zero") nil nil) ((nn_integrable_zero formula-decl nil nn_integral nil)) nil)) (nn_integrable_is_nonneg 0 (nn_integrable_is_nonneg-1 nil 3458999874 ("" (skosimp) (("" (typepred "f!1(x!1)") (("" (propax) nil nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (T formal-type-decl nil nn_integral nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (nn_integrable_is_measurable 0 (nn_integrable_is_measurable-1 nil 3395201393 ("" (skolem + ("f!1")) (("" (typepred "f!1") (("" (expand "nn_integrable?") (("" (skosimp) (("" (lemma "pointwise_measurable" ("u" "u!1" "f" "f!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pointwise_measurable formula-decl nil 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) (nat nonempty-type-eq-decl nil naturalnumbers 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) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil) (isf? const-decl "bool" isf nil) (isf nonempty-type-eq-decl nil isf nil) (nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral 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" nn_integral nil)) nil)) (nn_convergence 0 (nn_convergence-1 nil 3395566466 ("" (skosimp) (("" (name "U1" "lambda (m:nat): lambda n:min(u1!1(n),u2!1(m))") (("" (name "U2" "lambda (m:nat): lambda n:min(u2!1(n),u1!1(m))") (("" (case "forall n: pointwise_convergence?(U2(n), u1!1(n))") (("1" (case "forall n: pointwise_convergence?(U1(n), u2!1(n))") (("1" (hide -3 -4) (("1" (case "forall n: converges_upto?((isf_integral o U2(n)),isf_integral(u1!1(n)))") (("1" (case "forall n: converges_upto?((isf_integral o U1(n)),isf_integral(u2!1(n)))") (("1" (expand "convergent?" -7) (("1" (skosimp) (("1" (lemma "hausdorff_convergence.limit_def" ("v" "isf_integral o u1!1" "l" "l!1")) (("1" (assert) (("1" (replace -1) (("1" (case "convergence?(isf_integral o u2!1, l!1)") (("1" (lemma "hausdorff_convergence.limit_def" ("v" "isf_integral o u2!1" "l" "l!1")) (("1" (assert) (("1" (expand "convergent?") (("1" (inst + "l!1") nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "convergent?") (("2" (inst + "l!1") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1) (("2" (hide -5 -6) (("2" (case "FORALL (i1, i2: nn_isf): (FORALL x: i1(x) <= i2(x)) IMPLIES isf_integral(i1) <= isf_integral(i2)") (("1" (inst-cp - "lambda x: 0" "_") (("1" (rewrite "isf_integral_zero") (("1" (name-replace "II" "isf_integral") (("1" (case "forall (n,m:nat): (II o U2(n))(m) <= l!1") (("1" (case "forall (n,m:nat): (II o U1(n))(m) = (II o U2(m))(n)") (("1" (case "FORALL n: II(u1!1(n)) <= l!1") (("1" (case "FORALL (n, m: nat): (II o U2(n))(m) <= II(u1!1(n))") (("1" (case "FORALL (n, m: nat): (II o U1(n))(m) <= II(u2!1(n))") (("1" (case "FORALL n: II(u2!1(n)) <= l!1") (("1" (lemma "increasing_bounded_convergence" ("v1" "II o u2!1")) (("1" (split) (("1" (expand "sup") (("1" (typepred "lub(Im(II o u2!1))") (("1" (name-replace "LIMIT" "lub(Im(II o u2!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst - "l!1") (("1" (split -2) (("1" (expand "<=" -1) (("1" (split -1) (("1" (expand "Im" -2) (("1" (expand "upper_bound?") (("1" (hide 1) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "l!1-LIMIT" "py" "4")) (("1" (name-replace "RR" "(l!1 - LIMIT) / 4") (("1" (inst -17 "RR") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (expand "o" -17) (("1" (expand "o") (("1" (inst-cp -14 "n!1") (("1" (expand "converges_upto?" -15) (("1" (flatten) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (inst -15 "RR") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (hide -14 -17 -18) (("1" (inst -16 "n!1") (("1" (inst -14 "n!2") (("1" (hide -13 -15) (("1" (assert) (("1" (inst -8 "n!1") (("1" (expand "abs" -14) (("1" (assert) (("1" (inst -7 "n!1" "n!2") (("1" (expand "abs" -13) (("1" (assert) (("1" (hide -7 -8) (("1" (inst -7 "n!2" "n!1") (("1" (replace -7 * rl) (("1" (hide -7) (("1" (inst -6 "n!2" "n!1") (("1" (inst - "II(u2!1(n!2))") (("1" (expand "RR") (("1" (hide-all-but (-1 -2 -3 -10 -11 -6)) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "o") (("2" (inst + "n!2") 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) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (hide-all-but (-3 1)) (("2" (rewrite "metric_convergence_def" *) (("2" (expand "convergence") (("2" (expand "metric_converges_to") (("2" (skosimp) (("2" (inst - "r!1") (("2" (expand "ball") (("2" (expand "member") (("2" (skosimp) (("2" (inst + "n!1") (("2" (skosimp) (("2" (inst - "i!1") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "o" 1) (("2" (expand "Im" 1) (("2" (expand "upper_bound?" 1) (("2" (skosimp) (("2" (typepred "s!1") (("2" (skolem - ("n!1")) (("2" (replace -1) (("2" (hide -1) (("2" (inst -3 "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -7)) (("2" (expand "increasing?") (("2" (expand "o ") (("2" (skolem + ("n!1" "m!1")) (("2" (inst - "u2!1(n!1)" "u2!1(m!1)") (("2" (flatten) (("2" (split) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "u2!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (inst - "n!1" "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "o" 1) (("2" (expand "bounded_above?") (("2" (inst + "l!1") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst -8 "n!1") (("2" (expand "converges_upto?" -8) (("2" (flatten) (("2" (rewrite "metric_convergence_def" *) (("2" (expand "metric_converges_to") (("2" (expand "ball") (("2" (expand "member") (("2" (case "l!1 < II(u2!1(n!1))") (("1" (hide 1) (("1" (inst -9 "II(u2!1(n!1))-l!1") (("1" (skosimp) (("1" (inst -9 "n!1+n!2") (("1" (assert) (("1" (expand "o" -9) (("1" (inst - "n!1" "n!1+n!2") (("1" (expand "o" -2) (("1" (expand "abs" -9) (("1" (assert) (("1" (inst - "n!1+n!2" "n!1") (("1" (expand "o" -3) (("1" (inst - "n!1+n!2") (("1" (inst - "n!1" "n!1+n!2") (("1" (expand "o") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (skosimp) (("2" (expand "o") (("2" (expand "U1") (("2" (inst - "min(u1!1(m!1), u2!1(n!1))" "u2!1(n!1)") (("1" (assert) (("1" (hide 1) (("1" (grind) nil nil)) nil)) nil) ("2" (typepred "u1!1(m!1)") (("2" (typepred "u2!1(n!1)") (("2" (hide -1 -3 2) (("2" (expand "nn_isf?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (skosimp) (("2" (expand "U2") (("2" (expand "o ") (("2" (inst - "min(u2!1(m!1), u1!1(n!1))" "u1!1(n!1)") (("1" (assert) (("1" (hide 1) (("1" (grind) nil nil)) nil)) nil) ("2" (typepred "u2!1(m!1)") (("2" (typepred "u1!1(n!1)") (("2" (hide -1 -3 2) (("2" (expand "nn_isf?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (case "l!1<II(u1!1(n!1))") (("1" (hide 1) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (inst -10 "II(u1!1(n!1))-l!1") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (expand "o" -10) (("1" (inst -10 "n!1+n!2") (("1" (assert) (("1" (typepred "u1!1") (("1" (expand "increasing_nn_isf?") (("1" (expand "pointwise_increasing?") (("1" (inst -5 "u1!1(n!1)" "u1!1(n!1 + n!2)") (("1" (split -5) (("1" (expand "abs" -11) (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (inst - "n!1" "n!1+n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "U2") (("2" (expand "U1") (("2" (expand "o") (("2" (case-replace "min(u1!1(m!1), u2!1(n!1))=min(u2!1(n!1), u1!1(m!1))") (("2" (hide 2) (("2" (grind) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -4 -7 1)) (("2" (skosimp) (("2" (expand "o") (("2" (inst -3 "n!1") (("2" (expand "converges_upto?") (("2" (flatten) (("2" (expand "increasing?") (("2" (expand "U2") (("2" (inst-cp - "min(u2!1(m!1), u1!1(n!1))" "u1!1(n!1)") (("1" (split -2) (("1" (case "II(u1!1(n!1))<=l!1") (("1" (assert) nil nil) ("2" (case "l!1<II(u1!1(n!1))") (("1" (hide-all-but (-1 -7 -3)) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (inst -3 "II(u1!1(n!1))-l!1") (("1" (skosimp) (("1" (inst -3 "n!1+n!2") (("1" (assert) (("1" (expand "ball") (("1" (inst - "u1!1(n!1)" "u1!1(n!1+n!2)") (("1" (split -2) (("1" (expand "abs") (("1" (assert) nil nil)) nil) ("2" (skosimp) (("2" (typepred "u1!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (inst - "n!1" "n!1+n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "u1!1(n!1)") (("2" (typepred "u2!1(m!1)") (("2" (hide -1 -3) (("2" (expand "nn_isf?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "nn_isf_TCC1") nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (lemma "isf_integral_le" ("i1" "i1!1" "i2" "i2!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (inst + "l!1") nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 2) (("2" (skosimp) (("2" (inst - "n!1") (("2" (lemma "isf_convergence" ("u" "U1(n!1)" "i" "u2!1(n!1)")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (assert) (("2" (hide-all-but 1) (("2" (expand "U1") (("2" (typepred "u1!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "min") (("2" (expand "increasing?") (("2" (skosimp) (("2" (inst - "x!2" "y!1") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "U1") (("2" (typepred "u1!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "increasing_nn_simple?") (("2" (split) (("1" (skosimp) (("1" (typepred "u1!1(n!2)") (("1" (typepred "u2!1(n!1)") (("1" (expand "nn_isf?") (("1" (expand "nn_simple?") (("1" (split) (("1" (skosimp) (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (hide-all-but (-2 -4 1)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "isf?") (("2" (flatten) (("2" (rewrite "simple_min") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (skosimp) (("2" (inst - "x!2" "y!1") (("2" (assert) (("2" (expand "min") (("2" (grind) 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" (skosimp) (("2" (inst -2 "n!1") (("2" (hide -1) (("2" (lemma "isf_convergence" ("u" "U2(n!1)" "i" "u1!1(n!1)")) (("1" (split -1) (("1" (propax) nil nil) ("2" (expand "pointwise_converges_upto?") (("2" (assert) (("2" (hide-all-but 1) (("2" (expand "U2") (("2" (typepred "u2!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (skosimp*) (("2" (inst - "x!2" "y!1") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "U2") (("2" (typepred "u2!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "increasing_nn_simple?") (("2" (split) (("1" (skosimp) (("1" (expand "nn_simple?") (("1" (split) (("1" (hide -1) (("1" (skosimp) (("1" (typepred "u2!1(n!2)") (("1" (typepred "u1!1(n!1)") (("1" (expand "nn_isf?") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (expand "min") (("1" (hide -1 -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (typepred "u2!1(n!2)") (("2" (typepred "u1!1(n!1)") (("2" (expand "isf?") (("2" (flatten) (("2" (rewrite "simple_min") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "min") (("2" (expand "increasing?") (("2" (skosimp) (("2" (inst - "x!2" "y!1") (("2" (assert) (("2" (grind) 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 -1 -2 -3 2) (("2" (skosimp) (("2" (expand "pointwise_convergence?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (hide -3) (("2" (expand "U1") (("2" (rewrite "metric_convergence_def" *) (("2" (rewrite "metric_convergence_def" *) (("2" (rewrite "metric_convergence_def" *) (("2" (expand "metric_converges_to") (("2" (skosimp) (("2" (inst - "r!1/2") (("2" (inst - "r!1/2") (("2" (skosimp*) (("2" (inst + "n!1+n!2+n!3") (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (expand "ball") (("2" (expand "member") (("2" (assert) (("2" (typepred "u2!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (inst - "n!1" "i!1") (("2" (assert) (("2" (grind) 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" (hide -1 -2 2) (("2" (skosimp) (("2" (expand "U2") (("2" (expand "pointwise_convergence?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "min") (("2" (hide -3) (("2" (typepred "u2!1") (("2" (typepred "u1!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (rewrite "metric_convergence_def" *) (("2" (rewrite "metric_convergence_def" *) (("2" (rewrite "metric_convergence_def" *) (("2" (expand "metric_converges_to") (("2" (skosimp) (("2" (inst -3 "r!1/2") (("2" (inst -4 "r!1/2") (("2" (skosimp*) (("2" (expand "ball") (("2" (expand "member") (("2" (inst + "n!1+n!2+n!3") (("2" (skosimp) (("2" (inst -4 "i!1") (("2" (inst -5 "i!1") (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (assert) (("2" (expand "increasing?") (("2" (inst - "n!1" "i!1") (("2" (assert) (("2" (hide -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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (sequence type-eq-decl nil sequences nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (min const-decl "[T -> real]" real_fun_ops_aux "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (T formal-type-decl nil nn_integral 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) (isf_min application-judgement "isf[T, S, m]" nn_integral nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nn_integrable? const-decl "bool" nn_integral nil) (nn_integrable nonempty-type-eq-decl nil nn_integral nil) (real_minus_real_is_real application-judgement "real" reals nil) (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[real]" convergence_aux "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" convergence_aux "metric_space/") (convergence? const-decl "bool" topological_convergence "topology/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nn_isf_TCC1 subtype-tcc nil nn_integral nil) (isf_integral_zero formula-decl nil isf nil) (U2 skolem-const-decl "[nat -> [nat -> isf[T, S, m]]]" nn_integral nil) (m!1 skolem-const-decl "nat" nn_integral nil) (n!1 skolem-const-decl "nat" nn_integral nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (l!1 skolem-const-decl "real" nn_integral nil) (n!1 skolem-const-decl "nat" nn_integral nil) (< const-decl "bool" reals nil) (increasing_bounded_convergence formula-decl nil convergence_sequences "analysis/") (bounded_above? const-decl "bool" real_fun_preds "reals/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (increasing? const-decl "bool" real_fun_preds "reals/") (sup const-decl "real" real_fun_supinf "analysis/") (upper_bound? const-decl "bool" bounded_real_defs nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (RR skolem-const-decl "real" nn_integral nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (n!2 skolem-const-decl "nat" nn_integral nil) (u2!1 skolem-const-decl "increasing_nn_isf" nn_integral nil) (II skolem-const-decl "[isf[T, S, m] -> real]" nn_integral nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (minus_real_is_real application-judgement "real" reals nil) (convergence const-decl "bool" convergence_sequences "analysis/") (Im const-decl "setof[real]" real_fun_props "reals/") (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence "extended_nnreal/") (U1 skolem-const-decl "[nat -> [nat -> isf[T, S, m]]]" nn_integral nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (n!1 skolem-const-decl "nat" nn_integral nil) (m!1 skolem-const-decl "nat" nn_integral nil) (u1!1 skolem-const-decl "increasing_nn_isf" nn_integral nil) (n!1 skolem-const-decl "nat" nn_integral nil) (n!1 skolem-const-decl "nat" nn_integral nil) (m!1 skolem-const-decl "nat" nn_integral nil) (isf_integral_le formula-decl nil isf nil) (limit_def formula-decl nil hausdorff_convergence "topology/") (convergent type-eq-decl nil topological_convergence "topology/") (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/") (convergent? const-decl "bool" topological_convergence "topology/") (isf_convergence formula-decl nil isf nil) (measurable_function? const-decl "bool" measure_space_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (increasing_nn_simple? const-decl "bool" measure_space nil) (increasing_nn_simple nonempty-type-eq-decl nil measure_space nil) (pointwise_converges_upto? const-decl "bool" pointwise_convergence nil) (simple_min judgement-tcc nil measure_space nil) (simple? const-decl "bool" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil) (nn_simple? const-decl "bool" measure_space nil) (isf_integral const-decl "real" isf nil) (O const-decl "T3" function_props nil) (converges_upto? const-decl "bool" convergence_aux "metric_space/")) shostak)) (nn_integral_TCC1 0 (nn_integral_TCC1-1 nil 3395142648 ("" (skosimp) (("" (typepred "f!1") (("" (expand "nn_integrable?") (("" (skosimp) (("" (expand "nonempty?") (("" (expand "empty?") (("" (inst - "u!1") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (sequence type-eq-decl nil sequences nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (nonempty? const-decl "bool" sets nil)) nil)) (nn_integral_TCC2 0 (nn_integral_TCC2-1 nil 3395142648 ("" (skosimp) (("" (lemma "nn_integral_TCC1" ("f" "f!1")) (("" (lemma "choose_member" ("a" "{u | pointwise_convergence?[T](u, f!1)}")) (("" (split -1) (("1" (name-replace "U" "choose({u | pointwise_convergence?[T](u, f!1)})") (("1" (expand "member") (("1" (expand "o" 1) (("1" (hide -2) (("1" (typepred "U") (("1" (hide -2) (("1" (typepred "f!1") (("1" (expand "nn_integrable?") (("1" (skosimp) (("1" (lemma "nn_convergence" ("f" "f!1" "u1" "u!1" "u2" "U")) (("1" (assert) (("1" (flatten) (("1" (expand "o" -1) (("1" (propax) 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) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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 nn_integral nil) (nn_integral_TCC1 subtype-tcc nil nn_integral nil) (member const-decl "bool" sets nil) (nn_convergence formula-decl nil nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (O const-decl "T3" function_props nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (choose_member formula-decl nil sets_lemmas nil) (set type-eq-decl nil sets nil) (pointwise_convergence? const-decl "bool" pointwise_convergence 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) (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" nn_integral nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil) (isf? const-decl "bool" isf nil) (isf nonempty-type-eq-decl nil isf nil) (nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (sequence type-eq-decl nil sequences nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil)) nil)) (nn_integral_TCC3 0 (nn_integral_TCC3-1 nil 3395152739 ("" (skosimp) (("" (lemma "nn_integral_TCC1" ("f" "f!1")) (("" (lemma "nn_integral_TCC2" ("f" "f!1")) (("" (lemma "choose_member" ("a" "{u | pointwise_convergence?[T](u, f!1)}")) (("" (split -1) (("1" (name-replace "U" "choose({u | pointwise_convergence?[T](u, f!1)})") (("1" (expand "member") (("1" (hide -3) (("1" (expand "convergent?") (("1" (skosimp) (("1" (lemma "hausdorff_convergence.limit_def" ("v" "o[nat, isf[T, S, m], real](isf_integral[T, S, m], U)" "l" "l!1")) (("1" (assert) (("1" (expand "limit" 1) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "metric_convergence_def" -) (("1" (case "l!1<0") (("1" (hide 1) (("1" (expand "metric_converges_to") (("1" (inst - "-l!1") (("1" (skosimp) (("1" (inst - "n!1") (("1" (assert) (("1" (expand "ball") (("1" (expand "o" -3) (("1" (lemma "isf_integral_pos" ("i" "U(n!1)")) (("1" (split -1) (("1" (name-replace "II" "isf_integral(U(n!1))") (("1" (hide -3) (("1" (grind) nil nil)) nil)) nil) ("2" (typepred "U(n!1)") (("2" (expand "nn_isf?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) 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) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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 nn_integral nil) (nn_integral_TCC1 subtype-tcc nil nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (sequence type-eq-decl nil sequences nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (set type-eq-decl nil sets nil) (choose_member formula-decl nil sets_lemmas nil) (= const-decl "[T, T -> boolean]" equalities nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (l!1 skolem-const-decl "real" nn_integral nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (isf_integral_pos formula-decl nil isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (< const-decl "bool" reals nil) (limit macro-decl "[convergent -> real]" nn_integral nil) (limit_def formula-decl nil hausdorff_convergence "topology/") (convergent type-eq-decl nil topological_convergence "topology/") (O const-decl "T3" function_props nil) (isf_integral const-decl "real" isf 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/") (convergent? const-decl "bool" topological_convergence "topology/") (member const-decl "bool" sets nil) (nn_integral_TCC2 subtype-tcc nil nn_integral nil)) nil)) (nn_integrable_add 0 (nn_integrable_add-1 nil 3391018465 ("" (skosimp) (("" (typepred "f1!1") (("" (typepred "f2!1") (("" (split) (("1" (skosimp) (("1" (expand "+") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "nn_integrable?") (("2" (skosimp*) (("2" (inst + "u!2+u!1") (("1" (split) (("1" (hide -2 -4) (("1" (lemma "pointwise_convergence_sum" ("u" "u!2" "f0" "f1!1" "v" "u!1" "f1" "f2!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "convergent?") (("2" (skosimp*) (("2" (inst + "l!1+l!2") (("2" (hide-all-but (-2 -4 1)) (("2" (rewrite "metric_convergence_def" *) (("2" (rewrite "metric_convergence_def" *) (("2" (rewrite "metric_convergence_def" *) (("2" (expand "metric_converges_to") (("2" (skosimp) (("2" (inst - "r!1/2") (("2" (inst - "r!1/2") (("2" (skosimp*) (("2" (inst + " n!1+n!2") (("2" (skosimp) (("2" (inst - "i!1") (("2" (inst - "i!1") (("2" (assert) (("2" (expand "ball") (("2" (expand "o") (("2" (expand "+") (("2" (rewrite "isf_integral_add") (("2" (name-replace "I1" "isf_integral(u!1(i!1))") (("2" (name-replace "I2" "isf_integral(u!2(i!1))") (("2" (hide -1) (("2" (grind) 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" (typepred "u!1") (("2" (typepred "u!2") (("2" (split) (("1" (skosimp) (("1" (expand "+") (("1" (typepred "u!2(x1!1)") (("1" (typepred "u!1(x1!1)") (("1" (expand "nn_isf?") (("1" (skosimp) (("1" (expand "+") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "+") (("2" (expand "+") (("2" (expand "increasing?") (("2" (skosimp) (("2" (inst - "x!2" "y!1") (("2" (inst - "x!2" "y!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) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil nn_integral 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 "[T -> real]" real_fun_ops "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (isf_add application-judgement "isf" nn_integral nil) (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (increasing? const-decl "bool" real_fun_preds "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pointwise_convergence_sum formula-decl nil pointwise_convergence nil) (sum_measurable application-judgement "measurable_function[T, S]" nn_integral nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (= const-decl "[T, T -> boolean]" equalities 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_times_real_is_real application-judgement "real" reals nil) (isf_integral_add formula-decl nil isf nil) (member const-decl "bool" sets nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (- 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (isf_integral const-decl "real" isf nil) (O const-decl "T3" function_props nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (convergent? const-decl "bool" topological_convergence "topology/") (AND const-decl "[bool, bool -> bool]" booleans 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) (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" nn_integral nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil) (isf? const-decl "bool" isf nil) (sequence type-eq-decl nil sequences nil) (+ const-decl "sequence[[T -> real]]" pointwise_convergence nil) (isf nonempty-type-eq-decl nil isf nil) (nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (u!2 skolem-const-decl "increasing_nn_isf" nn_integral nil) (u!1 skolem-const-decl "increasing_nn_isf" nn_integral nil)) nil)) (nn_integrable_scal 0 (nn_integrable_scal-1 nil 3391018465 ("" (skosimp) (("" (typepred "f!1") (("" (typepred "c!1") (("" (expand "nn_integrable?") (("" (skosimp) (("" (split) (("1" (skosimp) (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "c!1*u!1") (("1" (split) (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (inst - "x!1") (("1" (expand "*") (("1" (expand "*") (("1" (hide -3) (("1" (rewrite "metric_convergence_def" *) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (case-replace "c!1=0") (("1" (inst + "0") (("1" (skosimp) (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "r!1" "py" "c!1")) (("1" (inst - "r!1 / c!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (lemma "abs_mult" ("x" "c!1" "y" "f!1(x!1) - u!1(i!1)(x!1)")) (("1" (expand "abs" -1 2) (("1" (replace -1 2) (("1" (rewrite "div_mult_pos_lt2" -5) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (expand "convergent?") (("2" (skosimp) (("2" (inst + "c!1*l!1") (("2" (rewrite "metric_convergence_def" *) (("2" (rewrite "metric_convergence_def" *) (("2" (expand "metric_converges_to") (("2" (skosimp) (("2" (expand "ball") (("2" (expand "member") (("2" (expand "o ") (("2" (expand "*") (("2" (case-replace "c!1=0") (("1" (inst + "0") (("1" (skosimp) (("1" (rewrite "isf_integral_scal") (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "r!1" "py" "c!1")) (("1" (inst - "r!1 / c!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (rewrite "isf_integral_scal") (("1" (lemma "abs_mult" ("x" "c!1" "y" "l!1 - isf_integral(u!1(i!1))")) (("1" (expand "abs" -1 2) (("1" (replace -1 2) (("1" (rewrite "div_mult_pos_lt2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "u!1") (("2" (split) (("1" (skosimp) (("1" (expand "*") (("1" (typepred "u!1(x1!1)") (("1" (expand "nn_isf?") (("1" (skosimp) (("1" (expand "*") (("1" (inst - "x!1") (("1" (assert) (("1" (case-replace "c!1=0") (("1" (assert) nil nil) ("2" (lemma "both_sides_times_pos_le1" ("x" "0" "y" "u!1(x1!1)(x!1)" "pz" "c!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "*") (("2" (expand "increasing?") (("2" (expand "*") (("2" (skosimp) (("2" (inst - "x!2" "y!1") (("2" (assert) (("2" (case-replace "c!1=0") (("1" (assert) nil nil) ("2" (lemma "both_sides_times_pos_le1" ("pz" "c!1" "x" "u!1(x!2)(x!1)" "y" "u!1(y!1)(x!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil nn_integral 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 "[T -> real]" real_fun_ops "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (increasing? const-decl "bool" real_fun_preds "reals/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (member const-decl "bool" sets nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (abs_mult formula-decl nil real_props nil) (r!1 skolem-const-decl "posreal" nn_integral nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (abs_nat formula-decl nil abs_lems "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (real_times_real_is_real application-judgement "real" reals nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (convergent? const-decl "bool" topological_convergence "topology/") (isf_scal application-judgement "isf" nn_integral nil) (r!1 skolem-const-decl "posreal" nn_integral nil) (isf_integral_scal formula-decl nil isf nil) (isf_integral const-decl "real" isf nil) (O const-decl "T3" function_props nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (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" nn_integral nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil) (isf? const-decl "bool" isf nil) (sequence type-eq-decl nil sequences nil) (* const-decl "sequence[[T -> real]]" pointwise_convergence nil) (c!1 skolem-const-decl "nnreal" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (u!1 skolem-const-decl "increasing_nn_isf" nn_integral nil)) nil)) (nn_isf_is_nn_integrable 0 (nn_isf_is_nn_integrable-1 nil 3395557668 ("" (skolem + ("i!1")) (("" (typepred "i!1") (("" (expand "nn_isf?") (("" (replace -2) (("" (expand "nn_integrable?") (("" (inst + "lambda n: i!1") (("1" (split) (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (expand "convergence?") (("1" (skosimp) (("1" (inst + "0") (("1" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "convergent?") (("2" (inst + "isf_integral(i!1)") (("2" (expand "o") (("2" (expand "convergence?") (("2" (skosimp) (("2" (inst + "0") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "increasing?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (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 nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (i!1 skolem-const-decl "nn_isf" nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (sequence type-eq-decl nil sequences 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) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (convergent? const-decl "bool" topological_convergence "topology/") (O const-decl "T3" function_props nil) (isf_integral const-decl "real" isf nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (convergence? const-decl "bool" topological_convergence "topology/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (increasing? const-decl "bool" real_fun_preds "reals/") (nn_integrable? const-decl "bool" nn_integral nil)) nil)) (nn_integral_isf 0 (nn_integral_isf-1 nil 3395144866 ("" (skosimp) (("" (typepred "i!1") (("" (lemma "nn_isf_is_nn_integrable") (("" (inst - "i!1") (("" (flatten) (("" (expand "nn_integral") (("" (case "nonempty?({u | pointwise_convergence?(u, i!1)})") (("1" (lemma "choose_member" ("a" "({u | pointwise_convergence?(u, i!1)})")) (("1" (name-replace "U" "choose({u | pointwise_convergence?(u, i!1)})") (("1" (split -1) (("1" (expand "member") (("1" (hide -2) (("1" (expand "nn_integrable?") (("1" (skosimp) (("1" (lemma "nn_convergence" ("f" "i!1" "u1" "u!1" "u2" "U")) (("1" (assert) (("1" (flatten) (("1" (replace -2 1 rl) (("1" (hide -1 -2 -3) (("1" (lemma "nn_convergence" ("f" "i!1" "u1" "u!1" "u2" "lambda n: i!1")) (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (replace -2 1) (("1" (hide -2) (("1" (rewrite "limit_def") (("1" (expand "o ") (("1" (expand "convergence?") (("1" (skosimp) (("1" (inst + "0") (("1" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "pointwise_convergence?") (("2" (skosimp) (("2" (expand "convergence?") (("2" (skosimp) (("2" (inst + "0") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -5)) (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "increasing?") (("2" (propax) 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) ("2" (hide 2) (("2" (expand "nn_integrable?") (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "u!1") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (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 nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nn_integral const-decl "nnreal" nn_integral nil) (empty? const-decl "bool" sets nil) (choose_member formula-decl nil sets_lemmas 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) (O const-decl "T3" function_props nil) (convergent type-eq-decl nil topological_convergence "topology/") (convergent? const-decl "bool" topological_convergence "topology/") (isf_integral const-decl "real" isf nil) (limit_def formula-decl nil hausdorff_convergence "topology/") (convergence? const-decl "bool" topological_convergence "topology/") (increasing? const-decl "bool" real_fun_preds "reals/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_convergence formula-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (member const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (choose const-decl "(p)" 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) (sequence type-eq-decl nil sequences nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (nn_isf_is_nn_integrable judgement-tcc nil nn_integral nil)) shostak)) (nn_integrable_le_TCC1 0 (nn_integrable_le_TCC1-1 nil 3395193452 ("" (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 nn_integral nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (nn_integrable? const-decl "bool" nn_integral nil) (nn_integrable nonempty-type-eq-decl nil nn_integral 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" nn_integral nil) (measurable_function? const-decl "bool" measure_space_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (measurable_set? const-decl "bool" measure_space_def nil) (convergent? const-decl "bool" topological_convergence "topology/") (O const-decl "T3" function_props nil) (isf_integral const-decl "real" isf nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (image const-decl "set[R]" function_image nil) (mu const-decl "nnreal" measure_props nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (convergence? const-decl "bool" topological_convergence "topology/") (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/") (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (sequence type-eq-decl nil sequences nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf 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) (increasing? const-decl "bool" real_fun_preds "reals/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (nn_integrable_le 0 (nn_integrable_le-1 nil 3395343631 ("" (skosimp) (("" (typepred "f!1") (("" (typepred "g!1") (("" (expand "nn_integrable?" -2) (("" (skosimp) (("" (lemma "nn_measurable_def" ("f" "g!1")) (("" (replace -2) (("" (split -1) (("1" (flatten) (("1" (skosimp) (("1" (typepred "w!1") (("1" (name "U" "lambda n: min(u!1(n),w!1(n))") (("1" (case "increasing_nn_isf?(U)") (("1" (hide -2) (("1" (case "forall n: nn_isf?(U(n))") (("1" (case "pointwise_converges_upto?(U, g!1)") (("1" (case "FORALL n: isf_integral(U(n)) <= (isf_integral o u!1)(n)") (("1" (case "convergent?(isf_integral o U)") (("1" (split 1) (("1" (expand "nn_integrable?" 1) (("1" (inst + "U") (("1" (expand "pointwise_converges_upto?") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "nn_integral") (("2" (case "nonempty?({u | pointwise_convergence?(u, f!1)})") (("1" (lemma "choose_member" ("a" "{u | pointwise_convergence?(u, f!1)}")) (("1" (split -1) (("1" (name-replace "CU" "choose({u | pointwise_convergence?(u, f!1)})") (("1" (expand "member") (("1" (lemma "nn_convergence" ("u1" "u!1" "u2" "CU" "f" "f!1")) (("1" (assert) (("1" (flatten) (("1" (replace -2 1 rl) (("1" (hide -1 -2 -3 -4) (("1" (case "nonempty?({u_1: increasing_nn_isf | pointwise_convergence?(u_1, g!1)})") (("1" (lemma "choose_member" ("a" "({u_1: increasing_nn_isf | pointwise_convergence?(u_1, g!1)})")) (("1" (split -1) (("1" (name-replace "CUG" "choose({u_1: increasing_nn_isf | pointwise_convergence?(u_1, g!1)})") (("1" (expand "member") (("1" (hide -2) (("1" (lemma "nn_convergence" ("f" "g!1")) (("1" (inst - "U" "CUG") (("1" (assert) (("1" (expand "pointwise_converges_upto?") (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (replace -2 1 rl) (("1" (hide -1 -2 -3) (("1" (expand "convergent?") (("1" (skosimp*) (("1" (lemma "hausdorff_convergence.limit_def" ("v" "isf_integral o U" "l" "l!1")) (("1" (lemma "hausdorff_convergence.limit_def" ("v" "isf_integral o u!1" "l" "l!2")) (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (case "l!1>l!2") (("1" (hide 1) (("1" (rewrite "metric_convergence_def" *) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (expand "ball") (("1" (expand "member") (("1" (inst - "(l!1-l!2)/2") (("1" (inst -13 "(l!1-l!2)/2") (("1" (skosimp*) (("1" (inst - "n!1+n!2") (("1" (inst -13 "n!1+n!2") (("1" (assert) (("1" (inst - "n!1+n!2") (("1" (expand "o") (("1" (name-replace "IL" "isf_integral(U(n!1 + n!2))") (("1" (name-replace "IH" "isf_integral(u!1(n!1 + n!2))") (("1" (hide-all-but (-1 -2 -3 -13)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (inst -12 "x1!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "nn_integrable?") (("2" (inst + "U") (("2" (assert) (("2" (expand "pointwise_converges_upto?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2 -1 -2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "U") (("2" (expand "pointwise_converges_upto?") (("2" (flatten) 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) ("2" (hide-all-but (-9 1)) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "u!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "increasing_bounded_convergence" ("v1" "isf_integral o U")) (("1" (split -1) (("1" (expand "convergent?") (("1" (expand "sup" -1) (("1" (inst + "lub(Im(isf_integral o U))") (("1" (hide-all-but (-1 1)) (("1" (rewrite "metric_convergence_def") (("1" (expand "convergence") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst - "r!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (expand "ball") (("1" (name-replace "DRL1" "lub(Im(isf_integral o U))") (("1" (name-replace "DRL2" "(isf_integral o U)(i!1)") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (expand "increasing?") (("2" (skolem + ("n!1" "n!2")) (("2" (flatten) (("2" (expand "o") (("2" (lemma "isf_integral_le" ("i1" "U(n!1)" "i2" "U(n!2)")) (("2" (split -1) (("1" (propax) nil nil) ("2" (skosimp) (("2" (inst -5 "x!1") (("2" (inst -5 "n!1" "n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "bounded_above?") (("2" (expand "convergent?") (("2" (skosimp) (("2" (inst + "l!1") (("2" (skolem + ("n!1")) (("2" (expand "o") (("2" (inst - "n!1") (("2" (name-replace "IL" "isf_integral[T, S, m](U(n!1))") (("2" (rewrite "metric_convergence_def" *) (("2" (expand "metric_converges_to") (("2" (case "l!1<IL") (("1" (hide 1) (("1" (expand "ball") (("1" (expand "member") (("1" (inst -10 "IL-l!1") (("1" (skosimp) (("1" (inst -10 "n!1+n!2") (("1" (assert) (("1" (hide-all-but (-1 -2 -10 -11)) (("1" (lemma "isf_integral_le" ("i1" "u!1(n!1)" "i2" "u!1(n!1+n!2)")) (("1" (split -1) (("1" (name-replace "II1" "isf_integral(u!1(n!1))") (("1" (name-replace "II2" "isf_integral(u!1(n!1+n!2))") (("1" (hide -5) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "u!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (inst - "n!1" "n!1+n!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "o" 1) (("2" (lemma "isf_integral_le" ("i1" "U(n!1)" "i2" "u!1(n!1)")) (("2" (assert) (("2" (hide 2) (("2" (skosimp) (("2" (expand "U") (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (case-replace "pointwise_increasing?(U)") (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (inst -5 "x!1") (("1" (inst -8 "x!1") (("1" (inst -10 "x!1") (("1" (flatten) (("1" (hide -9) (("1" (rewrite "metric_convergence_def" *) (("1" (rewrite "metric_convergence_def" *) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (expand "U") (("1" (hide -2) (("1" (expand "min" 1) (("1" (case-replace "g!1(x!1)=f!1(x!1)") (("1" (inst - "r!1/2") (("1" (inst - "r!1/2") (("1" (skosimp*) (("1" (inst + "n!1+n!2") (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst - "i!1") (("1" (assert) (("1" (hide-all-but (-6 -9 1)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "g!1(x!1)<f!1(x!1)") (("1" (hide -10 1) (("1" (inst - "r!1/2") (("1" (inst - "r!1/2") (("1" (skosimp*) (("1" (inst + "n!1+n!2") (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst - "i!1") (("1" (assert) (("1" (hide-all-but (-1 -6 -9 1)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) ("2" (hide 2) (("2" (expand "U") (("2" (expand "increasing_nn_isf?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "U") (("2" (skosimp) (("2" (typepred "u!1(n!1)") (("2" (hide-all-but (-1 -2 -4 1)) (("2" (expand "nn_isf?") (("2" (skosimp) (("2" (expand "min") (("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (expand "nn_simple?") (("2" (inst - "x!1") (("2" (inst - "n!1") (("2" (flatten) (("2" (inst - "x!1") (("2" (hide -1 -4 -5) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2 -3 -4 -5 -6) (("3" (expand "increasing_nn_simple?") (("3" (flatten) (("3" (skosimp) (("3" (expand "U") (("3" (typepred "u!1(n!1)") (("3" (expand "isf?") (("3" (flatten) (("3" (expand "increasing_nn_isf?") (("3" (hide -4) (("3" (inst - "n!1") (("3" (expand "nn_simple?") (("3" (flatten) (("3" (rewrite "simple_min") (("3" (lemma "m_monotone" ("a" "nonzero_set?(min(u!1(n!1), w!1(n!1)))" "b" "nonzero_set?(u!1(n!1))")) (("3" (split -1) (("1" (expand "x_le") (("1" (expand "mu_fin?") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "subset?") (("2" (expand "nonzero_set?") (("2" (expand "member") (("2" (skosimp) (("2" (expand "min") (("2" (replace -1) (("2" (inst - "x!1") (("2" (hide-all-but (-5 1)) (("2" (grind) 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 -3 -5 -6) (("2" (expand "U") (("2" (typepred "u!1") (("2" (hide -2) (("2" (expand "increasing_nn_isf?") (("2" (expand "increasing_nn_simple?") (("2" (flatten) (("2" (hide -2 -4) (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (skosimp) (("2" (inst - "x!2" "y!1") (("2" (inst - "x!2" "y!1") (("2" (assert) (("2" (hide-all-but (-1 -3 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "U") (("3" (typepred "u!1(x1!1)") (("3" (expand "nn_isf?") (("3" (expand "increasing_nn_simple?") (("3" (flatten) (("3" (hide -3) (("3" (hide 2) (("3" (split) (("1" (expand "isf?") (("1" (flatten) (("1" (inst -4 "x1!1") (("1" (expand "nn_simple?") (("1" (flatten) (("1" (rewrite "simple_min") (("1" (lemma "m_monotone" ("a" "nonzero_set?(min(u!1(x1!1), w!1(x1!1)))" "b" "nonzero_set?(u!1(x1!1))")) (("1" (split -1) (("1" (expand "x_le") (("1" (expand "mu_fin?") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "nonzero_set?") (("2" (expand "min") (("2" (expand "min") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (assert) (("2" (typepred "w!1") (("2" (expand "increasing_nn_simple?") (("2" (expand "nn_simple?") (("2" (flatten) (("2" (inst - "x1!1") (("2" (flatten) (("2" (inst - "x!1") (("2" (grind) 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" (inst - "x1!1") (("2" (expand "nn_simple?") (("2" (flatten) (("2" (inst - "x!1") (("2" (hide-all-but (-2 -3 1)) (("2" (grind) 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" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nn_measurable_def formula-decl nil measure_space nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (min const-decl "[T -> real]" real_fun_ops_aux "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (min_measurable application-judgement "measurable_function[T, S]" nn_integral nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (subset_algebra_fullset name-judgement "(S)" nn_integral nil) (measurable_fullset name-judgement "measurable_set[T, S]" nn_integral nil) (m_monotone formula-decl nil measure_props nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (nonzero_set? const-decl "set[T]" isf nil) (subset? const-decl "bool" sets nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (mu_fin? const-decl "bool" measure_props nil) (simple_min judgement-tcc nil measure_space nil) (simple? const-decl "bool" measure_space nil) (simple nonempty-type-eq-decl nil measure_space nil) (nn_simple? const-decl "bool" measure_space nil) (pointwise_converges_upto? const-decl "bool" pointwise_convergence nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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/") (convergent? const-decl "bool" topological_convergence "topology/") (nn_integral const-decl "nnreal" nn_integral nil) (choose_member formula-decl nil sets_lemmas nil) (choose const-decl "(p)" sets nil) (nn_convergence formula-decl nil nn_integral nil) (empty? const-decl "bool" sets nil) (limit_def formula-decl nil hausdorff_convergence "topology/") (convergent type-eq-decl nil topological_convergence "topology/") (> const-decl "bool" reals nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (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) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (U skolem-const-decl "[nat -> measurable_function[T, S]]" nn_integral nil) (increasing_bounded_convergence formula-decl nil convergence_sequences "analysis/") (bounded_above? const-decl "bool" real_fun_preds "reals/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (isf_integral_le formula-decl nil isf nil) (increasing? const-decl "bool" real_fun_preds "reals/") (nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence "extended_nnreal/") (Im const-decl "setof[real]" real_fun_props "reals/") (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (convergence const-decl "bool" convergence_sequences "analysis/") (sup const-decl "real" real_fun_supinf "analysis/") (< const-decl "bool" reals nil) (IL skolem-const-decl "real" nn_integral nil) (l!1 skolem-const-decl "real" nn_integral nil) (O const-decl "T3" function_props nil) (isf_integral const-decl "real" isf nil) (<= const-decl "bool" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (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) (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" nn_integral nil) (measurable_function? const-decl "bool" measure_space_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil)) shostak)) (nn_integral_zero 0 (nn_integral_zero-1 nil 3395147020 ("" (lemma "nn_integral_isf" ("i" "lambda x: 0")) (("1" (rewrite "isf_integral_zero") nil nil) ("2" (lemma "isf_zero") (("2" (assert) (("2" (expand "nn_isf?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((isf_zero formula-decl nil isf nil) (isf_integral_zero formula-decl nil isf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nn_integral_isf formula-decl nil nn_integral nil) (T formal-type-decl nil nn_integral 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" nn_integral nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil) (isf? const-decl "bool" isf nil) (isf nonempty-type-eq-decl nil isf nil) (nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil)) shostak)) (nn_integral_phi_TCC1 0 (nn_integral_phi_TCC1-1 nil 3391018465 ("" (skosimp) (("" (lemma "nn_isf_is_nn_integrable" ("x" "phi[T, S](F!1)")) (("1" (flatten) nil nil) ("2" (hide 2) (("2" (expand "nn_isf?") (("2" (skosimp) (("2" (expand "phi") (("2" (expand "member") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mu_fin? const-decl "bool" measure_props nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (phi const-decl "nat" measure_space nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (set type-eq-decl nil sets nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (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 nn_integral nil) (nn_isf_is_nn_integrable judgement-tcc nil nn_integral nil) (isf_phi application-judgement "isf" nn_integral nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil)) nil)) (nn_integral_phi_TCC2 0 (nn_integral_phi_TCC2-1 nil 3395557668 ("" (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 nn_integral nil) (set type-eq-decl nil sets 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" nn_integral nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil) (mu_fin? const-decl "bool" measure_props nil)) nil)) (nn_integral_phi 0 (nn_integral_phi-1 nil 3395154554 ("" (skosimp) (("" (lemma "nn_integral_isf" ("i" "phi(F!1)")) (("1" (rewrite "isf_integral_phi") nil nil) ("2" (lemma "isf_phi" ("E" "F!1")) (("2" (expand "nn_isf?") (("2" (skosimp) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mu_fin? const-decl "bool" measure_props nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (phi const-decl "nat" measure_space nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (set type-eq-decl nil sets nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (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 nn_integral nil) (nn_integral_isf formula-decl nil nn_integral nil) (isf_phi application-judgement "isf" nn_integral nil) (isf_integral_phi formula-decl nil isf nil) (member const-decl "bool" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (isf_phi judgement-tcc nil isf nil)) shostak)) (nn_integral_add 0 (nn_integral_add-1 nil 3395193493 ("" (skosimp) (("" (typepred "f2!1") (("" (typepred "f1!1") (("" (lemma "nn_integrable_add" ("f1" "f1!1" "f2" "f2!1")) (("" (flatten) (("" (expand "nn_integral") (("" (case "nonempty?({u | pointwise_convergence?(u, f2!1)})") (("1" (lemma "choose_member" ("a" "({u | pointwise_convergence?(u, f2!1)})")) (("1" (split -1) (("1" (name-replace "CU2" "choose({u | pointwise_convergence?(u, f2!1)})") (("1" (expand "member") (("1" (case "nonempty?({u_1: increasing_nn_isf | pointwise_convergence?(u_1, f1!1)})") (("1" (lemma "choose_member" ("a" "({u_1: increasing_nn_isf | pointwise_convergence?(u_1, f1!1)})")) (("1" (name-replace "CU1" "choose(({u_1: increasing_nn_isf | pointwise_convergence?(u_1, f1!1)}))") (("1" (split -1) (("1" (case "nonempty?({u_2: increasing_nn_isf | pointwise_convergence?(u_2, f1!1 + f2!1)})") (("1" (lemma "choose_member" ("a" "({u_2: increasing_nn_isf | pointwise_convergence?(u_2, f1!1 + f2!1)})")) (("1" (split -1) (("1" (name-replace "CU" "choose(({u_2: increasing_nn_isf | pointwise_convergence?(u_2, f1!1 + f2!1)}))") (("1" (expand "member") (("1" (hide -2 -4 -6) (("1" (expand "nn_integrable?") (("1" (skolem - ("u!3")) (("1" (skosimp*) (("1" (lemma "nn_convergence" ("f" "f1!1" "u1" "u!1" "u2" "CU1")) (("1" (assert) (("1" (flatten) (("1" (replace -2 * rl) (("1" (lemma "nn_convergence" ("f" "f2!1" "u1" "u!2" "u2" "CU2")) (("1" (assert) (("1" (flatten) (("1" (replace -2 * rl) (("1" (lemma "nn_convergence" ("f" "f1!1+f2!1" "u1" "u!3" "u2" "CU")) (("1" (assert) (("1" (flatten) (("1" (replace -2 * rl) (("1" (hide-all-but (1 -10 -11 -12 -13 -14 -15 -16)) (("1" (lemma "nn_convergence" ("f" "f1!1+f2!1" "u1" "u!3" "u2" "u!1+u!2")) (("1" (assert) (("1" (lemma "pointwise_convergence_sum" ("u" "u!1" "f0" "f1!1" "v" "u!2" "f1" "f2!1")) (("1" (assert) (("1" (flatten) (("1" (replace -3 1) (("1" (hide -1 -2 -3 -5 -6) (("1" (case-replace "isf_integral o (u!1 + u!2) = (isf_integral o u!1)+(isf_integral o u!2)") (("1" (hide -1) (("1" (name-replace "I1" "isf_integral o u!1") (("1" (name-replace "I2" "isf_integral o u!2") (("1" (hide -1 -2 -4) (("1" (expand "convergent?") (("1" (skosimp*) (("1" (lemma "hausdorff_convergence.limit_def" ("v" "I2" "l" "l!2")) (("1" (lemma "hausdorff_convergence.limit_def" ("v" "I1" "l" "l!1")) (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (rewrite "hausdorff_convergence.limit_def") (("1" (rewrite "metric_convergence_def" *) (("1" (rewrite "metric_convergence_def" *) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst - "r!1/2") (("1" (inst - "r!1/2") (("1" (skosimp*) (("1" (inst + "n!1+n!2") (("1" (skosimp) (("1" (inst - "i!1") (("1" (inst - "i!1") (("1" (assert) (("1" (expand "ball") (("1" (expand "+") (("1" (hide -3) (("1" (grind) 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" (apply-extensionality :hide? t) (("2" (expand "+") (("2" (expand "o") (("2" (rewrite "isf_integral_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "+") (("1" (skosimp) (("1" (typepred "u!1(x1!1)") (("1" (typepred "u!2(x1!1)") (("1" (expand "nn_isf?") (("1" (skosimp) (("1" (expand "+") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "u!1") (("2" (typepred "u!2") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (expand "+") (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (skosimp) (("2" (inst - "x!2" "y!1") (("2" (inst - "x!2" "y!1") (("2" (assert) (("2" (expand "+") (("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)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-6 1)) (("2" (expand "nn_integrable?") (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "u!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (expand "nn_integrable?") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "u!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (expand "nn_integrable?") (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "u!1") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nn_integrable_add judgement-tcc nil nn_integral nil) (nn_integral const-decl "nnreal" nn_integral nil) (choose_member formula-decl nil sets_lemmas nil) (choose const-decl "(p)" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (nn_integrable_add application-judgement "nn_integrable" nn_integral nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "sequence[[T -> real]]" pointwise_convergence nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pointwise_convergence_sum formula-decl nil pointwise_convergence nil) (isf_integral_add formula-decl nil isf nil) (convergent? const-decl "bool" topological_convergence "topology/") (limit_def formula-decl nil hausdorff_convergence "topology/") (convergent type-eq-decl nil topological_convergence "topology/") (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/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (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_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (O const-decl "T3" function_props nil) (isf_integral const-decl "real" isf nil) (isf_add application-judgement "isf" nn_integral nil) (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (increasing? const-decl "bool" real_fun_preds "reals/") (nn_convergence formula-decl nil nn_integral nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" 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) (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" nn_integral nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil) (isf? const-decl "bool" isf nil) (isf nonempty-type-eq-decl nil isf nil) (nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (sequence type-eq-decl nil sequences nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil)) shostak)) (nn_integral_scal 0 (nn_integral_scal-1 nil 3395195780 ("" (skosimp) (("" (typepred "f!1") (("" (expand "nn_integral") (("" (lemma "nn_integrable_scal" ("c" "c!1" "f" "f!1")) (("" (flatten) (("" (expand "nn_integrable?") (("" (skosimp*) (("" (case "nonempty?({u | pointwise_convergence?(u, f!1)})") (("1" (lemma "choose_member" ("a" "({u | pointwise_convergence?(u, f!1)})")) (("1" (split -1) (("1" (name-replace "U2" "choose({u | pointwise_convergence?(u, f!1)})") (("1" (case "nonempty?({u_1: increasing_nn_isf | pointwise_convergence?(u_1, c!1 * f!1)})") (("1" (lemma "choose_member" ("a" "({u_1: increasing_nn_isf | pointwise_convergence?(u_1, c!1 * f!1)})")) (("1" (split -1) (("1" (name-replace "U1" "choose(({u_1: increasing_nn_isf | pointwise_convergence?(u_1, c!1 * f!1)}))") (("1" (expand "member") (("1" (hide -2 -4) (("1" (lemma "nn_convergence" ("u1" "u!1" "f" "c!1*f!1" "u2" "U1")) (("1" (assert) (("1" (flatten) (("1" (replace -2 1 rl) (("1" (hide -1 -2 -3) (("1" (lemma "nn_convergence" ("u1" "u!2" "f" "f!1" "u2" "U2")) (("1" (assert) (("1" (flatten) (("1" (replace -2 1 rl) (("1" (hide -1 -2 3) (("1" (lemma "nn_convergence" ("u1" "u!1" "f" "c!1*f!1" "u2" "c!1*u!2")) (("1" (assert) (("1" (lemma "pointwise_convergence_scal" ("u" "u!2" "f" "f!1" "c" "c!1")) (("1" (assert) (("1" (flatten) (("1" (replace -3) (("1" (hide -3 -4 -7 -6) (("1" (case-replace "isf_integral o (c!1 * u!2) = c!1*(isf_integral o u!2)") (("1" (hide -1) (("1" (rewrite "hausdorff_convergence.limit_def" 1) (("1" (hide -1 -2 -3) (("1" (expand "convergent?") (("1" (skosimp) (("1" (lemma "hausdorff_convergence.limit_def" ("v" "isf_integral o u!2" "l" "l!1")) (("1" (assert) (("1" (replace -1) (("1" (hide -1 -2) (("1" (rewrite "metric_convergence_def" *) (("1" (rewrite "metric_convergence_def" *) (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (name-replace "FF" "isf_integral o u!2") (("1" (expand "*") (("1" (case-replace "c!1=0") (("1" (inst + "0") (("1" (skosimp) (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "r!1" "py" "c!1")) (("1" (inst - "r!1 / c!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (lemma "abs_mult" ("x" "c!1" "y" "l!1 - FF(i!1)")) (("1" (expand "abs" -1 2) (("1" (replace -1) (("1" (rewrite "div_mult_pos_lt2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) 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 2) (("2" (apply-extensionality :hide? t) (("2" (expand "o") (("2" (expand "*") (("2" (rewrite "isf_integral_scal") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (expand "*") (("1" (typepred "u!2(x1!1)") (("1" (expand "nn_isf?") (("1" (skosimp) (("1" (expand "*") (("1" (inst - "x!1") (("1" (assert) (("1" (case-replace "c!1=0") (("1" (assert) nil nil) ("2" (lemma "both_sides_times_pos_le1" ("pz" "c!1" "x" "0" "y" "u!2(x1!1)(x!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "u!2") (("2" (hide-all-but (-1 1)) (("2" (expand "*") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "*") (("2" (expand "increasing?") (("2" (skosimp) (("2" (inst - "x!2" "y!1") (("2" (assert) (("2" (case-replace "c!1=0") (("1" (assert) nil nil) ("2" (lemma "both_sides_times_pos_le1" ("pz" "c!1" "x" "u!2(x!2)(x!1)" "y" "u!2(y!1)(x!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -4)) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "u!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -4)) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "u!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nn_integrable_scal judgement-tcc nil nn_integral nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (sequence type-eq-decl nil sequences nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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_integrable_scal application-judgement "nn_integrable" nn_integral nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (member const-decl "bool" sets nil) (nn_convergence formula-decl nil nn_integral nil) (* const-decl "sequence[[T -> real]]" pointwise_convergence nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pointwise_convergence_scal formula-decl nil pointwise_convergence nil) (isf_integral_scal formula-decl nil isf nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs_mult formula-decl nil real_props nil) (c!1 skolem-const-decl "nnreal" nn_integral nil) (r!1 skolem-const-decl "posreal" nn_integral nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (abs_nat formula-decl nil abs_lems "reals/") (real_lt_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) (ball const-decl "set[T]" metric_space_def "metric_space/") (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (metric_convergence_def formula-decl nil metric_space "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[real]" convergence_aux "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" convergence_aux "metric_space/") (limit_def formula-decl nil hausdorff_convergence "topology/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (convergent? const-decl "bool" topological_convergence "topology/") (convergent type-eq-decl nil topological_convergence "topology/") (limit const-decl "T" topological_convergence "topology/") (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/") (O const-decl "T3" function_props nil) (isf_integral const-decl "real" isf nil) (isf_scal application-judgement "isf" nn_integral nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (increasing? const-decl "bool" real_fun_preds "reals/") (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (real_times_real_is_real application-judgement "real" reals nil) (empty? 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) (nn_integral const-decl "nnreal" nn_integral nil)) shostak)) (nn_integrable_prod 0 (nn_integrable_prod-1 nil 3395565025 ("" (skosimp) (("" (typepred "f!1") (("" (typepred "h!1") (("" (split) (("1" (skolem + ("x!1")) (("1" (expand "*") (("1" (typepred "f!1(x!1)") (("1" (expand "nn_bounded_measurable?") (("1" (flatten) (("1" (inst - "x!1") (("1" (lemma "le_times_le_pos" ("nnx" "0" "y" "f!1(x!1)" "nnz" "0" "w" "h!1(x!1)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nn_bounded_measurable?") (("2" (expand "bounded_measurable?") (("2" (flatten) (("2" (expand "bounded?") (("2" (skolem - ("M")) (("2" (case "M>0") (("1" (lemma "nn_integrable_scal" ("c" "M" "f" "f!1")) (("1" (flatten) (("1" (lemma "nn_integrable_le" ("g" "*[T](f!1, h!1)" "f" "*[T](M, f!1)")) (("1" (split -1) (("1" (flatten) nil nil) ("2" (skosimp) (("2" (expand "*") (("2" (inst -4 "x!1") (("2" (inst -6 "x!1") (("2" (typepred "f!1(x!1)") (("2" (expand "abs" -5) (("2" (assert) (("2" (lemma "le_times_le_pos" ("nnx" "0" "y" "f!1(x!1)" "nnz" "0" "w" "h!1(x!1)")) (("2" (assert) (("2" (case-replace "f!1(x!1)=0") (("1" (assert) nil nil) ("2" (lemma "both_sides_times_pos_le1" ("pz" "f!1(x!1)" "x" "h!1(x!1)" "y" "M")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "*[T](f!1, h!1)=lambda x: 0") (("1" (rewrite "nn_integrable_zero") nil nil) ("2" (apply-extensionality :hide? t) (("2" (expand "*") (("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) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil nn_integral 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 "[T -> real]" real_fun_ops "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_times_le_pos formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (bounded_measurable? const-decl "bool" measure_space nil) (bounded? const-decl "bool" sup_norm nil) (> const-decl "bool" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types 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) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (nn_integrable_le formula-decl nil nn_integral nil) (prod_measurable application-judgement "measurable_function[T, S]" nn_integral nil) (nn_integrable_scal application-judgement "nn_integrable" nn_integral nil) (nn_integrable_scal judgement-tcc nil nn_integral nil) (nn_integrable_zero formula-decl nil nn_integral 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" nn_integral nil) (nn_bounded_measurable? const-decl "bool" measure_space nil) (nn_bounded_measurable nonempty-type-eq-decl nil measure_space nil)) nil)) (nn_indefinite_integrable_TCC1 0 (nn_indefinite_integrable_TCC1-1 nil 3394683432 ("" (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 nn_integral nil) (set type-eq-decl nil sets 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" nn_integral nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (nn_integrable? const-decl "bool" nn_integral nil) (nn_integrable nonempty-type-eq-decl nil nn_integral 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) (convergence? const-decl "bool" topological_convergence "topology/") (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (m formal-const-decl "measure_type" nn_integral nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (measure? const-decl "bool" generalized_measure_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (mu const-decl "nnreal" measure_props nil) (image const-decl "set[R]" function_image nil) (empty? const-decl "bool" sets nil) (isf_integral const-decl "real" isf nil) (O const-decl "T3" function_props nil) (convergent? const-decl "bool" topological_convergence "topology/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (nn_indefinite_integrable 0 (nn_indefinite_integrable-1 nil 3395198128 ("" (skosimp) (("" (lemma "nn_integrable_prod" ("f" "f!1" "h" "phi(E!1)")) (("1" (flatten) (("1" (case-replace "*[T](f!1, phi(E!1))=phi(E!1) * f!1") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (expand "*") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "E!1") (("2" (expand "measurable_set?") (("2" (expand "nn_bounded_measurable?") (("2" (split) (("1" (rewrite "simple_is_bounded_measurable") (("1" (rewrite "phi_is_simple") nil nil)) nil) ("2" (skosimp) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (phi const-decl "nat" measure_space nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (set type-eq-decl nil sets nil) (nn_bounded_measurable nonempty-type-eq-decl nil measure_space nil) (nn_bounded_measurable? const-decl "bool" measure_space nil) (S formal-const-decl "sigma_algebra" nn_integral nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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 nn_integral nil) (nn_integrable_prod judgement-tcc nil nn_integral nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (simple nonempty-type-eq-decl nil measure_space nil) (simple? const-decl "bool" measure_space nil) (simple_is_bounded_measurable judgement-tcc nil measure_space nil) (phi_is_simple judgement-tcc nil measure_space nil)) shostak)) (nn_0_le 0 (nn_0_le-1 nil 3395147240 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (nn_integral_def 0 (nn_integral_def-1 nil 3452235344 ("" (skosimp) (("" (typepred "f!1") (("" (name "U" "choose({u | pointwise_convergence?(u,f!1)})") (("1" (expand "nn_integral" 1) (("1" (replace -1) (("1" (inst + "U") (("1" (split) (("1" (lemma "choose_member" ("a" "{u | pointwise_convergence?(u, f!1)}")) (("1" (replace -2) (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (rewrite "topological_convergence.limit_lemma") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nn_integrable?") (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "u!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nn_integrable nonempty-type-eq-decl nil nn_integral nil) (nn_integrable? const-decl "bool" nn_integral nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (T formal-type-decl nil nn_integral nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (empty? const-decl "bool" sets nil) (nn_integral const-decl "nnreal" nn_integral 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) (isf_integral const-decl "real" isf nil) (O const-decl "T3" function_props nil) (convergent type-eq-decl nil topological_convergence "topology/") (convergent? const-decl "bool" topological_convergence "topology/") (limit_lemma formula-decl nil topological_convergence "topology/") (choose_member formula-decl nil sets_lemmas nil) (member const-decl "bool" 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) (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" nn_integral nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" nn_integral nil) (isf? const-decl "bool" isf nil) (isf nonempty-type-eq-decl nil isf nil) (nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (sequence type-eq-decl nil sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil)) shostak)))
¤ Dauer der Verarbeitung: 0.797 Sekunden (vorverarbeitet am 2026-05-06) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26