Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: complex_measure_theory.prf Sprache: Lisp

Original von: PVS^©

(complex_measure_theory
(mu_TCC1 0
  (mu_TCC1-1 nil 3477286160
   ("" (typepred "S")
    (("" (expand "sigma_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (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/")
    (member 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 complex_measure_theory nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" complex_measure_theory
     nil))
   nil))
(cal_N_TCC1 0
  (cal_N_TCC1-1 nil 3477287562
   ("" (expand "cal_N?")
    (("" (split)
      (("1" (expand "ae_0?")
        (("1" (expand "pointwise_ae?")
          (("1" (expand "ae?")
            (("1" (expand "fullset")
              (("1" (expand "ae_in?")
                (("1" (inst + "emptyset")
                  (("1" (skosimp)
                    (("1" (expand "member") (("1" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (rewrite "const_measurable") nil nil))
      nil))
    nil)
   ((pointwise_ae? const-decl "bool" complex_measure_theory nil)
    (fullset const-decl "set" sets nil)
    (null_emptyset name-judgement "null_set[T, S, mu]"
     complex_measure_theory nil)
    (subset_algebra_emptyset name-judgement "(S)"
     complex_measure_theory 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 complex_measure_theory 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
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" complex_measure_theory 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
     "measure_integration/")
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (mu formal-const-decl "measure_type[T, S]" complex_measure_theory
     nil)
    (negligible_set? const-decl "bool" measure_theory
     "measure_integration/")
    (negligible nonempty-type-eq-decl nil measure_theory
     "measure_integration/")
    (emptyset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (c_eq1 formula-decl nil complex_types "complex_alt/")
    (ae_in? const-decl "bool" measure_theory "measure_integration/")
    (ae? const-decl "bool" measure_theory "measure_integration/")
    (measurable_fullset name-judgement "measurable_set[T, S]"
     complex_measure_theory nil)
    (subset_algebra_fullset name-judgement "(S)" complex_measure_theory
     nil)
    (ae_0? const-decl "bool" complex_measure_theory nil)
    (complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
     complex_types "complex_alt/")
    (complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
     "complex_alt/")
    (complex type-decl nil complex_types "complex_alt/")
    (const_measurable formula-decl nil complex_measurable nil)
    (cal_N? const-decl "bool" complex_measure_theory nil))
   nil))
(cal_N_is_measurable 0
  (cal_N_is_measurable-1 nil 3477464784
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "cal_N?") (("" (flatten) nil nil)) nil)) nil))
    nil)
   ((cal_N nonempty-type-eq-decl nil complex_measure_theory nil)
    (cal_N? const-decl "bool" complex_measure_theory nil)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil complex_measure_theory nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(cal_N_def 0
  (cal_N_def-1 nil 3477464873
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (expand "cal_N?")
          (("1" (flatten)
            (("1" (expand "complex_measurable?")
              (("1" (flatten)
                (("1" (replace -2)
                  (("1" (replace -3)
                    (("1" (hide -2 -3)
                      (("1" (expand "ae_0?")
                        (("1" (expand "restrict")
                          (("1" (expand "pointwise_ae?")
                            (("1" (expand "ae?")
                              (("1"
                                (expand "fullset")
                                (("1"
                                  (expand "ae_in?")
                                  (("1"
                                    (skosimp)
                                    (("1"
                                      (expand "member")
                                      (("1"
                                        (split)
                                        (("1"
                                          (inst + "E!1")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (inst - "x!1")
                                              (("1"
                                                (expand "Re")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (inst + "E!1")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (inst - "x!1")
                                              (("2"
                                                (expand "Im")
                                                (("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)
       ("2" (expand "cal_N?")
        (("2" (expand "complex_measurable?")
          (("2" (flatten)
            (("2" (assert)
              (("2" (hide -2 -4)
                (("2" (expand "ae_0?")
                  (("2" (expand "restrict")
                    (("2" (expand "pointwise_ae?")
                      (("2" (expand "ae?")
                        (("2" (expand "fullset")
                          (("2" (expand "ae_in?")
                            (("2" (skosimp*)
                              (("2"
                                (inst + "union(E!1,E!2)")
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (expand "union")
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (inst - "x!1")
                                          (("2"
                                            (inst - "x!1")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (expand "Re" -1)
                                                  (("2"
                                                    (expand "Im" -)
                                                    (("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)
   ((cal_N? const-decl "bool" complex_measure_theory nil)
    (complex_measurable? const-decl "bool" complex_measurable nil)
    (restrict const-decl "R" restrict nil)
    (subset_algebra_fullset name-judgement "(S)" complex_measure_theory
     nil)
    (measurable_fullset name-judgement "measurable_set[T, S]"
     complex_measure_theory nil)
    (ae? const-decl "bool" measure_theory "measure_integration/")
    (ae_in? const-decl "bool" measure_theory "measure_integration/")
    (member const-decl "bool" sets nil)
    (Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
    (T formal-type-decl nil complex_measure_theory 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
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" complex_measure_theory 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
     "measure_integration/")
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (mu formal-const-decl "measure_type[T, S]" complex_measure_theory
     nil)
    (negligible_set? const-decl "bool" measure_theory
     "measure_integration/")
    (negligible nonempty-type-eq-decl nil measure_theory
     "measure_integration/")
    (TRUE const-decl "bool" booleans nil)
    (Re_rew formula-decl nil complex_types "complex_alt/")
    (Im_rew formula-decl nil complex_types "complex_alt/")
    (c_eq1 formula-decl nil complex_types "complex_alt/")
    (Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
    (fullset const-decl "set" sets nil)
    (pointwise_ae? const-decl "bool" complex_measure_theory nil)
    (pointwise_ae? const-decl "bool" measure_theory
     "measure_integration/")
    (ae_0? const-decl "bool" complex_measure_theory nil)
    (ae_0? const-decl "bool" measure_theory "measure_integration/")
    (Re_fun_rew formula-decl nil complex_fun_ops "complex_alt/")
    (Im_fun_rew formula-decl nil complex_fun_ops "complex_alt/")
    (union const-decl "set" sets nil)
    (negligible_union application-judgement "negligible[T, S, mu]"
     complex_measure_theory nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.7 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.