Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: product_finite_measure.prf Sprache: Lisp

Original von: PVS^©

(product_finite_measure
(x_section_bounded_TCC1 0
  (x_section_bounded_TCC1-1 nil 3450064167
   ("" (skosimp)
    (("" (expand "x_section")
      ((""
        (lemma "x_section_measurable[T1,T2]"
         ("Z" "M!1" "x" "x1!1" "S1" "S1" "S2" "S2"))
        (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((x_section const-decl "[T1 -> set[T2]]" cross_product "topology/")
    (member const-decl "bool" sets nil)
    (x_section_measurable formula-decl nil product_sigma_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" product_finite_measure
     nil)
    (S2 formal-const-decl "sigma_algebra[T2]" product_finite_measure
     nil)
    (set type-eq-decl nil sets nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (T1 formal-type-decl nil product_finite_measure nil)
    (T2 formal-type-decl nil product_finite_measure nil))
   nil))
(x_section_bounded 0
  (x_section_bounded-1 nil 3450064365
   ("" (skosimp)
    (("" (expand "o ")
      (("" (split)
        (("1" (assert) nil nil)
         ("2" (expand "x_section")
          (("2"
            (lemma "x_section_measurable[T1,T2]"
             ("Z" "M!1" "x" "x!1" "S1" "S1" "S2" "S2"))
            (("2" (expand "member")
              (("2"
                (lemma "fm_monotone[T2,S2,nu!1]"
                 ("A" "x_section(M!1, x!1)" "B" "fullset[T2]"))
                (("2" (split)
                  (("1" (propax) nil nil)
                   ("2" (expand "subset?")
                    (("2" (skosimp)
                      (("2" (expand "member")
                        (("2" (expand "fullset")
                          (("2" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (x_section const-decl "[T1 -> set[T2]]" cross_product "topology/")
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (subset_algebra_fullset name-judgement "(S)" product_finite_measure
     nil)
    (fm_monotone formula-decl nil finite_measure nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (fullset const-decl "set" sets nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (x_section_measurable formula-decl nil product_sigma_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" product_finite_measure
     nil)
    (S2 formal-const-decl "sigma_algebra[T2]" product_finite_measure
     nil)
    (set type-eq-decl nil sets nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (T1 formal-type-decl nil product_finite_measure nil)
    (T2 formal-type-decl nil product_finite_measure nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(y_section_bounded_TCC1 0
  (y_section_bounded_TCC1-1 nil 3450064167
   ("" (skosimp)
    (("" (expand "y_section")
      ((""
        (lemma "y_section_measurable[T1,T2]"
         ("Z" "M!1" "y" "x1!1" "S1" "S1" "S2" "S2"))
        (("" (expand "member") (("" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((y_section const-decl "[T2 -> set[T1]]" cross_product "topology/")
    (member const-decl "bool" sets nil)
    (y_section_measurable formula-decl nil product_sigma_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" product_finite_measure
     nil)
    (S2 formal-const-decl "sigma_algebra[T2]" product_finite_measure
     nil)
    (set type-eq-decl nil sets nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (T1 formal-type-decl nil product_finite_measure nil)
    (T2 formal-type-decl nil product_finite_measure nil))
   nil))
(y_section_bounded 0
  (y_section_bounded-1 nil 3450064193
   ("" (skosimp)
    (("" (expand "o")
      (("" (split)
        (("1" (assert) nil nil)
         ("2" (expand "y_section")
          (("2"
            (lemma "y_section_measurable[T1,T2]"
             ("Z" "M!1" "y" "y!1" "S1" "S1" "S2" "S2"))
            (("2" (expand "member")
              (("2"
                (lemma "m_monotone[T1,S1,to_measure(mu!1)]"
                 ("a" "y_section(M!1, y!1)" "b" "fullset[T1]"))
                (("1" (split)
                  (("1" (expand "to_measure")
                    (("1" (expand "x_le") (("1" (propax) nil nil))
                      nil))
                    nil)
                   ("2" (expand "subset?")
                    (("2" (expand "fullset")
                      (("2" (expand "member") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert)
                  (("2" (expand "measurable_set?")
                    (("2" (propax) nil nil)) nil))
                  nil)
                 ("3" (expand "measurable_set?")
                  (("3" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (y_section const-decl "[T2 -> set[T1]]" cross_product "topology/")
    (member const-decl "bool" sets nil)
    (x_le const-decl "bool" extended_nnreal "extended_nnreal/")
    (subset? const-decl "bool" sets nil)
    (subset_algebra_fullset name-judgement "(S)" product_finite_measure
     nil)
    (m_monotone formula-decl nil measure_props nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (fullset const-decl "set" sets nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (finite_measure? const-decl "bool" generalized_measure_def nil)
    (finite_measure nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (to_measure const-decl "measure_type" generalized_measure_def nil)
    (y_section_measurable formula-decl nil product_sigma_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" product_finite_measure
     nil)
    (S2 formal-const-decl "sigma_algebra[T2]" product_finite_measure
     nil)
    (set type-eq-decl nil sets nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (T1 formal-type-decl nil product_finite_measure nil)
    (T2 formal-type-decl nil product_finite_measure nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(x_section_measurable 0
  (x_section_measurable-1 nil 3430980741
   ("" (skosimp)
    (("" (name "F" "lambda M: nu!1 o x_section(M)")
      (("1" (case-replace "nu!1 o x_section(M!1) = F(M!1)")
        (("1" (hide-all-but 1)
          (("1"
            (case "forall x,M: 0 <= F(M)(x) & F(M)(x) <= nu!1(fullset[T2])")
            (("1"
              (name "U"
                    "{M:set[[T1,T2]] | sigma_times(S1,S2)(M) & measurable_function?[T1,S1](F(M))}")
              (("1"
                (case "forall (R:measurable_rectangle(S1,S2)): U(R)")
                (("1"
                  (case "FORALL (a, b: (U)): disjoint?(a,b) => U(union(a, b))")
                  (("1" (case "FORALL (a: (U)): U(complement(a))")
                    (("1" (case "monotone?(U)")
                      (("1" (lemma "monotone_class" ("C" "U"))
                        (("1" (typepred "rectangle_algebra")
                          (("1" (typepred "M!1")
                            (("1" (inst -3 "rectangle_algebra")
                              (("1"
                                (split -3)
                                (("1"
                                  (expand "subset?")
                                  (("1"
                                    (inst - "M!1")
                                    (("1"
                                      (expand "member")
                                      (("1"
                                        (split)
                                        (("1"
                                          (expand "U")
                                          (("1" (propax) nil nil))
                                          nil)
                                         ("2"
                                          (hide 2)
                                          (("2"
                                            (expand "sigma_times" -1)
                                            (("2"
                                              (lemma
                                               "generated_sigma_algebra_subset2"
                                               ("X"
                                                "extend
                                  [setof[[T1, T2]],
                                   measurable_rectangle[T1, T2](S1, S2),
                                   bool, FALSE]
                                  (fullset
                                       [measurable_rectangle
                                        [T1, T2](S1, S2)])"
                                                "Y"
                                                "generated_sigma_algebra(rectangle_algebra)"))
                                              (("2"
                                                (name-replace
                                                 "SA"
                                                 "generated_sigma_algebra(extend
                                  [setof[[T1, T2]],
                                   measurable_rectangle[T1, T2](S1, S2),
                                   bool, FALSE]
                                  (fullset
                                       [measurable_rectangle
                                        [T1, T2](S1, S2)]))")
                                                (("2"
                                                  (split -1)
                                                  (("1"
                                                    (expand "subset?")
                                                    (("1"
                                                      (inst - "M!1")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide 2)
                                                    (("2"
                                                      (expand
                                                       "subset?")
                                                      (("2"
                                                        (expand
                                                         "fullset")
                                                        (("2"
                                                          (expand
                                                           "extend")
                                                          (("2"
                                                            (expand
                                                             "member")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (prop)
                                                                (("2"
                                                                  (lemma
                                                                   "generated_sigma_algebra_subset1"
                                                                   ("X"
                                                                    "rectangle_algebra"))
                                                                  (("2"
                                                                    (expand
                                                                     "subset?")
                                                                    (("2"
                                                                      (inst
                                                                       -
                                                                       "x!1")
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (hide-all-but
                                                                           (-1
                                                                            1))
                                                                          (("2"
                                                                            (expand
                                                                             "rectangle_algebra")
                                                                            (("2"
                                                                              (expand
                                                                               "finite_disjoint_unions")
                                                                              (("2"
                                                                                (expand
                                                                                 "fullset")
                                                                                (("2"
                                                                                  (expand
                                                                                   "extend")
                                                                                  (("2"
                                                                                    (prop)
                                                                                    (("2"
                                                                                      (expand
                                                                                       "finite_disjoint_union?")
                                                                                      (("2"
                                                                                        (inst
                                                                                         +
                                                                                         "lambda (i:nat): if i = 0 then x!1 else emptyset[[T1,T2]] endif"
                                                                                         "1")
                                                                                        (("2"
                                                                                          (split)
                                                                                          (("1"
                                                                                            (hide
                                                                                             -1)
                                                                                            (("1"
                                                                                              (grind)
                                                                                              nil
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (apply-extensionality
                                                                                             :hide?
                                                                                             t)
                                                                                            (("2"
                                                                                              (expand
                                                                                               "IUnion")
                                                                                              (("2"
                                                                                                (case-replace
                                                                                                 "x!1(x!2, x!3)")
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   +
                                                                                                   "0")
                                                                                                  nil
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (assert)
                                                                                                  (("2"
                                                                                                    (skosimp)
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "emptyset")
                                                                                                      (("2"
                                                                                                        (propax)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("3"
                                                                                            (skosimp)
                                                                                            (("3"
                                                                                              (case-replace
                                                                                               "i!1=0")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil)
                                                                                               ("2"
                                                                                                (assert)
                                                                                                (("2"
                                                                                                  (rewrite
                                                                                                   "emptyset_is_empty?")
                                                                                                  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)
                                                   ("3"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2"
                                    (expand "subset?")
                                    (("2"
                                      (skosimp)
                                      (("2"
                                        (expand "member")
                                        (("2"
                                          (expand "rectangle_algebra")
                                          (("2"
                                            (expand
                                             "finite_disjoint_unions")
                                            (("2"
                                              (hide -3)
                                              (("2"
                                                (expand "fullset")
                                                (("2"
                                                  (expand "extend")
                                                  (("2"
                                                    (prop)
                                                    (("2"
                                                      (expand
                                                       "finite_disjoint_union?")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (case
                                                           "forall (n:nat): U(IUnion(n,E!1))")
                                                          (("1"
                                                            (case-replace
                                                             "IUnion(E!1)=IUnion(n!1,E!1)")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "n!1")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (hide-all-but
                                                               (1 -4))
                                                              (("2"
                                                                (apply-extensionality
                                                                 :hide?
                                                                 t)
                                                                (("2"
                                                                  (expand
                                                                   "IUnion")
                                                                  (("2"
                                                                    (expand
                                                                     "image")
                                                                    (("2"
                                                                      (expand
                                                                       "Union")
                                                                      (("2"
                                                                        (case-replace
                                                                         "EXISTS (i: nat): E!1(i)(x!2, x!3)")
                                                                        (("1"
                                                                          (skosimp)
                                                                          (("1"
                                                                            (inst
                                                                             -
                                                                             "i!1")
                                                                            (("1"
                                                                              (flatten)
                                                                              (("1"
                                                                                (case-replace
                                                                                 "i!1)
                                                                                (("1"
                                                                                  (inst
                                                                                   +
                                                                                   "E!1(i!1)")
                                                                                  (("1"
                                                                                    (inst
                                                                                     +
                                                                                     "i!1")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (assert)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "empty?")
                                                                                    (("2"
                                                                                      (inst
                                                                                       -3
                                                                                       "(x!2,x!3)")
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (replace
                                                                           1
                                                                           2)
                                                                          (("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (skosimp)
                                                                              (("2"
                                                                                (typepred
                                                                                 "a!1")
                                                                                (("2"
                                                                                  (skolem
                                                                                   -
                                                                                   "n!2")
                                                                                  (("2"
                                                                                    (inst
                                                                                     +
                                                                                     "n!2")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (1
                                                              -7
                                                              -1
                                                              -8
                                                              -3))
                                                            (("2"
                                                              (induct
                                                               "n")
                                                              (("1"
                                                                (rewrite
                                                                 "IUnion_0_def")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "0")
                                                                  (("1"
                                                                    (flatten)
                                                                    (("1"
                                                                      (inst
                                                                       -5
                                                                       "E!1(0)")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (rewrite
                                                                           "emptyset_is_empty?")
                                                                          (("1"
                                                                            (replace
                                                                             -2)
                                                                            (("1"
                                                                              (hide-all-but
                                                                               1)
                                                                              (("1"
                                                                                (expand
                                                                                 "measurable_rectangle?")
                                                                                (("1"
                                                                                  (inst
                                                                                   +
                                                                                   "emptyset"
                                                                                   "emptyset")
                                                                                  (("1"
                                                                                    (split)
                                                                                    (("1"
                                                                                      (apply-extensionality
                                                                                       :hide?
                                                                                       t)
                                                                                      (("1"
                                                                                        (grind)
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (typepred
                                                                                       "S1")
                                                                                      (("2"
                                                                                        (expand
                                                                                         "sigma_algebra?")
                                                                                        (("2"
                                                                                          (flatten)
                                                                                          (("2"
                                                                                            (expand
                                                                                             "subset_algebra_empty?")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "member")
                                                                                              (("2"
                                                                                                (propax)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("3"
                                                                                      (typepred
                                                                                       "S2")
                                                                                      (("3"
                                                                                        (expand
                                                                                         "sigma_algebra?")
                                                                                        (("3"
                                                                                          (flatten)
                                                                                          (("3"
                                                                                            (expand
                                                                                             "subset_algebra_empty?")
                                                                                            (("3"
                                                                                              (expand
                                                                                               "member")
                                                                                              (("3"
                                                                                                (propax)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (skosimp)
                                                                (("2"
                                                                  (rewrite
                                                                   "IUnion_n_def")
                                                                  (("2"
                                                                    (inst
                                                                     -5
                                                                     "E!1(1 + j!1)")
                                                                    (("1"
                                                                      (inst
                                                                       -4
                                                                       "IUnion(j!1, E!1)"
                                                                       "E!1(1 + j!1)")
                                                                      (("1"
                                                                        (split)
                                                                        (("1"
                                                                          (propax)
                                                                          nil
                                                                          nil)
                                                                         ("2"
                                                                          (hide-all-but
                                                                           (-2
                                                                            1))
                                                                          (("2"
                                                                            (expand
                                                                             "disjoint?")
                                                                            (("2"
                                                                              (expand
                                                                               "disjoint?")
                                                                              (("2"
                                                                                (expand
                                                                                 "intersection")
                                                                                (("2"
                                                                                  (expand
                                                                                   "IUnion")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "empty?")
                                                                                    (("2"
                                                                                      (skosimp)
                                                                                      (("2"
                                                                                        (expand
                                                                                         "member")
                                                                                        (("2"
                                                                                          (flatten)
                                                                                          (("2"
                                                                                            (expand
                                                                                             "image")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "Union")
                                                                                              (("2"
                                                                                                (skosimp)
                                                                                                (("2"
                                                                                                  (typepred
                                                                                                   "a!1")
                                                                                                  (("2"
                                                                                                    (skolem
                                                                                                     -
                                                                                                     "n!2")
                                                                                                    (("2"
                                                                                                      (inst
                                                                                                       -
                                                                                                       "n!2"
                                                                                                       "1+j!1")
                                                                                                      (("2"
                                                                                                        (assert)
                                                                                                        (("2"
                                                                                                          (inst
                                                                                                           -
                                                                                                           "x!2")
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (inst
                                                                       -
                                                                       "1+j!1")
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (flatten)
                                                                          (("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (rewrite
                                                                               "emptyset_is_empty?")
                                                                              (("2"
                                                                                (replace
                                                                                 -3)
                                                                                (("2"
                                                                                  (hide-all-but
                                                                                   1)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "measurable_rectangle?")
                                                                                    (("2"
                                                                                      (inst
                                                                                       +
                                                                                       "emptyset"
                                                                                       "emptyset")
                                                                                      (("2"
                                                                                        (split)
                                                                                        (("1"
                                                                                          (apply-extensionality
                                                                                           :hide?
                                                                                           t)
                                                                                          (("1"
                                                                                            (grind)
                                                                                            nil
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (typepred
                                                                                           "S1")
                                                                                          (("2"
                                                                                            (expand
                                                                                             "sigma_algebra?")
                                                                                            (("2"
                                                                                              (flatten)
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "subset_algebra_empty?")
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "member")
                                                                                                  (("2"
                                                                                                    (propax)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("3"
                                                                                          (typepred
                                                                                           "S2")
                                                                                          (("3"
                                                                                            (expand
                                                                                             "sigma_algebra?")
                                                                                            (("3"
                                                                                              (flatten)
                                                                                              (("3"
                                                                                                (expand
                                                                                                 "subset_algebra_empty?")
                                                                                                (("3"
                                                                                                  (expand
                                                                                                   "member")
                                                                                                  (("3"
                                                                                                    (propax)
                                                                                                    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))
--> --------------------

--> maximum size reached

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

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