|
(measure_def
(IMP_generalized_measure_def_TCC1 0
(IMP_generalized_measure_def_TCC1-1 nil 3458457144
("" (assuming-tcc) nil nil)
((finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(subset_algebra_emptyset name-judgement "(S)" measure_def nil))
nil))
(increasing_indexed_measurable_TCC1 0
(increasing_indexed_measurable_TCC1-1 nil 3450166483
("" (expand "increasing_indexed_measurable?")
(("" (expand "increasing_indexed?")
(("" (split)
(("1" (apply-extensionality :hide? t)
(("1" (expand "fullset")
(("1" (expand "IUnion") (("1" (propax) nil nil)) nil))
nil))
nil)
("2" (expand "increasing?")
(("2" (expand "subset?")
(("2" (expand "fullset")
(("2" (expand "member") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((increasing_indexed? const-decl "bool" nat_indexed_sets
"sets_aux/")
(increasing? const-decl "bool" fun_preds_partial "structures/")
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil measure_def nil)
(fullset const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(set type-eq-decl nil sets nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(increasing_indexed_measurable? const-decl "bool" measure_def nil)
(subset_algebra_fullset name-judgement "(S)" measure_def nil))
nil))
(sigma_finite_measure_TCC1 0
(sigma_finite_measure_TCC1-1 nil 3396670582
("" (expand "sigma_finite_measure?")
(("" (split)
(("1" (lemma "measure_type_TCC1") (("1" (propax) nil nil)) nil)
("2" (expand "measure_sigma_finite?")
(("2" (expand "zero_measure")
(("2"
(inst +
"lambda i: if i = 0 then fullset[T] else emptyset[T] endif")
(("1" (apply-extensionality :hide? t)
(("1" (expand "fullset")
(("1" (expand "IUnion") (("1" (inst + "0") nil nil))
nil))
nil))
nil)
("2" (expand "disjoint_indexed_measurable?")
(("2" (expand "fullset")
(("2" (expand "emptyset")
(("2" (expand "disjoint?")
(("2" (skosimp)
(("2" (expand "disjoint?")
(("2" (expand "intersection")
(("2" (expand "empty?")
(("2" (expand "member")
(("2"
(skosimp*)
(("2"
(case-replace "i!1=0")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((measure_type_TCC1 subtype-tcc nil generalized_measure_def nil)
(T formal-type-decl nil measure_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil)
(subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "subset_algebra" measure_def nil)
(zero_measure const-decl "extended_nnreal" generalized_measure_def
nil)
(intersection const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
(IUnion const-decl "set[T]" indexed_sets nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(set type-eq-decl nil sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(fullset const-decl "set" sets nil)
(emptyset const-decl "set" sets nil)
(subset_algebra_fullset name-judgement "(S)" measure_def nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(subset_algebra_emptyset name-judgement "(S)" measure_def nil)
(measure_sigma_finite? const-decl "bool" measure_def nil)
(sigma_finite_measure? const-decl "bool" measure_def nil))
nil))
(discrete_measure_TCC1 0
(discrete_measure_TCC1-1 nil 3396670582
("" (expand "measure?")
(("" (split)
(("1" (expand "measure_empty?")
(("1" (rewrite "card_emptyset[T]") nil nil)) nil)
("2" (expand "measure_countably_additive?")
(("2"
(name-replace "MM" "LAMBDA a:
IF is_finite[T](a) THEN (TRUE, card[T](a)) ELSE (FALSE, 0) ENDIF")
(("2" (skosimp)
(("2" (expand "x_eq")
(("2" (expand "o ")
(("2" (expand "MM")
(("2" (expand "x_sum")
(("2"
(case-replace
"FORALL i: IF is_finite[T](X!1(i)) THEN TRUE ELSE FALSE ENDIF")
(("1" (case "FORALL i: is_finite[T](X!1(i))")
(("1" (hide -2)
(("1"
(case-replace "(LAMBDA (i_1: nat):
IF is_finite[T](X!1(i_1))
THEN card[T](X!1(i_1))
ELSE 0
ENDIF)=LAMBDA (i_1: nat):card[T](X!1(i_1))")
(("1" (hide -1)
(("1"
(case
"FORALL i: series(LAMBDA (i_1: nat): card[T](X!1(i_1)))(i) = card[T](IUnion(lambda (n:nat): if n <= i then X!1(n) else emptyset[T] endif))")
(("1"
(case
"FORALL i: is_finite[T](IUnion(LAMBDA (n: nat):
IF n <= i THEN X!1(n) ELSE emptyset[T] ENDIF))")
(("1"
(name-replace
"CS"
"series(LAMBDA (i_1: nat): card[T](X!1(i_1)))")
(("1"
(case-replace
"is_finite[T](IUnion(X!1))")
(("1"
(assert)
(("1"
(case-replace
"convergent(CS)")
(("1"
(case "increasing?(CS)")
(("1"
(case
"FORALL i: CS(i) <= card[T](IUnion(X!1))")
(("1"
(lemma
"converges_upto_is_lub"
("u"
"CS"
"x"
"card[T](IUnion(X!1))"))
(("1"
(expand
"converges_upto?"
-1)
(("1"
(replace -3)
(("1"
(flatten -1)
(("1"
(hide -1)
(("1"
(split -1)
(("1"
(rewrite
"convergence_sequences.limit_def")
(("1"
(hide-all-but
(-1 1))
(("1"
(rewrite
"metric_convergence_def")
(("1"
(expand
"metric_converges_to")
(("1"
(expand
"convergence")
(("1"
(expand
"ball")
(("1"
(expand
"member")
(("1"
(skosimp)
(("1"
(inst
-
"epsilon!1")
(("1"
(skosimp)
(("1"
(inst
+
"n!1")
(("1"
(skosimp)
(("1"
(inst
-
"i!1")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"bounded_above?")
(("2"
(inst
+
"card[T](IUnion(X!1))")
nil
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(expand
"fullset")
(("3"
(expand
"image")
(("3"
(expand
"least_upper_bound?")
(("3"
(split)
(("1"
(expand
"upper_bound?")
(("1"
(skosimp)
(("1"
(typepred
"s!1")
(("1"
(skosimp)
(("1"
(inst
-
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"upper_bound?")
(("2"
(case
"y!1)
(("1"
(hide
1)
(("1"
(case
"exists i: IUnion(LAMBDA (n: nat):
IF n <= i THEN X!1(n) ELSE emptyset[T] ENDIF) = IUnion(X!1)")
(("1"
(skosimp)
(("1"
(inst
-3
"CS(i!1)")
(("1"
(inst
-9
"i!1")
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(inst
+
"i!1")
nil
nil))
nil))
nil)
("2"
(hide
-1
-2)
(("2"
(lemma
"convergence_cauchy1"
("u"
"CS"))
(("2"
(assert)
(("2"
(expand
"cauchy")
(("2"
(inst
-
"1/2")
(("2"
(skosimp)
(("2"
(inst
+
"n!1")
(("2"
(apply-extensionality
:hide?
t)
(("2"
(inst
-
"_"
"n!1")
(("2"
(assert)
(("2"
(case-replace
"IUnion(LAMBDA (n: nat):
IF n <= n!1 THEN X!1(n) ELSE emptyset[T] ENDIF)
(x!1)")
(("1"
(expand
"IUnion")
(("1"
(skosimp)
(("1"
(expand
"emptyset")
(("1"
(prop)
(("1"
(inst
+
"i!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(replace
1
2)
(("2"
(assert)
(("2"
(expand
"IUnion")
(("2"
(skosimp)
(("2"
(expand
"emptyset")
(("2"
(case
"i!1>n!1")
(("1"
(inst
-
"i!1")
(("1"
(assert)
(("1"
(hide
1)
(("1"
(expand
"increasing?")
(("1"
(inst
-5
"n!1"
"i!1")
(("1"
(assert)
(("1"
(expand
"abs"
-3)
(("1"
(assert)
(("1"
(expand
"<="
-5)
(("1"
(split
-5)
(("1"
(assert)
(("1"
(inst-cp
-9
"n!1")
(("1"
(inst
-9
"i!1")
(("1"
(replace
-10)
(("1"
(replace
-9)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-4)
(("2"
(inst-cp
-8
"n!1")
(("2"
(inst
-8
"i!1")
(("2"
(replace
-9)
(("2"
(replace
-8)
(("2"
(hide
-9
-8)
(("2"
(lemma
"same_card_subset[T]"
("A"
"{x: T |
EXISTS (i_1: nat):
IF i_1 <= n!1 THEN X!1(i_1)(x) ELSE FALSE ENDIF}"
"B"
"{x_1: T |
EXISTS (i_2: nat):
IF i_2 <= i!1 THEN X!1(i_2)(x_1) ELSE FALSE ENDIF}"))
(("1"
(replace
-2)
(("1"
(hide
-2)
(("1"
(split
-1)
(("1"
(lemma
"extensionality_postulate"
("f"
"{x_1: T |
EXISTS (i_2: nat):
IF i_2 <= n!1 THEN X!1(i_2)(x_1) ELSE FALSE ENDIF}"
"g"
"{x_2: T |
EXISTS (i_1: nat):
IF i_1 <= i!1 THEN X!1(i_1)(x_2) ELSE FALSE ENDIF}"))
(("1"
(replace
-1
-2
rl)
(("1"
(hide
-1)
(("1"
(inst
-
"x!1")
(("1"
(case-replace
"(EXISTS (i_2: nat):
IF i_2 <= n!1 THEN X!1(i_2)(x!1) ELSE FALSE ENDIF)")
(("1"
(skosimp)
(("1"
(prop)
(("1"
(typepred
"X!1")
(("1"
(expand
"disjoint_indexed_measurable?")
(("1"
(expand
"disjoint?")
(("1"
(expand
"disjoint?")
(("1"
(expand
"intersection")
(("1"
(expand
"empty?")
(("1"
(expand
"member")
(("1"
(inst
-
"i!2"
"i!1")
(("1"
(assert)
(("1"
(inst
-
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
1
-1)
(("2"
(assert)
(("2"
(inst
2
"i!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"subset?")
(("2"
(expand
"member")
(("2"
(skosimp*)
(("2"
(prop)
(("2"
(inst
+
"i!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.32 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.
|
