| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 5 kB |
|
Quelle hahn_kolmogorov.prf Sprache: Lisp |
|||||||||
|
(hahn_kolmogorov
(IMP_outer_measure_props_TCC1 0 (IMP_outer_measure_props_TCC1-1 nil 3458543731 ("" (typepred "A") (("" (expand "subset_algebra?") (("" (flatten) (("" (expand "subset_algebra_empty?") (("" (expand "nonempty?") (("" (expand "empty?") (("" (inst - "emptyset[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (empty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (emptyset const-decl "set" sets nil) (nonempty? 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) (T formal-type-decl nil hahn_kolmogorov 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) (A formal-const-decl "subset_algebra" hahn_kolmogorov nil)) nil)) (algebra_in_induced_sigma_algebra 0 (algebra_in_induced_sigma_algebra-1 nil 3453612437 ("" (expand "subset?") (("" (skolem + "E!1") (("" (expand "member") (("" (flatten) (("" (expand "induced_sigma_algebra") (("" (rewrite "outer_measurable_def") (("" (skolem + ("A!1")) (("" (rewrite "epsilon_x_le") (("1" (skosimp) (("1" (expand "x_le") (("1" (flatten) (("1" (name "LHS" "x_add(ast(mu)(intersection(A!1, E!1)), ast(mu)(intersection(A!1, complement(E!1))))") (("1" (replace -1) (("1" (replace -3) (("1" (expand "x_add" (-3 1)) (("1" (case-replace "ast(mu)(A!1)`1") (("1" (lemma "outer_measure_def" ("mu" "mu" "epsilon" "epsilon!1" "X" "A!1")) (("1" (expand "x_add" -1) (("1" (replace -2) (("1" (skosimp*) (("1" (name "E1" "lambda (n:nat): intersection(I!1(n),E!1)") (("1" (name "E2" "lambda (n:nat): intersection(I!1(n),complement(E!1))") (("1" (hide -1 -2) (("1" (case "forall (n:nat): I!1(n) = union(E1(n),E2(n)) & A(E1(n)) & A(E2(n))") (("1" (case "subset?(intersection(A!1,E!1),IUnion(E1))") (("1" (case "subset?(intersection(A!1,complement(E!1)),IUnion(E2))") (("1" (typepred "ast(mu)") (("1" (expand "outer_measure?") (("1" (flatten) (("1" (expand "om_increasing?") (("1" (inst-cp - "intersection(A!1, complement(E!1))" "IUnion(E2)") (("1" (inst-cp - "intersection(A!1,E!1)" "IUnion(E1)") (("1" (assert) (("1" (expand "om_countably_subadditive?") (("1" (inst-cp - "E2") (("1" (inst - "E1") (("1" (lemma "x_sum_eq" ("S" "ast(mu) o E2" "T" "mu o E2")) (("1" (split) (("1" (lemma "x_sum_eq" ("S" "ast(mu) o E1" "T" "mu o E1")) (("1" (split) (("1" (lemma "x_le_add" ("x1" "ast(mu)(intersection(A!1, E!1))" "y1" "x_sum(mu o E1)" "x2" "ast(mu)(intersection(A!1, complement(E!1)))" "y2" "x_sum(mu o E2)")) (("1" (replace -16) (("1" (split -1) (("1" (lemma "x_add_sum" ("S" "mu o E1" "T" "mu o E2")) (("1" (case "x_le(LHS,x_sum(LAMBDA (i:nat): x_add((mu o E1)(i), (mu o E2)(i))))") (("1" (lemma "x_sum_le" ("S" "(LAMBDA (i: nat): x_add((mu o E1)(i), (mu o E2)(i)))" "T" "mu o I!1")) (("1" (split -1) (("1" (name-replace "DRL1" "x_add(x_sum(mu o E1), x_sum(mu o E2))") (("1" (name-replace "DRL2" "x_sum(LAMBDA (i:nat): x_add((mu o E1)(i), (mu o E2)(i)))") (("1" (name-replace "DRL3" "x_sum(mu o I!1)") (("1" (hide-all-but (-1 -2 -17 1)) (("1" (name-replace "DRL4" "ast(mu)(A!1)`2") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "o ") (("2" (hide-all-but (-19 1 -14)) (("2" (inst - "i!1") (("2" (flatten) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "measure_disjoint_union[T,A]" ("f" "mu" "a" "E1(i!1)" "b" "E2(i!1)")) (("2" (assert) (("2" (split) (("1" (expand "x_eq") (("1" (expand "x_le") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "E1") (("2" (expand "E2") (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "subset_algebra_union") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (name-replace "DRL2" "x_add(x_sum(mu o E1), x_sum(mu o E2))") (("2" (name-replace "RHS" "x_sum(LAMBDA (i: nat): x_add((mu o E1)(i), (mu o E2)(i)))") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (name-replace "DRL1" "ast(mu)(intersection(A!1, E!1))") (("2" (name-replace "DRL2" "ast(mu)(IUnion(E1))") (("2" (name-replace "DRL3" "x_sum(ast(mu) o E1)") (("2" (name-replace "DRL4" "x_sum(mu o E1)") (("2" (hide-all-but (1 -1 -5 -7)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (name-replace "DRL1" "ast(mu)(intersection(A!1, complement(E!1)))") (("3" (name-replace "DRL2" "ast(mu)(IUnion(E2))") (("3" (name-replace "DRL3" "x_sum(ast(mu) o E2)") (("3" (name-replace "DRL4" "x_sum(mu o E2)") (("3" (hide-all-but (1 -2 -6 -8)) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "o ") (("2" (skosimp) (("2" (inst -10 "i!1") (("2" (rewrite "outer_measure_eq" 1) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -10 "x1!1") (("2" (flatten) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "o ") (("2" (inst -9 "i!1") (("2" (flatten) (("2" (rewrite "outer_measure_eq" 1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst -9 "x1!1") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "subset?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "E2") (("2" (expand "intersection") (("2" (expand "member") (("2" (flatten) (("2" (assert) (("2" (expand "IUnion") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "E1") (("2" (expand "subset?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "member") (("2" (expand "intersection") (("2" (expand "member") (("2" (flatten) (("2" (assert) (("2" (expand "IUnion") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -5)) (("2" (skosimp) (("2" (split) (("1" (expand "E1") (("1" (expand "E2") (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "E1") (("2" (typepred "I!1(n!1)") (("2" (rewrite "subset_algebra_intersection") nil nil)) nil)) nil) ("3" (expand "E2") (("3" (rewrite "subset_algebra_intersection") (("3" (rewrite "subset_algebra_complement") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "E!1") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "E!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((outer_measurable_def formula-decl nil outer_measure_props nil) (T formal-type-decl nil hahn_kolmogorov 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) (A formal-const-decl "subset_algebra" hahn_kolmogorov 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) (set type-eq-decl nil sets nil) (outer_measure? const-decl "bool" outer_measure_def nil) (outer_measure nonempty-type-eq-decl nil outer_measure_def nil) (ast const-decl "outer_measure" ast_def nil) (mu formal-const-decl "measure_type" hahn_kolmogorov nil) (nonempty? const-decl "bool" sets nil) (epsilon_x_le formula-decl nil extended_nnreal "extended_nnreal/") (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (intersection const-decl "set" sets nil) (complement const-decl "set" sets nil) (x_le const-decl "bool" extended_nnreal "extended_nnreal/") (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (union const-decl "set" sets nil) (om_increasing? const-decl "bool" outer_measure_def nil) (om_countably_subadditive? const-decl "bool" outer_measure_def nil) (x_add_sum formula-decl nil extended_nnreal "extended_nnreal/") (x_sum_le formula-decl nil extended_nnreal "extended_nnreal/") (measure_disjoint_union formula-decl nil generalized_measure_def nil) (x_eq const-decl "bool" extended_nnreal "extended_nnreal/") (E1 skolem-const-decl "[nat -> set[T]]" hahn_kolmogorov nil) (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (E2 skolem-const-decl "[nat -> set[T]]" hahn_kolmogorov nil) (subset_algebra_union judgement-tcc nil subset_algebra nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_sum const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (x_le_add formula-decl nil extended_nnreal "extended_nnreal/") (outer_measure_eq formula-decl nil ast_def nil) (O const-decl "T3" function_props nil) (x_sum_eq formula-decl nil extended_nnreal "extended_nnreal/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (IUnion const-decl "set[T]" indexed_sets nil) (subset_algebra_complement judgement-tcc nil subset_algebra nil) (subset_algebra_intersection judgement-tcc nil subset_algebra nil) (sequence type-eq-decl nil sequences 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) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (outer_measure_def formula-decl nil ast_def nil) (x_add const-decl "extended_nnreal" extended_nnreal "extended_nnreal/") (induced_sigma_algebra const-decl "sigma_algebra[T]" outer_measure_props nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) shostak)) (IMP_measure_theory_TCC1 0 (IMP_measure_theory_TCC1-1 nil 3453445044 ("" (typepred "induced_measure[T, ast(mu)]") (("1" (expand "complete_measure?") (("1" (flatten) nil nil)) nil) ("2" (typepred "A") (("2" (expand "subset_algebra?") (("2" (expand "nonempty?") (("2" (expand "subset_algebra_empty?") (("2" (flatten) (("2" (expand "empty?") (("2" (inst - "emptyset[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((emptyset const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (nonempty? 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) (T formal-type-decl nil hahn_kolmogorov 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) (subset_algebra? const-decl "bool" subset_algebra_def nil) (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (A formal-const-decl "subset_algebra" hahn_kolmogorov 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) (set type-eq-decl nil sets nil) (outer_measure? const-decl "bool" outer_measure_def nil) (outer_measure nonempty-type-eq-decl nil outer_measure_def nil) (ast const-decl "outer_measure" ast_def nil) (mu formal-const-decl "measure_type" hahn_kolmogorov nil) (induced_sigma_algebra const-decl "sigma_algebra[T]" outer_measure_props nil) (complete_measure? const-decl "bool" generalized_measure_def nil) (complete_measure nonempty-type-eq-decl nil generalized_measure_def nil) (induced_measure const-decl "complete_measure" outer_measure_props nil)) nil)) (induced_measure_measure_TCC1 0 (induced_measure_measure_TCC1-1 nil 3453445345 ("" (skosimp) (("" (lemma "algebra_in_induced_sigma_algebra") (("" (expand "subset?") (("" (inst - "x!1") (("" (expand "induced_sigma_algebra") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((algebra_in_induced_sigma_algebra formula-decl nil hahn_kolmogorov nil) (T formal-type-decl nil hahn_kolmogorov 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) (A formal-const-decl "subset_algebra" hahn_kolmogorov nil) (member const-decl "bool" sets nil) (induced_sigma_algebra const-decl "sigma_algebra[T]" outer_measure_props nil) (subset? const-decl "bool" sets nil)) nil)) (induced_measure_measure 0 (induced_measure_measure-1 nil 3453445345 ("" (skosimp) (("" (rewrite "induced_measure_rew") (("1" (rewrite "outer_measure_eq") nil nil) ("2" (typepred "x!1") (("2" (typepred "A") (("2" (hide 2) (("2" (lemma "algebra_in_induced_sigma_algebra") (("2" (expand "subset?") (("2" (inst - "x!1") (("2" (assert) (("2" (expand "induced_sigma_algebra") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((induced_measure_rew formula-decl nil outer_measure_props nil) (outer_measurable? const-decl "bool" outer_measure_props nil) (outer_measurable nonempty-type-eq-decl nil outer_measure_props nil) (T formal-type-decl nil hahn_kolmogorov 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) (A formal-const-decl "subset_algebra" hahn_kolmogorov 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) (set type-eq-decl nil sets nil) (outer_measure? const-decl "bool" outer_measure_def nil) (outer_measure nonempty-type-eq-decl nil outer_measure_def nil) (ast const-decl "outer_measure" ast_def nil) (mu formal-const-decl "measure_type" hahn_kolmogorov nil) (outer_measure_eq formula-decl nil ast_def nil) (algebra_in_induced_sigma_algebra formula-decl nil hahn_kolmogorov nil) (induced_sigma_algebra const-decl "sigma_algebra[T]" outer_measure_props nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak))) ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28