Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: measure_completion.prf Sprache: Lisp

Original von: PVS^©

(measure_completion
(generated_completion 0
  (generated_completion-1 nil 3423913628
   ("" (expand "sigma_algebra_completion")
    (("" (rewrite "generated_completion") nil nil)) nil)
   ((generated_completion formula-decl nil measure_completion_aux 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)
    (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" measure_completion 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)
    (m formal-const-decl "measure_type" measure_completion nil)
    (T formal-type-decl nil measure_completion nil)
    (sigma_algebra_completion const-decl "sigma_algebra[T]"
     measure_completion nil))
   shostak))
(completion_TCC1 0
  (completion_TCC1-1 nil 3458543748
   ("" (expand "completion")
    (("" (expand "almost_measurable?")
      (("" (inst + "emptyset[T]" "emptyset[T]" "emptyset[T]")
        (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil))
          nil)
         ("2" (expand "negligible_set?")
          (("2" (inst + "emptyset[T]")
            (("2" (expand "null_set?")
              (("2" (expand "measurable_set?")
                (("2" (expand "mu_fin?")
                  (("2" (expand "mu")
                    (("2" (typepred "m")
                      (("2" (expand "measure?")
                        (("2" (flatten)
                          (("2" (expand "measure_empty?")
                            (("2" (replace -1)
                              (("2"
                                (assert)
                                (("2"
                                  (expand "subset?")
                                  (("2" (skosimp) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((almost_measurable? const-decl "bool" measure_completion_aux nil)
    (difference const-decl "set" sets nil)
    (union const-decl "set" sets nil)
    (finite_difference application-judgement "finite_set[T]"
     countable_setofsets "sets_aux/")
    (countable_difference application-judgement "countable_set[T]"
     countable_setofsets "sets_aux/")
    (measurable_difference application-judgement "measurable_set[T, S]"
     measure_completion nil)
    (null_difference application-judgement "null_set[T, S, m]"
     measure_completion nil)
    (subset_algebra_difference application-judgement "(S)"
     measure_completion nil)
    (finite_union application-judgement "finite_set[T]"
     countable_setofsets "sets_aux/")
    (countable_union application-judgement "countable_set[T]"
     countable_setofsets "sets_aux/")
    (measurable_union application-judgement "measurable_set[T, S]"
     measure_completion nil)
    (member const-decl "bool" sets nil)
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (negligible_set? const-decl "bool" measure_theory nil)
    (m formal-const-decl "measure_type" measure_completion nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (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)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (S formal-const-decl "sigma_algebra" measure_completion 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 measure_completion nil)
    (completion const-decl "sigma_algebra[T]" measure_completion_aux
     nil)
    (subset_algebra_emptyset name-judgement "(S)" measure_completion
     nil)
    (null_emptyset name-judgement "null_set" measure_completion 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))
   nil))
(completion_measurable_TCC1 0
  (completion_measurable_TCC1-1 nil 3423913505
   ("" (skosimp)
    (("" (expand "completion")
      (("" (expand "almost_measurable?")
        (("" (inst + "X!1" "emptyset[T]" "emptyset[T]")
          (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil))
            nil)
           ("2" (lemma "null_is_negligible")
            (("2" (lemma "null_emptyset")
              (("2" (inst - "emptyset[T]") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((completion const-decl "sigma_algebra[T]" measure_completion_aux
     nil)
    (subset_algebra_emptyset name-judgement "(S)" measure_completion
     nil)
    (null_emptyset name-judgement "null_set" measure_completion 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)
    (T formal-type-decl nil measure_completion 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)
    (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" measure_completion nil)
    (set type-eq-decl nil sets 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)
    (m formal-const-decl "measure_type" measure_completion nil)
    (negligible_set? const-decl "bool" measure_theory nil)
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (emptyset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (subset_algebra_union application-judgement "(S)"
     measure_completion nil)
    (subset_algebra_difference application-judgement "(S)"
     measure_completion nil)
    (union const-decl "set" sets nil)
    (difference const-decl "set" sets nil)
    (almost_measurable? const-decl "bool" measure_completion_aux nil))
   nil))
(completion_measurable 0
  (completion_measurable-1 nil 3423913655
   ("" (skosimp)
    (("" (expand "completion")
      (("" (rewrite "completion_measurable") nil nil)) nil))
    nil)
   ((completion const-decl "complete_measure[T, completion(S, m)]"
     measure_completion nil)
    (T formal-type-decl nil measure_completion nil)
    (m formal-const-decl "measure_type" measure_completion nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (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" measure_completion 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)
    (completion_measurable formula-decl nil measure_completion_aux
     nil))
   shostak))
(completion_negligible_TCC1 0
  (completion_negligible_TCC1-1 nil 3423913505
   ("" (skosimp)
    (("" (expand "completion")
      (("" (expand "almost_measurable?")
        (("" (inst + "emptyset[T]" "N!1" "emptyset[T]")
          (("1" (apply-extensionality :hide? t) (("1" (grind) nil nil))
            nil)
           ("2" (lemma "null_emptyset")
            (("2" (lemma "null_is_negligible")
              (("2" (inst - "emptyset[T]") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((completion const-decl "sigma_algebra[T]" measure_completion_aux
     nil)
    (subset_algebra_emptyset name-judgement "(S)" measure_completion
     nil)
    (null_emptyset name-judgement "null_set" measure_completion 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)
    (T formal-type-decl nil measure_completion 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)
    (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" measure_completion nil)
    (set type-eq-decl nil sets nil)
    (emptyset const-decl "set" sets 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)
    (m formal-const-decl "measure_type" measure_completion nil)
    (negligible_set? const-decl "bool" measure_theory nil)
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (member const-decl "bool" sets nil)
    (negligible_union application-judgement "negligible"
     measure_completion nil)
    (union const-decl "set" sets nil)
    (difference const-decl "set" sets nil)
    (almost_measurable? const-decl "bool" measure_completion_aux nil))
   nil))
(completion_negligible 0
  (completion_negligible-1 nil 3423913703
   ("" (skosimp)
    (("" (expand "completion")
      (("" (rewrite "completion_negligible") nil nil)) nil))
    nil)
   ((completion const-decl "complete_measure[T, completion(S, m)]"
     measure_completion nil)
    (T formal-type-decl nil measure_completion nil)
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (negligible_set? const-decl "bool" measure_theory nil)
    (set type-eq-decl nil sets nil)
    (m formal-const-decl "measure_type" measure_completion nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (measure? const-decl "bool" generalized_measure_def nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (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" measure_completion 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)
    (completion_negligible formula-decl nil measure_completion_aux
     nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.