|
(sigma_finite_measure_props
(sfm_integrable_TCC1 0
(sfm_integrable_TCC1-1 nil 3459603923
("" (expand "measurable_set?") (("" (propax) nil nil)) nil)
((measurable_set? const-decl "bool" measure_space_def nil)) nil))
(sfm_integrable_TCC2 0
(sfm_integrable_TCC2-1 nil 3459603923 ("" (skosimp*) nil nil) nil
nil))
(sfm_integrable 0
(sfm_integrable-1 nil 3459603934
("" (skosimp)
((""
(lemma "contraction_integrable_def[T, S, mu]"
("h" "h!1" "A" "A_of(mu)"))
(("" (rewrite "A_of_def1")
(("" (typepred "h!1")
(("" (expand "nn_measurable?")
(("" (flatten)
(("" (expand ">=" -3)
(("" (replace -2)
(("" (replace -3 1 rl) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((mu formal-const-decl "sigma_finite_measure"
sigma_finite_measure_props nil)
(sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
(sigma_finite_measure? const-decl "bool" 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" sigma_finite_measure_props
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 sigma_finite_measure_props nil)
(nn_measurable nonempty-type-eq-decl nil measure_space nil)
(nn_measurable? const-decl "bool" measure_space nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(A_of const-decl "disjoint_indexed_measurable" measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def 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)
(contraction_integrable_def formula-decl nil
measure_contraction_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
sigma_finite_measure_props nil)
(subset_algebra_fullset name-judgement "(S)"
sigma_finite_measure_props nil)
(A_of_def1 formula-decl nil measure_def nil))
shostak))
(sfm_integral_TCC1 0
(sfm_integral_TCC1-1 nil 3459603923
("" (skosimp)
(("" (typepred "f!1")
(("" (rewrite "contraction_integrable")
(("1" (rewrite "indefinite_integrable[T, S, mu]")
(("1" (expand "measurable_set?") (("1" (propax) nil nil))
nil))
nil)
("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
((nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(mu formal-const-decl "sigma_finite_measure"
sigma_finite_measure_props nil)
(sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
(sigma_finite_measure? const-decl "bool" measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(S formal-const-decl "sigma_algebra" sigma_finite_measure_props
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 sigma_finite_measure_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(indefinite_integrable formula-decl nil integral nil)
(prod_measurable application-judgement "measurable_function[T, S]"
sigma_finite_measure_props nil)
(phi_is_simple application-judgement "simple"
sigma_finite_measure_props nil)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(A_of const-decl "disjoint_indexed_measurable" measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(measurable_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)
(contraction_integrable formula-decl nil measure_contraction nil))
nil))
(sfm_integral 0
(sfm_integral-1 nil 3459604066
("" (skosimp)
((""
(lemma "indefinite_countably_additive[T, S, mu]"
("f" "f!1" "DX" "A_of(mu)"))
(("" (rewrite "A_of_def1" -1)
(("" (rewrite "indefinite_fullset[T, S, mu]")
((""
(case-replace "(LAMBDA n:
integral[T, S, contraction(mu, A_of(mu)(n))]
(f!1))=LAMBDA n: integral[T,S,mu](A_of(mu)(n), f!1)")
(("1" (apply-extensionality :hide? t)
(("1" (hide 2)
(("1" (rewrite "contraction_integral")
(("1" (expand "integral" 1 2)
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (typepred "f!1")
(("2" (skosimp)
(("2"
(lemma "nn_integrable_is_integrable[T, S, mu]")
(("2" (inst - "f!1")
(("2" (expand "integrable?" 1)
(("2"
(rewrite "indefinite_integrable[T, S, mu]")
(("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "measurable_set?") (("3" (propax) nil nil))
nil)
("4" (skosimp)
(("4" (hide-all-but 1)
(("4" (typepred "f!1")
(("4"
(lemma "nn_integrable_is_integrable[T, S, mu]")
(("4" (inst - "f!1")
(("4" (rewrite "contraction_integrable")
(("1"
(rewrite "indefinite_integrable[T, S, mu]")
(("1" (expand "measurable_set?")
(("1" (propax) nil nil)) nil))
nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (typepred "f!1")
(("2" (skosimp)
(("2" (expand "integrable?")
(("2" (rewrite "indefinite_integrable[T, S, mu]")
(("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "measurable_set?") (("3" (propax) nil nil))
nil)
("4" (hide-all-but 1)
(("4" (typepred "f!1")
(("4" (skosimp)
(("4" (lemma "nn_integrable_is_integrable[T, S, mu]")
(("4" (inst - "f!1")
(("4" (rewrite "contraction_integrable" 1)
(("1"
(rewrite "indefinite_integrable[T, S, mu]")
(("1" (expand "measurable_set?")
(("1" (propax) nil nil)) nil))
nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((mu formal-const-decl "sigma_finite_measure"
sigma_finite_measure_props nil)
(sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
(sigma_finite_measure? const-decl "bool" 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" sigma_finite_measure_props
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 sigma_finite_measure_props nil)
(nn_integrable nonempty-type-eq-decl nil nn_integral nil)
(nn_integrable? const-decl "bool" nn_integral nil)
(integrable nonempty-type-eq-decl nil integral nil)
(integrable? const-decl "bool" integral nil)
(A_of const-decl "disjoint_indexed_measurable" measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def 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)
(indefinite_countably_additive formula-decl nil indefinite_integral
nil)
(indefinite_fullset formula-decl nil indefinite_integral nil)
(f!1 skolem-const-decl "nn_integrable[T, S, mu]"
sigma_finite_measure_props nil)
(contraction_integral formula-decl nil measure_contraction nil)
(phi_is_simple application-judgement "simple"
sigma_finite_measure_props nil)
(prod_measurable application-judgement "measurable_function[T, S]"
sigma_finite_measure_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nn_integrable_is_integrable judgement-tcc nil integral nil)
(indefinite_integrable formula-decl nil integral nil)
(measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(contraction_integrable formula-decl nil measure_contraction nil)
(integral const-decl "real" indefinite_integral nil)
(integrable? const-decl "bool" indefinite_integral nil)
(integral const-decl "real" integral nil)
(contraction const-decl "measure_type" measure_contraction 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)
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure? const-decl "bool" generalized_measure_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(measurable_fullset name-judgement "measurable_set[T, S]"
sigma_finite_measure_props nil)
(subset_algebra_fullset name-judgement "(S)"
sigma_finite_measure_props nil)
(A_of_def1 formula-decl nil measure_def nil))
shostak))
(sfm_component_eq_TCC1 0
(sfm_component_eq_TCC1-1 nil 3459609819
("" (expand "measurable_set?")
(("" (skosimp) (("" (rewrite "A_of_def2") nil nil)) nil)) nil)
((S formal-const-decl "sigma_algebra" sigma_finite_measure_props
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 sigma_finite_measure_props 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)
(mu formal-const-decl "sigma_finite_measure"
sigma_finite_measure_props nil)
(sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
(sigma_finite_measure? const-decl "bool" 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)
(A_of_def2 formula-decl nil measure_def nil)
(measurable_set? const-decl "bool" measure_space_def nil))
nil))
(sfm_component_eq 0
(sfm_component_eq-1 nil 3459609938
("" (skosimp)
(("" (expand "fm_contraction")
(("" (expand "contraction")
(("" (expand "to_measure")
(("" (expand "x_eq")
(("" (lemma "A_of_def2" ("n" "n!1" "mu" "mu"))
((""
(lemma "m_monotone[T,S,mu]"
("a" "intersection(A_of(mu)(n!1), A!1)" "b"
"A_of(mu)(n!1)"))
(("1" (assert)
(("1" (expand "x_le")
(("1" (expand "subset?")
(("1" (expand "intersection")
(("1" (expand "member")
(("1" (skosimp) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil)
("3" (expand "measurable_set?")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fm_contraction const-decl "finite_measure" measure_contraction
nil)
(to_measure const-decl "measure_type" generalized_measure_def nil)
(S formal-const-decl "sigma_algebra" sigma_finite_measure_props
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 sigma_finite_measure_props 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)
(mu formal-const-decl "sigma_finite_measure"
sigma_finite_measure_props nil)
(sigma_finite_measure nonempty-type-eq-decl nil measure_def nil)
(sigma_finite_measure? const-decl "bool" 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)
(A_of_def2 formula-decl nil measure_def nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(subset_algebra_intersection application-judgement "(S)"
sigma_finite_measure_props nil)
(m_monotone formula-decl nil measure_props nil)
(set type-eq-decl nil sets nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(intersection const-decl "set" sets nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(A_of const-decl "disjoint_indexed_measurable" measure_def nil)
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(contraction const-decl "measure_type" measure_contraction nil))
shostak))
(sfm_monotone_convergence_TCC1 0
(sfm_monotone_convergence_TCC1-1 nil 3461644768
("" (skosimp)
(("" (skolem + "n!1")
(("" (expand "measurable_set?") (("" (propax) nil nil)) nil))
nil))
nil)
((measurable_set? const-decl "bool" measure_space_def nil)) nil))
(sfm_monotone_convergence_TCC2 0
(sfm_monotone_convergence_TCC2-1 nil 3461645137
("" (skosimp) nil nil) nil nil))
(sfm_monotone_convergence 0
(sfm_monotone_convergence-1 nil 3461645212
("" (skosimp)
((""
(case "forall n: integrable?[T, S, mu](*[T](phi(P_of(mu)(n)),F!1(n)))")
(("1"
(case "forall n: integral[T, S, contraction(mu, P_of(mu)(n))](F!1(n)) = integral[T, S, mu](*[T](phi(P_of(mu)(n)), F!1(n)))")
(("1" (name "G" "lambda n: *[T](phi(P_of(mu)(n)), F!1(n))")
(("1" (hide -1)
(("1" (case "forall n: integrable?[T, S, mu](G(n))")
(("1"
(case "FORALL n:
integral[T, S, contraction(mu, P_of(mu)(n))](F!1(n)) =
integral[T, S, mu](G(n))")
(("1"
(case-replace "(LAMBDA n:
integral[T, S, contraction(mu, P_of(mu)(n))](F!1(n)))=integral o G")
(("1" (hide -1)
(("1" (case "ae_increasing?(G)")
(("1"
(case "forall g: ae_convergence?(F!1,g) <=> ae_convergence?(G, g)")
(("1" (hide-all-but (-1 -2 -4 1))
(("1"
(lemma "monotone_convergence" ("F" "G"))
(("1" (replace -3)
(("1"
(case-replace
"((EXISTS g: ae_convergence?(F!1, g)) <=> bounded?(integral o G))")
(("1"
(expand "bounded?" 1)
(("1"
(skosimp)
(("1"
(inst -5 "g!1")
(("1"
(assert)
(("1"
(inst -5 "g!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(hide -3 2)
(("2"
(split 1)
(("1"
(skosimp*)
(("1"
(split -2)
(("1"
(name-replace
"DRL1"
"integral o G")
(("1"
(hide-all-but (-1 1))
(("1"
(expand "bounded?")
(("1"
(expand
"bounded_above?")
(("1"
(expand
"bounded_below?")
(("1"
(flatten)
(("1"
(skosimp*)
(("1"
(inst
+
"max(1,max(a!1,-a!2))")
(("1"
(skosimp)
(("1"
(inst
-
"x!1")
(("1"
(inst
-
"x!1")
(("1"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "g!1")
(("2"
(inst -3 "g!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(hide -2)
(("2"
(split -2)
(("1"
(skosimp)
(("1"
(inst + "f!1")
(("1"
(inst - "f!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2"
(name-replace
"DRL1"
"integral o G")
(("2"
(expand "bounded?")
(("2"
(skosimp)
(("2"
(typepred "c!1")
(("2"
(split)
(("1"
(expand
"bounded_above?")
(("1"
(inst
+
"c!1")
(("1"
(skosimp)
(("1"
(inst
-
"x!1")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"bounded_below?")
(("2"
(inst
+
"-c!1")
(("2"
(skosimp)
(("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" (hide-all-but (1 -6 -1 -7))
(("2" (skosimp)
(("2" (split)
(("1"
(flatten)
(("1"
(hide -3 -2)
(("1"
(expand "ae_convergence?")
(("1"
(expand "fullset")
(("1"
(expand "ae_convergence_in?")
(("1"
(expand "ae_in?")
(("1"
(skosimp)
(("1"
(inst + "E!1")
(("1"
(skosimp)
(("1"
(inst - "x!1")
(("1"
(expand "member")
(("1"
(assert)
(("1"
(expand "G")
(("1"
(expand "*")
(("1"
(expand
"phi")
(("1"
(expand
"member")
(("1"
(rewrite
"metric_convergence_def")
(("1"
(rewrite
"metric_convergence_def")
(("1"
(expand
"metric_converges_to")
(("1"
(skosimp)
(("1"
(inst
-
"r!1")
(("1"
(skosimp)
(("1"
(expand
"ball")
(("1"
(expand
"member")
(("1"
(lemma
"P_of_def1"
("mu"
"mu"))
(("1"
(expand
"fullset")
(("1"
(rewrite
"extensionality_postulate"
-1
:dir
rl)
(("1"
(inst
-
"x!1")
(("1"
(expand
"IUnion")
(("1"
(skolem
-
"k!1")
(("1"
(inst
+
"n!1+k!1")
(("1"
(skosimp)
(("1"
(inst
-
"i!1")
(("1"
(lemma
"P_of_def3"
("mu"
"mu"
"i"
"k!1"
"j"
"i!1"))
(("1"
(expand
"subset?")
(("1"
(assert)
(("1"
(inst
-
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(expand "ae_convergence?")
(("2"
(hide -2)
(("2"
(expand "ae_increasing?")
(("2"
(expand "fullset")
(("2"
(expand "ae_convergence_in?")
(("2"
(expand "ae_in?")
(("2"
(skosimp*)
(("2"
(inst
+
"union(E!1,E!2)")
(("2"
(skosimp)
(("2"
(inst - "x!1")
(("2"
(inst - "x!1")
(("2"
(expand
"union")
(("2"
(expand
"member")
(("2"
(flatten)
(("2"
(assert)
(("2"
(rewrite
"metric_convergence_def")
(("2"
(rewrite
"metric_convergence_def")
(("2"
(hide
1
2)
(("2"
(expand
"metric_converges_to")
(("2"
(skosimp)
(("2"
(inst
-
"r!1")
(("2"
(skosimp)
(("2"
(expand
"ball")
(("2"
(expand
"member")
(("2"
(expand
"G")
(("2"
(expand
"*")
(("2"
(expand
"phi")
(("2"
(expand
"member")
(("2"
(lemma
"P_of_def1"
("mu"
"mu"))
(("2"
(expand
"fullset")
(("2"
(rewrite
"extensionality_postulate"
-1
:dir
rl)
(("2"
(inst
-
"x!1")
(("2"
(expand
"IUnion")
(("2"
(skolem
-
"k!1")
(("2"
(inst
+
"n!1+k!1")
(("2"
(skosimp)
(("2"
(inst
-
"i!1")
(("2"
(lemma
"P_of_def3"
("mu"
"mu"
"i"
"k!1"
"j"
"i!1"))
(("2"
(expand
"subset?")
(("2"
(assert)
(("2"
(inst
-
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-5 -6 1))
(("2" (expand "ae_increasing?")
(("2" (skosimp)
(("2" (inst + "E!1")
(("2"
(skosimp)
(("2"
(inst - "x!1")
(("2"
(expand "G")
(("2"
(expand "*")
(("2"
(expand "phi")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst - "i!1" "j!1")
(("2"
(assert)
(("2"
(lemma
"P_of_def3"
("mu"
"mu"
"i"
"i!1"
"j"
"j!1"))
(("2"
(assert)
(("2"
(expand
"subset?")
(("2"
(inst - "x!1")
(("2"
(expand
"member")
(("2"
(inst
-
"j!1"
"x!1")
(("2"
(case-replace
"P_of(mu)(i!1)(x!1)")
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(lift-if
3)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (apply-extensionality :hide? t)
(("1" (inst - "x!1")
(("1" (expand "o ") (("1" (propax) nil nil))
nil))
nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "G") (("2" (propax) nil nil)) nil)
("3" (propax) nil nil))
nil)
("2" (expand "G") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (inst - "n!1")
(("2" (inst - "n!1")
(("2"
(lemma "contraction_integral[T,S]"
("f" "F!1(n!1)" "mu" "mu" "A" "P_of(mu)(n!1)"))
(("1" (propax) nil nil)
("2" (expand "measurable_set?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil)
("4" (expand "measurable_set?") (("4" (propax) nil nil)) nil)
("5" (propax) nil nil))
nil)
("2" (hide-all-but (-3 1))
(("2" (skosimp)
(("2" (inst - "n!1")
(("2"
(lemma "contraction_integrable[T,S]"
("mu" "mu" "A" "P_of(mu)(n!1)" "f"
"*[T](phi(P_of(mu)(n!1)), F!1(n!1))"))
(("1" (assert)
(("1"
(lemma
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.135 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.
|
