Quelle  measure_contraction_props.prf

(measure_contraction_props
 (contraction_integrable_def_TCC1 0
  (contraction_integrable_def_TCC1-1 nil 3459392552
   ("" (skosimp*)
    (("" (expand "measurable_set?") (("" (propax) nil nil)) nil)) nil)
   ((measurable_set? const-decl "bool" measure_space_def nil)) nil))
 (contraction_integrable_def_TCC2 0
  (contraction_integrable_def_TCC2-1 nil 3459397299
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil measure_contraction_props nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_contraction_props nil)
    (disjoint_indexed_measurable? const-decl "bool"
     generalized_measure_def nil)
    (disjoint_indexed_measurable nonempty-type-eq-decl nil
     generalized_measure_def nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (integrable? const-decl "bool" integral nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (contraction_integrable_def 0
  (contraction_integrable_def-1 nil 3459392897
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1"
          (case-replace
           "FORALL n: integrable?[T, S, contraction(mu, A!1(n))](h!1)")
          (("1"
            (lemma "indefinite_countably_additive[T, S, mu]"
             ("DX" "A!1" "f" "h!1"))
            (("1" (replace -4)
              (("1" (rewrite "indefinite_fullset[T, S, mu]")
                (("1"
                  (case-replace "(LAMBDA n:
                           integral[T, S, contraction(mu, A!1(n))](h!1))=LAMBDA n: integral[T, S, mu](A!1(n), h!1)")
                  (("1" (hide -1)
                    (("1" (expand "convergent?")
                      (("1" (inst + "integral[T, S, mu](h!1)") nil
                        nil))
                      nil))
                    nil)
                   ("2" (apply-extensionality :hide? t)
                    (("1" (expand "integral" 1 2)
                      (("1" (inst - "x!1")
                        (("1" (rewrite "contraction_integral" 1)
                          (("1" (expand "measurable_set?")
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (skosimp)
                      (("2" (expand "integrable?" 1)
                        (("2"
                          (rewrite "indefinite_integrable[T, S, mu]")
                          (("2" (expand "measurable_set?")
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("3" (expand "measurable_set?")
                      (("3" (propax) nil nil)) nil))
                    nil)
                   ("3" (skosimp)
                    (("3" (expand "integrable?" 1)
                      (("3" (rewrite "indefinite_integrable[T, S, mu]")
                        (("3" (expand "measurable_set?")
                          (("3" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("4" (expand "measurable_set?")
                    (("4" (propax) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (propax) nil nil))
            nil)
           ("2" (skosimp)
            (("2" (rewrite "contraction_integrable" 1)
              (("1" (rewrite "indefinite_integrable[T, S, mu]")
                (("1" (expand "measurable_set?")
                  (("1" (propax) nil nil)) nil))
                nil)
               ("2" (expand "measurable_set?") (("2" (propax) nil nil))
                nil))
              nil))
            nil)
           ("3" (expand "measurable_set?") (("3" (propax) nil nil))
            nil))
          nil))
        nil)
       ("2" (flatten)
        (("2" (name "F" "lambda n: *[T](phi(IUnion(n,A!1)),h!1)")
          (("2" (case "forall n: integrable?[T, S, mu](F(n))")
            (("1" (case "pointwise_converges_upto?(F,h!1)")
              (("1"
                (lemma "monotone_convergence_scaf[T, S, mu]"
                 ("f" "h!1" "F" "F"))
                (("1" (replace -2 -1)
                  (("1" (replace 1 -1)
                    (("1" (hide 2)
                      (("1" (expand "bounded?")
                        (("1" (split)
                          (("1" (expand "convergent?")
                            (("1" (skosimp)
                              (("1"
                                (expand "bounded_above?")
                                (("1"
                                  (inst + "l!1")
                                  (("1"
                                    (skolem + "n!1")
                                    (("1"
                                      (expand "o ")
                                      (("1"
                                        (expand
                                         "pointwise_converges_upto?")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (case-replace
                                             "series(LAMBDA n:
                            integral[T, S, contraction(mu, A!1(n))](h!1))=integral[T,S,mu] o F")
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (hide-all-but
                                                 (-2 -6 1 -3))
                                                (("1"
                                                  (rewrite
                                                   "metric_convergence_def")
                                                  (("1"
                                                    (expand
                                                     "metric_converges_to")
                                                    (("1"
                                                      (inst-cp - "n!1")
                                                      (("1"
                                                        (inst
                                                         -4
                                                         "integral[T, S, mu](F(n!1))-l!1")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (inst
                                                             -
                                                             "n!1+n!2")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "n!1+n!2")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (expand
                                                                   "ball")
                                                                  (("1"
                                                                    (expand
                                                                     "o ")
                                                                    (("1"
                                                                      (expand
                                                                       "pointwise_increasing?")
                                                                      (("1"
                                                                        (lemma
                                                                         "integral_ae_le[T, S, mu]"
                                                                         ("f1"
                                                                          "F(n!1)"
                                                                          "f2"
                                                                          "F(n!1 + n!2)"))
                                                                        (("1"
                                                                          (split)
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (hide-all-but
                                                                             (-1
                                                                              1))
                                                                            (("2"
                                                                              (expand
                                                                               "ae_le?")
                                                                              (("2"
                                                                                (expand
                                                                                 "pointwise_ae?")
                                                                                (("2"
                                                                                  (expand
                                                                                   "ae?")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "fullset")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "ae_in?")
                                                                                      (("2"
                                                                                        (inst
                                                                                         +
                                                                                         "emptyset")
                                                                                        (("1"
                                                                                          (skosimp)
                                                                                          (("1"
                                                                                            (expand
                                                                                             "member")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "x!1")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "increasing?")
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   -
                                                                                                   "n!1"
                                                                                                   "n!1+n!2")
                                                                                                  (("1"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (expand
                                                                                           "negligible_set?")
                                                                                          (("2"
                                                                                            (inst
                                                                                             +
                                                                                             "emptyset[T]")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "null_set?")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "mu_fin?")
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "mu")
                                                                                                  (("2"
                                                                                                    (typepred
                                                                                                     "mu")
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "measure?")
                                                                                                      (("2"
                                                                                                        (flatten)
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "measure_empty?")
                                                                                                          (("2"
                                                                                                            (replace
                                                                                                             -1)
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "subset?")
                                                                                                                (("2"
                                                                                                                  (skosimp)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide -6 2)
                                              (("2"
                                                (case
                                                 "forall n: series(LAMBDA n: integral[T, S, contraction(mu, A!1(n))](h!1))(n) =
       integral[T, S, mu](F(n))")
                                                (("1"
                                                  (rewrite
                                                   "extensionality_postulate"
                                                   -1)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (expand "o ")
                                                      (("1"
                                                        (replace
                                                         -1
                                                         1
                                                         rl)
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (apply-extensionality
                                                             :hide?
                                                             t)
                                                            (("1"
                                                              (expand
                                                               "measurable_set?")
                                                              (("1"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide -1 -2 2 -4)
                                                  (("2"
                                                    (induct "n")
                                                    (("1"
                                                      (expand "series")
                                                      (("1"
                                                        (expand
                                                         "sigma")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (inst
                                                             -
                                                             "n!1")
                                                            (("1"
                                                              (inst
                                                               -
                                                               "n!1")
                                                              (("1"
                                                                (rewrite
                                                                 "contraction_integral"
                                                                 +)
                                                                (("1"
                                                                  (expand
                                                                   "F")
                                                                  (("1"
                                                                    (rewrite
                                                                     "IUnion_0_def")
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (expand
                                                                   "measurable_set?")
                                                                  (("2"
                                                                    (propax)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (skosimp)
                                                      (("2"
                                                        (expand
                                                         "series")
                                                        (("2"
                                                          (expand
                                                           "sigma"
                                                           1)
                                                          (("2"
                                                            (replace
                                                             -1)
                                                            (("2"
                                                              (hide -1)
                                                              (("2"
                                                                (inst
                                                                 -2
                                                                 "1+j!1")
                                                                (("2"
                                                                  (rewrite
                                                                   "contraction_integral")
                                                                  (("1"
                                                                    (case-replace
                                                                     "F(1 + j!1)=+[T](*[T](phi[T,S](A!1(1 + j!1)), h!1),F(j!1))")
                                                                    (("1"
                                                                      (rewrite
                                                                       "integral_add[T,S,mu]")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2
                                                                       -1
                                                                       -2)
                                                                      (("2"
                                                                        (apply-extensionality
                                                                         :hide?
                                                                         t)
                                                                        (("2"
                                                                          (expand
                                                                           "+")
                                                                          (("2"
                                                                            (expand
                                                                             "F")
                                                                            (("2"
                                                                              (expand
                                                                               "*")
                                                                              (("2"
                                                                                (case-replace
                                                                                 "phi(IUnion(1 + j!1, A!1))(x!1)=phi[T, S](A!1(1 + j!1))(x!1)+phi(IUnion(j!1, A!1))(x!1)")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide
                                                                                   -2
                                                                                   2)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "phi")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "member")
                                                                                      (("2"
                                                                                        (hide
                                                                                         -1)
                                                                                        (("2"
                                                                                          (rewrite
                                                                                           "IUnion_n_def")
                                                                                          (("2"
                                                                                            (expand
                                                                                             "union")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "member")
                                                                                              (("2"
                                                                                                (case-replace
                                                                                                 "IUnion(j!1, A!1)(x!1)")
                                                                                                (("1"
                                                                                                  (case-replace
                                                                                                   "A!1(1 + j!1)(x!1)")
                                                                                                  (("1"
                                                                                                    (hide
                                                                                                     1)
                                                                                                    (("1"
                                                                                                      (typepred
                                                                                                       "A!1")
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "disjoint_indexed_measurable?")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "disjoint?")
                                                                                                          (("1"
                                                                                                            (expand
                                                                                                             "IUnion")
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "image")
                                                                                                              (("1"
                                                                                                                (expand
                                                                                                                 "Union")
                                                                                                                (("1"
                                                                                                                  (skosimp)
                                                                                                                  (("1"
                                                                                                                    (typepred
                                                                                                                     "a!1")
                                                                                                                    (("1"
                                                                                                                      (skolem
                                                                                                                       -
                                                                                                                       "k!1")
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -
                                                                                                                         "k!1"
                                                                                                                         "1+j!1")
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "disjoint?")
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "empty?")
                                                                                                                              (("1"
                                                                                                                                (inst
                                                                                                                                 -
                                                                                                                                 "x!1")
                                                                                                                                (("1"
                                                                                                                                  (grind)
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (expand
                                                                     "measurable_set?")
                                                                    (("2"
                                                                      (propax)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (expand
                                                       "measurable_set?")
                                                      (("3"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (expand
                                                   "measurable_set?")
                                                  (("3"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("4"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (expand
                                               "measurable_set?")
                                              (("3" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "bounded_below?")
                            (("2" (inst + "0")
                              (("2"
                                (skolem + "n!1")
                                (("2"
                                  (expand "o ")
                                  (("2"
                                    (inst - "n!1")
                                    (("2"
                                      (lemma
                                       "integral_nonneg[T, S, mu]"
                                       ("f" "F(n!1)"))
                                      (("2"
                                        (assert)
                                        (("2"
                                          (skosimp)
                                          (("2"
                                            (hide-all-but (1 -7))
                                            (("2"
                                              (inst - "x!1")
                                              (("2"
                                                (expand "F")
                                                (("2"
                                                  (expand "*")
                                                  (("2"
                                                    (expand "phi")
                                                    (("2"
                                                      (lift-if)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (propax) nil nil))
                nil)
               ("2" (hide 2)
                (("2" (expand "pointwise_converges_upto?")
                  (("2" (split)
                    (("1" (expand "pointwise_convergence?")
                      (("1" (skosimp)
                        (("1" (hide -4)
                          (("1" (rewrite "metric_convergence_def")
                            (("1" (expand "metric_converges_to")
                              (("1"
                                (skosimp)
                                (("1"
                                  (expand "ball")
                                  (("1"
                                    (expand "member")
                                    (("1"
                                      (hide-all-but (-4 -5 1))
                                      (("1"
                                        (expand "F")
                                        (("1"
                                          (expand "*")
                                          (("1"
                                            (expand "phi")
                                            (("1"
                                              (expand "member")
                                              (("1"
                                                (expand "fullset")
                                                (("1"
                                                  (rewrite
                                                   "extensionality_postulate"
                                                   -1
                                                   :dir
                                                   rl)
                                                  (("1"
                                                    (inst - "x!1")
                                                    (("1"
                                                      (expand
                                                       "IUnion"
                                                       -1)
                                                      (("1"
                                                        (skolem
                                                         -
                                                         "n!1")
                                                        (("1"
                                                          (inst
                                                           +
                                                           "n!1")
                                                          (("1"
                                                            (skosimp)
                                                            (("1"
                                                              (case-replace
                                                               "IUnion(i!1, A!1)(x!1)")
                                                              (("1"
                                                                (expand
                                                                 "abs")
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide
                                                                 2)
                                                                (("2"
                                                                  (expand
                                                                   "IUnion")
                                                                  (("2"
                                                                    (expand
                                                                     "image")
                                                                    (("2"
                                                                      (expand
                                                                       "Union")
                                                                      (("2"
                                                                        (inst
                                                                         +
                                                                         "A!1(n!1)")
                                                                        (("2"
                                                                          (inst
                                                                           +
                                                                           "n!1")
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "pointwise_increasing?")
                      (("2" (skosimp)
                        (("2" (expand "increasing?")
                          (("2" (skolem + ("i!1" "j!1"))
                            (("2" (flatten)
                              (("2"
                                (hide-all-but (-7 -6 -1 1))
                                (("2"
                                  (expand "F")
                                  (("2"
                                    (expand "*")
                                    (("2"
                                      (expand "phi")
                                      (("2"
                                        (expand "member")
                                        (("2"
                                          (inst - "x!1")
                                          (("2"
                                            (case-replace
                                             "IUnion(i!1, A!1)(x!1)")
                                            (("1"
                                              (case-replace
                                               "IUnion(j!1, A!1)(x!1)")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (hide 2 -3)
                                                (("2"
                                                  (expand "IUnion")
                                                  (("2"
                                                    (expand "image")
                                                    (("2"
                                                      (expand "Union")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (inst
                                                           +
                                                           "a!1")
                                                          (("2"
                                                            (typepred
                                                             "a!1")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (inst
                                                                 +
                                                                 "x!2")
                                                                (("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (assert)
                                              (("2"
                                                (lift-if 2)
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (replace -1 1 rl)
              (("2" (hide -3 -1 2)
                (("2" (induct "n")
                  (("1" (rewrite "IUnion_0_def")
                    (("1" (inst - "0")
                      (("1" (rewrite "contraction_integrable")
                        (("1" (expand "measurable_set?")
                          (("1" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp)
                    (("2" (rewrite "IUnion_n_def")
                      (("2" (inst - "1+j!1")
                        (("2" (rewrite "contraction_integrable" -2)
                          (("1"
                            (case-replace
                             "(*[T](phi(union(IUnion(j!1, A!1), A!1(1 + j!1))), h!1))=+[T]((*[T](phi(IUnion(j!1, A!1)), h!1)),*[T](phi[T, S](A!1(1 + j!1)), h!1))")
                            (("1" (hide -1)
                              (("1"
                                (rewrite "integrable_add[T, S, mu]" 1)
                                nil
                                nil))
                              nil)
                             ("2" (hide 2 -1 -2 -4)
                              (("2"
                                (expand "fullset")
                                (("2"
                                  (rewrite
                                   "extensionality_postulate"
                                   -1
                                   :dir
                                   rl)
                                  (("2"
                                    (apply-extensionality :hide? t)
                                    (("2"
                                      (expand "*")
                                      (("2"
                                        (expand "+")
                                        (("2"
                                          (expand "phi")
                                          (("2"
                                            (expand "union")
                                            (("2"
                                              (expand "member")
                                              (("2"
                                                (case-replace
                                                 "IUnion(j!1, A!1)(x!1)")
                                                (("1"
                                                  (expand "IUnion" -1)
                                                  (("1"
                                                    (expand "image")
                                                    (("1"
                                                      (expand "Union")
                                                      (("1"
                                                        (skosimp)
                                                        (("1"
                                                          (typepred
                                                           "a!1")
                                                          (("1"
                                                            (skolem
                                                             -
                                                             "n!1")
                                                            (("1"
                                                              (replace
                                                               -1)
                                                              (("1"
                                                                (hide
                                                                 -1
                                                                 -3)
                                                                (("1"
                                                                  (typepred
                                                                   "n!1")
                                                                  (("1"
                                                                    (typepred
                                                                     "A!1")
                                                                    (("1"
                                                                      (expand
                                                                       "disjoint_indexed_measurable?")
                                                                      (("1"
                                                                        (expand
                                                                         "disjoint?")
                                                                        (("1"
                                                                          (inst
                                                                           -
                                                                           "n!1"
                                                                           "1+j!1")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (expand
                                                                               "disjoint?")
                                                                              (("1"
                                                                                (expand
                                                                                 "intersection")
                                                                                (("1"
                                                                                  (expand
                                                                                   "empty?")
                                                                                  (("1"
                                                                                    (inst
                                                                                     -
                                                                                     "x!1")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "member")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "measurable_set?")
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (T formal-type-decl nil measure_contraction_props nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (S formal-const-decl "sigma_algebra" measure_contraction_props nil)
    (nnreal type-eq-decl nil real_types nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     nil)
    (set type-eq-decl nil sets nil)
    (measurable_set? const-decl "bool" measure_space_def nil)
    (measurable_set nonempty-type-eq-decl nil measure_space_def nil)
    (contraction const-decl "measure_type" measure_contraction nil)
    (mu formal-const-decl "measure_type" measure_contraction_props nil)
    (disjoint_indexed_measurable? const-decl "bool"
     generalized_measure_def nil)
    (disjoint_indexed_measurable nonempty-type-eq-decl nil
     generalized_measure_def nil)
    (integrable? const-decl "bool" integral nil)
    (measurable_function? const-decl "bool" measure_space_def nil)
    (measurable_function nonempty-type-eq-decl nil measure_space_def
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (integral const-decl "real" integral nil)
    (integrable? const-decl "bool" indefinite_integral nil)
    (integral const-decl "real" indefinite_integral nil)
    (convergent? const-decl "bool" topological_convergence "topology/")
    (indefinite_integrable formula-decl nil integral nil)
    (contraction_integral formula-decl nil measure_contraction nil)
    (prod_measurable application-judgement "measurable_function[T, S]"
     measure_contraction_props nil)
    (phi_is_simple application-judgement "simple"
     measure_contraction_props nil)
    (subset_algebra_fullset name-judgement "(S)"
     measure_contraction_props nil)
    (measurable_fullset name-judgement "measurable_set[T, S]"
     measure_contraction_props nil)
    (sigma_algebra_IUnion_rew application-judgement "(S)"
     measure_contraction_props nil)
    (A!1 skolem-const-decl "disjoint_indexed_measurable[T, S]"
     measure_contraction_props nil)
    (h!1 skolem-const-decl "measurable_function[T, S]"
     measure_contraction_props nil)
    (indefinite_fullset formula-decl nil indefinite_integral nil)
    (integrable nonempty-type-eq-decl nil integral nil)
    (indefinite_countably_additive formula-decl nil indefinite_integral
     nil)
    (contraction_integrable formula-decl nil measure_contraction nil)
    (IUnion const-decl "set[T]" nat_indexed_sets "sets_aux/")
    (sequence type-eq-decl nil sequences nil)
    (phi const-decl "nat" measure_space nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (integrable_add judgement-tcc nil integral nil)
    (pointwise_converges_upto? const-decl "bool" pointwise_convergence
     nil)
    (O const-decl "T3" function_props nil)
    (IUnion_n_def formula-decl nil nat_indexed_sets "sets_aux/")
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
    (image const-decl "set[R]" function_image nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (subset_algebra_intersection application-judgement "(S)"
     measure_contraction_props nil)
    (disjoint? const-decl "bool" sets nil)
    (<= const-decl "bool" reals nil) (Union const-decl "set" sets nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (union const-decl "set" sets nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (integral_add formula-decl nil integral nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sigma_0_neg formula-decl nil sigma_nat "reals/")
    (IUnion_0_def formula-decl nil nat_indexed_sets "sets_aux/")
    (sigma def-decl "real" sigma "reals/")
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (extensionality_postulate formula-decl nil functions nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (metric_convergence_def formula-decl nil metric_space
     "metric_space/")
    (ball const-decl "set[T]" metric_space_def "metric_space/")
    (pointwise_increasing? const-decl "bool" pointwise_convergence nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ae_le? const-decl "bool" measure_theory nil)
    (ae? const-decl "bool" measure_theory nil)
    (ae_in? const-decl "bool" measure_theory nil)
    (null_set? const-decl "bool" measure_theory nil)
    (mu const-decl "nnreal" measure_props nil)
    (measure_empty? const-decl "bool" generalized_measure_def nil)
    (subset? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (mu_fin? const-decl "bool" measure_props nil)
    (TRUE const-decl "bool" booleans nil)
    (increasing? const-decl "bool" real_fun_preds "reals/")
    (negligible nonempty-type-eq-decl nil measure_theory nil)
    (emptyset const-decl "set" sets nil)
    (negligible_set? const-decl "bool" measure_theory nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" sigma_countable
     "sigma_set/")
    (measurable_emptyset name-judgement "measurable_set"
     measure_contraction_props nil)
    (subset_algebra_emptyset name-judgement "(S)"
     measure_contraction_props nil)
    (fullset const-decl "set" sets nil)
    (pointwise_ae? const-decl "bool" measure_theory nil)
    (integral_ae_le formula-decl nil integral nil)
    (member const-decl "bool" sets nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (l!1 skolem-const-decl "real" measure_contraction_props nil)
    (n!1 skolem-const-decl "nat" measure_contraction_props nil)
    (F skolem-const-decl "[nat -> [T -> real]]"
     measure_contraction_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (metric_converges_to const-decl "bool" metric_space_def
     "metric_space/")
    (series const-decl "sequence[real]" series "series/")
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (integral_nonneg formula-decl nil integral nil)
    (bounded_below? const-decl "bool" real_fun_preds "reals/")
    (bounded? const-decl "bool" real_fun_preds "reals/")
    (monotone_convergence_scaf formula-decl nil
     integral_convergence_scaf nil)
    (j!1 skolem-const-decl "nat" measure_contraction_props nil)
    (i!1 skolem-const-decl "nat" measure_contraction_props nil)
    (a!1 skolem-const-decl
     "({y: set[T] | EXISTS (x: ({i | i <= i!1})): y = A!1(x)})"
     measure_contraction_props nil)
    (x!2 skolem-const-decl "({i | i <= i!1})" measure_contraction_props
     nil)
    (pointwise_convergence? const-decl "bool" pointwise_convergence
     nil)
    (IUnion const-decl "set[T]" indexed_sets nil)
    (n!1 skolem-const-decl "nat" measure_contraction_props nil)
    (i!1 skolem-const-decl "nat" measure_contraction_props nil))
   shostak)))