Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: measure_contraction_props.pvs Sprache: PVS

Original von: PVS^©

(measure_contraction_props
(contraction_integrable_def_TCC1 0
  (contraction_integrable_def_TCC1-1 nil 3459392552
   ("" (skosimp*)
    (("" (expand "measurable_set?") (("" (propax) nil nil)) nil)) nil)
   ((measurable_set? const-decl "bool" measure_space_def nil)) nil))
(contraction_integrable_def_TCC2 0
  (contraction_integrable_def_TCC2-1 nil 3459397299
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil measure_contraction_props 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_contraction_props nil)
    (disjoint_indexed_measurable? const-decl "bool"
     generalized_measure_def nil)
    (disjoint_indexed_measurable nonempty-type-eq-decl nil
     generalized_measure_def nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (integrable? const-decl "bool" integral nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(contraction_integrable_def 0
  (contraction_integrable_def-1 nil 3459392897
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1"
          (case-replace
           "FORALL n: integrable?[T, S, contraction(mu, A!1(n))](h!1)")
          (("1"
            (lemma "indefinite_countably_additive[T, S, mu]"
             ("DX" "A!1" "f" "h!1"))
            (("1" (replace -4)
              (("1" (rewrite "indefinite_fullset[T, S, mu]")
                (("1"
                  (case-replace "(LAMBDA n:
                           integral[T, S, contraction(mu, A!1(n))](h!1))=LAMBDA n: integral[T, S, mu](A!1(n), h!1)")
                  (("1" (hide -1)
                    (("1" (expand "convergent?")
                      (("1" (inst + "integral[T, S, mu](h!1)") nil
                        nil))
                      nil))
                    nil)
                   ("2" (apply-extensionality :hide? t)
                    (("1" (expand "integral" 1 2)
                      (("1" (inst - "x!1")
                        (("1" (rewrite "contraction_integral" 1)
                          (("1" (expand "measurable_set?")
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp)
                      (("2" (expand "integrable?" 1)
                        (("2"
                          (rewrite "indefinite_integrable[T, S, mu]")
                          (("2" (expand "measurable_set?")
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("3" (expand "measurable_set?")
                      (("3" (propax) nil nil)) nil))
                    nil)
                   ("3" (skosimp)
                    (("3" (expand "integrable?" 1)
                      (("3" (rewrite "indefinite_integrable[T, S, mu]")
                        (("3" (expand "measurable_set?")
                          (("3" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("4" (expand "measurable_set?")
                    (("4" (propax) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (propax) nil nil))
            nil)
           ("2" (skosimp)
            (("2" (rewrite "contraction_integrable" 1)
              (("1" (rewrite "indefinite_integrable[T, S, mu]")
                (("1" (expand "measurable_set?")
                  (("1" (propax) nil nil)) nil))
                nil)
               ("2" (expand "measurable_set?") (("2" (propax) nil nil))
                nil))
              nil))
            nil)
           ("3" (expand "measurable_set?") (("3" (propax) nil nil))
            nil))
          nil))
        nil)
       ("2" (flatten)
        (("2" (name "F" "lambda n: *[T](phi(IUnion(n,A!1)),h!1)")
          (("2" (case "forall n: integrable?[T, S, mu](F(n))")
            (("1" (case "pointwise_converges_upto?(F,h!1)")
              (("1"
                (lemma "monotone_convergence_scaf[T, S, mu]"
                 ("f" "h!1" "F" "F"))
                (("1" (replace -2 -1)
                  (("1" (replace 1 -1)
                    (("1" (hide 2)
                      (("1" (expand "bounded?")
                        (("1" (split)
                          (("1" (expand "convergent?")
                            (("1" (skosimp)
                              (("1"
                                (expand "bounded_above?")
                                (("1"
                                  (inst + "l!1")
                                  (("1"
                                    (skolem + "n!1")
                                    (("1"
                                      (expand "o ")
                                      (("1"
                                        (expand
                                         "pointwise_converges_upto?")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (case-replace
                                             "series(LAMBDA n:
                            integral[T, S, contraction(mu, A!1(n))](h!1))=integral[T,S,mu] o F")
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (hide-all-but
                                                 (-2 -6 1 -3))
                                                (("1"
                                                  (rewrite
                                                   "metric_convergence_def")
                                                  (("1"
                                                    (expand
                                                     "metric_converges_to")
                                                    (("1"
                                                      (inst-cp - "n!1")
                                                      (("1"
                                                        (inst
                                                         -4
                                                         "integral[T, S, mu](F(n!1))-l!1")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (inst
                                                             -
                                                             "n!1+n!2")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "n!1+n!2")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (expand
                                                                   "ball")
                                                                  (("1"
                                                                    (expand
                                                                     "o ")
                                                                    (("1"
                                                                      (expand
                                                                       "pointwise_increasing?")
                                                                      (("1"
                                                                        (lemma
                                                                         "integral_ae_le[T, S, mu]"
                                                                         ("f1"
                                                                          "F(n!1)"
                                                                          "f2"
                                                                          "F(n!1 + n!2)"))
                                                                        (("1"
                                                                          (split)
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (hide-all-but
                                                                             (-1
                                                                              1))
                                                                            (("2"
                                                                              (expand
                                                                               "ae_le?")
                                                                              (("2"
                                                                                (expand
                                                                                 "pointwise_ae?")
                                                                                (("2"
                                                                                  (expand
                                                                                   "ae?")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "fullset")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "ae_in?")
                                                                                      (("2"
                                                                                        (inst
                                                                                         +
                                                                                         "emptyset")
                                                                                        (("1"
                                                                                          (skosimp)
                                                                                          (("1"
                                                                                            (expand
                                                                                             "member")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "x!1")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "increasing?")
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   -
                                                                                                   "n!1"
                                                                                                   "n!1+n!2")
                                                                                                  (("1"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (expand
                                                                                           "negligible_set?")
                                                                                          (("2"
                                                                                            (inst
                                                                                             +
                                                                                             "emptyset[T]")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "null_set?")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "mu_fin?")
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "mu")
                                                                                                  (("2"
                                                                                                    (typepred
                                                                                                     "mu")
                                                                                                    (("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))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide -6 2)
                                              (("2"
                                                (case
                                                 "forall n: series(LAMBDA n: integral[T, S, contraction(mu, A!1(n))](h!1))(n) =
       integral[T, S, mu](F(n))")
                                                (("1"
                                                  (rewrite
                                                   "extensionality_postulate"
                                                   -1)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (expand "o ")
                                                      (("1"
                                                        (replace
                                                         -1
                                                         1
                                                         rl)
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (apply-extensionality
                                                             :hide?
                                                             t)
                                                            (("1"
                                                              (expand
                                                               "measurable_set?")
                                                              (("1"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide -1 -2 2 -4)
                                                  (("2"
                                                    (induct "n")
                                                    (("1"
                                                      (expand "series")
                                                      (("1"
                                                        (expand
                                                         "sigma")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (inst
                                                             -
                                                             "n!1")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "n!1")
                                                              (("1"
                                                                (rewrite
                                                                 "contraction_integral"
                                                                 +)
                                                                (("1"
                                                                  (expand
                                                                   "F")
                                                                  (("1"
                                                                    (rewrite
                                                                     "IUnion_0_def")
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (expand
                                                                   "measurable_set?")
                                                                  (("2"
                                                                    (propax)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (skosimp)
                                                      (("2"
                                                        (expand
                                                         "series")
                                                        (("2"
                                                          (expand
                                                           "sigma"
                                                           1)
                                                          (("2"
                                                            (replace
                                                             -1)
                                                            (("2"
                                                              (hide -1)
                                                              (("2"
                                                                (inst
                                                                 -2
                                                                 "1+j!1")
                                                                (("2"
                                                                  (rewrite
                                                                   "contraction_integral")
                                                                  (("1"
                                                                    (case-replace
                                                                     "F(1 + j!1)=+[T](*[T](phi[T,S](A!1(1 + j!1)), h!1),F(j!1))")
                                                                    (("1"
                                                                      (rewrite
                                                                       "integral_add[T,S,mu]")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2
                                                                       -1
                                                                       -2)
                                                                      (("2"
                                                                        (apply-extensionality
                                                                         :hide?
                                                                         t)
                                                                        (("2"
                                                                          (expand
                                                                           "+")
                                                                          (("2"
                                                                            (expand
                                                                             "F")
                                                                            (("2"
                                                                              (expand
                                                                               "*")
                                                                              (("2"
                                                                                (case-replace
                                                                                 "phi(IUnion(1 + j!1, A!1))(x!1)=phi[T, S](A!1(1 + j!1))(x!1)+phi(IUnion(j!1, A!1))(x!1)")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide
                                                                                   -2
                                                                                   2)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "phi")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "member")
                                                                                      (("2"
                                                                                        (hide
                                                                                         -1)
                                                                                        (("2"
                                                                                          (rewrite
                                                                                           "IUnion_n_def")
                                                                                          (("2"
                                                                                            (expand
                                                                                             "union")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "member")
                                                                                              (("2"
                                                                                                (case-replace
                                                                                                 "IUnion(j!1, A!1)(x!1)")
                                                                                                (("1"
                                                                                                  (case-replace
                                                                                                   "A!1(1 + j!1)(x!1)")
                                                                                                  (("1"
                                                                                                    (hide
                                                                                                     1)
                                                                                                    (("1"
                                                                                                      (typepred
                                                                                                       "A!1")
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "disjoint_indexed_measurable?")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "disjoint?")
                                                                                                          (("1"
                                                                                                            (expand
                                                                                                             "IUnion")
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "image")
                                                                                                              (("1"
                                                                                                                (expand
                                                                                                                 "Union")
                                                                                                                (("1"
                                                                                                                  (skosimp)
                                                                                                                  (("1"
                                                                                                                    (typepred
                                                                                                                     "a!1")
                                                                                                                    (("1"
                                                                                                                      (skolem
                                                                                                                       -
                                                                                                                       "k!1")
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -
                                                                                                                         "k!1"
                                                                                                                         "1+j!1")
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "disjoint?")
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "empty?")
                                                                                                                              (("1"
                                                                                                                                (inst
                                                                                                                                 -
                                                                                                                                 "x!1")
                                                                                                                                (("1"
                                                                                                                                  (grind)
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (expand
                                                                     "measurable_set?")
                                                                    (("2"
                                                                      (propax)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (expand
                                                       "measurable_set?")
                                                      (("3"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (expand
                                                   "measurable_set?")
                                                  (("3"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("4"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (expand
                                               "measurable_set?")
                                              (("3" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "bounded_below?")
                            (("2" (inst + "0")
                              (("2"
                                (skolem + "n!1")
                                (("2"
                                  (expand "o ")
                                  (("2"
                                    (inst - "n!1")
                                    (("2"
                                      (lemma
                                       "integral_nonneg[T, S, mu]"
                                       ("f" "F(n!1)"))
                                      (("2"
                                        (assert)
                                        (("2"
                                          (skosimp)
                                          (("2"
                                            (hide-all-but (1 -7))
                                            (("2"
                                              (inst - "x!1")
                                              (("2"
                                                (expand "F")
                                                (("2"
                                                  (expand "*")
                                                  (("2"
                                                    (expand "phi")
                                                    (("2"
                                                      (lift-if)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (propax) nil nil))
                nil)
               ("2" (hide 2)
                (("2" (expand "pointwise_converges_upto?")
                  (("2" (split)
                    (("1" (expand "pointwise_convergence?")
                      (("1" (skosimp)
                        (("1" (hide -4)
                          (("1" (rewrite "metric_convergence_def")
                            (("1" (expand "metric_converges_to")
                              (("1"
                                (skosimp)
                                (("1"
                                  (expand "ball")
                                  (("1"
                                    (expand "member")
                                    (("1"
                                      (hide-all-but (-4 -5 1))
                                      (("1"
                                        (expand "F")
                                        (("1"
                                          (expand "*")
                                          (("1"
                                            (expand "phi")
                                            (("1"
                                              (expand "member")
                                              (("1"
                                                (expand "fullset")
                                                (("1"
                                                  (rewrite
                                                   "extensionality_postulate"
                                                   -1
                                                   :dir
                                                   rl)
                                                  (("1"
                                                    (inst - "x!1")
                                                    (("1"
                                                      (expand
                                                       "IUnion"
                                                       -1)
                                                      (("1"
                                                        (skolem
                                                         -
                                                         "n!1")
                                                        (("1"
                                                          (inst
                                                           +
                                                           "n!1")
                                                          (("1"
                                                            (skosimp)
                                                            (("1"
                                                              (case-replace
                                                               "IUnion(i!1, A!1)(x!1)")
                                                              (("1"
                                                                (expand
                                                                 "abs")
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide
                                                                 2)
                                                                (("2"
                                                                  (expand
                                                                   "IUnion")
                                                                  (("2"
                                                                    (expand
                                                                     "image")
                                                                    (("2"
                                                                      (expand
                                                                       "Union")
                                                                      (("2"
                                                                        (inst
                                                                         +
                                                                         "A!1(n!1)")
                                                                        (("2"
                                                                          (inst
                                                                           +
                                                                           "n!1")
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "pointwise_increasing?")
                      (("2" (skosimp)
                        (("2" (expand "increasing?")
                          (("2" (skolem + ("i!1" "j!1"))
                            (("2" (flatten)
                              (("2"
                                (hide-all-but (-7 -6 -1 1))
                                (("2"
                                  (expand "F")
                                  (("2"
                                    (expand "*")
                                    (("2"
                                      (expand "phi")
                                      (("2"
                                        (expand "member")
                                        (("2"
                                          (inst - "x!1")
                                          (("2"
                                            (case-replace
                                             "IUnion(i!1, A!1)(x!1)")
                                            (("1"
                                              (case-replace
                                               "IUnion(j!1, A!1)(x!1)")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (hide 2 -3)
                                                (("2"
                                                  (expand "IUnion")
                                                  (("2"
                                                    (expand "image")
                                                    (("2"
                                                      (expand "Union")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (inst
                                                           +
                                                           "a!1")
                                                          (("2"
                                                            (typepred
                                                             "a!1")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (inst
                                                                 +
                                                                 "x!2")
                                                                (("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (assert)
                                              (("2"
                                                (lift-if 2)
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (replace -1 1 rl)
              (("2" (hide -3 -1 2)
                (("2" (induct "n")
                  (("1" (rewrite "IUnion_0_def")
                    (("1" (inst - "0")
                      (("1" (rewrite "contraction_integrable")
                        (("1" (expand "measurable_set?")
                          (("1" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp)
                    (("2" (rewrite "IUnion_n_def")
                      (("2" (inst - "1+j!1")
                        (("2" (rewrite "contraction_integrable" -2)
                          (("1"
                            (case-replace
                             "(*[T](phi(union(IUnion(j!1, A!1), A!1(1 + j!1))), h!1))=+[T]((*[T](phi(IUnion(j!1, A!1)), h!1)),*[T](phi[T, S](A!1(1 + j!1)), h!1))")
                            (("1" (hide -1)
                              (("1"
                                (rewrite "integrable_add[T, S, mu]" 1)
                                nil
                                nil))
                              nil)
                             ("2" (hide 2 -1 -2 -4)
                              (("2"
                                (expand "fullset")
                                (("2"
                                  (rewrite
                                   "extensionality_postulate"
                                   -1
                                   :dir
                                   rl)
                                  (("2"
                                    (apply-extensionality :hide? t)
                                    (("2"
                                      (expand "*")
                                      (("2"
                                        (expand "+")
                                        (("2"
                                          (expand "phi")
                                          (("2"
                                            (expand "union")
                                            (("2"
                                              (expand "member")
                                              (("2"
                                                (case-replace
                                                 "IUnion(j!1, A!1)(x!1)")
                                                (("1"
                                                  (expand "IUnion" -1)
                                                  (("1"
                                                    (expand "image")
                                                    (("1"
                                                      (expand "Union")
                                                      (("1"
                                                        (skosimp)
                                                        (("1"
--> --------------------

--> maximum size reached

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

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