| products/sources/formale sprachen/PVS/measure_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: monotone_classes.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(monotone_classes
(monotone_finite_measures_TCC1 0 (monotone_finite_measures_TCC1-1 nil 3453992461 ("" (skosimp) (("" (skolem + "a!1") (("" (typepred "a!1") (("" (lemma "generated_sigma_algebra_subset1" ("X" "C")) (("" (expand "subset?") (("" (inst - "a!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (generated_sigma_algebra_subset1 formula-decl nil subset_algebra_def nil) (subset_algebra_complement application-judgement "(S)" sigma_algebra nil) (subset_algebra_intersection application-judgement "(S)" sigma_algebra nil) (member const-decl "bool" sets nil) (subset? 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 monotone_classes nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (C formal-const-decl "(nonempty?[set[T]])" monotone_classes nil)) nil)) (monotone_finite_measures 0 (monotone_finite_measures-2 nil 3454001130 ("" (skosimp) (("" (name "S" "generated_sigma_algebra(C)") (("" (name "TT" "{E:(S) | mu!1(E)=nu!1(E)}") (("1" (case "forall (x:set[T]): S(x) => TT(x)") (("1" (skosimp) (("1" (typepred "x!1") (("1" (inst - "x!1") (("1" (expand "S") (("1" (expand "TT") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (case "generated_sigma_algebra(generated_subset_algebra(C))=S") (("1" (lemma "monotone_class[T]" ("B" "generated_subset_algebra[T](C)" "C" "{x:set[T] | S(x) & mu!1(x) = nu!1(x)}")) (("1" (replace -2 -1) (("1" (split) (("1" (expand "subset?") (("1" (inst - "x!1") (("1" (expand "member") (("1" (assert) (("1" (expand "TT") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (lemma "disjoint_algebra_construction" ("NX" "C")) (("2" (replace -7) (("2" (expand "member") (("2" (lemma "generated_sigma_algebra_subset1[T]" ("X" "generated_subset_algebra(C)")) (("2" (expand "subset?" -1) (("2" (inst - "x!2") (("2" (expand "member") (("2" (assert) (("2" (replace -2 -3) (("2" (hide-all-but (-3 -9 1)) (("2" (expand "finite_disjoint_unions") (("2" (expand "fullset") (("2" (expand "extend") (("2" (prop) (("2" (expand "finite_disjoint_union?") (("2" (skosimp) (("2" (expand "member") (("2" (typepred "mu!1") (("2" (typepred "nu!1") (("2" (expand "finite_measure?") (("2" (flatten) (("2" (case "disjoint_indexed_measurable?[T, (generated_sigma_algebra(C))](E!1)") (("1" (inst - "E!1") (("1" (inst - "E!1") (("1" (replace -7 * rl) (("1" (hide -1 -6 -7) (("1" (lemma "zero_tail_series_limit" ("n" "n!1" "a" "nu!1 o E!1")) (("1" (split) (("1" (lemma "zero_tail_series_limit" ("n" "n!1" "a" "mu!1 o E!1")) (("1" (split) (("1" (rewrite "convergence_sequences.limit_def" -4 :dir rl) (("1" (rewrite "convergence_sequences.limit_def" -6 :dir rl) (("1" (replace -1) (("1" (replace -2) (("1" (replace -4 * rl) (("1" (replace -6 * rl) (("1" (hide -1 -2 -4 -6) (("1" (expand "o ") (("1" (expand "series") (("1" (lemma "sigma_eq" ("low" "0" "high" "n!1" "F" "LAMBDA (x: nat): mu!1(E!1(x))" "G" "LAMBDA (x: nat): nu!1(E!1(x))")) (("1" (assert) (("1" (hide 2) (("1" (skosimp) (("1" (inst -3 "n!2") (("1" (flatten) (("1" (assert) (("1" (typepred "n!2") (("1" (expand "<=" -2) (("1" (split) (("1" (assert) (("1" (inst -7 "E!1(n!2)") 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)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "o ") (("2" (inst -7 "m!1") (("2" (flatten) (("2" (assert) (("2" (rewrite "emptyset_is_empty?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "o ") (("2" (inst -6 "m!1") (("2" (flatten) (("2" (assert) (("2" (rewrite "emptyset_is_empty?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 2) (("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil) ("3" (hide -1 -2 -3 -4 -6 2 -8) (("3" (skolem + "n!2") (("3" (inst - "n!2") (("3" (flatten) (("3" (case-replace "n!2 (("1" (lemma "generated_sigma_algebra_subset1[T]" ("X" "C")) (("1" (expand "subset?") (("1" (inst - "E!1(n!2)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "emptyset_is_empty?") (("2" (typepred "generated_sigma_algebra[T](C)") (("2" (expand "sigma_algebra?") (("2" (flatten) (("2" (expand "subset_algebra_empty?") (("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) ("2" (hide 2 -3) (("2" (expand "monotone?") (("2" (skosimp) (("2" (expand "member") (("2" (lemma "sigma_algebra_IUnion[T,S]" ("SS" "E!1")) (("1" (lemma "sigma_algebra_IIntersection[T,S]" ("SS" "E!1")) (("1" (expand "member") (("1" (replace -1) (("1" (replace -2) (("1" (split) (("1" (flatten) (("1" (lemma "m_increasing_convergence[T,S,to_measure(mu!1)]" ("E" "E!1")) (("1" (assert) (("1" (lemma "m_increasing_convergence[T,S,to_measure(nu!1)]" ("E" "E!1")) (("1" (assert) (("1" (expand "to_measure") (("1" (name-replace "MU" "mu!1(IUnion(E!1))") (("1" (name-replace "NU" "nu!1(IUnion(E!1))") (("1" (expand "o ") (("1" (expand "x_converges?") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))") (("1" (lemma "convergence_sequences.limit_lemma" ("v" "LAMBDA (i: nat): nu!1(E!1(i))")) (("1" (lemma "convergence_sequences.limit_lemma" ("v" "LAMBDA (i: nat): mu!1(E!1(i))")) (("1" (replace -5 * rl) (("1" (replace -6 * rl) (("1" (lemma "cnv_seq_diff" ("s1" "LAMBDA (i: nat): mu!1(E!1(i))" "l1" "MU" "s2" "LAMBDA (i: nat): nu!1(E!1(i))" "l2" "NU")) (("1" (assert) (("1" (lemma "cnv_seq_const" ("a" "0")) (("1" (expand "const_fun") (("1" (expand "-" -2) (("1" (case-replace "(LAMBDA (x: nat): mu!1(E!1(x)) - nu!1(E!1(x)))=(LAMBDA (x: nat): 0)") (("1" (lemma "convergence_sequences.unique_limit" ("u" "LAMBDA (x: nat): 0" "l1" "0" "l2" "MU-NU")) (("1" (assert) nil nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (inst -12 "x!2") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -12 "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil) ("3" (skosimp) (("3" (assert) (("3" (inst -8 "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst -7 "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst -6 "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (assert) (("1" (replace -8) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -9)) (("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](nu!1)") (("2" (expand "measure?") (("2" (expand "to_measure") (("2" (expand "measure_empty?") (("2" (flatten) (("2" (assert) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "o ") (("2" (inst - "X!1") (("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem + "n!1") (("2" (expand "measurable_set?") (("2" (inst - "n!1") (("2" (flatten) nil nil)) nil)) nil)) nil) ("3" (split) (("1" (skosimp) (("1" (replace -7) (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](mu!1)") (("2" (hide-all-but (-1 1 -8)) (("2" (expand "measure?") (("2" (flatten) (("2" (expand "measure_empty?") (("2" (expand "to_measure") (("2" (assert) (("2" (hide -1) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (inst - "X!1") (("1" (expand "o ") (("1" (propax) nil nil)) nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.38 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.Bot Zugriff |
