# Proofs

proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: finite_fubini_tonelli
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (expand "integrable1?")
   (typepred "g!1")
   (lemma "finite_fubini_tonelli_1" ("h" "g!1"))
   (("1"
     (flatten -1)
     (hide -2)
     (split -1)
     (("1" (expand "integrable1?") (propax))
      ("2" (hide 2) (rewrite "nn_integrable_is_integrable"))))
    ("2"
     (hide 2)
     (expand "nn_measurable?")
     (split)
     (("1" (rewrite "nn_integrable_is_measurable"))
      ("2" (hide -1) (grind))))))


proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: finite_fubini_tonelli
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (lemma "finite_fubini_tonelli_2" ("h" "g!1"))
   (("1"
     (assert)
     (hide 2)
     (typepred "g!1")
     (rewrite "nn_integrable_is_integrable"))
    ("2"
     (hide 2)
     (expand "nn_measurable?")
     (split)
     (("1" (typepred "g!1") (rewrite "nn_integrable_is_measurable"))
      ("2" (grind))))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (typepred "f!1")
   (lemma "integrable_pm_def" ("f0" "f!1"))
   (flatten)
   (split -1)
   (("1"
     (flatten)
     (hide -3 -4)
     (case "nn_measurable?[[T1, T2], sigma_times[T1, T2](S1, S2)]
                     (minus[[T1, T2]](f!1))")
     (("1"
       (case "nn_measurable?[[T1, T2], sigma_times[T1, T2](S1, S2)]
                       (plus[[T1, T2]](f!1))")
       (("1"
         (lemma "finite_fubini_tonelli_1" ("h" "minus(f!1)"))
         (("1"
           (lemma "finite_fubini_tonelli_1" ("h" "plus(f!1)"))
           (("1"
             (assert)
             (lemma "integrable1_diff"
              ("g1" "plus(f!1)" "h1" "minus(f!1)"))
             (case-replace "((-[[T1, T2]])(plus(f!1), minus(f!1)))=f!1")
             (assert)
             (hide-all-but 1)
             (apply-extensionality :hide? t)
             (grind))
            ("2" (propax))))
          ("2" (propax))))
        ("2"
         (hide-all-but (-2 1))
         (expand "nn_measurable?")
         (use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]")
         (replace -1)
         (hide-all-but 1)
         (grind))))
      ("2"
       (hide -1 2)
       (expand "nn_measurable?")
       (use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]")
       (assert)
       (hide-all-but 1)
       (grind))))
    ("2" (propax))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (typepred "f!1")
   (lemma "integrable_pm_def" ("f0" "f!1"))
   (flatten)
   (split -1)
   (("1"
     (flatten)
     (hide -3)
     (case "nn_measurable?[[T1, T2], sigma_times[T1, T2](S1, S2)]
                     (minus[[T1, T2]](f!1))")
     (("1"
       (case "nn_measurable?[[T1, T2], sigma_times[T1, T2](S1, S2)]
                       (plus[[T1, T2]](f!1))")
       (("1"
         (lemma "finite_fubini_tonelli_2" ("h" "minus(f!1)"))
         (("1"
           (lemma "finite_fubini_tonelli_2" ("h" "plus(f!1)"))
           (("1"
             (lemma "integrable2_diff"
              ("g2" "plus(f!1)" "h2" "minus(f!1)"))
             (("1"
               (case-replace
                "((-[[T1, T2]])(plus(f!1), minus(f!1)))=f!1")
               (hide-all-but 1)
               (apply-extensionality :hide? t)
               (grind))
              ("2" (assert)) ("3" (assert))))
            ("2" (propax))))
          ("2" (propax))))
        ("2"
         (expand "nn_measurable?")
         (use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]")
         (assert)
         (hide-all-but 1)
         (grind))))
      ("2"
       (expand "nn_measurable?")
       (use "integrable_is_measurable[[T1,T2],sigma_times(S1,S2),to_measure(fm_times(mu,nu))]")
       (assert)
       (hide-all-but 1)
       (grind))))
    ("2" (propax))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (rewrite "integral_pm")
   (lemma "integral_pm" ("f" "integral1(f!1)"))
   (replace -1)
   (hide -1)
   (lemma "finite_fubini_tonelli_3" ("g" "plus(f!1)"))
   (("1"
     (lemma "finite_fubini_tonelli_3" ("g" "minus(f!1)"))
     (("1"
       (assert)
       (replace -1)
       (replace -2)
       (hide -1 -2)
       (rewrite "integral_diff" 1 :dir rl)
       (rewrite "integral_diff" 1 :dir rl)
       (case-replace
        "plus(integral1(f!1)) - minus(integral1(f!1))=integral1(f!1)")
       (("1"
         (hide -1)
         (lemma "integral1_diff" ("g1" "plus(f!1)" "h1" "minus(f!1)"))
         (case-replace "plus(f!1) - minus(f!1)=f!1")
         (("1"
           (hide -1)
           (lemma "integral_ae_eq"
            ("f"
             "integral1(f!1)"
             "h"
             "integral1(plus(f!1)) - integral1(minus(f!1))"))
           (assert))
          ("2"
           (hide-all-but 1)
           (apply-extensionality :hide? t)
           (grind))))
        ("2"
         (hide 2)
         (name-replace "DRL" "integral1(f!1)")
         (apply-extensionality :hide? t)
         (grind))))
      ("2"
       (lemma "integrable_pm_def" ("f0" "f!1"))
       (lemma "nn_integrable_is_nn_integrable"
        ("f" "minus[[T1, T2]](f!1)"))
       (assert)
       (hide-all-but 1)
       (grind))))
    ("2"
     (lemma "nn_integrable_is_nn_integrable" ("f" "plus[[T1, T2]](f!1)"))
     (assert)
     (hide-all-but 1)
     (grind))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (rewrite "integral_pm")
   (lemma "integral_pm" ("f" "integral2(f!1)"))
   (replace -1)
   (hide -1)
   (lemma "finite_fubini_tonelli_4" ("g" "plus(f!1)"))
   (("1"
     (lemma "finite_fubini_tonelli_4" ("g" "minus(f!1)"))
     (("1"
       (replace -1)
       (replace -2)
       (hide -1 -2)
       (rewrite "integral_diff" 1 :dir rl)
       (rewrite "integral_diff" 1 :dir rl)
       (case-replace
        "plus(integral2(f!1)) - minus(integral2(f!1))=integral2(f!1)")
       (("1"
         (hide -1)
         (lemma "integral2_diff" ("g2" "plus(f!1)" "h2" "minus(f!1)"))
         (case-replace "plus(f!1) - minus(f!1)=f!1")
         (("1"
           (hide -1)
           (lemma "integral_ae_eq"
            ("f"
             "integral2(f!1)"
             "h"
             "integral2(plus(f!1)) - integral2(minus(f!1))"))
           (assert))
          ("2"
           (hide-all-but 1)
           (apply-extensionality :hide? t)
           (grind))))
        ("2"
         (name-replace "DRL" "integral2(f!1)")
         (hide 2)
         (apply-extensionality :hide? t)
         (grind))))
      ("2"
       (lemma "nn_integrable_is_nn_integrable"
        ("f" "minus[[T1, T2]](f!1)"))
       (assert)
       (hide-all-but 1)
       (grind))))
    ("2"
     (lemma "nn_integrable_is_nn_integrable" ("f" "plus[[T1, T2]](f!1)"))
     (assert)
     (hide-all-but 1)
     (grind))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (rewrite "integrable_abs_def" 1 :dir rl)
   (("1"
     (lemma "nn_integrable_is_integrable[T2,S2,to_measure(nu)]")
     (inst - "abs(LAMBDA y: h!1(x!1, y))")
     (hide 2)
     (typepred "h!1")
     (expand "bounded_measurable?")
     (flatten)
     (expand "bounded?")
     (skosimp)
     (lemma "measurable_x_section" ("x" "x!1" "m" "h!1"))
     (("1"
       (lemma "nn_integrable_le[T2, S2, to_measure(nu)]"
        ("g" "abs[T2](LAMBDA y: h!1(x!1, y))" "f" "lambda y: c!1"))
       (("1"
         (assert)
         (skolem + "y!1")
         (inst - "(x!1,y!1)")
         (expand "abs" 1)
         (assert))
        ("2" (assert) (rewrite "abs_measurable[T2, S2]"))
        ("3"
         (hide-all-but (-2 1))
         (lemma "nn_isf_is_nn_integrable[T2, S2, to_measure(nu)]")
         (inst - "LAMBDA y: c!1")
         (("1" (flatten))
          ("2"
           (expand "nn_isf?")
           (hide 2)
           (expand "isf?")
           (expand "mu_fin?")
           (expand "to_measure")
           (lemma "phi_is_simple[T2,S2]" ("X" "fullset[T2]"))
           (lemma "simple_scal[T2,S2]"
            ("c" "c!1" "h" "phi(fullset[T2])"))
           (expand "fullset")
           (expand "phi")
           (expand "member")
           (expand "*")
           (propax))))))
      ("2" (propax))))
    ("2"
     (typepred "h!1")
     (expand "bounded_measurable?")
     (flatten)
     (rewrite "measurable_x_section"))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (rewrite "integrable_abs_def" 1 :dir rl)
   (("1"
     (lemma "nn_integrable_is_integrable[T1,S1,to_measure(mu)]")
     (inst - "abs(LAMBDA x: h!1(x, y!1))")
     (hide 2)
     (typepred "h!1")
     (expand "bounded_measurable?")
     (flatten)
     (expand "bounded?")
     (skosimp)
     (lemma "measurable_y_section" ("y" "y!1" "m" "h!1"))
     (("1"
       (lemma "nn_integrable_le[T1, S1, to_measure(mu)]"
        ("g" "abs[T1](LAMBDA x: h!1(x, y!1))" "f" "lambda x: c!1"))
       (("1"
         (assert)
         (skosimp)
         (assert)
         (expand "abs" 1)
         (assert)
         (inst - "(x!1,y!1)")
         (assert))
        ("2" (rewrite "abs_measurable[T1, S1]"))
        ("3"
         (hide-all-but 1)
         (lemma "nn_isf_is_nn_integrable[T1,S1,to_measure(mu)]")
         (inst - "LAMBDA x: c!1")
         (("1" (flatten))
          ("2"
           (hide 2)
           (expand "nn_isf?")
           (expand "isf?")
           (expand "mu_fin?")
           (expand "to_measure")
           (lemma "phi_is_simple[T1,S1]" ("X" "fullset[T1]"))
           (lemma "simple_scal[T1,S1]"
            ("c" "c!1" "h" "phi(fullset[T1])"))
           (expand "fullset")
           (expand "phi")
           (expand "member")
           (expand "*")
           (propax))))))
      ("2" (propax))))
    ("2"
     (typepred "h!1")
     (expand "bounded_measurable?")
     (flatten)
     (hide -1 2)
     (rewrite "measurable_y_section"))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (case "FORALL (h: bounded_measurable[[T1, T2], sigma_times(S1, S2)]):
                (forall x,y: 0<=h(x,y)) => integrable?(LAMBDA x: integral(LAMBDA y: h(x, y)))")
   (("1"
     (skosimp)
     (typepred "h!1")
     (inst-cp - "plus(h!1)")
     (("1"
       (inst - "minus(h!1)")
       (("1"
         (split -2)
         (("1"
           (split -3)
           (("1"
             (lemma "integrable_diff"
              ("f1"
               "LAMBDA x: integral(LAMBDA y: plus(h!1)(x, y))"
               "f2"
               "LAMBDA x: integral(LAMBDA y: minus(h!1)(x, y))"))
             (("1"
               (case-replace
                "((-[T1])
                                      (LAMBDA x: integral(LAMBDA y: plus(h!1)(x, y)),
                                       LAMBDA x: integral(LAMBDA y: minus(h!1)(x, y))))=(LAMBDA x: integral(LAMBDA y: h!1(x, y)))")
               (("1"
                 (expand "-" 1)
                 (apply-extensionality 1 :hide? t)
                 (("1"
                   (lemma "integral_pm" ("f" "LAMBDA y: h!1(x!1, y)"))
                   (("1"
                     (expand "plus")
                     (expand "minus")
                     (replace -1 1 rl)
                     (propax))
                    ("2" (rewrite "integrable_x_section"))))
                  ("2" (skosimp) (rewrite "integrable_x_section"))
                  ("3"
                   (skosimp)
                   (lemma "integrable_x_section" ("x" "x!1" "h" "h!1"))
                   (lemma "integrable_minus"
                    ("f" "LAMBDA y: h!1(x!1, y)"))
                   (("1" (expand "minus") (propax)) ("2" (propax))))
                  ("4"
                   (skosimp)
                   (lemma "integrable_x_section" ("x" "x!1" "h" "h!1"))
                   (lemma "integrable_plus"
                    ("f" "LAMBDA y: h!1(x!1, y)"))
                   (("1" (expand "plus") (propax)) ("2" (propax))))))
                ("2" (skosimp) (rewrite "integrable_x_section"))))
              ("2" (propax))
              ("3"
               (skosimp)
               (lemma "integrable_x_section" ("x" "x!1" "h" "h!1"))
               (hide-all-but (-1 1))
               (lemma "integrable_minus[T2, S2, to_measure(nu)]"
                ("f" "LAMBDA y: h!1(x!1, y)"))
               (("1" (expand "minus") (propax)) ("2" (propax))))
              ("4" (propax))
              ("5"
               (skosimp)
               (lemma "integrable_x_section" ("x" "x!1" "h" "h!1"))
               (lemma "integrable_plus[T2, S2, to_measure(nu)]"
                ("f" "LAMBDA y: h!1(x!1, y)"))
               (("1" (expand "plus") (propax)) ("2" (propax))))))
            ("2" (hide-all-but 1) (grind))))
          ("2" (hide-all-but 1) (grind))))
        ("2"
         (hide-all-but (-1 1))
         (expand "bounded_measurable?")
         (flatten)
         (split)
         (("1"
           (hide -2)
           (expand "bounded?")
           (skosimp)
           (inst + "c!1")
           (skosimp)
           (inst - "x!1")
           (grind))
          ("2" (rewrite "minus_measurable"))))))
      ("2"
       (hide 2)
       (expand "bounded_measurable?")
       (flatten)
       (split)
       (("1"
         (hide -2)
         (expand "bounded?")
         (skosimp)
         (inst + "c!1")
         (skosimp)
         (inst - "x!1")
         (grind))
        ("2" (rewrite "plus_measurable"))))))
    ("2"
     (hide 2)
     (skosimp)
     (case "forall x: bounded_measurable?(LAMBDA y: h!1(x, y))")
     (("1"
       (case "forall x: integrable?(LAMBDA y: h!1(x, y))")
       (("1"
         (lemma "nn_measurable_def" ("f" "h!1"))
         (split -1)
         (("1"
           (flatten -1)
           (hide -2)
           (split -1)
           (("1"
             (skosimp)
             (typepred "w!1")
             (case "forall (n:nat): integrable?(LAMBDA x: isf_integral(LAMBDA y: w!1(n)(x, y)))")
             (("1"
               (lemma "monotone_convergence_scaf[T1,S1,to_measure(mu)]"
                ("f"
                 "LAMBDA x: integral(LAMBDA y: h!1(x, y))"
                 "F"
                 "lambda (n:nat): LAMBDA x: isf_integral(LAMBDA y: w!1(n)(x, y))"))
               (("1"
                 (replace 1 -1)
                 (hide 2)
                 (split)
                 (("1"
                   (expand "pointwise_converges_upto?")
                   (flatten)
                   (split)
                   (("1"
                     (expand "pointwise_convergence?")
                     (skosimp)
                     (lemma
                      "monotone_convergence_scaf[T2,S2,to_measure(nu)]"
                      ("f"
                       "LAMBDA y: h!1(x!1, y)"
                       "F"
                       "lambda (n:nat): LAMBDA y: w!1(n)(x!1, y)"))
                     (("1"
                       (expand "converges_upto?")
                       (split -1)
                       (("1"
                         (flatten)
                         (expand "o")
                         (case-replace
                          "(LAMBDA (n: nat): integral(LAMBDA y: w!1(n)(x!1, y)))=LAMBDA (n: nat):
                                               isf_integral(LAMBDA y: w!1(n)(x!1, y))")
                         (("1"
                           (apply-extensionality :hide? t)
                           (("1"
                             (rewrite "isf_integral")
                             (rewrite "isf_x_section" 1)
                             (expand "isf?")
                             (expand "mu_fin?")
                             (expand "to_measure")
                             (expand "increasing_nn_simple?")
                             (inst -5 "x!2")
                             (expand "nn_simple?")
                             (flatten))
                            ("2"
                             (skosimp)
                             (rewrite "isf_x_section" 1)
                             (expand "isf?")
                             (expand "mu_fin?")
                             (expand "to_measure")
                             (expand "increasing_nn_simple?")
                             (inst -5 "n!1")
                             (expand "nn_simple?")
                             (flatten))
                            ("3"
                             (skosimp)
                             (lemma
                              "isf_is_integrable[T2, S2, to_measure(nu)]")
                             (inst - "LAMBDA y: w!1(n!1)(x!1, y)")
                             (rewrite "isf_x_section")
                             (expand "isf?")
                             (expand "mu_fin?")
                             (expand "to_measure")
                             (expand "increasing_nn_simple?")
                             (inst -5 "n!1")
                             (expand "nn_simple?")
                             (flatten))))
                          ("2"
                           (skosimp)
                           (rewrite "isf_x_section")
                           (expand "isf?")
                           (expand "mu_fin?")
                           (expand "to_measure")
                           (expand "increasing_nn_simple?")
                           (inst -5 "n!1")
                           (expand "nn_simple?")
                           (flatten))))
                        ("2"
                         (expand "pointwise_converges_upto?")
                         (hide 2)
                         (split)
                         (("1"
                           (expand "pointwise_convergence?")
                           (skolem + "y!1")
                           (inst -3 "(x!1,y!1)"))
                          ("2"
                           (expand "pointwise_increasing?")
                           (skolem + "y!1")
                           (inst -4 "(x!1,y!1)"))))
                        ("3"
                         (hide 2)
                         (expand "o ")
                         (expand "bounded?")
                         (split)
                         (("1"
                           (expand "bounded_above?")
                           (inst -6 "x!1")
                           (expand "bounded_measurable?")
                           (flatten)
                           (expand "bounded?")
                           (skosimp)
                           (inst + "c!1*nu(fullset[T2])")
                           (skolem + "n!1")
                           (case "forall y: w!1(n!1)(x!1,y) <= c!1")
                           (("1"
                             (expand "increasing_nn_simple?")
                             (flatten)
                             (hide -2 -4 -5)
                             (lemma "integral_ae_le"
                              ("f1"
                               "LAMBDA y: w!1(n!1)(x!1, y)"
                               "f2"
                               "c!1*phi(fullset[T2])"))
                             (("1"
                               (split -1)
                               (("1"
                                 (name-replace
                                  "LHS"
                                  "integral(LAMBDA y: w!1(n!1)(x!1, y))")
                                 (hide-all-but (-1 1))
                                 (rewrite "integral_scal" -1)
                                 (rewrite "integral_phi" -1)
                                 (("1"
                                   (expand "mu")
                                   (expand "to_measure")
                                   (propax))
                                  ("2"
                                   (expand "mu_fin?")
                                   (expand "to_measure")
                                   (propax))))
                                ("2"
                                 (hide-all-but (1 -1))
                                 (expand "ae_le?")
                                 (expand "pointwise_ae?")
                                 (expand "ae?")
                                 (expand "fullset")
                                 (expand "phi")
                                 (expand "ae_in?")
                                 (expand "member")
                                 (inst + "emptyset[T2]")
                                 (skosimp)
                                 (expand "*")
                                 (inst - "x!2"))))
                              ("2"
                               (hide 2)
                               (inst -2 "n!1")
                               (expand "nn_simple?")
                               (flatten)
                               (lemma
                                "isf_is_integrable[T2, S2, to_measure(nu)]")
                               (lemma "isf_x_section"
                                ("i" "w!1(n!1)" "x" "x!1"))
                               (("1"
                                 (inst
                                  -
                                  "LAMBDA (y: T2): w!1(n!1)(x!1, y)"))
                                ("2"
                                 (expand "isf?")
                                 (expand "mu_fin?")
                                 (expand "to_measure")
                                 (propax))))))
                            ("2"
                             (skosimp)
                             (hide -1 -2 -5 -7 2)
                             (inst - "(x!1,y!1)")
                             (inst - "x!1" "y!1")
                             (inst - "y!1")
                             (expand "abs")
                             (assert)
                             (rewrite "metric_convergence_def")
                             (expand "pointwise_increasing?")
                             (inst - "(x!1,y!1)")
                             (expand "metric_converges_to")
                             (expand "ball")
                             (expand "member")
                             (name "R" "w!1(n!1)(x!1, y!1)-c!1")
                             (case "R>0")
                             (("1"
                               (inst - "R")
                               (("1"
                                 (skosimp)
                                 (inst -3 "n!1+n!2")
                                 (assert)
                                 (expand "increasing?")
                                 (inst - "n!1" "n!1+n!2")
                                 (name-replace
                                  "DRL"
                                  "w!1(n!1 + n!2)(x!1, y!1)")
                                 (assert))
                                ("2" (assert))))
                              ("2" (hide-all-but (-1 1 2)) (grind))))))
                          ("2"
                           (expand "bounded_below?")
                           (inst + "0")
                           (skolem + "n!1")
                           (expand "increasing_nn_simple?")
                           (expand "nn_simple?")
                           (flatten)
                           (inst -2 "n!1")
                           (flatten)
                           (lemma "integral_nonneg"
                            ("f" "LAMBDA y: w!1(n!1)(x!1, y)"))
                           (("1"
                             (assert)
                             (skolem + "y!1")
                             (inst -2 "(x!1,y!1)")
                             (assert))
                            ("2"
                             (hide 2)
                             (lemma
                              "isf_is_integrable[T2, S2, to_measure(nu)]")
                             (inst - "LAMBDA y: w!1(n!1)(x!1, y)")
                             (rewrite "isf_x_section")
                             (expand "isf?")
                             (expand "mu_fin?")
                             (expand "to_measure")
                             (propax))))))))
                      ("2"
                       (skosimp)
                       (lemma
                        "isf_is_integrable[T2, S2, to_measure(nu)]")
                       (inst - "LAMBDA y: w!1(n!1)(x!1, y)")
                       (rewrite "isf_x_section")
                       (expand "isf?")
                       (expand "mu_fin?")
                       (expand "to_measure")
                       (expand "increasing_nn_simple?")
                       (expand "nn_simple?")
                       (inst -2 "n!1")
                       (flatten))))
                    ("2"
                     (expand "pointwise_increasing?")
                     (skosimp)
                     (expand "increasing?")
                     (skolem + ("i!1" "j!1"))
                     (flatten)
                     (lemma "isf_integral_le[T2,S2,to_measure(nu)]"
                      ("i1"
                       "LAMBDA y: w!1(i!1)(x!1, y)"
                       "i2"
                       "LAMBDA y: w!1(j!1)(x!1, y)"))
                     (("1"
                       (assert)
                       (skolem + "y!1")
                       (inst -5 "(x!1,y!1)")
                       (inst -5 "i!1" "j!1")
                       (assert))
                      ("2"
                       (rewrite "isf_x_section")
                       (expand "increasing_nn_simple?")
                       (flatten)
                       (inst -3 "j!1")
                       (expand "nn_simple?")
                       (flatten)
                       (expand "isf?")
                       (expand "mu_fin?")
                       (expand "to_measure")
                       (propax))
                      ("3"
                       (rewrite "isf_x_section")
                       (expand "isf?")
                       (expand "mu_fin?")
                       (expand "to_measure")
                       (expand "increasing_nn_simple?")
                       (flatten)
                       (inst -3 "i!1")
                       (expand "nn_simple?")
                       (flatten))))))
                  ("2"
                   (expand "o" 1)
                   (expand "bounded?")
                   (split)
                   (("1"
                     (typepred "h!1")
                     (expand "bounded_measurable?" -1)
                     (flatten)
                     (expand "bounded?" -1)
                     (skosimp)
                     (case "forall (n:nat,x,y): w!1(n)(x,y) <= c!1")
                     (("1"
                       (expand "bounded_above?")
                       (inst + "c!1 * mu(fullset[T1]) * nu(fullset[T2])")
                       (skolem + "n!1")
                       (inst -4 "n!1")
                       (lemma "integral_ae_le"
                        ("f1"
                         "LAMBDA x: isf_integral(LAMBDA y: w!1(n!1)(x, y))"
                         "f2"
                         "(c!1*nu(fullset[T2]))*phi(fullset[T1])"))
                       (("1"
                         (name-replace "LHS"
                          "integral(LAMBDA x: isf_integral(LAMBDA y: w!1(n!1)(x, y)))")
                         (split -1)
                         (("1"
                           (rewrite "integral_scal" -1)
                           (rewrite "integral_phi" -1)
                           (("1"
                             (expand "mu")
                             (expand "to_measure")
                             (assert))
                            ("2"
                             (expand "mu_fin?")
                             (expand "to_measure")
                             (propax))))
                          ("2"
                           (hide 2)
                           (expand "ae_le?")
                           (expand "pointwise_ae?")
                           (expand "ae?")
                           (expand "fullset" 1 2)
                           (expand "fullset" 1 2)
                           (expand "ae_in?")
                           (inst + "emptyset[T1]")
                           (skosimp)
                           (expand "member")
                           (expand "*" 2)
                           (expand "phi")
                           (expand "member")
                           (expand "increasing_nn_simple?")
                           (flatten)
                           (inst -5 "n!1")
                           (expand "nn_simple?")
                           (flatten)
                           (lemma "isf_integral_le"
                            ("i1"
                             "LAMBDA y: w!1(n!1)(x!1, y)"
                             "i2"
                             "c!1*phi(fullset[T2])"))
                           (("1"
                             (split -1)
                             (("1"
                               (name-replace "LHS1"
                                "isf_integral(LAMBDA y: w!1(n!1)(x!1, y))")
                               (rewrite "isf_integral_scal" -1)
                               (("1"
                                 (rewrite "isf_integral_phi" -1)
                                 (("1"
                                   (expand "mu")
                                   (expand "to_measure")
                                   (assert))
                                  ("2"
                                   (expand "mu_fin?")
                                   (expand "to_measure")
                                   (propax))))
                                ("2"
                                 (rewrite "isf_phi" 1)
                                 (expand "mu_fin?")
                                 (expand "to_measure")
                                 (propax))))
                              ("2"
                               (skolem + "y!1")
                               (expand "*")
                               (expand "fullset")
                               (expand "phi")
                               (expand "member")
                               (inst - "n!1" "x!1" "y!1"))))
                            ("2"
                             (rewrite "isf_scal")
                             (rewrite "isf_phi")
                             (expand "mu_fin?")
                             (expand "to_measure")
                             (propax))
                            ("3"
                             (rewrite "isf_x_section")
                             (expand "isf?")
                             (expand "mu_fin?")
                             (expand "to_measure")
                             (propax))))))
                        ("2" (propax))
                        ("3"
                         (skosimp)
                         (expand "increasing_nn_simple?")
                         (flatten)
                         (expand "nn_simple?")
                         (inst -5 "n!1")
                         (flatten)
                         (rewrite "isf_x_section" 1)
                         (expand "isf?")
                         (expand "mu_fin?")
                         (expand "to_measure")
                         (propax))))
                      ("2"
                       (hide-all-but (-1 -5 -8 1))
                       (skosimp)
                       (inst - "(x!1,y!1)")
                       (inst - "x!1" "y!1")
                       (expand "abs")
                       (expand "pointwise_converges_upto?")
                       (flatten)
                       (assert)
                       (expand "pointwise_convergence?")
                       (expand "pointwise_increasing?")
                       (inst - "(x!1,y!1)")
                       (inst - "(x!1,y!1)")
                       (rewrite "metric_convergence_def")
                       (expand "metric_converges_to")
                       (expand "ball")
                       (expand "member")
                       (name "R" "w!1(n!1)(x!1, y!1)-c!1")
                       (case "R>0")
                       (("1"
                         (inst - "R")
                         (("1"
                           (skosimp)
                           (inst - "n!1+n!2")
                           (expand "increasing?")
                           (inst - "n!1" "n!1+n!2")
                           (assert)
                           (grind))
                          ("2" (assert))))
                        ("2" (assert))))))
                    ("2"
                     (expand "bounded_below?")
                     (inst + "0")
                     (skolem + "n!1")
                     (inst - "n!1")
                     (lemma "integral_nonneg[T1,S1,to_measure(mu)]"
                      ("f"
                       "LAMBDA x: isf_integral(LAMBDA y: w!1(n!1)(x, y))"))
                     (("1"
                       (assert)
                       (skosimp)
                       (hide 2)
                       (expand "increasing_nn_simple?")
                       (flatten)
                       (expand "nn_simple?")
                       (inst - "n!1")
                       (flatten)
                       (lemma "isf_x_section" ("i" "w!1(n!1)" "x" "x!1"))
                       (("1"
                         (lemma "isf_integral_pos"
                          ("i" "LAMBDA (y: T2): w!1(n!1)(x!1, y)"))
                         (("1"
                           (assert)
                           (skolem + "y!1")
                           (inst - "(x!1,y!1)")
                           (assert))
                          ("2" (propax))))
                        ("2"
                         (expand "isf?")
                         (expand "mu_fin?")
                         (expand "to_measure")
                         (propax))))
                      ("2" (propax))
                      ("3"
                       (skosimp)
                       (expand "increasing_nn_simple?")
                       (expand "nn_simple?")
                       (flatten)
                       (inst -2 "n!1")
                       (flatten)
                       (rewrite "isf_x_section" 1)
                       (expand "isf?")
                       (expand "mu_fin?")
                       (expand "to_measure")
                       (propax))))))))
                ("2" (propax)) ("3" (propax))))
              ("2"
               (skosimp)
               (lemma "isf_integral_x" ("i" "w!1(n!1)"))
               (("1" (propax))
                ("2"
                 (expand "increasing_nn_simple?")
                 (flatten)
                 (inst - "n!1")
                 (expand "isf?")
                 (expand "mu_fin?")
                 (expand "to_measure")
                 (expand "nn_simple?")
                 (flatten))))
              ("3"
               (skosimp)
               (rewrite "isf_x_section" 1)
               (expand "increasing_nn_simple?")
               (flatten)
               (inst - "n!1")
               (expand "nn_simple?")
               (flatten)
               (expand "isf?")
               (expand "mu_fin?")
               (expand "to_measure")
               (propax))))
            ("2"
             (typepred "h!1")
             (expand "bounded_measurable?")
             (flatten))))
          ("2" (propax))))
        ("2"
         (skosimp)
         (inst - "x!1")
         (hide -2 -3 2)
         (use "bounded_measurable_is_integrable[T2,S2,nu]"))))
      ("2"
       (skosimp)
       (hide-all-but 1)
       (typepred "h!1")
       (expand "bounded_measurable?")
       (flatten)
       (split)
       (("1"
         (hide -2)
         (expand "bounded?")
         (skosimp)
         (inst + "c!1")
         (skosimp)
         (inst - "(x!1, x!2)"))
        ("2"
         (lemma "measurable_x_section" ("x" "x!1" "m" "h!1"))
         (("1" (propax)) ("2" (propax))))))))
    ("3" (skosimp*) (rewrite "integrable_x_section"))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (case "FORALL (h: bounded_measurable[[T1, T2], sigma_times(S1, S2)]):
                 (forall x,y: 0<=h(x,y)) => integrable?(LAMBDA y: integral(LAMBDA x: h(x, y)))")
   (("1"
     (skosimp)
     (typepred "h!1")
     (inst-cp - "plus(h!1)")
     (("1"
       (inst - "minus(h!1)")
       (("1"
         (split -2)
         (("1"
           (split -3)
           (("1"
             (lemma "integrable_diff"
              ("f1"
               "LAMBDA y: integral(LAMBDA x: plus(h!1)(x, y))"
               "f2"
               "LAMBDA y: integral(LAMBDA x: minus(h!1)(x, y))"))
             (("1"
               (case-replace
                "((-[T2])
                                      (LAMBDA y: integral(LAMBDA x: plus(h!1)(x, y)),
                                       LAMBDA y: integral(LAMBDA x: minus(h!1)(x, y))))=(LAMBDA y: integral(LAMBDA x: h!1(x, y)))")
               (("1"
                 (expand "-")
                 (apply-extensionality :hide? t)
                 (("1"
                   (hide 2)
                   (rewrite "integral_diff" 1 :dir rl)
                   (("1"
                     (case-replace
                      "((LAMBDA x: plus(h!1)(x, x!1)) -
                                      (LAMBDA x: minus(h!1)(x, x!1)))=(LAMBDA x: h!1(x, x!1))")
                     (apply-extensionality :hide? t)
                     (hide-all-but 1)
                     (grind))
                    ("2"
                     (lemma "integrable_y_section" ("h" "h!1" "y" "x!1"))
                     (lemma "integrable_minus"
                      ("f" "LAMBDA x: h!1(x, x!1)"))
                     (("1" (expand "minus") (propax)) ("2" (propax))))
                    ("3"
                     (lemma "integrable_y_section" ("h" "h!1" "y" "x!1"))
                     (lemma "integrable_plus"
                      ("f" "LAMBDA x: h!1(x, x!1)"))
                     (("1" (expand "plus") (propax)) ("2" (propax))))))
                  ("2" (skosimp) (rewrite "integrable_y_section"))
                  ("3"
                   (skosimp)
                   (lemma "integrable_y_section" ("h" "h!1" "y" "x!1"))
                   (lemma "integrable_minus"
                    ("f" "LAMBDA x: h!1(x, x!1)"))
                   (("1" (expand "minus") (propax)) ("2" (propax))))
                  ("4"
                   (skosimp)
                   (lemma "integrable_y_section" ("h" "h!1" "y" "x!1"))
                   (lemma "integrable_plus"
                    ("f" "LAMBDA x: h!1(x, x!1)"))
                   (("1" (expand "plus") (propax)) ("2" (propax))))))
                ("2" (skosimp) (rewrite "integrable_y_section"))))
              ("2" (propax))
              ("3"
               (skosimp)
               (lemma "integrable_y_section" ("y" "y!1" "h" "h!1"))
               (lemma "integrable_minus[T1, S1, to_measure(mu)]"
                ("f" "LAMBDA x: h!1(x, y!1)"))
               (("1" (expand "minus") (propax)) ("2" (propax))))
              ("4" (propax))
              ("5"
               (skosimp)
               (lemma "integrable_y_section" ("y" "y!1" "h" "h!1"))
               (lemma "integrable_plus[T1, S1, to_measure(mu)]"
                ("f" "LAMBDA x: h!1(x, y!1)"))
               (("1" (expand "plus") (propax)) ("2" (propax))))))
            ("2" (hide-all-but 1) (grind))))
          ("2" (hide-all-but 1) (grind))))
        ("2"
         (hide-all-but (-1 1))
         (expand "bounded_measurable?")
         (flatten)
         (split)
         (("1"
           (hide -2)
           (expand "bounded?")
           (skosimp)
           (inst + "c!1")
           (skosimp)
           (inst - "x!1")
           (grind))
          ("2" (rewrite "minus_measurable"))))))
      ("2"
       (hide 2)
       (expand "bounded_measurable?")
       (flatten)
       (split)
       (("1"
         (hide -2)
         (expand "bounded?")
         (skosimp)
         (inst + "c!1")
         (skosimp)
         (inst - "x!1")
         (grind))
        ("2" (rewrite "plus_measurable"))))))
    ("2"
     (hide 2)
     (skosimp)
     (case "forall y: bounded_measurable?(LAMBDA x: h!1(x, y))")
     (("1"
       (case "forall y: integrable?(LAMBDA x: h!1(x, y))")
       (("1"
         (lemma "nn_measurable_def" ("f" "h!1"))
         (replace -4)
         (flatten)
         (hide -2)
         (split -1)
         (("1"
           (skosimp)
           (typepred "h!1")
           (expand "bounded_measurable?" -1)
           (flatten)
           (expand "bounded?" -1)
           (hide -2)
           (skosimp)
           (case "forall (n:nat): isf?(w!1(n))")
           (("1"
             (case "forall (n:nat,x,y): 0<=w!1(n)(x,y)&w!1(n)(x,y)<=h!1(x,y)")
             (("1"
               (case "forall (n:nat): integrable?(LAMBDA y: isf_integral(LAMBDA x: w!1(n)(x, y)))")
               (("1"
                 (lemma "monotone_convergence_scaf[T2,S2,to_measure(nu)]"
                  ("f"
                   "LAMBDA y: integral(LAMBDA x: h!1(x, y))"
                   "F"
                   "lambda (n:nat): LAMBDA y: isf_integral(LAMBDA x: w!1(n)(x, y))"))
                 (("1"
                   (replace 1 -1)
                   (hide 2)
                   (split)
                   (("1"
                     (expand "pointwise_converges_upto?")
                     (flatten)
                     (split)
                     (("1"
                       (expand "pointwise_convergence?")
                       (skolem + "y!1")
                       (lemma
                        "monotone_convergence_scaf[T1,S1,to_measure(mu)]"
                        ("f"
                         "LAMBDA x: h!1(x, y!1)"
                         "F"
                         "lambda (n:nat): LAMBDA x: w!1(n)(x, y!1)"))
                       (("1"
                         (expand "converges_upto?")
                         (expand "o")
                         (assert)
                         (case-replace
                          "(LAMBDA (x_1: nat):
                                                  integral(LAMBDA x: w!1(x_1)(x, y!1)))=LAMBDA (n_1: nat):
                                               isf_integral(LAMBDA x: w!1(n_1)(x, y!1))")
                         (("1"
                           (hide -1)
                           (replace 1 -1)
                           (hide 2)
                           (split)
                           (("1"
                             (expand "pointwise_converges_upto?")
                             (split)
                             (("1"
                               (expand "pointwise_convergence?")
                               (skosimp)
                               (inst -5 "(x!1,y!1)"))
                              ("2"
                               (expand "pointwise_increasing?")
                               (skosimp)
                               (inst -6 "(x!1,y!1)"))))
                            ("2"
                             (expand "bounded?")
                             (split)
                             (("1"
                               (expand "bounded_above?")
                               (inst + "c!1*mu(fullset[T1])")
                               (skolem + "n!1")
                               (inst -2 "n!1" "_" "y!1")
                               (inst -3 "n!1")
                               (lemma "isf_y_section"
                                ("i" "w!1(n!1)" "y" "y!1"))
                               (("1"
                                 (lemma
                                  "isf_integral_le"
                                  ("i1"
                                   "LAMBDA x: w!1(n!1)(x, y!1)"
                                   "i2"
                                   "c!1*phi(fullset[T1])"))
                                 (("1"
                                   (split -1)
                                   (("1"
                                     (name-replace
                                      "LHS1"
                                      "isf_integral(LAMBDA x: w!1(n!1)(x, y!1))")
                                     (rewrite "isf_integral_scal")
                                     (("1"
                                       (rewrite "isf_integral_phi")
                                       (("1"
                                         (expand "mu")
                                         (expand "to_measure")
                                         (propax))
                                        ("2"
                                         (expand "mu_fin?")
                                         (expand "to_measure")
                                         (propax))))
                                      ("2"
                                       (rewrite "isf_phi")
                                       (expand "mu_fin?")
                                       (expand "to_measure")
                                       (propax))))
                                    ("2"
                                     (skosimp)
                                     (expand "fullset")
                                     (expand "phi")
                                     (expand "member")
                                     (expand "*")
                                     (hide-all-but (-3 -5 -10 1))
                                     (inst - "x!1")
                                     (inst - "(x!1,y!1)")
                                     (inst - "x!1" "y!1")
                                     (grind))))
                                  ("2"
                                   (rewrite "isf_scal")
                                   (rewrite "isf_phi")
                                   (expand "mu_fin?")
                                   (expand "to_measure")
                                   (propax))
                                  ("3" (propax))))
                                ("2" (propax))))
                              ("2"
                               (expand "bounded_below?")
                               (inst + "0")
                               (skolem + "n!1")
                               (inst -3 "n!1")
                               (lemma "isf_y_section"
                                ("y" "y!1" "i" "w!1(n!1)"))
                               (("1"
                                 (lemma
                                  "isf_integral_pos"
                                  ("i" "LAMBDA x: w!1(n!1)(x, y!1)"))
                                 (("1"
                                   (split -1)
                                   (("1" (assert))
                                    ("2"
                                     (skosimp)
                                     (inst - "n!1" "x!1" "y!1")
                                     (flatten)
                                     (assert))))
                                  ("2" (propax))))
                                ("2" (propax))))))))
                          ("2"
                           (apply-extensionality :hide? t)
                           (("1"
                             (inst -4 "x!1")
                             (lemma "isf_y_section"
                              ("i" "w!1(x!1)" "y" "y!1"))
                             (("1" (rewrite "isf_integral"))
                              ("2" (propax))))
                            ("2"
                             (skosimp)
                             (inst -4 "n!1")
                             (rewrite "isf_y_section" 1))
                            ("3"
                             (skolem + "n!1")
                             (inst -4 "n!1")
                             (lemma "isf_y_section"
                              ("y" "y!1" "i" "w!1(n!1)"))
                             (("1"
                               (lemma
                                "isf_is_integrable[T1, S1, to_measure(mu)]")
                               (inst - "LAMBDA x: w!1(n!1)(x, y!1)"))
                              ("2" (propax))))))
                          ("3"
                           (skosimp)
                           (inst -4 "n!1")
                           (lemma "isf_y_section"
                            ("y" "y!1" "i" "w!1(n!1)"))
                           (("1" (propax)) ("2" (propax))))))
                        ("2"
                         (skosimp)
                         (inst -3 "n!1")
                         (lemma "isf_y_section"
                          ("y" "y!1" "i" "w!1(n!1)"))
                         (("1" (rewrite "isf_is_integrable" 1))
                          ("2" (propax))))))
                      ("2"
                       (expand "pointwise_increasing?")
                       (skolem + "y!1")
                       (expand "increasing?")
                       (skolem + ("i!1" "j!1"))
                       (flatten)
                       (hide-all-but (1 -1 -7 -4))
                       (inst-cp - "i!1")
                       (inst - "j!1")
                       (lemma "isf_y_section" ("i" "w!1(i!1)" "y" "y!1"))
                       (("1"
                         (lemma "isf_y_section"
                          ("i" "w!1(j!1)" "y" "y!1"))
                         (("1"
                           (lemma "isf_integral_le"
                            ("i1"
                             "LAMBDA x: w!1(i!1)(x, y!1)"
                             "i2"
                             "LAMBDA x: w!1(j!1)(x, y!1)"))
                           (("1"
                             (assert)
                             (skosimp)
                             (inst -6 "(x!1,y!1)")
                             (inst -6 "i!1" "j!1")
                             (assert))
                            ("2" (propax)) ("3" (propax))))
                          ("2" (propax))))
                        ("2" (propax))))))
                    ("2"
                     (expand "o")
                     (expand "bounded?")
                     (split)
                     (("1"
                       (expand "bounded_above?")
                       (inst + "mu(fullset[T1])*nu(fullset[T2])*c!1")
                       (skolem + "n!1")
                       (inst - "n!1")
                       (inst - "n!1" "_" "_")
                       (inst - "n!1")
                       (lemma "integral_ae_le"
                        ("f1"
                         "LAMBDA y: isf_integral(LAMBDA x: w!1(n!1)(x, y))"
                         "f2"
                         "(c!1*mu(fullset[T1]))*phi(fullset[T2])"))
                       (("1"
                         (split -1)
                         (("1"
                           (name-replace "LHS"
                            "integral(LAMBDA y: isf_integral(LAMBDA x: w!1(n!1)(x, y)))")
                           (rewrite "integral_scal" -1)
                           (rewrite "integral_phi" -1)
                           (("1"
                             (expand "mu")
                             (expand "to_measure")
                             (propax))
                            ("2"
                             (expand "mu_fin?")
                             (expand "to_measure")
                             (propax))))
                          ("2"
                           (hide 2)
                           (expand "ae_le?")
                           (expand "pointwise_ae?")
                           (expand "ae?")
                           (expand "fullset" 1 2)
                           (expand "fullset" 1 2)
                           (expand "phi")
                           (expand "member")
                           (expand "ae_in?")
                           (expand "member")
                           (inst + " emptyset[T2]")
                           (skolem + "y!1")
                           (flatten)
                           (expand "*" 2)
                           (lemma "isf_y_section"
                            ("i" "w!1(n!1)" "y" "y!1"))
                           (("1"
                             (hide 1)
                             (lemma "isf_integral_le"
                              ("i1"
                               "LAMBDA x: w!1(n!1)(x, y!1)"
                               "i2"
                               "c!1*phi(fullset[T1])"))
                             (("1"
                               (split -1)
                               (("1"
                                 (rewrite "isf_integral_scal")
                                 (("1"
                                   (rewrite "isf_integral_phi")
                                   (("1"
                                     (assert)
                                     (expand "mu")
                                     (expand "to_measure")
                                     (assert))
                                    ("2"
                                     (expand "mu_fin?")
                                     (expand "to_measure")
                                     (propax))))
                                  ("2"
                                   (rewrite "isf_phi")
                                   (expand "mu_fin?")
                                   (expand "to_measure")
                                   (propax))))
                                ("2"
                                 (skosimp)
                                 (expand "fullset")
                                 (expand "phi")
                                 (expand "*")
                                 (expand "member")
                                 (inst - "x!1" "y!1")
                                 (flatten)
                                 (inst -10 "x!1" "y!1")
                                 (inst -6 "(x!1,y!1)")
                                 (assert))))
                              ("2"
                               (rewrite "isf_scal")
                               (rewrite "isf_phi")
                               (expand "mu_fin?")
                               (expand "to_measure")
                               (propax))
                              ("3" (propax))))
                            ("2" (propax))))))
                        ("2" (propax))
                        ("3" (skosimp) (rewrite "isf_y_section"))))
                      ("2"
                       (expand "bounded_below?")
                       (inst + "0")
                       (skolem + "n!1")
                       (inst - "n!1")
                       (inst - "n!1")
                       (lemma "isf_y_section" ("i" "w!1(n!1)"))
                       (("1"
                         (lemma "integral_nonneg"
                          ("f"
                           "LAMBDA y: isf_integral(LAMBDA x: w!1(n!1)(x, y))"))
                         (("1"
                           (assert)
                           (skolem + "y!1")
                           (hide 2)
                           (inst - "y!1")
                           (lemma "isf_integral_pos"
                            ("i" "LAMBDA x: w!1(n!1)(x, y!1)"))
                           (("1"
                             (assert)
                             (skosimp)
                             (inst -3 "n!1" "x!1" "y!1")
                             (flatten)
                             (assert))
                            ("2" (propax))))
                          ("2" (propax)) ("3" (propax))))
                        ("2" (propax))))))))
                  ("2" (propax)) ("3" (propax))))
                ("2"
                 (skosimp)
                 (inst -2 "n!1")
                 (rewrite "isf_integral_y" 1)
                 (hide-all-but (-2 1))
                 (case-replace
                  "(LAMBDA (x, y): w!1(n!1)(x, y))=w!1(n!1)")
                 (apply-extensionality :hide? t))
                ("3"
                 (skosimp)
                 (inst -2 "n!1")
                 (hide-all-but (-2 1))
                 (rewrite "isf_y_section"))))
              ("2"
               (hide-all-but (-3 1))
               (skosimp)
               (expand "pointwise_converges_upto?")
               (flatten)
               (typepred "w!1")
               (expand "increasing_nn_simple?")
               (flatten)
               (inst - "n!1")
               (expand "nn_simple?")
               (flatten)
               (inst - "(x!1,y!1)")
               (assert)
               (hide -1 -2 -3)
               (expand "pointwise_convergence?")
               (expand "pointwise_increasing?")
               (inst - "(x!1,y!1)")
               (inst - "(x!1,y!1)")
               (rewrite "metric_convergence_def")
               (expand "metric_converges_to")
               (name "R" "w!1(n!1)(x!1, y!1) - h!1(x!1, y!1)")
               (case "R>0")
               (("1"
                 (inst - "R")
                 (("1"
                   (skosimp)
                   (inst - "n!1+n!2")
                   (expand "ball")
                   (expand "increasing?")
                   (inst - "n!1" "n!1+n!2")
                   (grind))
                  ("2" (assert))))
                ("2" (assert))))))
            ("2"
             (typepred "w!1")
             (expand "increasing_nn_simple?")
             (flatten)
             (skosimp)
             (inst - "n!1")
             (expand "nn_simple?")
             (flatten)
             (expand "isf?")
             (expand "mu_fin?")
             (expand "to_measure")
             (propax))))
          ("2"
           (typepred "h!1")
           (expand "bounded_measurable?")
           (flatten))))
        ("2"
         (skosimp)
         (inst - "y!1")
         (lemma "bounded_measurable_is_integrable[T1,S1,mu]")
         (inst - "LAMBDA x: h!1(x, y!1)"))))
      ("2"
       (skosimp)
       (typepred "h!1")
       (expand "bounded_measurable?")
       (flatten)
       (hide 2 -3)
       (split)
       (("1"
         (hide -2)
         (expand "bounded?")
         (skosimp)
         (inst + "c!1")
         (skosimp)
         (inst - "(x!1,y!1)"))
        ("2"
         (lemma "measurable_y_section" ("m" "h!1" "y" "y!1"))
         (("1" (propax)) ("2" (propax))))))))
    ("3"
     (skosimp)
     (skosimp)
     (typepred "h!1")
     (lemma "bounded_measurable_is_integrable[T1, S1, mu]")
     (inst - "LAMBDA x: h!1(x, y1!1)")
     (hide 2 3)
     (expand "bounded_measurable?")
     (flatten)
     (split)
     (("1"
       (hide -2 -3)
       (expand "bounded?")
       (skosimp)
       (inst + "c!1")
       (skosimp)
       (inst - "(x!1,y1!1)"))
      ("2"
       (lemma "measurable_y_section" ("m" "h!1" "y" "y1!1"))
       (("1" (propax)) ("2" (propax))))))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (typepred "h!1")
   (lemma
    "bounded_measurable_is_integrable[[T1,T2],sigma_times(S1,S2),fm_times(mu,nu)]")
   (inst - "h!1")
   (rewrite "finite_fubini1" 1)
   (lemma "finite_integrable_is_integrable1" ("f" "h!1"))
   (("1"
     (lemma "integrable_integral_x_section" ("h" "h!1"))
     (lemma "integral_ae_eq[T1,S1,to_measure(mu)]"
      ("f"
       "LAMBDA x: integral(LAMBDA y: h!1(x, y))"
       "h"
       "integral1(h!1)"))
     (("1"
       (assert)
       (hide 2 -1 -3)
       (expand "ae_eq?")
       (expand "restrict")
       (expand "pointwise_ae?")
       (expand "ae?")
       (expand "fullset")
       (expand "ae_in?")
       (expand "member")
       (name "FF" "integral1(h!1)")
       (replace -1)
       (name "NI" "null_integrable1(h!1)")
       (expand "integral1" -2)
       (replace -1)
       (expand "member")
       (inst + "NI`1")
       (skosimp)
       (replace -2 2 rl)
       (assert)
       (hide -2)
       (lemma "null_integral1_def"
        ("h1" "h!1" "N1" "NI`1" "f" "NI`2" "x" "x!1"))
       (expand "member")
       (decompose-equality 1))
      ("2" (propax))
      ("3"
       (skosimp)
       (lemma "integrable_x_section" ("h" "h!1" "x" "x!1"))
       (propax))))
    ("2" (propax))))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (typepred "h!1")
   (lemma
    "bounded_measurable_is_integrable[[T1,T2],sigma_times(S1,S2),fm_times(mu,nu)]")
   (inst - "h!1")
   (rewrite "finite_fubini2" 1)
   (lemma "finite_integrable_is_integrable2" ("f" "h!1"))
   (("1"
     (lemma "integrable_integral_y_section" ("h" "h!1"))
     (lemma "integral_ae_eq[T2,S2,to_measure(nu)]"
      ("f"
       "LAMBDA y: integral(LAMBDA x: h!1(x, y))"
       "h"
       "integral2(h!1)"))
     (("1"
       (assert)
       (hide 2)
       (expand "ae_eq?")
       (expand "restrict")
       (expand "pointwise_ae?")
       (expand "ae?")
       (expand "fullset")
       (expand "ae_in?")
       (expand "member")
       (name "NI" "null_integrable2(h!1)")
       (inst + "NI`1")
       (skolem + "y!1")
       (flatten)
       (lemma "null_integral2_def"
        ("h2" "h!1" "N2" "NI`1" "g" "NI`2" "y" "y!1"))
       (expand "member")
       (assert)
       (expand "integral2")
       (expand "member")
       (replace -2)
       (assert)
       (decompose-equality))
      ("2" (propax)) ("3" (skosimp) (rewrite "integrable_y_section"))))
    ("2" (propax))))


proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-complete
description: nil
script:
  (""
   (typepred "S1")
   (expand "sigma_algebra?")
   (flatten)
   (expand "subset_algebra_empty?")
   (expand "member")
   (propax))


proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: finite_fubini
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (typepred "h!1")
   (lemma
    "bounded_measurable_is_integrable[[T1, T2], sigma_times(S1, S2),fm_times(mu, nu)]")
   (inst - "h!1"))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: product_measure
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (expand "m_times")
   (expand "product_measure_approx")
   (name "FF"
         "LAMBDA i,j:to_measure(fm_times
                                               (fm_contraction[T1, S1]
                                                (mu!1, A_of(mu!1)(i)),
                                                fm_contraction[T2, S2]
                                                (nu!1, A_of(nu!1)(j))))")
   (("1"
     (case "x_eq(x_sum(LAMBDA i:
                              x_sum(LAMBDA j: FF(i,j)(cross_product(X!1, Y!1)))),x_times(mu!1(X!1), nu!1(Y!1)))")
     (("1" (expand "FF") (propax))
      ("2"
       (hide 2)
       (case "forall i,j: x_eq(FF(i, j)(cross_product(X!1, Y!1)),fm_contraction[T1, S1](mu!1, A_of(mu!1)(i))(X!1)*fm_contraction[T2, S2](nu!1, A_of(nu!1)(j))(Y!1))")
       (("1"
         (hide -2)
         (lemma "x_sum_eq"
          ("S"
           "LAMBDA i:
                              x_sum(LAMBDA j: FF(i, j)(cross_product(X!1, Y!1)))"
           "T"
           "LAMBDA i:x_times(fm_contraction[T1, S1](mu!1, A_of(mu!1)(i))(X!1),nu!1(Y!1))"))
         (split -1)
         (("1"
           (name-replace "LHS"
            "x_sum(LAMBDA i:
                               x_sum(LAMBDA j: FF(i, j)(cross_product(X!1, Y!1))))")
           (lemma "sigma_finite_contraction_def[T1,S1]"
            ("nu" "mu!1" "E" "X!1"))
           (("1"
             (lemma "x_times_sum"
              ("x"
               "nu!1(Y!1)"
               "S"
               "LAMBDA i:
                                  (TRUE, fm_contraction(mu!1, A_of(mu!1)(i))(X!1))"
               "T"
               "LAMBDA i:
                                  x_times(fm_contraction[T1, S1]
                                              (mu!1, A_of(mu!1)(i))(X!1),
                                          nu!1(Y!1))"))
             (split -1)
             (("1"
               (name-replace "DRL1"
                "x_sum(LAMBDA i:
                                   x_times(fm_contraction[T1, S1]
                                               (mu!1, A_of(mu!1)(i))(X!1),
                                           nu!1(Y!1)))")
               (name-replace "DRL2"
                "x_sum(LAMBDA i:
                                   (TRUE, fm_contraction(mu!1, A_of(mu!1)(i))(X!1)))")
               (hide -4)
               (expand "x_times")
               (expand "x_eq")
               (flatten)
               (case-replace "LHS`1")
               (("1"
                 (assert)
                 (case-replace "mu!1(X!1)`1")
                 (("1"
                   (assert)
                   (case-replace "nu!1(Y!1)`1")
                   (("1" (assert))
                    ("2"
                     (assert)
                     (prop)
                     (("1" (assert)) ("2" (assert))))))
                  ("2"
                   (assert)
                   (case-replace "nu!1(Y!1)`1")
                   (("1" (assert) (prop) (assert)) ("2" (assert))))))
                ("2"
                 (assert)
                 (case-replace "nu!1(Y!1)`1")
                 (("1" (assert) (case-replace "DRL2`1") (assert))
                  ("2"
                   (assert)
                   (case-replace "DRL2`1")
                   (("1" (assert) (prop) (("1" (assert)) ("2" (assert))))
                    ("2" (assert))))))))
              ("2"
               (hide 2)
               (skosimp)
               (expand "x_times")
               (expand "x_times")
               (expand "x_eq")
               (case-replace "nu!1(Y!1)`1")
               (assert))))
            ("2" (expand "measurable_set?") (propax))))
          ("2"
           (hide 2)
           (skosimp)
           (expand "x_times")
           (lemma "x_sum_eq"
            ("S"
             "LAMBDA j: FF(i!1, j)(cross_product(X!1, Y!1))"
             "T"
             "lambda j: (TRUE,fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1))(X!1) *
                           fm_contraction[T2, S2](nu!1, A_of(nu!1)(j))(Y!1))"))
           (split)
           (("1"
             (name-replace "LHS"
              "x_sum(LAMBDA j: FF(i!1, j)(cross_product(X!1, Y!1)))")
             (inst - "i!1" "_")
             (name-replace "KX"
              "fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1))(X!1)")
             (lemma "x_times_sum"
              ("S"
               "LAMBDA j:(TRUE,fm_contraction[T2, S2](nu!1, A_of(nu!1)(j))(Y!1))"
               "x"
               "(TRUE,KX)"
               "T"
               "LAMBDA j:
                                  (TRUE,
                                   KX * fm_contraction[T2, S2](nu!1, A_of(nu!1)(j))(Y!1))"))
             (split)
             (("1"
               (name-replace "DRL1"
                "x_sum(LAMBDA j:
                                   (TRUE,
                                    KX * fm_contraction[T2, S2](nu!1, A_of(nu!1)(j))(Y!1)))")
               (lemma "sigma_finite_contraction_def"
                ("nu" "nu!1" "E" "Y!1"))
               (("1"
                 (name-replace "DRL2"
                  "x_sum(LAMBDA i:
                                     (TRUE, fm_contraction(nu!1, A_of(nu!1)(i))(Y!1)))")
                 (hide -4)
                 (expand "x_times")
                 (expand "x_eq")
                 (flatten)
                 (assert)
                 (case-replace "KX = 0")
                 (("1" (assert))
                  ("2"
                   (assert)
                   (case-replace "DRL2`1")
                   (("1" (assert)) ("2" (assert))))))
                ("2" (expand "measurable_set?") (propax))))
              ("2"
               (hide-all-but 1)
               (skosimp)
               (expand "x_times")
               (expand "x_eq")
               (propax))))
            ("2"
             (hide 2)
             (skolem + "j!1")
             (inst - "i!1" "j!1")
             (assert)
             (expand "x_eq")
             (flatten)
             (assert))))))
        ("2"
         (hide -1 2)
         (skosimp)
         (expand "FF")
         (expand "to_measure")
         (expand "x_eq")
         (lemma "rectangle_measure1"
          ("M"
           "cross_product(X!1, Y!1)"
           "X"
           "X!1"
           "Y"
           "Y!1"
           "mu"
           "fm_contraction[T1, S1](mu!1, A_of(mu!1)(i!1))"
           "nu"
           "fm_contraction[T2, S2](nu!1, A_of(nu!1)(j!1))"))
         (expand "fm_times")
         (assert))))
      ("3" (hide-all-but 1) (rewrite "rectangle_measure_TCC1"))))
    ("2"
     (hide 2)
     (skosimp)
     (expand "measurable_set?")
     (expand "A_of")
     (lemma "A_of_TCC1[T2,S2]" ("f" "nu!1"))
     (lemma "choose_member"
      ("a"
       "{X: disjoint_indexed_measurable[T2, S2] |
                            IUnion(X) = fullset[T2] AND (FORALL i: nu!1(X(i))`1)}"))
     (split)
     (("1" (expand "member") (flatten) (inst - "j!1"))
      ("2" (expand "nonempty?") (propax))))
    ("3"
     (hide 2)
     (skosimp)
     (expand "measurable_set?")
     (expand "A_of")
     (lemma "A_of_TCC1[T1,S1]" ("f" "mu!1"))
     (lemma "choose_member"
      ("a"
       "{X: disjoint_indexed_measurable[T1, S1] |
                            IUnion(X) = fullset[T1] AND (FORALL i: mu!1(X(i))`1)}"))
     (split)
     (("1" (expand "member") (flatten) (inst - "i!1"))
      ("2" (expand "nonempty?") (propax))))))


proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: product_measure
signature: nil
run_date: Unknown date
run_time: ----
status: proved-complete
description: nil
script:
  (""
   (skosimp)
   (typepred "A_of[T1, S1](mu!1)(i!1)")
   (expand "measurable_set?")
   (expand "A_of")
   (lemma "A_of_TCC1[T1,S1]" ("f" "mu!1"))
   (name-replace "XX"
    "{X: disjoint_indexed_measurable[T1, S1] |
                         IUnion(X) = fullset[T1] AND (FORALL i: mu!1(X(i))`1)}")
   (lemma "choose_member" ("a" "XX"))
   (expand "nonempty?")
   (name-replace "CC" "choose(XX)")
   (expand "XX")
   (assert)
   (flatten)
   (inst - "i!1"))


proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: product_measure
signature: nil
run_date: Unknown date
run_time: ----
status: proved-complete
description: nil
script:
  (""
   (skosimp)
   (typepred "A_of[T2, S2](nu!1)(j!1)")
   (expand "measurable_set?")
   (lemma "A_of_TCC1[T2, S2]" ("f" "nu!1"))
   (expand "A_of")
   (name "XX"
         "{X: disjoint_indexed_measurable[T2, S2] |
                              IUnion(X) = fullset[T2] AND (FORALL i: nu!1(X(i))`1)}")
   (replace -1)
   (lemma "choose_member" ("a" "XX"))
   (split)
   (("1"
     (name-replace "CC" "choose(XX)")
     (expand "XX")
     (expand "member")
     (flatten)
     (inst - "j!1"))
    ("2" (expand "nonempty?") (propax))))


proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: product_measure
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (lemma "x_sum_measure"
    ("F"
     "LAMBDA i: lambda M:
                          x_sum(LAMBDA j:
                                  to_measure[[T1, T2], sigma_times(S1, S2)]
                                      (product_measure_approx(mu!1, nu!1)(i, j))(M))
                                      "))
   (("1"
     (assert)
     (expand "sigma_finite_measure?")
     (hide -1)
     (expand "product_measure_approx")
     (typepred "A_of(nu!1)")
     (typepred "A_of(mu!1)")
     (name "X!1" "A_of(mu!1)")
     (name "Y!1" "A_of(nu!1)")
     (replace -1)
     (replace -2)
     (expand "disjoint_indexed_measurable?")
     (case "forall i,j: sigma_times(S1, S2)(cross_product(X!1(i),Y!1(j)))")
     (("1"
       (lemma "A_of_TCC1[T2,S2]" ("f" "nu!1"))
       (lemma "A_of_TCC1[T1,S1]" ("f" "mu!1"))
       (expand "nonempty?")
       (expand "A_of")
       (lemma "choose_member"
        ("a"
         "{X: disjoint_indexed_measurable[T1, S1] |
                         IUnion[nat, T1](X) = fullset[T1] AND
                          (FORALL i: mu!1(X(i))`1)}"))
       (replace -4)
       (replace 1)
       (lemma "choose_member"
        ("a"
         "{X: disjoint_indexed_measurable[T2, S2] |
                         IUnion[nat, T2](X) = fullset[T2] AND
                          (FORALL i: nu!1(X(i))`1)}"))
       (replace -4)
       (replace 2)
       (hide -4 -5 1 2)
       (expand "member")
       (flatten)
       (expand "measure_sigma_finite?")
       (name "UU" "lambda i,j: cross_product(X!1(i), Y!1(j))")
       (hide -1)
       (case "FORALL i, j: sigma_times(S1, S2)(UU(i,j))")
       (("1"
         (hide -6)
         (case "disjoint?(single_index(UU))")
         (("1"
           (inst + "single_index(UU)")
           (("1"
             (split)
             (("1"
               (apply-extensionality :hide? t)
               (lemma "extensionality_postulate"
                ("f" "IUnion[nat, T2](Y!1)" "g" "fullset[T2]"))
               (lemma "extensionality_postulate"
                ("f" "IUnion[nat, T1](X!1)" "g" "fullset[T1]"))
               (flatten)
               (split -2)
               (("1"
                 (split -4)
                 (("1"
                   (hide-all-but (-1 -2 1))
                   (expand "fullset")
                   (expand "single_index")
                   (expand "IUnion")
                   (inst - "x!2")
                   (skolem - "j!1")
                   (inst - "x!1")
                   (skolem - "i!1")
                   (inst + "double_index_n(i!1,j!1)")
                   (lemma "double_index_ij_n" ("i" "i!1" "j" "j!1"))
                   (flatten)
                   (assert)
                   (replace -1)
                   (replace -2)
                   (expand "UU")
                   (expand "cross_product")
                   (propax))
                  ("2" (propax))))
                ("2" (propax))))
              ("2"
               (skolem + "n!1")
               (expand "single_index")
               (case "forall i,j: to_measure[[T1, T2], sigma_times(S1, S2)]
                                               (fm_times(fm_contraction[T1, S1](mu!1, X!1(i)),
                                                         fm_contraction[T2, S2](nu!1, Y!1(j))))
                                               (UU(double_index_i(n!1), double_index_j(n!1))) = if i = double_index_i(n!1) & j = double_index_j(n!1) then (TRUE, mu!1(X!1(i))`2*nu!1(Y!1(j))`2) else (TRUE,0) endif")
               (("1"
                 (case "forall i:  x_sum(LAMBDA j:
                                             to_measure[[T1, T2], sigma_times(S1, S2)]
                                                 (fm_times(fm_contraction[T1, S1](mu!1, X!1(i)),
                                                           fm_contraction[T2, S2](nu!1, Y!1(j))))
                                                 (UU(double_index_i(n!1), double_index_j(n!1)))) = IF i = double_index_i(n!1)
                                  THEN (TRUE, mu!1(X!1(i))`2 * nu!1(Y!1(double_index_j(n!1)))`2)
                                ELSE (TRUE, 0)
                                ENDIF")
                 (("1"
                   (case-replace
                    "(LAMBDA i:
                                  x_sum(LAMBDA j:
                                          to_measure[[T1, T2], sigma_times(S1, S2)]
                                              (fm_times(fm_contraction[T1, S1](mu!1, X!1(i)),
                                                        fm_contraction[T2, S2](nu!1, Y!1(j))))
                                              (UU(double_index_i(n!1), double_index_j(n!1)))))=lambda i: IF i = double_index_i(n!1)
                               THEN (TRUE, mu!1(X!1(i))`2 * nu!1(Y!1(double_index_j(n!1)))`2)
                             ELSE (TRUE, 0)
                             ENDIF")
                   (("1"
                     (hide -1 -2)
                     (expand "x_sum")
                     (case-replace
                      "(FORALL (i_1: nat):
                                  IF i_1 = double_index_i(n!1) THEN TRUE ELSE TRUE ENDIF)")
                     (("1"
                       (prop)
                       (lemma "single_nz_series_conv"
                        ("a"
                         "(LAMBDA (i_1: nat):
                                                   IF i_1 = double_index_i(n!1)
                                                     THEN mu!1(X!1(i_1))`2 *
                                                           nu!1(Y!1(double_index_j(n!1)))`2
                                                   ELSE 0
                                                   ENDIF)"
                         "n"
                         "double_index_i(n!1)"))
                       (assert)
                       (hide 2)
                       (skosimp)
                       (assert))
                      ("2" (replace 1) (skosimp))))
                    ("2"
                     (apply-extensionality :hide? t)
                     (("1" (expand "measurable_set?") (propax))
                      ("2" (expand "measurable_set?") (propax))
                      ("3"
                       (inst -4 "double_index_i(n!1)"
                        "double_index_j(n!1)"))))))
                  ("2"
                   (hide 2)
                   (skosimp)
                   (inst - "i!1" "_")
                   (hide -4 -6 -8 -9)
                   (case-replace
                    "(LAMBDA j:
                                  to_measure[[T1, T2], sigma_times(S1, S2)]
                                      (fm_times(fm_contraction[T1, S1](mu!1, X!1(i!1)),
                                                fm_contraction[T2, S2](nu!1, Y!1(j))))
                                      (UU(double_index_i(n!1), double_index_j(n!1))))=lambda j: IF i!1 = double_index_i(n!1) & j = double_index_j(n!1)
                               THEN (TRUE, mu!1(X!1(i!1))`2 * nu!1(Y!1(j))`2)
                             ELSE (TRUE, 0)
                             ENDIF")
                   (("1"
                     (hide -1 -2)
                     (hide -1)
                     (case-replace "i!1 = double_index_i(n!1)")
                     (("1"
                       (replace -1 * rl)
                       (hide -1)
                       (expand "x_sum")
                       (lift-if)
                       (lift-if 1)
                       (assert)
                       (lemma "single_nz_series_conv"
                        ("a"
                         "LAMBDA i:
                                                      IF i = double_index_j(n!1)
                                                        THEN mu!1(X!1(i!1))`2 * nu!1(Y!1(i))`2
                                                      ELSE 0
                                                      ENDIF"
                         "n"
                         "double_index_j(n!1)"))
                       (lemma "single_nz_series_limit"
                        ("a"
                         "LAMBDA i:
                                                      IF i = double_index_j(n!1)
                                                        THEN mu!1(X!1(i!1))`2 * nu!1(Y!1(i))`2
                                                      ELSE 0
                                                      ENDIF"
                         "n"
                         "double_index_j(n!1)"))
                       (case-replace
                        "(FORALL (m:nat):
                                 double_index_j(n!1) /= m =>
                                  (LAMBDA i:
                                     IF i = double_index_j(n!1)
                                       THEN mu!1(X!1(i!1))`2 * nu!1(Y!1(i))`2
                                     ELSE 0
                                     ENDIF)
                                      (m)
                                   = 0)")
                       (("1" (assert))
                        ("2" (hide 2 -1 -2) (skosimp) (assert))))
                      ("2"
                       (assert)
                       (expand "x_sum")
                       (rewrite "zero_series_conv")
                       (rewrite "zero_series_limit"))))
                    ("2"
                     (apply-extensionality :hide? t)
                     (("1" (expand "measurable_set?") (propax))
                      ("2" (expand "measurable_set?") (inst -5 "i!1"))
                      ("3"
                       (inst -3 "double_index_i(n!1)"
                        "double_index_j(n!1)"))))
                    ("3" (expand "measurable_set?") (inst -5 "i!1"))))))
                ("2"
                 (hide 2)
                 (skosimp)
                 (expand "to_measure")
                 (expand "fm_times")
                 (lift-if)
                 (assert)
                 (expand "UU")
                 (lemma "rectangle_measure1"
                  ("M"
                   "cross_product(X!1(double_index_i(n!1)),
                                                              Y!1(double_index_j(n!1)))"
                   "X"
                   "X!1(double_index_i(n!1))"
                   "Y"
                   "Y!1(double_index_j(n!1))"
                   "mu"
                   "fm_contraction[T1, S1](mu!1, X!1(i!1))"
                   "nu"
                   "fm_contraction[T2, S2](nu!1, Y!1(j!1))"))
                 (("1"
                   (assert)
                   (replace -1)
                   (hide -1)
                   (expand "fm_contraction")
                   (case-replace "double_index_i(n!1)=i!1")
                   (("1"
                     (rewrite "intersection_idempotent")
                     (case-replace "double_index_j(n!1)=j!1")
                     (("1" (rewrite "intersection_idempotent"))
                      ("2"
                       (assert)
                       (expand "disjoint?" -9)
                       (inst -9 "j!1" "double_index_j(n!1)")
                       (assert)
                       (expand "disjoint?")
                       (rewrite "emptyset_is_empty?")
                       (replace -9)
                       (typepred "nu!1")
                       (expand "sigma_finite_measure?")
                       (expand "measure?")
                       (flatten)
                       (expand "measure_empty?")
                       (replace -1)
                       (assert))))
                    ("2"
                     (assert)
                     (expand "disjoint?" -7)
                     (inst -7 "i!1" "double_index_i(n!1)")
                     (assert)
                     (expand "disjoint?")
                     (rewrite "emptyset_is_empty?")
                     (replace -7)
                     (typepred "mu!1")
                     (expand "sigma_finite_measure?")
                     (expand "measure?")
                     (flatten)
                     (expand "measure_empty?")
                     (replace -1)
                     (assert))))
                  ("2" (expand "measurable_set?") (inst -4 "j!1"))
                  ("3" (expand "measurable_set?") (inst -6 "i!1"))
                  ("4"
                   (inst -2 "double_index_i(n!1)"
                    "double_index_j(n!1)"))))
                ("3"
                 (skosimp)
                 (expand "measurable_set?")
                 (inst -4 "j!1"))
                ("4" (expand "measurable_set?") (propax))
                ("5"
                 (inst - "double_index_i(n!1)"
                  "double_index_j(n!1)"))))))
            ("2"
             (assert)
             (split)
             (("1"
               (skolem + "n!1")
               (expand "single_index")
               (inst - "double_index_i(n!1)" "double_index_j(n!1)"))
              ("2" (expand "disjoint_indexed_measurable?") (propax))))))
          ("2"
           (hide-all-but (-6 -7 1))
           (expand "disjoint?")
           (skosimp)
           (expand "single_index")
           (expand "UU")
           (case-replace "double_index_i(j!1)=double_index_i(i!1)")
           (("1"
             (lemma "double_index_n_ij" ("n" "i!1"))
             (lemma "double_index_n_ij" ("n" "j!1"))
             (replace -3)
             (case-replace "double_index_j(j!1)=double_index_j(i!1)")
             (("1" (assert))
              ("2"
               (inst -5 "double_index_j(i!1)" "double_index_j(j!1)")
               (assert)
               (hide-all-but (-5 3))
               (expand "cross_product")
               (expand "disjoint?")
               (expand "intersection")
               (expand "empty?")
               (expand "member")
               (skosimp)
               (inst - "x!1`2")
               (assert))))
            ("2"
             (inst -1 "double_index_i(i!1)" "double_index_i(j!1)")
             (assert)
             (hide-all-but (-1 3))
             (expand "cross_product")
             (expand "disjoint?")
             (expand "intersection")
             (expand "empty?")
             (expand "member")
             (skosimp)
             (inst - "x!1`1")
             (assert))))))
        ("2" (skosimp) (inst - "i!1" "j!1") (expand "UU") (propax))))
      ("2"
       (hide 2)
       (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?")
       (inst - "cross_product(X!1(i!1), Y!1(j!1))")
       (assert)
       (hide 2)
       (expand "fullset")
       (expand "extend")
       (prop)
       (expand "measurable_rectangle?")
       (inst + "X!1(i!1)" "Y!1(j!1)")
       (assert)
       (expand "cross_product")
       (propax))))
    ("2"
     (hide 2)
     (skosimp)
     (lemma "x_sum_measure"
      ("F"
       "lambda j: to_measure[[T1, T2], sigma_times[T1, T2](S1, S2)]
                                (product_measure_approx(mu!1, nu!1)(i!1, j))"))
     (assert))))


proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: product_measure
signature: nil
run_date: Unknown date
run_time: ----
status: proved-complete
description: nil
script:
  (""
   (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[T1, T2](X!1, Y!1)")
   (assert)
   (hide 2)
   (expand "fullset")
   (expand "extend")
   (prop)
   (expand "measurable_rectangle?")
   (inst + "X!1" "Y!1")
   (assert)
   (expand "cross_product")
   (propax))


proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: product_measure
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (lemma "cross_product_is_sigma_times" ("X" "X!1" "Y" "fullset[T2]"))
   (rewrite "phi_is_simple"))


proof_type: t_proof
decl_type: tcc
library: measure_integration
theory: product_measure
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (lemma "cross_product_is_sigma_times" ("Y" "Y!1" "X" "fullset[T1]"))
   (rewrite "phi_is_simple"))


proof_type: f_proof
decl_type: formula
library: measure_integration
theory: fubini_tonelli_scaf
signature: nil
run_date: Unknown date
run_time: ----
status: proved-incomplete
description: nil
script:
  (""
   (skosimp)
   (lemma "cross_product_is_sigma_times" ("X" "X!1" "Y" "Y!1"))
   (lemma "measurable_intersection"
    ("a" "cross_product(X!1, Y!1)" "b" "E!1"))
   (("1"
     (expand "contraction" 1 1)
     (name "F"
           "lambda j: fm_contraction[T2, S2](nu, A_of(nu)(j)) o
                                                      x_section(intersection
                                                                (cross_product(X!1, Y!1),
                                                                 E!1))")
     (("1"
       (case "forall j,x: F(j)(x)>=0")
       (("1"
         (name "MU"
               "lambda i: fm_contraction[T1, S1]
                                                                        (mu, A_of(mu)(i))")
         (("1"
           (case "forall (E:(S1)): x_eq(mu(E),
                                             x_sum(LAMBDA i: to_measure(MU(i))(E)))")
           (("1"
             (case "forall i,j: integrable?[T1,S1,to_measure(MU(i))](F(j))")
             (("1"
               (case "forall x: measurable_set?(x_section(intersection(cross_product(X!1, Y!1), E!1),x))")
               (("1"
                 (name "EE"
                       "intersection(cross_product(X!1, Y!1),
                                                                                           E!1)")
                 (replace -1)
                 (case "forall x: x_eq(x_sum(lambda j: F(j)(x)),nu(x_section(EE,x)))")
                 (("1"
                   (hide -6 -8)
                   (case "forall x: measurable_set?(x_section(E!1,x))")
                   (("1"
                     (name "G"
                           "lambda j: (fm_contraction[T2, S2]
                                                                                         (contraction(nu, Y!1),
                                                                                          A_of(contraction(nu, Y!1))(j))
                                                                                      o x_section(E!1))")
                     (("1"
                       (case "forall j,x: G(j)(x)>=0")
                       (("1"
                         (name "NU"
                               "lambda i: fm_contraction[T1, S1]
                                                                                                        (contraction(mu, X!1),
                                                                                                         A_of
                                                                                                         (contraction(mu, X!1))(i))")
                         (("1"
                           (case "forall i,j: integrable?[T1,S1,to_measure(NU(i))](G(j))")
                           (("1"
                             (hide -2 -4)
                             (case "FORALL (E: (S1)): x_eq(contraction(mu, X!1)(E), x_sum(LAMBDA i: to_measure(NU(i))(E)))")
                             (("1"
                               (case "FORALL x: x_eq(x_sum(LAMBDA j: G(j)(x)), contraction(nu, Y!1)(x_section(E!1, x)))")
                               (("1"
                                 (case
                                  "forall x: X!1(x)=> x_eq(contraction(nu, Y!1)(x_section(E!1, x)), nu(x_section(EE, x)))")
                                 (("1"
                                   (case
                                    "x_eq(x_sum(LAMBDA i:
                                                                                         x_sum(LAMBDA j:
                                                                                                 (TRUE,
                                                                                                  integral
                                                                                                      [T1, S1,
                                                                                                       to_measure(MU(i))]
                                                                                                      (F(j))))),
                                                                                 x_sum(LAMBDA i:
                                                                                         x_sum(LAMBDA j:
                                                                                                 (TRUE,
                                                                                                  integral
                                                                                                      [T1, S1,
                                                                                                       to_measure(NU(i))]
                                                                                                      (G(j))))))")
                                   (("1"
                                     (expand "m_times")
                                     (expand "to_measure" 1)
                                     (expand "product_measure_approx")
                                     (expand "fm_times")
                                     (lemma
                                      "x_sum_eq"
                                      ("S"
                                       "LAMBDA i:
                                                                                               x_sum(LAMBDA j:
                                                                                                       (TRUE,
                                                                                                        integral[T1, S1, to_measure(MU(i))](F(j))))"
                                       "T"
                                       "LAMBDA i:
                                                                                               x_sum(LAMBDA j:
                                                                                                       (TRUE,
                                                                                                        integral
                                                                                                            [T1, S1,
                                                                                                             to_measure(fm_contraction[T1, S1]
                                                                                                                        (mu, A_of(mu)(i)))]
                                                                                                            (fm_contraction[T2, S2](nu, A_of(nu)(j)) o
                                                                                                              x_section(EE))))"))
                                     (("1"
                                       (split -1)
                                       (("1"
                                         (lemma
                                          "x_sum_eq"
                                          ("S"
                                           "LAMBDA i:
                                                                                                       x_sum(LAMBDA j:
                                                                                                               (TRUE,
                                                                                                                integral
                                                                                                                    [T1, S1,
                                                                                                                     to_measure(fm_contraction[T1, S1]
                                                                                                                                (contraction(mu, X!1),
                                                                                                                                 A_of
                                                                                                                                 (contraction(mu, X!1))(i)))]
                                                                                                                    (fm_contraction[T2, S2]
                                                                                                                         (contraction(nu, Y!1),
                                                                                                                          A_of(contraction(nu, Y!1))(j))
                                                                                                                      o x_section(E!1))))"
                                           "T"
                                           "LAMBDA i:
                                                                                                       x_sum(LAMBDA j:
                                                                                                               (TRUE,
                                                                                                                integral[T1, S1, to_measure(NU(i))](G(j))))"))
                                         (("1"
                                           (split -1)
                                           (("1"
                                             (hide-all-but (-1 -2 -3 1))
                                             (expand "x_eq")
                                             (flatten)
                                             (assert)
                                             (flatten)
                                             (assert))
                                            ("2"
                                             (hide 2 -1 -2)
                                             (assert)
                                             (skolem + "i!1")
                                             (lemma
                                              "x_sum_eq"
                                              ("S"
                                               "LAMBDA j:
                                                                                                               (TRUE,
                                                                                                                integral
                                                                                                                    [T1, S1,
                                                                                                                     to_measure(fm_contraction[T1, S1]
                                                                                                                                (contraction(mu, X!1),
                                                                                                                                 A_of(contraction(mu, X!1))(i!1)))]
                                                                                                                    (fm_contraction[T2, S2]
                                                                                                                         (contraction(nu, Y!1),
                                                                                                                          A_of(contraction(nu, Y!1))(j))
                                                                                                                      o x_section(E!1)))"
                                               "T"
                                               "LAMBDA j:
                                                                                                               (TRUE, integral[T1, S1, to_measure(NU(i!1))](G(j)))"))
                                             (("1"
                                               (split)
                                               (("1" (propax))
                                                ("2"
                                                 (hide 2)
                                                 (assert)
                                                 (skolem + "j!1")
                                                 (expand "x_eq" 1)
                                                 (inst -4 "i!1" "j!1")
                                                 (lemma
                                                  "measure_eq_integral[T1,S1]"
                                                  ("mu"
                                                   "to_measure(fm_contraction[T1, S1]
                                                                                                                              (contraction(mu, X!1),
                                                                                                                               A_of(contraction(mu, X!1))(i!1)))"
                                                   "nu"
                                                   "to_measure(NU(i!1))"
                                                   "f"
                                                   "G(j!1)"))
                                                 (assert)
                                                 (expand "G")
                                                 (assert)
                                                 (hide-all-but
                                                  (1 -6 -8 -9 -13))
                                                 (skosimp)
                                                 (expand "to_measure")
                                                 (expand "x_eq")
                                                 (expand "NU")
                                                 (propax))))
                                              ("2"
                                               (hide 2)
                                               (skosimp)
                                               (inst -4 "i!1" "j!1")
                                               (inst -5 "j!1" "_")
                                               (lemma
                                                "integral_nonneg[T1, S1, to_measure[T1, S1](NU(i!1))]"
                                                ("f" "G(j!1)"))
                                               (assert))
                                              ("3"
                                               (skosimp)
                                               (inst -4 "i!1" "j!1"))
                                              ("4"
                                               (hide 2)
                                               (skosimp)
                                               (inst -4 "i!1" "j!1")
                                               (inst -5 "j!1" "_")
                                               (lemma
                                                "integral_nonneg[T1, S1, to_measure(NU(i!1))]"
                                                ("f" "G(j!1)"))
                                               (("1"
                                                 (replace -6)
                                                 (lemma
                                                  "measure_eq_integral[T1,S1]"
                                                  ("mu"
                                                   "to_measure[T1, S1]
                                                                                                                   (fm_contraction[T1, S1]
                                                                                                                        (contraction[T1, S1](mu, X!1),
                                                                                                                         A_of[T1, S1](contraction[T1, S1](mu, X!1))(i!1)))"
                                                   "nu"
                                                   "to_measure(NU(i!1))"
                                                   "f"
                                                   "G(j!1)"))
                                                 (("1"
                                                   (assert)
                                                   (expand "G" -1 1)
                                                   (hide-all-but 1)
                                                   (skosimp)
                                                   (expand "to_measure")
                                                   (expand "NU")
                                                   (expand "x_eq")
                                                   (propax))
                                                  ("2"
                                                   (expand
                                                    "measurable_set?")
                                                   (rewrite
                                                    "A_of_def2"))))
                                                ("2" (propax))))
                                              ("5"
                                               (expand "measurable_set?")
                                               (rewrite "A_of_def2"))
                                              ("6"
                                               (skosimp)
                                               (inst -4 "i!1" "j!1")
                                               (hide 2)
                                               (lemma
                                                "measure_eq_integrable?[T1,S1]"
                                                ("mu"
                                                 "to_measure(NU(i!1))"
                                                 "nu"
                                                 "to_measure(fm_contraction[T1, S1]
                                                                                                                          (contraction(mu, X!1),
                                                                                                                           A_of(contraction(mu, X!1))(i!1)))"
                                                 "f"
                                                 "G(j!1)"))
                                               (("1"
                                                 (split -1)
                                                 (("1"
                                                   (assert)
                                                   (expand "G")
                                                   (propax))
                                                  ("2"
                                                   (hide-all-but 1)
                                                   (skosimp)
                                                   (expand "to_measure")
                                                   (expand "x_eq")
                                                   (expand "NU")
                                                   (propax))))
                                                ("2"
                                                 (expand
                                                  "measurable_set?")
                                                 (rewrite
                                                  "A_of_def2"))))))))
                                          ("2"
                                           (hide -1 -2 2)
                                           (skosimp)
                                           (inst -4 "i!1" "j!1")
                                           (inst -5 "j!1" "_")
                                           (lemma
                                            "integral_nonneg[T1, S1, to_measure(NU(i!1))]"
                                            ("f" "G(j!1)"))
                                           (("1"
                                             (replace -6)
                                             (lemma
                                              "measure_eq_integral[T1,S1]"
                                              ("mu"
                                               "to_measure[T1, S1]
                                                                                                           (fm_contraction[T1, S1]
                                                                                                                (contraction[T1, S1](mu, X!1),
                                                                                                                 A_of[T1, S1](contraction[T1, S1](mu, X!1))(i!1)))"
                                               "nu"
                                               "to_measure(NU(i!1))"
                                               "f"
                                               "G(j!1)"))
                                             (("1"
                                               (split -1)
                                               (("1"
                                                 (expand "G" -1 1)
                                                 (assert))
                                                ("2"
                                                 (hide-all-but 1)
                                                 (skosimp)
                                                 (expand "to_measure")
                                                 (expand "x_eq")
                                                 (expand "NU")
                                                 (propax))
                                                ("3" (flatten))))
                                              ("2"
                                               (expand "measurable_set?")
                                               (rewrite "A_of_def2"))
                                              ("3"
                                               (expand "measurable_set?")
                                               (propax))))
                                            ("2" (propax))))
                                          ("3"
                                           (expand "measurable_set?")
                                           (propax))
                                          ("4"
                                           (hide -1 -2 2)
                                           (skosimp)
                                           (inst -4 "i!1" "j!1")
                                           (lemma
                                            "measure_eq_integrable?[T1,S1]"
                                            ("mu"
                                             "to_measure(fm_contraction[T1, S1]
                                                                                                                  (contraction(mu, X!1),
                                                                                                                   A_of(contraction(mu, X!1))(i!1)))"
                                             "nu"
                                             "to_measure(NU(i!1))"
                                             "f"
                                             "G(j!1)"))
                                           (("1"
                                             (assert)
                                             (expand "G")
                                             (assert)
                                             (hide-all-but 1)
                                             (skosimp)
                                             (expand "to_measure")
                                             (expand "x_eq")
                                             (expand "NU")
                                             (propax))
                                            ("2"
                                             (expand "measurable_set?")
                                             (rewrite "A_of_def2"))
                                            ("3"
                                             (expand "measurable_set?")
                                             (propax))))
                                          ("5"
                                           (expand "measurable_set?")
                                           (propax))))
                                        ("2"
                                         (hide 2 -1)
                                         (assert)
                                         (skolem + "i!1")
                                         (lemma
                                          "x_sum_eq"
                                          ("S"
                                           "LAMBDA j:
                                                                                                       (TRUE, integral[T1, S1, to_measure(MU(i!1))](F(j)))"
                                           "T"
                                           "LAMBDA j:
                                                                                                       (TRUE,
                                                                                                        integral
                                                                                                            [T1, S1,
                                                                                                             to_measure(fm_contraction[T1, S1]
                                                                                                                        (mu, A_of(mu)(i!1)))]
                                                                                                            (fm_contraction[T2, S2](nu, A_of(nu)(j)) o
                                                                                                              x_section(EE)))"))
                                         (("1"
                                           (assert)
                                           (skolem + "j!1")
                                           (hide -1 2)
                                           (expand "x_eq" 1)
                                           (lemma
                                            "measure_eq_integral[T1,S1]"
                                            ("mu"
                                             "to_measure(fm_contraction[T1, S1](mu, A_of(mu)(i!1)))"
                                             "nu"
                                             "to_measure(MU(i!1))"
                                             "f"
                                             "F(j!1)"))
                                           (inst -10 "i!1" "j!1")
                                           (assert)
                                           (expand "F" -1 1)
                                           (hide-all-but 1)
                                           (skosimp)
                                           (expand "MU")
                                           (expand "to_measure")
                                           (expand "x_eq")
                                           (propax))
                                          ("2"
                                           (skosimp)
                                           (inst -10 "i!1" "j!1")
                                           (inst -12 "j!1" "_")
                                           (lemma
                                            "integral_nonneg[T1, S1, to_measure(MU(i!1))]"
                                            ("f" "F(j!1)"))
                                           (("1"
                                             (replace -13)
                                             (lemma
                                              "measure_eq_integral[T1,S1]"
                                              ("mu"
                                               "to_measure[T1, S1]
                                                                                                           (fm_contraction[T1, S1](mu, A_of[T1, S1](mu)(i!1)))"
                                               "nu"
                                               "to_measure(MU(i!1))"
                                               "f"
                                               "F(j!1)"))
                                             (("1"
                                               (replace -12)
                                               (expand "F" -1 1)
                                               (assert)
                                               (hide-all-but 1)
                                               (skosimp)
                                               (expand "MU")
                                               (expand "to_measure")
                                               (expand "x_eq")
                                               (propax))
                                              ("2"
                                               (expand "measurable_set?")
                                               (rewrite "A_of_def2"))))
                                            ("2" (propax))))
                                          ("3"
                                           (expand "measurable_set?")
                                           (rewrite "A_of_def2"))
                                          ("4"
                                           (skosimp)
                                           (inst -10 "i!1" "j!1")
                                           (lemma
                                            "measure_eq_integrable?[T1,S1]"
                                            ("mu"
                                             "to_measure(fm_contraction[T1, S1](mu, A_of(mu)(i!1)))"
                                             "nu"
                                             "to_measure(MU(i!1))"
                                             "f"
                                             "F(j!1)"))
                                           (("1"
                                             (expand "F" -1 1)
                                             (expand "EE")
                                             (assert)
                                             (hide-all-but 1)
                                             (skosimp)
                                             (expand "MU")
                                             (expand "to_measure")
                                             (expand "x_eq")
                                             (propax))
                                            ("2"
                                             (expand "measurable_set?")
                                             (rewrite "A_of_def2"))))
                                          ("5"
                                           (skosimp)
                                           (inst -10 "i!1" "j!1")
                                           (inst -12 "j!1" "_")
                                           (lemma
                                            "integral_nonneg[T1, S1, to_measure[T1, S1](MU(i!1))]"
                                            ("f" "F(j!1)"))
                                           (assert))
                                          ("6"
                                           (skosimp)
                                           (inst -10 "i!1" "j!1"))))))
                                      ("2"
                                       (skosimp)
                                       (hide -1 2)
                                       (inst -10 "i!1" "j!1")
                                       (inst -12 "j!1" "_")
                                       (lemma
                                        "measure_eq_integral[T1,S1]"
                                        ("mu"
                                         "to_measure[T1, S1]
                                                                                               (fm_contraction[T1, S1](mu, A_of[T1, S1](mu)(i!1)))"
                                         "nu"
                                         "to_measure(MU(i!1))"
                                         "f"
                                         "F(j!1)"))
                                       (("1"
                                         (lemma
                                          "integral_nonneg[T1,S1,to_measure(MU(i!1))]"
                                          ("f" "F(j!1)"))
                                         (("1"
                                           (assert)
                                           (replace -14)
                                           (split -2)
                                           (("1"
                                             (assert)
                                             (expand "F")
                                             (assert))
                                            ("2"
                                             (hide-all-but 1)
                                             (skosimp)
                                             (expand "to_measure")
                                             (expand "MU")
                                             (expand "x_eq")
                                             (propax))))
                                          ("2" (propax))))
                                        ("2"
                                         (expand "measurable_set?")
                                         (rewrite "A_of_def2"))))
                                      ("3"
                                       (skosimp)
                                       (hide -1 2)
                                       (inst -10 "i!1" "j!1")
                                       (lemma
                                        "measure_eq_integrable?[T1,S1]"
                                        ("mu"
                                         "to_measure(fm_contraction[T1, S1](mu, A_of(mu)(i!1)))"
                                         "nu"
                                         "to_measure(MU(i!1))"
                                         "f"
                                         "F(j!1)"))
                                       (("1"
                                         (expand "F")
                                         (assert)
                                         (hide-all-but 1)
                                         (skosimp)
                                         (expand "MU")
                                         (expand "to_measure")
                                         (expand "x_eq")
                                         (propax))
                                        ("2"
                                         (expand "measurable_set?")
                                         (rewrite "A_of_def2"))))
                                      ("4"
                                       (skosimp)
                                       (inst -10 "x1!1")
                                       (expand "measurable_set?")
                                       (assert)
                                       (expand "x_section" 1)
                                       (propax))))
                                    ("2"
                                     (hide 2)
                                     (case
                                      "x_eq(x_sum(LAMBDA j:
                                                                                             x_sum(LAMBDA i:
                                                                                                     (TRUE,
                                                                                                      integral[T1, S1, to_measure(MU(i))](F(j))))),
                                                                                     x_sum(LAMBDA j:
                                                                                             x_sum(LAMBDA i:
                                                                                                     (TRUE,
                                                                                                      integral[T1, S1, to_measure(NU(i))](G(j))))))")
                                     (("1"
                                       (lemma
                                        "double_x_sum_eq"
                                        ("U"
                                         "lambda i,j: (TRUE,
                                                                                                            integral[T1, S1, to_measure(MU(i))](F(j)))"))
                                       (lemma
                                        "double_x_sum_eq"
                                        ("U"
                                         "lambda i,j: (TRUE,
                                                                                                            integral[T1, S1, to_measure(NU(i))](G(j)))"))
                                       (assert)
                                       (hide-all-but (-1 -2 -3 1))
                                       (expand "x_eq")
                                       (flatten)
                                       (assert)
                                       (flatten)
                                       (assert))
                                      ("2"
                                       (hide 2)
                                       (case
                                        "forall (E:(S1),i): x_eq(contraction(mu,A_of(mu)(i))(E),to_measure(MU(i))(E))")
                                       (("1"
                                         (case
                                          "forall j: integrable?[T1,S1,mu](F(j)) <=> convergent?(series(lambda i: integral[T1, S1, to_measure(MU(i))](F(j))))")
                                         (("1"
                                           (lemma
                                            "x_sum_eq"
                                            ("S"
                                             "LAMBDA j:
                                                                                                           x_sum(LAMBDA i:
                                                                                                                   (TRUE,
                                                                                                                    integral[T1, S1, to_measure(MU(i))](F(j))))"
                                             "T"
                                             "lambda j: if integrable?[T1,S1,mu](F(j)) then (TRUE,integral[T1,S1,mu](F(j))) else (FALSE,0) endif"))
                                           (("1"
                                             (split -1)
                                             (("1"
                                               (case
                                                "x_eq(x_sum(LAMBDA j:
                                                                                                                 IF integrable?[T1, S1, mu](F(j))
                                                                                                                   THEN (TRUE, integral[T1, S1, mu](F(j)))
                                                                                                                 ELSE (FALSE, 0)
                                                                                                                 ENDIF), x_sum(LAMBDA j:
                                                                                                                 x_sum(LAMBDA i:
                                                                                                                         (TRUE,
                                                                                                                          integral[T1, S1, to_measure(NU(i))](G(j))))))")
                                               (("1"
                                                 (hide-all-but (-1 -2 1))
                                                 (expand "x_eq")
                                                 (flatten)
                                                 (assert)
                                                 (flatten)
                                                 (assert))
                                                ("2"
                                                 (hide -1 2)
                                                 (hide -1 -2 -12 -13)
                                                 (case
                                                  "measurable_set?[T1, S1](X!1)")
                                                 (("1"
                                                   (case
                                                    "FORALL j:
                                                                                                              integrable?[T1, S1, contraction(mu, X!1)](G(j))=>integral[T1, S1, contraction[T1, S1](mu, X!1)](G(j)) >= 0")
                                                   (("1"
                                                     (case
                                                      "x_eq(x_sum(LAMBDA j:
                                                                                                                             IF integrable?[T1, S1, mu](F(j))
                                                                                                                               THEN (TRUE, integral[T1, S1, mu](F(j)))
                                                                                                                             ELSE (FALSE, 0)
                                                                                                                             ENDIF),
                                                                                                                     x_sum(LAMBDA j:IF integrable?[T1, S1, contraction(mu,X!1)](G(j))
                                                                                                                               THEN (TRUE, integral[T1, S1, contraction(mu,X!1)](G(j)))
                                                                                                                             ELSE (FALSE, 0)
                                                                                                                             ENDIF))")
                                                     (("1"
                                                       (lemma
                                                        "x_sum_eq"
                                                        ("S"
                                                         "LAMBDA j:
                                                                                                                                   IF integrable?[T1, S1, contraction(mu, X!1)](G(j))
                                                                                                                                     THEN (TRUE,
                                                                                                                                           integral[T1, S1, contraction(mu, X!1)](G(j)))
                                                                                                                                   ELSE (FALSE, 0)
                                                                                                                                   ENDIF"
                                                         "T"
                                                         "LAMBDA j:
                                                                                                                                   x_sum(LAMBDA i:
                                                                                                                                           (TRUE,
                                                                                                                                            integral[T1, S1, to_measure(NU(i))](G(j))))"))
                                                       (split -1)
                                                       (("1"
                                                         (hide-all-but
                                                          (-1 -2 1))
                                                         (expand "x_eq")
                                                         (flatten)
                                                         (assert)
                                                         (flatten)
                                                         (assert))
                                                        ("2"
                                                         (hide -1 2)
                                                         (assert)
                                                         (skolem + "j!1")
                                                         (case
                                                          "forall (E:(S1),i): x_eq(contraction(contraction(mu, X!1),A_of(contraction(mu,X!1))(i))(E),to_measure(NU(i))(E))")
                                                         (("1"
                                                           (case
                                                            "forall j: integrable?[T1,S1,contraction(mu, X!1)](G(j)) <=> convergent?(series(lambda i: integral[T1, S1, to_measure(NU(i))](G(j))))")
                                                           (("1"
                                                             (expand
                                                              "x_eq"
                                                              1)
                                                             (case-replace
                                                              "integrable?[T1, S1, contraction(mu, X!1)](G(j!1))")
                                                             (("1"
                                                               (inst
                                                                -
                                                                "j!1")
                                                               (assert)
                                                               (expand
                                                                "x_sum"
                                                                1)
                                                               (lemma
                                                                "sfm_integral[T1,S1,contraction(mu, X!1)]"
                                                                ("f"
                                                                 "G(j!1)"))
                                                               (("1"
                                                                 (case-replace
                                                                  "(LAMBDA i:
                                                                                                                                                              integral
                                                                                                                                                                  [T1, S1,
                                                                                                                                                                   contraction(contraction(mu, X!1),
                                                                                                                                                                               A_of(contraction(mu, X!1))(i))]
                                                                                                                                                                  (G(j!1)))=(LAMBDA i:
                                                                                                                                                             integral[T1, S1, to_measure(NU(i))](G(j!1)))")
                                                                 (("1"
                                                                   (hide
                                                                    -1)
                                                                   (name-replace
                                                                    "DRL1"
                                                                    "(series(LAMBDA (i_1: nat):
                                                                                                                                                                   integral[T1, S1, to_measure(NU(i_1))]
                                                                                                                                                                       (G(j!1))))")
                                                                   (("1"
                                                                     (name-replace
                                                                      "LHS"
                                                                      "integral[T1, S1, contraction(mu, X!1)](G(j!1))")
                                                                     (hide-all-but
                                                                      (-1
                                                                       1))
                                                                     (assert)
                                                                     (rewrite
                                                                      "metric_convergence_def")
                                                                     (lemma
                                                                      "convergence_sequences.limit_def"
                                                                      ("l"
                                                                       "LHS"
                                                                       "v"
                                                                       "DRL1"))
                                                                     (("1"
                                                                       (assert)
                                                                       (expand
                                                                        "metric_converges_to")
                                                                       (expand
                                                                        "convergence")
                                                                       (skosimp)
                                                                       (lift-if
                                                                        1)
                                                                       (case-replace
                                                                        "convergence_sequences.convergent?(DRL1)")
                                                                       (("1"
                                                                         (hide
                                                                          -2)
                                                                         (assert)
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "epsilon!1")
                                                                         (skosimp)
                                                                         (inst
                                                                          +
                                                                          "n!1")
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "i!1")
                                                                         (assert)
                                                                         (hide-all-but
                                                                          (-3
                                                                           1))
                                                                         (grind))
                                                                        ("2"
                                                                         (replace
                                                                          1
                                                                          2)
                                                                         (expand
                                                                          "convergent?")
                                                                         (inst
                                                                          +
                                                                          "LHS")
                                                                         (expand
                                                                          "convergence")
                                                                         (hide
                                                                          -1
                                                                          -2)
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "epsilon!1")
                                                                         (skosimp)
                                                                         (inst
                                                                          +
                                                                          "n!1")
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "i!1")
                                                                         (grind))))
                                                                      ("2"
                                                                       (replace
                                                                        1)
                                                                       (expand
                                                                        "convergent?")
                                                                       (inst
                                                                        +
                                                                        "LHS")
                                                                       (expand
                                                                        "metric_converges_to")
                                                                       (expand
                                                                        "convergence")
                                                                       (skosimp)
                                                                       (inst
                                                                        -
                                                                        "epsilon!1")
                                                                       (skosimp)
                                                                       (inst
                                                                        +
                                                                        "n!1")
                                                                       (skosimp)
                                                                       (inst
                                                                        -
                                                                        "i!1")
                                                                       (grind))))
                                                                    ("2"
                                                                     (skosimp)
                                                                     (inst
                                                                      -10
                                                                      "i!1"
                                                                      "j!1"))))
                                                                  ("2"
                                                                   (apply-extensionality
                                                                    :hide?
                                                                    t)
                                                                   (("1"
                                                                     (hide
                                                                      -1
                                                                      2)
                                                                     (lemma
                                                                      "measure_eq_integral[T1,S1]"
                                                                      ("mu"
                                                                       "contraction(contraction(mu, X!1),
                                                                                                                                                                     A_of(contraction(mu, X!1))(x!1))"
                                                                       "nu"
                                                                       "to_measure(NU(x!1))"
                                                                       "f"
                                                                       "G(j!1)"))
                                                                     (("1"
                                                                       (assert)
                                                                       (inst
                                                                        -9
                                                                        "x!1"
                                                                        "j!1")
                                                                       (replace
                                                                        -9)
                                                                       (inst
                                                                        -3
                                                                        "_"
                                                                        "x!1"))
                                                                      ("2"
                                                                       (expand
                                                                        "measurable_set?")
                                                                       (propax))))
                                                                    ("2"
                                                                     (skosimp)
                                                                     (inst
                                                                      -10
                                                                      "i!1"
                                                                      "j!1"))
                                                                    ("3"
                                                                     (expand
                                                                      "measurable_set?")
                                                                     (propax))
                                                                    ("4"
                                                                     (hide
                                                                      -1
                                                                      2)
                                                                     (skosimp)
                                                                     (inst
                                                                      -3
                                                                      "_"
                                                                      "i!1")
                                                                     (inst
                                                                      -9
                                                                      "i!1"
                                                                      "j!1")
                                                                     (lemma
                                                                      "measure_eq_integrable?[T1,S1]"
                                                                      ("mu"
                                                                       "contraction(contraction(mu, X!1),
                                                                                                                                                                     A_of(contraction(mu, X!1))(i!1))"
                                                                       "nu"
                                                                       "to_measure(NU(i!1))"
                                                                       "f"
                                                                       "G(j!1)"))
                                                                     (("1"
                                                                       (replace
                                                                        -4)
                                                                       (replace
                                                                        -1)
                                                                       (propax))
                                                                      ("2"
                                                                       (hide-all-but
                                                                        1)
                                                                       (typepred
                                                                        "A_of[T1, S1](contraction[T1, S1](mu, X!1))(i!1)")
                                                                       (expand
                                                                        "measurable_set?")
                                                                       (propax))))))
                                                                  ("3"
                                                                   (skosimp)
                                                                   (inst
                                                                    -10
                                                                    "i!1"
                                                                    "j!1"))
                                                                  ("4"
                                                                   (expand
                                                                    "measurable_set?")
                                                                   (propax))
                                                                  ("5"
                                                                   (skosimp)
                                                                   (hide
                                                                    2
                                                                    -1
                                                                    -3)
                                                                   (inst
                                                                    -2
                                                                    "_"
                                                                    "i!1")
                                                                   (inst
                                                                    -8
                                                                    "i!1"
                                                                    "j!1")
                                                                   (lemma
                                                                    "measure_eq_integrable?[T1,S1]"
                                                                    ("mu"
                                                                     "contraction(contraction(mu, X!1),
                                                                                                                                                               A_of(contraction(mu, X!1))(i!1))"
                                                                     "nu"
                                                                     "to_measure(NU(i!1))"
                                                                     "f"
                                                                     "G(j!1)"))
                                                                   (("1"
                                                                     (assert))
                                                                    ("2"
                                                                     (expand
                                                                      "measurable_set?")
                                                                     (propax))))))
                                                                ("2"
                                                                 (hide-all-but
                                                                  (-1
                                                                   1
                                                                   -10))
                                                                 (lemma
                                                                  "nn_integrable_is_nn_integrable[T1, S1, contraction[T1, S1](mu, X!1)]"
                                                                  ("f"
                                                                   "G(j!1)"))
                                                                 (assert)
                                                                 (skosimp)
                                                                 (inst
                                                                  -
                                                                  "j!1"
                                                                  "x!1"))))
                                                              ("2"
                                                               (replace
                                                                1)
                                                               (assert)
                                                               (expand
                                                                "x_sum"
                                                                -3)
                                                               (prop)
                                                               (inst
                                                                -
                                                                "j!1")
                                                               (name-replace
                                                                "DRL1"
                                                                "series(LAMBDA (i_1: nat):
                                                                                                                                                        integral[T1, S1, to_measure(NU(i_1))](G(j!1)))")
                                                               (("1"
                                                                 (replace
                                                                  -2)
                                                                 (hide-all-but
                                                                  (-1 1))
                                                                 (expand
                                                                  "convergent?")
                                                                 (skosimp)
                                                                 (inst
                                                                  +
                                                                  "l!1")
                                                                 (expand
                                                                  "convergence")
                                                                 (rewrite
                                                                  "metric_convergence_def")
                                                                 (expand
                                                                  "metric_converges_to")
                                                                 (skosimp)
                                                                 (inst
                                                                  -
                                                                  "r!1")
                                                                 (skosimp)
                                                                 (inst
                                                                  +
                                                                  "n!1")
                                                                 (skosimp)
                                                                 (inst
                                                                  -
                                                                  "i!1")
                                                                 (grind))
                                                                ("2"
                                                                 (skosimp)
                                                                 (inst
                                                                  -10
                                                                  "i!1"
                                                                  "j!1"))))))
                                                            ("2"
                                                             (hide 2)
                                                             (skosimp)
                                                             (case
                                                              "nn_measurable?[T1,S1](G(j!2))")
                                                             (("1"
                                                               (lemma
                                                                "sfm_integrable[T1, S1, contraction(mu, X!1)]"
                                                                ("h"
                                                                 "G(j!2)"))
                                                               (("1"
                                                                 (case-replace
                                                                  "(LAMBDA i:
                                                                                                                                                               integral
                                                                                                                                                                   [T1, S1,
                                                                                                                                                                    contraction(contraction(mu, X!1),
                                                                                                                                                                                A_of
                                                                                                                                                                                (contraction(mu, X!1))(i))]
                                                                                                                                                                   (G(j!2)))=(LAMBDA i:
                                                                                                                                                              integral[T1, S1, to_measure(NU(i))](G(j!2)))")
                                                                 (("1"
                                                                   (hide
                                                                    -1)
                                                                   (case-replace
                                                                    "(FORALL i:
                                                                                                                                                integrable?
                                                                                                                                                    [T1, S1,
                                                                                                                                                     contraction(contraction(mu, X!1),
                                                                                                                                                                 A_of(contraction(mu, X!1))(i))]
                                                                                                                                                    (G(j!2)))")
                                                                   (("1"
                                                                     (assert)
                                                                     (replace
                                                                      -2
                                                                      1
                                                                      rl)
                                                                     (name-replace
                                                                      "UU"
                                                                      "(series((LAMBDA i: integral[T1, S1, to_measure(NU(i))](G(j!2)))))")
                                                                     (("1"
                                                                       (hide-all-but
                                                                        1)
                                                                       (split)
                                                                       (("1"
                                                                         (flatten))
                                                                        ("2"
                                                                         (flatten))))
                                                                      ("2"
                                                                       (inst
                                                                        -10
                                                                        "_"
                                                                        "j!2"))))
                                                                    ("2"
                                                                     (skosimp)
                                                                     (inst
                                                                      -4
                                                                      "_"
                                                                      "i!1")
                                                                     (inst
                                                                      -10
                                                                      "i!1"
                                                                      "j!2")
                                                                     (lemma
                                                                      "measure_eq_integrable?[T1,S1]"
                                                                      ("mu"
                                                                       "contraction(contraction(mu, X!1),
                                                                                                                                                                   A_of(contraction(mu, X!1))(i!1))"
                                                                       "nu"
                                                                       "to_measure(NU(i!1))"
                                                                       "f"
                                                                       "G(j!2)"))
                                                                     (("1"
                                                                       (assert))
                                                                      ("2"
                                                                       (expand
                                                                        "measurable_set?")
                                                                       (propax))))
                                                                    ("3"
                                                                     (expand
                                                                      "measurable_set?")
                                                                     (propax))))
                                                                  ("2"
                                                                   (hide
                                                                    -1
                                                                    2)
                                                                   (apply-extensionality
                                                                    :hide?
                                                                    t)
                                                                   (("1"
                                                                     (lemma
                                                                      "measure_eq_integral[T1,S1]"
                                                                      ("mu"
                                                                       "contraction(contraction(mu, X!1),
                                                                                                                                                                   A_of(contraction(mu, X!1))(x!1))"
                                                                       "nu"
                                                                       "to_measure(NU(x!1))"
                                                                       "f"
                                                                       "G(j!2)"))
                                                                     (("1"
                                                                       (inst
                                                                        -9
                                                                        "x!1"
                                                                        "j!2")
                                                                       (inst
                                                                        -3
                                                                        "_"
                                                                        "x!1")
                                                                       (assert))
                                                                      ("2"
                                                                       (expand
                                                                        "measurable_set?")
                                                                       (propax))))
                                                                    ("2"
                                                                     (skosimp)
                                                                     (inst
                                                                      -8
                                                                      "i!1"
                                                                      "j!2"))
                                                                    ("3"
                                                                     (expand
                                                                      "measurable_set?")
                                                                     (propax))
                                                                    ("4"
                                                                     (skosimp)
                                                                     (inst
                                                                      -8
                                                                      "i!1"
                                                                      "j!2")
                                                                     (inst
                                                                      -2
                                                                      "_"
                                                                      "i!1")
                                                                     (lemma
                                                                      "measure_eq_integrable?[T1,S1]"
                                                                      ("mu"
                                                                       "contraction(contraction(mu, X!1),
                                                                                                                                                                     A_of(contraction(mu, X!1))(i!1))
                                                                                                                                                                    "
                                                                       "nu"
                                                                       "to_measure(NU(i!1))"
                                                                       "f"
                                                                       "G(j!2)"))
                                                                     (("1"
                                                                       (replace
                                                                        -3)
                                                                       (replace
                                                                        -1)
                                                                       (propax))
                                                                      ("2"
                                                                       (expand
                                                                        "measurable_set?")
                                                                       (propax))))))
                                                                  ("3"
                                                                   (skosimp)
                                                                   (inst
                                                                    -10
                                                                    "i!1"
                                                                    "j!2"))
                                                                  ("4"
                                                                   (expand
                                                                    "measurable_set?")
                                                                   (propax))
                                                                  ("5"
                                                                   (skosimp)
                                                                   (inst
                                                                    -
                                                                    "_"
                                                                    "i!1")
                                                                   (inst
                                                                    -10
                                                                    "i!1"
                                                                    "j!2")
                                                                   (lemma
                                                                    "measure_eq_integrable?[T1,S1]"
                                                                    ("mu"
                                                                     "contraction(contraction(mu, X!1),
                                                                                                                                                               A_of(contraction(mu, X!1))(i!1))"
                                                                     "nu"
                                                                     "to_measure(NU(i!1))"
                                                                     "f"
                                                                     "G(j!2)"))
                                                                   (("1"
                                                                     (assert))
                                                                    ("2"
                                                                     (expand
                                                                      "measurable_set?")
                                                                     (propax))))))
                                                                ("2"
                                                                 (propax))))
                                                              ("2"
                                                               (expand
                                                                "nn_measurable?")
                                                               (split)
                                                               (("1"
                                                                 (expand
                                                                  "G")
                                                                 (hide-all-but
                                                                  (1 -9))
                                                                 (lemma
                                                                  "x_section_measurable"
                                                                  ("nu"
                                                                   "fm_contraction[T2, S2]
                                                                                                                                                                    (contraction(nu, Y!1),
                                                                                                                                                                     A_of(contraction(nu, Y!1))(j!2))"
                                                                   "M"
                                                                   "E!1"))
                                                                 (propax))
                                                                ("2"
                                                                 (skosimp)
                                                                 (inst
                                                                  -8
                                                                  "j!2"
                                                                  "x!1")
                                                                 (assert))))))))
                                                          ("2"
                                                           (hide-all-but
                                                            1)
                                                           (skosimp)
                                                           (expand "NU")
                                                           (typepred
                                                            "contraction(mu, X!1)")
                                                           (name-replace
                                                            "MU1"
                                                            "contraction(mu, X!1)")
                                                           (expand
                                                            "to_measure")
                                                           (expand
                                                            "fm_contraction")
                                                           (expand
                                                            "contraction")
                                                           (expand
                                                            "x_eq")
                                                           (lemma
                                                            "A_of_def2"
                                                            ("mu"
                                                             "MU1"
                                                             "n"
                                                             "i!1"))
                                                           (lemma
                                                            "m_monotone[T1,S1,MU1]"
                                                            ("a"
                                                             "intersection(A_of(MU1)(i!1), E!2)"
                                                             "b"
                                                             "A_of(MU1)(i!1)"))
                                                           (("1"
                                                             (expand
                                                              "x_le")
                                                             (assert)
                                                             (expand
                                                              "intersection")
                                                             (expand
                                                              "subset?")
                                                             (expand
                                                              "member")
                                                             (skosimp))
                                                            ("2"
                                                             (expand
                                                              "measurable_set?")
                                                             (propax))
                                                            ("3"
                                                             (expand
                                                              "measurable_set?")
                                                             (propax))))
                                                          ("3"
                                                           (expand
                                                            "measurable_set?")
                                                           (propax))))))
                                                      ("2"
                                                       (hide 2)
                                                       (case
                                                        "forall (l:real): ((forall j: integrable?[T1, S1, mu](F(j)))&convergence(series(LAMBDA j:integral[T1, S1, mu](F(j))),l)) <=> ((forall j: integrable?[T1, S1, contraction(mu, X!1)](G(j)))&convergence(series(LAMBDA j:integral[T1, S1, contraction(mu, X!1)](G(j))),l))")
                                                       (("1"
                                                         (expand
                                                          "x_sum"
                                                          1)
                                                         (case-replace
                                                          "(FORALL i:
                                                                                                                                   IF integrable?[T1, S1, mu](F(i)) THEN TRUE
                                                                                                                                   ELSE FALSE
                                                                                                                                   ENDIF)
                                                                                                                                 AND
                                                                                                                                 convergence_sequences.convergent?(series(LAMBDA i:
                                                                                                                                                     IF integrable?[T1, S1, mu](F(i))
                                                                                                                                                       THEN integral[T1, S1, mu](F(i))
                                                                                                                                                     ELSE 0
                                                                                                                                                     ENDIF))")
                                                         (("1"
                                                           (flatten -1)
                                                           (case-replace
                                                            "FORALL j: integrable?[T1, S1, mu](F(j))")
                                                           (("1"
                                                             (case-replace
                                                              "(LAMBDA i:
                                                                                                                                                    IF integrable?[T1, S1, mu](F(i))
                                                                                                                                                      THEN integral[T1, S1, mu](F(i))
                                                                                                                                                    ELSE 0
                                                                                                                                                    ENDIF)=(LAMBDA j: integral[T1, S1, mu](F(j)))")
                                                             (("1"
                                                               (hide -1)
                                                               (lemma
                                                                "convergence_sequences.limit_lemma"
                                                                ("v"
                                                                 "series(LAMBDA j: integral[T1, S1, mu](F(j)))"))
                                                               (("1"
                                                                 (inst
                                                                  -5
                                                                  "convergence_sequences.limit
                                                                                                                                                  (series(LAMBDA j: integral[T1, S1, mu](F(j))))")
                                                                 (replace
                                                                  -1)
                                                                 (case-replace
                                                                  "(FORALL i:
                                                                                                                                                   IF integrable?[T1, S1, contraction(mu, X!1)](G(i))
                                                                                                                                                     THEN TRUE
                                                                                                                                                   ELSE FALSE
                                                                                                                                                   ENDIF)
                                                                                                                                                 AND
                                                                                                                                                 convergence_sequences.convergent?(series(LAMBDA i:
                                                                                                                                                                     IF integrable?
                                                                                                                                                                        [T1, S1, contraction(mu, X!1)]
                                                                                                                                                                        (G(i))
                                                                                                                                                                       THEN integral
                                                                                                                                                                            [T1, S1, contraction(mu, X!1)]
                                                                                                                                                                            (G(i))
                                                                                                                                                                     ELSE 0
                                                                                                                                                                     ENDIF))")
                                                                 (("1"
                                                                   (expand
                                                                    "x_eq"
                                                                    1)
                                                                   (case-replace
                                                                    "(LAMBDA i:
                                                                                                                                                           IF integrable?[T1, S1, contraction(mu, X!1)](G(i))
                                                                                                                                                             THEN integral[T1, S1, contraction(mu, X!1)](G(i))
                                                                                                                                                           ELSE 0
                                                                                                                                                           ENDIF)=(LAMBDA j:
                                                                                                                                                                    integral[T1, S1, contraction(mu, X!1)]
                                                                                                                                                                        (G(j)))")
                                                                   (("1"
                                                                     (flatten)
                                                                     (rewrite
                                                                      "convergence_sequences.limit_def"
                                                                      -9
                                                                      :dir
                                                                      rl)
                                                                     (assert))
                                                                    ("2"
                                                                     (hide
                                                                      2)
                                                                     (apply-extensionality
                                                                      :hide?
                                                                      t)
                                                                     (("1"
                                                                       (flatten)
                                                                       (inst
                                                                        -
                                                                        "x!1")
                                                                       (prop)
                                                                       (assert))
                                                                      ("2"
                                                                       (skosimp)
                                                                       (inst
                                                                        -
                                                                        "j!1")
                                                                       (assert))))
                                                                    ("3"
                                                                     (skosimp)
                                                                     (inst
                                                                      -
                                                                      "j!1")
                                                                     (assert))))
                                                                  ("2"
                                                                   (hide
                                                                    2)
                                                                   (flatten)
                                                                   (split)
                                                                   (("1"
                                                                     (skosimp)
                                                                     (inst
                                                                      -5
                                                                      "i!1")
                                                                     (assert))
                                                                    ("2"
                                                                     (case-replace
                                                                      "(LAMBDA i:
                                                                                                                                                                    IF integrable?[T1, S1, contraction(mu, X!1)]
                                                                                                                                                                           (G(i))
                                                                                                                                                                      THEN integral[T1, S1, contraction(mu, X!1)]
                                                                                                                                                                               (G(i))
                                                                                                                                                                    ELSE 0
                                                                                                                                                                    ENDIF)=(LAMBDA j:
                                                                                                                                                                     integral[T1, S1, contraction(mu, X!1)](G(j)))")
                                                                     (("1"
                                                                       (expand
                                                                        "convergence_sequences.convergent?")
                                                                       (inst
                                                                        +
                                                                        "convergence_sequences.limit
                                                                                                                                                                    (series(LAMBDA j: integral[T1, S1, mu](F(j))))"))
                                                                      ("2"
                                                                       (apply-extensionality
                                                                        :hide?
                                                                        t)
                                                                       (inst
                                                                        -5
                                                                        "x!1")
                                                                       (assert))))))
                                                                  ("3"
                                                                   (expand
                                                                    "measurable_set?")
                                                                   (propax))
                                                                  ("4"
                                                                   (expand
                                                                    "measurable_set?")
                                                                   (propax))))
                                                                ("2"
                                                                 (propax))))
                                                              ("2"
                                                               (hide 2)
                                                               (apply-extensionality
                                                                :hide?
                                                                t)
                                                               (inst
                                                                -
                                                                "x!1")
                                                               (assert))))
                                                            ("2"
                                                             (hide 2)
                                                             (skosimp)
                                                             (inst
                                                              -
                                                              "j!1")
                                                             (assert))))
                                                          ("2"
                                                           (replace 1 2)
                                                           (expand
                                                            "x_eq"
                                                            2)
                                                           (case-replace
                                                            "FORALL j: integrable?[T1, S1, contraction(mu, X!1)](G(j))")
                                                           (("1"
                                                             (case-replace
                                                              "(LAMBDA i:
                                                                                                                                                        IF integrable?[T1, S1, contraction(mu, X!1)]
                                                                                                                                                               (G(i))
                                                                                                                                                          THEN integral[T1, S1, contraction(mu, X!1)]
                                                                                                                                                               (G(i))
                                                                                                                                                        ELSE 0
                                                                                                                                                        ENDIF)=(LAMBDA j:
                                                                                                                                                        integral[T1, S1, contraction(mu, X!1)]
                                                                                                                                                            (G(j)))")
                                                             (("1"
                                                               (case-replace
                                                                "convergence_sequences.convergent?(series(LAMBDA j:
                                                                                                                                                             integral[T1, S1, contraction(mu, X!1)]
                                                                                                                                                                 (G(j))))")
                                                               (("1"
                                                                 (hide
                                                                  -5)
                                                                 (lemma
                                                                  "convergence_sequences.limit_lemma"
                                                                  ("v"
                                                                   "series(LAMBDA j: integral[T1, S1, contraction(mu, X!1)](G(j)))"))
                                                                 (("1"
                                                                   (inst
                                                                    -5
                                                                    "convergence_sequences.limit(series(LAMBDA j:
                                                                                                                                                                       integral[T1, S1, contraction(mu, X!1)]
                                                                                                                                                                           (G(j))))")
                                                                   (replace
                                                                    -1)
                                                                   (hide-all-but
                                                                    (-4
                                                                     -5
                                                                     1))
                                                                   (flatten)
                                                                   (split)
                                                                   (("1"
                                                                     (skosimp)
                                                                     (inst
                                                                      -2
                                                                      "i!1")
                                                                     (assert))
                                                                    ("2"
                                                                     (case-replace
                                                                      "(LAMBDA i:
                                                                                                                                                                    IF integrable?[T1, S1, mu](F(i))
                                                                                                                                                                      THEN integral[T1, S1, mu](F(i))
                                                                                                                                                                    ELSE 0
                                                                                                                                                                    ENDIF)=(LAMBDA j: integral[T1, S1, mu](F(j)))")
                                                                     (("1"
                                                                       (hide
                                                                        -1)
                                                                       (expand
                                                                        "convergence_sequences.convergent?")
                                                                       (inst
                                                                        +
                                                                        "convergence_sequences.limit
                                                                                                                                                                    (series(LAMBDA j:
                                                                                                                                                                              integral[T1, S1, contraction(mu, X!1)]
                                                                                                                                                                                  (G(j))))")
                                                                       (expand
                                                                        "measurable_set?")
                                                                       (propax))
                                                                      ("2"
                                                                       (apply-extensionality
                                                                        :hide?
                                                                        t)
                                                                       (inst
                                                                        -2
                                                                        "x!1")
                                                                       (assert))))))
                                                                  ("2"
                                                                   (propax))
                                                                  ("3"
                                                                   (propax))))
                                                                ("2"
                                                                 (replace
                                                                  1
                                                                  -4)
                                                                 (propax))))
                                                              ("2"
                                                               (apply-extensionality
                                                                1
                                                                :hide?
                                                                t)
                                                               (inst
                                                                -1
                                                                "x!1")
                                                               (assert))))
                                                            ("2"
                                                             (hide-all-but
                                                              (-2 1))
                                                             (prop)
                                                             (skosimp)
                                                             (inst
                                                              -
                                                              "j!1")
                                                             (assert))))))
                                                        ("2"
                                                         (hide 2)
                                                         (skosimp)
                                                         (split 1)
                                                         (("1"
                                                           (flatten)
                                                           (name
                                                            "FF"
                                                            "lambda j: lambda x: series(lambda i: F(i)(x))(j)")
                                                           (case
                                                            "forall j: integrable?[T1, S1, mu](FF(j))")
                                                           (("1"
                                                             (case
                                                              "forall (n:nat): series(LAMBDA j: integral[T1, S1, mu](F(j)))(n) = (integral[T1, S1, mu] o FF)(n)")
                                                             (("1"
                                                               (lemma
                                                                "extensionality_postulate"
                                                                ("f"
                                                                 "series(LAMBDA j: integral[T1, S1, mu](F(j)))"
                                                                 "g"
                                                                 "integral[T1, S1, mu] o FF"))
                                                               (replace
                                                                -2
                                                                -1)
                                                               (assert)
                                                               (replace
                                                                -1)
                                                               (hide
                                                                -1
                                                                -2
                                                                -4)
                                                               (lemma
                                                                "monotone_convergence[T1, S1, mu]"
                                                                ("F"
                                                                 "FF"))
                                                               (case-replace
                                                                "ae_increasing?(FF)")
                                                               (("1"
                                                                 (case-replace
                                                                  "real_fun_preds.bounded?(integral[T1,S1,mu] o FF)")
                                                                 (("1"
                                                                   (assert)
                                                                   (flatten)
                                                                   (skosimp)
                                                                   (inst
                                                                    -
                                                                    "f!1")
                                                                   (assert)
                                                                   (typepred
                                                                    "f!1")
                                                                   (case
                                                                    "forall x: x_eq(x_limit(LAMBDA j: (TRUE,FF(j)(x))), nu(x_section(EE, x)))")
                                                                   (("1"
                                                                     (case
                                                                      "ae?(lambda x: x_eq((TRUE,plus(f!1)(x)),nu(x_section(EE, x))))")
                                                                     (("1"
                                                                       (hide
                                                                        -2)
                                                                       (case-replace
                                                                        "FORALL j: integrable?[T1, S1, contraction(mu, X!1)](G(j))")
                                                                       (("1"
                                                                         (name
                                                                          "GG"
                                                                          "lambda j: lambda x: series(LAMBDA i: G(i)(x))(j)")
                                                                         (hide
                                                                          -1)
                                                                         (case
                                                                          "FORALL j: integrable?[T1, S1, contraction(mu, X!1)](GG(j))")
                                                                         (("1"
                                                                           (case
                                                                            "forall j,x: GG(j)(x) >= 0")
                                                                           (("1"
                                                                             (case
                                                                              "forall j: series(LAMBDA i:
                                                                                                                                                                                     integral[T1, S1, contraction(mu, X!1)](G(i)))(j)=(integral[T1, S1, contraction(mu, X!1)] o GG)(j)")
                                                                             (("1"
                                                                               (case-replace
                                                                                "series(LAMBDA j:
                                                                                                                                                                                         integral[T1, S1, contraction(mu, X!1)](G(j)))=integral[T1, S1, contraction(mu, X!1)] o GG")
                                                                               (("1"
                                                                                 (case-replace
                                                                                  "l!1=integral[T1,S1,mu](f!1)")
                                                                                 (("1"
                                                                                   (hide
                                                                                    -1)
                                                                                   (case
                                                                                    "ae_nonneg?(f!1)")
                                                                                   (("1"
                                                                                     (case
                                                                                      "ae_eq?(f!1,*[T1](phi(X!1),f!1))")
                                                                                     (("1"
                                                                                       (hide
                                                                                        -4
                                                                                        -3)
                                                                                       (name
                                                                                        "HH"
                                                                                        "lambda j: *[T1](phi(X!1),GG(j))")
                                                                                       (case
                                                                                        "forall j: integrable?[T1, S1, mu](HH(j))")
                                                                                       (("1"
                                                                                         (case
                                                                                          "FORALL j, x: HH(j)(x) >= 0")
                                                                                         (("1"
                                                                                           (hide
                                                                                            -3
                                                                                            -6)
                                                                                           (case
                                                                                            "forall j: (integral[T1, S1, contraction(mu, X!1)] o GG)(j) = (integral[T1,S1,mu] o HH)(j)")
                                                                                           (("1"
                                                                                             (case-replace
                                                                                              "integral[T1, S1, contraction(mu, X!1)] o GG=integral[T1, S1, mu] o HH")
                                                                                             (("1"
                                                                                               (hide
                                                                                                -1
                                                                                                -2)
                                                                                               (lemma
                                                                                                "monotone_convergence[T1, S1, mu]"
                                                                                                ("F"
                                                                                                 "HH"))
                                                                                               (case-replace
                                                                                                "ae_increasing?(HH)")
                                                                                               (("1"
                                                                                                 (flatten)
                                                                                                 (hide
                                                                                                  -2
                                                                                                  -3)
                                                                                                 (lemma
                                                                                                  "indefinite_integrable[T1, S1, mu]"
                                                                                                  ("f"
                                                                                                   "f!1"
                                                                                                   "E"
                                                                                                   "X!1"))
                                                                                                 (inst
                                                                                                  -3
                                                                                                  "*[T1](phi(X!1), f!1)")
                                                                                                 (split
                                                                                                  -3)
                                                                                                 (("1"
                                                                                                   (expand
                                                                                                    "converges_upto?")
                                                                                                   (flatten)
                                                                                                   (name-replace
                                                                                                    "SS"
                                                                                                    "integral[T1, S1, mu] o HH")
                                                                                                   (lemma
                                                                                                    "integral_ae_eq[T1,S1,mu]"
                                                                                                    ("f"
                                                                                                     "f!1"
                                                                                                     "h"
                                                                                                     "*[T1](phi(X!1), f!1)"))
                                                                                                   (assert)
                                                                                                   (replace
                                                                                                    -1
                                                                                                    *
                                                                                                    rl)
                                                                                                   (name-replace
                                                                                                    "LIMIT"
                                                                                                    "integral[T1, S1, mu](f!1)")
                                                                                                   (hide-all-but
                                                                                                    (-2
                                                                                                     1))
                                                                                                   (expand
                                                                                                    "convergence")
                                                                                                   (rewrite
                                                                                                    "metric_convergence_def")
                                                                                                   (expand
                                                                                                    "metric_converges_to")
                                                                                                   (skosimp)
                                                                                                   (inst
                                                                                                    -
                                                                                                    "epsilon!1")
                                                                                                   (skosimp)
                                                                                                   (inst
                                                                                                    +
                                                                                                    "n!1")
                                                                                                   (skosimp)
                                                                                                   (inst
                                                                                                    -
                                                                                                    "i!1")
                                                                                                   (grind))
                                                                                                  ("2"
                                                                                                   (hide
                                                                                                    2)
                                                                                                   (hide-all-but
                                                                                                    (-6
                                                                                                     -9
                                                                                                     -20
                                                                                                     -21
                                                                                                     1))
                                                                                                   (expand
                                                                                                    "HH")
                                                                                                   (expand
                                                                                                    "ae_convergence?")
                                                                                                   (expand
                                                                                                    "ae_convergence_in?")
                                                                                                   (expand
                                                                                                    "ae_nonneg?")
                                                                                                   (expand
                                                                                                    "pointwise_ae?")
                                                                                                   (expand
                                                                                                    "ae?")
                                                                                                   (expand
                                                                                                    "fullset")
                                                                                                   (expand
                                                                                                    "ae_in?")
                                                                                                   (skosimp*)
                                                                                                   (inst
                                                                                                    +
                                                                                                    "union(E!2,E!3)")
                                                                                                   (skosimp)
                                                                                                   (expand
                                                                                                    "union")
                                                                                                   (inst
                                                                                                    -
                                                                                                    "x!1")
                                                                                                   (inst
                                                                                                    -
                                                                                                    "x!1")
                                                                                                   (assert)
                                                                                                   (flatten)
                                                                                                   (assert)
                                                                                                   (expand
                                                                                                    "plus")
                                                                                                   (expand
                                                                                                    "max")
                                                                                                   (expand
                                                                                                    "*")
                                                                                                   (expand
                                                                                                    "phi")
                                                                                                   (expand
                                                                                                    "member")
                                                                                                   (rewrite
                                                                                                    "metric_convergence_def")
                                                                                                   (expand
                                                                                                    "x_eq"
                                                                                                    -2)
                                                                                                   (flatten)
                                                                                                   (inst
                                                                                                    -
                                                                                                    "x!1")
                                                                                                   (inst
                                                                                                    -
                                                                                                    "x!1")
                                                                                                   (case-replace
                                                                                                    "X!1(x!1)")
                                                                                                   (("1"
                                                                                                     (expand
                                                                                                      "x_eq")
                                                                                                     (flatten)
                                                                                                     (assert)
                                                                                                     (lemma
                                                                                                      "x_limit_to_sum"
                                                                                                      ("S"
                                                                                                       "LAMBDA j: (TRUE,GG(j)(x!1))"
                                                                                                       "T"
                                                                                                       "LAMBDA j: (TRUE,G(j)(x!1))"))
                                                                                                     (("1"
                                                                                                       (split
                                                                                                        -1)
                                                                                                       (("1"
                                                                                                         (expand
                                                                                                          "x_eq")
                                                                                                         (flatten)
                                                                                                         (assert)
                                                                                                         (expand
                                                                                                          "x_sum")
                                                                                                         (case-replace
                                                                                                          "convergence_sequences.convergent?(series(LAMBDA j: G(j)(x!1)))")
                                                                                                         (("1"
                                                                                                           (replace
                                                                                                            -10)
                                                                                                           (replace
                                                                                                            -7
                                                                                                            *
                                                                                                            rl)
                                                                                                           (replace
                                                                                                            -9)
                                                                                                           (expand
                                                                                                            "x_limit")
                                                                                                           (case-replace
                                                                                                            "convergence_sequences.convergent?(LAMBDA i: GG(i)(x!1))")
                                                                                                           (("1"
                                                                                                             (case
                                                                                                              "convergence(LAMBDA j: GG(j)(x!1),f!1(x!1))")
                                                                                                             (("1"
                                                                                                               (hide-all-but
                                                                                                                (-1
                                                                                                                 3))
                                                                                                               (expand
                                                                                                                "metric_converges_to")
                                                                                                               (expand
                                                                                                                "convergence")
                                                                                                               (skosimp)
                                                                                                               (inst
                                                                                                                -
                                                                                                                "r!1")
                                                                                                               (skosimp)
                                                                                                               (inst
                                                                                                                +
                                                                                                                "n!1")
                                                                                                               (skosimp)
                                                                                                               (inst
                                                                                                                -
                                                                                                                "i!1")
                                                                                                               (grind))
                                                                                                              ("2"
                                                                                                               (lemma
                                                                                                                "convergence_sequences.limit_def"
                                                                                                                ("v"
                                                                                                                 "LAMBDA i: GG(i)(x!1)"
                                                                                                                 "l"
                                                                                                                 "f!1(x!1)"))
                                                                                                               (("1"
                                                                                                                 (assert))
                                                                                                                ("2"
                                                                                                                 (propax))))))
                                                                                                            ("2"
                                                                                                             (assert))))
                                                                                                          ("2"
                                                                                                           (assert))))
                                                                                                        ("2"
                                                                                                         (hide-all-but
                                                                                                          1)
                                                                                                         (skosimp)
                                                                                                         (expand
                                                                                                          "GG")
                                                                                                         (expand
                                                                                                          "series")
                                                                                                         (expand
                                                                                                          "x_sigma")
                                                                                                         (expand
                                                                                                          "x_eq")
                                                                                                         (propax))))
                                                                                                      ("2"
                                                                                                       (hide-all-but
                                                                                                        1)
                                                                                                       (expand
                                                                                                        "GG")
                                                                                                       (expand
                                                                                                        "series")
                                                                                                       (induct
                                                                                                        "j")
                                                                                                       (("1"
                                                                                                         (expand
                                                                                                          "sigma")
                                                                                                         (assert))
                                                                                                        ("2"
                                                                                                         (skosimp)
                                                                                                         (expand
                                                                                                          "sigma"
                                                                                                          1)
                                                                                                         (assert))))))
                                                                                                    ("2"
                                                                                                     (assert)
                                                                                                     (hide-all-but
                                                                                                      4)
                                                                                                     (expand
                                                                                                      "metric_converges_to")
                                                                                                     (skosimp)
                                                                                                     (inst
                                                                                                      +
                                                                                                      "0")
                                                                                                     (skosimp)
                                                                                                     (grind))))))
                                                                                                ("2"
                                                                                                 (hide-all-but
                                                                                                  (1
                                                                                                   -23))
                                                                                                 (expand
                                                                                                  "ae_increasing?")
                                                                                                 (expand
                                                                                                  "HH")
                                                                                                 (expand
                                                                                                  "*")
                                                                                                 (expand
                                                                                                  "phi")
                                                                                                 (expand
                                                                                                  "member")
                                                                                                 (inst
                                                                                                  +
                                                                                                  "emptyset")
                                                                                                 (skosimp)
                                                                                                 (hide
                                                                                                  1)
                                                                                                 (skosimp)
                                                                                                 (lift-if
                                                                                                  1)
                                                                                                 (assert)
                                                                                                 (prop)
                                                                                                 (expand
                                                                                                  "GG")
                                                                                                 (expand
                                                                                                  "series")
                                                                                                 (inst
                                                                                                  -
                                                                                                  "_"
                                                                                                  "x!1")
                                                                                                 (lemma
                                                                                                  "sigma_split"
                                                                                                  ("low"
                                                                                                   "0"
                                                                                                   "high"
                                                                                                   "j!1"
                                                                                                   "z"
                                                                                                   "i!1"
                                                                                                   "F"
                                                                                                   "LAMBDA i: G(i)(x!1)"))
                                                                                                 (assert)
                                                                                                 (replace
                                                                                                  -1)
                                                                                                 (assert))))
                                                                                              ("2"
                                                                                               (apply-extensionality
                                                                                                1
                                                                                                :hide?
                                                                                                t))))
                                                                                            ("2"
                                                                                             (hide
                                                                                              2)
                                                                                             (skosimp)
                                                                                             (expand
                                                                                              "o")
                                                                                             (expand
                                                                                              "HH")
                                                                                             (inst
                                                                                              -5
                                                                                              "j!1")
                                                                                             (lemma
                                                                                              "contraction_integral[T1,S1]"
                                                                                              ("A"
                                                                                               "X!1"
                                                                                               "f"
                                                                                               "GG(j!1)"
                                                                                               "mu"
                                                                                               "mu"))
                                                                                             (propax))
                                                                                            ("3"
                                                                                             (propax))))
                                                                                          ("2"
                                                                                           (expand
                                                                                            "HH")
                                                                                           (expand
                                                                                            "*")
                                                                                           (hide-all-but
                                                                                            (-5
                                                                                             1))
                                                                                           (skosimp)
                                                                                           (inst
                                                                                            -
                                                                                            "j!1"
                                                                                            "x!1")
                                                                                           (expand
                                                                                            "phi")
                                                                                           (lift-if
                                                                                            1)
                                                                                           (assert))))
                                                                                        ("2"
                                                                                         (hide-all-but
                                                                                          (1
                                                                                           -5))
                                                                                         (skosimp)
                                                                                         (inst
                                                                                          -
                                                                                          "j!1")
                                                                                         (lemma
                                                                                          "contraction_integrable[T1,S1]"
                                                                                          ("mu"
                                                                                           "mu"
                                                                                           "A"
                                                                                           "X!1"
                                                                                           "f"
                                                                                           "GG(j!1)"))
                                                                                         (("1"
                                                                                           (expand
                                                                                            "HH")
                                                                                           (assert))
                                                                                          ("2"
                                                                                           (lemma
                                                                                            "integrable_is_measurable[T1, S1, contraction(mu, X!1)]")
                                                                                           (inst
                                                                                            -
                                                                                            "GG(j!1)"))))))
                                                                                      ("2"
                                                                                       (hide-all-but
                                                                                        (1
                                                                                         -7
                                                                                         -1))
                                                                                       (expand
                                                                                        "ae_nonneg?")
                                                                                       (expand
                                                                                        "ae_eq?")
                                                                                       (expand
                                                                                        "restrict")
                                                                                       (expand
                                                                                        "pointwise_ae?")
                                                                                       (expand
                                                                                        "ae?")
                                                                                       (expand
                                                                                        "fullset")
                                                                                       (expand
                                                                                        "ae_in?")
                                                                                       (skosimp*)
                                                                                       (inst
                                                                                        +
                                                                                        "union(E!2,E!3)")
                                                                                       (skosimp)
                                                                                       (inst
                                                                                        -
                                                                                        "x!1")
                                                                                       (inst
                                                                                        -
                                                                                        "x!1")
                                                                                       (expand
                                                                                        "union")
                                                                                       (expand
                                                                                        "member")
                                                                                       (flatten)
                                                                                       (assert)
                                                                                       (expand
                                                                                        "plus")
                                                                                       (expand
                                                                                        "max")
                                                                                       (expand
                                                                                        "x_eq")
                                                                                       (flatten)
                                                                                       (expand
                                                                                        "*")
                                                                                       (expand
                                                                                        "phi")
                                                                                       (expand
                                                                                        "member")
                                                                                       (lift-if
                                                                                        3)
                                                                                       (assert)
                                                                                       (prop)
                                                                                       (expand
                                                                                        "EE")
                                                                                       (expand
                                                                                        "cross_product")
                                                                                       (expand
                                                                                        "intersection")
                                                                                       (expand
                                                                                        "x_section")
                                                                                       (expand
                                                                                        "member")
                                                                                       (assert)
                                                                                       (typepred
                                                                                        "nu")
                                                                                       (expand
                                                                                        "sigma_finite_measure?")
                                                                                       (expand
                                                                                        "measure?")
                                                                                       (flatten)
                                                                                       (expand
                                                                                        "measure_empty?")
                                                                                       (expand
                                                                                        "emptyset")
                                                                                       (assert)
                                                                                       (replace
                                                                                        -1)
                                                                                       (assert))))
                                                                                    ("2"
                                                                                     (hide-all-but
                                                                                      (1
                                                                                       -9
                                                                                       -10
                                                                                       -26))
                                                                                     (expand
                                                                                      "ae_increasing?")
                                                                                     (expand
                                                                                      "ae_convergence?")
                                                                                     (expand
                                                                                      "ae_convergence_in?")
                                                                                     (expand
                                                                                      "ae_nonneg?")
                                                                                     (expand
                                                                                      "pointwise_ae?")
                                                                                     (expand
                                                                                      "ae?")
                                                                                     (expand
                                                                                      "fullset")
                                                                                     (expand
                                                                                      "ae_in?")
                                                                                     (skosimp*)
                                                                                     (inst
                                                                                      +
                                                                                      "union(E!2,E!3)")
                                                                                     (skosimp)
                                                                                     (inst
                                                                                      -
                                                                                      "x!1")
                                                                                     (inst
                                                                                      -
                                                                                      "x!1")
                                                                                     (expand
                                                                                      "union")
                                                                                     (expand
                                                                                      "member")
                                                                                     (flatten)
                                                                                     (assert)
                                                                                     (rewrite
                                                                                      "metric_convergence_def")
                                                                                     (expand
                                                                                      "metric_converges_to")
                                                                                     (inst
                                                                                      -3
                                                                                      "0"
                                                                                      "x!1")
                                                                                     (inst
                                                                                      -
                                                                                      "F(0)(x!1)-f!1(x!1)")
                                                                                     (("1"
                                                                                       (skosimp)
                                                                                       (inst
                                                                                        -
                                                                                        "0"
                                                                                        "n!1")
                                                                                       (inst
                                                                                        -
                                                                                        "n!1")
                                                                                       (expand
                                                                                        "FF"
                                                                                        -1
                                                                                        1)
                                                                                       (expand
                                                                                        "series")
                                                                                       (expand
                                                                                        "sigma")
                                                                                       (assert)
                                                                                       (expand
                                                                                        "ball")
                                                                                       (assert))
                                                                                      ("2"
                                                                                       (assert))))))
                                                                                  ("2"
                                                                                   (expand
                                                                                    "converges_upto?")
                                                                                   (flatten)
                                                                                   (name-replace
                                                                                    "SS"
                                                                                    "integral[T1, S1, mu] o FF")
                                                                                   (name-replace
                                                                                    "RHS"
                                                                                    "integral[T1, S1, mu](f!1)")
                                                                                   (hide-all-but
                                                                                    (1
                                                                                     -11
                                                                                     -15))
                                                                                   (lemma
                                                                                    "convergence_sequences.unique_limit"
                                                                                    ("u"
                                                                                     "SS"
                                                                                     "l1"
                                                                                     "l!1"
                                                                                     "l2"
                                                                                     "RHS"))
                                                                                   (assert)
                                                                                   (hide
                                                                                    -2
                                                                                    2)
                                                                                   (expand
                                                                                    "convergence")
                                                                                   (rewrite
                                                                                    "metric_convergence_def")
                                                                                   (expand
                                                                                    "metric_converges_to")
                                                                                   (skosimp)
                                                                                   (inst
                                                                                    -
                                                                                    "epsilon!1")
                                                                                   (skosimp)
                                                                                   (inst
                                                                                    +
                                                                                    "n!1")
                                                                                   (skosimp)
                                                                                   (inst
                                                                                    -
                                                                                    "i!1")
                                                                                   (grind))))
                                                                                ("2"
                                                                                 (apply-extensionality
                                                                                  :hide?
                                                                                  t))))
                                                                              ("2"
                                                                               (hide
                                                                                2)
                                                                               (expand
                                                                                "o ")
                                                                               (expand
                                                                                "GG")
                                                                               (expand
                                                                                "series")
                                                                               (induct
                                                                                "j")
                                                                               (("1"
                                                                                 (expand
                                                                                  "sigma")
                                                                                 (assert)
                                                                                 (expand
                                                                                  "G")
                                                                                 (expand
                                                                                  "o ")
                                                                                 (propax))
                                                                                ("2"
                                                                                 (skosimp)
                                                                                 (expand
                                                                                  "sigma"
                                                                                  1)
                                                                                 (replace
                                                                                  -1)
                                                                                 (hide
                                                                                  -1)
                                                                                 (lemma
                                                                                  "integral_add[T1, S1, contraction(mu, X!1)]"
                                                                                  ("f1"
                                                                                   "G(1 + j!1)"
                                                                                   "f2"
                                                                                   "LAMBDA x: sigma(0, j!1, LAMBDA i: G(i)(x))"))
                                                                                 (("1"
                                                                                   (expand
                                                                                    "+")
                                                                                   (assert))
                                                                                  ("2"
                                                                                   (inst
                                                                                    -2
                                                                                    "j!1"))))))
                                                                              ("3"
                                                                               (propax))
                                                                              ("4"
                                                                               (propax))))
                                                                            ("2"
                                                                             (hide-all-but
                                                                              (-18
                                                                               1))
                                                                             (expand
                                                                              "GG")
                                                                             (expand
                                                                              "series")
                                                                             (skosimp)
                                                                             (inst
                                                                              -
                                                                              "_"
                                                                              "x!1")
                                                                             (assert))))
                                                                          ("2"
                                                                           (hide-all-but
                                                                            (-1
                                                                             1))
                                                                           (expand
                                                                            "GG")
                                                                           (expand
                                                                            "series")
                                                                           (induct
                                                                            "j")
                                                                           (("1"
                                                                             (expand
                                                                              "sigma")
                                                                             (assert)
                                                                             (inst
                                                                              -
                                                                              "0")
                                                                             (expand
                                                                              "G")
                                                                             (expand
                                                                              "o ")
                                                                             (propax))
                                                                            ("2"
                                                                             (skosimp)
                                                                             (expand
                                                                              "sigma"
                                                                              1)
                                                                             (inst
                                                                              -
                                                                              "1+j!1")
                                                                             (lemma
                                                                              "integrable_add[T1, S1, contraction(mu, X!1)]"
                                                                              ("f1"
                                                                               "G(1 + j!1)"
                                                                               "f2"
                                                                               "LAMBDA x: sigma(0, j!1, LAMBDA i: G(i)(x))"))
                                                                             (("1"
                                                                               (expand
                                                                                "+")
                                                                               (propax))
                                                                              ("2"
                                                                               (propax))
                                                                              ("3"
                                                                               (propax))))))))
                                                                        ("2"
                                                                         (hide
                                                                          2)
                                                                         (skosimp)
                                                                         (rewrite
                                                                          "contraction_integrable[T1,S1]")
                                                                         (("1"
                                                                           (expand
                                                                            "G"
                                                                            1)
                                                                           (lemma
                                                                            "integral_ae_abs[T1, S1, mu]"
                                                                            ("h"
                                                                             "*[T1](phi[T1, S1](X!1),
                                                                                                                                                                         (fm_contraction[T2, S2]
                                                                                                                                                                              (contraction(nu, Y!1),
                                                                                                                                                                               A_of(contraction(nu, Y!1))(j!1))
                                                                                                                                                                           o x_section(E!1)))"
                                                                             "f"
                                                                             "plus(f!1)"))
                                                                           (("1"
                                                                             (assert)
                                                                             (hide-all-but
                                                                              (-1
                                                                               -12
                                                                               1))
                                                                             (expand
                                                                              "ae_le?")
                                                                             (expand
                                                                              "pointwise_ae?")
                                                                             (expand
                                                                              "ae?")
                                                                             (expand
                                                                              "fullset")
                                                                             (expand
                                                                              "ae_in?")
                                                                             (skosimp)
                                                                             (inst
                                                                              +
                                                                              "E!2")
                                                                             (skosimp)
                                                                             (expand
                                                                              "phi")
                                                                             (expand
                                                                              "member")
                                                                             (inst
                                                                              -
                                                                              "x!1")
                                                                             (inst
                                                                              -
                                                                              "x!1")
                                                                             (expand
                                                                              "abs"
                                                                              2)
                                                                             (expand
                                                                              "*")
                                                                             (case-replace
                                                                              "X!1(x!1)")
                                                                             (("1"
                                                                               (expand
                                                                                "o")
                                                                               (rewrite
                                                                                "one_times")
                                                                               (expand
                                                                                "abs"
                                                                                2)
                                                                               (assert)
                                                                               (typepred
                                                                                "plus(f!1)(x!1)")
                                                                               (assert)
                                                                               (expand
                                                                                "x_eq")
                                                                               (flatten)
                                                                               (assert)
                                                                               (replace
                                                                                -4
                                                                                *
                                                                                rl)
                                                                               (expand
                                                                                "x_section"
                                                                                2)
                                                                               (expand
                                                                                "fm_contraction"
                                                                                2)
                                                                               (lemma
                                                                                "m_monotone[T2,S2,contraction(nu, Y!1)]"
                                                                                ("a"
                                                                                 "intersection(A_of(contraction(nu, Y!1))(j!1),
                                                                                                                                                                                                x_section(E!1, x!1))"
                                                                                 "b"
                                                                                 "x_section(E!1, x!1)"))
                                                                               (("1"
                                                                                 (expand
                                                                                  "x_le")
                                                                                 (assert)
                                                                                 (hide-all-but
                                                                                  1)
                                                                                 (expand
                                                                                  "intersection")
                                                                                 (expand
                                                                                  "subset?")
                                                                                 (expand
                                                                                  "member")
                                                                                 (skosimp))
                                                                                ("2"
                                                                                 (assert)
                                                                                 (lemma
                                                                                  "x_section_measurable"
                                                                                  ("S1"
                                                                                   "S1"
                                                                                   "S2"
                                                                                   "S2"
                                                                                   "x"
                                                                                   "x!1"
                                                                                   "Z"
                                                                                   "E!1"))
                                                                                 (expand
                                                                                  "measurable_set?")
                                                                                 (assert))
                                                                                ("3"
                                                                                 (hide-all-but
                                                                                  1)
                                                                                 (typepred
                                                                                  "A_of[T2, S2](contraction[T2, S2](nu, Y!1))(j!1)")
                                                                                 (lemma
                                                                                  "x_section_measurable"
                                                                                  ("S1"
                                                                                   "S1"
                                                                                   "S2"
                                                                                   "S2"
                                                                                   "x"
                                                                                   "x!1"
                                                                                   "Z"
                                                                                   "E!1"))
                                                                                 (expand
                                                                                  "member")
                                                                                 (lemma
                                                                                  "measurable_intersection[T2,S2]"
                                                                                  ("a"
                                                                                   "A_of[T2, S2](contraction[T2, S2](nu, Y!1))(j!1)"
                                                                                   "b"
                                                                                   "x_section[T1, T2](E!1, x!1)"))
                                                                                 (("1"
                                                                                   (propax))
                                                                                  ("2"
                                                                                   (expand
                                                                                    "measurable_set?")
                                                                                   (propax))
                                                                                  ("3"
                                                                                   (expand
                                                                                    "measurable_set?")
                                                                                   (propax))))))
                                                                              ("2"
                                                                               (assert))))
                                                                            ("2"
                                                                             (rewrite
                                                                              "prod_measurable")
                                                                             (rewrite
                                                                              "x_section_measurable"))))
                                                                          ("2"
                                                                           (expand
                                                                            "G")
                                                                           (rewrite
                                                                            "x_section_measurable"
                                                                            1))))))
                                                                      ("2"
                                                                       (hide-all-but
                                                                        (-1
                                                                         -4
                                                                         -5
                                                                         1))
                                                                       (expand
                                                                        "ae_increasing?")
                                                                       (expand
                                                                        "ae_convergence?")
                                                                       (expand
                                                                        "ae_convergence_in?")
                                                                       (expand
                                                                        "ae?")
                                                                       (expand
                                                                        "fullset")
                                                                       (expand
                                                                        "ae_in?")
                                                                       (skosimp*)
                                                                       (inst
                                                                        +
                                                                        "union(E!2,E!3)")
                                                                       (skosimp)
                                                                       (inst
                                                                        -
                                                                        "x!1")
                                                                       (inst
                                                                        -
                                                                        "x!1")
                                                                       (inst
                                                                        -
                                                                        "x!1")
                                                                       (expand
                                                                        "union")
                                                                       (expand
                                                                        "member")
                                                                       (flatten)
                                                                       (assert)
                                                                       (expand
                                                                        "x_eq"
                                                                        3)
                                                                       (expand
                                                                        "x_limit")
                                                                       (case
                                                                        "convergence(LAMBDA (n:nat): FF(n)(x!1), f!1(x!1))")
                                                                       (("1"
                                                                         (lemma
                                                                          "convergence_sequences.limit_def"
                                                                          ("v"
                                                                           "LAMBDA (n: nat): FF(n)(x!1)"
                                                                           "l"
                                                                           "f!1(x!1)"))
                                                                         (("1"
                                                                           (assert)
                                                                           (replace
                                                                            -1)
                                                                           (case-replace
                                                                            "convergence_sequences.convergent?(LAMBDA i: FF(i)(x!1))")
                                                                           (("1"
                                                                             (expand
                                                                              "x_eq")
                                                                             (flatten)
                                                                             (assert)
                                                                             (expand
                                                                              "plus")
                                                                             (assert)
                                                                             (expand
                                                                              "max")
                                                                             (propax))
                                                                            ("2"
                                                                             (expand
                                                                              "convergence_sequences.convergent?")
                                                                             (inst
                                                                              +
                                                                              "f!1(x!1)"))))
                                                                          ("2"
                                                                           (expand
                                                                            "convergence_sequences.convergent?")
                                                                           (inst
                                                                            +
                                                                            "f!1(x!1)"))))
                                                                        ("2"
                                                                         (hide-all-but
                                                                          (-3
                                                                           1))
                                                                         (expand
                                                                          "convergence")
                                                                         (rewrite
                                                                          "metric_convergence_def")
                                                                         (expand
                                                                          "metric_converges_to")
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "epsilon!1")
                                                                         (skosimp)
                                                                         (inst
                                                                          +
                                                                          "n!1")
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "i!1")
                                                                         (grind))))))
                                                                    ("2"
                                                                     (hide-all-but
                                                                      (1
                                                                       -17
                                                                       -18
                                                                       -19
                                                                       -20
                                                                       -21
                                                                       -22))
                                                                     (skosimp)
                                                                     (inst
                                                                      -
                                                                      "x!1")
                                                                     (name-replace
                                                                      "RHS"
                                                                      "nu(x_section(EE, x!1))")
                                                                     (lemma
                                                                      "x_limit_to_sum"
                                                                      ("S"
                                                                       "LAMBDA j: (TRUE, FF(j)(x!1))"
                                                                       "T"
                                                                       "LAMBDA j: (TRUE, F(j)(x!1))"))
                                                                     (("1"
                                                                       (split
                                                                        -1)
                                                                       (("1"
                                                                         (name-replace
                                                                          "LHS"
                                                                          "x_limit(LAMBDA j: (TRUE, FF(j)(x!1)))")
                                                                         (hide-all-but
                                                                          (-1
                                                                           -2
                                                                           1))
                                                                         (expand
                                                                          "x_sum")
                                                                         (expand
                                                                          "x_eq")
                                                                         (flatten)
                                                                         (case-replace
                                                                          "convergence_sequences.convergent?(series(LAMBDA i: F(i)(x!1)))")
                                                                         (("1"
                                                                           (assert))
                                                                          ("2"
                                                                           (assert))))
                                                                        ("2"
                                                                         (hide
                                                                          2
                                                                          -1)
                                                                         (expand
                                                                          "FF")
                                                                         (expand
                                                                          "series")
                                                                         (hide-all-but
                                                                          1)
                                                                         (skosimp)
                                                                         (expand
                                                                          "x_sigma")
                                                                         (expand
                                                                          "x_eq")
                                                                         (propax))))
                                                                      ("2"
                                                                       (hide-all-but
                                                                        (1
                                                                         -4))
                                                                       (expand
                                                                        "FF")
                                                                       (expand
                                                                        "series")
                                                                       (induct
                                                                        "j")
                                                                       (("1"
                                                                         (expand
                                                                          "sigma")
                                                                         (assert))
                                                                        ("2"
                                                                         (skosimp)
                                                                         (expand
                                                                          "sigma"
                                                                          1)
                                                                         (inst
                                                                          -
                                                                          "1+j!1"
                                                                          "x!1")
                                                                         (assert))))))
                                                                    ("3"
                                                                     (skolem
                                                                      +
                                                                      ("x!1"
                                                                       "_"))
                                                                     (hide-all-but
                                                                      (1
                                                                       -20))
                                                                     (expand
                                                                      "FF")
                                                                     (expand
                                                                      "series")
                                                                     (induct
                                                                      "j")
                                                                     (("1"
                                                                       (expand
                                                                        "sigma")
                                                                       (assert))
                                                                      ("2"
                                                                       (skosimp)
                                                                       (expand
                                                                        "sigma"
                                                                        1)
                                                                       (assert))))))
                                                                  ("2"
                                                                   (hide
                                                                    2)
                                                                   (expand
                                                                    "bounded?"
                                                                    1)
                                                                   (split)
                                                                   (("1"
                                                                     (expand
                                                                      "bounded_above?")
                                                                     (inst
                                                                      +
                                                                      "l!1")
                                                                     (skolem
                                                                      +
                                                                      "n!1")
                                                                     (case
                                                                      "increasing?(integral[T1, S1, mu] o FF)")
                                                                     (("1"
                                                                       (name-replace
                                                                        "HH"
                                                                        "integral[T1, S1, mu] o FF")
                                                                       (hide-all-but
                                                                        (-1
                                                                         -6
                                                                         1))
                                                                       (expand
                                                                        "convergence")
                                                                       (inst
                                                                        -
                                                                        "HH(n!1)-l!1")
                                                                       (("1"
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "n!1+n!2")
                                                                         (expand
                                                                          "increasing?")
                                                                         (inst
                                                                          -
                                                                          "n!1"
                                                                          "n!1+n!2")
                                                                         (grind))
                                                                        ("2"
                                                                         (assert))))
                                                                      ("2"
                                                                       (hide-all-but
                                                                        (1
                                                                         -1))
                                                                       (expand
                                                                        "increasing?")
                                                                       (skolem
                                                                        +
                                                                        ("i!3"
                                                                         "j!3"))
                                                                       (flatten)
                                                                       (expand
                                                                        "o ")
                                                                       (expand
                                                                        "ae_increasing?")
                                                                       (skosimp)
                                                                       (expand
                                                                        "member")
                                                                       (lemma
                                                                        "integral_ae_le[T1, S1, mu]"
                                                                        ("f1"
                                                                         "FF(i!3)"
                                                                         "f2"
                                                                         "FF(j!3)"))
                                                                       (assert)
                                                                       (expand
                                                                        "ae_le?")
                                                                       (expand
                                                                        "pointwise_ae?")
                                                                       (hide
                                                                        2)
                                                                       (expand
                                                                        "ae?")
                                                                       (expand
                                                                        "fullset")
                                                                       (expand
                                                                        "ae_in?")
                                                                       (inst
                                                                        +
                                                                        "E!2")
                                                                       (skosimp)
                                                                       (expand
                                                                        "member")
                                                                       (inst
                                                                        -
                                                                        "x!1")
                                                                       (assert)
                                                                       (inst
                                                                        -
                                                                        "i!3"
                                                                        "j!3")
                                                                       (assert))))
                                                                    ("2"
                                                                     (expand
                                                                      "bounded_below?")
                                                                     (inst
                                                                      +
                                                                      "0")
                                                                     (skolem
                                                                      +
                                                                      "n!1")
                                                                     (expand
                                                                      "o ")
                                                                     (hide-all-but
                                                                      (-1
                                                                       1
                                                                       -4
                                                                       -17))
                                                                     (lemma
                                                                      "integral_nonneg[T1, S1, mu]"
                                                                      ("f"
                                                                       "F(0)"))
                                                                     (("1"
                                                                       (inst
                                                                        -
                                                                        "0"
                                                                        "_")
                                                                       (replace
                                                                        -4)
                                                                       (lemma
                                                                        "integral_ae_le[T1, S1, mu]"
                                                                        ("f1"
                                                                         "F(0)"
                                                                         "f2"
                                                                         "FF(n!1)"))
                                                                       (assert)
                                                                       (hide-all-but
                                                                        (-2
                                                                         1))
                                                                       (expand
                                                                        "ae_increasing?")
                                                                       (expand
                                                                        "ae_le?")
                                                                       (expand
                                                                        "pointwise_ae?")
                                                                       (expand
                                                                        "ae?")
                                                                       (expand
                                                                        "fullset")
                                                                       (expand
                                                                        "ae_in?")
                                                                       (skosimp)
                                                                       (inst
                                                                        +
                                                                        "E!2")
                                                                       (skosimp)
                                                                       (expand
                                                                        "member")
                                                                       (inst
                                                                        -
                                                                        "x!1")
                                                                       (assert)
                                                                       (inst
                                                                        -
                                                                        "0"
                                                                        "n!1")
                                                                       (assert)
                                                                       (expand
                                                                        "FF"
                                                                        -1
                                                                        1)
                                                                       (expand
                                                                        "series")
                                                                       (expand
                                                                        "sigma")
                                                                       (assert))
                                                                      ("2"
                                                                       (inst
                                                                        -
                                                                        "0"))))))))
                                                                ("2"
                                                                 (hide-all-but
                                                                  (1
                                                                   -16))
                                                                 (expand
                                                                  "FF")
                                                                 (expand
                                                                  "ae_increasing?")
                                                                 (inst
                                                                  +
                                                                  "emptyset")
                                                                 (skosimp)
                                                                 (skosimp)
                                                                 (expand
                                                                  "series")
                                                                 (hide 1)
                                                                 (lemma
                                                                  "sigma_split"
                                                                  ("low"
                                                                   "0"
                                                                   "high"
                                                                   "j!1"
                                                                   "z"
                                                                   "i!1"
                                                                   "F"
                                                                   "LAMBDA i: F(i)(x!1)"))
                                                                 (assert)
                                                                 (replace
                                                                  -1)
                                                                 (assert))))
                                                              ("2"
                                                               (hide-all-but
                                                                (-1
                                                                 -3
                                                                 1))
                                                               (induct
                                                                "n")
                                                               (("1"
                                                                 (expand
                                                                  "o ")
                                                                 (expand
                                                                  "FF")
                                                                 (expand
                                                                  "series")
                                                                 (expand
                                                                  "sigma")
                                                                 (assert)
                                                                 (expand
                                                                  "F")
                                                                 (expand
                                                                  "o")
                                                                 (propax))
                                                                ("2"
                                                                 (skosimp)
                                                                 (expand
                                                                  "FF")
                                                                 (expand
                                                                  "series")
                                                                 (assert)
                                                                 (expand
                                                                  "o")
                                                                 (expand
                                                                  "sigma"
                                                                  1)
                                                                 (replace
                                                                  -1)
                                                                 (lemma
                                                                  "integral_add[T1, S1, mu]"
                                                                  ("f1"
                                                                   "F(1 + j!1)"
                                                                   "f2"
                                                                   "LAMBDA x: sigma(0, j!1, LAMBDA i: F(i)(x))"))
                                                                 (("1"
                                                                   (expand
                                                                    "+")
                                                                   (assert))
                                                                  ("2"
                                                                   (inst
                                                                    -2
                                                                    "j!1"))))))
                                                              ("3"
                                                               (propax))
                                                              ("4"
                                                               (propax))))
                                                            ("2"
                                                             (hide-all-but
                                                              (1 -2))
                                                             (induct "j")
                                                             (("1"
                                                               (expand
                                                                "FF")
                                                               (assert)
                                                               (expand
                                                                "series")
                                                               (expand
                                                                "sigma")
                                                               (assert)
                                                               (inst
                                                                -
                                                                "0")
                                                               (rewrite
                                                                "eta")
                                                               (expand
                                                                "F")
                                                               (assert)
                                                               (expand
                                                                "o")
                                                               (propax))
                                                              ("2"
                                                               (skosimp)
                                                               (expand
                                                                "FF")
                                                               (expand
                                                                "series")
                                                               (expand
                                                                "sigma"
                                                                1)
                                                               (inst
                                                                -
                                                                "1+j!1")
                                                               (lemma
                                                                "integrable_add[T1, S1, mu]"
                                                                ("f1"
                                                                 "F(1 + j!1)"
                                                                 "f2"
                                                                 "LAMBDA x: sigma(0, j!1, LAMBDA i: F(i)(x))"))
                                                               (("1"
                                                                 (expand
                                                                  "+")
                                                                 (propax))
                                                                ("2"
                                                                 (propax))
                                                                ("3"
                                                                 (propax))))))))
                                                          ("2"
                                                           (flatten)
                                                           (name
                                                            "GG"
                                                            "lambda j: lambda x: series(lambda i: *[T1](phi(X!1),G(i))(x))(j)")
                                                           (case
                                                            "forall j: integrable?[T1, S1, mu](GG(j))")
                                                           (("1"
                                                             (case
                                                              "forall j,x: GG(j)(x)>=0")
                                                             (("1"
                                                               (case
                                                                "pointwise_increasing?(GG)")
                                                               (("1"
                                                                 (hide
                                                                  -4)
                                                                 (case
                                                                  "forall (n:nat): series(LAMBDA j: integral[T1, S1, contraction(mu, X!1)](G(j)))(n) = (integral[T1, S1, mu] o GG)(n)")
                                                                 (("1"
                                                                   (lemma
                                                                    "extensionality_postulate"
                                                                    ("f"
                                                                     "series(LAMBDA j: integral[T1, S1, contraction(mu, X!1)](G(j)))"
                                                                     "g"
                                                                     "integral[T1, S1, mu] o GG"))
                                                                   (replace
                                                                    -2
                                                                    -1)
                                                                   (assert)
                                                                   (replace
                                                                    -1)
                                                                   (hide
                                                                    -1
                                                                    -2
                                                                    -8)
                                                                   (lemma
                                                                    "monotone_convergence[T1, S1, mu]"
                                                                    ("F"
                                                                     "GG"))
                                                                   (split
                                                                    -1)
                                                                   (("1"
                                                                     (flatten)
                                                                     (hide
                                                                      -1)
                                                                     (case-replace
                                                                      "real_fun_preds.bounded?(integral[T1,S1,mu] o GG)")
                                                                     (("1"
                                                                       (skolem
                                                                        -
                                                                        "g!1")
                                                                       (inst
                                                                        -
                                                                        "g!1")
                                                                       (assert)
                                                                       (typepred
                                                                        "g!1")
                                                                       (case-replace
                                                                        "l!1=integral(g!1)")
                                                                       (("1"
                                                                         (hide
                                                                          -1)
                                                                         (case
                                                                          "ae_nonneg?(g!1)")
                                                                         (("1"
                                                                           (hide
                                                                            -3)
                                                                           (case
                                                                            "forall x: x_eq(x_limit(LAMBDA j: (TRUE,GG(j)(x))), nu(x_section(EE, x)))")
                                                                           (("1"
                                                                             (hide
                                                                              -10
                                                                              -12
                                                                              -13
                                                                              -14
                                                                              -15)
                                                                             (case
                                                                              "ae?(lambda x: x_eq((TRUE,plus(g!1)(x)),nu(x_section(EE, x))))")
                                                                             (("1"
                                                                               (name
                                                                                "FF"
                                                                                "lambda j: lambda x: series(LAMBDA i: F(i)(x))(j)")
                                                                               (hide
                                                                                -1)
                                                                               (case
                                                                                "forall j,x: FF(j)(x)>=0")
                                                                               (("1"
                                                                                 (case
                                                                                  "FORALL x:
                                                                                                                                                                          x_eq(x_limit(LAMBDA j: (TRUE, FF(j)(x))), nu(x_section(EE, x)))")
                                                                                 (("1"
                                                                                   (case
                                                                                    "pointwise_increasing?(FF)")
                                                                                   (("1"
                                                                                     (case
                                                                                      "ae_convergence?(FF, g!1)")
                                                                                     (("1"
                                                                                       (case-replace
                                                                                        "FORALL j: integrable?[T1, S1, mu](F(j))")
                                                                                       (("1"
                                                                                         (case-replace
                                                                                          "FORALL j: integrable?[T1, S1, mu](FF(j))")
                                                                                         (("1"
                                                                                           (case
                                                                                            "forall (n:nat): series(LAMBDA j: integral[T1, S1, mu](F(j)))(n)= (integral[T1,S1,mu] o FF)(n)")
                                                                                           (("1"
                                                                                             (case-replace
                                                                                              "series(LAMBDA j: integral[T1, S1, mu](F(j)))=integral[T1, S1, mu] o FF")
                                                                                             (("1"
                                                                                               (hide
                                                                                                -1
                                                                                                -2)
                                                                                               (lemma
                                                                                                "monotone_convergence[T1, S1, mu]"
                                                                                                ("F"
                                                                                                 "FF"))
                                                                                               (split
                                                                                                -1)
                                                                                               (("1"
                                                                                                 (flatten)
                                                                                                 (hide
                                                                                                  -1
                                                                                                  -2)
                                                                                                 (inst
                                                                                                  -
                                                                                                  "g!1")
                                                                                                 (assert)
                                                                                                 (expand
                                                                                                  "converges_upto?")
                                                                                                 (flatten)
                                                                                                 (name-replace
                                                                                                  "SS"
                                                                                                  "integral[T1, S1, mu] o FF")
                                                                                                 (name-replace
                                                                                                  "LIMIT"
                                                                                                  "integral[T1, S1, mu](g!1)")
                                                                                                 (hide-all-but
                                                                                                  (-1
                                                                                                   1))
                                                                                                 (expand
                                                                                                  "convergence")
                                                                                                 (rewrite
                                                                                                  "metric_convergence_def")
                                                                                                 (expand
                                                                                                  "metric_converges_to")
                                                                                                 (skosimp)
                                                                                                 (inst
                                                                                                  -
                                                                                                  "epsilon!1")
                                                                                                 (skosimp)
                                                                                                 (inst
                                                                                                  +
                                                                                                  "n!1")
                                                                                                 (skosimp)
                                                                                                 (inst
                                                                                                  -
                                                                                                  "i!1")
                                                                                                 (grind))
                                                                                                ("2"
                                                                                                 (hide-all-but
                                                                                                  (-4
                                                                                                   1))
                                                                                                 (expand
                                                                                                  "ae_increasing?")
                                                                                                 (inst
                                                                                                  +
                                                                                                  "emptyset")
                                                                                                 (skosimp)
                                                                                                 (expand
                                                                                                  "pointwise_increasing?")
                                                                                                 (inst
                                                                                                  -
                                                                                                  "x!1")
                                                                                                 (expand
                                                                                                  "increasing?")
                                                                                                 (propax))))
                                                                                              ("2"
                                                                                               (apply-extensionality
                                                                                                :hide?
                                                                                                t))))
                                                                                            ("2"
                                                                                             (hide
                                                                                              2)
                                                                                             (expand
                                                                                              "o"
                                                                                              1)
                                                                                             (hide-all-but
                                                                                              (-1
                                                                                               1
                                                                                               -2))
                                                                                             (expand
                                                                                              "FF")
                                                                                             (expand
                                                                                              "series")
                                                                                             (induct
                                                                                              "n")
                                                                                             (("1"
                                                                                               (expand
                                                                                                "sigma")
                                                                                               (assert)
                                                                                               (expand
                                                                                                "F")
                                                                                               (expand
                                                                                                "o")
                                                                                               (propax))
                                                                                              ("2"
                                                                                               (skosimp)
                                                                                               (expand
                                                                                                "sigma"
                                                                                                1)
                                                                                               (replace
                                                                                                -1)
                                                                                               (hide
                                                                                                -1)
                                                                                               (inst
                                                                                                -
                                                                                                "j!1")
                                                                                               (inst
                                                                                                -
                                                                                                "1+j!1")
                                                                                               (lemma
                                                                                                "integral_add[T1, S1, mu]"
                                                                                                ("f1"
                                                                                                 "F(1 + j!1)"
                                                                                                 "f2"
                                                                                                 "LAMBDA x: sigma(0, j!1, LAMBDA i: F(i)(x))"))
                                                                                               (("1"
                                                                                                 (expand
                                                                                                  "+")
                                                                                                 (assert))
                                                                                                ("2"
                                                                                                 (propax))))))
                                                                                            ("3"
                                                                                             (propax))
                                                                                            ("4"
                                                                                             (propax))))
                                                                                          ("2"
                                                                                           (hide-all-but
                                                                                            (-1
                                                                                             1))
                                                                                           (expand
                                                                                            "FF")
                                                                                           (expand
                                                                                            "series")
                                                                                           (induct
                                                                                            "j")
                                                                                           (("1"
                                                                                             (inst
                                                                                              -
                                                                                              "0")
                                                                                             (expand
                                                                                              "sigma")
                                                                                             (expand
                                                                                              "F")
                                                                                             (expand
                                                                                              "o")
                                                                                             (assert))
                                                                                            ("2"
                                                                                             (skosimp)
                                                                                             (expand
                                                                                              "sigma"
                                                                                              1)
                                                                                             (inst
                                                                                              -
                                                                                              "1+j!1")
                                                                                             (lemma
                                                                                              "integrable_add[T1, S1, mu]"
                                                                                              ("f1"
                                                                                               "F(1 + j!1)"
                                                                                               "f2"
                                                                                               "LAMBDA x: sigma(0, j!1, LAMBDA i: F(i)(x))"))
                                                                                             (("1"
                                                                                               (expand
                                                                                                "+")
                                                                                               (propax))
                                                                                              ("2"
                                                                                               (propax))
                                                                                              ("3"
                                                                                               (propax))))))))
                                                                                        ("2"
                                                                                         (hide
                                                                                          2)
                                                                                         (case
                                                                                          "forall j,x: F(j)(x)<=FF(j)(x)")
                                                                                         (("1"
                                                                                           (skosimp)
                                                                                           (inst
                                                                                            -
                                                                                            "j!1"
                                                                                            "_")
                                                                                           (case
                                                                                            "ae_le?(F(j!1),g!1)")
                                                                                           (("1"
                                                                                             (lemma
                                                                                              "integral_ae_abs[T1,S1,mu]"
                                                                                              ("h"
                                                                                               "F(j!1)"
                                                                                               "f"
                                                                                               "g!1"))
                                                                                             (("1"
                                                                                               (assert)
                                                                                               (hide-all-but
                                                                                                (-1
                                                                                                 -9
                                                                                                 -23
                                                                                                 1))
                                                                                               (expand
                                                                                                "ae_nonneg?")
                                                                                               (expand
                                                                                                "ae_le?")
                                                                                               (expand
                                                                                                "pointwise_ae?")
                                                                                               (expand
                                                                                                "ae?")
                                                                                               (expand
                                                                                                "fullset")
                                                                                               (expand
                                                                                                "ae_in?")
                                                                                               (skosimp*)
                                                                                               (inst
                                                                                                +
                                                                                                "union(E!2,E!3)")
                                                                                               (skosimp)
                                                                                               (inst
                                                                                                -
                                                                                                "x!1")
                                                                                               (inst
                                                                                                -
                                                                                                "x!1")
                                                                                               (expand
                                                                                                "union")
                                                                                               (expand
                                                                                                "member")
                                                                                               (flatten)
                                                                                               (assert)
                                                                                               (expand
                                                                                                "abs")
                                                                                               (expand
                                                                                                "abs")
                                                                                               (inst
                                                                                                -
                                                                                                "j!1"
                                                                                                "x!1")
                                                                                               (assert))
                                                                                              ("2"
                                                                                               (expand
                                                                                                "F")
                                                                                               (replace
                                                                                                -21)
                                                                                               (hide-all-but
                                                                                                (1
                                                                                                 -21
                                                                                                 -24))
                                                                                               (lemma
                                                                                                "x_section_measurable"
                                                                                                ("nu"
                                                                                                 "fm_contraction[T2, S2](nu, A_of(nu)(j!1))"
                                                                                                 "M"
                                                                                                 "EE"))
                                                                                               (("1"
                                                                                                 (propax))
                                                                                                ("2"
                                                                                                 (expand
                                                                                                  "measurable_set?")
                                                                                                 (propax))))))
                                                                                            ("2"
                                                                                             (hide-all-but
                                                                                              (-1
                                                                                               -2
                                                                                               -3
                                                                                               -22
                                                                                               1))
                                                                                             (expand
                                                                                              "ae_convergence?")
                                                                                             (expand
                                                                                              "ae_le?")
                                                                                             (expand
                                                                                              "pointwise_ae?")
                                                                                             (expand
                                                                                              "ae_convergence_in?")
                                                                                             (expand
                                                                                              "ae?")
                                                                                             (expand
                                                                                              "fullset")
                                                                                             (expand
                                                                                              "ae_in?")
                                                                                             (skosimp)
                                                                                             (inst
                                                                                              +
                                                                                              "E!2")
                                                                                             (skosimp)
                                                                                             (inst
                                                                                              -
                                                                                              "x!1")
                                                                                             (inst
                                                                                              -
                                                                                              "x!1")
                                                                                             (assert)
                                                                                             (rewrite
                                                                                              "metric_convergence_def")
                                                                                             (expand
                                                                                              "metric_converges_to")
                                                                                             (inst
                                                                                              -
                                                                                              "FF(j!1)(x!1)-g!1(x!1)")
                                                                                             (skosimp)
                                                                                             (inst
                                                                                              -
                                                                                              "n!1+j!1")
                                                                                             (expand
                                                                                              "pointwise_increasing?")
                                                                                             (inst
                                                                                              -
                                                                                              "x!1")
                                                                                             (expand
                                                                                              "increasing?")
                                                                                             (inst
                                                                                              -
                                                                                              "j!1"
                                                                                              "n!1+j!1")
                                                                                             (expand
                                                                                              "ball")
                                                                                             (assert))))
                                                                                          ("2"
                                                                                           (hide-all-but
                                                                                            (-21
                                                                                             1))
                                                                                           (skosimp)
                                                                                           (expand
                                                                                            "FF")
                                                                                           (expand
                                                                                            "series")
                                                                                           (inst
                                                                                            -
                                                                                            "_"
                                                                                            "x!1")
                                                                                           (expand
                                                                                            "sigma")
                                                                                           (assert))))))
                                                                                      ("2"
                                                                                       (hide-all-but
                                                                                        (-1
                                                                                         -3
                                                                                         -2
                                                                                         -4
                                                                                         -6
                                                                                         1))
                                                                                       (expand
                                                                                        "ae_convergence?")
                                                                                       (expand
                                                                                        "ae_convergence_in?")
                                                                                       (expand
                                                                                        "ae_nonneg?")
                                                                                       (expand
                                                                                        "pointwise_ae?")
                                                                                       (expand
                                                                                        "ae?")
                                                                                       (expand
                                                                                        "fullset")
                                                                                       (expand
                                                                                        "ae_in?")
                                                                                       (skosimp*)
                                                                                       (inst
                                                                                        +
                                                                                        "union(E!2,E!3)")
                                                                                       (skosimp)
                                                                                       (expand
                                                                                        "union")
                                                                                       (expand
                                                                                        "member")
                                                                                       (flatten)
                                                                                       (inst
                                                                                        -
                                                                                        "x!1")
                                                                                       (inst
                                                                                        -
                                                                                        "x!1")
                                                                                       (inst
                                                                                        -
                                                                                        "x!1")
                                                                                       (assert)
                                                                                       (expand
                                                                                        "plus")
                                                                                       (expand
                                                                                        "max")
                                                                                       (expand
                                                                                        "x_eq")
                                                                                       (flatten)
                                                                                       (assert)
                                                                                       (expand
                                                                                        "x_limit")
                                                                                       (case
                                                                                        "convergence(LAMBDA (n:nat): FF(n)(x!1), g!1(x!1))")
                                                                                       (("1"
                                                                                         (name-replace
                                                                                          "SS"
                                                                                          "LAMBDA (n: nat): FF(n)(x!1)")
                                                                                         (name-replace
                                                                                          "LIMIT"
                                                                                          "g!1(x!1)")
                                                                                         (hide-all-but
                                                                                          (-1
                                                                                           3))
                                                                                         (expand
                                                                                          "convergence")
                                                                                         (rewrite
                                                                                          "metric_convergence_def")
                                                                                         (expand
                                                                                          "metric_converges_to")
                                                                                         (skosimp)
                                                                                         (inst
                                                                                          -
                                                                                          "r!1")
                                                                                         (skosimp)
                                                                                         (inst
                                                                                          +
                                                                                          "n!1")
                                                                                         (skosimp)
                                                                                         (inst
                                                                                          -
                                                                                          "i!1")
                                                                                         (assert)
                                                                                         (ground)
                                                                                         (grind))
                                                                                        ("2"
                                                                                         (replace
                                                                                          -6
                                                                                          *
                                                                                          rl)
                                                                                         (lift-if)
                                                                                         (prop)
                                                                                         (lemma
                                                                                          "convergence_sequences.limit_def"
                                                                                          ("l"
                                                                                           "g!1(x!1)"
                                                                                           "v"
                                                                                           "LAMBDA i: FF(i)(x!1)"))
                                                                                         (("1"
                                                                                           (assert))
                                                                                          ("2"
                                                                                           (propax))))))))
                                                                                    ("2"
                                                                                     (hide-all-but
                                                                                      (1
                                                                                       -19))
                                                                                     (expand
                                                                                      "pointwise_increasing?")
                                                                                     (skosimp)
                                                                                     (expand
                                                                                      "increasing?")
                                                                                     (skolem
                                                                                      +
                                                                                      ("i!1"
                                                                                       "j!1"))
                                                                                     (flatten)
                                                                                     (expand
                                                                                      "FF")
                                                                                     (expand
                                                                                      "series")
                                                                                     (inst
                                                                                      -
                                                                                      "_"
                                                                                      "x!1")
                                                                                     (lemma
                                                                                      "sigma_split"
                                                                                      ("low"
                                                                                       "0"
                                                                                       "high"
                                                                                       "j!1"
                                                                                       "z"
                                                                                       "i!1"
                                                                                       "F"
                                                                                       "LAMBDA i: F(i)(x!1)"))
                                                                                     (assert)
                                                                                     (replace
                                                                                      -1)
                                                                                     (assert))))
                                                                                  ("2"
                                                                                   (hide-all-but
                                                                                    (1
                                                                                     -15
                                                                                     -18
                                                                                     -1))
                                                                                   (skosimp)
                                                                                   (inst
                                                                                    -
                                                                                    "x!1")
                                                                                   (lemma
                                                                                    "x_limit_to_sum"
                                                                                    ("S"
                                                                                     "LAMBDA j: (TRUE, FF(j)(x!1))"
                                                                                     "T"
                                                                                     "LAMBDA j: (TRUE, F(j)(x!1))"))
                                                                                   (("1"
                                                                                     (split
                                                                                      -1)
                                                                                     (("1"
                                                                                       (expand
                                                                                        "x_eq")
                                                                                       (flatten)
                                                                                       (expand
                                                                                        "x_sum")
                                                                                       (case-replace
                                                                                        "convergence_sequences.convergent?(series(LAMBDA j: F(j)(x!1)))")
                                                                                       (("1"
                                                                                         (assert))
                                                                                        ("2"
                                                                                         (assert))))
                                                                                      ("2"
                                                                                       (hide
                                                                                        -2
                                                                                        2)
                                                                                       (skosimp)
                                                                                       (expand
                                                                                        "FF")
                                                                                       (expand
                                                                                        "series")
                                                                                       (expand
                                                                                        "x_sigma")
                                                                                       (expand
                                                                                        "x_eq")
                                                                                       (propax))))
                                                                                    ("2"
                                                                                     (skosimp)
                                                                                     (inst
                                                                                      -
                                                                                      "j!1"
                                                                                      "x!1"))))
                                                                                  ("3"
                                                                                   (skosimp)
                                                                                   (inst
                                                                                    -
                                                                                    "j!1"
                                                                                    "x!1"))))
                                                                                ("2"
                                                                                 (hide-all-but
                                                                                  (1
                                                                                   -17))
                                                                                 (expand
                                                                                  "FF")
                                                                                 (expand
                                                                                  "series")
                                                                                 (induct
                                                                                  "j")
                                                                                 (("1"
                                                                                   (skosimp)
                                                                                   (inst
                                                                                    -
                                                                                    "0"
                                                                                    "x!1")
                                                                                   (expand
                                                                                    "sigma")
                                                                                   (assert))
                                                                                  ("2"
                                                                                   (skosimp)
                                                                                   (skosimp)
                                                                                   (inst
                                                                                    -
                                                                                    "x!1")
                                                                                   (inst
                                                                                    -
                                                                                    "j!1+1"
                                                                                    "x!1")
                                                                                   (expand
                                                                                    "sigma"
                                                                                    1)
                                                                                   (assert))))))
                                                                              ("2"
                                                                               (hide-all-but
                                                                                (-1
                                                                                 -2
                                                                                 -4
                                                                                 1))
                                                                               (expand
                                                                                "ae_nonneg?")
                                                                               (expand
                                                                                "ae_convergence?")
                                                                               (expand
                                                                                "ae_convergence_in?")
                                                                               (expand
                                                                                "pointwise_ae?")
                                                                               (expand
                                                                                "ae?")
                                                                               (expand
                                                                                "fullset")
                                                                               (expand
                                                                                "ae_in?")
                                                                               (skosimp*)
                                                                               (inst
                                                                                +
                                                                                "union(E!2,E!3)")
                                                                               (skosimp)
                                                                               (expand
                                                                                "union")
                                                                               (expand
                                                                                "member")
                                                                               (flatten)
                                                                               (inst
                                                                                -
                                                                                "x!1")
                                                                               (inst
                                                                                -
                                                                                "x!1")
                                                                               (inst
                                                                                -
                                                                                "x!1")
                                                                               (assert)
                                                                               (expand
                                                                                "plus")
                                                                               (expand
                                                                                "max")
                                                                               (expand
                                                                                "x_limit")
                                                                               (case
                                                                                "convergence(LAMBDA (n:nat): GG(n)(x!1), g!1(x!1))")
                                                                               (("1"
                                                                                 (hide
                                                                                  -4)
                                                                                 (case-replace
                                                                                  "convergence_sequences.convergent?(LAMBDA i: GG(i)(x!1))")
                                                                                 (("1"
                                                                                   (lemma
                                                                                    "convergence_sequences.limit_def"
                                                                                    ("v"
                                                                                     "LAMBDA i: GG(i)(x!1)"
                                                                                     "l"
                                                                                     "g!1(x!1)"))
                                                                                   (("1"
                                                                                     (assert))
                                                                                    ("2"
                                                                                     (propax))))
                                                                                  ("2"
                                                                                   (expand
                                                                                    "convergence_sequences.convergent?")
                                                                                   (inst
                                                                                    +
                                                                                    "g!1(x!1)"))))
                                                                                ("2"
                                                                                 (hide-all-but
                                                                                  (-3
                                                                                   1))
                                                                                 (expand
                                                                                  "convergence")
                                                                                 (rewrite
                                                                                  "metric_convergence_def")
                                                                                 (expand
                                                                                  "metric_converges_to")
                                                                                 (skosimp)
                                                                                 (inst
                                                                                  -
                                                                                  "epsilon!1")
                                                                                 (skosimp)
                                                                                 (inst
                                                                                  +
                                                                                  "n!1")
                                                                                 (skosimp)
                                                                                 (inst
                                                                                  -
                                                                                  "i!1")
                                                                                 (grind))))))
                                                                            ("2"
                                                                             (hide
                                                                              2)
                                                                             (skosimp)
                                                                             (inst
                                                                              -11
                                                                              "x!1")
                                                                             (case-replace
                                                                              "X!1(x!1)")
                                                                             (("1"
                                                                               (lemma
                                                                                "x_limit_to_sum"
                                                                                ("S"
                                                                                 "LAMBDA j: (TRUE, GG(j)(x!1))"
                                                                                 "T"
                                                                                 "LAMBDA j: (TRUE,G(j)(x!1))"))
                                                                               (("1"
                                                                                 (split
                                                                                  -1)
                                                                                 (("1"
                                                                                   (inst
                                                                                    -14
                                                                                    "x!1")
                                                                                   (hide-all-but
                                                                                    (-1
                                                                                     -13
                                                                                     -14
                                                                                     1))
                                                                                   (expand
                                                                                    "x_eq")
                                                                                   (expand
                                                                                    "x_sum")
                                                                                   (flatten)
                                                                                   (case-replace
                                                                                    "convergence_sequences.convergent?(series(LAMBDA j: G(j)(x!1)))")
                                                                                   (("1"
                                                                                     (assert))
                                                                                    ("2"
                                                                                     (assert))))
                                                                                  ("2"
                                                                                   (hide-all-but
                                                                                    (1
                                                                                     -1))
                                                                                   (expand
                                                                                    "GG")
                                                                                   (expand
                                                                                    "series")
                                                                                   (expand
                                                                                    "*")
                                                                                   (expand
                                                                                    "phi")
                                                                                   (expand
                                                                                    "member")
                                                                                   (replace
                                                                                    -1)
                                                                                   (expand
                                                                                    "x_sigma")
                                                                                   (skosimp)
                                                                                   (expand
                                                                                    "x_eq")
                                                                                   (assert))))
                                                                                ("2"
                                                                                 (skosimp)
                                                                                 (inst
                                                                                  -7
                                                                                  "j!1"
                                                                                  "x!1"))))
                                                                              ("2"
                                                                               (case-replace
                                                                                "(LAMBDA j: (TRUE, GG(j)(x!1)))=(lambda j: (TRUE,0))")
                                                                               (("1"
                                                                                 (hide-all-but
                                                                                  (1
                                                                                   2))
                                                                                 (expand
                                                                                  "x_limit")
                                                                                 (lemma
                                                                                  "convergent_const"
                                                                                  ("a"
                                                                                   "0"))
                                                                                 (expand
                                                                                  "const_fun")
                                                                                 (replace
                                                                                  -1)
                                                                                 (lemma
                                                                                  "limit_const"
                                                                                  ("a"
                                                                                   "0"))
                                                                                 (expand
                                                                                  "const_fun")
                                                                                 (replace
                                                                                  -1)
                                                                                 (case-replace
                                                                                  "x_section(EE, x!1)=emptyset")
                                                                                 (("1"
                                                                                   (typepred
                                                                                    "nu")
                                                                                   (expand
                                                                                    "sigma_finite_measure?")
                                                                                   (expand
                                                                                    "measure?")
                                                                                   (flatten)
                                                                                   (expand
                                                                                    "measure_empty?")
                                                                                   (replace
                                                                                    -1)
                                                                                   (expand
                                                                                    "x_eq")
                                                                                   (propax))
                                                                                  ("2"
                                                                                   (apply-extensionality
                                                                                    :hide?
                                                                                    t)
                                                                                   (expand
                                                                                    "emptyset")
                                                                                   (expand
                                                                                    "x_section")
                                                                                   (expand
                                                                                    "EE")
                                                                                   (expand
                                                                                    "cross_product")
                                                                                   (expand
                                                                                    "intersection")
                                                                                   (expand
                                                                                    "member")
                                                                                   (propax))))
                                                                                ("2"
                                                                                 (hide-all-but
                                                                                  (1
                                                                                   2))
                                                                                 (apply-extensionality
                                                                                  :hide?
                                                                                  t)
                                                                                 (expand
                                                                                  "GG")
                                                                                 (expand
                                                                                  "*")
                                                                                 (expand
                                                                                  "phi")
                                                                                 (expand
                                                                                  "member")
                                                                                 (expand
                                                                                  "series")
                                                                                 (rewrite
                                                                                  "sigma_zero"))))))
                                                                            ("3"
                                                                             (skosimp)
                                                                             (inst
                                                                              -6
                                                                              "j!1"
                                                                              "x!1"))))
                                                                          ("2"
                                                                           (hide-all-but
                                                                            (-3
                                                                             1
                                                                             -5
                                                                             -6))
                                                                           (expand
                                                                            "ae_convergence?")
                                                                           (expand
                                                                            "ae_nonneg?")
                                                                           (expand
                                                                            "pointwise_ae?")
                                                                           (expand
                                                                            "ae_convergence_in?")
                                                                           (expand
                                                                            "ae?")
                                                                           (expand
                                                                            "fullset")
                                                                           (expand
                                                                            "ae_in?")
                                                                           (skosimp)
                                                                           (inst
                                                                            +
                                                                            "E!2")
                                                                           (skosimp)
                                                                           (inst
                                                                            -
                                                                            "x!1")
                                                                           (expand
                                                                            "pointwise_increasing?")
                                                                           (inst
                                                                            -
                                                                            "x!1")
                                                                           (assert)
                                                                           (inst
                                                                            -
                                                                            "_"
                                                                            "x!1")
                                                                           (rewrite
                                                                            "metric_convergence_def")
                                                                           (expand
                                                                            "metric_converges_to")
                                                                           (inst
                                                                            -
                                                                            "GG(0)(x!1)-g!1(x!1)")
                                                                           (("1"
                                                                             (skosimp)
                                                                             (inst
                                                                              -
                                                                              "n!1")
                                                                             (assert)
                                                                             (expand
                                                                              "ball")
                                                                             (expand
                                                                              "increasing?")
                                                                             (inst
                                                                              -
                                                                              "0"
                                                                              "n!1")
                                                                             (inst
                                                                              -
                                                                              "0")
                                                                             (grind))
                                                                            ("2"
                                                                             (inst
                                                                              -
                                                                              "0")
                                                                             (assert))))))
                                                                        ("2"
                                                                         (name-replace
                                                                          "SS"
                                                                          "integral[T1, S1, mu] o GG")
                                                                         (name-replace
                                                                          "LIMIT"
                                                                          "integral(g!1)")
                                                                         (expand
                                                                          "converges_upto?")
                                                                         (flatten)
                                                                         (hide-all-but
                                                                          (-4
                                                                           -10
                                                                           1))
                                                                         (lemma
                                                                          "convergence_sequences.unique_limit"
                                                                          ("u"
                                                                           "SS"
                                                                           "l1"
                                                                           "l!1"
                                                                           "l2"
                                                                           "LIMIT"))
                                                                         (assert)
                                                                         (hide-all-but
                                                                          (1
                                                                           -1))
                                                                         (rewrite
                                                                          "metric_convergence_def")
                                                                         (expand
                                                                          "metric_converges_to")
                                                                         (expand
                                                                          "convergence")
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "epsilon!1")
                                                                         (skosimp)
                                                                         (inst
                                                                          +
                                                                          "n!1")
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "i!1")
                                                                         (assert)
                                                                         (ground)
                                                                         (grind))))
                                                                      ("2"
                                                                       (hide-all-but
                                                                        (-7
                                                                         -3
                                                                         1
                                                                         -4
                                                                         -5))
                                                                       (case
                                                                        "increasing(integral[T1, S1, mu] o GG)")
                                                                       (("1"
                                                                         (expand
                                                                          "bounded?")
                                                                         (split)
                                                                         (("1"
                                                                           (name-replace
                                                                            "SS"
                                                                            "integral[T1, S1, mu] o GG")
                                                                           (hide
                                                                            -3
                                                                            -4
                                                                            -2)
                                                                           (expand
                                                                            "bounded_above?")
                                                                           (inst
                                                                            +
                                                                            "l!1")
                                                                           (skolem
                                                                            +
                                                                            "n!1")
                                                                           (expand
                                                                            "increasing?")
                                                                           (expand
                                                                            "convergence")
                                                                           (inst
                                                                            -
                                                                            "SS(n!1)-l!1")
                                                                           (("1"
                                                                             (skosimp)
                                                                             (inst
                                                                              -
                                                                              "n!1+n!2")
                                                                             (inst
                                                                              -
                                                                              "n!1"
                                                                              "n!1+n!2")
                                                                             (assert)
                                                                             (grind))
                                                                            ("2"
                                                                             (assert))))
                                                                          ("2"
                                                                           (expand
                                                                            "bounded_below?")
                                                                           (inst
                                                                            +
                                                                            "0")
                                                                           (skolem
                                                                            +
                                                                            "n!1")
                                                                           (expand
                                                                            "o")
                                                                           (inst
                                                                            -
                                                                            "n!1"
                                                                            "_")
                                                                           (lemma
                                                                            "integral_nonneg[T1, S1, mu]"
                                                                            ("f"
                                                                             "GG(n!1)"))
                                                                           (assert))))
                                                                        ("2"
                                                                         (hide
                                                                          2
                                                                          -4)
                                                                         (expand
                                                                          "pointwise_increasing?")
                                                                         (expand
                                                                          "increasing?")
                                                                         (skolem
                                                                          +
                                                                          ("i!1"
                                                                           "j!1"))
                                                                         (flatten)
                                                                         (expand
                                                                          "o")
                                                                         (inst-cp
                                                                          -4
                                                                          "j!1")
                                                                         (inst
                                                                          -4
                                                                          "i!1")
                                                                         (lemma
                                                                          "integral_ae_le[T1, S1, mu]"
                                                                          ("f1"
                                                                           "GG(i!1)"
                                                                           "f2"
                                                                           "GG(j!1)"))
                                                                         (assert)
                                                                         (hide-all-but
                                                                          (-2
                                                                           1))
                                                                         (expand
                                                                          "ae_le?")
                                                                         (expand
                                                                          "pointwise_ae?")
                                                                         (expand
                                                                          "ae?")
                                                                         (expand
                                                                          "fullset")
                                                                         (expand
                                                                          "ae_in?")
                                                                         (inst
                                                                          +
                                                                          "emptyset")
                                                                         (skosimp)
                                                                         (inst
                                                                          -
                                                                          "x!1")
                                                                         (inst
                                                                          -
                                                                          "i!1"
                                                                          "j!1")
                                                                         (assert))))))
                                                                    ("2"
                                                                     (hide-all-but
                                                                      (-1
                                                                       1))
                                                                     (expand
                                                                      "pointwise_increasing?")
                                                                     (expand
                                                                      "ae_increasing?")
                                                                     (inst
                                                                      +
                                                                      "emptyset")
                                                                     (skosimp)
                                                                     (inst
                                                                      -
                                                                      "x!1")
                                                                     (expand
                                                                      "increasing?")
                                                                     (propax))))
                                                                  ("2"
                                                                   (hide
                                                                    2)
                                                                   (induct
                                                                    "n")
                                                                   (("1"
                                                                     (expand
                                                                      "o"
                                                                      1)
                                                                     (expand
                                                                      "GG")
                                                                     (expand
                                                                      "series")
                                                                     (expand
                                                                      "sigma")
                                                                     (assert)
                                                                     (inst
                                                                      -4
                                                                      "0")
                                                                     (lemma
                                                                      "contraction_integral[T1,S1]"
                                                                      ("mu"
                                                                       "mu"
                                                                       "A"
                                                                       "X!1"
                                                                       "f"
                                                                       "G(0)"))
                                                                     (assert)
                                                                     (expand
                                                                      "*")
                                                                     (propax))
                                                                    ("2"
                                                                     (expand
                                                                      "o"
                                                                      1)
                                                                     (expand
                                                                      "GG"
                                                                      1)
                                                                     (expand
                                                                      "series"
                                                                      1)
                                                                     (skosimp)
                                                                     (expand
                                                                      "sigma"
                                                                      1)
                                                                     (replace
                                                                      -1)
                                                                     (hide
                                                                      -1)
                                                                     (inst
                                                                      -4
                                                                      "1+j!1")
                                                                     (inst
                                                                      -3
                                                                      "j!1")
                                                                     (expand
                                                                      "GG"
                                                                      -3)
                                                                     (expand
                                                                      "series"
                                                                      -3)
                                                                     (lemma
                                                                      "contraction_integral[T1,S1]"
                                                                      ("mu"
                                                                       "mu"
                                                                       "A"
                                                                       "X!1"
                                                                       "f"
                                                                       "G(1+j!1)"))
                                                                     (replace
                                                                      -1)
                                                                     (hide
                                                                      -1
                                                                      -2
                                                                      -3
                                                                      -6
                                                                      -7)
                                                                     (lemma
                                                                      "integral_add[T1,S1,mu]"
                                                                      ("f1"
                                                                       "*[T1](phi(X!1), G(1 + j!1))"
                                                                       "f2"
                                                                       "LAMBDA x: sigma(0, j!1, LAMBDA i: *[T1](phi(X!1), G(i))(x))"))
                                                                     (("1"
                                                                       (expand
                                                                        "+"
                                                                        -1)
                                                                       (assert))
                                                                      ("2"
                                                                       (propax))))))
                                                                  ("3"
                                                                   (propax))
                                                                  ("4"
                                                                   (propax))))
                                                                ("2"
                                                                 (expand
                                                                  "pointwise_increasing?")
                                                                 (skosimp)
                                                                 (expand
                                                                  "increasing?")
                                                                 (skolem
                                                                  +
                                                                  ("i!1"
                                                                   "j!1"))
                                                                 (flatten)
                                                                 (hide-all-but
                                                                  (-1
                                                                   -13
                                                                   1))
                                                                 (expand
                                                                  "GG")
                                                                 (expand
                                                                  "series")
                                                                 (expand
                                                                  "*")
                                                                 (expand
                                                                  "phi")
                                                                 (expand
                                                                  "member")
                                                                 (case-replace
                                                                  "X!1(x!1)")
                                                                 (("1"
                                                                   (inst
                                                                    -
                                                                    "_"
                                                                    "x!1")
                                                                   (lemma
                                                                    "sigma_split"
                                                                    ("low"
                                                                     "0"
                                                                     "high"
                                                                     "j!1"
                                                                     "z"
                                                                     "i!1"
                                                                     "F"
                                                                     "LAMBDA i: 1 * G(i)(x!1)"))
                                                                   (assert)
                                                                   (replace
                                                                    -1)
                                                                   (assert))
                                                                  ("2"
                                                                   (assert)
                                                                   (rewrite
                                                                    "sigma_zero")
                                                                   (rewrite
                                                                    "sigma_zero")
                                                                   (assert))))))
                                                              ("2"
                                                               (hide-all-but
                                                                (1 -11))
                                                               (expand
                                                                "GG")
                                                               (expand
                                                                "series")
                                                               (expand
                                                                "*")
                                                               (skolem
                                                                +
                                                                ("_"
                                                                 "x!1"))
                                                               (inst
                                                                -
                                                                "_"
                                                                "x!1")
                                                               (induct
                                                                "j")
                                                               (("1"
                                                                 (expand
                                                                  "sigma")
                                                                 (inst
                                                                  -
                                                                  "0")
                                                                 (expand
                                                                  "phi")
                                                                 (expand
                                                                  "member")
                                                                 (assert)
                                                                 (lift-if)
                                                                 (assert))
                                                                ("2"
                                                                 (skosimp)
                                                                 (expand
                                                                  "sigma"
                                                                  1)
                                                                 (expand
                                                                  "phi"
                                                                  1
                                                                  2)
                                                                 (lift-if
                                                                  1)
                                                                 (assert)
                                                                 (inst
                                                                  -
                                                                  "1+j!1")
                                                                 (assert))))))
                                                            ("2"
                                                             (hide-all-but
                                                              (-2 1 -5))
                                                             (expand
                                                              "GG")
                                                             (expand
                                                              "series")
                                                             (induct "j")
                                                             (("1"
                                                               (expand
                                                                "sigma")
                                                               (assert)
                                                               (inst
                                                                -
                                                                "0")
                                                               (lemma
                                                                "contraction_integrable[T1,S1]"
                                                                ("mu"
                                                                 "mu"
                                                                 "A"
                                                                 "X!1"
                                                                 "f"
                                                                 "G(0)"))
                                                               (("1"
                                                                 (assert)
                                                                 (expand
                                                                  "*")
                                                                 (propax))
                                                                ("2"
                                                                 (lemma
                                                                  "integrable_is_measurable[T1, S1, contraction(mu, X!1)]")
                                                                 (inst
                                                                  -
                                                                  "G(0)"))))
                                                              ("2"
                                                               (skosimp)
                                                               (expand
                                                                "sigma"
                                                                1)
                                                               (inst
                                                                -
                                                                "1+j!1")
                                                               (lemma
                                                                "integrable_is_measurable[T1, S1, contraction(mu, X!1)]")
                                                               (inst
                                                                -
                                                                "G(1 + j!1)")
                                                               (lemma
                                                                "contraction_integrable[T1,S1]"
                                                                ("mu"
                                                                 "mu"
                                                                 "A"
                                                                 "X!1"
                                                                 "f"
                                                                 "G(1+j!1)"))
                                                               (("1"
                                                                 (assert)
                                                                 (lemma
                                                                  "integrable_add[T1, S1, mu]"
                                                                  ("f1"
                                                                   "*[T1](phi(X!1), G(1 + j!1))"
                                                                   "f2"
                                                                   "LAMBDA x:sigma(0, j!1, LAMBDA i: *[T1](phi(X!1), G(i))(x))"))
                                                                 (expand
                                                                  "+")
                                                                 (propax))
                                                                ("2"
                                                                 (propax))))))))))
                                                        ("3"
                                                         (expand
                                                          "measurable_set?")
                                                         (propax))
                                                        ("4" (skosimp))
                                                        ("5" (skosimp))))
                                                      ("3" (propax))))
                                                    ("2"
                                                     (hide 2)
                                                     (skosimp)
                                                     (lemma
                                                      "integral_nonneg[T1, S1, contraction[T1, S1](mu, X!1)]"
                                                      ("f" "G(j!1)"))
                                                     (inst -8 "j!1" "_")
                                                     (replace -8)
                                                     (propax))
                                                    ("3" (assert))
                                                    ("4" (propax))))
                                                  ("2"
                                                   (assert)
                                                   (expand
                                                    "measurable_set?")
                                                   (propax))))))
                                              ("2"
                                               (hide 2)
                                               (assert)
                                               (skolem + "j!1")
                                               (inst - "j!1")
                                               (expand "x_sum" 1)
                                               (case-replace
                                                "integrable?[T1, S1, mu](F(j!1))")
                                               (("1"
                                                 (assert)
                                                 (lemma
                                                  "sfm_integral[T1,S1,mu]"
                                                  ("f" "F(j!1)"))
                                                 (("1"
                                                   (case-replace
                                                    "(LAMBDA i:
                                                                                                                                  integral[T1, S1, contraction(mu, A_of(mu)(i))]
                                                                                                                                      (F(j!1)))=(LAMBDA (i_1: nat):
                                                                                                                                        integral[T1, S1, to_measure(MU(i_1))]
                                                                                                                                            (F(j!1)))")
                                                   (("1"
                                                     (hide -1)
                                                     (name-replace
                                                      "DRL1"
                                                      "(series(LAMBDA (i_1: nat):
                                                                                                                                            integral[T1, S1, to_measure(MU(i_1))]
                                                                                                                                                (F(j!1))))")
                                                     (("1"
                                                       (rewrite
                                                        "metric_convergence_def"
                                                        -1)
                                                       (expand
                                                        "metric_converges_to")
                                                       (expand "ball")
                                                       (expand "member")
                                                       (name-replace
                                                        "RHS"
                                                        "integral[T1, S1, mu](F(j!1))")
                                                       (expand "x_eq" 1)
                                                       (lift-if 1)
                                                       (assert)
                                                       (lemma
                                                        "convergence_sequences.limit_def"
                                                        ("v"
                                                         "DRL1"
                                                         "l"
                                                         "RHS"))
                                                       (("1"
                                                         (replace -1)
                                                         (hide-all-but
                                                          (-2 1))
                                                         (expand
                                                          "convergence")
                                                         (prop)
                                                         (("1"
                                                           (hide -1)
                                                           (skosimp)
                                                           (inst
                                                            -
                                                            "epsilon!1")
                                                           (skosimp)
                                                           (inst + "n!1")
                                                           (skosimp)
                                                           (inst - "i!1")
                                                           (grind))
                                                          ("2"
                                                           (expand
                                                            "convergent?")
                                                           (inst + "RHS")
                                                           (expand
                                                            "convergence")
                                                           (skosimp)
                                                           (inst
                                                            -
                                                            "epsilon!1")
                                                           (skosimp)
                                                           (inst + "n!1")
                                                           (skosimp)
                                                           (inst - "i!1")
                                                           (grind))))
                                                        ("2"
                                                         (hide-all-but
                                                          (-1 1))
                                                         (expand
                                                          "convergent?")
                                                         (inst + "RHS")
                                                         (expand
                                                          "convergence")
                                                         (skosimp)
                                                         (inst
                                                          -
                                                          "epsilon!1")
                                                         (skosimp)
                                                         (inst + "n!1")
                                                         (skosimp)
                                                         (inst - "i!1")
                                                         (grind))))
                                                      ("2"
                                                       (skosimp)
                                                       (inst
                                                        -14
                                                        "i!1"
                                                        "j!1"))))
                                                    ("2"
                                                     (apply-extensionality
                                                      :hide?
                                                      t)
                                                     (("1"
                                                       (inst
                                                        -4
                                                        "_"
                                                        "x!1")
                                                       (lemma
                                                        "measure_eq_integral[T1,S1]"
                                                        ("mu"
                                                         "contraction(mu, A_of(mu)(x!1))"
                                                         "nu"
                                                         "to_measure(MU(x!1))"
                                                         "f"
                                                         "F(j!1)"))
                                                       (("1"
                                                         (replace -5)
                                                         (assert)
                                                         (flatten)
                                                         (inst
                                                          -14
                                                          "x!1"
                                                          "j!1"))
                                                        ("2"
                                                         (expand
                                                          "measurable_set?")
                                                         (propax))))
                                                      ("2"
                                                       (skosimp)
                                                       (inst
                                                        -14
                                                        "i!1"
                                                        "j!1"))
                                                      ("3"
                                                       (skosimp)
                                                       (expand
                                                        "measurable_set?")
                                                       (propax))
                                                      ("4"
                                                       (skosimp)
                                                       (expand
                                                        "measurable_set?")
                                                       (hide-all-but
                                                        (1 -14 -4))
                                                       (inst
                                                        -2
                                                        "i!1"
                                                        "j!1")
                                                       (inst - "_" "i!1")
                                                       (lemma
                                                        "measure_eq_integrable?[T1,S1]"
                                                        ("mu"
                                                         "contraction(mu, A_of(mu)(i!1))"
                                                         "nu"
                                                         "to_measure(MU(i!1))"
                                                         "f"
                                                         "F(j!1)"))
                                                       (("1"
                                                         (replace -2)
                                                         (replace -1)
                                                         (propax))
                                                        ("2"
                                                         (expand
                                                          "measurable_set?")
                                                         (propax))))))
                                                    ("3"
                                                     (skosimp)
                                                     (inst
                                                      -14
                                                      "i!1"
                                                      "j!1"))
                                                    ("4"
                                                     (expand
                                                      "measurable_set?")
                                                     (propax))
                                                    ("5"
                                                     (skosimp)
                                                     (inst
                                                      -14
                                                      "i!1"
                                                      "j!1")
                                                     (lemma
                                                      "measure_eq_integrable?[T1,S1]"
                                                      ("mu"
                                                       "contraction(mu, A_of(mu)(i!1))"
                                                       "nu"
                                                       "to_measure(MU(i!1))"
                                                       "f"
                                                       "F(j!1)"))
                                                     (("1"
                                                       (inst
                                                        -5
                                                        "_"
                                                        "i!1")
                                                       (assert))
                                                      ("2"
                                                       (expand
                                                        "measurable_set?")
                                                       (propax))))))
                                                  ("2"
                                                   (lemma
                                                    "nn_integrable_is_nn_integrable[T1, S1, mu]"
                                                    ("f" "F(j!1)"))
                                                   (inst -16 "j!1" "_")
                                                   (replace -16)
                                                   (propax))))
                                                ("2"
                                                 (replace 1)
                                                 (expand "x_eq" 2)
                                                 (lift-if 2)
                                                 (assert)
                                                 (prop)
                                                 (hide 1)
                                                 (expand "convergent?")
                                                 (skosimp)
                                                 (inst + "l!1")
                                                 (name-replace
                                                  "UU"
                                                  "series(LAMBDA (i_1: nat):
                                                                                                                             integral[T1, S1, to_measure(MU(i_1))](F(j!1)))")
                                                 (("1"
                                                   (hide-all-but (-1 1))
                                                   (expand "convergence")
                                                   (rewrite
                                                    "metric_convergence_def")
                                                   (expand
                                                    "metric_converges_to")
                                                   (skosimp)
                                                   (inst - "r!1")
                                                   (skosimp)
                                                   (inst + " n!1")
                                                   (skosimp)
                                                   (inst - "i!1")
                                                   (grind))
                                                  ("2"
                                                   (skosimp)
                                                   (inst
                                                    -12
                                                    "i!1"
                                                    "j!1"))))))))
                                            ("2"
                                             (skosimp)
                                             (lemma
                                              "integral_nonneg[T1, S1, mu]"
                                              ("f" "F(j!1)"))
                                             (inst -16 "j!1" "_")
                                             (assert))))
                                          ("2"
                                           (hide-all-but
                                            (-1 1 -14 -13 -11))
                                           (skosimp)
                                           (lemma
                                            "sfm_integrable[T1,S1,mu]"
                                            ("h" "F(j!1)"))
                                           (("1"
                                             (case
                                              "forall i: integrable?[T1, S1, contraction(mu, A_of(mu)(i))](F(j!1)) <=> integrable?[T1, S1, to_measure(MU(i))](F(j!1))")
                                             (("1"
                                               (case-replace
                                                "(LAMBDA i:
                                                                                                                           integral[T1, S1, contraction(mu, A_of(mu)(i))]
                                                                                                                               (F(j!1)))=(LAMBDA i:
                                                                                                                          integral[T1, S1, to_measure(MU(i))](F(j!1)))")
                                               (("1"
                                                 (case-replace
                                                  "(FORALL i:
                                                                                                            integrable?[T1, S1, contraction(mu, A_of(mu)(i))](F(j!1)))")
                                                 (("1"
                                                   (assert)
                                                   (replace -4 1 rl)
                                                   (name-replace
                                                    "UU"
                                                    "(series((LAMBDA i: integral[T1, S1, to_measure(MU(i))](F(j!1)))))")
                                                   (("1"
                                                     (hide-all-but 1)
                                                     (expand
                                                      "convergent?")
                                                     (propax))
                                                    ("2"
                                                     (inst
                                                      -6
                                                      "_"
                                                      "j!1"))))
                                                  ("2"
                                                   (skosimp)
                                                   (inst -2 "i!1")
                                                   (inst -6 "i!1" "j!1")
                                                   (assert))))
                                                ("2"
                                                 (apply-extensionality
                                                  :hide?
                                                  t)
                                                 (("1"
                                                   (inst -3 "_" "x!1")
                                                   (inst - "x!1")
                                                   (inst -4 "x!1" "j!1")
                                                   (lemma
                                                    "measure_eq_integral[T1,S1]"
                                                    ("mu"
                                                     "contraction(mu, A_of(mu)(x!1))"
                                                     "nu"
                                                     "to_measure(MU(x!1))"
                                                     "f"
                                                     "F(j!1)"))
                                                   (("1"
                                                     (replace -4)
                                                     (replace -5)
                                                     (propax))
                                                    ("2"
                                                     (expand
                                                      "measurable_set?")
                                                     (propax))))
                                                  ("2"
                                                   (skosimp)
                                                   (inst -5 "i!1" "j!1"))
                                                  ("3"
                                                   (expand
                                                    "measurable_set?")
                                                   (propax))
                                                  ("4"
                                                   (flatten)
                                                   (skosimp)
                                                   (inst - "i!1")
                                                   (inst -5 "i!1" "j!1")
                                                   (assert))))
                                                ("3"
                                                 (skosimp)
                                                 (inst -5 "i!1" "j!1"))
                                                ("4"
                                                 (skosimp)
                                                 (inst -5 "i!1" "j!1")
                                                 (inst - "i!1")
                                                 (assert))))
                                              ("2"
                                               (skosimp)
                                               (hide-all-but
                                                (1 -4 -5 -3))
                                               (lemma
                                                "measure_eq_integrable?[T1,S1]"
                                                ("mu"
                                                 "contraction(mu, A_of(mu)(i!1))"
                                                 "nu"
                                                 "to_measure(MU(i!1))"
                                                 "f"
                                                 "F(j!1)"))
                                               (("1"
                                                 (assert)
                                                 (inst - "_" "i!1")
                                                 (assert)
                                                 (replace -2 -1)
                                                 (propax))
                                                ("2"
                                                 (expand
                                                  "measurable_set?")
                                                 (propax))))
                                              ("3"
                                               (expand "measurable_set?")
                                               (propax))))
                                            ("2"
                                             (hide-all-but (-3 -4 1))
                                             (expand "nn_measurable?")
                                             (expand "EE")
                                             (split)
                                             (("1"
                                               (expand "F")
                                               (lemma
                                                "x_section_measurable"
                                                ("nu"
                                                 "fm_contraction[T2, S2](nu, A_of(nu)(j!1))"
                                                 "M"
                                                 "intersection(cross_product(X!1, Y!1), E!1)"))
                                               (("1" (propax))
                                                ("2"
                                                 (expand
                                                  "measurable_set?")
                                                 (propax))))
                                              ("2"
                                               (skosimp)
                                               (inst - "j!1" "x!1")
                                               (assert))))))))
                                        ("2"
                                         (hide-all-but 1)
                                         (skosimp)
                                         (expand "to_measure")
                                         (expand "MU")
                                         (expand "fm_contraction")
                                         (expand "contraction")
                                         (expand "x_eq")
                                         (lemma
                                          "A_of_def2"
                                          ("mu" "mu" "n" "i!1"))
                                         (lemma
                                          "m_monotone[T1,S1,mu]"
                                          ("b"
                                           "A_of(mu)(i!1)"
                                           "a"
                                           "intersection(A_of(mu)(i!1), E!2)"))
                                         (("1"
                                           (expand "x_le")
                                           (assert)
                                           (expand "intersection")
                                           (expand "subset?")
                                           (expand "member")
                                           (skosimp))
                                          ("2"
                                           (expand "measurable_set?")
                                           (propax))
                                          ("3"
                                           (expand "measurable_set?")
                                           (propax))))
                                        ("3"
                                         (expand "measurable_set?")
                                         (propax))))
                                      ("3"
                                       (skosimp)
                                       (inst -4 "i!1" "j!1")
                                       (inst -5 "j!1" "_")
                                       (lemma
                                        "integral_nonneg[T1, S1, to_measure[T1, S1](NU(i!1))]"
                                        ("f" "G(j!1)"))
                                       (assert))
                                      ("4"
                                       (skosimp)
                                       (inst -4 "i!1" "j!1"))
                                      ("5"
                                       (skosimp)
                                       (inst -10 "i!1" "j!1")
                                       (lemma
                                        "integral_nonneg[T1, S1, to_measure[T1, S1](MU(i!1))]"
                                        ("f" "F(j!1)"))
                                       (assert)
                                       (skosimp)
                                       (inst -12 "j!1" "x!1"))
                                      ("6"
                                       (skosimp)
                                       (inst -10 "i!1" "j!1"))))
                                    ("3"
                                     (skosimp)
                                     (inst -5 "j!1" "_")
                                     (inst -4 "i!1" "j!1")
                                     (lemma
                                      "integral_nonneg[T1, S1, to_measure[T1, S1](NU(i!1))]"
                                      ("f" "G(j!1)"))
                                     (assert))
                                    ("4" (propax))
                                    ("5"
                                     (skosimp)
                                     (inst -10 "i!1" "j!1")
                                     (inst -12 "j!1" "_")
                                     (lemma
                                      "integral_nonneg[T1, S1, to_measure[T1, S1](MU(i!1))]"
                                      ("f" "F(j!1)"))
                                     (assert))
                                    ("6" (propax))))
                                  ("2"
                                   (hide-all-but 1)
                                   (skosimp)
                                   (expand "contraction")
                                   (expand "EE")
                                   (expand "cross_product")
                                   (expand "intersection")
                                   (expand "x_section")
                                   (expand "member")
                                   (assert)
                                   (expand "x_eq")
                                   (propax))
                                  ("3"
                                   (skosimp)
                                   (inst -9 "x!1")
                                   (expand "measurable_set?")
                                   (propax))
                                  ("4"
                                   (skosimp)
                                   (inst -6 "x!1")
                                   (expand "measurable_set?")
                                   (propax))))
                                ("2"
                                 (hide-all-but (-4 1))
                                 (skosimp)
                                 (inst - "x!1")
                                 (expand "G")
                                 (expand "o ")
                                 (expand "x_section" 1 1)
                                 (name-replace
                                  "MM"
                                  "x_section(E!1, x!1)")
                                 (lemma
                                  "sigma_finite_contraction_def"
                                  ("nu" "contraction(nu, Y!1)" "E" "MM"))
                                 (("1"
                                   (expand "x_sum")
                                   (expand "x_eq")
                                   (lift-if)
                                   (assert)
                                   (prop)
                                   (assert))
                                  ("2" (propax))))
                                ("3"
                                 (skosimp)
                                 (inst -4 "x!1")
                                 (expand "measurable_set?")
                                 (propax))))
                              ("2"
                               (expand "NU")
                               (hide-all-but 1)
                               (skosimp)
                               (expand "to_measure")
                               (lemma
                                "sigma_finite_contraction_def[T1,S1]"
                                ("nu" "contraction(mu, X!1)" "E" "E!2"))
                               (("1" (propax))
                                ("2"
                                 (expand "measurable_set?")
                                 (propax))))))
                            ("2"
                             (skosimp)
                             (expand "G")
                             (lemma "x_section_integrable"
                              ("mu"
                               "NU(i!1)"
                               "nu"
                               "fm_contraction[T2, S2]
                                                                            (contraction(nu, Y!1), A_of(contraction(nu, Y!1))(j!1))"
                               "M"
                               "E!1"))
                             (propax))))
                          ("2"
                           (expand "measurable_set?")
                           (skosimp)
                           (rewrite "A_of_def2"))))
                        ("2" (skosimp) (expand "G") (assert))))
                      ("2"
                       (skosimp)
                       (inst - "x1!1")
                       (expand "measurable_set?")
                       (expand "x_section")
                       (expand "x_section")
                       (propax))
                      ("3"
                       (expand "measurable_set?")
                       (skosimp)
                       (lemma "A_of_def2"
                        ("n" "j!1" "mu" "contraction[T2, S2](nu, Y!1)"))
                       (propax))))
                    ("2"
                     (skosimp)
                     (expand "measurable_set?")
                     (lemma "x_section_measurable"
                      ("x" "x!1" "S1" "S1" "S2" "S2" "Z" "E!1"))
                     (assert))))
                  ("2"
                   (skosimp)
                   (expand "F")
                   (replace -1)
                   (expand "o" 1)
                   (expand "x_section" 1 1)
                   (inst - "x!1")
                   (name-replace "MM" "x_section(EE, x!1)")
                   (hide-all-but (-2 1))
                   (lemma "sigma_finite_contraction_def[T2,S2]"
                    ("E" "MM" "nu" "nu"))
                   (("1"
                     (expand "fm_contraction")
                     (expand "x_sum")
                     (expand "x_eq")
                     (flatten)
                     (assert)
                     (lift-if)
                     (assert)
                     (prop)
                     (assert))
                    ("2" (propax))))
                  ("3"
                   (skosimp)
                   (inst - "x!1")
                   (expand "measurable_set?")
                   (propax))))
                ("2"
                 (skosimp)
                 (lemma "x_section_measurable"
                  ("S1"
                   "S1"
                   "S2"
                   "S2"
                   "x"
                   "x!1"
                   "Z"
                   "intersection(cross_product(X!1, Y!1), E!1)"))
                 (assert)
                 (expand "measurable_set?")
                 (assert))))
              ("2"
               (hide -1 2 -4 -2)
               (skosimp)
               (expand "F")
               (lemma "x_section_integrable"
                ("mu"
                 "MU(i!1)"
                 "nu"
                 "fm_contraction[T2, S2](nu, A_of(nu)(j!1))"
                 "M"
                 "intersection(cross_product(X!1, Y!1), E!1)"))
               (("1" (propax))
                ("2" (expand "measurable_set?") (propax))))))
            ("2"
             (hide-all-but 1)
             (skosimp)
             (lemma "sigma_finite_contraction_def" ("E" "E!2" "nu" "mu"))
             (("1" (expand "to_measure") (expand "MU") (propax))
              ("2" (expand "measurable_set?") (propax))))))
          ("2"
           (expand "measurable_set?")
           (skosimp)
           (rewrite "A_of_def2"))))
        ("2" (skosimp) (expand "F") (assert))))
      ("2"
       (skolem + "x!1")
       (expand "x_section")
       (lemma "x_section_measurable"
        ("S1"
         "S1"
         "S2"
         "S2"
         "Z"
         "intersection[[T1, T2]](cross_product(X!1, Y!1), E!1)"
         "x"
         "x!1"))
       (assert)
       (expand "measurable_set?")
       (propax))
      ("3" (expand "measurable_set?") (skosimp) (rewrite "A_of_def2"))))
    ("2" (expand "measurable_set?") (propax))))


