|
(product_integral_def
(mu_TCC1 0
(mu_TCC1-1 nil 3458545281
("" (typepred "S1")
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra_empty?")
(("" (flatten)
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T1 formal-type-decl nil product_integral_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def
nil))
nil))
(nu_TCC1 0
(nu_TCC1-1 nil 3458545281
("" (typepred "S2")
(("" (expand "sigma_algebra?")
(("" (flatten)
(("" (expand "subset_algebra_empty?")
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(member const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T2 formal-type-decl nil product_integral_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def
nil))
nil))
(integrable1_TCC1 0
(integrable1_TCC1-1 nil 3431150732
("" (expand "integrable1?")
(("" (inst + "emptyset[T1]" "lambda x: 0")
(("1" (skosimp)
(("1" (hide 1)
(("1" (rewrite "integrable_zero")
(("1" (rewrite "integral_zero") nil nil)) nil))
nil))
nil)
("2" (rewrite "integrable_zero") nil nil))
nil))
nil)
((null_emptyset name-judgement "null_set" product_integral_def nil)
(subset_algebra_emptyset name-judgement "(S)" product_integral_def
nil)
(finite_emptyset name-judgement "finite_set[T]" sigma_countable
"sigma_set/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(integrable? const-decl "bool" integral nil)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
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)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def 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)
(T1 formal-type-decl nil product_integral_def nil)
(set type-eq-decl nil sets nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(emptyset const-decl "set" sets nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integral_zero formula-decl nil integral nil)
(integrable_zero formula-decl nil integral nil)
(T2 formal-type-decl nil product_integral_def nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def nil)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
nil)
(integrable1? const-decl "bool" product_integral_def nil))
nil))
(integrable2_TCC1 0
(integrable2_TCC1-1 nil 3431150732
("" (expand "integrable2?")
(("" (inst + "emptyset[T2]" "lambda y: 0")
(("1" (skosimp)
(("1" (hide 1)
(("1" (rewrite "integrable_zero")
(("1" (rewrite "integral_zero") nil nil)) nil))
nil))
nil)
("2" (rewrite "integrable_zero") nil nil))
nil))
nil)
((null_emptyset name-judgement "null_set" product_integral_def nil)
(subset_algebra_emptyset name-judgement "(S)" product_integral_def
nil)
(finite_emptyset name-judgement "finite_set[T]" sigma_countable
"sigma_set/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(integrable? const-decl "bool" integral nil)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
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)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def 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)
(T2 formal-type-decl nil product_integral_def nil)
(set type-eq-decl nil sets nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(emptyset const-decl "set" sets nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integral_zero formula-decl nil integral nil)
(integrable_zero formula-decl nil integral nil)
(T1 formal-type-decl nil product_integral_def nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def nil)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
nil)
(integrable2? const-decl "bool" product_integral_def nil))
nil))
(integrable1_zero 0
(integrable1_zero-1 nil 3458969271
("" (lemma "integrable1_TCC1") (("" (propax) nil nil)) nil)
((integrable1_TCC1 subtype-tcc nil product_integral_def nil))
shostak))
(integrable1_add 0
(integrable1_add-1 nil 3458969501
("" (skosimp)
(("" (typepred "h1!1")
(("" (typepred "g1!1")
(("" (expand "integrable1?")
(("" (skosimp*)
(("" (expand "member")
(("" (inst + "union(N1!1,N1!2)" "f!1+f!2")
(("" (skosimp)
(("" (inst - "x!1")
(("" (inst - "x!1")
(("" (expand "union")
(("" (expand "member")
(("" (flatten)
(("" (assert)
((""
(flatten)
((""
(expand "+" 3)
((""
(lemma
"integrable_add"
("f1"
"LAMBDA y: g1!1(x!1, y)"
"f2"
"LAMBDA y: h1!1(x!1, y)"))
(("1"
(expand "+" -1)
(("1"
(assert)
(("1"
(lemma
"integral_add"
("f1"
"LAMBDA y: g1!1(x!1, y)"
"f2"
"LAMBDA y: h1!1(x!1, y)"))
(("1"
(expand "+")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(integrable1? const-decl "bool" product_integral_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(integral_add formula-decl nil integral nil)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def nil)
(integrable_add judgement-tcc nil integral nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(union const-decl "set" sets nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
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)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def 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)
(measurable_union application-judgement "measurable_set[T1, S1]"
product_integral_def nil)
(negligible_union application-judgement "negligible"
product_integral_def nil)
(null_union application-judgement "null_set[T1, S1, mu]"
product_integral_def nil)
(sum_measurable application-judgement "measurable_function[T, S]"
product_integral_def nil)
(integrable_add application-judgement "integrable"
product_integral_def nil))
nil))
(integrable1_scal 0
(integrable1_scal-1 nil 3458969296
("" (skosimp)
(("" (typepred "h1!1")
(("" (expand "integrable1?")
(("" (skosimp)
(("" (inst + "N1!1" "c!1*f!1")
(("" (skosimp)
(("" (inst - "x!1")
(("" (assert)
(("" (flatten)
(("" (hide 1)
((""
(lemma "integrable_scal"
("c" "c!1" "f" "LAMBDA y: h1!1(x!1, y)"))
(("1"
(lemma "integral_scal"
("c" "c!1" "f" "LAMBDA y: h1!1(x!1, y)"))
(("1" (expand "*") (("1" (assert) nil nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(integrable1? const-decl "bool" product_integral_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(integral_scal formula-decl nil integral nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def nil)
(integrable_scal judgement-tcc nil integral nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
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)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def 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)
(scal_measurable application-judgement "measurable_function[T, S]"
product_integral_def nil)
(integrable_scal application-judgement "integrable"
product_integral_def nil))
shostak))
(integrable1_opp 0
(integrable1_opp-1 nil 3458969501
("" (skosimp)
(("" (lemma "integrable1_scal" ("h1" "h1!1" "c" "-1"))
(("" (expand "*")
(("" (expand "-")
((""
(case-replace
"(LAMBDA (x: [T1, T2]): -1 * h1!1(x))=(LAMBDA (x: [T1, T2]): -h1!1(x))")
(("" (apply-extensionality :hide? t) nil nil)) nil))
nil))
nil))
nil))
nil)
((integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(integrable1? const-decl "bool" product_integral_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(integrable1_scal judgement-tcc nil product_integral_def nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(integrable1_diff 0
(integrable1_diff-1 nil 3458969501
("" (skosimp)
(("" (lemma "integrable1_opp" ("h1" "h1!1"))
(("" (lemma "integrable1_add" ("g1" "g1!1" "h1" "-h1!1"))
((""
(case-replace
"((+[[T1, T2]])(g1!1, -h1!1))=((-[[T1, T2]])(g1!1, h1!1))")
(("" (apply-extensionality :hide? t)
(("" (expand "+")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(integrable1? const-decl "bool" product_integral_def 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)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(integrable1_opp judgement-tcc nil product_integral_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(integrable1_add application-judgement "integrable1"
product_integral_def 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)
(integrable1_opp application-judgement "integrable1"
product_integral_def nil)
(integrable1_add judgement-tcc nil product_integral_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(integrable2_zero 0
(integrable2_zero-1 nil 3458970055
("" (rewrite "integrable2_TCC1") nil nil)
((integrable2_TCC1 subtype-tcc nil product_integral_def nil))
shostak))
(integrable2_add 0
(integrable2_add-1 nil 3458970054
("" (skosimp)
(("" (typepred "h2!1")
(("" (typepred "g2!1")
(("" (expand "integrable2?")
(("" (skosimp*)
(("" (inst + "union(N2!1,N2!2)" "g!1+g!2")
(("" (skosimp)
(("" (inst - "y!1")
(("" (inst - "y!1")
(("" (expand "union")
(("" (assert)
(("" (flatten)
(("" (assert)
(("" (flatten)
((""
(expand "+")
((""
(lemma
"integrable_add"
("f1"
"LAMBDA x: g2!1(x, y!1)"
"f2"
"LAMBDA x: h2!1(x, y!1)"))
(("1"
(lemma
"integral_add"
("f1"
"LAMBDA x: g2!1(x, y!1)"
"f2"
"LAMBDA x: h2!1(x, y!1)"))
(("1"
(expand "+")
(("1" (assert) nil nil))
nil))
nil)
("2" (propax) nil nil)
("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable2 nonempty-type-eq-decl nil product_integral_def nil)
(integrable2? const-decl "bool" product_integral_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(integrable_add application-judgement "integrable"
product_integral_def nil)
(sum_measurable application-judgement "measurable_function[T, S]"
product_integral_def nil)
(null_union application-judgement "null_set[T2, S2, nu]"
product_integral_def nil)
(negligible_union application-judgement "negligible"
product_integral_def nil)
(measurable_union application-judgement "measurable_set[T2, S2]"
product_integral_def 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)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def 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)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(union const-decl "set" sets nil)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(integrable_add judgement-tcc nil integral nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def nil)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
nil)
(integral_add formula-decl nil integral nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil))
nil))
(integrable2_scal 0
(integrable2_scal-1 nil 3458970054
("" (skosimp)
(("" (typepred "h2!1")
(("" (expand "integrable2?")
(("" (skosimp)
(("" (inst + "N2!1" "c!1*g!1")
(("" (skosimp)
(("" (inst - "y!1")
(("" (assert)
(("" (flatten)
((""
(lemma "integrable_scal"
("c" "c!1" "f" "LAMBDA x: h2!1(x, y!1)"))
(("1"
(lemma "integral_scal"
("c" "c!1" "f" "LAMBDA x: h2!1(x, y!1)"))
(("1" (expand "*") (("1" (assert) nil nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable2 nonempty-type-eq-decl nil product_integral_def nil)
(integrable2? const-decl "bool" product_integral_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(integrable_scal judgement-tcc nil integral nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def nil)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(integral_scal formula-decl nil integral nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
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)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def 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)
(scal_measurable application-judgement "measurable_function[T, S]"
product_integral_def nil)
(integrable_scal application-judgement "integrable"
product_integral_def nil))
nil))
(integrable2_opp 0
(integrable2_opp-1 nil 3458970054
("" (skosimp)
(("" (lemma "integrable2_scal" ("h2" "h2!1" "c" "-1"))
(("" (expand "*")
(("" (expand "-")
((""
(case-replace
"(LAMBDA (x: [T1, T2]): -1 * h2!1(x))=(LAMBDA (x: [T1, T2]): -h2!1(x))")
(("" (apply-extensionality :hide? t) nil nil)) nil))
nil))
nil))
nil))
nil)
((integrable2 nonempty-type-eq-decl nil product_integral_def nil)
(integrable2? const-decl "bool" product_integral_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(integrable2_scal judgement-tcc nil product_integral_def nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(integrable2_diff 0
(integrable2_diff-1 nil 3458970054
("" (skosimp)
(("" (lemma "integrable2_opp" ("h2" "h2!1"))
(("" (lemma "integrable2_add" ("g2" "g2!1" "h2" "-h2!1"))
((""
(case-replace
"((+[[T1, T2]])(g2!1, -h2!1))=((-[[T1, T2]])(g2!1, h2!1))")
(("" (apply-extensionality :hide? t)
(("" (expand "+")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((integrable2 nonempty-type-eq-decl nil product_integral_def nil)
(integrable2? const-decl "bool" product_integral_def 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)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(integrable2_opp judgement-tcc nil product_integral_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(integrable2_add application-judgement "integrable2"
product_integral_def 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)
(integrable2_opp application-judgement "integrable2"
product_integral_def nil)
(integrable2_add judgement-tcc nil product_integral_def nil)
(- const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(null_integrable1_TCC1 0
(null_integrable1_TCC1-1 nil 3458969029
("" (skosimp)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (typepred "h1!1")
(("" (expand "integrable1?")
(("" (skosimp)
(("" (expand "member")
(("" (inst -2 "(N1!1,f!1)") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(integrable1? const-decl "bool" product_integral_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(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)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def 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)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil))
nil))
(null_integrable2_TCC1 0
(null_integrable2_TCC1-1 nil 3458969029
("" (skosimp)
(("" (typepred "h2!1")
(("" (expand "integrable2?")
(("" (skosimp)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (inst -2 "(N2!1,g!1)")
(("" (expand "member") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable2 nonempty-type-eq-decl nil product_integral_def nil)
(integrable2? const-decl "bool" product_integral_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def 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)
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
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)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def 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)
(nonempty? const-decl "bool" sets nil))
nil))
(null_integral1_def 0
(null_integral1_def-1 nil 3458973205
("" (skosimp)
(("" (expand "null_integrable1")
((""
(case "nonempty?({(N1,f) |
FORALL x:
NOT member(x, N1) =>
integrable?(LAMBDA y: h1!1(x, y)) AND
integral(LAMBDA y: h1!1(x, y)) = f(x)})")
(("1"
(lemma "choose_member"
("a" "{(N1,f) |
FORALL x:
NOT member(x, N1) =>
integrable?(LAMBDA y: h1!1(x, y)) AND
integral(LAMBDA y: h1!1(x, y)) = f(x)}"))
(("1" (expand "nonempty?")
(("1" (assert)
(("1" (replace -2 -1 rl)
(("1" (hide -2 1)
(("1" (inst - "x!1") (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (typepred "h1!1")
(("2" (expand "nonempty?")
(("2" (expand "integrable1?")
(("2" (skosimp)
(("2" (expand "empty?")
(("2" (inst -2 "(N1!2,f!2)")
(("2" (expand "member") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((null_integrable1 const-decl
"[null_set[T1, S1, mu], integrable[T1, S1, mu]]"
product_integral_def nil)
(empty? const-decl "bool" sets nil)
(choose_member formula-decl nil sets_lemmas nil)
(T1 formal-type-decl nil product_integral_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans 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)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_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)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(nonempty? const-decl "bool" sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T2 formal-type-decl nil product_integral_def nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def nil)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
nil)
(integrable1? const-decl "bool" product_integral_def nil)
(integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(integral const-decl "real" integral nil))
shostak))
(null_integral2_def 0
(null_integral2_def-1 nil 3458973437
("" (skosimp)
(("" (expand "null_integrable2")
((""
(case "nonempty?({(N2,g) |
FORALL y:
NOT member(y, N2) =>
integrable?(LAMBDA x: h2!1(x, y)) AND
integral(LAMBDA x: h2!1(x, y)) = g(y)})")
(("1"
(lemma "choose_member"
("a" "{(N2,g) |
FORALL y:
NOT member(y, N2) =>
integrable?(LAMBDA x: h2!1(x, y)) AND
integral(LAMBDA x: h2!1(x, y)) = g(y)}"))
(("1" (expand "nonempty?")
(("1" (assert)
(("1" (replace -2 * rl)
(("1" (inst - "y!1") (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (typepred "h2!1")
(("2" (expand "integrable2?")
(("2" (skosimp)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (inst -2 "(N2!2,g!2)")
(("2" (expand "member") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((null_integrable2 const-decl
"[null_set[T2, S2, nu], integrable[T2, S2, nu]]"
product_integral_def nil)
(empty? const-decl "bool" sets nil)
(choose_member formula-decl nil sets_lemmas nil)
(T2 formal-type-decl nil product_integral_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans 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)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_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)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(nonempty? const-decl "bool" sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T1 formal-type-decl nil product_integral_def nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def nil)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
nil)
(integrable2? const-decl "bool" product_integral_def nil)
(integrable2 nonempty-type-eq-decl nil product_integral_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(integral const-decl "real" integral nil))
shostak))
(integral1_TCC1 0
(integral1_TCC1-1 nil 3458972704
("" (skosimp)
(("" (name "DRL" "null_integrable1(h1!1)")
(("" (replace -1)
(("" (assert)
(("" (name "NN" "DRL`1")
(("" (name "FF" "DRL`2")
((""
(lemma "null_integral1_def"
("N1" "NN" "f" "FF" "h1" "h1!1"))
(("" (assert)
(("" (typepred "FF")
((""
(lemma "indefinite_integrable[T1, S1, mu]"
("E" "complement(NN)" "f" "FF"))
(("" (expand "complement")
(("" (expand "phi")
(("" (expand "member")
(("" (expand "*")
((""
(expand "FF")
((""
(expand "NN")
((""
(case-replace
"(LAMBDA (x: T1):
IF NOT DRL`1(x) THEN 1 ELSE 0 ENDIF * DRL`2(x))=(LAMBDA x: IF DRL`1(x) THEN 0 ELSE DRL`2(x) ENDIF)")
((""
(apply-extensionality :hide? t)
((""
(lift-if)
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((null_integrable1 const-decl
"[null_set[T1, S1, mu], integrable[T1, S1, mu]]"
product_integral_def nil)
(integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(integrable1? const-decl "bool" product_integral_def nil)
(T2 formal-type-decl nil product_integral_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
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)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil product_integral_def nil)
(member const-decl "bool" sets nil)
(subset_algebra_complement application-judgement "(S)" measure_def
nil)
(measurable_complement application-judgement "measurable_set"
product_integral_def nil)
(indefinite_integrable formula-decl nil integral nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(complement const-decl "set" sets nil)
(phi const-decl "nat" measure_space nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(NN skolem-const-decl "null_set[T1, S1, mu]" product_integral_def
nil)
(real_times_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(FF skolem-const-decl "integrable[T1, S1, mu]" product_integral_def
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(null_integral1_def formula-decl nil product_integral_def nil))
nil))
(integral2_TCC1 0
(integral2_TCC1-1 nil 3458972704
("" (skosimp)
(("" (lemma "null_integral2_def" ("h2" "h2!1"))
(("" (name "DRL" "null_integrable2(h2!1)")
(("" (replace -1)
(("" (name "NN" "DRL`1")
(("" (name "GG" "DRL`2")
(("" (inst - "NN" "GG" "_")
(("" (assert)
(("" (replace -1)
(("" (replace -2)
((""
(lemma "indefinite_integrable[T2, S2, nu]"
("E" "complement(NN)" "f" "GG"))
(("" (expand "complement")
(("" (expand "phi")
(("" (expand "member")
((""
(expand "*")
((""
(case-replace
"(LAMBDA (x: T2): IF NOT NN(x) THEN 1 ELSE 0 ENDIF * GG(x))=(LAMBDA y: IF NN(y) THEN 0 ELSE GG(y) ENDIF)")
((""
(apply-extensionality :hide? t)
((""
(lift-if)
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((integrable2 nonempty-type-eq-decl nil product_integral_def nil)
(integrable2? const-decl "bool" product_integral_def 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)
(T2 formal-type-decl nil product_integral_def nil)
(T1 formal-type-decl nil product_integral_def nil)
(null_integral2_def formula-decl nil product_integral_def nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(phi const-decl "nat" measure_space nil)
(complement const-decl "set" sets nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(indefinite_integrable formula-decl nil integral nil)
(measurable_complement application-judgement "measurable_set"
product_integral_def nil)
(subset_algebra_complement application-judgement "(S)" measure_def
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)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def 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)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(null_integrable2 const-decl
"[null_set[T2, S2, nu], integrable[T2, S2, nu]]"
product_integral_def nil))
nil))
(integral1_zero 0
(integral1_zero-1 nil 3458973878
("" (apply-extensionality :hide? t)
(("1" (expand "integral1")
(("1" (expand "member")
(("1" (lemma "null_integral1_def" ("h1" "LAMBDA x, y: 0"))
(("1"
(inst - "null_integrable1(LAMBDA x, y: 0)`1"
"null_integrable1(LAMBDA x, y: 0)`2" "x!1")
(("1" (expand "member")
(("1"
(case-replace
"null_integrable1(LAMBDA x, y: 0)`1(x!1)")
(("1" (assert)
(("1" (split)
(("1" (flatten)
(("1" (rewrite "integral_zero")
(("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2" (decompose-equality)
(("2" (rewrite "integrable1_zero") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "integrable1_zero") nil nil))
nil)
("2" (rewrite "integrable1_zero") nil nil))
nil))
nil))
nil)
("2" (rewrite "integrable1_zero") nil nil))
nil)
((null_integral1_def formula-decl nil product_integral_def nil)
(integrable1_zero formula-decl nil product_integral_def nil)
(integral_zero formula-decl nil integral nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_integral_def nil)
(nu formal-const-decl "measure_type[T2, S2]" product_integral_def
nil)
(null_integrable1 const-decl
"[null_set[T1, S1, mu], integrable[T1, S1, mu]]"
product_integral_def nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
(integrable1? const-decl "bool" product_integral_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T2 formal-type-decl nil product_integral_def nil)
(integrable1 nonempty-type-eq-decl nil product_integral_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_integral_def 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)
(mu formal-const-decl "measure_type[T1, S1]" product_integral_def
nil)
(integrable? const-decl "bool" integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integral1 const-decl "integrable[T1, S1, mu]" product_integral_def
nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(T1 formal-type-decl nil product_integral_def nil))
shostak))
(integral1_add 0
(integral1_add-1 nil 3458971378
("" (skosimp)
(("" (expand "ae_eq?")
(("" (expand "restrict")
(("" (expand "pointwise_ae?")
(("" (expand "ae?")
(("" (expand "fullset")
(("" (expand "ae_in?")
(("" (expand "member")
(("" (expand "integral1")
(("" (expand "member")
(("" (name "NN3" "null_integrable1(h1!1)`1")
(("" (name "NN2" "null_integrable1(g1!1)`1")
((""
(name "NN1"
"null_integrable1(g1!1+h1!1)`1")
(("" (inst + "union(NN1,union(NN2,NN3))")
((""
(skosimp)
((""
(expand "union")
((""
(expand "member")
((""
(flatten)
((""
(replace -1)
((""
(replace -2)
((""
(replace -3)
((""
(expand "+" 4 2)
((""
(assert)
((""
(name
"FF3"
"null_integrable1(h1!1)`2")
((""
(name
"FF2"
"null_integrable1(g1!1)`2")
((""
(name
"FF1"
"null_integrable1(g1!1+h1!1)`2")
((""
(replace -1)
((""
(replace -2)
((""
(replace
-3)
((""
(lemma
"null_integral1_def"
("h1"
"h1!1"
"f"
"FF3"
"N1"
"NN3"
"x"
"x!1"))
((""
(assert)
((""
(flatten)
((""
(lemma
"null_integral1_def"
("h1"
"g1!1"
"f"
"FF2"
"N1"
"NN2"
"x"
"x!1"))
((""
(assert)
((""
(flatten)
((""
(lemma
"null_integral1_def"
("h1"
"g1!1+h1!1"
"f"
"FF1"
"N1"
"NN1"
"x"
"x!1"))
((""
(assert)
((""
(flatten)
((""
(replace
-2
*
rl)
((""
(replace
-4
*
rl)
((""
(replace
-6
*
rl)
((""
(lemma
"integral_add[T2,S2,nu]"
("f1"
"LAMBDA y: g1!1(x!1, y)"
"f2"
"LAMBDA y: h1!1(x!1, y)"))
((""
(expand
"+"
4)
((""
(expand
"+"
-1)
((""
(propax)
nil
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.54 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.
|
