products/Sources/formale Sprachen/PVS/measure_integration/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: finite_fubini_tonelli.prf   Sprache: Lisp

Original von: PVS©
(finite_fubini_tonelli
 (mu_TCC1 0
  (mu_TCC1-1 nil 3458551591
   ("" (typepred "S1")
    (("" (expand "sigma_algebra?")
      (("" (expand "subset_algebra_empty?")
        (("" (flatten)
          (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets 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)
    (T1 formal-type-decl nil finite_fubini_tonelli 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)
    (S1 formal-const-decl "sigma_algebra[T1]" finite_fubini_tonelli
     nil))
   nil))
 (nu_TCC1 0
  (nu_TCC1-1 nil 3458551591
   ("" (typepred "S2")
    (("" (expand "sigma_algebra?")
      (("" (expand "subset_algebra_empty?")
        (("" (flatten)
          (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets 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)
    (T2 formal-type-decl nil finite_fubini_tonelli 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)
    (S2 formal-const-decl "sigma_algebra[T2]" finite_fubini_tonelli
     nil))
   nil))
 (finite_fubini_tonelli_1 0
  (finite_fubini_tonelli_1-1 nil 3458552933
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (typepred "h!1")
          (("1" (expand "nn_measurable?")
            (("1" (flatten)
              (("1"
                (lemma "nn_integrable_is_nn_integrable" ("f" "h!1"))
                (("1" (split)
                  (("1" (hide -4)
                    (("1" (lemma "nn_integral_def" ("f" "h!1"))
                      (("1" (skolem - "HH")
                        (("1" (flatten)
                          (("1" (typepred "HH")
                            (("1" (case "FORALL (n: nat): isf?(HH(n))")
                              (("1"
                                (case
                                 "FORALL (n: nat,z:[T1,T2]): HH(n)(z)>=0")
                                (("1"
                                  (name
                                   "FF"
                                   "lambda (n:nat): lambda (x:T1): isf_integral(lambda (y:T2): HH(n)(x,y))")
                                  (("1"
                                    (case
                                     "FORALL (n: nat): integrable?[T1, S1, to_measure(mu)](FF(n))")
                                    (("1"
                                      (case
                                       "forall (n:nat): integral[T1,S1,to_measure(mu)](FF(n))=integral[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))](HH(n))")
                                      (("1"
                                        (case-replace
                                         "(isf_integral o HH)=integral o FF")
                                        (("1"
                                          (case
                                           "forall (n:nat,x:T1): FF(n)(x)>=0")
                                          (("1"
                                            (case
                                             "pointwise_increasing?(FF)")
                                            (("1"
                                              (case
                                               "bounded?(integral o FF)")
                                              (("1"
                                                (lemma
                                                 "monotone_convergence[T1, S1, to_measure(mu)]"
                                                 ("F" "FF"))
                                                (("1"
                                                  (split -1)
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (hide -1)
                                                      (("1"
                                                        (split -1)
                                                        (("1"
                                                          (skolem
                                                           -
                                                           "F")
                                                          (("1"
                                                            (inst
                                                             -
                                                             "F")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (typepred
                                                                 "F")
                                                                (("1"
                                                                  (expand
                                                                   "integrable1?")
                                                                  (("1"
                                                                    (expand
                                                                     "ae_convergence?")
                                                                    (("1"
                                                                      (expand
                                                                       "fullset")
                                                                      (("1"
                                                                        (expand
                                                                         "ae_convergence_in?")
                                                                        (("1"
                                                                          (expand
                                                                           "ae_in?")
                                                                          (("1"
                                                                            (skosimp)
                                                                            (("1"
                                                                              (expand
                                                                               "member")
                                                                              (("1"
                                                                                (typepred
                                                                                 "E!1")
                                                                                (("1"
                                                                                  (expand
                                                                                   "negligible_set?")
                                                                                  (("1"
                                                                                    (skolem
                                                                                     -
                                                                                     "N1")
                                                                                    (("1"
                                                                                      (flatten)
                                                                                      (("1"
                                                                                        (inst
                                                                                         +
                                                                                         "N1"
                                                                                         "F")
                                                                                        (("1"
                                                                                          (skosimp)
                                                                                          (("1"
                                                                                            (expand
                                                                                             "subset?")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "x!1")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "member")
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   -
                                                                                                   "x!1")
                                                                                                  (("1"
                                                                                                    (assert)
                                                                                                    (("1"
                                                                                                      (lemma
                                                                                                       "monotone_convergence_scaf[T2,S2,to_measure(nu)]"
                                                                                                       ("f"
                                                                                                        "LAMBDA (y: T2): h!1(x!1, y)"
                                                                                                        "F"
                                                                                                        "lambda (n:nat): lambda (y:T2): HH(n)(x!1,y)"))
                                                                                                      (("1"
                                                                                                        (split
                                                                                                         -1)
                                                                                                        (("1"
                                                                                                          (flatten)
                                                                                                          (("1"
                                                                                                            (replace
                                                                                                             -1)
                                                                                                            (("1"
                                                                                                              (name-replace
                                                                                                               "LHS"
                                                                                                               "integral(LAMBDA (y: T2): h!1(x!1, y))")
                                                                                                              (("1"
                                                                                                                (case-replace
                                                                                                                 "(integral o
                        (LAMBDA (n: nat): LAMBDA (y: T2): HH(n)(x!1, y)))=LAMBDA (n:nat): FF(n)(x!1)")
                                                                                                                (("1"
                                                                                                                  (expand
                                                                                                                   "converges_upto?")
                                                                                                                  (("1"
                                                                                                                    (flatten)
                                                                                                                    (("1"
                                                                                                                      (hide-all-but
                                                                                                                       (-3
                                                                                                                        -7
                                                                                                                        3))
                                                                                                                      (("1"
                                                                                                                        (lemma
                                                                                                                         "hausdorff_convergence.unique_limit"
                                                                                                                         ("u"
                                                                                                                          "LAMBDA (n: nat): FF(n)(x!1)"
                                                                                                                          "l1"
                                                                                                                          "LHS"
                                                                                                                          "l2"
                                                                                                                          "F(x!1)"))
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("2"
                                                                                                                  (apply-extensionality
                                                                                                                   :hide?
                                                                                                                   t)
                                                                                                                  (("1"
                                                                                                                    (expand
                                                                                                                     "FF"
                                                                                                                     1)
                                                                                                                    (("1"
                                                                                                                      (expand
                                                                                                                       "o"
                                                                                                                       1)
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -15
                                                                                                                         "x!2")
                                                                                                                        (("1"
                                                                                                                          (lemma
                                                                                                                           "isf_x_section"
                                                                                                                           ("x"
                                                                                                                            "x!1"
                                                                                                                            "i"
                                                                                                                            "HH(x!2)"))
                                                                                                                          (("1"
                                                                                                                            (rewrite
                                                                                                                             "isf_integral"
                                                                                                                             1)
                                                                                                                            nil
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("2"
                                                                                                                    (skosimp)
                                                                                                                    (("2"
                                                                                                                      (inst
                                                                                                                       -15
                                                                                                                       "n!1")
                                                                                                                      (("2"
                                                                                                                        (lemma
                                                                                                                         "isf_x_section"
                                                                                                                         ("x"
                                                                                                                          "x!1"
                                                                                                                          "i"
                                                                                                                          "HH(n!1)"))
                                                                                                                        (("2"
                                                                                                                          (lemma
                                                                                                                           "isf_is_integrable[T2, S2, to_measure(nu)]")
                                                                                                                          (("2"
                                                                                                                            (inst
                                                                                                                             -
                                                                                                                             "LAMBDA (y: T2): HH(n!1)(x!1, y)")
                                                                                                                            nil
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (hide-all-but
                                                                                                           (1
                                                                                                            -14
                                                                                                            -15))
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "increasing_nn_isf?")
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "pointwise_converges_upto?")
                                                                                                              (("2"
                                                                                                                (split)
                                                                                                                (("1"
                                                                                                                  (expand
                                                                                                                   "pointwise_convergence?")
                                                                                                                  (("1"
                                                                                                                    (skolem
                                                                                                                     +
                                                                                                                     "y!1")
                                                                                                                    (("1"
                                                                                                                      (inst
                                                                                                                       -
                                                                                                                       "(x!1,y!1)")
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("2"
                                                                                                                  (expand
                                                                                                                   "pointwise_increasing?")
                                                                                                                  (("2"
                                                                                                                    (skolem
                                                                                                                     +
                                                                                                                     "y!1")
                                                                                                                    (("2"
                                                                                                                      (inst
                                                                                                                       -
                                                                                                                       "(x!1,y!1)")
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("3"
                                                                                                          (replace
                                                                                                           -8
                                                                                                           -5
                                                                                                           rl)
                                                                                                          (("3"
                                                                                                            (hide-all-but
                                                                                                             (-7
                                                                                                              1
                                                                                                              -13
                                                                                                              -12
                                                                                                              -8
                                                                                                              -3
                                                                                                              -6))
                                                                                                            (("3"
                                                                                                              (expand
                                                                                                               "FF")
                                                                                                              (("3"
                                                                                                                (expand
                                                                                                                 "o ")
                                                                                                                (("3"
                                                                                                                  (expand
                                                                                                                   "pointwise_increasing?")
                                                                                                                  (("3"
                                                                                                                    (inst
                                                                                                                     -2
                                                                                                                     "x!1")
                                                                                                                    (("3"
                                                                                                                      (hide
                                                                                                                       -4)
                                                                                                                      (("3"
                                                                                                                        (expand
                                                                                                                         "bounded?")
                                                                                                                        (("3"
                                                                                                                          (split)
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "bounded_above?")
                                                                                                                            (("1"
                                                                                                                              (inst
                                                                                                                               +
                                                                                                                               "F(x!1)")
                                                                                                                              (("1"
                                                                                                                                (skolem
                                                                                                                                 +
                                                                                                                                 "n!1")
                                                                                                                                (("1"
                                                                                                                                  (inst-cp
                                                                                                                                   -5
                                                                                                                                   "n!1")
                                                                                                                                  (("1"
                                                                                                                                    (lemma
                                                                                                                                     "isf_x_section"
                                                                                                                                     ("i"
                                                                                                                                      "HH(n!1)"
                                                                                                                                      "x"
                                                                                                                                      "x!1"))
                                                                                                                                    (("1"
                                                                                                                                      (rewrite
                                                                                                                                       "isf_integral")
                                                                                                                                      (("1"
                                                                                                                                        (rewrite
                                                                                                                                         "metric_convergence_def")
                                                                                                                                        (("1"
                                                                                                                                          (expand
                                                                                                                                           "metric_converges_to")
                                                                                                                                          (("1"
                                                                                                                                            (inst
                                                                                                                                             -
                                                                                                                                             "isf_integral(LAMBDA (y: T2): HH(n!1)(x!1, y))-F(x!1)")
                                                                                                                                            (("1"
                                                                                                                                              (skosimp)
                                                                                                                                              (("1"
                                                                                                                                                (inst
                                                                                                                                                 -
                                                                                                                                                 "n!1+n!2")
                                                                                                                                                (("1"
                                                                                                                                                  (assert)
                                                                                                                                                  (("1"
                                                                                                                                                    (expand
                                                                                                                                                     "ball")
                                                                                                                                                    (("1"
                                                                                                                                                      (expand
                                                                                                                                                       "increasing?")
                                                                                                                                                      (("1"
                                                                                                                                                        (inst
                                                                                                                                                         -3
                                                                                                                                                         "n!1"
                                                                                                                                                         "n!1+n!2")
                                                                                                                                                        (("1"
                                                                                                                                                          (assert)
                                                                                                                                                          nil
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil)
                                                                                                                                             ("2"
                                                                                                                                              (assert)
                                                                                                                                              nil
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil)
                                                                                                                                         ("2"
                                                                                                                                          (skosimp)
                                                                                                                                          (("2"
                                                                                                                                            (rewrite
                                                                                                                                             "isf_x_section")
                                                                                                                                            nil
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil)
                                                                                                                           ("2"
                                                                                                                            (expand
                                                                                                                             "bounded_below?")
                                                                                                                            (("2"
                                                                                                                              (inst
                                                                                                                               +
                                                                                                                               "0")
                                                                                                                              (("2"
                                                                                                                                (skolem
                                                                                                                                 +
                                                                                                                                 "n!1")
                                                                                                                                (("2"
                                                                                                                                  (inst
                                                                                                                                   -5
                                                                                                                                   "n!1")
                                                                                                                                  (("2"
                                                                                                                                    (lemma
                                                                                                                                     "isf_x_section"
                                                                                                                                     ("i"
                                                                                                                                      "HH(n!1)"
                                                                                                                                      "x"
                                                                                                                                      "x!1"))
                                                                                                                                    (("2"
                                                                                                                                      (rewrite
                                                                                                                                       "isf_integral"
                                                                                                                                       1)
                                                                                                                                      (("2"
                                                                                                                                        (inst
                                                                                                                                         -4
                                                                                                                                         "n!1"
                                                                                                                                         "x!1")
                                                                                                                                        (("2"
                                                                                                                                          (assert)
                                                                                                                                          nil
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil)
                                                                                                       ("2"
                                                                                                        (skosimp)
                                                                                                        (("2"
                                                                                                          (inst
                                                                                                           -13
                                                                                                           "n!1")
                                                                                                          (("2"
                                                                                                            (lemma
                                                                                                             "isf_x_section"
                                                                                                             ("i"
                                                                                                              "HH(n!1)"
                                                                                                              "x"
                                                                                                              "x!1"))
                                                                                                            (("2"
                                                                                                              (lemma
                                                                                                               "isf_is_integrable[T2, S2, to_measure(nu)]")
                                                                                                              (("2"
                                                                                                                (inst
                                                                                                                 -
                                                                                                                 "LAMBDA (y: T2): HH(n!1)(x!1, y)")
                                                                                                                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-all-but
                                                           (-2 1 -7))
                                                          (("2"
                                                            (expand
                                                             "bounded?")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (split)
                                                                (("1"
                                                                  (expand
                                                                   "bounded_above?")
                                                                  (("1"
                                                                    (inst
                                                                     +
                                                                     "c!1")
                                                                    (("1"
                                                                      (skolem
                                                                       +
                                                                       "n!1")
                                                                      (("1"
                                                                        (inst
                                                                         -
                                                                         "n!1")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (expand
                                                                   "bounded_below?")
                                                                  (("2"
                                                                    (inst
                                                                     +
                                                                     "-c!1")
                                                                    (("2"
                                                                      (skolem
                                                                       +
                                                                       "n!1")
                                                                      (("2"
                                                                        (inst
                                                                         -
                                                                         "n!1")
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide-all-but
                                                     (1 -2))
                                                    (("2"
                                                      (expand
                                                       "ae_increasing?")
                                                      (("2"
                                                        (inst
                                                         +
                                                         "emptyset")
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (expand
                                                             "pointwise_increasing?")
                                                            (("2"
                                                              (inst
                                                               -
                                                               "x!1")
                                                              (("2"
                                                                (expand
                                                                 "increasing?")
                                                                (("2"
                                                                  (propax)
--> --------------------

--> maximum size reached

--> --------------------

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.28Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff