(taylor_series
 (T_pred_0 0
  (T_pred_0-1 nil 3298383901
   ("" (name "XX" "choose({X:T | TRUE})")
    (("1" (lemma "ball")
      (("1" (inst - "XX")
        (("1" (assert)
          (("1" (lemma "connected_domain")
            (("1" (expand "connected?")
              (("1" (case "XX >= 0")
                (("1" (inst - "-XX" "XX" "0") (("1" (assert) nil nil))
                  nil)
                 ("2" (inst - "XX" "-XX" "0") (("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (expand "nonempty?")
      (("2" (expand "empty?")
        (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (ball formula-decl nil taylor_series nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (>= const-decl "bool" reals nil)
    (connected_domain formula-decl nil taylor_series nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil)
    (TRUE const-decl "bool" booleans nil))
   nil))
 (IMP_power_series_deriv_TCC1 0
  (IMP_power_series_deriv_TCC1-1 nil 3298366313
   ("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
   ((connected_domain formula-decl nil taylor_series nil)) shostak))
 (IMP_power_series_deriv_TCC2 0
  (IMP_power_series_deriv_TCC2-1 nil 3298366313
   ("" (skosimp*)
    (("" (lemma "not_one_element") (("" (inst?) nil nil)) nil)) nil)
   ((not_one_element formula-decl nil taylor_series nil)) shostak))
 (IMP_power_series_deriv_TCC3 0
  (IMP_power_series_deriv_TCC3-1 nil 3298366313
   ("" (skosimp*) (("" (lemma "open") (("" (inst?) nil nil)) nil)) nil)
   ((open formula-decl nil taylor_series nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (IMP_power_series_deriv_TCC4 0
  (IMP_power_series_deriv_TCC4-1 nil 3298366313
   ("" (lemma "ball")
    (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series 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)
    (ball formula-decl nil taylor_series nil))
   shostak))
 (deriv_domain 0
  (deriv_domain-1 nil 3472466626
   ("" (lemma connected_domain)
    (("" (lemma not_one_element)
      (("" (lemma connected_deriv_domain[T]) (("" (assert) nil nil))
        nil))
      nil))
    nil)
   ((not_one_element formula-decl nil taylor_series nil)
    (connected_deriv_domain formula-decl nil deriv_domain_def
     "analysis/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (connected_domain formula-decl nil taylor_series nil))
   shostak))
 (Inf_sum_0_TCC1 0
  (Inf_sum_0_TCC1-1 nil 3298366313
   ("" (skosimp*)
    (("" (name "XX" "epsilon({X:T | TRUE})")
      (("" (lemma "ball")
        (("" (inst - "XX")
          (("" (assert)
            (("" (lemma "connected_domain")
              (("" (expand "connected?")
                (("" (case "XX >= 0")
                  (("1" (inst - "-XX" "XX" "0")
                    (("1" (assert) nil nil)) nil)
                   ("2" (inst - "XX" "-XX" "0")
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((TRUE const-decl "bool" booleans nil)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (connected_domain formula-decl nil taylor_series nil)
    (>= const-decl "bool" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (minus_real_is_real application-judgement "real" reals nil)
    (ball formula-decl nil taylor_series nil))
   shostak))
 (Inf_sum_0 0
  (Inf_sum_0-1 nil 3298299936
   ("" (skosimp*)
    (("" (expand "Inf_sum")
      (("" (assert)
        (("" (expand "powerseries")
          (("" (expand "powerseq")
            ((""
              (case-replace "(LAMBDA (k: nat): a!1(k) * 0 ^ k) =
                       (LAMBDA (k: nat):
                       IF k = 0 THEN a!1(0) ELSE 0 ENDIF)")
              (("1" (hide -1)
                (("1" (expand "series")
                  (("1" (lemma "sigma_first[nat]")
                    (("1" (inst?)
                      (("1"
                        (case-replace "(LAMBDA (n: nat):
                  sigma(0, n,
                        (LAMBDA (k: nat): IF k = 0 THEN a!1(0) ELSE 0 ENDIF))) =
                 (LAMBDA (n: nat): a!1(0) )")
                        (("1" (lemma "limit_const")
                          (("1" (inst - "a!1(0)")
                            (("1" (assert)
                              (("1"
                                (expand "const_fun")
                                (("1" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide 2)
                          (("2" (apply-extensionality 1 :hide? t)
                            (("2" (lemma "sigma_first[nat]")
                              (("2"
                                (inst?)
                                (("2"
                                  (assert)
                                  (("2"
                                    (case-replace "x!1 = 0")
                                    (("1"
                                      (expand "sigma" 1)
                                      (("1"
                                        (expand "sigma")
                                        (("1" (propax) nil nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (replace -1)
                                        (("2"
                                          (hide -1)
                                          (("2"
                                            (rewrite
                                             "sigma_restrict_to")
                                            (("2"
                                              (expand "restrict")
                                              (("2"
                                                (lemma "sigma_const")
                                                (("2"
                                                  (inst?)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (apply-extensionality 1 :hide? t)
                  (("2" (lift-if)
                    (("2" (ground) (("2" (grind) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Inf_sum const-decl "real" power_series_conv nil)
    (powerseries const-decl "sequence[real]" power_series nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sequence type-eq-decl nil sequences nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (series const-decl "sequence[real]" series nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (T_low type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (restrict const-decl "[T -> real]" sigma "reals/")
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (sigma_nat application-judgement "nat" sigma_nat "reals/")
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (sigma_const formula-decl nil sigma "reals/")
    (sigma_restrict_to formula-decl nil sigma "reals/")
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (limit_const formula-decl nil convergence_ops "analysis/")
    (constant_seq1 application-judgement "(convergent?)"
     convergence_ops "analysis/")
    (derivable_const application-judgement "deriv_fun" derivatives
     "analysis/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (sigma def-decl "real" sigma "reals/")
    (sigma_first formula-decl nil sigma "reals/")
    (nat_exp application-judgement "nat" exponentiation nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero_hat formula-decl nil exponent_props "reals/")
    (nat_expt application-judgement "nat" exponentiation nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (expt def-decl "real" exponentiation nil)
    (powerseq const-decl "sequence[real]" power_series nil))
   shostak))
 (nderivseq_lem 0
  (nderivseq_lem-1 nil 3298373671
   ("" (skosimp*)
    (("" (expand "nderivseq")
      (("" (apply-extensionality 1 :hide? t)
        (("" (rewrite "factorial_plus1")
          (("" (assert)
            (("" (expand "derivseq")
              (("" (name-replace "FNX" "factorial(n!1 + x!1)")
                (("" (field 1) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nderivseq const-decl "sequence[real]" taylor_series nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (factorial_plus1 formula-decl nil factorial "ints/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (TRUE const-decl "bool" booleans nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (* const-decl "[numfield, numfield -> numfield]" 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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (factorial def-decl "posnat" factorial "ints/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sequence type-eq-decl nil sequences nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (derivseq const-decl "sequence[real]" power_series_derivseq nil)
    (numfield nonempty-type-eq-decl nil number_fields 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))
 (conv_nderivseq 0
  (conv_nderivseq-1 nil 3298367015
   ("" (induct "n")
    (("1" (skosimp*)
      (("1" (expand "nderivseq")
        (("1"
          (case-replace
           "(LAMBDA (k: nat): factorial(k) / factorial(k) * a!1(k)) = a!1")
          (("1" (apply-extensionality 1 :hide? t) nil nil)) nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (rewrite "nderivseq_lem")
        (("2" (inst?)
          (("2" (assert)
            (("2" (hide 2) (("2" (rewrite "conv_derivseq") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((derivseq const-decl "sequence[real]" power_series_derivseq nil)
    (conv_derivseq formula-decl nil power_series_derivseq nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nderivseq_lem formula-decl nil taylor_series nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "[numfield, numfield -> numfield]" 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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (factorial def-decl "posnat" factorial "ints/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (nderivseq const-decl "sequence[real]" taylor_series nil)
    (conv_powerseries? const-decl "bool" power_series_conv nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (pred type-eq-decl nil defined_types 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))
 (Inf_sum_derivable_n_times_TCC1 0
  (Inf_sum_derivable_n_times_TCC1-1 nil 3471697763
   ("" (skosimp*)
    (("" (lemma "deriv_domain") (("" (inst?) nil nil)) nil)) nil)
   ((deriv_domain formula-decl nil taylor_series nil)) nil))
 (Inf_sum_derivable_n_times 0
  (Inf_sum_derivable_n_times-1 nil 3298373838
   ("" (induct "n")
    (("1" (skosimp*)
      (("1" (expand "derivable_n_times?") (("1" (propax) nil nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "derivable_n_times?" 1)
        (("2" (rewrite "Inf_sum_derivable")
          (("2" (inst - "derivseq(a!1)")
            (("2" (rewrite "conv_derivseq")
              (("2" (rewrite "deriv_Inf_sum") nil nil)) nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2)
      (("3" (lemma "not_one_element") (("3" (skosimp*) nil nil)) nil))
      nil)
     ("4" (hide 2)
      (("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil))
      nil))
    nil)
   ((Inf_sum_derivable formula-decl nil power_series_deriv nil)
    (conv_derivseq formula-decl nil power_series_derivseq nil)
    (deriv_Inf_sum formula-decl nil power_series_deriv nil)
    (derivseq const-decl "sequence[real]" power_series_derivseq nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (Inf_sum const-decl "real" power_series_conv nil)
    (derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
    (conv_powerseries? const-decl "bool" power_series_conv nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (pred type-eq-decl nil defined_types 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))
 (nderiv_Inf_sum_TCC1 0
  (nderiv_Inf_sum_TCC1-1 nil 3298366314
   ("" (skosimp*) (("" (rewrite "Inf_sum_derivable_n_times") nil nil))
    nil)
   ((Inf_sum_derivable_n_times formula-decl nil taylor_series nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil))
   shostak))
 (nderiv_Inf_sum_TCC2 0
  (nderiv_Inf_sum_TCC2-1 nil 3298366314
   ("" (skosimp*)
    (("" (lemma " conv_nderivseq")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((conv_nderivseq formula-decl nil taylor_series nil)
    (sequence type-eq-decl nil sequences 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))
 (nderiv_Inf_sum 0
  (nderiv_Inf_sum-1 nil 3298302128
   ("" (induct "n")
    (("1" (skosimp*)
      (("1" (expand "nderiv")
        (("1" (expand "nderivseq")
          (("1"
            (case-replace
             "(LAMBDA (k: nat): factorial(k) / factorial(k) * a!1(k)) = a!1")
            (("1" (hide 2)
              (("1" (apply-extensionality 1 :hide? t) nil nil)) nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "nderiv" 1)
        (("2" (lemma "deriv_Inf_sum")
          (("2" (inst?)
            (("2" (assert)
              (("2" (replace -1)
                (("2" (hide -1)
                  (("2" (inst?)
                    (("2" (rewrite "conv_derivseq")
                      (("2" (replace -1)
                        (("2" (hide -1)
                          (("2"
                            (case-replace
                             "nderivseq(j!1, derivseq(a!1)) = nderivseq(1 + j!1, a!1)")
                            (("2" (hide 2)
                              (("2"
                                (expand "nderivseq")
                                (("2"
                                  (expand "derivseq")
                                  (("2"
                                    (apply-extensionality 1 :hide? t)
                                    (("2"
                                      (name-replace
                                       "AA"
                                       "a!1(1 + j!1 + x!1)")
                                      (("2"
                                        (case-replace
                                         "factorial(1 + j!1 + x!1) = (1 + j!1 + x!1)*factorial(j!1 + x!1)")
                                        (("1"
                                          (name-replace
                                           "FF"
                                           "factorial(j!1 + x!1)")
                                          (("1" (field 1) nil nil))
                                          nil)
                                         ("2"
                                          (hide 2)
                                          (("2"
                                            (expand "factorial" 1 1)
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (hide 2)
      (("3" (skosimp*) (("3" (rewrite "conv_nderivseq") nil nil)) nil))
      nil)
     ("4" (hide 2)
      (("4" (skosimp*)
        (("4" (rewrite "Inf_sum_derivable_n_times") nil nil)) nil))
      nil))
    nil)
   ((Inf_sum_derivable_n_times formula-decl nil taylor_series nil)
    (conv_nderivseq formula-decl nil taylor_series nil)
    (deriv_Inf_sum formula-decl nil power_series_deriv nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (conv_derivseq formula-decl nil power_series_derivseq nil)
    (TRUE const-decl "bool" booleans nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (derivseq const-decl "sequence[real]" power_series_derivseq nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" 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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (factorial def-decl "posnat" factorial "ints/")
    (nat_induction formula-decl nil naturalnumbers nil)
    (nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
    (nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types nil)
    (nderivseq const-decl "sequence[real]" taylor_series nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (conv_powerseries? const-decl "bool" power_series_conv nil)
    (derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
    (Inf_sum const-decl "real" power_series_conv nil))
   shostak))
 (Taylor_expansion 0
  (Taylor_expansion-1 nil 3298298896
   ("" (skosimp*)
    (("" (replace -2)
      (("" (lemma "nderiv_Inf_sum")
        (("" (inst?)
          (("" (assert)
            (("" (replace -1)
              (("" (hide -1)
                (("" (lemma "Inf_sum_0")
                  (("" (rewrite "Inf_sum_0")
                    (("1" (lemma "Inf_sum_derivable_n_times")
                      (("1" (inst?)
                        (("1" (assert)
                          (("1" (expand "nderivseq")
                            (("1" (expand "factorial" 1 3)
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (rewrite "conv_nderivseq") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (Inf_sum_0 formula-decl nil taylor_series nil)
    (conv_nderivseq formula-decl nil taylor_series nil)
    (Inf_sum_derivable_n_times formula-decl nil taylor_series nil)
    (factorial def-decl "posnat" factorial "ints/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (nderivseq const-decl "sequence[real]" taylor_series nil)
    (nderiv_Inf_sum formula-decl nil taylor_series nil))
   shostak))
 (Taylor_seq_TCC1 0
  (Taylor_seq_TCC1-1 nil 3298631644
   ("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil)
   ((T_pred_0 formula-decl nil taylor_series nil)) shostak))
 (Taylor_seq_TCC2 0
  (Taylor_seq_TCC2-1 nil 3298631644
   ("" (skosimp*)
    (("" (typepred "f!1")
      (("" (expand "inf_deriv_fun?") (("" (inst?) nil nil)) nil)) nil))
    nil)
   ((inf_deriv_fun? const-decl "bool" taylors "analysis/")
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans 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))
   shostak))
 (Taylor_seq_TCC3 0
  (Taylor_seq_TCC3-1 nil 3471697763
   ("" (skosimp*)
    (("" (lemma "deriv_domain") (("" (inst?) nil nil)) nil)) nil)
   ((deriv_domain formula-decl nil taylor_series nil)) nil))
 (Taylor_seq_term_TCC1 0
  (Taylor_seq_term_TCC1-1 nil 3298631644
   ("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil)
   ((T_pred_0 formula-decl nil taylor_series nil)) shostak))
 (Taylor_seq_term_TCC2 0
  (Taylor_seq_term_TCC2-1 nil 3298631644
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (Taylor_seq_term_TCC3 0
  (Taylor_seq_term_TCC3-1 nil 3298631644
   ("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil)
   ((T_pred_0 formula-decl nil taylor_series nil)) shostak))
 (Taylor_seq_term 0
  (Taylor_seq_term-1 nil 3298383588
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (expand "Taylor_seq")
        (("1" (expand "Taylor_term")
          (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
        nil)
       ("2" (rewrite "T_pred_0") nil nil)
       ("3" (rewrite "T_pred_0") (("3" (skosimp*) nil nil)) nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Taylor_term const-decl "real" taylors "analysis/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (Taylor_seq const-decl "real" taylor_series nil)
    (inf_deriv_fun? const-decl "bool" taylors "analysis/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   shostak))
 (GET_C_TCC1 0
  (GET_C_TCC1-1 nil 3298631645
   ("" (skosimp*)
    (("" (typepred "f!1")
      (("" (expand "inf_deriv_fun?") (("" (inst?) nil nil)) nil)) nil))
    nil)
   ((inf_deriv_fun? const-decl "bool" taylors "analysis/")
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   shostak))
 (GET_C_TCC2 0
  (GET_C_TCC2-1 nil 3298631645
   ("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil)
   ((T_pred_0 formula-decl nil taylor_series nil)) shostak))
 (GET_C_TCC3 0
  (GET_C_TCC3-3 nil 3306575811
   (""
    (inst + "(LAMBDA (f:(inf_deriv_fun?[T]), x:T, k: nat):
                             choose({c: between[T](0, x) |
                                      powerseries(Taylor_seq(f))(x)(k) =
                                       f(x) -
                                        Taylor_rem(k, f, 0, x, c)}))")
    (("1" (skosimp*)
      (("1" (expand "nonempty?")
        (("1" (expand "empty?")
          (("1" (expand "member")
            (("1" (lemma "Taylors_inf[T]")
              (("1" (inst - "0" "x!1" "f!1" "k!1")
                (("1" (assert)
                  (("1" (skosimp*)
                    (("1" (inst - "c!1")
                      (("1" (lemma "Taylor_seq_term")
                        (("1" (inst?)
                          (("1" (assert)
                            (("1" (replace -2)
                              (("1"
                                (assert)
                                (("1"
                                  (expand "powerseries")
                                  (("1"
                                    (expand "powerseq")
                                    (("1"
                                      (replace -1 * rl)
                                      (("1"
                                        (hide -1)
                                        (("1"
                                          (expand "series")
                                          (("1"
                                            (case-replace
                                             "(LAMBDA (k: nat): Taylor_seq(f!1)(k) * x!1 ^ k
                                     ) = (LAMBDA n:
                                               IF n = 0 THEN f!1(0) ELSE Taylor_seq(f!1)(n) * x!1 ^ n ENDIF)")
                                            (("1"
                                              (hide 2)
                                              (("1"
                                                (apply-extensionality
                                                 1
                                                 :hide?
                                                 t)
                                                (("1"
                                                  (lift-if)
                                                  (("1"
                                                    (ground)
                                                    (("1"
                                                      (expand
                                                       "Taylor_seq")
                                                      (("1"
                                                        (expand
                                                         "nderiv")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (replace
                                                             -1)
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (rewrite "T_pred_0") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (skosimp*) (("2" (rewrite "T_pred_0") nil nil)) nil)
     ("3" (skosimp*)
      (("3" (typepred "f!1")
        (("3" (expand "inf_deriv_fun?") (("3" (inst?) nil nil)) nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (empty? const-decl "bool" sets nil)
    (Taylors_inf formula-decl nil taylors "analysis/")
    (T_pred_0 formula-decl nil taylor_series nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (series const-decl "sequence[real]" series nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (factorial_0 formula-decl nil factorial "ints/")
    (expt_x0 formula-decl nil exponentiation nil)
    (nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (powerseq const-decl "sequence[real]" power_series nil)
    (real_plus_real_is_real application-judgement "real" reals 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)
    (Taylor_seq_term formula-decl nil taylor_series nil)
    (member const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (Taylor_rem const-decl "real" taylors "analysis/")
    (nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (Taylor_seq const-decl "real" taylor_series nil)
    (powerseries const-decl "sequence[real]" power_series nil)
    (sequence type-eq-decl nil sequences nil)
    (between type-eq-decl nil taylors "analysis/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (< const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (inf_deriv_fun? const-decl "bool" taylors "analysis/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series 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)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)
  (GET_C_TCC3-2 nil 3298627880
   (""
    (inst + "(LAMBDA (f:(inf_deriv_fun?[T]), x:T, k: nat):
                     choose({c: between[T](0, x) |
                              powerseries(Taylor_seq[T](f))(x)(k) =
                               f(x) -
                                Taylor_rem[T](k, f, 0, x, c)}))")
    (("1" (skosimp*)
      (("1" (expand "nonempty?")
        (("1" (expand "empty?")
          (("1" (expand "member")
            (("1" (lemma "Taylors_inf[T]")
              (("1" (inst - "0" "x!1" "f!1" "k!1")
                (("1" (assert)
                  (("1" (skosimp*)
                    (("1" (inst - "c!1")
                      (("1" (lemma "Taylor_seq_term")
                        (("1" (inst?)
                          (("1" (assert)
                            (("1" (replace -2)
                              (("1"
                                (assert)
                                (("1"
                                  (expand "powerseries")
                                  (("1"
                                    (expand "powerseq")
                                    (("1"
                                      (replace -1 * rl)
                                      (("1"
                                        (hide -1)
                                        (("1"
                                          (expand "series")
                                          (("1"
                                            (case-replace
                                             "(LAMBDA (k: nat):
              IF k = 0 THEN Taylor_seq[T](f!1)(0)
              ELSE Taylor_seq[T](f!1)(k) * x!1 ^ k
              ENDIF) = (LAMBDA n:
               IF n = 0 THEN f!1(0) ELSE Taylor_seq(f!1)(n) * x!1 ^ n ENDIF)")
                                            (("1"
                                              (hide 2)
                                              (("1"
                                                (apply-extensionality
                                                 1
                                                 :hide?
                                                 t)
                                                (("1"
                                                  (lift-if)
                                                  (("1"
                                                    (ground)
                                                    (("1"
                                                      (expand
                                                       "Taylor_seq")
                                                      (("1"
                                                        (expand
                                                         "nderiv")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (rewrite "T_pred_0")
                                                  nil
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (rewrite "T_pred_0")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (rewrite "T_pred_0") nil nil))
                nil)
               ("2" (lemma "not_one_element") (("2" (propax) nil nil))
                nil)
               ("3" (lemma "connected_domain") (("3" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (lemma "not_one_element") (("2" (skosimp*) nil nil)) nil)
     ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)
     ("4" (skosimp*) (("4" (rewrite "T_pred_0") nil nil)) nil)
     ("5" (skosimp*)
      (("5" (typepred "f!1")
        (("5" (expand "inf_deriv_fun?") (("5" (inst?) nil nil)) nil))
        nil))
      nil)
     ("6" (lemma "not_one_element") (("6" (skosimp*) nil nil)) nil)
     ("7" (lemma "connected_domain") (("7" (skosimp*) nil nil)) nil))
    nil)
   ((Taylors_inf formula-decl nil taylors "analysis/")
    (nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
    (powerseq const-decl "sequence[real]" power_series nil)
    (Taylor_rem const-decl "real" taylors "analysis/")
    (nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
    (between type-eq-decl nil taylors "analysis/")
    (inf_deriv_fun? const-decl "bool" taylors "analysis/"))
   nil)
  (GET_C_TCC3-1 nil 3298627046
   (""
    (inst + "(LAMBDA (f:(inf_deriv_fun?[T]), x:T, k: nat):
                   choose({c: between[T](0, x) |
                            powerseries(Taylor_seq[T](f))(x)(k) =
                             f(x) -
                              Taylor_rem[T](1 + k, f, 0, x, c)}))")
    (("1" (skosimp*)
      (("1" (expand "nonempty?")
        (("1" (expand "empty?")
          (("1" (expand "member")
            (("1" (lemma "Taylors_inf[T]")
              (("1" (inst - "0" "x!1" "f!1" "k!1")
                (("1" (assert)
                  (("1" (skosimp*)
                    (("1" (inst - "c!1")
                      (("1" (lemma "Taylor_seq_term")
                        (("1" (inst?)
                          (("1" (assert) (("1" (postpone) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (postpone) nil nil))
                nil)
               ("2" (postpone) nil nil) ("3" (postpone) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (lemma "not_one_element") (("2" (skosimp*) nil nil)) nil)
     ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)
     ("4" (skosimp*) (("4" (rewrite "T_pred_0") nil nil)) nil)
     ("5" (skosimp*)
      (("5" (typepred "f!1")
        (("5" (expand "inf_deriv_fun?") (("5" (inst?) nil nil)) nil))
        nil))
      nil)
     ("6" (lemma "not_one_element") (("6" (skosimp*) nil nil)) nil)
     ("7" (lemma "connected_domain") (("7" (skosimp*) nil nil)) nil))
    nil)
   nil shostak))
 (is_taylor_prep_TCC1 0
  (is_taylor_prep_TCC1-1 nil 3298631645
   ("" (skosimp*)
    (("" (expand "inf_deriv_fun?") (("" (inst?) nil nil)) nil)) nil)
   ((inf_deriv_fun? const-decl "bool" taylors "analysis/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   shostak))
 (is_taylor_prep 0
  (is_taylor_prep-3 nil 3306575640
   ("" (skosimp*)
    (("" (expand "conv_powerseries?")
      (("" (skosimp*)
        ((""
          (case-replace "powerseries(Taylor_seq(f!1))(x!1) = (LAMBDA n:
                          f!1(x!1) - Taylor_rem(n, f!1, 0, x!1, GET_C(f!1,x!1,n)))")
          (("1" (hide -1)
            (("1" (inst?)
              (("1" (lemma "convergent_diff")
                (("1"
                  (inst - "(LAMBDA n: f!1(x!1))"
                   "(LAMBDA n: Taylor_rem(n, f!1, 0, x!1, GET_C(f!1, x!1, n)))")
                  (("1" (assert)
                    (("1" (expand "-")
                      (("1" (assert)
                        (("1" (hide 2)
                          (("1" (lemma "convergent_const")
                            (("1" (expand "const_fun")
                              (("1" (inst?) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (rewrite "T_pred_0") nil nil)
                   ("3" (skosimp*)
                    (("3" (expand "inf_deriv_fun?")
                      (("3" (inst?) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (apply-extensionality 1 :hide? t)
              (("1" (rewrite "T_pred_0") nil nil)
               ("2" (skosimp*)
                (("2" (expand "inf_deriv_fun?") (("2" (inst?) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (rewrite "T_pred_0") nil nil)
           ("4" (skosimp*)
            (("4" (expand "inf_deriv_fun?") (("4" (inst?) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((conv_powerseries? const-decl "bool" power_series_conv nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sequence type-eq-decl nil sequences nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (powerseries const-decl "sequence[real]" power_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (inf_deriv_fun? const-decl "bool" taylors "analysis/")
    (Taylor_seq const-decl "real" taylor_series nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (Taylor_rem const-decl "real" taylors "analysis/")
    (between type-eq-decl nil taylors "analysis/")
    (GET_C const-decl "{c: between[T](0, x) |
         powerseries(Taylor_seq(f))(x)(k) =
          f(x) - Taylor_rem(k, f, 0, x, c)}" taylor_series nil)
    (f!1 skolem-const-decl "[T -> real]" taylor_series nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (convergent_const formula-decl nil convergence_ops "analysis/")
    (T_pred_0 formula-decl nil taylor_series nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (convergent_diff formula-decl nil convergence_ops "analysis/"))
   nil)
  (is_taylor_prep-2 nil 3298631567
   ("" (skosimp*)
    (("" (expand "conv_powerseries?")
      (("" (skosimp*)
        ((""
          (case-replace
           "powerseries(Taylor_seq[T](f!1))(x!1) = (LAMBDA n:
                        f!1(x!1) - Taylor_rem(n, f!1, 0, x!1, GET_C(f!1,x!1,n)))")
          (("1" (hide -1)
            (("1" (inst?)
              (("1" (lemma "convergent_diff")
                (("1"
                  (inst - "(LAMBDA n: f!1(x!1))"
                   "(LAMBDA n: Taylor_rem(n, f!1, 0, x!1, GET_C(f!1, x!1, n)))")
                  (("1" (assert)
                    (("1" (expand "-")
                      (("1" (assert)
                        (("1" (hide 2)
                          (("1" (lemma "convergent_const")
                            (("1" (expand "const_fun")
                              (("1" (inst?) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (rewrite "T_pred_0") nil nil)
                   ("3" (skosimp*)
                    (("3" (expand "inf_deriv_fun?")
                      (("3" (inst?) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (apply-extensionality 1 :hide? t)
              (("1" (rewrite "T_pred_0") nil nil)
               ("2" (skosimp*)
                (("2" (expand "inf_deriv_fun?") (("2" (inst?) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (rewrite "T_pred_0") nil nil)
           ("4" (skosimp*)
            (("4" (expand "inf_deriv_fun?") (("4" (inst?) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent_diff formula-decl nil convergence_ops "analysis/")
    (convergent_const formula-decl nil convergence_ops "analysis/")
    (const_fun const-decl "[T -> real]" real_fun_ops "reals/")
    (Taylor_rem const-decl "real" taylors "analysis/")
    (between type-eq-decl nil taylors "analysis/")
    (nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
    (inf_deriv_fun? const-decl "bool" taylors "analysis/"))
   nil)
  (is_taylor_prep-1 nil 3298379071
   ("" (skosimp*)
    (("" (expand "conv_powerseries?")
      (("" (skosimp*)
        (("" (lemma "convergent_diff")
          ((""
            (inst - "(LAMBDA (k: nat): f!1(x!1))"
             "(LAMBDA k: Taylor_rem(k+1, f!1, 0, x!1, GET_C(f!1,x!1,k)))")
            (("1" (expand "-")
              (("1" (expand "powerseries")
                (("1" (lemma "Taylor_seq_term")
                  (("1" (inst?)
                    (("1" (expand "powerseq")
                      (("1" (inst - "x!1")
                        (("1" (assert) (("1" (postpone) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (rewrite "T_pred_0") nil nil)
             ("3" (postpone) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
 (is_taylor_TCC1 0
  (is_taylor_TCC1-1 nil 3298374726
   ("" (skosimp*)
    (("" (lemma "is_taylor_prep")
      (("" (inst?)
        (("" (assert)
          (("" (hide 2)
            (("" (skosimp*)
              (("" (inst?)
                (("" (expand "convergent?") (("" (inst + "0") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_taylor_prep formula-decl nil taylor_series nil)
    (convergent? const-decl "bool" convergence_sequences "analysis/")
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (T_pred const-decl "[real -> boolean]" taylor_series 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))
 (is_taylor 0
  (is_taylor-2 "sdf" 3298630239
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (expand "Inf_sum")
        (("1" (expand "powerseries")
          (("1" (lemma "limit_def")
            (("1" (inst?)
              (("1" (inst - "f!1(x!1)")
                (("1" (assert)
                  (("1" (hide 2)
                    (("1" (inst?)
                      (("1" (expand "convergence")
                        (("1" (skosimp*)
                          (("1" (inst - "epsilon!1")
                            (("1" (skosimp*)
                              (("1"
                                (inst + "n!1")
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (inst - "i!1")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (name
                                         "C"
                                         "GET_C(f!1, x!1, i!1)")
                                        (("1"
                                          (typepred "C")
                                          (("1"
                                            (expand "powerseries")
                                            (("1"
                                              (replace -5)
                                              (("1"
                                                (hide -5)
                                                (("1"
                                                  (lemma "abs_neg")
                                                  (("1"
                                                    (inst
                                                     -
                                                     "Taylor_rem(i!1, f!1, 0, x!1, C)")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil)
                                                     ("2"
                                                      (rewrite
                                                       "T_pred_0")
                                                      nil
                                                      nil)
                                                     ("3"
                                                      (expand
                                                       "inf_deriv_fun?")
                                                      (("3"
                                                        (inst?)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (lemma "is_taylor_prep")
                  (("2" (inst?)
                    (("2" (assert)
                      (("2" (expand "conv_powerseries?")
                        (("2" (split -1)
                          (("1" (expand "powerseries")
                            (("1" (inst?) nil nil)) nil)
                           ("2" (hide 2)
                            (("2" (skosimp*)
                              (("2"
                                (expand "convergent?")
                                (("2"
                                  (inst + "0")
                                  (("2" (inst?) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "is_taylor_prep")
        (("2" (inst?)
          (("2" (assert)
            (("2" (hide 2)
              (("2" (skosimp*)
                (("2" (inst?)
                  (("2" (assert)
                    (("2" (expand "convergent?")
                      (("2" (inst + "0") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (T_pred const-decl "[real -> boolean]" taylor_series nil)
    (T formal-nonempty-subtype-decl nil taylor_series nil)
    (Taylor_seq const-decl "real" taylor_series nil)
    (inf_deriv_fun? const-decl "bool" taylors "analysis/")
    (Inf_sum const-decl "real" power_series_conv nil)
    (conv_powerseries? const-decl "bool" power_series_conv nil)
    (sequence type-eq-decl nil sequences 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)
    (powerseries const-decl "sequence[real]" power_series nil)
    (powerseq const-decl "sequence[real]" power_series nil)
    (series const-decl "sequence[real]" series nil)
    (convergent? const-decl "bool" convergence_sequences "analysis/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (abs_neg formula-decl nil abs_lems "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (GET_C const-decl "{c: between[T](0, x) |
         powerseries(Taylor_seq(f))(x)(k) =
          f(x) - Taylor_rem(k, f, 0, x, c)}" taylor_series nil)
    (Taylor_rem const-decl "real" taylors "analysis/")
    (nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (between type-eq-decl nil taylors "analysis/")
    (< const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (convergence const-decl "bool" convergence_sequences "analysis/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (limit_def formula-decl nil convergence_sequences "analysis/"))
   nil)
  (sdf "sdf" 3298630207
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (expand "Inf_sum") (("1" (postpone) nil nil)) nil)
       ("2" (postpone) nil nil))
      nil))
    nil)
   nil shostak)
  (is_taylor-1 nil 3298374780
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (expand "Inf_sum")
        (("1" (expand "powerseries")
          (("1" (lemma "limit_def")
            (("1" (inst?)
              (("1" (inst - "f!1(x!2)")
                (("1" (assert)
                  (("1" (hide 2)
                    (("1" (expand "convergence")
                      (("1" (skosimp*)
                        (("1" (lemma "Taylors_inf[T]")
                          (("1" (inst?)
                            (("1" (assert)
                              (("1"
                                (expand "powerseq")
                                (("1" (postpone) nil nil))
                                nil))
                              nil)
                             ("2" (postpone) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (postpone) nil nil) ("3" (postpone) nil nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (postpone) nil nil))
      nil))
    nil)
   nil shostak)))

