| products/Sources/formale Sprachen/VDM/VDMRT/ChessWayRT/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: measure_props.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(sigma_algebra
(sigma_algebra_emptyset 0 (sigma_algebra_emptyset-1 nil 3313843435 ("" (typepred "S") (("" (expand "sigma_algebra?") (("" (expand "subset_algebra_empty?") (("" (flatten) nil nil)) nil)) nil)) nil) ((subset_algebra_empty? const-decl "bool" subset_algebra_def 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 sigma_algebra 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" sigma_algebra nil)) shostak)) (sigma_algebra_fullset 0 (sigma_algebra_fullset-1 nil 3313843485 ("" (typepred "S") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_empty?") (("" (expand "subset_algebra_complement?") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (subset_algebra_complement application-judgement "(S)" sigma_algebra nil) (subset_algebra_fullset name-judgement "(S)" sigma_algebra nil) (member const-decl "bool" sets nil) (subset_algebra_complement? const-decl "bool" subset_algebra_def 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 sigma_algebra 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" sigma_algebra nil)) shostak)) (sigma_algebra_complement 0 (sigma_algebra_complement-1 nil 3313843549 ("" (skosimp) (("" (expand "member") (("" (typepred "S") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_complement?") (("" (inst - "x!1") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset_algebra_complement application-judgement "(S)" sigma_algebra nil) (member const-decl "bool" sets nil)) shostak)) (sigma_algebra_union 0 (sigma_algebra_union-1 nil 3313843595 ("" (skosimp) (("" (expand "member") (("" (lemma "subset_algebra_union" ("x" "x!1" "y" "y!1")) (("" (propax) nil nil)) nil)) nil)) nil) ((subset_algebra_union application-judgement "(S)" sigma_algebra nil) (member const-decl "bool" sets nil)) shostak)) (sigma_algebra_intersection 0 (sigma_algebra_intersection-1 nil 3313843684 ("" (skosimp) (("" (lemma "sigma_algebra_complement" ("x" "x!1")) (("" (lemma "sigma_algebra_complement" ("x" "y!1")) (("" (expand "member") (("" (lemma "sigma_algebra_union" ("x" "complement(x!1)" "y" "complement(y!1)")) (("1" (expand "member") (("1" (lemma "sigma_algebra_complement" ("x" "union(complement(x!1), complement(y!1))")) (("1" (expand "member") (("1" (rewrite "demorgan1") (("1" (rewrite "complement_complement") (("1" (rewrite "complement_complement") nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" sigma_algebra 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 sigma_algebra nil) (sigma_algebra_complement formula-decl nil sigma_algebra nil) (subset_algebra_intersection application-judgement "(S)" sigma_algebra nil) (member const-decl "bool" sets nil)) shostak)) (sigma_algebra_difference 0 (sigma_algebra_difference-1 nil 3313843914 ("" (skosimp) (("" (typepred "x!1") (("" (typepred "y!1") (("" (rewrite "difference_intersection") (("" (lemma "sigma_algebra_complement" ("x" "y!1")) (("" (expand "member") (("" (lemma "sigma_algebra_intersection" ("x" "x!1" "y" "complement(y!1)")) (("1" (expand "member") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" sigma_algebra 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 sigma_algebra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (difference_intersection formula-decl nil sets_lemmas nil) (set type-eq-decl nil sets 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) (sigma_algebra_complement formula-decl nil sigma_algebra nil)) shostak)) (sigma_algebra_IUnion 0 (sigma_algebra_IUnion-1 nil 3314292445 ("" (skosimp) (("" (typepred "S") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "sigma_algebra_union?") (("" (inst - "image[nat,(S)](SS!1,fullset[nat])") (("" (split -3) (("1" (case-replace "Union(extend[setof[T], ((S)), bool, FALSE] (image[nat, (S)](SS!1, fullset[nat]))) = IUnion(SS!1)") (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "extend") (("1" (expand "Union") (("1" (expand "IUnion") (("1" (case-replace "EXISTS (i: nat): SS!1(i)(x!1)") (("1" (skosimp) (("1" (inst + "SS!1(i!1)") (("1" (inst + "i!1") nil nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (assert) (("2" (skosimp) (("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "countable_image[nat,set[T]]" ("S" "fullset[nat]" "f" "SS!1")) (("2" (split -1) (("1" (hide-all-but (-1 1)) (("1" (expand "extend") (("1" (expand "is_countable") (("1" (skosimp) (("1" (inst + "f!1") (("1" (split) (("1" (skosimp) (("1" (case-replace "image[nat, set[T]](SS!1)(fullset[nat])(x!1)") (("1" (assert) (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "image") (("1" (skosimp) (("1" (assert) (("1" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "image") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "injective?") (("2" (skosimp) (("2" (typepred "f!1") (("2" (expand "injective?") (("2" (inst - "x1!1" "x2!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "is_countable") (("2" (inst + "lambda (n:nat): n") (("2" (expand "restrict") (("2" (expand "injective?") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp) (("3" (typepred "x!1") (("3" (expand "fullset") (("3" (expand "image") (("3" (expand "extend") (("3" (expand "member") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" sigma_algebra 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 sigma_algebra nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend 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) (set type-eq-decl nil sets nil) (image const-decl "set[R]" function_image nil) (sequence type-eq-decl nil sequences nil) (fullset const-decl "set" sets nil) (member const-decl "bool" sets nil) (countable_image formula-decl nil countable_image "sets_aux/") (restrict const-decl "R" restrict nil) (is_countable const-decl "bool" countability "sets_aux/") (image const-decl "set[R]" function_image nil) (injective? const-decl "bool" functions nil) (f!1 skolem-const-decl "(injective?[(image(SS!1)(fullset[nat])), nat])" sigma_algebra nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Union const-decl "set" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (TRUE const-decl "bool" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (SS!1 skolem-const-decl "sequence[(S)]" sigma_algebra nil) (i!1 skolem-const-decl "nat" sigma_algebra nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sigma_algebra_union? const-decl "bool" subset_algebra_def nil)) shostak)) (sigma_algebra_IIntersection 0 (sigma_algebra_IIntersection-1 nil 3314294875 ("" (skosimp) (("" (case "IIntersection(SS!1) = complement(IUnion(lambda (n:nat): complement(SS!1(n) (("1" (lemma "sigma_algebra_IUnion" ("SS" "LAMBDA (n: nat): complement(SS!1(n))")) (("1" (lemma "sigma_algebra_complement" ("x" "IUnion(LAMBDA (n: nat): complement(SS!1(n)))")) (("1" (assert) nil nil) ("2" (expand "member") (("2" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (typepred "SS!1(n!1)") (("2" (lemma "sigma_algebra_complement" ("x" "SS!1(n!1)")) (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "IIntersection") (("2" (expand "complement") (("2" (expand "IUnion") (("2" (expand "member") (("2" (case-replace "(FORALL (i: nat): SS!1(i)(x!1))") (("1" (skosimp) (("1" (inst - "i!1") nil nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IUnion const-decl "set[T]" indexed_sets nil) (complement const-decl "set" sets nil) (sequence type-eq-decl nil sequences nil) (S formal-const-decl "sigma_algebra" sigma_algebra 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) (IIntersection const-decl "set[T]" indexed_sets 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) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil sigma_algebra nil) (subset_algebra_complement application-judgement "(S)" sigma_algebra nil) (sigma_algebra_complement formula-decl nil sigma_algebra nil) (member const-decl "bool" sets nil) (sigma_algebra_IUnion formula-decl nil sigma_algebra nil)) shostak)) (sigma_algebra_IUnion_rew 0 (sigma_algebra_IUnion_rew-1 nil 3322193116 ("" (lemma "sigma_algebra_IUnion") (("" (expand "member") (("" (propax) nil nil)) nil)) nil) ((member const-decl "bool" sets nil) (sigma_algebra_IUnion formula-decl nil sigma_algebra nil)) shostak)) (sigma_algebra_IIntersection_rew 0 (sigma_algebra_IIntersection_rew-1 nil 3322193117 ("" (lemma "sigma_algebra_IIntersection") (("" (expand "member") (("" (propax) nil nil)) nil)) nil) ((member const-decl "bool" sets nil) (sigma_algebra_IIntersection formula-decl nil sigma_algebra nil)) shostak))) ¤ Dauer der Verarbeitung: 0.10 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 |
