|
(finite_measure
(fm_emptyset 0
(fm_emptyset-1 nil 3321844720
("" (typepred "mu")
(("" (expand "finite_measure?") (("" (flatten) nil nil)) nil)) nil)
((sigma_algebra_IUnion_rew application-judgement "(S)"
finite_measure nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil finite_measure nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" finite_measure 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)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(mu formal-const-decl "finite_measure" finite_measure nil))
shostak))
(fm_convergence 0
(fm_convergence-1 nil 3321844756
("" (skosimp)
(("" (typepred "mu")
(("" (expand "finite_measure?")
(("" (flatten)
(("" (inst - "X!1")
(("" (expand "disjoint_indexed_measurable?")
(("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((mu formal-const-decl "finite_measure" finite_measure nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def 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)
(S formal-const-decl "sigma_algebra" finite_measure 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)
(T formal-type-decl nil finite_measure nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(X!1 skolem-const-decl "[nat -> (S)]" finite_measure 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)
(sigma_algebra_IUnion_rew application-judgement "(S)"
finite_measure nil))
shostak))
(fm_disjointunion 0
(fm_disjointunion-1 nil 3321844999
("" (skosimp)
((""
(name "AA"
"lambda (n:nat): IF n=0 THEN A!1 ELSIF n=1 THEN B!1 ELSE emptyset[T] ENDIF")
(("" (lemma "fm_convergence" ("X" "AA"))
(("" (split -1)
(("1" (hide -2)
(("1" (lemma "zero_tail_series" ("a" "mu o AA" "n" "1"))
(("1" (split)
(("1" (rewrite "limit_equiv")
(("1" (rewrite "limit_equiv")
(("1" (flatten)
(("1" (replace -2)
(("1" (hide-all-but (-4 1))
(("1" (expand "o ")
(("1" (expand "series")
(("1"
(case-replace
"IUnion(AA)=union(A!1, B!1)")
(("1"
(expand "sigma")
(("1"
(expand "sigma")
(("1"
(expand "sigma")
(("1"
(assert)
(("1"
(expand "AA")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality :hide? t)
(("2"
(expand "union")
(("2"
(expand "IUnion")
(("2"
(expand "AA")
(("2"
(expand "member")
(("2"
(case-replace "A!1(x!1)")
(("1"
(inst + "0")
nil
nil)
("2"
(case-replace
"B!1(x!1)")
(("1"
(inst + "1")
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(expand
"emptyset")
(("2"
(propax)
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)
(("2" (skosimp)
(("2" (expand "AA")
(("2" (expand "o")
(("2" (typepred "mu")
(("2" (expand "finite_measure?")
(("2" (flatten)
(("2"
(replace -1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2" (expand "AA")
(("2" (expand "disjoint?")
(("2" (skosimp)
(("2" (case-replace "i!1=0")
(("1" (assert)
(("1" (case-replace "j!1=1")
(("1" (expand "disjoint?")
(("1" (propax) nil nil)) nil)
("2" (expand "disjoint?")
(("2" (assert)
(("2" (expand "intersection")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(skosimp)
(("2"
(expand "emptyset")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "i!1=1")
(("1" (assert)
(("1" (case-replace "j!1=0")
(("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)
("2" (assert)
(("2" (expand "disjoint?")
(("2"
(expand "intersection")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(expand "emptyset")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "disjoint?")
(("2" (expand "emptyset")
(("2" (expand "intersection")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((emptyset const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(S formal-const-decl "sigma_algebra" finite_measure 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil finite_measure 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(subset_algebra_emptyset name-judgement "(S)" finite_measure nil)
(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)
(zero_tail_series formula-decl nil series_aux "series/")
(sequence type-eq-decl nil sequences nil)
(nnreal type-eq-decl nil real_types nil)
(O const-decl "T3" function_props nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(mu formal-const-decl "finite_measure" finite_measure nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(series const-decl "sequence[real]" series "series/")
(limit_equiv formula-decl nil convergence_ops "analysis/")
(member const-decl "bool" sets nil)
(sigma def-decl "real" sigma "reals/")
(AA skolem-const-decl "[nat -> (S)]" finite_measure nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(subset_algebra_union application-judgement "(S)" finite_measure
nil)
(union const-decl "set" sets nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
finite_measure nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(finite_intersection2 application-judgement "finite_set[T]"
countable_setofsets "sets_aux/")
(countable_intersection1 application-judgement "countable_set[T]"
countable_setofsets "sets_aux/")
(subset_algebra_intersection application-judgement "(S)"
finite_measure nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(finite_intersection1 application-judgement "finite_set[T]"
countable_setofsets "sets_aux/")
(countable_intersection2 application-judgement "countable_set[T]"
countable_setofsets "sets_aux/")
(disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
(disjoint? const-decl "bool" sets nil)
(fm_convergence formula-decl nil finite_measure nil))
shostak))
(fm_complement 0
(fm_complement-1 nil 3321856987
("" (skosimp)
(("" (lemma "fm_disjointunion" ("A" "A!1" "B" "complement(A!1)"))
(("1" (split -1)
(("1" (rewrite "union_complement") (("1" (assert) nil nil))
nil)
("2" (hide 2)
(("2" (expand "complement")
(("2" (expand "disjoint?")
(("2" (expand "intersection")
(("2" (expand "empty?")
(("2" (expand "member") (("2" (skosimp*) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sigma_algebra_complement" ("x" "A!1"))
(("2" (expand "member") (("2" (propax) nil nil)) nil)) nil))
nil))
nil)
((complement const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(S formal-const-decl "sigma_algebra" finite_measure 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 finite_measure nil)
(fm_disjointunion formula-decl nil finite_measure nil)
(subset_algebra_complement application-judgement "(S)"
finite_measure nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(union_complement formula-decl nil sets_lemmas_aux nil)
(subset_algebra_fullset name-judgement "(S)" finite_measure nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(fm_union 0
(fm_union-1 nil 3321853771
("" (skosimp)
(("" (rewrite "union_difference")
(("" (lemma "difference_disjoint" ("a" "A!1" "b" "B!1"))
((""
(lemma "fm_disjointunion"
("A" "A!1" "B" "difference(B!1, A!1)"))
(("1" (assert)
(("1" (replace -1)
(("1" (hide -1)
(("1" (assert)
(("1" (rewrite "intersection_commutative")
(("1"
(case "B!1 = union(difference(B!1, A!1),intersection(B!1, A!1))")
(("1"
(case "disjoint?(difference(B!1, A!1), intersection(B!1, A!1))")
(("1"
(lemma "fm_disjointunion"
("A" "difference(B!1, A!1)" "B"
"intersection(B!1, A!1)"))
(("1" (assert) nil nil)
("2"
(lemma "sigma_algebra_intersection"
("x" "B!1" "y" "A!1"))
(("2" (expand "member")
(("2" (propax) nil nil)) nil))
nil))
nil)
("2" (hide -1 -2 2)
(("2" (expand "disjoint?")
(("2" (expand "intersection")
(("2"
(expand "difference")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2" (skosimp*) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality :hide? t)
(("2" (expand "intersection")
(("2" (expand "difference")
(("2"
(expand "union")
(("2"
(expand "member")
(("2"
(case-replace "B!1(x!1)")
(("1"
(assert)
(("1" (flatten) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2"
(lemma "sigma_algebra_difference" ("x" "B!1" "y" "A!1"))
(("2" (expand "member") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((union_difference formula-decl nil sets_lemmas 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)
(S formal-const-decl "sigma_algebra" finite_measure nil)
(T formal-type-decl nil finite_measure nil)
(subset_algebra_difference application-judgement "(S)"
finite_measure nil)
(subset_algebra_union application-judgement "(S)" finite_measure
nil)
(fm_disjointunion formula-decl nil finite_measure nil)
(difference const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(union const-decl "set" sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(intersection_commutative formula-decl nil sets_lemmas nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(subset_algebra_intersection application-judgement "(S)"
finite_measure nil)
(difference_disjoint formula-decl nil sets_lemmas nil))
shostak))
(fm_intersection 0
(fm_intersection-1 nil 3321854440
("" (skosimp)
(("" (lemma "fm_union" ("A" "A!1" "B" "B!1"))
(("" (assert) nil nil)) nil))
nil)
((S formal-const-decl "sigma_algebra" finite_measure 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 finite_measure nil)
(fm_union formula-decl nil finite_measure nil)
(subset_algebra_union application-judgement "(S)" finite_measure
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(subset_algebra_intersection application-judgement "(S)"
finite_measure nil))
shostak))
(fm_difference 0
(fm_difference-1 nil 3321854478
("" (skosimp)
(("" (lemma "disjoint_diff_inter" ("a" "A!1" "b" "B!1"))
(("" (lemma "disjoint_diff_inter" ("a" "B!1" "b" "A!1"))
((""
(lemma "fm_disjointunion"
("A" "difference(A!1, B!1)" "B" "intersection(A!1, B!1)"))
(("1"
(lemma "fm_disjointunion"
("A" "difference(B!1, A!1)" "B" "intersection(B!1, A!1)"))
(("1" (assert)
(("1" (rewrite "union_diff_inter")
(("1" (rewrite "union_diff_inter")
(("1" (rewrite "intersection_commutative")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2"
(lemma "sigma_algebra_intersection"
("x" "B!1" "y" "A!1"))
(("2" (expand "member") (("2" (propax) nil nil)) nil))
nil)
("3"
(lemma "sigma_algebra_difference" ("x" "B!1" "y" "A!1"))
(("3" (expand "member") (("3" (propax) nil nil)) nil))
nil))
nil)
("2"
(lemma "sigma_algebra_intersection" ("y" "B!1" "x" "A!1"))
(("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)
("3"
(lemma "sigma_algebra_difference" ("y" "B!1" "x" "A!1"))
(("3" (expand "member") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil finite_measure nil)
(S formal-const-decl "sigma_algebra" finite_measure 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)
(disjoint_diff_inter formula-decl nil sets_lemmas_aux nil)
(intersection const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(fm_disjointunion formula-decl nil finite_measure nil)
(subset_algebra_intersection application-judgement "(S)"
finite_measure nil)
(subset_algebra_difference application-judgement "(S)"
finite_measure nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(intersection_commutative formula-decl nil sets_lemmas nil)
(union_diff_inter formula-decl nil sets_lemmas_aux nil))
shostak))
(fm_subset 0
(fm_subset-1 nil 3321855702
("" (skosimp)
(("" (lemma "fm_difference" ("A" "A!1" "B" "B!1"))
(("" (lemma "difference_subset2" ("a" "A!1" "b" "B!1"))
(("" (assert)
(("" (replace -1)
(("" (rewrite "fm_emptyset") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((S formal-const-decl "sigma_algebra" finite_measure 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 finite_measure nil)
(fm_difference formula-decl nil finite_measure nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas_aux nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(subset_algebra_difference application-judgement "(S)"
finite_measure nil)
(fm_emptyset formula-decl nil finite_measure 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)" finite_measure nil)
(difference_subset2 formula-decl nil sets_lemmas nil)
(set type-eq-decl nil sets nil))
shostak))
(fm_subset_le 0
(fm_subset_le-1 nil 3321855786
("" (skosimp)
(("" (lemma "fm_subset" ("A" "A!1" "B" "B!1"))
(("" (assert)
(("" (typepred "mu(difference(B!1, A!1))")
(("1" (assert) nil nil)
("2"
(lemma "sigma_algebra_difference" ("x" "B!1" "y" "A!1"))
(("2" (expand "member") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((S formal-const-decl "sigma_algebra" finite_measure 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 finite_measure nil)
(fm_subset formula-decl nil finite_measure nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(mu formal-const-decl "finite_measure" finite_measure nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(subset_algebra_difference application-judgement "(S)"
finite_measure nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas_aux nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(fm_monotone 0
(fm_monotone-1 nil 3455335004
("" (skosimp)
(("" (lemma "fm_subset_le" ("A" "A!1" "B" "B!1"))
(("" (assert) nil nil)) nil))
nil)
((S formal-const-decl "sigma_algebra" finite_measure 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 finite_measure nil)
(fm_subset_le formula-decl nil finite_measure nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas_aux nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(fm_IUnion 0
(fm_IUnion-1 nil 3321857494
("" (skosimp)
((""
(name "DS"
"LAMBDA (i:nat): IF i = 0 THEN X!1(i) ELSE difference(X!1(i),X!1(i-1)) ENDIF")
(("1" (case "disjoint?(DS)")
(("1" (case-replace "IUnion(X!1) = IUnion(DS)")
(("1" (lemma "fm_convergence" ("X" "DS"))
(("1" (assert)
(("1" (expand "o")
(("1"
(case-replace
"series(LAMBDA (x: nat): mu(DS(x))) = LAMBDA (x: nat): mu(X!1(x))")
(("1" (hide-all-but (-3 -5 1))
(("1" (expand "series")
(("1"
(rewrite "extensionality_postulate" 1 :dir rl)
(("1" (induct "x_1")
(("1" (expand "sigma")
(("1" (expand "DS")
(("1"
(expand "sigma")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (expand "sigma" 1)
(("2"
(replace -1 1)
(("2"
(expand "DS")
(("2"
(rewrite "fm_difference")
(("2"
(expand "increasing?")
(("2"
(inst - "j!1" "1+j!1")
(("2"
(assert)
(("2"
(lemma
"difference_subset2"
("a"
"X!1(j!1)"
"b"
"X!1(1 + j!1)"))
(("2"
(assert)
(("2"
(replace -1)
(("2"
(rewrite
"fm_emptyset")
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)
(("2" (apply-extensionality :hide? t)
(("2" (expand "IUnion")
(("2" (expand "DS")
(("2" (hide -1)
(("2" (case-replace "EXISTS (i: nat): X!1(i)(x!1)")
(("1" (skosimp)
(("1"
(case "forall (n:nat): X!1(n) = IUnion(lambda (i:nat): IF i <= n THEN DS(i) ELSE emptyset[T] ENDIF)")
(("1" (inst - "i!1")
(("1" (replace -1 -2)
(("1"
(hide -1)
(("1"
(expand "IUnion")
(("1"
(skosimp*)
(("1"
(expand "emptyset")
(("1"
(case-replace "i!2 <= i!1")
(("1"
(expand "DS")
(("1"
(inst + "i!2")
nil
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2" (induct "n")
(("1"
(expand "IUnion")
(("1"
(apply-extensionality :hide? t)
(("1"
(case-replace "X!1(0)(x!2)")
(("1"
(inst + "0")
(("1"
(assert)
(("1"
(expand "DS")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand "emptyset")
(("2"
(skosimp*)
(("2"
(assert)
(("2"
(expand "<=")
(("2"
(case-replace "i!2=0")
(("1"
(expand "DS")
(("1"
(propax)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(apply-extensionality :hide? t)
(("2"
(expand "IUnion")
(("2"
(expand "emptyset")
(("2"
(expand "increasing?")
(("2"
(inst - "j!1" "j!1+1")
(("2"
(rewrite
"extensionality_postulate"
-1
:dir
rl)
(("2"
(inst - "x!2")
(("2"
(case-replace
"X!1(j!1)(x!2)")
(("1"
(expand "subset?")
(("1"
(inst - "x!2")
(("1"
(expand "member")
(("1"
(assert)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst
+
"i!2")
(("1"
(case-replace
"i!2 <= j!1")
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case-replace
"X!1(1 + j!1)(x!2)")
(("1"
(inst + "1+j!1")
(("1"
(assert)
(("1"
(expand "DS")
(("1"
(expand
"difference")
(("1"
(expand
"member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace 1 3)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(case-replace
"i!2 <= 1 + j!1")
(("1"
(expand
"<="
-1)
(("1"
(split
-1)
(("1"
(inst
+
"i!2")
(("1"
(assert)
nil
nil))
nil)
("2"
(replace
-1)
(("2"
(expand
"DS")
(("2"
(expand
"difference")
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2)
(("2" (assert)
(("2" (skosimp*)
(("2" (inst + "i!1")
(("2"
(case-replace "i!1=0")
(("2"
(assert)
(("2"
(expand "difference")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2" (expand "disjoint?")
(("2" (skosimp*)
(("2" (expand "increasing?")
(("2"
(case "forall (i,j:nat): i < j => disjoint?(DS(i), DS(j))")
(("1" (lemma "trich_lt" ("x" "i!1" "y" "j!1"))
(("1" (split -1)
(("1" (inst - "i!1" "j!1")
(("1" (assert) nil nil)) nil)
("2" (propax) nil nil)
("3" (inst - "j!1" "i!1")
(("3" (assert)
(("3" (rewrite "disjoint_commutative") nil
nil))
nil))
nil))
nil))
nil)
("2" (hide 2 3)
(("2" (skolem 1 ("i" "_"))
(("2" (induct "j")
(("1" (assert) nil nil)
("2" (skosimp*)
(("2" (case-replace "j!2=i")
(("1" (expand "disjoint?")
(("1"
(expand "intersection")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(skosimp*)
(("1"
(expand "DS")
(("1"
(expand "difference")
(("1"
(flatten)
(("1"
(inst - "i" "i+1")
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1"
(inst - "x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(expand "disjoint?")
(("2"
(expand "intersection")
(("2"
(expand "empty?")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(skosimp*)
(("2"
(expand "DS")
(("2"
(expand "difference")
(("2"
(expand "member")
(("2"
(case-replace "i=0")
(("1"
(flatten)
(("1"
(inst
-
"0"
"j!2")
(("1"
(assert)
(("1"
(inst
-6
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(inst
-
"i"
"j!2")
(("2"
(assert)
(("2"
(inst
-5
"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)
("2" (skosimp) (("2" (assert) nil nil)) nil))
nil))
nil)
((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(S formal-const-decl "sigma_algebra" finite_measure 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil finite_measure 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(subset_algebra_difference application-judgement "(S)"
finite_measure nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(disjoint? const-decl "bool" sets nil)
(disjoint_commutative formula-decl nil sets_lemmas_aux nil)
(trich_lt formula-decl nil real_props nil)
(subset_algebra_intersection application-judgement "(S)"
finite_measure nil)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(sigma_algebra_IUnion_rew application-judgement "(S)"
finite_measure nil)
(mu formal-const-decl "finite_measure" finite_measure nil)
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(series const-decl "sequence[real]" series "series/")
(sequence type-eq-decl nil sequences nil)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(DS skolem-const-decl "[nat -> (S)]" finite_measure nil)
(increasing? const-decl "bool" fun_preds_partial "structures/")
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas_aux nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(fm_emptyset formula-decl nil finite_measure nil)
(difference_subset2 formula-decl nil sets_lemmas nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(fm_difference formula-decl nil finite_measure nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
(extensionality_postulate formula-decl nil functions nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(sigma def-decl "real" sigma "reals/")
(O const-decl "T3" function_props nil)
(fm_convergence formula-decl nil finite_measure nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset const-decl "set" sets nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(FALSE const-decl "bool" booleans nil)
(disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(fm_IIntersection 0
(fm_IIntersection-1 nil 3321856529
("" (skosimp)
(("" (lemma "fm_IUnion" ("X" "IComplement(X!1)"))
(("1" (split -1)
(("1" (rewrite "IDemorgan2" -1 :dir rl)
(("1" (hide -2)
(("1" (rewrite "fm_complement")
(("1" (expand "convergence")
(("1" (skosimp*)
(("1" (inst - "epsilon!1")
(("1" (skosimp)
(("1" (inst + "n!1")
(("1" (skosimp)
(("1" (inst - "i!1")
(("1" (assert)
(("1"
(expand "IComplement")
(("1"
(expand "o")
(("1"
(rewrite "fm_complement")
(("1"
(assert)
(("1"
(lemma "abs_neg")
(("1"
(inst
-
"mu(IIntersection(X!1)) - mu(X!1(i!1))")
(("1" (assert) nil nil)
("2"
(lemma
"sigma_algebra_IIntersection"
("SS" "X!1"))
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sigma_algebra_IIntersection" ("SS" "X!1"))
(("2" (expand "member") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "decreasing?")
(("2" (expand "increasing?")
(("2" (expand "IComplement")
(("2" (expand "subset?")
(("2" (expand "complement")
(("2" (expand "member")
(("2" (skosimp*)
(("2" (inst - "x!1" "y!1")
(("2" (assert)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.77 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.
|
