products/sources/formale sprachen/PVS/measure_integration/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: OnOffSwitch.vdmrt   Sprache: Lisp

Original von: PVS©
(product_sigma
 (cross_product_is_sigma_times 0
  (cross_product_is_sigma_times-1 nil 3459218355
   ("" (skosimp)
    (("" (expand "sigma_times")
      ((""
        (lemma "generated_sigma_algebra_subset1"
         ("X" "extend
                                  [setof[[T1, T2]],
                                   measurable_rectangle[T1, T2](S1, S2),
                                   bool, FALSE]
                                  (fullset
                                       [measurable_rectangle
                                        [T1, T2](S1, S2)])"))
        (("" (expand "subset?")
          (("" (expand "member")
            (("" (inst - "cross_product(X!1, Y!1)")
              (("" (assert)
                (("" (hide 2)
                  (("" (expand "fullset")
                    (("" (expand "extend")
                      (("" (prop)
                        (("" (expand "measurable_rectangle?")
                          (("" (inst + "X!1" "Y!1")
                            (("" (assert)
                              ((""
                                (apply-extensionality :hide? t)
                                ((""
                                  (expand "cross_product")
                                  (("" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_times const-decl "sigma_algebra[[T1, T2]]" product_sigma_def
     nil)
    (subset? const-decl "bool" sets nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product
     "topology/")
    (member const-decl "bool" sets nil)
    (generated_sigma_algebra_subset1 formula-decl nil
     subset_algebra_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)
    (set 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)
    (measurable_rectangle? const-decl "bool" product_sigma_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" product_sigma nil)
    (S2 formal-const-decl "sigma_algebra[T2]" product_sigma nil)
    (measurable_rectangle nonempty-type-eq-decl nil product_sigma_def
     nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (fullset const-decl "set" sets nil)
    (T1 formal-type-decl nil product_sigma nil)
    (T2 formal-type-decl nil product_sigma nil))
   shostak))
 (rectangle_algebra_aux 0
  (rectangle_algebra_aux-1 nil 3450413455
   (""
    (case "FORALL (a, b: (measurable_rectangle?[T1, T2](S1, S2))):
                 measurable_rectangle?[T1, T2](S1, S2)(intersection(a,b))")
    (("1"
      (lemma "disjoint_algebra_construction[[T1,T2]]"
       ("NX" "measurable_rectangle?[T1, T2](S1, S2)"))
      (("1" (split -1)
        (("1" (propax) nil nil)
         ("2" (hide 2)
          (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)
         ("3" (hide -1 2)
          (("3" (skosimp)
            (("3" (typepred "a!1")
              (("3" (expand "finite_disjoint_union?")
                (("3" (expand "member")
                  (("3" (expand "measurable_rectangle?")
                    (("3" (skosimp)
                      (("3"
                        (inst +
                         "lambda (i:nat): if i=0 then cross_product(X!1,complement(Y!1)) elsif i=1 then cross_product(complement(X!1),complement(Y!1)) elsif i=2 then cross_product(complement(X!1),Y!1) else emptyset endif"
                         "3")
                        (("3" (split)
                          (("1" (expand "disjoint?")
                            (("1" (expand "cross_product")
                              (("1"
                                (expand "complement")
                                (("1"
                                  (expand "disjoint?")
                                  (("1"
                                    (expand "intersection")
                                    (("1"
                                      (expand "empty?")
                                      (("1"
                                        (expand "member")
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (expand "emptyset")
                                              (("1"
                                                (case-replace "i!1=0")
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (case-replace
                                                   "i!1=1")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (case-replace
                                                     "i!1=2")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (flatten)
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (replace -1)
                            (("2" (hide -1)
                              (("2"
                                (apply-extensionality :hide? t)
                                (("2"
                                  (expand "complement")
                                  (("2"
                                    (expand "cross_product")
                                    (("2"
                                      (expand "member")
                                      (("2"
                                        (expand "emptyset")
                                        (("2"
                                          (expand "IUnion")
                                          (("2"
                                            (case-replace "X!1(x!1)")
                                            (("1"
                                              (case-replace "Y!1(x!2)")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (assert)
                                                (("2"
                                                  (inst + "0")
                                                  nil
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (case-replace "Y!1(x!2)")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (inst + "2")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (assert)
                                                (("2"
                                                  (inst + "1")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("3" (skosimp*)
                            (("3" (hide -1)
                              (("3"
                                (case "i!1=0")
                                (("1"
                                  (assert)
                                  (("1"
                                    (typepred "S2")
                                    (("1"
                                      (expand "sigma_algebra?")
                                      (("1"
                                        (expand
                                         "subset_algebra_complement?")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (inst - "Y!1")
                                            (("1"
                                              (expand "member")
                                              (("1"
                                                (inst
                                                 +
                                                 "X!1"
                                                 "complement(Y!1)")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (apply-extensionality
                                                     :hide?
                                                     t)
                                                    (("1"
                                                      (expand
                                                       "cross_product")
                                                      (("1"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (case-replace "i!1=1")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (typepred "S2")
                                      (("1"
                                        (typepred "S1")
                                        (("1"
                                          (expand "sigma_algebra?")
                                          (("1"
                                            (expand
                                             "subset_algebra_complement?")
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (inst - "X!1")
                                                  (("1"
                                                    (inst - "Y!1")
                                                    (("1"
                                                      (inst
                                                       +
                                                       "complement(X!1)"
                                                       "complement(Y!1)")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (hide-all-but
                                                           2)
                                                          (("1"
                                                            (apply-extensionality
                                                             :hide?
                                                             t)
                                                            (("1"
                                                              (expand
                                                               "cross_product")
                                                              (("1"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (case-replace "i!1=2")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (typepred "S1")
                                        (("1"
                                          (expand "sigma_algebra?")
                                          (("1"
                                            (expand
                                             "subset_algebra_complement?")
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (inst - "X!1")
                                                  (("1"
                                                    (inst
                                                     +
                                                     "complement(X!1)"
                                                     "Y!1")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (expand
                                                         "cross_product")
                                                        (("1"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        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)
       ("2" (hide-all-but 1)
        (("2" (expand "nonempty?")
          (("2" (expand "empty?")
            (("2" (expand "member")
              (("2" (inst - "emptyset")
                (("2" (expand "measurable_rectangle?")
                  (("2" (inst + "emptyset" "emptyset")
                    (("2" (typepred "S2")
                      (("2" (typepred "S1")
                        (("2" (expand "sigma_algebra?")
                          (("2" (flatten)
                            (("2" (expand "subset_algebra_empty?")
                              (("2"
                                (expand "member")
                                (("2"
                                  (assert)
                                  (("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)
     ("2" (hide 2)
      (("2" (skosimp)
        (("2" (typepred "b!1")
          (("2" (typepred "a!1")
            (("2" (expand "measurable_rectangle?")
              (("2" (skosimp*)
                (("2"
                  (inst + "intersection(X!1,X!2)"
                   "intersection(Y!1,Y!2)")
                  (("2"
                    (lemma "sigma_algebra_intersection[T1,S1]"
                     ("x" "X!1" "y" "X!2"))
                    (("1"
                      (lemma "sigma_algebra_intersection[T2,S2]"
                       ("x" "Y!1" "y" "Y!2"))
                      (("1" (expand "member")
                        (("1" (assert)
                          (("1" (replace -3)
                            (("1" (replace -6)
                              (("1"
                                (hide-all-but 1)
                                (("1"
                                  (apply-extensionality :hide? t)
                                  (("1" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (propax) nil nil) ("3" (propax) nil nil))
                      nil)
                     ("2" (propax) nil nil) ("3" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_algebra_intersection formula-decl nil sigma_algebra nil)
    (nonempty? const-decl "bool" sets nil)
    (disjoint_algebra_construction formula-decl nil subset_algebra_def
     nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (disjoint? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
    (IUnion const-decl "set[T]" indexed_sets nil)
    (subset_algebra_complement application-judgement "(S)"
     sigma_algebra nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (subset_algebra_complement? const-decl "bool" subset_algebra_def
     nil)
    (emptyset const-decl "set" sets nil)
    (complement const-decl "set" sets nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product
     "topology/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (sequence type-eq-decl nil sequences nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (finite_disjoint_union? const-decl "bool" subset_algebra_def nil)
    (member const-decl "bool" sets nil)
    (subset_algebra_intersection application-judgement "(S)"
     sigma_algebra nil)
    (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (T1 formal-type-decl nil product_sigma nil)
    (T2 formal-type-decl nil product_sigma nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (measurable_rectangle? const-decl "bool" product_sigma_def nil)
    (S1 formal-const-decl "sigma_algebra[T1]" product_sigma nil)
    (S2 formal-const-decl "sigma_algebra[T2]" product_sigma nil)
    (intersection const-decl "set" sets nil))
   shostak))
 (rectangle_algebra_TCC1 0
  (rectangle_algebra_TCC1-1 nil 3450331052
   ("" (lemma "rectangle_algebra_aux")
    ((""
      (typepred
       "generated_subset_algebra[[T1, T2]](measurable_rectangle?(S1, S2))")
      (("" (assert) nil nil)) nil))
    nil)
   ((S2 formal-const-decl "sigma_algebra[T2]" product_sigma nil)
    (S1 formal-const-decl "sigma_algebra[T1]" product_sigma nil)
    (measurable_rectangle? const-decl "bool" product_sigma_def nil)
    (set type-eq-decl nil sets nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (generated_subset_algebra const-decl "subset_algebra"
     subset_algebra_def nil)
    (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (subset_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T2 formal-type-decl nil product_sigma nil)
    (T1 formal-type-decl nil product_sigma nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (rectangle_algebra_aux formula-decl nil product_sigma nil))
   nil))
 (rectangle_algebra_def 0
  (rectangle_algebra_def-1 nil 3450414364
   ("" (lemma "rectangle_algebra_aux")
    (("" (expand "rectangle_algebra") (("" (assert) nil nil)) nil))
    nil)
   ((rectangle_algebra const-decl "subset_algebra[[T1, T2]]"
     product_sigma nil)
    (rectangle_algebra_aux formula-decl nil product_sigma nil))
   shostak))
 (finite_disjoint_rectangles 0
  (finite_disjoint_rectangles-1 nil 3455513659
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (expand "finite_disjoint_unions")
          (("1" (expand "fullset")
            (("1" (expand "extend")
              (("1" (prop)
                (("1" (expand "finite_disjoint_union?")
                  (("1" (skosimp)
                    (("1" (expand "member")
                      (("1"
                        (case "forall (i:nat): measurable_rectangle?[T1, T2](S1, S2)(E!1(i))")
                        (("1"
                          (inst +
                           "image[nat,(measurable_rectangle?(S1, S2))](E!1,{n | n < n!1})")
                          (("1" (split)
                            (("1" (replace -3)
                              (("1"
                                (apply-extensionality :hide? t)
                                (("1"
                                  (hide -3 -2)
                                  (("1"
                                    (case-replace
                                     "IUnion(E!1)(x!1, x!2)")
                                    (("1"
                                      (expand "IUnion")
                                      (("1"
                                        (skosimp)
                                        (("1"
                                          (expand "Union")
                                          (("1"
                                            (typepred "i!1")
                                            (("1"
                                              (inst -4 "i!1")
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (case-replace
                                                   "i!1)
                                                  (("1"
                                                    (inst + "E!1(i!1)")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (expand
                                                         "image")
                                                        (("1"
                                                          (inst
                                                           +
                                                           "i!1")
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    (("2"
                                                      (expand "empty?")
                                                      (("2"
                                                        (inst
                                                         -5
                                                         "(x!1,x!2)")
                                                        (("2"
                                                          (expand
                                                           "member")
                                                          (("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (expand "IUnion")
                                        (("2"
                                          (expand "Union")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (typepred "a!1")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (expand "image")
                                                  (("2"
                                                    (skolem - "i!1")
                                                    (("2"
                                                      (typepred "i!1")
                                                      (("2"
                                                        (inst + "i!1")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2" (skosimp) nil nil))
                                nil))
                              nil)
                             ("2"
                              (lemma
                               "finite_image[nat, (measurable_rectangle?(S1, S2))]"
                               ("f" "E!1" "S" "{n | n < n!1}"))
                              (("1" (propax) nil nil)
                               ("2"
                                (hide-all-but 1)
                                (("2"
                                  (expand "is_finite")
                                  (("2"
                                    (inst
                                     +
                                     "n!1"
                                     "lambda (i:{n | n < n!1}): i")
                                    (("2"
                                      (expand "injective?")
                                      (("2" (skosimp) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (skosimp)
                              (("3"
                                (typepred "x!1")
                                (("3"
                                  (typepred "y!1")
                                  (("3"
                                    (expand "image")
                                    (("3"
                                      (skolem - "i!1")
                                      (("3"
                                        (skolem - "i!2")
                                        (("3"
                                          (typepred "i!1")
                                          (("3"
                                            (typepred "i!2")
                                            (("3"
                                              (expand "disjoint?" -8)
                                              (("3"
                                                (replace -4)
                                                (("3"
                                                  (replace -6)
                                                  (("3"
                                                    (hide-all-but
                                                     (1 2 -8))
                                                    (("3"
                                                      (inst
                                                       -
                                                       "i!1"
                                                       "i!2")
                                                      (("3"
                                                        (case-replace
                                                         "i!1=i!2")
                                                        (("3"
                                                          (assert)
                                                          (("3"
                                                            (expand
                                                             "disjoint?")
                                                            (("3"
                                                              (expand
                                                               "intersection")
                                                              (("3"
                                                                (expand
                                                                 "empty?")
                                                                (("3"
                                                                  (skosimp)
                                                                  (("3"
                                                                    (inst
                                                                     -
                                                                     "x!2")
                                                                    (("3"
                                                                      (expand
                                                                       "member")
                                                                      (("3"
                                                                        (flatten)
                                                                        (("3"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide -1 -2 2)
                          (("2" (skosimp)
                            (("2" (inst - "i!1")
                              (("2"
                                (case-replace "i!1)
                                (("1" (flatten) nil nil)
                                 ("2"
                                  (assert)
                                  (("2"
                                    (rewrite "emptyset_is_empty?")
                                    (("2"
                                      (replace -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"
                                                  (expand
                                                   "subset_algebra_empty?")
                                                  (("2"
                                                    (expand "member")
                                                    (("2"
                                                      (flatten)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (typepred "S2")
                                              (("3"
                                                (expand
                                                 "sigma_algebra?")
                                                (("3"
                                                  (expand
                                                   "subset_algebra_empty?")
                                                  (("3"
                                                    (expand "member")
                                                    (("3"
                                                      (flatten)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2" (expand "finite_disjoint_unions")
          (("2" (expand "extend")
            (("2" (expand "fullset")
              (("2" (prop)
                (("2" (expand "finite_disjoint_union?")
                  (("2"
                    (case "forall (n:nat,R,Z): is_finite(R) & card(R) <= n & Union(LAMBDA (t: setof[[T1, T2]]):
              IF measurable_rectangle?(S1, S2)(t) THEN R(t)
              ELSE FALSE
              ENDIF)
       = Z & (FORALL (x, y: (R)): x = y OR disjoint?(x, y)) => EXISTS (E: sequence[set[[T1, T2]]]), n:
        disjoint?(E) AND
         Z = IUnion(E) AND
          (FORALL i:
             (i < n => member(E(i), measurable_rectangle?(S1, S2))) AND
              (i >= n => empty?(E(i))))")
                    (("1" (inst - "card(R!1)" "R!1" "Z!1")
                      (("1" (assert)
                        (("1" (replace -4) (("1" (propax) nil nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide-all-but 1)
                      (("2" (induct "n")
                        (("1" (skosimp)
                          (("1" (expand "<=" -2)
                            (("1" (split)
                              (("1" (assert) nil nil)
                               ("2"
                                (lemma "card_is_0" ("S" "R!2"))
                                (("2"
                                  (replace -2 -1)
                                  (("2"
                                    (replace -1)
                                    (("2"
                                      (hide -2 -3)
                                      (("2"
                                        (case-replace
                                         "Z!2=emptyset[[T1,T2]]")
                                        (("1"
                                          (hide-all-but 1)
                                          (("1"
                                            (inst
                                             +
                                             "lambda (i:nat): emptyset[[T1,T2]]"
                                             "0")
                                            (("1"
                                              (split)
                                              (("1" (grind) nil nil)
                                               ("2"
                                                (apply-extensionality
                                                 :hide?
                                                 t)
                                                (("2"
                                                  (expand "emptyset")
                                                  (("2"
                                                    (expand "IUnion")
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (skosimp)
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (rewrite
                                                     "emptyset_is_empty?")
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide-all-but (-1 -2 1))
                                          (("2"
                                            (apply-extensionality
                                             :hide?
                                             t)
                                            (("2"
                                              (replace -2 1 rl)
                                              (("2"
                                                (hide -2)
                                                (("2"
                                                  (expand "emptyset")
                                                  (("2"
                                                    (expand "Union")
                                                    (("2"
                                                      (skosimp)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (skosimp*)
                          (("2" (expand "<=" -3)
                            (("2" (split -3)
                              (("1"
                                (inst -2 "R!2" "Z!2")
                                (("1"
                                  (assert)
                                  (("1"
                                    (replace -5)
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (lemma "nonempty_card" ("S" "R!2"))
                                (("2"
                                  (flatten -1)
                                  (("2"
                                    (hide -1)
                                    (("2"
                                      (split -1)
                                      (("1"
                                        (lemma "card_rest" ("S" "R!2"))
                                        (("1"
                                          (copy -2)
                                          (("1"
                                            (expand "nonempty?" -1)
                                            (("1"
                                              (replace 1)
                                              (("1"
                                                (replace -3)
                                                (("1"
                                                  (simplify -1)
                                                  (("1"
                                                    (lemma
                                                     "choose_rest"
                                                     ("a" "R!2"))
                                                    (("1"
                                                      (replace 1)
                                                      (("1"
                                                        (inst
                                                         -5
                                                         "rest(R!2)"
                                                         "Union(rest(R!2))")
                                                        (("1"
                                                          (split -5)
                                                          (("1"
                                                            (skosimp)
                                                            (("1"
                                                              (lemma
                                                               "extensionality_postulate"
                                                               ("f"
                                                                "Union(extend
                [setof[[T1, T2]],
                 ((measurable_rectangle?[T1, T2](S1, S2))), bool, FALSE]
                (rest(R!2)))"
                                                                "g"
                                                                "IUnion(E!1)"))
                                                              (("1"
                                                                (flatten)
                                                                (("1"
                                                                  (hide
                                                                   -1)
                                                                  (("1"
                                                                    (split
                                                                     -1)
                                                                    (("1"
                                                                      (hide
                                                                       -3)
                                                                      (("1"
                                                                        (case
                                                                         "Z!2 = union(choose(R!2), IUnion(E!1))")
                                                                        (("1"
                                                                          (case
                                                                           "forall (i:nat): disjoint?(choose(R!2),E!1(i))")
                                                                          (("1"
                                                                            (inst
                                                                             +
                                                                             "lambda (i:nat): if i=0 then choose(R!2) else E!1(i-1) endif"
                                                                             "n!1+1")
                                                                            (("1"
                                                                              (split)
                                                                              (("1"
                                                                                (expand
                                                                                 "disjoint?"
                                                                                 (-4
                                                                                  1))
                                                                                (("1"
                                                                                  (skosimp)
                                                                                  (("1"
                                                                                    (case-replace
                                                                                     "i!1=0")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      (("1"
                                                                                        (inst
                                                                                         -2
                                                                                         "j!2-1")
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (replace
                                                                                       1)
                                                                                      (("2"
                                                                                        (case-replace
                                                                                         "j!2=0")
                                                                                        (("1"
                                                                                          (inst
                                                                                           -2
                                                                                           "i!1-1")
                                                                                          (("1"
                                                                                            (hide-all-but
                                                                                             (-2
                                                                                              3))
                                                                                            (("1"
                                                                                              (expand
                                                                                               "disjoint?")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "intersection")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "empty?")
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "member")
                                                                                                    (("1"
                                                                                                      (skosimp)
                                                                                                      (("1"
                                                                                                        (inst
                                                                                                         -
                                                                                                         "x!1")
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (assert)
                                                                                          (("2"
                                                                                            (inst
                                                                                             -4
                                                                                             "i!1-1"
                                                                                             "j!2-1")
                                                                                            (("2"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (apply-extensionality
                                                                                 :hide?
                                                                                 t)
                                                                                (("1"
                                                                                  (replace
                                                                                   -2
                                                                                   1)
                                                                                  (("1"
                                                                                    (hide
                                                                                     -2)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "union")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "member")
                                                                                        (("1"
                                                                                          (case-replace
                                                                                           "choose(R!2)(x!1, x!2)")
                                                                                          (("1"
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.31 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




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.


Bot Zugriff