|
(integral
(integrable_TCC1 0
(integrable_TCC1-1 nil 3390735612
("" (expand "integrable?")
(("" (lemma "nn_integrable_zero")
(("" (inst + "lambda x: 0" "lambda x: 0")
(("" (apply-extensionality 1 :hide? t)
(("" (expand "-") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((m formal-const-decl "measure_type" 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)
(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)
(S formal-const-decl "sigma_algebra" 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)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil integral nil)
(nn_integrable_zero formula-decl nil nn_integral nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(integrable? const-decl "bool" integral nil))
nil))
(nn_integrable_is_integrable 0
(nn_integrable_is_integrable-1 nil 3391020617
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "integrable?")
(("" (inst + "x!1" "lambda x: 0")
(("1" (apply-extensionality :hide? t)
(("1" (expand "-") (("1" (propax) nil nil)) nil)
("2" (skosimp)
(("2" (expand "-") (("2" (assert) nil nil)) nil)) nil))
nil)
("2" (rewrite "nn_integrable_zero") nil nil))
nil))
nil))
nil))
nil)
((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(m formal-const-decl "measure_type" 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" 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)
(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 integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x!1 skolem-const-decl "nn_integrable" integral nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(nn_integrable_zero formula-decl nil nn_integral nil)
(integrable? const-decl "bool" integral nil))
nil))
(isf_is_integrable 0
(isf_is_integrable-1 nil 3391430136
("" (skosimp)
(("" (expand "integrable?")
(("" (inst + "plus(x!1)" "minus(x!1)")
(("1" (lemma "plus_minus_def" ("f" "x!1"))
(("1" (propax) nil nil)) nil)
("2" (lemma "isf_minus" ("i" "x!1"))
(("2" (assert)
(("2" (lemma "nn_isf_is_nn_integrable")
(("2" (inst - "minus[T](x!1)")
(("1" (flatten) nil nil)
("2" (expand "nn_isf?")
(("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (lemma "isf_plus" ("i" "x!1"))
(("3" (assert)
(("3" (lemma "nn_isf_is_nn_integrable")
(("3" (inst - "plus[T](x!1)")
(("1" (flatten) nil nil)
("2" (hide 2)
(("2" (expand "nn_isf?")
(("2" (hide -1) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable? const-decl "bool" integral nil)
(isf_plus judgement-tcc nil isf nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(isf_minus judgement-tcc nil isf nil)
(nn_isf_is_nn_integrable judgement-tcc nil nn_integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nn_isf nonempty-type-eq-decl nil nn_integral nil)
(nn_isf? const-decl "bool" nn_integral nil)
(plus_minus_def formula-decl nil real_fun_ops_aux "reals/")
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(minus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(T formal-type-decl nil 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types 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" 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" integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(plus const-decl "[T -> nnreal]" real_fun_ops_aux "reals/")
(isf? const-decl "bool" isf nil)
(isf nonempty-type-eq-decl nil isf nil)
(x!1 skolem-const-decl "isf" integral nil)
(isf_plus application-judgement "isf" integral nil)
(isf_minus application-judgement "isf[T, S, m]" integral nil))
nil))
(integrable_is_measurable 0
(integrable_is_measurable-1 nil 3395201756
("" (skosimp)
(("" (lemma "nn_integrable_is_measurable")
(("" (typepred "x!1")
(("" (expand "integrable?")
(("" (skosimp)
(("" (replace -1)
(("" (inst-cp - "g!1")
(("" (inst - "h!1")
(("" (rewrite "diff_measurable") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((m formal-const-decl "measure_type" 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)
(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)
(S formal-const-decl "sigma_algebra" 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)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil integral nil)
(nn_integrable_is_measurable judgement-tcc nil nn_integral nil)
(diff_measurable judgement-tcc nil measure_space_def nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(integrable_equiv 0
(integrable_equiv-1 nil 3395200583
("" (skosimp)
(("" (lemma "nn_integral_add" ("f1" "g1!1" "f2" "g4!1"))
(("" (lemma "nn_integral_add" ("f1" "g2!1" "f2" "g3!1"))
(("" (case-replace "g2!1 + g3!1=g1!1 + g4!1")
(("1" (assert) nil nil)
("2" (apply-extensionality 1 :hide? t)
(("2"
(lemma "extensionality_postulate"
("f" "g1!1 - g3!1" "g" "g2!1 - g4!1"))
(("2" (replace -1 -4 rl)
(("2" (inst -4 "x!1")
(("2" (hide-all-but (-4 1)) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((m formal-const-decl "measure_type" 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)
(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)
(S formal-const-decl "sigma_algebra" 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)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(nn_integral_add formula-decl nil nn_integral nil)
(nn_integrable_add application-judgement "nn_integrable" integral
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(diff_measurable application-judgement "measurable_function[T, S]"
integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(extensionality_postulate formula-decl nil functions nil)
(- const-decl "[T -> real]" real_fun_ops "reals/"))
shostak))
(integrable_add 0
(integrable_add-1 nil 3391020617
("" (skosimp)
(("" (typepred "f1!1")
(("" (typepred "f2!1")
(("" (expand "integrable?")
(("" (skosimp*)
(("" (inst + "g!1+g!2" "h!1+h!2")
(("" (apply-extensionality 1 :hide? t)
(("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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 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 application-judgement "nn_integrable" integral
nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types 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" 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" integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(diff_measurable application-judgement "measurable_function[T, S]"
integral nil)
(sum_measurable application-judgement "measurable_function[T, S]"
integral nil)
(- const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(integrable_scal 0
(integrable_scal-1 nil 3391020617
("" (skosimp)
(("" (typepred "f!1")
(("" (expand "integrable?")
(("" (skosimp)
(("" (case "c!1>=0")
(("1" (inst + "c!1*g!1" "c!1*h!1")
(("1" (apply-extensionality :hide? t)
(("1" (grind) nil nil)) nil)
("2" (split)
(("1" (skosimp)
(("1" (expand "*")
(("1"
(lemma "le_times_le_pos"
("nnx" "0" "y" "c!1" "nnz" "0" "w" "h!1(x1!1)"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (typepred "h!1")
(("2"
(lemma "nn_integrable_scal" ("c" "c!1" "f" "h!1"))
(("1" (flatten) nil nil) ("2" (propax) nil nil))
nil))
nil))
nil)
("3" (split)
(("1" (skosimp)
(("1"
(lemma "nn_integrable_scal" ("c" "c!1" "f" "g!1"))
(("1" (flatten) (("1" (inst - "x1!1") nil nil))
nil)
("2" (propax) nil nil))
nil))
nil)
("2"
(lemma "nn_integrable_scal" ("c" "c!1" "f" "g!1"))
(("1" (flatten) nil nil) ("2" (propax) nil nil))
nil))
nil))
nil)
("2" (inst + "-c!1*h!1" "-c!1*g!1")
(("1" (replace -1)
(("1" (hide-all-but 2)
(("1" (apply-extensionality :hide? t)
(("1" (grind) nil nil)) nil))
nil))
nil)
("2" (split)
(("1" (hide -1)
(("1" (skosimp)
(("1" (grind)
(("1"
(lemma "both_sides_times_pos_le1"
("pz" "-c!1" "x" "0" "y" "g!1(x1!1)"))
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2"
(lemma "nn_integrable_scal" ("c" "-c!1" "f" "g!1"))
(("1" (flatten) nil nil) ("2" (assert) nil nil))
nil))
nil)
("3" (split)
(("1" (skosimp)
(("1"
(lemma "both_sides_times_pos_le1"
("pz" "-c!1" "x" "0" "y" "h!1(x1!1)"))
(("1" (assert) (("1" (grind) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil)
("2"
(lemma "nn_integrable_scal" ("c" "-c!1" "f" "h!1"))
(("1" (flatten) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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 integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(scal_measurable application-judgement "measurable_function[T, S]"
integral nil)
(g!1 skolem-const-decl "nn_integrable" integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(m formal-const-decl "measure_type" 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" 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)
(nnreal type-eq-decl nil real_types nil)
(c!1 skolem-const-decl "real" integral nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(h!1 skolem-const-decl "nn_integrable" integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(diff_measurable application-judgement "measurable_function[T, S]"
integral nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(nn_integrable_scal judgement-tcc nil nn_integral nil)
(le_times_le_pos formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(>= const-decl "bool" reals nil))
nil))
(integrable_opp 0
(integrable_opp-1 nil 3391020617
("" (skosimp)
(("" (typepred "f!1")
(("" (lemma "integrable_scal" ("c" "-1" "f" "f!1"))
(("" (expand "*")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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 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_times_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(integrable_scal judgement-tcc nil integral nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil))
nil))
(integrable_diff 0
(integrable_diff-1 nil 3391142033
("" (skosimp)
(("" (lemma "integrable_opp" ("f" "f2!1"))
(("" (lemma "integrable_add" ("f1" "f1!1" "f2" "-f2!1"))
(("" (case-replace "(+[T])(f1!1, -f2!1)=(-[T])(f1!1, f2!1)")
(("" (apply-extensionality 1 :hide? t)
(("" (expand "+")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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 integral nil)
(integrable_opp judgement-tcc nil integral nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(diff_measurable application-judgement "measurable_function[T, S]"
integral nil)
(integrable_add application-judgement "integrable" integral nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(integrable_opp application-judgement "integrable" integral nil)
(integrable_add judgement-tcc nil integral nil)
(- const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(integrable_zero 0
(integrable_zero-1 nil 3391332663
("" (rewrite "integrable_TCC1") nil nil)
((integrable_TCC1 subtype-tcc nil integral nil)) shostak))
(nonempty_integrals 0
(nonempty_integrals-1 nil 3391183431
("" (skosimp)
(("" (typepred "f!1")
(("" (expand "integrable?")
(("" (skosimp)
(("" (expand "integrals")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (inst - "nn_integral(g!1)-nn_integral(h!1)")
(("" (inst + "g!1" "h!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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 integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(nn_integral const-decl "nnreal" nn_integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(m formal-const-decl "measure_type" 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" 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)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(empty? const-decl "bool" sets nil)
(integrals const-decl "set[real]" integral nil))
shostak))
(singleton_integrals 0
(singleton_integrals-1 nil 3391183368
("" (skosimp)
(("" (lemma "nonempty_integrals" ("f" "f!1"))
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (skosimp)
(("" (expand "singleton?")
(("" (inst + "x!1")
(("1" (skosimp)
(("1" (typepred "y!1")
(("1" (expand "member")
(("1" (expand "integrals")
(("1" (skosimp*)
(("1" (replace -2)
(("1" (replace -4)
(("1"
(hide -2 -4)
(("1"
(lemma
"nn_integrable_add"
("f1" "g!2" "f2" "h!1"))
(("1"
(lemma
"nn_integrable_add"
("f1" "g!1" "f2" "h!2"))
(("1"
(flatten)
(("1"
(lemma
"nn_integral_add"
("f1" "g!2" "f2" "h!1"))
(("1"
(lemma
"nn_integral_add"
("f1" "g!1" "f2" "h!2"))
(("1"
(assert)
(("1"
(case-replace
"g!1 + h!2=g!2 + h!1")
(("1" (assert) nil nil)
("2"
(apply-extensionality
1
:hide?
t)
(("2"
(hide-all-but
(-7 -8 1))
(("2"
(lemma
"extensionality_postulate"
("f"
"f!1"
"g"
"g!1-h!1"))
(("2"
(lemma
"extensionality_postulate"
("f"
"f!1"
"g"
"g!2-h!2"))
(("2"
(flatten)
(("2"
(split -2)
(("1"
(split -4)
(("1"
(hide
-3
-4
-5
-6)
(("1"
(inst
-
"x!2")
(("1"
(inst
-
"x!2")
(("1"
(expand
"+")
(("1"
(assert)
(("1"
(expand
"-")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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 integral nil)
(nonempty_integrals formula-decl nil integral nil)
(empty? const-decl "bool" sets nil)
(singleton? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(m formal-const-decl "measure_type" 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" 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)
(nn_integrable_add judgement-tcc nil nn_integral nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(extensionality_postulate formula-decl nil functions nil)
(integrable_add application-judgement "integrable" integral nil)
(nn_integrable_add application-judgement "nn_integrable" integral
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(integrable_diff application-judgement "integrable" integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nn_integral_add formula-decl nil nn_integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(integrals const-decl "set[real]" integral nil)
(f!1 skolem-const-decl "integrable" integral nil)
(x!1 skolem-const-decl "real" integral nil)
(nonempty? const-decl "bool" sets nil))
shostak))
(integral_TCC1 0
(integral_TCC1-1 nil 3391183280
("" (skosimp)
(("" (lemma "nonempty_integrals" ("f" "f!1"))
(("" (propax) nil nil)) nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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 integral nil)
(nonempty_integrals formula-decl nil integral nil))
nil))
(nn_integrable_is_nn_integrable 0
(nn_integrable_is_nn_integrable-1 nil 3391225798
("" (skosimp)
(("" (typepred "f!1")
(("" (expand "integrable?")
(("" (skosimp)
(("" (typepred "g!1")
(("" (typepred "h!1")
(("" (lemma "nn_integrable_le" ("f" "g!1" "g" "f!1"))
(("" (split -1)
(("1" (flatten) nil nil)
("2" (skosimp)
(("2" (replace -3)
(("2" (expand "-")
(("2" (inst - "x!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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 integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nn_integrable_le formula-decl nil nn_integral nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types 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" 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" integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil))
shostak))
(integral_nn 0
(integral_nn-1 nil 3391166946
("" (skosimp)
(("" (typepred "g!1")
(("" (name "CC" "integral(g!1)")
(("" (replace -1)
(("" (expand "integral")
(("" (typepred "choose[real](integrals(g!1))")
(("" (replace -2)
(("" (expand "integrals" -1)
(("" (skosimp)
((""
(lemma "nn_integral_add" ("f1" "g!1" "f2" "h!1"))
(("" (replace -3)
(("" (case "g!2=g!1+h!1")
(("1" (assert) nil nil)
("2" (hide-all-but (-2 1))
(("2" (apply-extensionality :hide? t)
(("2"
(replace -1)
(("2"
(hide -1)
(("2" (grind) 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)
(m formal-const-decl "measure_type" 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" 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)
(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 integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(integrals const-decl "set[real]" integral nil)
(set type-eq-decl nil sets nil)
(nn_integral_add formula-decl nil nn_integral nil)
(integrable_add application-judgement "integrable" integral nil)
(nn_integrable_add application-judgement "nn_integrable" integral
nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(integrable_diff application-judgement "integrable" integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integral const-decl "real" integral nil))
shostak))
(integral_zero 0
(integral_zero-1 nil 3391167424
("" (lemma "integrable_zero")
(("" (lemma "nn_integrable_is_nn_integrable" ("f" "LAMBDA x: 0"))
(("1" (split -1)
(("1" (lemma "integral_nn" ("g" "LAMBDA x: 0"))
(("1" (replace -1)
(("1" (hide -1 -3)
(("1" (rewrite "nn_integral_zero") nil nil)) nil))
nil)
("2" (propax) nil nil))
nil)
("2" (skosimp) (("2" (assert) nil nil)) nil))
nil)
("2" (propax) nil nil))
nil))
nil)
((integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral 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 integral nil)
(nn_integrable_is_nn_integrable formula-decl nil integral nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(m formal-const-decl "measure_type" 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" 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)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(integral_nn formula-decl nil integral nil)
(nn_integral_zero formula-decl nil nn_integral nil)
(integrable_zero formula-decl nil integral nil))
shostak))
(integral_phi_TCC1 0
(integral_phi_TCC1-1 nil 3391167398
("" (skosimp)
(("" (typepred "F!1")
(("" (assert)
(("" (expand "measurable_set?") (("" (propax) nil nil)) nil))
nil))
nil))
nil)
((mu_fin? const-decl "bool" measure_props nil)
(m formal-const-decl "measure_type" 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)
(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)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" 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)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil integral nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(integral_phi 0
(integral_phi-1 nil 3391181089
("" (skosimp)
(("" (lemma "nn_integral_phi" ("F" "F!1"))
(("" (rewrite "integral_nn") nil nil)) nil))
nil)
((m formal-const-decl "measure_type" 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)
(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)
(S formal-const-decl "sigma_algebra" 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)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil integral 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)
(set type-eq-decl nil sets nil)
(nn_integral_phi formula-decl nil nn_integral 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)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(integral_nn formula-decl nil integral nil)
(isf_phi application-judgement "isf" integral nil))
shostak))
(integral_add 0
(integral_add-1 nil 3390735896
("" (skosimp)
(("" (expand "integral")
(("" (typepred "choose[real](integrals(f1!1 + f2!1))")
(("" (typepred "choose[real](integrals(f2!1))")
(("" (typepred "choose[real](integrals(f1!1))")
((""
(name-replace "XY"
"choose[real](integrals(f1!1 + f2!1))")
(("" (name-replace "X" "choose[real](integrals(f1!1))")
(("" (name-replace "Y" "choose[real](integrals(f2!1))")
(("" (expand "integrals")
(("" (skosimp*)
(("" (replace -2)
(("" (replace -4)
(("" (replace -6)
(("" (hide -2 -4 -6)
((""
(replace -1)
((""
(replace -2)
((""
(hide -1 -2)
((""
(lemma
"nn_integral_add"
("f1" "g!1" "f2" "g!2"))
((""
(lemma
"nn_integral_add"
("f1" "h!1" "f2" "h!2"))
((""
(case
"(g!1+g!2)+h!3=(h!1+h!2)+g!3")
(("1"
(lemma
"nn_integral_add"
("f1"
"g!1 + g!2"
"f2"
"h!3"))
(("1"
(lemma
"nn_integral_add"
("f1"
"h!1 + h!2"
"f2"
"g!3"))
(("1" (assert) nil nil))
nil))
nil)
("2"
(lemma
"extensionality_postulate"
("f"
"g!1 - h!1 + (g!2 - h!2)"
"g"
"g!3 - h!3"))
(("2"
(flatten)
(("2"
(split -2)
(("1"
(hide-all-but (-1 1))
(("1"
(apply-extensionality
:hide?
t)
(("1"
(inst - "x!1")
(("1"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integral const-decl "real" integral nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(m formal-const-decl "measure_type" 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" 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)
(nn_integral_add formula-decl nil nn_integral nil)
(nn_integrable_add application-judgement "nn_integrable" integral
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(integrable_diff application-judgement "integrable" integral nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(extensionality_postulate formula-decl nil functions nil)
(integrable_add application-judgement "integrable" integral 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 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)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(set type-eq-decl nil sets nil)
(integrals const-decl "set[real]" integral nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil))
shostak))
(integral_scal 0
(integral_scal-1 nil 3390736302
("" (skosimp)
(("" (expand "integral")
(("" (typepred "choose[real](integrals(f!1))")
(("" (typepred "choose[real](integrals(c!1*f!1))")
(("" (name-replace "X" "choose[real](integrals(f!1))")
(("" (name-replace "CX" "choose[real](integrals(c!1*f!1))")
(("" (expand "integrals")
(("" (skosimp*)
(("" (replace -3)
(("" (replace -2)
(("" (replace -4)
(("" (hide-all-but (-1 1))
(("" (case "c!1*g!2+h!1 = c!1*h!2+g!1")
(("1" (hide -2)
(("1"
(case "c!1>=0")
(("1"
(lemma
"nn_integral_scal"
("c" "c!1" "f" "g!2"))
(("1"
(lemma
"nn_integral_scal"
("c" "c!1" "f" "h!2"))
(("1"
(lemma
"nn_integral_add"
("f1" "c!1 * g!2" "f2" "h!1"))
(("1"
(lemma
"nn_integral_add"
("f1" "c!1 * h!2" "f2" "g!1"))
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2"
(case "-c!1*h!2+h!1=-c!1*g!2+g!1")
(("1"
(hide -2)
(("1"
(lemma
"nn_integral_scal"
("c" "-c!1" "f" "h!2"))
(("1"
(lemma
"nn_integral_scal"
("c" "-c!1" "f" "g!2"))
(("1"
(lemma
"nn_integral_add"
("f1"
"-c!1 * g!2"
"f2"
"g!1"))
(("1"
(lemma
"nn_integral_add"
("f1"
"-c!1 * h!2"
"f2"
"h!1"))
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2"
(lemma
"extensionality_postulate"
("f"
"c!1 * g!2 + h!1"
"g"
"c!1 * h!2 + g!1"))
(("2"
(flatten)
(("2"
(split -2)
(("1"
(hide-all-but (-1 1))
(("1"
(apply-extensionality
:hide?
t)
(("1"
(inst - "x!1")
(("1" (grind) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "extensionality_postulate"
("f"
"c!1 * (g!2 - h!2)"
"g"
"g!1 - h!1"))
(("2"
(flatten)
(("2"
(split -2)
(("1"
(hide-all-but (1 -1))
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(inst - "x!1")
(("1" (grind) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integral const-decl "real" integral nil)
(integrable_scal application-judgement "integrable" integral nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(integrable_diff application-judgement "integrable" integral nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(extensionality_postulate formula-decl nil functions nil)
(nn_integral_scal formula-decl nil nn_integral nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nn_integral_add formula-decl nil nn_integral nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(integrable_add application-judgement "integrable" integral nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types 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" 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" integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(= const-decl "[T, T -> boolean]" equalities 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 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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.106 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
