Bilddatei product_sigma.prf

(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<n!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<n!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"
                                                                                            (expand
                                                                                             "IUnion")
                                                                                            (("1"
                                                                                              (inst
                                                                                               +
                                                                                               "0")
                                                                                              nil
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (case-replace
                                                                                               "IUnion(E!1)(x!1, x!2)")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "IUnion")
                                                                                                (("1"
                                                                                                  (skosimp)
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     +
                                                                                                     "i!1+1")
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (assert)
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "IUnion")
                                                                                                  (("2"
                                                                                                    (skosimp)
                                                                                                    (("2"
                                                                                                      (replace
                                                                                                       2)
                                                                                                      (("2"
                                                                                                        (prop)
                                                                                                        (("2"
                                                                                                          (inst
                                                                                                           +
                                                                                                           "i!1-1")
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("3"
                                                                                (skosimp*)
                                                                                (("3"
                                                                                  (expand
                                                                                   "member")
                                                                                  (("3"
                                                                                    (case-replace
                                                                                     "i!1=0")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil)
                                                                                     ("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (inst
                                                                                         -5
                                                                                         "i!1-1")
                                                                                        (("2"
                                                                                          (flatten)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (case-replace
                                                                                               "i!1 < 1 + n!1")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil)
                                                                                               ("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (skosimp)
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (hide
                                                                             3)
                                                                            (("2"
                                                                              (skosimp)
                                                                              (("2"
                                                                                (expand
                                                                                 "disjoint?"
                                                                                 1)
                                                                                (("2"
                                                                                  (expand
                                                                                   "intersection")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "empty?"
                                                                                     1)
                                                                                    (("2"
                                                                                      (expand
                                                                                       "member")
                                                                                      (("2"
                                                                                        (skosimp)
                                                                                        (("2"
                                                                                          (inst
                                                                                           -4
                                                                                           "x!1")
                                                                                          (("2"
                                                                                            (case-replace
                                                                                             "IUnion(E!1)(x!1)")
                                                                                            (("1"
                                                                                              (expand
                                                                                               "extend")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "Union")
                                                                                                (("1"
                                                                                                  (skosimp)
                                                                                                  (("1"
                                                                                                    (typepred
                                                                                                     "a!1")
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      (("1"
                                                                                                        (inst
                                                                                                         -16
                                                                                                         "choose(R!2)"
                                                                                                         "a!1")
                                                                                                        (("1"
                                                                                                          (lemma
                                                                                                           "choose_not_member"
                                                                                                           ("a"
                                                                                                            "R!2"))
                                                                                                          (("1"
                                                                                                            (assert)
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "member")
                                                                                                              (("1"
                                                                                                                (split)
                                                                                                                (("1"
                                                                                                                  (assert)
                                                                                                                  nil
                                                                                                                  nil)
                                                                                                                 ("2"
                                                                                                                  (expand
                                                                                                                   "disjoint?")
                                                                                                                  (("2"
                                                                                                                    (expand
                                                                                                                     "intersection")
                                                                                                                    (("2"
                                                                                                                      (expand
                                                                                                                       "empty?")
                                                                                                                      (("2"
                                                                                                                        (expand
                                                                                                                         "member")
                                                                                                                        (("2"
                                                                                                                          (inst
                                                                                                                           -
                                                                                                                           "x!1")
                                                                                                                          (("2"
                                                                                                                            (assert)
                                                                                                                            nil
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (expand
                                                                                                           "rest")
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "remove")
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "member")
                                                                                                              (("2"
                                                                                                                (flatten)
                                                                                                                nil
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (expand
                                                                                               "IUnion")
                                                                                              (("2"
                                                                                                (inst
                                                                                                 +
                                                                                                 "i!1")
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (hide
                                                                           3)
                                                                          (("2"
                                                                            (apply-extensionality
                                                                             :hide?
                                                                             t)
                                                                            (("2"
                                                                              (replace
                                                                               -9
                                                                               1
                                                                               rl)
                                                                              (("2"
                                                                                (expand
                                                                                 "union")
                                                                                (("2"
                                                                                  (expand
                                                                                   "member")
                                                                                  (("2"
                                                                                    (case-replace
                                                                                     "choose(R!2)(x!1, x!2)")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "Union")
                                                                                      (("1"
                                                                                        (inst
                                                                                         +
                                                                                         "choose(R!2)")
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (inst
                                                                                         -
                                                                                         "(x!1,x!2)")
                                                                                        (("2"
                                                                                          (case-replace
                                                                                           "IUnion(E!1)(x!1, x!2)")
                                                                                          (("1"
                                                                                            (expand
                                                                                             "Union")
                                                                                            (("1"
                                                                                              (skosimp)
                                                                                              (("1"
                                                                                                (typepred
                                                                                                 "a!1")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "extend")
                                                                                                  (("1"
                                                                                                    (prop)
                                                                                                    (("1"
                                                                                                      (inst
                                                                                                       +
                                                                                                       "a!1")
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "rest")
                                                                                                          (("1"
                                                                                                            (expand
                                                                                                             "remove")
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "member")
                                                                                                              (("1"
                                                                                                                (propax)
                                                                                                                nil
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (expand
                                                                                               "extend")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "Union")
                                                                                                (("2"
                                                                                                  (skosimp)
                                                                                                  (("2"
                                                                                                    (typepred
                                                                                                     "a!1")
                                                                                                    (("2"
                                                                                                      (assert)
                                                                                                      (("2"
                                                                                                        (inst
                                                                                                         +
                                                                                                         "a!1")
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "rest")
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "remove")
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "member")
                                                                                                              (("2"
                                                                                                                (propax)
                                                                                                                nil
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (propax)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (lemma
                                                             "finite_rest"
                                                             ("A"
                                                              "R!2"))
                                                            (("2"
                                                              (propax)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("3"
                                                            (assert)
                                                            nil
                                                            nil)
                                                           ("4"
                                                            (hide 3)
                                                            (("4"
                                                              (expand
                                                               "extend")
                                                              (("4"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("5"
                                                            (skosimp)
                                                            (("5"
                                                              (typepred
                                                               "x!1")
                                                              (("5"
                                                                (typepred
                                                                 "y!1")
                                                                (("5"
                                                                  (inst
                                                                   -11
                                                                   "x!1"
                                                                   "y!1")
                                                                  (("1"
                                                                    (split)
                                                                    (("1"
                                                                      (propax)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (propax)
                                                                      nil
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (expand
                                                                     "rest")
                                                                    (("2"
                                                                      (expand
                                                                       "remove")
                                                                      (("2"
                                                                        (expand
                                                                         "member")
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("3"
                                                                    (expand
                                                                     "rest")
                                                                    (("3"
                                                                      (expand
                                                                       "remove")
                                                                      (("3"
                                                                        (expand
                                                                         "member")
                                                                        (("3"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_disjoint_unions const-decl "setofsets[T]"
     subset_algebra_def nil)
    (extend const-decl "R" extend nil)
    (finite_disjoint_union? const-decl "bool" subset_algebra_def nil)
    (member const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (subset_algebra_empty? const-decl "bool" subset_algebra_def nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product
     "topology/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (E!1 skolem-const-decl "sequence[set[[T1, T2]]]" product_sigma nil)
    (< const-decl "bool" reals nil)
    (image const-decl "set[R]" function_image nil)
    (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
    (intersection const-decl "set" sets nil)
    (disjoint? const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_image judgement-tcc nil function_image_aux nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (injective? const-decl "bool" functions nil)
    (below type-eq-decl nil nat_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (n!1 skolem-const-decl "nat" product_sigma nil)
    (i!1 skolem-const-decl "nat" product_sigma nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (FALSE const-decl "bool" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (Union const-decl "set" sets nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T1 formal-type-decl nil product_sigma 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)
    (T2 formal-type-decl nil product_sigma nil)
    (set type-eq-decl nil sets 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)
    (sequence type-eq-decl nil sequences nil)
    (fullset const-decl "set" sets nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (extensionality_postulate formula-decl nil functions nil)
    (a!1 skolem-const-decl "(extend
     [setof[[T1, T2]], ((measurable_rectangle?[T1, T2](S1, S2))), bool,
      FALSE]
     (rest(R!2)))" product_sigma nil)
    (a!1 skolem-const-decl "(LAMBDA (t: setof[[T1, T2]]):
   IF measurable_rectangle?(S1, S2)(t) THEN R!2(t) ELSE FALSE ENDIF)"
     product_sigma nil)
    (i!1 skolem-const-decl "nat" product_sigma nil)
    (i!1 skolem-const-decl "nat" product_sigma nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (remove const-decl "set" sets nil)
    (choose_not_member formula-decl nil sets_lemmas nil)
    (a!1 skolem-const-decl "(LAMBDA (t: setof[[T1, T2]]):
   IF measurable_rectangle?[T1, T2](S1, S2)(t) THEN rest(R!2)(t)
   ELSE FALSE
   ENDIF)" product_sigma nil)
    (R!2 skolem-const-decl "set[(measurable_rectangle?(S1, S2))]"
     product_sigma nil)
    (choose const-decl "(p)" sets nil)
    (union const-decl "set" sets nil)
    (finite_rest judgement-tcc nil finite_sets nil)
    (x!1 skolem-const-decl "(rest(R!2))" product_sigma nil)
    (y!1 skolem-const-decl "(rest(R!2))" product_sigma nil)
    (rest const-decl "set" sets nil)
    (choose_rest formula-decl nil sets_lemmas nil)
    (nonempty? const-decl "bool" sets nil)
    (card_rest formula-decl nil finite_sets nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonempty_card formula-decl nil finite_sets nil)
    (finite_intersection1 application-judgement "finite_set[T]"
     countable_props "sets_aux/")
    (countable_intersection2 application-judgement "countable_set[T]"
     countable_props "sets_aux/")
    (/= const-decl "boolean" notequal nil)
    (sigma_algebra_IUnion_rew application-judgement "(S)" sigma_algebra
     nil)
    (card_is_0 formula-decl nil finite_sets nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (R!1 skolem-const-decl "set[(measurable_rectangle?(S1, S2))]"
     product_sigma nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
 (intersection_rectangle 0
  (intersection_rectangle-1 nil 3455519645
   ("" (skosimp)
    (("" (typepred "r2!1")
      (("" (typepred "r1!1")
        (("" (expand "measurable_rectangle?")
          (("" (skosimp*)
            (("" (expand "finite_disjoint_union?")
              ((""
                (inst +
                 "lambda (i:nat): if i=0 then cross_product(intersection(X!1,X!2),intersection(Y!1,Y!2)) else emptyset endif"
                 "1")
                (("" (split)
                  (("1" (grind) nil nil)
                   ("2" (apply-extensionality :hide? t)
                    (("2" (grind) nil nil)) nil)
                   ("3" (skosimp)
                    (("3" (case-replace "i!1=0")
                      (("1" (assert)
                        (("1" (expand "member")
                          (("1"
                            (inst + "intersection(X!1, X!2)"
                             "intersection(Y!1, Y!2)")
                            (("1"
                              (lemma
                               "sigma_algebra_intersection[T1,S1]"
                               ("x" "X!1" "y" "X!2"))
                              (("1"
                                (expand "member")
                                (("1"
                                  (assert)
                                  (("1"
                                    (lemma
                                     "sigma_algebra_intersection[T2,S2]"
                                     ("x" "Y!1" "y" "Y!2"))
                                    (("1"
                                      (expand "member")
                                      (("1"
                                        (expand "cross_product")
                                        (("1" (propax) 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)
   ((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)
    (T2 formal-type-decl nil product_sigma 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)
    (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)
    (subset_algebra_intersection application-judgement "(S)"
     sigma_algebra nil)
    (finite_disjoint_union? const-decl "bool" subset_algebra_def nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
    (disjoint? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (/= const-decl "boolean" notequal nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (sigma_algebra_intersection formula-decl nil sigma_algebra nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas 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)
    (intersection 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))
   shostak))
 (complement_rectangle 0
  (complement_rectangle-1 nil 3455520014
   ("" (skosimp)
    (("" (typepred "r!1")
      (("" (expand "measurable_rectangle?")
        (("" (skosimp)
          (("" (expand "finite_disjoint_union?")
            ((""
              (inst +
               "lambda (i:nat): if i=0 then cross_product(complement(X!1), Y!1) elsif i=1 then cross_product(X!1, complement(Y!1)) elsif i=2 then cross_product(complement(X!1),complement(Y!1)) else emptyset endif"
               "3")
              (("" (split)
                (("1" (expand "disjoint?")
                  (("1" (skosimp) (("1" (grind) nil nil)) nil)) nil)
                 ("2" (apply-extensionality :hide? t)
                  (("2" (replace -1)
                    (("2" (hide -1)
                      (("2" (expand "complement")
                        (("2" (expand "member")
                          (("2" (expand "cross_product")
                            (("2" (case-replace "X!1(x!1)")
                              (("1"
                                (case-replace "Y!1(x!2)")
                                (("1"
                                  (assert)
                                  (("1"
                                    (expand "IUnion")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (expand "emptyset")
                                        (("1" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (assert)
                                  (("2"
                                    (expand "IUnion")
                                    (("2"
                                      (expand "emptyset")
                                      (("2"
                                        (inst + "1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (case-replace "Y!1(x!2)")
                                (("1"
                                  (assert)
                                  (("1"
                                    (expand "IUnion")
                                    (("1"
                                      (assert)
                                      (("1" (inst + "0") nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (assert)
                                  (("2"
                                    (expand "IUnion")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (inst + "2")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (expand "cross_product")
                  (("3" (expand "complement")
                    (("3" (expand "empty?")
                      (("3" (expand "member")
                        (("3" (skosimp)
                          (("3" (assert)
                            (("3" (case-replace "i!1=0")
                              (("1"
                                (assert)
                                (("1"
                                  (inst + "complement(X!1)" "Y!1")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (lemma
                                       "sigma_algebra_complement[T1,S1]"
                                       ("x" "X!1"))
                                      (("1"
                                        (expand "member")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (apply-extensionality
                                             :hide?
                                             t)
                                            (("1"
                                              (expand "complement")
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (case-replace "i!1=1")
                                (("1"
                                  (assert)
                                  (("1"
                                    (inst + "X!1" "complement(Y!1)")
                                    (("1"
                                      (lemma
                                       "sigma_algebra_complement[T2,S2]"
                                       ("x" "Y!1"))
                                      (("1"
                                        (expand "member")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (apply-extensionality
                                             2
                                             :hide?
                                             t)
                                            (("1"
                                              (expand "complement")
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (case-replace "i!1=2")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (lemma
                                       "sigma_algebra_complement[T2,S2]"
                                       ("x" "Y!1"))
                                      (("1"
                                        (lemma
                                         "sigma_algebra_complement[T1,S1]"
                                         ("x" "X!1"))
                                        (("1"
                                          (expand "member")
                                          (("1"
                                            (inst
                                             +
                                             "complement(X!1)"
                                             "complement(Y!1)")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (apply-extensionality
                                                 3
                                                 :hide?
                                                 t)
                                                (("1"
                                                  (expand "complement")
                                                  (("1"
                                                    (expand "member")
                                                    (("1"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (assert)
                                    (("2"
                                      (expand "emptyset")
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          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)
    (T2 formal-type-decl nil product_sigma 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)
    (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)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (cross_product const-decl "set[[T1, T2]]" cross_product
     "topology/")
    (complement const-decl "set" sets nil)
    (emptyset const-decl "set" sets nil)
    (sigma_algebra_complement formula-decl nil sigma_algebra nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" sets nil)
    (finite_disjoint_union? const-decl "bool" subset_algebra_def nil)
    (subset_algebra_complement application-judgement "(S)"
     sigma_algebra nil))
   shostak)))