Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: measure_space_def.pvs Sprache: PVS

Original von: PVS^©

(product_sigma_def
(measurable_rectangle_TCC1 0
  (measurable_rectangle_TCC1-1 nil 3421794703
   ("" (skosimp)
    (("" (expand "measurable_rectangle?")
      (("" (inst + "emptyset[T1]" "emptyset[T2]")
        (("" (assert)
          (("" (typepred "S1!1")
            (("" (typepred "S2!1")
              (("" (expand "sigma_algebra?")
                (("" (flatten)
                  (("" (expand "subset_algebra_empty?")
                    (("" (expand "member")
                      (("" (assert)
                        (("" (expand "cross_product")
                          (("" (apply-extensionality :hide? t)
                            (("" (expand "emptyset")
                              (("" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((measurable_rectangle? const-decl "bool" product_sigma_def nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (member const-decl "bool" sets nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product
     "topology/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T2 formal-type-decl nil product_sigma_def nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil product_sigma_def nil))
   nil))
(x_section_measurable 0
  (x_section_measurable-1 nil 3421796361
   ("" (expand "member")
    (("" (skosimp)
      (("" (name "G" "lambda y: (x!1,y)")
        ((""
          (case-replace "x_section(Z!1, x!1) = inverse_image(G)(Z!1)")
          (("1" (hide -1)
            (("1" (name "U" "{Z | S2!1(inverse_image(G)(Z))}")
              (("1" (case "sigma_algebra?(U)")
                (("1" (hide -2 -3)
                  (("1"
                    (case "forall (M:measurable_rectangle(S1!1,S2!1)): U(M)")
                    (("1" (typepred "sigma_times(S1!1,S2!1)")
                      (("1"
                        (lemma "generated_sigma_algebra_subset2"
                         ("Y" "U"))
                        (("1" (expand "sigma_times" -5)
                          (("1"
                            (inst - "extend
                                  [setof[[T1, T2]],
                                   measurable_rectangle(S1!1, S2!1), bool,
                                   FALSE]
                                  (fullset
                                       [measurable_rectangle(S1!1, S2!1)])")
                            (("1"
                              (name-replace "AA"
                               "generated_sigma_algebra(extend
                                  [setof[[T1, T2]],
                                   measurable_rectangle(S1!1, S2!1), bool,
                                   FALSE]
                                  (fullset
                                       [measurable_rectangle(S1!1, S2!1)]))")
                              (("1"
                                (replace -4)
                                (("1"
                                  (split -1)
                                  (("1"
                                    (expand "subset?")
                                    (("1"
                                      (inst - "Z!1")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (expand "member")
                                          (("1"
                                            (expand "U")
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (expand "fullset")
                                      (("2"
                                        (expand "extend")
                                        (("2"
                                          (expand "subset?")
                                          (("2"
                                            (expand "member")
                                            (("2"
                                              (skosimp)
                                              (("2"
                                                (prop)
                                                (("2"
                                                  (inst - "x!2")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (skosimp)
                        (("2" (typepred "M!1")
                          (("2" (expand "measurable_rectangle?")
                            (("2" (skosimp)
                              (("2"
                                (expand "U" 1)
                                (("2"
                                  (expand "inverse_image")
                                  (("2"
                                    (expand "inverse_image")
                                    (("2"
                                      (expand "G")
                                      (("2"
                                        (expand "member")
                                        (("2"
                                          (case-replace "X!1(x!1)")
                                          (("1"
                                            (case-replace
                                             "{x: T2 | M!1(x!1, x)}=Y!1")
                                            (("1"
                                              (hide-all-but (-1 -2 1))
                                              (("1"
                                                (apply-extensionality
                                                 :hide?
                                                 t)
                                                (("1"
                                                  (replace -2)
                                                  (("1"
                                                    (expand
                                                     "cross_product")
                                                    (("1"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (case-replace
                                             "{x: T2 | M!1(x!1, x)}=emptyset[T2]")
                                            (("1"
                                              (typepred "S2!1")
                                              (("1"
                                                (expand
                                                 "sigma_algebra?")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (expand
                                                     "subset_algebra_empty?")
                                                    (("1"
                                                      (expand "member")
                                                      (("1"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (replace -1)
                                              (("2"
                                                (hide-all-but (1 2))
                                                (("2"
                                                  (apply-extensionality
                                                   :hide?
                                                   t)
                                                  (("2"
                                                    (expand "emptyset")
                                                    (("2"
                                                      (expand
                                                       "cross_product")
                                                      (("2"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but (-3 1))
                  (("2" (typepred "S2!1")
                    (("2" (expand "U")
                      (("2" (expand "sigma_algebra?")
                        (("2" (flatten)
                          (("2" (split)
                            (("1" (expand "subset_algebra_empty?")
                              (("1"
                                (expand "member")
                                (("1"
                                  (expand "inverse_image")
                                  (("1"
                                    (expand "inverse_image")
                                    (("1"
                                      (expand "member")
                                      (("1"
                                        (expand "G")
                                        (("1"
                                          (expand "emptyset")
                                          (("1" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "subset_algebra_complement?")
                              (("2"
                                (skosimp)
                                (("2"
                                  (typepred "x!2")
                                  (("2"
                                    (expand "complement")
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (inst
                                         -
                                         "inverse_image(G)(x!2)")
                                        (("2"
                                          (expand "inverse_image")
                                          (("2"
                                            (expand "inverse_image")
                                            (("2"
                                              (expand "member")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (expand "sigma_algebra_union?")
                              (("3"
                                (skosimp)
                                (("3"
                                  (expand "member")
                                  (("3"
                                    (inst
                                     -5
                                     "image[set[[T1,T2]],set[T2]](inverse_image(G),X!1)")
                                    (("3"
                                      (split)
                                      (("1"
                                        (case-replace
                                         "Union(image[set[[T1, T2]], set[T2]](inverse_image(G), X!1))=inverse_image(G)(Union(X!1))")
                                        (("1"
                                          (hide-all-but 1)
                                          (("1"
                                            (apply-extensionality
                                             :hide?
                                             t)
                                            (("1"
                                              (expand "inverse_image")
                                              (("1"
                                                (expand "image")
                                                (("1"
                                                  (expand
                                                   "inverse_image")
                                                  (("1"
                                                    (expand "member")
                                                    (("1"
                                                      (expand "Union")
                                                      (("1"
                                                        (case-replace
                                                         "EXISTS (a: (X!1)): a(G(x!2))")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (typepred
                                                             "a!1")
                                                            (("1"
                                                              (inst
                                                               +
                                                               "a!1 o G")
                                                              (("1"
                                                                (expand
                                                                 "o ")
                                                                (("1"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (expand
                                                                 "o")
                                                                (("2"
                                                                  (inst
                                                                   +
                                                                   "a!1")
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (replace 1 2)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (typepred
                                                                 "a!1")
                                                                (("2"
                                                                  (skosimp)
                                                                  (("2"
                                                                    (replace
                                                                     -1)
                                                                    (("2"
                                                                      (assert)
                                                                      (("2"
                                                                        (typepred
                                                                         "x!3")
                                                                        (("2"
                                                                          (inst
                                                                           +
                                                                           "x!3")
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide-all-but (-1 1))
                                        (("2"
                                          (lemma
                                           "countable_image"
                                           ("f"
                                            "inverse_image(G)"
                                            "S"
                                            "X!1"))
                                          (("2"
                                            (assert)
                                            (("2"
                                              (expand "image" -1)
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("3"
                                        (hide 2)
                                        (("3"
                                          (skosimp)
                                          (("3"
                                            (typepred "x!2")
                                            (("3"
                                              (expand "image")
                                              (("3"
                                                (skosimp)
                                                (("3"
                                                  (typepred "x!3")
                                                  (("3"
                                                    (expand
                                                     "inverse_image")
                                                    (("3"
                                                      (replace -2 1)
                                                      (("3"
                                                        (inst - "x!3")
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide-all-but 1)
            (("2" (apply-extensionality :hide? t)
              (("2" (expand "G") (("2" (grind) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (inverse_image const-decl "set[D]" function_image nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
    (X!1 skolem-const-decl "setofsets[[T1, T2]]" product_sigma_def nil)
    (O const-decl "T3" function_props nil)
    (a!1 skolem-const-decl "(X!1)" product_sigma_def nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (Union const-decl "set" sets nil)
    (countable_image formula-decl nil countable_image "sets_aux/")
    (image const-decl "set[R]" function_image nil)
    (image const-decl "set[R]" function_image nil)
    (subset_algebra_complement? const-decl "bool" subset_algebra_def
     nil)
    (complement const-decl "set" sets nil)
    (G skolem-const-decl "[T2 -> [T1, T2]]" product_sigma_def nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product
     "topology/")
    (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (emptyset const-decl "set" sets nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (generated_sigma_algebra const-decl "sigma_algebra"
     subset_algebra_def nil)
    (U skolem-const-decl "[set[[T1, T2]] -> bool]" product_sigma_def
     nil)
    (subset? const-decl "bool" sets nil)
    (S1!1 skolem-const-decl "sigma_algebra[T1]" product_sigma_def nil)
    (S2!1 skolem-const-decl "sigma_algebra[T2]" product_sigma_def nil)
    (x!2 skolem-const-decl "setof[[T1, T2]]" product_sigma_def nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (fullset const-decl "set" sets nil)
    (generated_sigma_algebra_subset2 formula-decl nil
     subset_algebra_def nil)
    (measurable_rectangle nonempty-type-eq-decl nil product_sigma_def
     nil)
    (measurable_rectangle? const-decl "bool" product_sigma_def nil)
    (T2 formal-type-decl nil product_sigma_def nil)
    (T1 formal-type-decl nil product_sigma_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (member const-decl "bool" sets nil))
   shostak))
(y_section_measurable 0
  (y_section_measurable-1 nil 3421874773
   ("" (skosimp)
    (("" (expand "member")
      (("" (name "G" "lambda x: (x,y!1)")
        ((""
          (case-replace "y_section(Z!1, y!1) = inverse_image(G)(Z!1)")
          (("1" (hide -1 -2)
            (("1" (name "U" "{Z | S1!1(inverse_image(G)(Z))}")
              (("1" (case "sigma_algebra?(U)")
                (("1" (hide -2)
                  (("1"
                    (case "forall (M:measurable_rectangle(S1!1,S2!1)): U(M)")
                    (("1"
                      (lemma "generated_sigma_algebra_subset2"
                       ("Y" "U"))
                      (("1" (expand "sigma_times" -4)
                        (("1"
                          (inst - "extend
                                  [setof[[T1, T2]],
                                   measurable_rectangle(S1!1, S2!1), bool,
                                   FALSE]
                                  (fullset
                                       [measurable_rectangle(S1!1, S2!1)])")
                          (("1"
                            (name-replace "AA" "extend
                                  [setof[[T1, T2]],
                                   measurable_rectangle(S1!1, S2!1), bool,
                                   FALSE]
                                  (fullset
                                       [measurable_rectangle(S1!1, S2!1)])")
                            (("1" (replace -3)
                              (("1"
                                (split -1)
                                (("1"
                                  (expand "subset?")
                                  (("1"
                                    (expand "member")
                                    (("1"
                                      (inst - "Z!1")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (expand "U")
                                          (("1" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2"
                                    (expand "subset?")
                                    (("2"
                                      (skosimp)
                                      (("2"
                                        (expand "member")
                                        (("2"
                                          (expand "AA")
                                          (("2"
                                            (expand "fullset")
                                            (("2"
                                              (expand "extend")
                                              (("2"
                                                (prop)
                                                (("2"
                                                  (inst - "x!1")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (skosimp)
                        (("2" (typepred "M!1")
                          (("2" (expand "measurable_rectangle?")
                            (("2" (skosimp)
                              (("2"
                                (expand "U")
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (expand "inverse_image")
                                    (("2"
                                      (expand "inverse_image")
                                      (("2"
                                        (expand "cross_product")
                                        (("2"
                                          (expand "member")
                                          (("2"
                                            (expand "G")
                                            (("2"
                                              (case-replace "Y!1(y!1)")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (case-replace
                                                   "{x: T1 | X!1(x)}=X!1")
                                                  (("1"
                                                    (apply-extensionality
                                                     1
                                                     :hide?
                                                     t)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (replace 1)
                                                (("2"
                                                  (typepred "S1!1")
                                                  (("2"
                                                    (expand
                                                     "sigma_algebra?")
                                                    (("2"
                                                      (expand
                                                       "subset_algebra_empty?")
                                                      (("2"
                                                        (expand
                                                         "member")
                                                        (("2"
                                                          (expand
                                                           "emptyset")
                                                          (("2"
                                                            (flatten)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but 1)
                  (("2" (typepred "S1!1")
                    (("2" (expand "sigma_algebra?")
                      (("2" (flatten)
                        (("2" (split)
                          (("1" (expand "subset_algebra_empty?")
                            (("1" (expand "member")
                              (("1"
                                (expand "U")
                                (("1"
                                  (expand "inverse_image")
                                  (("1"
                                    (expand "inverse_image")
                                    (("1"
                                      (expand "member")
                                      (("1"
                                        (expand "emptyset")
                                        (("1" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "subset_algebra_complement?")
                            (("2" (skosimp)
                              (("2"
                                (expand "complement")
                                (("2"
                                  (expand "member")
                                  (("2"
                                    (typepred "x!1")
                                    (("2"
                                      (expand "U")
                                      (("2"
                                        (inst
                                         -
                                         "inverse_image(G)(x!1)")
                                        (("2"
                                          (expand "inverse_image")
                                          (("2"
                                            (expand "G")
                                            (("2"
                                              (expand "inverse_image")
                                              (("2"
                                                (expand "member")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (expand "sigma_algebra_union?")
                            (("3" (skosimp)
                              (("3"
                                (expand "member")
                                (("3"
                                  (inst
                                   -5
                                   "image[set[[T1,T2]],set[T1]](inverse_image(G),X!1)")
                                  (("3"
                                    (split -5)
                                    (("1"
                                      (case-replace
                                       "Union(image[set[[T1, T2]], set[T1]](inverse_image(G), X!1))=inverse_image(G)(Union(X!1))")
                                      (("1"
                                        (expand "U")
                                        (("1" (propax) nil nil))
                                        nil)
                                       ("2"
                                        (hide-all-but 1)
                                        (("2"
                                          (apply-extensionality
                                           :hide?
                                           t)
                                          (("2"
                                            (expand "inverse_image")
                                            (("2"
                                              (expand "inverse_image")
                                              (("2"
                                                (expand "member")
                                                (("2"
                                                  (expand "image")
                                                  (("2"
                                                    (expand "Union")
                                                    (("2"
                                                      (case-replace
                                                       "EXISTS (a: (X!1)): a(G(x!1))")
                                                      (("1"
                                                        (skosimp)
                                                        (("1"
                                                          (typepred
                                                           "a!1")
                                                          (("1"
                                                            (inst
                                                             +
                                                             "a!1 o G")
                                                            (("1"
                                                              (expand
                                                               "o ")
                                                              (("1"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "o")
                                                              (("2"
                                                                (inst
                                                                 +
                                                                 "a!1")
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (replace 1 2)
                                                        (("2"
                                                          (assert)
                                                          (("2"
                                                            (skosimp)
                                                            (("2"
                                                              (typepred
                                                               "a!1")
                                                              (("2"
                                                                (skosimp)
                                                                (("2"
                                                                  (replace
                                                                   -1)
                                                                  (("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (inst
                                                                       +
                                                                       "x!2")
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (lemma
                                       "countable_image"
                                       ("f"
                                        "inverse_image(G)"
                                        "S"
                                        "X!1"))
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "image" -1)
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("3"
                                      (skosimp)
                                      (("3"
                                        (typepred "x!1")
                                        (("3"
                                          (expand "image")
                                          (("3"
                                            (skosimp)
                                            (("3"
                                              (inst - "x!2")
                                              (("3"
                                                (expand "U")
                                                (("3"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide-all-but 1)
            (("2" (apply-extensionality :hide? t)
              (("2" (expand "y_section")
                (("2" (expand "inverse_image")
                  (("2" (expand "G")
                    (("2" (expand "inverse_image")
                      (("2" (expand "member") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (inverse_image const-decl "set[D]" function_image nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (x!1 skolem-const-decl "(U)" product_sigma_def nil)
    (complement const-decl "set" sets nil)
    (subset_algebra_complement? const-decl "bool" subset_algebra_def
     nil)
    (image const-decl "set[R]" function_image nil)
    (countable_image formula-decl nil countable_image "sets_aux/")
    (image const-decl "set[R]" function_image nil)
    (Union const-decl "set" sets nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (a!1 skolem-const-decl "(X!1)" product_sigma_def nil)
    (O const-decl "T3" function_props nil)
    (X!1 skolem-const-decl "setofsets[[T1, T2]]" product_sigma_def nil)
    (sigma_algebra_union? const-decl "bool" subset_algebra_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (emptyset const-decl "set" sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (G skolem-const-decl "[T1 -> [T1, T2]]" product_sigma_def nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product
     "topology/")
    (generated_sigma_algebra_subset2 formula-decl nil
     subset_algebra_def nil)
    (fullset const-decl "set" sets nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (AA skolem-const-decl "[setof[[T1, T2]] -> bool]" product_sigma_def
     nil)
    (S1!1 skolem-const-decl "sigma_algebra[T1]" product_sigma_def nil)
    (S2!1 skolem-const-decl "sigma_algebra[T2]" product_sigma_def nil)
    (x!1 skolem-const-decl "setof[[T1, T2]]" product_sigma_def nil)
    (subset? const-decl "bool" sets nil)
    (U skolem-const-decl "[set[[T1, T2]] -> bool]" product_sigma_def
     nil)
    (sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (measurable_rectangle nonempty-type-eq-decl nil product_sigma_def
     nil)
    (measurable_rectangle? const-decl "bool" product_sigma_def nil)
    (T1 formal-type-decl nil product_sigma_def nil)
    (T2 formal-type-decl nil product_sigma_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   shostak))
(sigma_cross_projection 0
  (sigma_cross_projection-1 nil 3421795427
   ("" (skosimp)
    (("" (typepred "NX!1")
      (("" (typepred "NY!1")
        (("" (expand "nonempty?")
          (("" (expand "empty?")
            (("" (skosimp*)
              (("" (expand "member")
                (("" (lemma "x_section_measurable")
                  (("" (inst - "S1!1" "S2!1" "_" "_")
                    (("" (inst - "cross_product(NX!1, NY!1)" "x!2")
                      (("" (expand "member")
                        ((""
                          (lemma "y_section_measurable"
                           ("S1" "S1!1" "S2" "S2!1" "Z"
                            "cross_product(NX!1, NY!1)" "y" "x!1"))
                          (("" (expand "member")
                            (("" (replace -5)
                              ((""
                                (expand "y_section")
                                ((""
                                  (expand "x_section")
                                  ((""
                                    (expand "cross_product")
                                    ((""
                                      (replace -3)
                                      ((""
                                        (replace -4)
                                        ((""
                                          (case-replace
                                           "{x | NX!1(x)}=NX!1")
                                          (("1"
                                            (case-replace
                                             "{y | NY!1(y)}=NY!1")
                                            (("1" (assert) nil nil)
                                             ("2"
                                              (apply-extensionality
                                               1
                                               :hide?
                                               t)
                                              nil
                                              nil))
                                            nil)
                                           ("2"
                                            (apply-extensionality
                                             1
                                             :hide?
                                             t)
                                            nil
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T1 formal-type-decl nil product_sigma_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (x_section_measurable formula-decl nil product_sigma_def nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product
     "topology/")
    (y_section_measurable formula-decl nil product_sigma_def nil)
    (x_section const-decl "set[T2]" cross_product "topology/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (y_section const-decl "set[T1]" cross_product "topology/")
    (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)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (T2 formal-type-decl nil product_sigma_def nil))
   shostak)))

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