|
(product_sigma
(cross_product_is_sigma_times 0
(cross_product_is_sigma_times-1 nil 3459218355
("" (skosimp)
(("" (expand "sigma_times")
((""
(lemma "generated_sigma_algebra_subset1"
("X" "extend
[setof[[T1, T2]],
measurable_rectangle[T1, T2](S1, S2),
bool, FALSE]
(fullset
[measurable_rectangle
[T1, T2](S1, S2)])"))
(("" (expand "subset?")
(("" (expand "member")
(("" (inst - "cross_product(X!1, Y!1)")
(("" (assert)
(("" (hide 2)
(("" (expand "fullset")
(("" (expand "extend")
(("" (prop)
(("" (expand "measurable_rectangle?")
(("" (inst + "X!1" "Y!1")
(("" (assert)
((""
(apply-extensionality :hide? t)
((""
(expand "cross_product")
(("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
nil)
(subset? const-decl "bool" sets nil)
(cross_product const-decl "set[[T1, T2]]" cross_product
"topology/")
(member const-decl "bool" sets nil)
(generated_sigma_algebra_subset1 formula-decl nil
subset_algebra_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)
(set 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)
(measurable_rectangle? const-decl "bool" product_sigma_def nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_sigma nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_sigma nil)
(measurable_rectangle nonempty-type-eq-decl nil product_sigma_def
nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(fullset const-decl "set" sets nil)
(T1 formal-type-decl nil product_sigma nil)
(T2 formal-type-decl nil product_sigma nil))
shostak))
(rectangle_algebra_aux 0
(rectangle_algebra_aux-1 nil 3450413455
(""
(case "FORALL (a, b: (measurable_rectangle?[T1, T2](S1, S2))):
measurable_rectangle?[T1, T2](S1, S2)(intersection(a,b))")
(("1"
(lemma "disjoint_algebra_construction[[T1,T2]]"
("NX" "measurable_rectangle?[T1, T2](S1, S2)"))
(("1" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)
("3" (hide -1 2)
(("3" (skosimp)
(("3" (typepred "a!1")
(("3" (expand "finite_disjoint_union?")
(("3" (expand "member")
(("3" (expand "measurable_rectangle?")
(("3" (skosimp)
(("3"
(inst +
"lambda (i:nat): if i=0 then cross_product(X!1,complement(Y!1)) elsif i=1 then cross_product(complement(X!1),complement(Y!1)) elsif i=2 then cross_product(complement(X!1),Y!1) else emptyset endif"
"3")
(("3" (split)
(("1" (expand "disjoint?")
(("1" (expand "cross_product")
(("1"
(expand "complement")
(("1"
(expand "disjoint?")
(("1"
(expand "intersection")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(skosimp)
(("1"
(skosimp*)
(("1"
(expand "emptyset")
(("1"
(case-replace "i!1=0")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil)
("2"
(case-replace
"i!1=1")
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(case-replace
"i!1=2")
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (hide -1)
(("2"
(apply-extensionality :hide? t)
(("2"
(expand "complement")
(("2"
(expand "cross_product")
(("2"
(expand "member")
(("2"
(expand "emptyset")
(("2"
(expand "IUnion")
(("2"
(case-replace "X!1(x!1)")
(("1"
(case-replace "Y!1(x!2)")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(inst + "0")
nil
nil))
nil))
nil)
("2"
(case-replace "Y!1(x!2)")
(("1"
(assert)
(("1"
(inst + "2")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(inst + "1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (hide -1)
(("3"
(case "i!1=0")
(("1"
(assert)
(("1"
(typepred "S2")
(("1"
(expand "sigma_algebra?")
(("1"
(expand
"subset_algebra_complement?")
(("1"
(flatten)
(("1"
(inst - "Y!1")
(("1"
(expand "member")
(("1"
(inst
+
"X!1"
"complement(Y!1)")
(("1"
(assert)
(("1"
(apply-extensionality
:hide?
t)
(("1"
(expand
"cross_product")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace "i!1=1")
(("1"
(assert)
(("1"
(typepred "S2")
(("1"
(typepred "S1")
(("1"
(expand "sigma_algebra?")
(("1"
(expand
"subset_algebra_complement?")
(("1"
(flatten)
(("1"
(expand "member")
(("1"
(inst - "X!1")
(("1"
(inst - "Y!1")
(("1"
(inst
+
"complement(X!1)"
"complement(Y!1)")
(("1"
(assert)
(("1"
(hide-all-but
2)
(("1"
(apply-extensionality
:hide?
t)
(("1"
(expand
"cross_product")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace "i!1=2")
(("1"
(assert)
(("1"
(typepred "S1")
(("1"
(expand "sigma_algebra?")
(("1"
(expand
"subset_algebra_complement?")
(("1"
(flatten)
(("1"
(expand "member")
(("1"
(inst - "X!1")
(("1"
(inst
+
"complement(X!1)"
"Y!1")
(("1"
(assert)
(("1"
(expand
"cross_product")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(rewrite "emptyset_is_empty?")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst - "emptyset")
(("2" (expand "measurable_rectangle?")
(("2" (inst + "emptyset" "emptyset")
(("2" (typepred "S2")
(("2" (typepred "S1")
(("2" (expand "sigma_algebra?")
(("2" (flatten)
(("2" (expand "subset_algebra_empty?")
(("2"
(expand "member")
(("2"
(assert)
(("2"
(apply-extensionality :hide? t)
(("2"
(expand "emptyset")
(("2"
(expand "cross_product")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (typepred "b!1")
(("2" (typepred "a!1")
(("2" (expand "measurable_rectangle?")
(("2" (skosimp*)
(("2"
(inst + "intersection(X!1,X!2)"
"intersection(Y!1,Y!2)")
(("2"
(lemma "sigma_algebra_intersection[T1,S1]"
("x" "X!1" "y" "X!2"))
(("1"
(lemma "sigma_algebra_intersection[T2,S2]"
("x" "Y!1" "y" "Y!2"))
(("1" (expand "member")
(("1" (assert)
(("1" (replace -3)
(("1" (replace -6)
(("1"
(hide-all-but 1)
(("1"
(apply-extensionality :hide? t)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sigma_algebra_intersection formula-decl nil sigma_algebra nil)
(nonempty? const-decl "bool" sets nil)
(disjoint_algebra_construction formula-decl nil subset_algebra_def
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
(IUnion const-decl "set[T]" indexed_sets nil)
(subset_algebra_complement application-judgement "(S)"
sigma_algebra nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(subset_algebra_complement? const-decl "bool" subset_algebra_def
nil)
(emptyset const-decl "set" sets nil)
(complement const-decl "set" sets nil)
(cross_product const-decl "set[[T1, T2]]" cross_product
"topology/")
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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)
(finite_disjoint_union? const-decl "bool" subset_algebra_def nil)
(member const-decl "bool" sets nil)
(subset_algebra_intersection application-judgement "(S)"
sigma_algebra nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
(T1 formal-type-decl nil product_sigma nil)
(T2 formal-type-decl nil product_sigma 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)
(measurable_rectangle? const-decl "bool" product_sigma_def nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_sigma nil)
(S2 formal-const-decl "sigma_algebra[T2]" product_sigma nil)
(intersection const-decl "set" sets nil))
shostak))
(rectangle_algebra_TCC1 0
(rectangle_algebra_TCC1-1 nil 3450331052
("" (lemma "rectangle_algebra_aux")
((""
(typepred
"generated_subset_algebra[[T1, T2]](measurable_rectangle?(S1, S2))")
(("" (assert) nil nil)) nil))
nil)
((S2 formal-const-decl "sigma_algebra[T2]" product_sigma nil)
(S1 formal-const-decl "sigma_algebra[T1]" product_sigma nil)
(measurable_rectangle? const-decl "bool" product_sigma_def nil)
(set type-eq-decl nil sets nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(generated_subset_algebra const-decl "subset_algebra"
subset_algebra_def nil)
(subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(subset_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T2 formal-type-decl nil product_sigma nil)
(T1 formal-type-decl nil product_sigma nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(rectangle_algebra_aux formula-decl nil product_sigma nil))
nil))
(rectangle_algebra_def 0
(rectangle_algebra_def-1 nil 3450414364
("" (lemma "rectangle_algebra_aux")
(("" (expand "rectangle_algebra") (("" (assert) nil nil)) nil))
nil)
((rectangle_algebra const-decl "subset_algebra[[T1, T2]]"
product_sigma nil)
(rectangle_algebra_aux formula-decl nil product_sigma nil))
shostak))
(finite_disjoint_rectangles 0
(finite_disjoint_rectangles-1 nil 3455513659
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (expand "finite_disjoint_unions")
(("1" (expand "fullset")
(("1" (expand "extend")
(("1" (prop)
(("1" (expand "finite_disjoint_union?")
(("1" (skosimp)
(("1" (expand "member")
(("1"
(case "forall (i:nat): measurable_rectangle?[T1, T2](S1, S2)(E!1(i))")
(("1"
(inst +
"image[nat,(measurable_rectangle?(S1, S2))](E!1,{n | n < n!1})")
(("1" (split)
(("1" (replace -3)
(("1"
(apply-extensionality :hide? t)
(("1"
(hide -3 -2)
(("1"
(case-replace
"IUnion(E!1)(x!1, x!2)")
(("1"
(expand "IUnion")
(("1"
(skosimp)
(("1"
(expand "Union")
(("1"
(typepred "i!1")
(("1"
(inst -4 "i!1")
(("1"
(flatten)
(("1"
(case-replace
"i!1)
(("1"
(inst + "E!1(i!1)")
(("1"
(assert)
(("1"
(expand
"image")
(("1"
(inst
+
"i!1")
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand "empty?")
(("2"
(inst
-5
"(x!1,x!2)")
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand "IUnion")
(("2"
(expand "Union")
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(assert)
(("2"
(expand "image")
(("2"
(skolem - "i!1")
(("2"
(typepred "i!1")
(("2"
(inst + "i!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp) nil nil))
nil))
nil)
("2"
(lemma
"finite_image[nat, (measurable_rectangle?(S1, S2))]"
("f" "E!1" "S" "{n | n < n!1}"))
(("1" (propax) nil nil)
("2"
(hide-all-but 1)
(("2"
(expand "is_finite")
(("2"
(inst
+
"n!1"
"lambda (i:{n | n < n!1}): i")
(("2"
(expand "injective?")
(("2" (skosimp) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp)
(("3"
(typepred "x!1")
(("3"
(typepred "y!1")
(("3"
(expand "image")
(("3"
(skolem - "i!1")
(("3"
(skolem - "i!2")
(("3"
(typepred "i!1")
(("3"
(typepred "i!2")
(("3"
(expand "disjoint?" -8)
(("3"
(replace -4)
(("3"
(replace -6)
(("3"
(hide-all-but
(1 2 -8))
(("3"
(inst
-
"i!1"
"i!2")
(("3"
(case-replace
"i!1=i!2")
(("3"
(assert)
(("3"
(expand
"disjoint?")
(("3"
(expand
"intersection")
(("3"
(expand
"empty?")
(("3"
(skosimp)
(("3"
(inst
-
"x!2")
(("3"
(expand
"member")
(("3"
(flatten)
(("3"
(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 -1 -2 2)
(("2" (skosimp)
(("2" (inst - "i!1")
(("2"
(case-replace "i!1)
(("1" (flatten) nil nil)
("2"
(assert)
(("2"
(rewrite "emptyset_is_empty?")
(("2"
(replace -1)
(("2"
(expand
"measurable_rectangle?")
(("2"
(inst
+
"emptyset"
"emptyset")
(("2"
(split)
(("1"
(apply-extensionality
:hide?
t)
(("1" (grind) nil nil))
nil)
("2"
(typepred "S1")
(("2"
(expand
"sigma_algebra?")
(("2"
(expand
"subset_algebra_empty?")
(("2"
(expand "member")
(("2"
(flatten)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(typepred "S2")
(("3"
(expand
"sigma_algebra?")
(("3"
(expand
"subset_algebra_empty?")
(("3"
(expand "member")
(("3"
(flatten)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "finite_disjoint_unions")
(("2" (expand "extend")
(("2" (expand "fullset")
(("2" (prop)
(("2" (expand "finite_disjoint_union?")
(("2"
(case "forall (n:nat,R,Z): is_finite(R) & card(R) <= n & Union(LAMBDA (t: setof[[T1, T2]]):
IF measurable_rectangle?(S1, S2)(t) THEN R(t)
ELSE FALSE
ENDIF)
= Z & (FORALL (x, y: (R)): x = y OR disjoint?(x, y)) => EXISTS (E: sequence[set[[T1, T2]]]), n:
disjoint?(E) AND
Z = IUnion(E) AND
(FORALL i:
(i < n => member(E(i), measurable_rectangle?(S1, S2))) AND
(i >= n => empty?(E(i))))")
(("1" (inst - "card(R!1)" "R!1" "Z!1")
(("1" (assert)
(("1" (replace -4) (("1" (propax) nil nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (induct "n")
(("1" (skosimp)
(("1" (expand "<=" -2)
(("1" (split)
(("1" (assert) nil nil)
("2"
(lemma "card_is_0" ("S" "R!2"))
(("2"
(replace -2 -1)
(("2"
(replace -1)
(("2"
(hide -2 -3)
(("2"
(case-replace
"Z!2=emptyset[[T1,T2]]")
(("1"
(hide-all-but 1)
(("1"
(inst
+
"lambda (i:nat): emptyset[[T1,T2]]"
"0")
(("1"
(split)
(("1" (grind) nil nil)
("2"
(apply-extensionality
:hide?
t)
(("2"
(expand "emptyset")
(("2"
(expand "IUnion")
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(assert)
(("3"
(rewrite
"emptyset_is_empty?")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 -2 1))
(("2"
(apply-extensionality
:hide?
t)
(("2"
(replace -2 1 rl)
(("2"
(hide -2)
(("2"
(expand "emptyset")
(("2"
(expand "Union")
(("2"
(skosimp)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "<=" -3)
(("2" (split -3)
(("1"
(inst -2 "R!2" "Z!2")
(("1"
(assert)
(("1"
(replace -5)
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(lemma "nonempty_card" ("S" "R!2"))
(("2"
(flatten -1)
(("2"
(hide -1)
(("2"
(split -1)
(("1"
(lemma "card_rest" ("S" "R!2"))
(("1"
(copy -2)
(("1"
(expand "nonempty?" -1)
(("1"
(replace 1)
(("1"
(replace -3)
(("1"
(simplify -1)
(("1"
(lemma
"choose_rest"
("a" "R!2"))
(("1"
(replace 1)
(("1"
(inst
-5
"rest(R!2)"
"Union(rest(R!2))")
(("1"
(split -5)
(("1"
(skosimp)
(("1"
(lemma
"extensionality_postulate"
("f"
"Union(extend
[setof[[T1, T2]],
((measurable_rectangle?[T1, T2](S1, S2))), bool, FALSE]
(rest(R!2)))"
"g"
"IUnion(E!1)"))
(("1"
(flatten)
(("1"
(hide
-1)
(("1"
(split
-1)
(("1"
(hide
-3)
(("1"
(case
"Z!2 = union(choose(R!2), IUnion(E!1))")
(("1"
(case
"forall (i:nat): disjoint?(choose(R!2),E!1(i))")
(("1"
(inst
+
"lambda (i:nat): if i=0 then choose(R!2) else E!1(i-1) endif"
"n!1+1")
(("1"
(split)
(("1"
(expand
"disjoint?"
(-4
1))
(("1"
(skosimp)
(("1"
(case-replace
"i!1=0")
(("1"
(assert)
(("1"
(inst
-2
"j!2-1")
nil
nil))
nil)
("2"
(replace
1)
(("2"
(case-replace
"j!2=0")
(("1"
(inst
-2
"i!1-1")
(("1"
(hide-all-but
(-2
3))
(("1"
(expand
"disjoint?")
(("1"
(expand
"intersection")
(("1"
(expand
"empty?")
(("1"
(expand
"member")
(("1"
(skosimp)
(("1"
(inst
-
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
(("2"
(inst
-4
"i!1-1"
"j!2-1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(apply-extensionality
:hide?
t)
(("1"
(replace
-2
1)
(("1"
(hide
-2)
(("1"
(expand
"union")
(("1"
(expand
"member")
(("1"
(case-replace
"choose(R!2)(x!1, x!2)")
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.45 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.
|
