(th_D
 (sum_TCC1 0
  (sum_TCC1-1 nil 3667129223 ("" (subtype-tcc) nil nil) nil nil))
 (sum_TCC2 0
  (sum_TCC2-1 nil 3667129223 ("" (termination-tcc) nil nil) nil nil))
 (D_1 0
  (D_1-1 nil 3667129225
   ("" (induct n)
    (("1" (assert) (("1" (grind) nil nil)) nil)
     ("2" (skeep) (("2" (expand sum 1) (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    nil
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
 (D_2 0
  (D_2-1 nil 3667129345
   ("" (induct n)
    (("1" (grind) nil nil)
     ("2" (skeep)
      (("2" (expand sum 1)
        (("2" (expand id 1 1) (("2" (grind) nil nil)) nil)) nil))
      nil))
    nil)
   ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (id_preserves application-judgement "S" identity_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil) nil
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
 (pow_TCC1 0
  (pow_TCC1-1 nil 3667129223 ("" (skeep) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (pow_TCC2 0
  (pow_TCC2-1 nil 3667144387 ("" (termination-tcc) nil nil) nil nil)))
(th_Da
 (Da_1 0
  (Da_1-1 nil 3667129545
   ("" (induct n1)
    (("1" (expand sum)
      (("1" (expand square) (("1" (propax) nil nil)) nil)) nil)
     ("2" (skeep)
      (("2" (expand sum 1)
        (("2" (replace -1 1)
          (("2" (assert) (("2" (grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (square const-decl "nat" th_Da nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil) nil
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers
     nil))
   shostak))
 (Da_2 0
  (Da_2-1 nil 3667129831
   ("" (induct n)
    (("1" (grind) nil nil)
     ("2" (skeep)
      (("2" (expand sum 1)
        (("2" (replace -1 1) (("2" (grind) nil nil)) nil)) nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_even_is_even application-judgement "even_int" integers
     nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (square const-decl "nat" th_Da nil) nil
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities 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))
 (Da_3 0
  (Da_3-1 nil 3667129862
   ("" (induct n)
    (("1" (grind) nil nil)
     ("2" (skeep)
      (("2" (expand sum 1 1)
        (("2" (expand sum 1 2)
          (("2" (replace -1 1)
            (("2" (expand square 1)
              (("2" (expand cube 1)
                (("2" (lemma D_1)
                  (("2" (inst -1 j)
                    (("2" (replace -1 1) (("2" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((mult_divides2 application-judgement "(divides(m))" divides nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (D_1 formula-decl nil th_D nil)
    (even_plus_even_is_even application-judgement "even_int" integers
     nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil) nil
    (square const-decl "nat" th_Da nil)
    (cube const-decl "nat" th_Da nil) nil
    (= const-decl "[T, T -> boolean]" equalities 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))
 (Da_4 0
  (Da_4-1 nil 3667130517
   ("" (induct n1)
    (("1" (grind) nil nil)
     ("2" (skeep)
      (("2" (expand sum 1)
        (("2" (replace -1 1)
          (("2" (expand pow 1 3) (("2" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((nnint_plus_posint_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)
    (pred type-eq-decl nil defined_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sum def-decl "nat" th_D nil) (pow def-decl "nat" th_D nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (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)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil))
   shostak))
 (Da_5 0
  (Da_5-1 nil 3667130601
   ("" (induct n1)
    (("1" (expand sum 1) (("1" (propax) nil nil)) nil)
     ("2" (skeep) (("2" (expand sum 1) (("2" (propax) nil nil)) nil))
      nil))
    nil)
   ((nat_induction formula-decl nil naturalnumbers nil) nil
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   shostak)))
(th_Db
 (geom_TCC1 0
  (geom_TCC1-1 nil 3667129224 ("" (subtype-tcc) nil nil) nil nil))
 (geom_TCC2 0
  (geom_TCC2-1 nil 3667129224 ("" (subtype-tcc) nil nil) nil nil))
 (geom_TCC3 0
  (geom_TCC3-1 nil 3667129224 ("" (termination-tcc) nil nil) nil nil))
 (geom_sum 0
  (geom_sum-1 nil 3667130791
   ("" (induct a)
    (("1" (induct n)
      (("1" (grind) nil nil)
       ("2" (skeep)
        (("2" (split -1)
          (("1" (expand geom 1)
            (("1" (replace -1 1) (("1" (grind) nil nil)) nil)) nil)
           ("2" (propax) nil nil))
          nil))
        nil))
      nil)
     ("2" (skeep)
      (("2" (induct n)
        (("1" (grind) nil nil)
         ("2" (skolem 1 k)
          (("2" (flatten 1)
            (("2" (split -1)
              (("1" (expand geom 1)
                (("1" (replace -1 1)
                  (("1" (expand pow 1 3) (("1" (propax) nil nil)) nil))
                  nil))
                nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nnint_times_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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (nzint_times_nzint_is_nzint application-judgement "nzint" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pow def-decl "nat" th_D nil) (geom def-decl "posnat" th_Db nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (> const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)))