Impressum countable_convergence.prf

(countable_convergence
 (convergent?_TCC1 0
  (convergent?_TCC1-1 nil 3322366680
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (lemma "countably_infinite_def" ("S" "X!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countable_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (countably_infinite_def formula-decl nil countable_props
     "sets_aux/"))
   shostak))
 (convergent_zero 0
  (convergent_zero-1 nil 3323142075
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "convergent?")
        (("" (flatten)
          (("" (expand "o")
            (("" (expand "absconvergent?")
              (("" (expand "abs")
                (("" (expand "abs")
                  (("" (rewrite "zero_series_conv") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countable_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (zero_series_conv formula-decl nil series "series/")
    (abs const-decl "sequence[real]" series "series/")
    (O const-decl "T3" function_props nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
 (convergent_plus 0
  (convergent_plus-1 nil 3351595333
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "convergent?")
        (("" (flatten)
          (("" (assert)
            (("" (expand "absconvergent?")
              (("" (name-replace "DX" "denumerable_enumeration(X!1)")
                ((""
                  (lemma "sum_absconvergent"
                   ("aa" "f!1 o DX" "bb" "g!1 o DX"))
                  (("1" (expand "absconvergent?")
                    (("1" (expand "o ")
                      (("1" (expand "+") (("1" (propax) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (expand "o")
                    (("2" (expand "absconvergent?")
                      (("2" (propax) nil nil)) nil))
                    nil)
                   ("3" (expand "o")
                    (("3" (expand "absconvergent?")
                      (("3" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countable_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (sum_absconvergent formula-decl nil absconv_series "series/")
    (sequence type-eq-decl nil sequences nil)
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (O const-decl "T3" function_props nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
 (convergent_scal 0
  (convergent_scal-1 nil 3351595652
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (flatten)
        (("" (assert)
          (("" (name-replace "DX" "denumerable_enumeration(X!1)")
            ((""
              (lemma "scal_absconvergent" ("aa" "f!1 o DX" "x" "a!1"))
              (("1" (expand "o")
                (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" countable_convergence nil)
    (O const-decl "T3" function_props nil)
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (absconvergent? const-decl "bool" absconv_series "series/")
    (sequence type-eq-decl nil sequences nil)
    (scal_absconvergent formula-decl nil absconv_series "series/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countable_convergence nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
 (convergent_opp 0
  (convergent_opp-1 nil 3351596230
   ("" (skosimp)
    (("" (lemma "convergent_scal" ("X" "X!1" "f" "f!1" "a" "-1"))
      (("" (expand "-") (("" (expand "*") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil countable_convergence nil)
    (convergent_scal formula-decl nil countable_convergence nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (convergent_diff 0
  (convergent_diff-1 nil 3351596280
   ("" (skosimp)
    (("" (lemma "convergent_opp" ("X" "X!1" "f" "g!1"))
      (("" (assert)
        (("" (lemma "convergent_plus" ("X" "X!1" "f" "f!1" "g" "-g!1"))
          (("" (assert)
            (("" (expand "-")
              (("" (expand "+") (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil countable_convergence nil)
    (convergent_opp formula-decl nil countable_convergence nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (convergent_plus formula-decl nil countable_convergence nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/"))
   shostak))
 (convergent_le 0
  (convergent_le-1 nil 3351599438
   ("" (expand "convergent?")
    (("" (skosimp*)
      (("" (assert)
        (("" (expand "absconvergent?")
          (("" (name-replace "DX" "denumerable_enumeration(X!1)")
            ((""
              (lemma "comparison_test"
               ("b" "abs(f!1 o DX)" "a" "abs(g!1 o DX)"))
              (("" (split -1)
                (("1" (propax) nil nil) ("2" (propax) nil nil)
                 ("3" (hide-all-but (-1 1))
                  (("3" (skosimp)
                    (("3" (inst - "DX(n!1)") (("3" (grind) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((absconvergent? const-decl "bool" absconv_series "series/")
    (comparison_test formula-decl nil series "series/")
    (sequence type-eq-decl nil sequences nil)
    (abs const-decl "sequence[real]" series "series/")
    (O const-decl "T3" function_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countable_convergence nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
 (convergent_zeros 0
  (convergent_zeros-1 nil 3406442125
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "convergent?")
        (("" (flatten)
          (("" (expand "absconvergent?")
            (("" (lemma "zero_series_conv")
              (("" (expand "o ")
                (("" (lemma "countably_infinite_def" ("S" "X!1"))
                  (("" (assert)
                    ((""
                      (case-replace "abs(LAMBDA (x: nat):
                              g!1(denumerable_enumeration(X!1)(x)))=lambda (x:nat): 0")
                      (("" (hide-all-but (1 -4 -1))
                        (("" (apply-extensionality :hide? t)
                          (("" (expand "abs")
                            ((""
                              (inst -
                               "denumerable_enumeration(X!1)(x!1)")
                              ((""
                                (replace -2)
                                ((""
                                  (expand "abs")
                                  (("" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil countable_convergence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (zero_series_conv formula-decl nil series "series/")
    (countably_infinite_def formula-decl nil countable_props
     "sets_aux/")
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sequence type-eq-decl nil sequences nil)
    (abs const-decl "sequence[real]" series "series/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (O const-decl "T3" function_props nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
 (convergent_empty 0
  (convergent_empty-1 nil 3351591225
   ("" (skosimp)
    (("" (expand "convergent?") (("" (propax) nil nil)) nil)) 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_convergence nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
 (convergent_singleton 0
  (convergent_singleton-1 nil 3351591618
   ("" (skosimp*)
    (("" (expand "convergent?") (("" (propax) nil nil)) nil)) nil)
   ((nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" countable_convergence nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
 (convergent_subset 0
  (convergent_subset-1 nil 3323142263
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (flatten)
        (("" (case-replace "is_finite(Y!1)")
          (("1" (lemma "finite_subset" ("s" "X!1" "A" "Y!1"))
            (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)
           ("2" (assert)
            (("2" (typepred "X!1")
              (("2" (typepred "Y!1")
                (("2" (rewrite "countable_props.countable_card" -1)
                  (("2" (rewrite "countable_props.countable_card" -2)
                    (("2" (hide 1 2)
                      (("2"
                        (lemma "denumerable_enumeration_bij"
                         ("X" "X!1"))
                        (("2"
                          (lemma "denumerable_enumeration_bij"
                           ("X" "Y!1"))
                          (("2"
                            (name-replace "PHI_X"
                             "denumerable_enumeration(X!1)")
                            (("2"
                              (name-replace "PHI_Y"
                               "denumerable_enumeration(Y!1)")
                              (("2"
                                (expand "o")
                                (("2"
                                  (lemma
                                   "bijective_inverse_exists[nat, (X!1)]"
                                   ("f" "PHI_X"))
                                  (("1"
                                    (lemma
                                     "bijective_inverse_exists[nat, (Y!1)]"
                                     ("f" "PHI_Y"))
                                    (("1"
                                      (expand "exists1")
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (skolem - ("PSI_Y"))
                                          (("1"
                                            (skolem - ("PSI_X"))
                                            (("1"
                                              (lemma
                                               "bij_inv_is_bij_alt[nat,(X!1)]"
                                               ("f"
                                                "PHI_X"
                                                "g"
                                                "PSI_X"))
                                              (("1"
                                                (lemma
                                                 "bij_inv_is_bij_alt[nat,(Y!1)]"
                                                 ("f"
                                                  "PHI_Y"
                                                  "g"
                                                  "PSI_Y"))
                                                (("1"
                                                  (case
                                                   "FORALL (a:sequence[real],inj:(injective?[nat,nat])):absconvergent?(a) =>  absconvergent?(a o inj)")
                                                  (("1"
                                                    (case
                                                     "injective?[nat,nat](PSI_Y o PHI_X)")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "g!1 o PHI_Y"
                                                       "PSI_Y o PHI_X")
                                                      (("1"
                                                        (split -2)
                                                        (("1"
                                                          (expand "o")
                                                          (("1"
                                                            (lemma
                                                             "comp_inverse_right_surj_alt[nat,(Y!1)]"
                                                             ("f"
                                                              "PHI_Y"
                                                              "g"
                                                              "PSI_Y"))
                                                            (("1"
                                                              (lemma
                                                               "extensionality"
                                                               ("f"
                                                                "LAMBDA (x_1: nat): g!1(PHI_Y(PSI_Y(PHI_X(x_1))))"
                                                                "g"
                                                                "LAMBDA (x: nat): g!1(PHI_X(x))"))
                                                              (("1"
                                                                (split
                                                                 -1)
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (propax)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (skosimp)
                                                                  (("2"
                                                                    (typepred
                                                                     "PHI_X(x!1)")
                                                                    (("2"
                                                                      (hide-all-but
                                                                       (-1
                                                                        -2
                                                                        -15
                                                                        1))
                                                                      (("2"
                                                                        (expand
                                                                         "subset?")
                                                                        (("2"
                                                                          (inst
                                                                           -3
                                                                           "PHI_X(x!1)")
                                                                          (("2"
                                                                            (expand
                                                                             "member")
                                                                            (("2"
                                                                              (inst
                                                                               -
                                                                               "PHI_X(x!1)")
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "bijective?")
                                                              (("2"
                                                                (flatten)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (expand "o ")
                                                          (("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide-all-but
                                                       (-2 -12 -9 1))
                                                      (("2"
                                                        (expand
                                                         "bijective?")
                                                        (("2"
                                                          (flatten)
                                                          (("2"
                                                            (expand
                                                             "injective?")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (expand
                                                                 "o")
                                                                (("2"
                                                                  (inst
                                                                   -4
                                                                   "x1!1"
                                                                   "x2!1")
                                                                  (("2"
                                                                    (expand
                                                                     "subset?")
                                                                    (("2"
                                                                      (expand
                                                                       "member")
                                                                      (("2"
                                                                        (inst-cp
                                                                         -6
                                                                         "PHI_X(x1!1)")
                                                                        (("2"
                                                                          (inst
                                                                           -6
                                                                           "PHI_X(x2!1)")
                                                                          (("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (hide
                                                                               1
                                                                               -3
                                                                               -4)
                                                                              (("2"
                                                                                (inst
                                                                                 -
                                                                                 "PHI_X(x1!1)"
                                                                                 "PHI_X(x2!1)")
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (hide -1 -13 2)
                                                      (("3"
                                                        (skosimp)
                                                        (("3"
                                                          (expand
                                                           "subset?")
                                                          (("3"
                                                            (inst
                                                             -
                                                             "PHI_X(x1!1)")
                                                            (("3"
                                                              (expand
                                                               "member")
                                                              (("3"
                                                                (propax)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide-all-but 1)
                                                    (("2"
                                                      (skosimp*)
                                                      (("2"
                                                        (expand
                                                         "absconvergent?")
                                                        (("2"
                                                          (lemma
                                                           "abs_series_inj_conv"
                                                           ("aa"
                                                            "abs(a!1)"
                                                            "inj"
                                                            "inj!1"))
                                                          (("1"
                                                            (lemma
                                                             "extensionality"
                                                             ("f"
                                                              "abs(a!1) o inj!1"
                                                              "g"
                                                              "abs(a!1 o inj!1)"))
                                                            (("1"
                                                              (split
                                                               -1)
                                                              (("1"
                                                                (replace
                                                                 -1)
                                                                (("1"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 1)
                                                                (("2"
                                                                  (skosimp)
                                                                  (("2"
                                                                    (expand
                                                                     "abs")
                                                                    (("2"
                                                                      (expand
                                                                       "o")
                                                                      (("2"
                                                                        (propax)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "absconvergent?")
                                                            (("2"
                                                              (hide 2)
                                                              (("2"
                                                                (lemma
                                                                 "extensionality"
                                                                 ("f"
                                                                  "abs(a!1)"
                                                                  "g"
                                                                  "abs(abs(a!1))"))
                                                                (("2"
                                                                  (split
                                                                   -1)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (hide-all-but
                                                                     1)
                                                                    (("2"
                                                                      (grind)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil)
                                               ("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (propax) nil nil))
                                    nil)
                                   ("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" countable_convergence nil)
    (T formal-type-decl nil countable_convergence nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (finite_subset formula-decl nil finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (countable_card formula-decl nil countable_props "sets_aux/")
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (bijective? const-decl "bool" functions nil)
    (exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (sequence type-eq-decl nil sequences nil)
    (injective? const-decl "bool" functions nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (Y!1 skolem-const-decl "countable_set[T]" countable_convergence
     nil)
    (PSI_Y skolem-const-decl "[(Y!1) -> nat]" countable_convergence
     nil)
    (X!1 skolem-const-decl "countable_set[T]" countable_convergence
     nil)
    (PHI_X skolem-const-decl "[nat -> (X!1)]" countable_convergence
     nil)
    (extensionality formula-decl nil functions nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (surjective? const-decl "bool" functions nil)
    (comp_inverse_right_surj_alt formula-decl nil function_inverse_def
     nil)
    (abs_series_inj_conv formula-decl nil absconv_series_aux nil)
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (abs const-decl "sequence[real]" series "series/")
    (minus_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (O const-decl "T3" function_props nil)
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (denumerable_enumeration_bij formula-decl nil
     denumerable_enumeration nil))
   shostak))
 (convergent_intersection 0
  (convergent_intersection-1 nil 3351591237
   ("" (skosimp)
    (("" (split)
      (("1"
        (lemma "convergent_subset"
         ("X" "intersection(X!1, Y!1)" "Y" "X!1" "g" "g!1"))
        (("1" (assert)
          (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil))
        nil)
       ("2"
        (lemma "convergent_subset"
         ("X" "intersection(X!1, Y!1)" "Y" "Y!1" "g" "g!1"))
        (("2" (split)
          (("1" (propax) nil nil)
           ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)
           ("3" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (countable_intersection1 application-judgement "countable_set[T]"
     countable_convergence nil)
    (convergent_subset formula-decl nil countable_convergence nil)
    (T formal-type-decl nil countable_convergence nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (intersection const-decl "set" sets nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil))
   shostak))
 (convergent_difference 0
  (convergent_difference-1 nil 3351593239
   ("" (skosimp)
    ((""
      (lemma "convergent_subset"
       ("X" "difference(X!1, Y!1)" "Y" "X!1" "g" "g!1"))
      (("" (assert) (("" (hide-all-but 1) (("" (grind) nil nil)) nil))
        nil))
      nil))
    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)
    (difference const-decl "set" sets nil)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil countable_convergence nil)
    (convergent_subset formula-decl nil countable_convergence nil)
    (countable_difference application-judgement "countable_set[T]"
     countable_convergence nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil))
   shostak))
 (convergent_disjoint_union 0
  (convergent_disjoint_union-2 nil 3462016397
   (""
    (case "FORALL (X:finite_set[T], Y: countable_set[T], g: [T -> real]):
               disjoint?(X, Y) AND convergent?(X)(g) AND convergent?(Y)(g) IMPLIES
                convergent?(union(X, Y))(g)")
    (("1" (skosimp)
      (("1" (expand "convergent?")
        (("1" (case-replace "is_finite(X!1)")
          (("1" (inst - "X!1" "Y!1" "g!1")
            (("1" (replace -4) (("1" (assert) nil nil)) nil)) nil)
           ("2" (assert)
            (("2" (case-replace "is_finite(Y!1)")
              (("1" (inst - "Y!1" "X!1" "g!1")
                (("1" (assert)
                  (("1" (split -2)
                    (("1" (rewrite "union_commutative")
                      (("1" (assert) nil nil)) nil)
                     ("2" (rewrite "union_commutative")
                      (("2" (assert) nil nil)) nil)
                     ("3" (hide-all-but (-2 1))
                      (("3" (expand "disjoint?")
                        (("3" (rewrite "intersection_commutative") nil
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (flatten)
                (("2" (assert)
                  (("2" (hide -1)
                    (("2" (expand "absconvergent?")
                      (("2"
                        (lemma "denumerable_enumeration_bij"
                         ("X" "X!1"))
                        (("2"
                          (lemma "denumerable_enumeration_bij"
                           ("X" "Y!1"))
                          (("2"
                            (lemma "denumerable_enumeration_bij"
                             ("X" "union(X!1,Y!1)"))
                            (("2"
                              (name-replace "DX"
                               "denumerable_enumeration(X!1)")
                              (("2"
                                (name-replace
                                 "DY"
                                 "denumerable_enumeration(Y!1)")
                                (("2"
                                  (name-replace
                                   "DXY"
                                   "denumerable_enumeration(union(X!1,Y!1))")
                                  (("2"
                                    (lemma
                                     "bijective_inverse_exists[nat, (union(X!1, Y!1))]"
                                     ("f" "DXY"))
                                    (("1"
                                      (expand "exists1")
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (skolem - ("CXY"))
                                          (("1"
                                            (lemma
                                             "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]"
                                             ("f" "DXY" "g" "CXY"))
                                            (("1"
                                              (name
                                               "PHI"
                                               "LAMBDA (n:nat): IF even?(n) THEN DX(n/2) ELSE DY((n-1)/2) ENDIF")
                                              (("1"
                                                (case
                                                 "bijective?[nat, (union(X!1, Y!1))](PHI)")
                                                (("1"
                                                  (hide -2)
                                                  (("1"
                                                    (case
                                                     "forall (a:sequence[real]): convergent?(series(a)) => convergent?(series(LAMBDA (n:nat): IF even?(n) THEN a(n/2) ELSE 0 ENDIF))")
                                                    (("1"
                                                      (case
                                                       "FORALL (a: sequence[real]):
                               convergent?(series(a)) =>
                                convergent?(series(LAMBDA (n: nat):
                                                    IF odd?(n) THEN a((n-1)/2) ELSE 0 ENDIF))")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "abs(g!1 o DY)")
                                                        (("1"
                                                          (inst
                                                           -
                                                           "abs(g!1 o DX)")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (lemma
                                                               "series_sum_conv"
                                                               ("a"
                                                                "(LAMBDA (n: nat):
                                               IF even?(n) THEN abs(g!1 o DX)(n / 2)
                                               ELSE 0
                                               ENDIF)"
                                                                "b"
                                                                "(LAMBDA (n: nat):
                                               IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)
                                               ELSE 0
                                               ENDIF)"))
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (hide
                                                                   -2
                                                                   -3)
                                                                  (("1"
                                                                    (lemma
                                                                     "extensionality"
                                                                     ("f"
                                                                      "((LAMBDA (n: nat):
                                                  IF even?(n) THEN abs(g!1 o DX)(n / 2)
                                                  ELSE 0
                                                  ENDIF)
                                                +
                                                (LAMBDA (n: nat):
                                                   IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)
                                                   ELSE 0
                                                   ENDIF))"
                                                                      "g"
                                                                      "abs(g!1 o PHI)"))
                                                                    (("1"
                                                                      (split
                                                                       -1)
                                                                      (("1"
                                                                        (replace
                                                                         -1)
                                                                        (("1"
                                                                          (hide
                                                                           -1)
                                                                          (("1"
                                                                            (lemma
                                                                             "bijective_inverse_exists[nat, (union(X!1, Y!1))]"
                                                                             ("f"
                                                                              "PHI"))
                                                                            (("1"
                                                                              (expand
                                                                               "exists1")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (skolem
                                                                                   -
                                                                                   ("PSI"))
                                                                                  (("1"
                                                                                    (hide
                                                                                     -7
                                                                                     -2)
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]"
                                                                                       ("f"
                                                                                        "PHI"
                                                                                        "g"
                                                                                        "PSI"))
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "composition_bijective[nat,(union(X!1, Y!1)),nat]"
                                                                                         ("f2"
                                                                                          "PSI"
                                                                                          "f1"
                                                                                          "DXY"))
                                                                                        (("1"
                                                                                          (lemma
                                                                                           "comp_inverse_right_alt[nat, (union(X!1, Y!1))]"
                                                                                           ("f"
                                                                                            "PHI"
                                                                                            "g"
                                                                                            "PSI"))
                                                                                          (("1"
                                                                                            (hide-all-but
                                                                                             (-1
                                                                                              -2
                                                                                              -5
                                                                                              4))
                                                                                            (("1"
                                                                                              (lemma
                                                                                               "abs_series_bij_conv_abs"
                                                                                               ("phi"
                                                                                                "PSI o DXY"
                                                                                                "aa"
                                                                                                "abs(g!1 o PHI)"))
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (case-replace
                                                                                                   "abs(g!1 o PHI) o (PSI o DXY) = abs(g!1 o DXY)")
                                                                                                  (("1"
                                                                                                    (hide-all-but
                                                                                                     (-2
                                                                                                      1))
                                                                                                    (("1"
                                                                                                      (apply-extensionality
                                                                                                       1
                                                                                                       :hide?
                                                                                                       t)
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "o")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "abs")
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "DXY(x!1)")
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (propax)
                                                                                                nil
                                                                                                nil)
                                                                                               ("3"
                                                                                                (expand
                                                                                                 "absconvergent?")
                                                                                                (("3"
                                                                                                  (hide-all-but
                                                                                                   (-3
                                                                                                    1))
                                                                                                  (("3"
                                                                                                    (case-replace
                                                                                                     "abs(abs(o[nat, T, real](g!1, PHI))) = abs(g!1 o PHI)")
                                                                                                    (("3"
                                                                                                      (hide-all-but
                                                                                                       1)
                                                                                                      (("3"
                                                                                                        (apply-extensionality
                                                                                                         :hide?
                                                                                                         t)
                                                                                                        (("3"
                                                                                                          (expand
                                                                                                           "abs")
                                                                                                          (("3"
                                                                                                            (expand
                                                                                                             "o ")
                                                                                                            (("3"
                                                                                                              (grind)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (propax)
                                                                                          nil
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (propax)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (skosimp)
                                                                          (("2"
                                                                            (expand
                                                                             "+")
                                                                            (("2"
                                                                              (expand
                                                                               "PHI")
                                                                              (("2"
                                                                                (expand
                                                                                 "abs")
                                                                                (("2"
                                                                                  (expand
                                                                                   "o")
                                                                                  (("2"
                                                                                    (case-replace
                                                                                     "even?(x!1)")
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "even_or_odd"
                                                                                       ("x"
                                                                                        "x!1"))
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (lemma
                                                                                       "even_or_odd"
                                                                                       ("x"
                                                                                        "x!1"))
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide-all-but
                                                                       1)
                                                                      (("2"
                                                                        (expand
                                                                         "even?")
                                                                        (("2"
                                                                          (skosimp*)
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 1)
                                                                (("2"
                                                                  (expand
                                                                   "odd?")
                                                                  (("2"
                                                                    (skosimp*)
                                                                    (("2"
                                                                      (assert)
                                                                      (("2"
                                                                        (replace
                                                                         -1)
                                                                        (("2"
                                                                          (assert)
                                                                          (("2"
                                                                            (case
                                                                             "forall (i,j:int):i<j=>i+1<=j")
                                                                            (("1"
                                                                              (inst
                                                                               -
                                                                               "-1"
                                                                               "j!1")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (hide-all-but
                                                                               1)
                                                                              (("2"
                                                                                (grind)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("3"
                                                                (hide-all-but
                                                                 1)
                                                                (("3"
                                                                  (expand
                                                                   "even?")
                                                                  (("3"
                                                                    (skosimp*)
                                                                    (("3"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide-all-but
                                                         1)
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (expand
                                                             "convergent?")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (inst
                                                                 +
                                                                 "l!1")
                                                                (("2"
                                                                  (expand
                                                                   "convergence")
                                                                  (("2"
                                                                    (skosimp)
                                                                    (("2"
                                                                      (inst
                                                                       -
                                                                       "epsilon!1")
                                                                      (("2"
                                                                        (skosimp)
                                                                        (("2"
                                                                          (case
                                                                           "FORALL (m: nat):
                                 sigma(0, m, a!1) =
                                  sigma(0, 2 * m + 1,
                                        LAMBDA (n: nat):
                                          IF odd?(n) THEN a!1((n - 1) / 2) ELSE 0 ENDIF)")
                                                                          (("1"
                                                                            (inst
                                                                             +
                                                                             "2*n!1+1")
                                                                            (("1"
                                                                              (skosimp)
                                                                              (("1"
                                                                                (case
                                                                                 "even?(i!1)")
                                                                                (("1"
                                                                                  (expand
                                                                                   "even?")
                                                                                  (("1"
                                                                                    (skosimp)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "series")
                                                                                      (("1"
                                                                                        (replace
                                                                                         -1)
                                                                                        (("1"
                                                                                          (case-replace
                                                                                           "j!1=0")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("2"
                                                                                            (inst
                                                                                             -
                                                                                             "j!1-1")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "j!1-1")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (replace
                                                                                                   -2
                                                                                                   -3)
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "sigma"
                                                                                                     2)
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "odd?"
                                                                                                       2
                                                                                                       1)
                                                                                                      (("1"
                                                                                                        (propax)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (rewrite
                                                                                   "even_or_odd"
                                                                                   1)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "odd?"
                                                                                     -1)
                                                                                    (("2"
                                                                                      (skosimp)
                                                                                      (("2"
                                                                                        (replace
                                                                                         -1)
                                                                                        (("2"
                                                                                          (inst
                                                                                           -3
                                                                                           "j!1")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "j!1")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "series")
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (hide-all-but
                                                                             1)
                                                                            (("2"
                                                                              (induct
                                                                               "m")
                                                                              (("1"
                                                                                (expand
                                                                                 "sigma")
                                                                                (("1"
                                                                                  (expand
                                                                                   "sigma")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "odd?")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (skosimp*)
                                                                                (("2"
                                                                                  (expand
                                                                                   "sigma"
                                                                                   1)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "sigma"
                                                                                     1
                                                                                     2)
                                                                                    (("2"
                                                                                      (replace
                                                                                       -1
                                                                                       1
                                                                                       rl)
                                                                                      (("2"
                                                                                        (hide
                                                                                         -1)
                                                                                        (("2"
                                                                                          (assert)
                                                                                          (("2"
                                                                                            (expand
                                                                                             "odd?")
                                                                                            (("2"
                                                                                              (lemma
                                                                                               "div_cancel2"
                                                                                               ("x"
                                                                                                "1+j!1"
                                                                                                "n0z"
                                                                                                "2"))
                                                                                              (("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("3"
                                                                                (hide
                                                                                 2)
                                                                                (("3"
                                                                                  (expand
                                                                                   "odd?")
                                                                                  (("3"
                                                                                    (skosimp*)
                                                                                    (("3"
                                                                                      (replace
                                                                                       -1)
                                                                                      (("3"
                                                                                        (assert)
                                                                                        (("3"
                                                                                          (case
                                                                                           "forall (i,j:int):i<j=>i+1<=j")
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "-1"
                                                                                             "j!1")
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             1)
                                                                                            (("2"
                                                                                              (grind)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("3"
                                                                            (hide-all-but
                                                                             1)
                                                                            (("3"
                                                                              (expand
                                                                               "odd?")
                                                                              (("3"
                                                                                (skosimp*)
                                                                                (("3"
                                                                                  (assert)
                                                                                  (("3"
                                                                                    (assert)
                                                                                    (("3"
                                                                                      (case
                                                                                       "forall (i,j:int):i<j=>i+1<=j")
                                                                                      (("1"
                                                                                        (inst
                                                                                         -
                                                                                         "-1"
                                                                                         "j!1")
                                                                                        (("1"
                                                                                          (assert)
                                                                                          nil
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (hide-all-but
                                                                                         1)
                                                                                        (("2"
                                                                                          (grind)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("3"
                                                        (skosimp*)
                                                        (("3"
                                                          (hide-all-but
                                                           (-2 1))
                                                          (("3"
                                                            (expand
                                                             "odd?")
                                                            (("3"
                                                              (skosimp)
                                                              (("3"
                                                                (replace
                                                                 -1)
                                                                (("3"
                                                                  (assert)
                                                                  (("3"
                                                                    (typepred
                                                                     "n!1")
                                                                    (("3"
                                                                      (case
                                                                       "forall (i,j:int): i<j => i+1<=j")
                                                                      (("1"
                                                                        (inst
                                                                         -
                                                                         "-1"
                                                                         "j!1")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (skosimp)
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide-all-but 1)
                                                      (("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (expand
                                                           "convergent?")
                                                          (("2"
                                                            (skosimp)
                                                            (("2"
                                                              (inst
                                                               +
                                                               "l!1")
                                                              (("2"
                                                                (expand
                                                                 "convergence")
                                                                (("2"
                                                                  (skosimp*)
                                                                  (("2"
                                                                    (inst
                                                                     -
                                                                     "epsilon!1")
                                                                    (("2"
                                                                      (skosimp)
                                                                      (("2"
                                                                        (inst
                                                                         +
                                                                         "2*n!1")
                                                                        (("2"
                                                                          (skosimp)
                                                                          (("2"
                                                                            (case
                                                                             "even?(i!1)")
                                                                            (("1"
                                                                              (expand
                                                                               "even?"
                                                                               -1)
                                                                              (("1"
                                                                                (skosimp)
                                                                                (("1"
                                                                                  (replace
                                                                                   -1)
                                                                                  (("1"
                                                                                    (inst
                                                                                     -
                                                                                     "j!1")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "series")
                                                                                        (("1"
                                                                                          (case
                                                                                           "forall (m:nat): sigma(0, m, a!1) = sigma(0, 2*m,
                                           LAMBDA (n: nat):
                                             IF even?(n) THEN a!1(n / 2) ELSE 0 ENDIF)")
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "j!1")
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             1)
                                                                                            (("2"
                                                                                              (induct
                                                                                               "m")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "sigma")
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (skosimp)
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "sigma"
                                                                                                   1)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "sigma"
                                                                                                     1
                                                                                                     2)
                                                                                                    (("2"
                                                                                                      (lemma
                                                                                                       "div_cancel2"
                                                                                                       ("x"
                                                                                                        "1+j!1"
                                                                                                        "n0z"
                                                                                                        "2"))
                                                                                                      (("2"
                                                                                                        (assert)
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "even?"
                                                                                                           1
                                                                                                           1)
                                                                                                          (("2"
                                                                                                            (replace
                                                                                                             -2
                                                                                                             1
                                                                                                             rl)
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("3"
                                                                                                (expand
                                                                                                 "even?")
                                                                                                (("3"
                                                                                                  (skosimp*)
                                                                                                  (("3"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("3"
                                                                                            (expand
                                                                                             "even?")
                                                                                            (("3"
                                                                                              (skosimp*)
                                                                                              (("3"
                                                                                                (lemma
                                                                                                 "div_cancel2"
                                                                                                 ("x"
                                                                                                  "j!2"
                                                                                                  "n0z"
                                                                                                  "2"))
                                                                                                (("3"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (rewrite
                                                                               "even_or_odd"
                                                                               1)
                                                                              (("2"
                                                                                (expand
                                                                                 "odd?")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (replace
                                                                                     -1)
                                                                                    (("2"
                                                                                      (inst
                                                                                       -
                                                                                       "j!1")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (expand
                                                                                           "series")
                                                                                          (("1"
                                                                                            (case
                                                                                             "forall (m:nat): sigma(0,m,a!1) = sigma(0,1+2*m,LAMBDA (n:nat): IF even?(n) THEN a!1(n/2) ELSE 0 ENDIF)")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "j!1")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (hide-all-but
                                                                                               1)
                                                                                              (("2"
                                                                                                (induct
                                                                                                 "m")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "sigma")
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "sigma")
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "even?")
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (skosimp*)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "sigma"
                                                                                                     1)
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "sigma"
                                                                                                       1
                                                                                                       2)
                                                                                                      (("2"
                                                                                                        (replace
                                                                                                         -1
                                                                                                         1
                                                                                                         rl)
                                                                                                        (("2"
                                                                                                          (assert)
                                                                                                          (("2"
                                                                                                            (hide
                                                                                                             -1)
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "even?")
                                                                                                              (("2"
                                                                                                                (lemma
                                                                                                                 "div_cancel2"
                                                                                                                 ("x"
                                                                                                                  "1+j!2"
                                                                                                                  "n0z"
                                                                                                                  "2"))
                                                                                                                (("2"
                                                                                                                  (assert)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("3"
                                                                                                  (expand
                                                                                                   "even?")
                                                                                                  (("3"
                                                                                                    (skosimp*)
                                                                                                    (("3"
                                                                                                      (lemma
                                                                                                       "div_cancel2"
                                                                                                       ("x"
                                                                                                        "j!2"
                                                                                                        "n0z"
                                                                                                        "2"))
                                                                                                      (("3"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("3"
                                                                                              (expand
                                                                                               "even?")
                                                                                              (("3"
                                                                                                (skosimp*)
                                                                                                (("3"
                                                                                                  (lemma
                                                                                                   "div_cancel2"
                                                                                                   ("x"
                                                                                                    "j!2"
                                                                                                    "n0z"
                                                                                                    "2"))
                                                                                                  (("3"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (skosimp)
                                                      (("3"
                                                        (skosimp)
                                                        (("3"
                                                          (hide-all-but
                                                           (-2 1))
                                                          (("3"
                                                            (expand
                                                             "even?")
                                                            (("3"
                                                              (skosimp)
                                                              (("3"
                                                                (lemma
                                                                 "div_cancel2"
                                                                 ("x"
                                                                  "j!1"
                                                                  "n0z"
                                                                  "2"))
                                                                (("3"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide-all-but
                                                   (1 -6 -7 -8))
                                                  (("2"
                                                    (expand
                                                     "bijective?")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (expand "PHI")
                                                        (("2"
                                                          (split)
                                                          (("1"
                                                            (expand
                                                             "injective?")
                                                            (("1"
                                                              (skosimp*)
                                                              (("1"
                                                                (case-replace
                                                                 "even?(x1!1)")
                                                                (("1"
                                                                  (case-replace
                                                                   "even?(x2!1)")
                                                                  (("1"
                                                                    (inst
                                                                     -6
                                                                     "x1!1/2"
                                                                     "x2!1/2")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (hide-all-but
                                                                       (-1
                                                                        1))
                                                                      (("2"
                                                                        (expand
                                                                         "even?")
                                                                        (("2"
                                                                          (skosimp)
                                                                          (("2"
                                                                            (lemma
                                                                             "div_cancel2"
                                                                             ("x"
                                                                              "j!1"
                                                                              "n0z"
                                                                              "2"))
                                                                            (("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("3"
                                                                      (hide-all-but
                                                                       (-2
                                                                        1))
                                                                      (("3"
                                                                        (expand
                                                                         "even?")
                                                                        (("3"
                                                                          (skosimp)
                                                                          (("3"
                                                                            (lemma
                                                                             "div_cancel2"
                                                                             ("x"
                                                                              "j!1"
                                                                              "n0z"
                                                                              "2"))
                                                                            (("3"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (expand
                                                                       "disjoint?")
                                                                      (("2"
                                                                        (expand
                                                                         "intersection")
                                                                        (("2"
                                                                          (expand
                                                                           "empty?")
                                                                          (("2"
                                                                            (expand
                                                                             "member")
                                                                            (("2"
                                                                              (inst
                                                                               -7
                                                                               "DX(x1!1 / 2)")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (expand
                                                                                 "even?")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (lemma
                                                                                     "div_cancel2"
                                                                                     ("x"
                                                                                      "j!1"
                                                                                      "n0z"
                                                                                      "2"))
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (case-replace
                                                                   "even?(x2!1)")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (expand
                                                                       "disjoint?")
                                                                      (("1"
                                                                        (expand
                                                                         "intersection")
                                                                        (("1"
                                                                          (expand
                                                                           "empty?")
                                                                          (("1"
                                                                            (expand
                                                                             "member")
                                                                            (("1"
                                                                              (inst
                                                                               -7
                                                                               "DX(x2!1 / 2)")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (expand
                                                                                 "even?")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (lemma
                                                                                     "div_cancel2"
                                                                                     ("x"
                                                                                      "j!1"
                                                                                      "n0z"
                                                                                      "2"))
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (inst
                                                                       -2
                                                                       "(x1!1 - 1) / 2"
                                                                       "(x2!1 - 1) / 2")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         (1
                                                                          2))
                                                                        (("2"
                                                                          (rewrite
                                                                           "even_or_odd")
                                                                          (("2"
                                                                            (expand
                                                                             "odd?")
                                                                            (("2"
                                                                              (skosimp)
                                                                              (("2"
                                                                                (lemma
                                                                                 "div_cancel2"
                                                                                 ("x"
                                                                                  "j!1"
                                                                                  "n0z"
                                                                                  "2"))
                                                                                (("2"
                                                                                  (assert)
                                                                                  (("2"
                                                                                    (replace
                                                                                     -2)
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("3"
                                                                        (hide-all-but
                                                                         (1
                                                                          3))
                                                                        (("3"
                                                                          (rewrite
                                                                           "even_or_odd")
                                                                          (("3"
                                                                            (expand
                                                                             "odd?")
                                                                            (("3"
                                                                              (skosimp*)
                                                                              (("3"
                                                                                (lemma
                                                                                 "div_cancel2"
                                                                                 ("x"
                                                                                  "j!1"
                                                                                  "n0z"
                                                                                  "2"))
                                                                                (("3"
                                                                                  (assert)
                                                                                  (("3"
                                                                                    (replace
                                                                                     -2)
                                                                                    (("3"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "surjective?")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (typepred
                                                                 "y!1")
                                                                (("2"
                                                                  (expand
                                                                   "union")
                                                                  (("2"
                                                                    (expand
                                                                     "member")
                                                                    (("2"
                                                                      (expand
                                                                       "disjoint?")
                                                                      (("2"
                                                                        (expand
                                                                         "intersection")
                                                                        (("2"
                                                                          (expand
                                                                           "empty?")
                                                                          (("2"
                                                                            (expand
                                                                             "member")
                                                                            (("2"
                                                                              (split
                                                                               -1)
                                                                              (("1"
                                                                                (inst
                                                                                 -5
                                                                                 "y!1")
                                                                                (("1"
                                                                                  (skosimp)
                                                                                  (("1"
                                                                                    (inst
                                                                                     +
                                                                                     "2*x!1")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (inst
                                                                                 -3
                                                                                 "y!1")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (inst
                                                                                     +
                                                                                     "2*x!1+1")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (lemma
                                                                                         "div_cancel2"
                                                                                         ("x"
                                                                                          "x!1"
                                                                                          "n0z"
                                                                                          "2"))
                                                                                        (("2"
                                                                                          (replace
                                                                                           -1)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (replace
                                                                                               -4)
                                                                                              (("2"
                                                                                                (lift-if
                                                                                                 1)
                                                                                                (("2"
                                                                                                  (prop)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "even?")
                                                                                                    (("2"
                                                                                                      (propax)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (skosimp)
                                                  (("3"
                                                    (expand "union")
                                                    (("3"
                                                      (expand "member")
                                                      (("3"
                                                        (expand "PHI")
                                                        (("3"
                                                          (hide-all-but
                                                           1)
                                                          (("3"
                                                            (prop)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil)
                                                             ("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (skosimp)
                                                (("2"
                                                  (hide-all-but (1 2))
                                                  (("2"
                                                    (rewrite
                                                     "even_or_odd")
                                                    (("2"
                                                      (expand "odd?")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (replace -1)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (lemma
                                                                 "div_cancel1"
                                                                 ("x"
                                                                  "j!1"
                                                                  "n0z"
                                                                  "2"))
                                                                (("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (typepred
                                                                     "n!1")
                                                                    (("2"
                                                                      (case
                                                                       "0 <= j!1")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (lemma
                                                                         "trich_lt"
                                                                         ("x"
                                                                          "j!1"
                                                                          "y"
                                                                          "-1"))
                                                                        (("2"
                                                                          (split
                                                                           -1)
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("3"
                                                                            (assert)
                                                                            (("3"
                                                                              (case
                                                                               "forall (i,j:int): i < j IFF i + 1 <= j")
                                                                              (("1"
                                                                                (inst
                                                                                 -
                                                                                 "-1"
                                                                                 "j!1")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (hide-all-but
                                                                                 1)
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (split)
                                                                                    (("1"
                                                                                      (flatten)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (flatten)
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (skosimp)
                                                (("3"
                                                  (hide-all-but (1 -1))
                                                  (("3"
                                                    (expand "even?")
                                                    (("3"
                                                      (skosimp)
                                                      (("3"
                                                        (replace -1)
                                                        (("3"
                                                          (lemma
                                                           "div_cancel1"
                                                           ("x"
                                                            "j!1"
                                                            "n0z"
                                                            "2"))
                                                          (("3"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp)
        (("2" (expand "convergent?")
          (("2" (typepred "X!1")
            (("2" (hide -3)
              (("2" (flatten)
                (("2" (split -3)
                  (("1" (lemma "finite_union" ("A" "X!1" "B" "Y!1"))
                    (("1" (propax) nil nil) ("2" (propax) nil nil))
                    nil)
                   ("2"
                    (lemma "denumerable_enumeration_bij" ("X" "Y!1"))
                    (("2"
                      (lemma "denumerable_enumeration_bij"
                       ("X" "union(X!1,Y!1)"))
                      (("2"
                        (lemma "infinite_union" ("S" "X!1" "R" "Y!1"))
                        (("2" (assert)
                          (("2"
                            (name-replace "DXY"
                             "denumerable_enumeration(union(X!1, Y!1))")
                            (("2"
                              (name-replace "DY"
                               "denumerable_enumeration(Y!1)")
                              (("2"
                                (expand "absconvergent?")
                                (("2"
                                  (lemma
                                   "bijective_inverse_exists[nat, (union(X!1, Y!1))]"
                                   ("f" "DXY"))
                                  (("1"
                                    (expand "exists1")
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (skolem - ("CXY"))
                                        (("1"
                                          (hide -2)
                                          (("1"
                                            (lemma
                                             "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]"
                                             ("f" "DXY" "g" "CXY"))
                                            (("1"
                                              (name "N" "card(X!1)")
                                              (("1"
                                                (lemma
                                                 "card_bij_inv"
                                                 ("S" "X!1" "N" "N"))
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (skolem - ("DX"))
                                                    (("1"
                                                      (name
                                                       "PHI"
                                                       "LAMBDA (n:nat): IF n < N THEN DX(n) ELSE DY(n-N) ENDIF")
                                                      (("1"
                                                        (case
                                                         "bijective?[nat, (union(X!1, Y!1))](PHI)")
                                                        (("1"
                                                          (lemma
                                                           "composition_bijective[nat,(union(X!1, Y!1)),nat]"
                                                           ("f1"
                                                            "PHI"
                                                            "f2"
                                                            "CXY"))
                                                          (("1"
                                                            (case
                                                             "absconvergent?(g!1 o PHI)")
                                                            (("1"
                                                              (lemma
                                                               "bijective_inverse_exists[nat,(union(X!1,Y!1))]"
                                                               ("f"
                                                                "PHI"))
                                                              (("1"
                                                                (expand
                                                                 "exists1")
                                                                (("1"
                                                                  (flatten)
                                                                  (("1"
                                                                    (skolem
                                                                     -
                                                                     ("PSI"))
                                                                    (("1"
                                                                      (lemma
                                                                       "bij_inv_is_bij_alt[nat,(union(X!1,Y!1))]"
                                                                       ("f"
                                                                        "PHI"
                                                                        "g"
                                                                        "PSI"))
                                                                      (("1"
                                                                        (lemma
                                                                         "composition_bijective[nat,(union(X!1,Y!1)),nat]"
                                                                         ("f1"
                                                                          "DXY"
                                                                          "f2"
                                                                          "PSI"))
                                                                        (("1"
                                                                          (lemma
                                                                           "abs_series_bij_conv_abs"
                                                                           ("aa"
                                                                            "abs(g!1 o PHI)"
                                                                            "phi"
                                                                            "PSI o DXY"))
                                                                          (("1"
                                                                            (expand
                                                                             "absconvergent?"
                                                                             -6)
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (lemma
                                                                                 "comp_inverse_right_alt[nat, (union(X!1, Y!1))]"
                                                                                 ("f"
                                                                                  "PHI"
                                                                                  "g"
                                                                                  "PSI"))
                                                                                (("1"
                                                                                  (case-replace
                                                                                   "abs(g!1 o PHI) o (PSI o DXY) = abs(g!1 o DXY)")
                                                                                  (("1"
                                                                                    (hide-all-but
                                                                                     (1
                                                                                      -1))
                                                                                    (("1"
                                                                                      (apply-extensionality
                                                                                       1
                                                                                       :hide?
                                                                                       t)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "o ")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "abs")
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "DXY(x!1)")
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (propax)
                                                                            nil
                                                                            nil)
                                                                           ("3"
                                                                            (hide-all-but
                                                                             (-5
                                                                              1))
                                                                            (("3"
                                                                              (expand
                                                                               "absconvergent?")
                                                                              (("3"
                                                                                (expand
                                                                                 "o ")
                                                                                (("3"
                                                                                  (case-replace
                                                                                   "abs(abs(LAMBDA (x: nat): g!1(PHI(x)))) = abs(LAMBDA (x: nat): g!1(PHI(x)))")
                                                                                  (("3"
                                                                                    (hide-all-but
                                                                                     1)
                                                                                    (("3"
                                                                                      (apply-extensionality
                                                                                       1
                                                                                       :hide?
                                                                                       t)
                                                                                      (("3"
                                                                                        (expand
                                                                                         "abs")
                                                                                        (("3"
                                                                                          (grind)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (propax)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "absconvergent?")
                                                              (("2"
                                                                (lemma
                                                                 "conv_series_shift"
                                                                 ("N"
                                                                  "N"))
                                                                (("2"
                                                                  (inst
                                                                   -
                                                                   "abs(g!1 o PHI)")
                                                                  (("2"
                                                                    (replace
                                                                     -1
                                                                     1)
                                                                    (("2"
                                                                      (case-replace
                                                                       "(LAMBDA n: abs(g!1 o PHI)(n + N)) = abs(g!1 o DY)")
                                                                      (("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (apply-extensionality
                                                                           :hide?
                                                                           t)
                                                                          (("2"
                                                                            (expand
                                                                             "abs")
                                                                            (("2"
                                                                              (expand
                                                                               "o ")
                                                                              (("2"
                                                                                (expand
                                                                                 "abs")
                                                                                (("2"
                                                                                  (expand
                                                                                   "PHI")
                                                                                  (("2"
                                                                                    (propax)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide-all-but
                                                           (-2
                                                            -7
                                                            -10
                                                            1))
                                                          (("2"
                                                            (expand
                                                             "bijective?")
                                                            (("2"
                                                              (flatten)
                                                              (("2"
                                                                (split)
                                                                (("1"
                                                                  (expand
                                                                   "injective?")
                                                                  (("1"
                                                                    (skosimp)
                                                                    (("1"
                                                                      (expand
                                                                       "PHI")
                                                                      (("1"
                                                                        (case-replace
                                                                         "x1!1<N")
                                                                        (("1"
                                                                          (case-replace
                                                                           "x2!1 < N")
                                                                          (("1"
                                                                            (inst
                                                                             -4
                                                                             "x1!1"
                                                                             "x2!1")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (typepred
                                                                               "DX(x1!1)")
                                                                              (("2"
                                                                                (typepred
                                                                                 "DY(x2!1-N)")
                                                                                (("2"
                                                                                  (expand
                                                                                   "disjoint?")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "intersection")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "empty?")
                                                                                      (("2"
                                                                                        (expand
                                                                                         "member")
                                                                                        (("2"
                                                                                          (inst
                                                                                           -9
                                                                                           "DX(x1!1)")
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (case-replace
                                                                           "x2!1<N")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (expand
                                                                               "disjoint?")
                                                                              (("1"
                                                                                (expand
                                                                                 "intersection")
                                                                                (("1"
                                                                                  (expand
                                                                                   "empty?")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("1"
                                                                                      (inst
                                                                                       -7
                                                                                       "DX(x2!1)")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (inst
                                                                               -4
                                                                               "x1!1-N"
                                                                               "x2!1-N")
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (expand
                                                                   "surjective?")
                                                                  (("2"
                                                                    (skosimp)
                                                                    (("2"
                                                                      (typepred
                                                                       "y!1")
                                                                      (("2"
                                                                        (expand
                                                                         "union")
                                                                        (("2"
                                                                          (expand
                                                                           "member")
                                                                          (("2"
                                                                            (split
                                                                             -1)
                                                                            (("1"
                                                                              (inst
                                                                               -3
                                                                               "y!1")
                                                                              (("1"
                                                                                (skosimp)
                                                                                (("1"
                                                                                  (inst
                                                                                   +
                                                                                   "x!1")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "PHI")
                                                                                    (("1"
                                                                                      (propax)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (inst
                                                                               -5
                                                                               "y!1")
                                                                              (("2"
                                                                                (skosimp)
                                                                                (("2"
                                                                                  (inst
                                                                                   +
                                                                                   "N+x!1")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "PHI")
                                                                                    (("2"
                                                                                      (propax)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("3"
                                                          (skosimp)
                                                          (("3"
                                                            (expand
                                                             "PHI")
                                                            (("3"
                                                              (expand
                                                               "union")
                                                              (("3"
                                                                (expand
                                                                 "member")
                                                                (("3"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (skosimp)
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2)
      (("3" (skosimp) (("3" (rewrite "countable_union") nil nil)) nil))
      nil)
     ("4" (skosimp)
      (("4" (assert)
        (("4" (typepred "X!1")
          (("4" (lemma "finite_countable" ("x" "X!1"))
            (("4" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_union judgement-tcc nil finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (below type-eq-decl nil nat_types nil)
    (X!1 skolem-const-decl "finite_set[T]" countable_convergence nil)
    (Y!1 skolem-const-decl "countable_set[T]" countable_convergence
     nil)
    (y!1 skolem-const-decl "(union(X!1, Y!1))" countable_convergence
     nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (PHI skolem-const-decl "[nat -> T]" countable_convergence nil)
    (conv_series_shift formula-decl nil series "series/")
    (card_bij_inv formula-decl nil finite_sets nil)
    (infinite_union formula-decl nil infinite_sets_def nil)
    (X!1 skolem-const-decl "countable_set[T]" countable_convergence
     nil)
    (intersection_commutative formula-decl nil sets_lemmas nil)
    (countable_intersection1 application-judgement "countable_set[T]"
     countable_convergence nil)
    (union_commutative formula-decl nil sets_lemmas nil)
    (Y!1 skolem-const-decl "countable_set[T]" countable_convergence
     nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (exists1 const-decl "bool" exists1 nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (even? const-decl "bool" integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (x2!1 skolem-const-decl "nat" countable_convergence nil)
    (x1!1 skolem-const-decl "nat" countable_convergence nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (injective? const-decl "bool" functions nil)
    (y!1 skolem-const-decl "(union(X!1, Y!1))" countable_convergence
     nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (surjective? const-decl "bool" functions nil)
    (j!1 skolem-const-decl "int" countable_convergence nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (j!1 skolem-const-decl "int" countable_convergence nil)
    (odd? const-decl "bool" integers nil)
    (series_sum_conv formula-decl nil series "series/")
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (comp_inverse_right_alt formula-decl nil function_inverse_def nil)
    (abs_series_bij_conv_abs formula-decl nil absconv_series "series/")
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (PHI skolem-const-decl "[nat -> T]" countable_convergence nil)
    (even_or_odd formula-decl nil naturalnumbers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (extensionality formula-decl nil functions nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (abs const-decl "sequence[real]" series "series/")
    (O const-decl "T3" function_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (convergence const-decl "bool" convergence_sequences "analysis/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (T_low type-eq-decl nil sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (sigma def-decl "real" sigma "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (j!1 skolem-const-decl "int" countable_convergence nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (j!1 skolem-const-decl "int" countable_convergence nil)
    (pred type-eq-decl nil defined_types nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (sigma_0_neg formula-decl nil sigma_nat "reals/")
    (even_plus_even_is_even application-judgement "even_int" integers
     nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (series const-decl "sequence[real]" series "series/")
    (convergent? const-decl "bool" convergence_sequences "analysis/")
    (sequence type-eq-decl nil sequences nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (trich_lt formula-decl nil real_props nil)
    (div_cancel1 formula-decl nil real_props nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (bijective? const-decl "bool" functions nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (denumerable_enumeration_bij formula-decl nil
     denumerable_enumeration nil)
    (countable_union application-judgement "countable_set[T]"
     countable_convergence nil)
    (T formal-type-decl nil countable_convergence nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (disjoint? const-decl "bool" sets nil)
    (convergent? const-decl "bool" countable_convergence nil)
    (union const-decl "set" sets nil))
   nil)
  (convergent_disjoint_union-1 nil 3351593524
   (""
    (case "FORALL (X:finite_set[T], Y: countable_set[T], g: [T -> real]):
        disjoint?(X, Y) AND convergent?(X)(g) AND convergent?(Y)(g) IMPLIES
         convergent?(union(X, Y))(g)")
    (("1" (skosimp)
      (("1" (expand "convergent?")
        (("1" (case-replace "is_finite(X!1)")
          (("1" (inst - "X!1" "Y!1" "g!1")
            (("1" (replace -4) (("1" (assert) nil nil)) nil)) nil)
           ("2" (assert)
            (("2" (case-replace "is_finite(Y!1)")
              (("1" (inst - "Y!1" "X!1" "g!1")
                (("1" (assert)
                  (("1" (split -2)
                    (("1" (rewrite "union_commutative")
                      (("1" (assert) nil nil)) nil)
                     ("2" (rewrite "union_commutative")
                      (("2" (assert) nil nil)) nil)
                     ("3" (hide-all-but (-2 1))
                      (("3" (expand "disjoint?")
                        (("3" (rewrite "intersection_commutative") nil
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (flatten)
                (("2" (assert)
                  (("2" (hide -1)
                    (("2" (expand "absconvergent?")
                      (("2"
                        (lemma "denumerable_enumeration_bij"
                         ("X" "X!1"))
                        (("2"
                          (lemma "denumerable_enumeration_bij"
                           ("X" "Y!1"))
                          (("2"
                            (lemma "denumerable_enumeration_bij"
                             ("X" "union(X!1,Y!1)"))
                            (("2"
                              (name-replace "DX"
                               "denumerable_enumeration(X!1)")
                              (("2"
                                (name-replace
                                 "DY"
                                 "denumerable_enumeration(Y!1)")
                                (("2"
                                  (name-replace
                                   "DXY"
                                   "denumerable_enumeration(union(X!1,Y!1))")
                                  (("2"
                                    (lemma
                                     "bijective_inverse_exists[nat, (union(X!1, Y!1))]"
                                     ("f" "DXY"))
                                    (("1"
                                      (expand "exists1")
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (skolem - ("CXY"))
                                          (("1"
                                            (lemma
                                             "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]"
                                             ("f" "DXY" "g" "CXY"))
                                            (("1"
                                              (name
                                               "PHI"
                                               "LAMBDA (n:nat): IF even?(n) THEN DX(n/2) ELSE DY((n-1)/2) ENDIF")
                                              (("1"
                                                (case
                                                 "bijective?[nat, (union(X!1, Y!1))](PHI)")
                                                (("1"
                                                  (hide -2)
                                                  (("1"
                                                    (case
                                                     "forall (a:sequence[real]): convergent(series(a)) => convergent(series(LAMBDA (n:nat): IF even?(n) THEN a(n/2) ELSE 0 ENDIF))")
                                                    (("1"
                                                      (case
                                                       "FORALL (a: sequence[real]):
        convergent(series(a)) =>
         convergent(series(LAMBDA (n: nat):
                             IF odd?(n) THEN a((n-1)/2) ELSE 0 ENDIF))")
                                                      (("1"
                                                        (inst
                                                         -
                                                         "abs(g!1 o DY)")
                                                        (("1"
                                                          (inst
                                                           -
                                                           "abs(g!1 o DX)")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (lemma
                                                               "series_sum_conv"
                                                               ("a"
                                                                "(LAMBDA (n: nat):
                          IF even?(n) THEN abs(g!1 o DX)(n / 2)
                          ELSE 0
                          ENDIF)"
                                                                "b"
                                                                "(LAMBDA (n: nat):
                          IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)
                          ELSE 0
                          ENDIF)"))
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (hide
                                                                   -2
                                                                   -3)
                                                                  (("1"
                                                                    (lemma
                                                                     "extensionality"
                                                                     ("f"
                                                                      "((LAMBDA (n: nat):
                           IF even?(n) THEN abs(g!1 o DX)(n / 2)
                           ELSE 0
                           ENDIF)
                         +
                         (LAMBDA (n: nat):
                            IF odd?(n) THEN abs(g!1 o DY)((n - 1) / 2)
                            ELSE 0
                            ENDIF))"
                                                                      "g"
                                                                      "abs(g!1 o PHI)"))
                                                                    (("1"
                                                                      (split
                                                                       -1)
                                                                      (("1"
                                                                        (replace
                                                                         -1)
                                                                        (("1"
                                                                          (hide
                                                                           -1)
                                                                          (("1"
                                                                            (lemma
                                                                             "bijective_inverse_exists[nat, (union(X!1, Y!1))]"
                                                                             ("f"
                                                                              "PHI"))
                                                                            (("1"
                                                                              (expand
                                                                               "exists1")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (skolem
                                                                                   -
                                                                                   ("PSI"))
                                                                                  (("1"
                                                                                    (hide
                                                                                     -7
                                                                                     -2)
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]"
                                                                                       ("f"
                                                                                        "PHI"
                                                                                        "g"
                                                                                        "PSI"))
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "composition_bijective[nat,(union(X!1, Y!1)),nat]"
                                                                                         ("f2"
                                                                                          "PSI"
                                                                                          "f1"
                                                                                          "DXY"))
                                                                                        (("1"
                                                                                          (lemma
                                                                                           "comp_inverse_right_alt[nat, (union(X!1, Y!1))]"
                                                                                           ("f"
                                                                                            "PHI"
                                                                                            "g"
                                                                                            "PSI"))
                                                                                          (("1"
                                                                                            (hide-all-but
                                                                                             (-1
                                                                                              -2
                                                                                              -5
                                                                                              4))
                                                                                            (("1"
                                                                                              (lemma
                                                                                               "abs_series_bij_conv_abs"
                                                                                               ("phi"
                                                                                                "PSI o DXY"
                                                                                                "aa"
                                                                                                "abs(g!1 o PHI)"))
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (case-replace
                                                                                                   "abs(g!1 o PHI) o (PSI o DXY) = abs(g!1 o DXY)")
                                                                                                  (("1"
                                                                                                    (hide-all-but
                                                                                                     (-2
                                                                                                      1))
                                                                                                    (("1"
                                                                                                      (apply-extensionality
                                                                                                       1
                                                                                                       :hide?
                                                                                                       t)
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "o")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           "abs")
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "DXY(x!1)")
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (propax)
                                                                                                nil
                                                                                                nil)
                                                                                               ("3"
                                                                                                (expand
                                                                                                 "absconvergent?")
                                                                                                (("3"
                                                                                                  (hide-all-but
                                                                                                   (-3
                                                                                                    1))
                                                                                                  (("3"
                                                                                                    (case-replace
                                                                                                     "abs(abs(o[nat, T, real](g!1, PHI))) = abs(g!1 o PHI)")
                                                                                                    (("3"
                                                                                                      (hide-all-but
                                                                                                       1)
                                                                                                      (("3"
                                                                                                        (apply-extensionality
                                                                                                         :hide?
                                                                                                         t)
                                                                                                        (("3"
                                                                                                          (expand
                                                                                                           "abs")
                                                                                                          (("3"
                                                                                                            (expand
                                                                                                             "o ")
                                                                                                            (("3"
                                                                                                              (grind)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (propax)
                                                                                          nil
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (propax)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (skosimp)
                                                                          (("2"
                                                                            (expand
                                                                             "+")
                                                                            (("2"
                                                                              (expand
                                                                               "PHI")
                                                                              (("2"
                                                                                (expand
                                                                                 "abs")
                                                                                (("2"
                                                                                  (expand
                                                                                   "o")
                                                                                  (("2"
                                                                                    (case-replace
                                                                                     "even?(x!1)")
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "even_or_odd"
                                                                                       ("x"
                                                                                        "x!1"))
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (lemma
                                                                                       "even_or_odd"
                                                                                       ("x"
                                                                                        "x!1"))
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide-all-but
                                                                       1)
                                                                      (("2"
                                                                        (expand
                                                                         "even?")
                                                                        (("2"
                                                                          (skosimp*)
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 1)
                                                                (("2"
                                                                  (expand
                                                                   "odd?")
                                                                  (("2"
                                                                    (skosimp*)
                                                                    (("2"
                                                                      (assert)
                                                                      (("2"
                                                                        (replace
                                                                         -1)
                                                                        (("2"
                                                                          (assert)
                                                                          (("2"
                                                                            (case
                                                                             "forall (i,j:int):i<j=>i+1<=j")
                                                                            (("1"
                                                                              (inst
                                                                               -
                                                                               "-1"
                                                                               "j!1")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (hide-all-but
                                                                               1)
                                                                              (("2"
                                                                                (grind)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("3"
                                                                (hide-all-but
                                                                 1)
                                                                (("3"
                                                                  (expand
                                                                   "even?")
                                                                  (("3"
                                                                    (skosimp*)
                                                                    (("3"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide-all-but
                                                         1)
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (expand
                                                             "convergent")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (inst
                                                                 +
                                                                 "l!1")
                                                                (("2"
                                                                  (expand
                                                                   "convergence")
                                                                  (("2"
                                                                    (skosimp)
                                                                    (("2"
                                                                      (inst
                                                                       -
                                                                       "epsilon!1")
                                                                      (("2"
                                                                        (skosimp)
                                                                        (("2"
                                                                          (case
                                                                           "FORALL (m: nat):
        sigma(0, m, a!1) =
         sigma(0, 2 * m + 1,
               LAMBDA (n: nat):
                 IF odd?(n) THEN a!1((n - 1) / 2) ELSE 0 ENDIF)")
                                                                          (("1"
                                                                            (inst
                                                                             +
                                                                             "2*n!1+1")
                                                                            (("1"
                                                                              (skosimp)
                                                                              (("1"
                                                                                (case
                                                                                 "even?(i!1)")
                                                                                (("1"
                                                                                  (expand
                                                                                   "even?")
                                                                                  (("1"
                                                                                    (skosimp)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "series")
                                                                                      (("1"
                                                                                        (replace
                                                                                         -1)
                                                                                        (("1"
                                                                                          (case-replace
                                                                                           "j!1=0")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("2"
                                                                                            (inst
                                                                                             -
                                                                                             "j!1-1")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "j!1-1")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (replace
                                                                                                   -2
                                                                                                   -3)
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "sigma"
                                                                                                     2)
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "odd?"
                                                                                                       2
                                                                                                       1)
                                                                                                      (("1"
                                                                                                        (propax)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (rewrite
                                                                                   "even_or_odd"
                                                                                   1)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "odd?"
                                                                                     -1)
                                                                                    (("2"
                                                                                      (skosimp)
                                                                                      (("2"
                                                                                        (replace
                                                                                         -1)
                                                                                        (("2"
                                                                                          (inst
                                                                                           -3
                                                                                           "j!1")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "j!1")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "series")
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (hide-all-but
                                                                             1)
                                                                            (("2"
                                                                              (induct
                                                                               "m")
                                                                              (("1"
                                                                                (expand
                                                                                 "sigma")
                                                                                (("1"
                                                                                  (expand
                                                                                   "sigma")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "odd?")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (skosimp*)
                                                                                (("2"
                                                                                  (expand
                                                                                   "sigma"
                                                                                   1)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "sigma"
                                                                                     1
                                                                                     2)
                                                                                    (("2"
                                                                                      (replace
                                                                                       -1
                                                                                       1
                                                                                       rl)
                                                                                      (("2"
                                                                                        (hide
                                                                                         -1)
                                                                                        (("2"
                                                                                          (assert)
                                                                                          (("2"
                                                                                            (expand
                                                                                             "odd?")
                                                                                            (("2"
                                                                                              (lemma
                                                                                               "div_cancel2"
                                                                                               ("x"
                                                                                                "1+j!1"
                                                                                                "n0z"
                                                                                                "2"))
                                                                                              (("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("3"
                                                                                (hide
                                                                                 2)
                                                                                (("3"
                                                                                  (expand
                                                                                   "odd?")
                                                                                  (("3"
                                                                                    (skosimp*)
                                                                                    (("3"
                                                                                      (replace
                                                                                       -1)
                                                                                      (("3"
                                                                                        (assert)
                                                                                        (("3"
                                                                                          (case
                                                                                           "forall (i,j:int):i<j=>i+1<=j")
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "-1"
                                                                                             "j!1")
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             1)
                                                                                            (("2"
                                                                                              (grind)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("3"
                                                                            (hide-all-but
                                                                             1)
                                                                            (("3"
                                                                              (expand
                                                                               "odd?")
                                                                              (("3"
                                                                                (skosimp*)
                                                                                (("3"
                                                                                  (assert)
                                                                                  (("3"
                                                                                    (assert)
                                                                                    (("3"
                                                                                      (case
                                                                                       "forall (i,j:int):i<j=>i+1<=j")
                                                                                      (("1"
                                                                                        (inst
                                                                                         -
                                                                                         "-1"
                                                                                         "j!1")
                                                                                        (("1"
                                                                                          (assert)
                                                                                          nil
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (hide-all-but
                                                                                         1)
                                                                                        (("2"
                                                                                          (grind)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("3"
                                                        (skosimp*)
                                                        (("3"
                                                          (hide-all-but
                                                           (-2 1))
                                                          (("3"
                                                            (expand
                                                             "odd?")
                                                            (("3"
                                                              (skosimp)
                                                              (("3"
                                                                (replace
                                                                 -1)
                                                                (("3"
                                                                  (assert)
                                                                  (("3"
                                                                    (typepred
                                                                     "n!1")
                                                                    (("3"
                                                                      (case
                                                                       "forall (i,j:int): i<j => i+1<=j")
                                                                      (("1"
                                                                        (inst
                                                                         -
                                                                         "-1"
                                                                         "j!1")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (skosimp)
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide-all-but 1)
                                                      (("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (expand
                                                           "convergent")
                                                          (("2"
                                                            (skosimp)
                                                            (("2"
                                                              (inst
                                                               +
                                                               "l!1")
                                                              (("2"
                                                                (expand
                                                                 "convergence")
                                                                (("2"
                                                                  (skosimp*)
                                                                  (("2"
                                                                    (inst
                                                                     -
                                                                     "epsilon!1")
                                                                    (("2"
                                                                      (skosimp)
                                                                      (("2"
                                                                        (inst
                                                                         +
                                                                         "2*n!1")
                                                                        (("2"
                                                                          (skosimp)
                                                                          (("2"
                                                                            (case
                                                                             "even?(i!1)")
                                                                            (("1"
                                                                              (expand
                                                                               "even?"
                                                                               -1)
                                                                              (("1"
                                                                                (skosimp)
                                                                                (("1"
                                                                                  (replace
                                                                                   -1)
                                                                                  (("1"
                                                                                    (inst
                                                                                     -
                                                                                     "j!1")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "series")
                                                                                        (("1"
                                                                                          (case
                                                                                           "forall (m:nat): sigma(0, m, a!1) = sigma(0, 2*m,
                LAMBDA (n: nat):
                  IF even?(n) THEN a!1(n / 2) ELSE 0 ENDIF)")
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "j!1")
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             1)
                                                                                            (("2"
                                                                                              (induct
                                                                                               "m")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "sigma")
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (skosimp)
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "sigma"
                                                                                                   1)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "sigma"
                                                                                                     1
                                                                                                     2)
                                                                                                    (("2"
                                                                                                      (lemma
                                                                                                       "div_cancel2"
                                                                                                       ("x"
                                                                                                        "1+j!1"
                                                                                                        "n0z"
                                                                                                        "2"))
                                                                                                      (("2"
                                                                                                        (assert)
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "even?"
                                                                                                           1
                                                                                                           1)
                                                                                                          (("2"
                                                                                                            (replace
                                                                                                             -2
                                                                                                             1
                                                                                                             rl)
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("3"
                                                                                                (expand
                                                                                                 "even?")
                                                                                                (("3"
                                                                                                  (skosimp*)
                                                                                                  (("3"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("3"
                                                                                            (expand
                                                                                             "even?")
                                                                                            (("3"
                                                                                              (skosimp*)
                                                                                              (("3"
                                                                                                (lemma
                                                                                                 "div_cancel2"
                                                                                                 ("x"
                                                                                                  "j!2"
                                                                                                  "n0z"
                                                                                                  "2"))
                                                                                                (("3"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (rewrite
                                                                               "even_or_odd"
                                                                               1)
                                                                              (("2"
                                                                                (expand
                                                                                 "odd?")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (replace
                                                                                     -1)
                                                                                    (("2"
                                                                                      (inst
                                                                                       -
                                                                                       "j!1")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (expand
                                                                                           "series")
                                                                                          (("1"
                                                                                            (case
                                                                                             "forall (m:nat): sigma(0,m,a!1) = sigma(0,1+2*m,LAMBDA (n:nat): IF even?(n) THEN a!1(n/2) ELSE 0 ENDIF)")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "j!1")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (hide-all-but
                                                                                               1)
                                                                                              (("2"
                                                                                                (induct
                                                                                                 "m")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "sigma")
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "sigma")
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "even?")
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (skosimp*)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "sigma"
                                                                                                     1)
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "sigma"
                                                                                                       1
                                                                                                       2)
                                                                                                      (("2"
                                                                                                        (replace
                                                                                                         -1
                                                                                                         1
                                                                                                         rl)
                                                                                                        (("2"
                                                                                                          (assert)
                                                                                                          (("2"
                                                                                                            (hide
                                                                                                             -1)
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "even?")
                                                                                                              (("2"
                                                                                                                (lemma
                                                                                                                 "div_cancel2"
                                                                                                                 ("x"
                                                                                                                  "1+j!2"
                                                                                                                  "n0z"
                                                                                                                  "2"))
                                                                                                                (("2"
                                                                                                                  (assert)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("3"
                                                                                                  (expand
                                                                                                   "even?")
                                                                                                  (("3"
                                                                                                    (skosimp*)
                                                                                                    (("3"
                                                                                                      (lemma
                                                                                                       "div_cancel2"
                                                                                                       ("x"
                                                                                                        "j!2"
                                                                                                        "n0z"
                                                                                                        "2"))
                                                                                                      (("3"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("3"
                                                                                              (expand
                                                                                               "even?")
                                                                                              (("3"
                                                                                                (skosimp*)
                                                                                                (("3"
                                                                                                  (lemma
                                                                                                   "div_cancel2"
                                                                                                   ("x"
                                                                                                    "j!2"
                                                                                                    "n0z"
                                                                                                    "2"))
                                                                                                  (("3"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (skosimp)
                                                      (("3"
                                                        (skosimp)
                                                        (("3"
                                                          (hide-all-but
                                                           (-2 1))
                                                          (("3"
                                                            (expand
                                                             "even?")
                                                            (("3"
                                                              (skosimp)
                                                              (("3"
                                                                (lemma
                                                                 "div_cancel2"
                                                                 ("x"
                                                                  "j!1"
                                                                  "n0z"
                                                                  "2"))
                                                                (("3"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide-all-but
                                                   (1 -6 -7 -8))
                                                  (("2"
                                                    (expand
                                                     "bijective?")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (expand "PHI")
                                                        (("2"
                                                          (split)
                                                          (("1"
                                                            (expand
                                                             "injective?")
                                                            (("1"
                                                              (skosimp*)
                                                              (("1"
                                                                (case-replace
                                                                 "even?(x1!1)")
                                                                (("1"
                                                                  (case-replace
                                                                   "even?(x2!1)")
                                                                  (("1"
                                                                    (inst
                                                                     -6
                                                                     "x1!1/2"
                                                                     "x2!1/2")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (hide-all-but
                                                                       (-1
                                                                        1))
                                                                      (("2"
                                                                        (expand
                                                                         "even?")
                                                                        (("2"
                                                                          (skosimp)
                                                                          (("2"
                                                                            (lemma
                                                                             "div_cancel2"
                                                                             ("x"
                                                                              "j!1"
                                                                              "n0z"
                                                                              "2"))
                                                                            (("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("3"
                                                                      (hide-all-but
                                                                       (-2
                                                                        1))
                                                                      (("3"
                                                                        (expand
                                                                         "even?")
                                                                        (("3"
                                                                          (skosimp)
                                                                          (("3"
                                                                            (lemma
                                                                             "div_cancel2"
                                                                             ("x"
                                                                              "j!1"
                                                                              "n0z"
                                                                              "2"))
                                                                            (("3"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (expand
                                                                       "disjoint?")
                                                                      (("2"
                                                                        (expand
                                                                         "intersection")
                                                                        (("2"
                                                                          (expand
                                                                           "empty?")
                                                                          (("2"
                                                                            (expand
                                                                             "member")
                                                                            (("2"
                                                                              (inst
                                                                               -7
                                                                               "DX(x1!1 / 2)")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (expand
                                                                                 "even?")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (lemma
                                                                                     "div_cancel2"
                                                                                     ("x"
                                                                                      "j!1"
                                                                                      "n0z"
                                                                                      "2"))
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (case-replace
                                                                   "even?(x2!1)")
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (expand
                                                                       "disjoint?")
                                                                      (("1"
                                                                        (expand
                                                                         "intersection")
                                                                        (("1"
                                                                          (expand
                                                                           "empty?")
                                                                          (("1"
                                                                            (expand
                                                                             "member")
                                                                            (("1"
                                                                              (inst
                                                                               -7
                                                                               "DX(x2!1 / 2)")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (expand
                                                                                 "even?")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (lemma
                                                                                     "div_cancel2"
                                                                                     ("x"
                                                                                      "j!1"
                                                                                      "n0z"
                                                                                      "2"))
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (inst
                                                                       -2
                                                                       "(x1!1 - 1) / 2"
                                                                       "(x2!1 - 1) / 2")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         (1
                                                                          2))
                                                                        (("2"
                                                                          (rewrite
                                                                           "even_or_odd")
                                                                          (("2"
                                                                            (expand
                                                                             "odd?")
                                                                            (("2"
                                                                              (skosimp)
                                                                              (("2"
                                                                                (lemma
                                                                                 "div_cancel2"
                                                                                 ("x"
                                                                                  "j!1"
                                                                                  "n0z"
                                                                                  "2"))
                                                                                (("2"
                                                                                  (assert)
                                                                                  (("2"
                                                                                    (replace
                                                                                     -2)
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("3"
                                                                        (hide-all-but
                                                                         (1
                                                                          3))
                                                                        (("3"
                                                                          (rewrite
                                                                           "even_or_odd")
                                                                          (("3"
                                                                            (expand
                                                                             "odd?")
                                                                            (("3"
                                                                              (skosimp*)
                                                                              (("3"
                                                                                (lemma
                                                                                 "div_cancel2"
                                                                                 ("x"
                                                                                  "j!1"
                                                                                  "n0z"
                                                                                  "2"))
                                                                                (("3"
                                                                                  (assert)
                                                                                  (("3"
                                                                                    (replace
                                                                                     -2)
                                                                                    (("3"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (expand
                                                             "surjective?")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (typepred
                                                                 "y!1")
                                                                (("2"
                                                                  (expand
                                                                   "union")
                                                                  (("2"
                                                                    (expand
                                                                     "member")
                                                                    (("2"
                                                                      (expand
                                                                       "disjoint?")
                                                                      (("2"
                                                                        (expand
                                                                         "intersection")
                                                                        (("2"
                                                                          (expand
                                                                           "empty?")
                                                                          (("2"
                                                                            (expand
                                                                             "member")
                                                                            (("2"
                                                                              (split
                                                                               -1)
                                                                              (("1"
                                                                                (inst
                                                                                 -5
                                                                                 "y!1")
                                                                                (("1"
                                                                                  (skosimp)
                                                                                  (("1"
                                                                                    (inst
                                                                                     +
                                                                                     "2*x!1")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (inst
                                                                                 -3
                                                                                 "y!1")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (inst
                                                                                     +
                                                                                     "2*x!1+1")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (lemma
                                                                                         "div_cancel2"
                                                                                         ("x"
                                                                                          "x!1"
                                                                                          "n0z"
                                                                                          "2"))
                                                                                        (("2"
                                                                                          (replace
                                                                                           -1)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (replace
                                                                                               -4)
                                                                                              (("2"
                                                                                                (lift-if
                                                                                                 1)
                                                                                                (("2"
                                                                                                  (prop)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "even?")
                                                                                                    (("2"
                                                                                                      (propax)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (skosimp)
                                                  (("3"
                                                    (expand "union")
                                                    (("3"
                                                      (expand "member")
                                                      (("3"
                                                        (expand "PHI")
                                                        (("3"
                                                          (hide-all-but
                                                           1)
                                                          (("3"
                                                            (prop)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil)
                                                             ("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (skosimp)
                                                (("2"
                                                  (hide-all-but (1 2))
                                                  (("2"
                                                    (rewrite
                                                     "even_or_odd")
                                                    (("2"
                                                      (expand "odd?")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (replace -1)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (lemma
                                                                 "div_cancel1"
                                                                 ("x"
                                                                  "j!1"
                                                                  "n0z"
                                                                  "2"))
                                                                (("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (typepred
                                                                     "n!1")
                                                                    (("2"
                                                                      (case
                                                                       "0 <= j!1")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (lemma
                                                                         "trich_lt"
                                                                         ("x"
                                                                          "j!1"
                                                                          "y"
                                                                          "-1"))
                                                                        (("2"
                                                                          (split
                                                                           -1)
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("3"
                                                                            (assert)
                                                                            (("3"
                                                                              (case
                                                                               "forall (i,j:int): i < j IFF i + 1 <= j")
                                                                              (("1"
                                                                                (inst
                                                                                 -
                                                                                 "-1"
                                                                                 "j!1")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (hide-all-but
                                                                                 1)
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (split)
                                                                                    (("1"
                                                                                      (flatten)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (flatten)
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (skosimp)
                                                (("3"
                                                  (hide-all-but (1 -1))
                                                  (("3"
                                                    (expand "even?")
                                                    (("3"
                                                      (skosimp)
                                                      (("3"
                                                        (replace -1)
                                                        (("3"
                                                          (lemma
                                                           "div_cancel1"
                                                           ("x"
                                                            "j!1"
                                                            "n0z"
                                                            "2"))
                                                          (("3"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp)
        (("2" (expand "convergent?")
          (("2" (typepred "X!1")
            (("2" (hide -3)
              (("2" (flatten)
                (("2" (split -3)
                  (("1" (lemma "finite_union" ("A" "X!1" "B" "Y!1"))
                    (("1" (propax) nil nil) ("2" (propax) nil nil))
                    nil)
                   ("2"
                    (lemma "denumerable_enumeration_bij" ("X" "Y!1"))
                    (("2"
                      (lemma "denumerable_enumeration_bij"
                       ("X" "union(X!1,Y!1)"))
                      (("2"
                        (lemma "infinite_union" ("S" "X!1" "R" "Y!1"))
                        (("2" (assert)
                          (("2"
                            (name-replace "DXY"
                             "denumerable_enumeration(union(X!1, Y!1))")
                            (("2"
                              (name-replace "DY"
                               "denumerable_enumeration(Y!1)")
                              (("2"
                                (expand "absconvergent?")
                                (("2"
                                  (lemma
                                   "bijective_inverse_exists[nat, (union(X!1, Y!1))]"
                                   ("f" "DXY"))
                                  (("1"
                                    (expand "exists1")
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (skolem - ("CXY"))
                                        (("1"
                                          (hide -2)
                                          (("1"
                                            (lemma
                                             "bij_inv_is_bij_alt[nat, (union(X!1, Y!1))]"
                                             ("f" "DXY" "g" "CXY"))
                                            (("1"
                                              (name "N" "card(X!1)")
                                              (("1"
                                                (lemma
                                                 "card_bij_inv"
                                                 ("S" "X!1" "N" "N"))
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (skolem - ("DX"))
                                                    (("1"
                                                      (name
                                                       "PHI"
                                                       "LAMBDA (n:nat): IF n < N THEN DX(n) ELSE DY(n-N) ENDIF")
                                                      (("1"
                                                        (case
                                                         "bijective?[nat, (union(X!1, Y!1))](PHI)")
                                                        (("1"
                                                          (lemma
                                                           "composition_bijective[nat,(union(X!1, Y!1)),nat]"
                                                           ("f1"
                                                            "PHI"
                                                            "f2"
                                                            "CXY"))
                                                          (("1"
                                                            (case
                                                             "absconvergent?(g!1 o PHI)")
                                                            (("1"
                                                              (lemma
                                                               "bijective_inverse_exists[nat,(union(X!1,Y!1))]"
                                                               ("f"
                                                                "PHI"))
                                                              (("1"
                                                                (expand
                                                                 "exists1")
                                                                (("1"
                                                                  (flatten)
                                                                  (("1"
                                                                    (skolem
                                                                     -
                                                                     ("PSI"))
                                                                    (("1"
                                                                      (lemma
                                                                       "bij_inv_is_bij_alt[nat,(union(X!1,Y!1))]"
                                                                       ("f"
                                                                        "PHI"
                                                                        "g"
                                                                        "PSI"))
                                                                      (("1"
                                                                        (lemma
                                                                         "composition_bijective[nat,(union(X!1,Y!1)),nat]"
                                                                         ("f1"
                                                                          "DXY"
                                                                          "f2"
                                                                          "PSI"))
                                                                        (("1"
                                                                          (lemma
                                                                           "abs_series_bij_conv_abs"
                                                                           ("aa"
                                                                            "abs(g!1 o PHI)"
                                                                            "phi"
                                                                            "PSI o DXY"))
                                                                          (("1"
                                                                            (expand
                                                                             "absconvergent?"
                                                                             -6)
                                                                            (("1"
                                                                              (assert)
                                                                              (("1"
                                                                                (lemma
                                                                                 "comp_inverse_right_alt[nat, (union(X!1, Y!1))]"
                                                                                 ("f"
                                                                                  "PHI"
                                                                                  "g"
                                                                                  "PSI"))
                                                                                (("1"
                                                                                  (case-replace
                                                                                   "abs(g!1 o PHI) o (PSI o DXY) = abs(g!1 o DXY)")
                                                                                  (("1"
                                                                                    (hide-all-but
                                                                                     (1
                                                                                      -1))
                                                                                    (("1"
                                                                                      (apply-extensionality
                                                                                       1
                                                                                       :hide?
                                                                                       t)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "o ")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "abs")
                                                                                          (("1"
                                                                                            (inst
                                                                                             -
                                                                                             "DXY(x!1)")
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (propax)
                                                                            nil
                                                                            nil)
                                                                           ("3"
                                                                            (hide-all-but
                                                                             (-5
                                                                              1))
                                                                            (("3"
                                                                              (expand
                                                                               "absconvergent?")
                                                                              (("3"
                                                                                (expand
                                                                                 "o ")
                                                                                (("3"
                                                                                  (case-replace
                                                                                   "abs(abs(LAMBDA (x: nat): g!1(PHI(x)))) = abs(LAMBDA (x: nat): g!1(PHI(x)))")
                                                                                  (("3"
                                                                                    (hide-all-but
                                                                                     1)
                                                                                    (("3"
                                                                                      (apply-extensionality
                                                                                       1
                                                                                       :hide?
                                                                                       t)
                                                                                      (("3"
                                                                                        (expand
                                                                                         "abs")
                                                                                        (("3"
                                                                                          (grind)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (propax)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (expand
                                                               "absconvergent?")
                                                              (("2"
                                                                (lemma
                                                                 "conv_series_shift"
                                                                 ("N"
                                                                  "N"))
                                                                (("2"
                                                                  (inst
                                                                   -
                                                                   "abs(g!1 o PHI)")
                                                                  (("2"
                                                                    (replace
                                                                     -1
                                                                     1)
                                                                    (("2"
                                                                      (case-replace
                                                                       "(LAMBDA n: abs(g!1 o PHI)(n + N)) = abs(g!1 o DY)")
                                                                      (("2"
                                                                        (hide-all-but
                                                                         1)
                                                                        (("2"
                                                                          (apply-extensionality
                                                                           :hide?
                                                                           t)
                                                                          (("2"
                                                                            (expand
                                                                             "abs")
                                                                            (("2"
                                                                              (expand
                                                                               "o ")
                                                                              (("2"
                                                                                (expand
                                                                                 "abs")
                                                                                (("2"
                                                                                  (expand
                                                                                   "PHI")
                                                                                  (("2"
                                                                                    (propax)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide-all-but
                                                           (-2
                                                            -7
                                                            -10
                                                            1))
                                                          (("2"
                                                            (expand
                                                             "bijective?")
                                                            (("2"
                                                              (flatten)
                                                              (("2"
                                                                (split)
                                                                (("1"
                                                                  (expand
                                                                   "injective?")
                                                                  (("1"
                                                                    (skosimp)
                                                                    (("1"
                                                                      (expand
                                                                       "PHI")
                                                                      (("1"
                                                                        (case-replace
                                                                         "x1!1<N")
                                                                        (("1"
                                                                          (case-replace
                                                                           "x2!1 < N")
                                                                          (("1"
                                                                            (inst
                                                                             -4
                                                                             "x1!1"
                                                                             "x2!1")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (typepred
                                                                               "DX(x1!1)")
                                                                              (("2"
                                                                                (typepred
                                                                                 "DY(x2!1-N)")
                                                                                (("2"
                                                                                  (expand
                                                                                   "disjoint?")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "intersection")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "empty?")
                                                                                      (("2"
                                                                                        (expand
                                                                                         "member")
                                                                                        (("2"
                                                                                          (inst
                                                                                           -9
                                                                                           "DX(x1!1)")
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (case-replace
                                                                           "x2!1<N")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (expand
                                                                               "disjoint?")
                                                                              (("1"
                                                                                (expand
                                                                                 "intersection")
                                                                                (("1"
                                                                                  (expand
                                                                                   "empty?")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("1"
                                                                                      (inst
                                                                                       -7
                                                                                       "DX(x2!1)")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (inst
                                                                               -4
                                                                               "x1!1-N"
                                                                               "x2!1-N")
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (expand
                                                                   "surjective?")
                                                                  (("2"
                                                                    (skosimp)
                                                                    (("2"
                                                                      (typepred
                                                                       "y!1")
                                                                      (("2"
                                                                        (expand
                                                                         "union")
                                                                        (("2"
                                                                          (expand
                                                                           "member")
                                                                          (("2"
                                                                            (split
                                                                             -1)
                                                                            (("1"
                                                                              (inst
                                                                               -3
                                                                               "y!1")
                                                                              (("1"
                                                                                (skosimp)
                                                                                (("1"
                                                                                  (inst
                                                                                   +
                                                                                   "x!1")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "PHI")
                                                                                    (("1"
                                                                                      (propax)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (inst
                                                                               -5
                                                                               "y!1")
                                                                              (("2"
                                                                                (skosimp)
                                                                                (("2"
                                                                                  (inst
                                                                                   +
                                                                                   "N+x!1")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "PHI")
                                                                                    (("2"
                                                                                      (propax)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("3"
                                                          (skosimp)
                                                          (("3"
                                                            (expand
                                                             "PHI")
                                                            (("3"
                                                              (expand
                                                               "union")
                                                              (("3"
                                                                (expand
                                                                 "member")
                                                                (("3"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (skosimp)
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2)
      (("3" (skosimp) (("3" (rewrite "countable_union") nil nil)) nil))
      nil)
     ("4" (skosimp)
      (("4" (assert)
        (("4" (typepred "X!1")
          (("4" (lemma "finite_countable" ("x" "X!1"))
            (("4" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_union judgement-tcc nil finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (conv_series_shift formula-decl nil series "series/")
    (card_bij_inv formula-decl nil finite_sets nil)
    (infinite_union formula-decl nil infinite_sets_def nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (series_sum_conv formula-decl nil series "series/")
    (abs_series_bij_conv_abs formula-decl nil absconv_series "series/")
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (abs const-decl "sequence[real]" series "series/")
    (convergence const-decl "bool" convergence_sequences "analysis/")
    (T_low type-eq-decl nil sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (sigma def-decl "real" sigma "reals/")
    (sigma_0_neg formula-decl nil sigma_nat "reals/")
    (denumerable_enumeration_bij formula-decl nil
     denumerable_enumeration nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (disjoint? const-decl "bool" sets nil)
    (union const-decl "set" sets nil))
   shostak))
 (convergent_union 0
  (convergent_union-1 nil 3351591647
   ("" (skosimp*)
    (("" (rewrite "union_difference")
      ((""
        (lemma "convergent_difference" ("X" "Y!1" "Y" "X!1" "g" "g!1"))
        (("" (assert)
          ((""
            (lemma "convergent_disjoint_union"
             ("X" "X!1" "Y" "difference(Y!1,X!1)" "g" "g!1"))
            (("" (assert)
              (("" (hide-all-but 1) (("" (grind) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((union_difference formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (T formal-type-decl nil countable_convergence nil)
    (countable_difference application-judgement "countable_set[T]"
     countable_convergence nil)
    (countable_union application-judgement "countable_set[T]"
     countable_convergence nil)
    (countable_intersection1 application-judgement "countable_set[T]"
     countable_convergence nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (disjoint? const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (convergent_disjoint_union formula-decl nil countable_convergence
     nil)
    (convergent_difference formula-decl nil countable_convergence nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil))
   shostak))
 (convergent_add 0
  (convergent_add-1 nil 3351591509
   ("" (skosimp)
    (("" (lemma "add_as_union" ("x" "t!1" "a" "X!1"))
      ((""
        (lemma "convergent_union"
         ("X" "X!1" "Y" "singleton(t!1)" "g" "g!1"))
        (("1" (rewrite "convergent_singleton") (("1" (assert) nil nil))
          nil)
         ("2" (lemma "finite_countable" ("x" "singleton[T](t!1)"))
          (("2" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil countable_convergence nil)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (add_as_union formula-decl nil sets_lemmas nil)
    (convergent_singleton formula-decl nil countable_convergence nil)
    (countable_add application-judgement "countable_set[T]"
     countable_convergence nil)
    (nonempty_union2 application-judgement "(nonempty?)" sets nil)
    (countable_union application-judgement "countable_set[T]"
     countable_convergence nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" countable_convergence nil)
    (convergent_union formula-decl nil countable_convergence nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil))
   shostak))
 (convergent_remove 0
  (convergent_remove-1 nil 3351595861
   ("" (skosimp)
    ((""
      (lemma "convergent_subset"
       ("X" "remove(t!1,X!1)" "Y" "X!1" "g" "g!1"))
      (("" (split -1)
        (("1" (propax) nil nil)
         ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)
         ("3" (propax) nil nil))
        nil))
      nil))
    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)
    (remove const-decl "set" sets nil)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil countable_convergence nil)
    (convergent_subset formula-decl nil countable_convergence nil)
    (countable_remove application-judgement "countable_set[T]"
     countable_convergence nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (/= const-decl "boolean" notequal nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil))
   shostak))
 (convergent_abs 0
  (convergent_abs-1 nil 3395767351
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (case-replace "is_finite(X!1)")
        (("1" (assert) nil nil)
         ("2" (assert)
          (("2" (name-replace "D" "denumerable_enumeration(X!1)")
            (("2" (expand "absconvergent?")
              (("2" (expand "o ")
                (("2" (expand "abs")
                  (("2"
                    (case-replace
                     "(LAMBDA (n: nat): abs(abs(g!1(D(n)))))=(LAMBDA (n: nat): abs(g!1(D(n))))")
                    (("1" (assert) nil nil)
                     ("2" (apply-extensionality :hide? t)
                      (("1" (hide-all-but 1) (("1" (grind) nil nil))
                        nil)
                       ("2" (skosimp)
                        (("2" (hide-all-but 1) (("2" (grind) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" countable_convergence nil)
    (absconvergent? const-decl "bool" absconv_series "series/")
    (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
    (abs const-decl "sequence[real]" series "series/")
    (D skolem-const-decl "[nat -> (X!1)]" countable_convergence nil)
    (X!1 skolem-const-decl "countable_set[T]" countable_convergence
     nil)
    (g!1 skolem-const-decl "[T -> real]" countable_convergence nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (O const-decl "T3" function_props nil)
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil countable_convergence nil))
   shostak)))