Quelle  essentially_bounded.prf   Sprache: Lisp

(essentially_bounded
 (mu_TCC1 0
  (mu_TCC1-1 nil 3477287079
   ("" (typepred "S")
    (("" (expand "sigma_algebra?")
      (("" (flatten)
        (("" (expand "subset_algebra_empty?") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_algebra_empty? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil essentially_bounded nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" essentially_bounded nil))
   nil))
 (essentially_bounded_TCC1 0
  (essentially_bounded_TCC1-1 nil 3477287079
   ("" (expand "essentially_bounded?")
    (("" (rewrite "const_measurable")
      (("" (expand "ae_bounded?")
        (("" (inst + "0")
          (("" (expand "abs")
            (("" (expand "abs")
              (("" (expand "sq_abs")
                (("" (assert)
                  (("" (expand "ae_le?")
                    (("" (expand "pointwise_ae?")
                      (("" (expand "ae?")
                        (("" (expand "ae_in?")
                          (("" (inst + "emptyset[T]")
                            (("" (skosimp) (("" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((const_measurable formula-decl nil complex_measurable nil)
    (complex type-decl nil complex_types "complex_alt/")
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (complex_? adt-recognizer-decl "[complex -> boolean]" complex_types
     "complex_alt/")
    (complex_ adt-constructor-decl "[[real, real] -> (complex_?)]"
     complex_types "complex_alt/")
    (T formal-type-decl nil essentially_bounded nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" essentially_bounded nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (abs const-decl "nnreal" polar "complex_alt/")
    (Im_rew formula-decl nil complex_types "complex_alt/")
    (sq_0 formula-decl nil sq "reals/")
    (Re_rew formula-decl nil complex_types "complex_alt/")
    (sqrt_0 formula-decl nil sqrt "reals/")
    (pointwise_ae? const-decl "bool" measure_theory
     "measure_integration/")
    (ae_in? const-decl "bool" measure_theory "measure_integration/")
    (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (measure? const-decl "bool" generalized_measure_def
     "measure_integration/")
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (mu formal-const-decl "measure_type[T, S]" essentially_bounded nil)
    (negligible_set? const-decl "bool" measure_theory
     "measure_integration/")
    (negligible nonempty-type-eq-decl nil measure_theory
     "measure_integration/")
    (emptyset const-decl "set" sets nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (null_emptyset name-judgement "null_set[T, S, mu]"
     essentially_bounded nil)
    (subset_algebra_emptyset name-judgement "(S)" essentially_bounded
     nil)
    (ae? const-decl "bool" measure_theory "measure_integration/")
    (subset_algebra_fullset name-judgement "(S)" essentially_bounded
     nil)
    (measurable_fullset name-judgement "measurable_set[T, S]"
     essentially_bounded nil)
    (ae_le? const-decl "bool" measure_theory "measure_integration/")
    (sq_abs const-decl "nnreal" complex_types "complex_alt/")
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (ae_bounded? const-decl "bool" complex_measure_theory nil)
    (essentially_bounded? const-decl "bool" essentially_bounded nil))
   nil))
 (essential_bound_TCC1 0
  (essential_bound_TCC1-1 nil 3477287079
   ("" (skosimp)
    (("" (split)
      (("1" (typepred "f!1")
        (("1" (expand "essentially_bounded?")
          (("1" (flatten)
            (("1" (expand "ae_bounded?")
              (("1" (skosimp)
                (("1" (expand "extend")
                  (("1" (expand "nonempty?")
                    (("1" (expand "empty?")
                      (("1" (expand "member")
                        (("1" (inst - "K!1") (("1" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "extend")
        (("2" (expand "below_bounded")
          (("2" (inst + "0")
            (("2" (expand "lower_bound") (("2" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((ae_bounded? const-decl "bool" complex_measure_theory nil)
    (extend const-decl "R" extend nil)
    (empty? const-decl "bool" sets nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (complex_measurable_def formula-decl nil complex_measurable nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (S formal-const-decl "sigma_algebra[T]" essentially_bounded nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil essentially_bounded nil)
    (complex type-decl nil complex_types "complex_alt/")
    (essentially_bounded? const-decl "bool" essentially_bounded nil)
    (essentially_bounded nonempty-type-eq-decl nil essentially_bounded
     nil)
    (below_bounded const-decl "bool" bounded_reals "reals/")
    (lower_bound const-decl "bool" bound_defs "reals/"))
   nil))
 (essential_bound_TCC2 0
  (essential_bound_TCC2-1 nil 3477287079
   ("" (skosimp)
    (("" (lemma "essential_bound_TCC1" ("f" "f!1"))
      (("" (flatten)
        ((""
          (typepred "inf[real]
          (extend[real, nnreal, bool, FALSE]
               ({K | ae_le?[T, S, mu](abs[T](f!1), LAMBDA x: K)}))")
          ((""
            (name-replace "INF" "inf[real]
          (extend[real, nnreal, bool, FALSE]
               ({K | ae_le?[T, S, mu](abs[T](f!1), LAMBDA x: K)}))")
            (("" (hide -2 -3)
              (("" (expand "greatest_lower_bound")
                (("" (flatten)
                  (("" (expand "lower_bound")
                    (("" (inst -2 "0")
                      (("" (split -2)
                        (("1" (assert) nil nil) ("2" (assert) nil nil)
                         ("3" (skosimp)
                          (("3" (typepred "z!1")
                            (("3" (case "z!1<0")
                              (("1"
                                (hide 1)
                                (("1"
                                  (expand "extend")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((essentially_bounded nonempty-type-eq-decl nil essentially_bounded
     nil)
    (essentially_bounded? const-decl "bool" essentially_bounded nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (complex type-decl nil complex_types "complex_alt/")
    (T formal-type-decl nil essentially_bounded nil)
    (essential_bound_TCC1 subtype-tcc nil essentially_bounded nil)
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (ae_le? const-decl "bool" measure_theory "measure_integration/")
    (mu formal-const-decl "measure_type[T, S]" essentially_bounded nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (measure? const-decl "bool" generalized_measure_def
     "measure_integration/")
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (S formal-const-decl "sigma_algebra[T]" essentially_bounded nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (setofsets type-eq-decl nil sets nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
     bounded_reals "reals/")
    (inf_set type-eq-decl nil bounded_reals "reals/")
    (below_bounded const-decl "bool" bounded_reals "reals/")
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
    (greatest_lower_bound const-decl "bool" bound_defs "reals/")
    (pred type-eq-decl nil defined_types nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lower_bound const-decl "bool" bound_defs "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil))
   nil))
 (essential_bound_def1 0
  (essential_bound_def1-1 nil 3477311458
   ("" (skosimp)
    (("" (expand "essential_bound")
      (("" (lemma "essential_bound_TCC1" ("f" "f!1"))
        ((""
          (typepred "inf(extend[real, nnreal, bool, FALSE]
              ({K | ae_le?(abs(f!1), LAMBDA x: K)}))")
          ((""
            (name-replace "INF" "inf(extend[real, nnreal, bool, FALSE]
              ({K | ae_le?(abs(f!1), LAMBDA x: K)}))")
            (("" (expand "greatest_lower_bound")
              (("" (flatten)
                (("" (expand "lower_bound")
                  (("" (inst - "K!1")
                    (("" (hide -1 -2 -3 2)
                      (("" (expand "extend") (("" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((essential_bound const-decl "nnreal" essentially_bounded nil)
    (abs const-decl "[T -> nonneg_real]" complex_fun_ops
         "complex_alt/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (ae_le? const-decl "bool" measure_theory "measure_integration/")
    (mu formal-const-decl "measure_type[T, S]" essentially_bounded nil)
    (measure_type nonempty-type-eq-decl nil generalized_measure_def
     "measure_integration/")
    (measure? const-decl "bool" generalized_measure_def
     "measure_integration/")
    (extended_nnreal nonempty-type-eq-decl nil extended_nnreal
     "extended_nnreal/")
    (S formal-const-decl "sigma_algebra[T]" essentially_bounded nil)
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
     "measure_integration/")
    (sigma_algebra? const-decl "bool" subset_algebra_def
     "measure_integration/")
    (setofsets type-eq-decl nil sets nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
     bounded_reals "reals/")
    (inf_set type-eq-decl nil bounded_reals "reals/")
    (below_bounded const-decl "bool" bounded_reals "reals/")
    (setof type-eq-decl nil defined_types nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
    (greatest_lower_bound const-decl "bool" bound_defs "reals/")
    (pred type-eq-decl nil defined_types nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (lower_bound const-decl "bool" bound_defs "reals/")
    (K!1 skolem-const-decl "nnreal" essentially_bounded nil)
    (f!1 skolem-const-decl "essentially_bounded" essentially_bounded
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (essential_bound_TCC1 subtype-tcc nil essentially_bounded nil)
    (T formal-type-decl nil essentially_bounded nil)
    (complex type-decl nil complex_types "complex_alt/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (essentially_bounded? const-decl "bool" essentially_bounded nil)
    (essentially_bounded nonempty-type-eq-decl nil essentially_bounded
     nil))
   shostak))
 (essential_bound_def2 0
  (essential_bound_def2-1 nil 3477312383
   ("" (skosimp)
    (("" (lemma "essential_bound_TCC1" ("f" "f!1"))
      (("" (expand "essential_bound")
        ((""
          (typepred "inf(extend[real, nnreal, bool, FALSE]
                       ({K | ae_le?(abs(f!1), LAMBDA x: K)}))")
          (("1"
            (name-replace "INF" "inf(extend[real, nnreal, bool, FALSE]
                       ({K | ae_le?(abs(f!1), LAMBDA x: K)}))")
            (("1" (flatten)
              (("1"
                (name "X"
                      "{a:real | a >= 0 & ae_le?(abs(f!1), LAMBDA x: a)}")
                (("1" (case "nonempty?[real](X)")
                  (("1" (case "below_bounded[real](X)")
                    (("1" (hide -5 -6)
                      (("1" (name "M" "lambda (n:posnat): inf(X)+1/n")
                        (("1" (case "forall (n:posnat): X(M(n))")
                          (("1" (case-replace "inf(X)=INF")
                            (("1" (hide -1)
                              (("1"
                                (expand "greatest_lower_bound")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (case
                                     "convergence?(lambda (n:nat): M(n+1),INF)")
                                    (("1"
                                      (expand "lower_bound")
                                      (("1"
                                        (name
                                         "E"
                                         "lambda (n:nat): choose({N:null_set[T,S,mu] | FORALL x: (not N(x)) => abs(f!1(x)) <= M(1+n)})")
                                        (("1"
                                          (case "null_set?(IUnion(E))")
                                          (("1"
                                            (case
                                             "forall x: (not IUnion(E)(x)) => abs(f!1(x)) <= INF")
                                            (("1"
                                              (expand "ae_le?")
                                              (("1"
                                                (expand
                                                 "pointwise_ae?")
                                                (("1"
                                                  (expand "ae?")
                                                  (("1"
                                                    (expand "fullset")
                                                    (("1"
                                                      (expand "ae_in?")
                                                      (("1"
                                                        (inst
                                                         +
                                                         "IUnion(E)")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (expand
                                                             "member")
                                                            (("1"
                                                              (expand
                                                               "abs"
                                                               2)
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "x!1")
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (skosimp)
                                                (("2"
                                                  (hide -1)
                                                  (("2"
                                                    (expand "IUnion" 1)
                                                    (("2"
                                                      (inst
                                                       -9
                                                       "abs(f!1(x!1))")
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (split -9)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (replace
                                                               -1
                                                               2
                                                               rl)
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (skosimp)
                                                            (("2"
                                                              (case
                                                               "z!1)
                                                              (("1"
                                                                (hide
                                                                 1)
                                                                (("1"
                                                                  (typepred
                                                                   "z!1")
                                                                  (("1"
                                                                    (expand
                                                                     "extend"
                                                                     -1)
                                                                    (("1"
                                                                      (prop)
                                                                      (("1"
                                                                        (inst
                                                                         -11
                                                                         "z!1")
                                                                        (("1"
                                                                          (expand
                                                                           "<="
                                                                           -11)
                                                                          (("1"
                                                                            (split
                                                                             -11)
                                                                            (("1"
                                                                              (name
                                                                               "EPS"
                                                                               "z!1-INF")
                                                                              (("1"
                                                                                (case
                                                                                 "EPS>0")
                                                                                (("1"
                                                                                  (lemma
                                                                                   "archimedean"
                                                                                   ("px"
                                                                                    "EPS"))
                                                                                  (("1"
                                                                                    (skosimp)
                                                                                    (("1"
                                                                                      (inst
                                                                                       -10
                                                                                       "n!1+1")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "X"
                                                                                         -10)
                                                                                        (("1"
                                                                                          (flatten)
                                                                                          (("1"
                                                                                            (case
                                                                                             "INF < M(1 + n!1) & M(1 + n!1) < z!1")
                                                                                            (("1"
                                                                                              (flatten)
                                                                                              (("1"
                                                                                                (inst
                                                                                                 +
                                                                                                 "n!1")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "E"
                                                                                                   1)
                                                                                                  (("1"
                                                                                                    (lemma
                                                                                                     "choose_member"
                                                                                                     ("a"
                                                                                                      "{N: null_set[T, S, mu] |
                FORALL x: (NOT N(x)) => abs(f!1(x)) <= M(1 + n!1)}"))
                                                                                                    (("1"
                                                                                                      (name-replace
                                                                                                       "EE"
                                                                                                       "choose({N: null_set[T, S, mu] |
                FORALL x: (NOT N(x)) => abs(f!1(x)) <= M(1 + n!1)})")
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "member")
                                                                                                        (("1"
                                                                                                          (split
                                                                                                           -1)
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "x!1")
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil)
                                                                                                           ("2"
                                                                                                            (expand
                                                                                                             "empty?")
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "member")
                                                                                                              (("2"
                                                                                                                (hide-all-but
                                                                                                                 (-1
                                                                                                                  -14))
                                                                                                                (("2"
                                                                                                                  (expand
                                                                                                                   "ae_le?")
                                                                                                                  (("2"
                                                                                                                    (expand
                                                                                                                     "pointwise_ae?")
                                                                                                                    (("2"
                                                                                                                      (expand
                                                                                                                       "ae?")
                                                                                                                      (("2"
                                                                                                                        (expand
                                                                                                                         "fullset")
                                                                                                                        (("2"
                                                                                                                          (expand
                                                                                                                           "ae_in?")
                                                                                                                          (("2"
                                                                                                                            (skosimp)
                                                                                                                            (("2"
                                                                                                                              (typepred
                                                                                                                               "E!1")
                                                                                                                              (("2"
                                                                                                                                (expand
                                                                                                                                 "negligible_set?")
                                                                                                                                (("2"
                                                                                                                                  (skosimp)
                                                                                                                                  (("2"
                                                                                                                                    (inst
                                                                                                                                     -
                                                                                                                                     "X!1")
                                                                                                                                    (("2"
                                                                                                                                      (skosimp)
                                                                                                                                      (("2"
                                                                                                                                        (inst
                                                                                                                                         -
                                                                                                                                         "x!2")
                                                                                                                                        (("2"
                                                                                                                                          (expand
                                                                                                                                           "abs"
                                                                                                                                           -3)
                                                                                                                                          (("2"
                                                                                                                                            (assert)
                                                                                                                                            (("2"
                                                                                                                                              (expand
                                                                                                                                               "subset?")
                                                                                                                                              (("2"
                                                                                                                                                (inst
                                                                                                                                                 -
                                                                                                                                                 "x!2")
                                                                                                                                                (("2"
                                                                                                                                                  (assert)
                                                                                                                                                  nil
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil)
                                                                                                       ("2"
                                                                                                        (hide-all-but
                                                                                                         (1
                                                                                                          -14))
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "nonempty?")
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "ae_le?")
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "empty?")
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "pointwise_ae?")
                                                                                                                (("2"
                                                                                                                  (expand
                                                                                                                   "ae?")
                                                                                                                  (("2"
                                                                                                                    (expand
                                                                                                                     "fullset")
                                                                                                                    (("2"
                                                                                                                      (expand
                                                                                                                       "ae_in?")
                                                                                                                      (("2"
                                                                                                                        (skosimp)
                                                                                                                        (("2"
                                                                                                                          (typepred
                                                                                                                           "E!1")
                                                                                                                          (("2"
                                                                                                                            (expand
                                                                                                                             "negligible_set?")
                                                                                                                            (("2"
                                                                                                                              (skosimp)
                                                                                                                              (("2"
                                                                                                                                (inst
                                                                                                                                 -3
                                                                                                                                 "X!1")
                                                                                                                                (("2"
                                                                                                                                  (expand
                                                                                                                                   "subset?")
                                                                                                                                  (("2"
                                                                                                                                    (expand
                                                                                                                                     "member")
                                                                                                                                    (("2"
                                                                                                                                      (skosimp)
                                                                                                                                      (("2"
                                                                                                                                        (inst
                                                                                                                                         -
                                                                                                                                         "x!2")
                                                                                                                                        (("2"
                                                                                                                                          (inst
                                                                                                                                           -
                                                                                                                                           "x!2")
                                                                                                                                          (("2"
                                                                                                                                            (expand
                                                                                                                                             "abs"
                                                                                                                                             -3)
                                                                                                                                            (("2"
                                                                                                                                              (assert)
                                                                                                                                              nil
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (replace
                                                                                               -12
                                                                                               *
                                                                                               rl)
                                                                                              (("2"
                                                                                                (hide-all-but
                                                                                                 (-1
                                                                                                  -2
                                                                                                  -3
                                                                                                  -4
                                                                                                  -5
                                                                                                  1))
                                                                                                (("2"
                                                                                                  (assert)
                                                                                                  (("2"
                                                                                                    (lemma
                                                                                                     "posreal_div_posreal_is_posreal"
                                                                                                     ("px"
                                                                                                      "1"
                                                                                                      "py"
                                                                                                      "1+n!1"))
                                                                                                    (("2"
                                                                                                      (assert)
                                                                                                      (("2"
                                                                                                        (replace
                                                                                                         -4
                                                                                                         -2
                                                                                                         rl)
                                                                                                        (("2"
                                                                                                          (lemma
                                                                                                           "both_sides_div_pos_lt2"
                                                                                                           ("pz"
                                                                                                            "1"
                                                                                                            "py"
                                                                                                            "n!1"
                                                                                                            "px"
                                                                                                            "1+n!1"))
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (reveal
                                                                               2)
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (rewrite "null_IUnion")
                                            nil
                                            nil))
                                          nil)
                                         ("2"
                                          (skosimp)
                                          (("2"
                                            (inst -2 "1+n!1")
                                            (("2"
                                              (expand "X" -2)
                                              (("2"
                                                (flatten)
                                                (("2"
                                                  (hide-all-but
                                                   (-2 -3 1))
                                                  (("2"
                                                    (expand
                                                     "nonempty?")
                                                    (("2"
                                                      (expand "empty?")
                                                      (("2"
                                                        (expand
                                                         "ae_le?")
                                                        (("2"
                                                          (expand
                                                           "pointwise_ae?")
                                                          (("2"
                                                            (expand
                                                             "ae?")
                                                            (("2"
                                                              (expand
                                                               "fullset")
                                                              (("2"
                                                                (expand
                                                                 "ae_in?")
                                                                (("2"
                                                                  (expand
                                                                   "member")
                                                                  (("2"
                                                                    (skosimp)
                                                                    (("2"
                                                                      (typepred
                                                                       "E!1")
                                                                      (("2"
                                                                        (expand
                                                                         "negligible_set?")
                                                                        (("2"
                                                                          (skosimp)
                                                                          (("2"
                                                                            (inst
                                                                             -3
                                                                             "X!1")
--> --------------------

--> maximum size reached

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