Quelle  sqrt_approx.prf

(sqrt_approx
 (sq_sq_aux 0
  (sq_sq_aux-1 nil 3320768920 ("" (grind) nil nil)
   ((nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (sq const-decl "nonneg_real" sq nil))
   shostak))
 (sqrt_newton_aux_TCC1 0
  (sqrt_newton_aux_TCC1-1 nil 3320768919 ("" (grind-reals) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (sqrt_newton_aux_TCC2 0
  (sqrt_newton_aux_TCC2-1 nil 3320768919 ("" (grind-reals) nil nil)
   ((posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_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)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (sqrt_newton_aux_TCC3 0
  (sqrt_newton_aux_TCC3-1 nil 3320768919 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (< const-decl "bool" reals 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)
    (real_ge_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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq const-decl "nonneg_real" sq nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil))
 (sqrt_newton_aux_TCC4 0
  (sqrt_newton_aux_TCC4-1 nil 3320768919 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (< const-decl "bool" reals 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)
    (real_ge_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)
    (sq const-decl "nonneg_real" sq nil)
    (/= const-decl "boolean" notequal nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil))
 (sqrt_newton_aux_TCC5 0
  (sqrt_newton_aux_TCC5-2 nil 3320769110
   ("" (skosimp* :preds? t)
    (("" (case "y!1 > 0")
      (("1" (split)
        (("1" (cross-mult 1) (("1" (field) nil nil)) nil)
         ("2" (move-terms 1 l)
          (("2" (rewrite "sq_sq_aux")
            (("2" (rewrite "sq_div")
              (("2" (grind-reals)
                (("1" (rewrite "sq_times") (("1" (assert) nil nil))
                  nil)
                 ("2" (name-replace "AA" "sq(y!1) - x!1")
                  (("2" (expand "sq") (("2" (grind-reals) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (case "sq(y!1) > 0")
        (("1" (expand "sq" -1) (("1" (grind-reals) nil nil)) nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq_div formula-decl nil sq nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sq_times formula-decl nil sq nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (pos_times_lt formula-decl nil real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pos_div_lt formula-decl nil real_props nil)
    (sq_sq_aux formula-decl nil sqrt_approx nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (both_sides_times_pos_ge1 formula-decl nil real_props nil)
    (FDX_87 skolem-const-decl "{y | x!1 < sq(y)}" sqrt_approx nil)
    (x!1 skolem-const-decl "nnreal" sqrt_approx nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil))
   nil))
 (sqrt_newton_aux_TCC6 0
  (sqrt_newton_aux_TCC6-2 nil 3320772107
   ("" (skosimp :preds? t)
    (("" (assert)
      (("" (lift-if)
        (("" (split 2)
          (("1" (flatten) (("1" (assert) nil nil)) nil)
           ("2" (flatten)
            (("2" (case "y!1 > 0")
              (("1" (lemma "sq_sq_aux")
                (("1" (inst -1 "x!1" "y!1")
                  (("1" (replaces -1)
                    (("1" (rewrite "sq_div")
                      (("1" (rewrite "sq_times")
                        (("1" (case-replace "sq(2) = 4")
                          (("1" (lemma "log_nat_incr")
                            (("1" (inst?)
                              (("1"
                                (inst -1 "(sq(y!1)-x!1)/eps!1")
                                (("1"
                                  (assert)
                                  (("1"
                                    (hide 3)
                                    (("1"
                                      (field 1)
                                      (("1"
                                        (factor 1 r)
                                        (("1"
                                          (name-replace
                                           "AA"
                                           "sq(y!1)-x!1"
                                           :hide?
                                           nil)
                                          (("1"
                                            (expand "sq" 1 1)
                                            (("1"
                                              (cancel-by 1 "AA")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "sq" 1)
                            (("2" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (wrap-formula 1 "sq")
                (("1" (rewrite "sq_0") (("1" (grind) nil nil)) nil)
                 ("2" (grind) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (x!1 skolem-const-decl "nnreal" sqrt_approx nil)
    (y!1 skolem-const-decl "{y | x!1 < sq(y)}" sqrt_approx 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)
    (sq_div formula-decl nil sq nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (above nonempty-type-eq-decl nil integers 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_times_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonzero_times3 formula-decl nil real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (pos_times_gt formula-decl nil real_props nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (FDX_89 skolem-const-decl "posreal" sqrt_approx nil)
    (FDX_88 skolem-const-decl "nonneg_real" sqrt_approx nil)
    (div_cancel2 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (zero_times1 formula-decl nil real_props nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (pos_div_gt formula-decl nil real_props nil)
    (CBD_90 skolem-const-decl "real" sqrt_approx nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (log_nat_incr formula-decl nil log_nat nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (sq_times formula-decl nil sq nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_sq_aux formula-decl nil sqrt_approx nil)
    (sq_0 formula-decl nil sq nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil))
   nil))
 (sqrt_newton_aux_NOT_increasing 0
  (sqrt_newton_aux_NOT_increasing-1 nil 3557592665
   ("" (eval-expr "sq(2.9)")
    (("" (eval-expr "sq(2.91)")
      (("" (inst + "8.32" "8.31681" "2.9" "2.91" "0.1")
        (("1" (assert) nil nil) ("2" (grind) nil nil)
         ("3" (grind) nil nil))
        nil))
      nil))
    nil)
   ((nnreal type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (sqrt_newton_TCC1 0
  (sqrt_newton_TCC1-1 nil 3320768919 ("" (subtype-tcc) nil nil)
   ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
 (sqrt_newton_is_NOT_increasing 0
  (sqrt_newton_is_NOT_increasing-1 nil 3557676691
   ("" (eval-formula) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (sq_sqrt_newton 0
  (sq_sqrt_newton-1 nil 3321016010
   ("" (skeep)
    (("" (typepred "sqrt_newton(x, eps)") (("" (assert) nil nil)) nil))
    nil)
   ((sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}"
                 sqrt_approx nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sq const-decl "nonneg_real" sq nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   shostak))
 (sqrt_newton_gt 0
  (sqrt_newton_gt-1 nil 3321016041
   ("" (skeep)
    (("" (lemma "sq_sqrt_newton")
      (("" (inst -1 "eps" "x")
        (("" (wrap-formula -1 "sqrt")
          (("1" (rewrite "sqrt_sq") nil nil)
           ("2" (hide 2) (("2" (rewrite "sqrt_gt") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_sqrt_newton formula-decl nil sqrt_approx nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (sq const-decl "nonneg_real" sq nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}"
                 sqrt_approx nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (sqrt_sq formula-decl nil sqrt nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqrt_gt formula-decl nil sqrt nil)
    (nnreal type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (sq_nz_pos application-judgement "posreal" sq nil))
   shostak))
 (sqrt_newton_lt 0
  (sqrt_newton_lt-1 nil 3321016482
   ("" (skeep)
    (("" (cross-mult 2)
      (("" (lemma "sqrt_newton_gt")
        (("" (inst -1 "eps" "x")
          (("" (mult-by -1 "sqrt(x)") (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}"
                 sqrt_approx nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sq const-decl "nonneg_real" sq nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nnreal type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (x skolem-const-decl "nnreal" sqrt_approx nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (sqrt_newton_gt formula-decl nil sqrt_approx nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   shostak))
 (sqrt_newton_le 0
  (sqrt_newton_le-1 nil 3321016611
   ("" (skeep)
    (("" (lemma "sqrt_newton_lt")
      (("" (inst -1 "eps" "x")
        (("" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((sqrt_newton_lt formula-decl nil sqrt_approx nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (sq_nz_pos application-judgement "posreal" sq nil))
   shostak))
 (sqrt_approx_TCC1 0
  (sqrt_approx_TCC1-2 nil 3557832683
   ("" (skosimp*)
    (("" (assert)
      (("" (replaces -4)
        (("" (cross-mult 1)
          (("" (ground)
            (("1" (case "x!1*N!1>=0")
              (("1" (assert) nil)
               ("2" (assert)
                (("2" (lemma "nnreal_times_nnreal_is_nnreal")
                  (("2" (inst?) nil)))))))
             ("2" (case "2*10^n!1>=1")
              (("1" (assert) nil)
               ("2" (case "FORALL (nn:nat): 2*10^nn >=1")
                (("1" (inst?) nil)
                 ("2" (hide-all-but 1)
                  (("2" (induct "nn")
                    (("1" (grind) nil)
                     ("2" (skeep)
                      (("2" (expand "^")
                        (("2" (expand "expt" +)
                          (("2" (assert) nil))))))))))))))))))))))))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (posint_exp application-judgement "posint" exponentiation 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)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (integer nonempty-type-from-decl nil integers nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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))
   nil)
  (sqrt_approx_TCC1-1 nil 3557745411
   ("" (skeep)
    (("" (skeep)
      (("" (skosimp*)
        (("" (assert)
          (("" (typepred "floor(2*10^n)")
            (("" (assert)
              (("" (typepred "floor(1)")
                (("" (assert)
                  (("" (case "2*10^n >= 1")
                    (("1" (assert) nil nil)
                     ("2" (hide-all-but 1)
                      (("2" (case "FORALL (nn:nat): 2*10^nn >=1")
                        (("1" (inst?) nil nil)
                         ("2" (induct "nn")
                          (("1" (hide 2) (("1" (grind) nil nil)) nil)
                           ("2" (hide 2)
                            (("2" (skeep)
                              (("2"
                                (expand "^")
                                (("2"
                                  (expand "expt" +)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
 (sqrt_approx_TCC2 0
  (sqrt_approx_TCC2-2 nil 3557832760
   ("" (skeep)
    (("" (skeep)
      (("" (skeep)
        (("" (skeep)
          (("" (name "qq" "sqrt_newton(xx, 10 ^ (-n)/2)")
            (("1" (replaces -1)
              (("1" (typepred "qq")
                (("1" (hide (-1 -2))
                  (("1" (case "x >= xx AND abs(x-xx)<10^(-n)/2")
                    (("1" (flatten)
                      (("1" (grind :exclude ("sq" "floor" "^")) nil
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (split)
                        (("1" (mult-by 1 "N") (("1" (assert) nil nil))
                          nil)
                         ("2" (case "1/N = 10^(-n)/2")
                          (("1" (case "abs(x-xx)<1/N")
                            (("1" (assert)
                              (("1" (replaces -2) nil nil)) nil)
                             ("2" (hide 2)
                              (("2"
                                (cross-mult 1)
                                (("2"
                                  (ground)
                                  (("2"
                                    (lemma "abs_mult")
                                    (("2"
                                      (inst - "x-xx" "N")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "abs" - 3)
                                          (("2"
                                            (replaces -1 :dir rl)
                                            (("2"
                                              (assert)
                                              (("2"
                                                (case "N*xx = k")
                                                (("1"
                                                  (replace -1)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (replace -7)
                                                      (("1"
                                                        (hide-all-but
                                                         1)
                                                        (("1"
                                                          (grind
                                                           :exclude
                                                           ("sq"
                                                            "floor"
                                                            "^"))
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (cross-mult -7)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (cross-mult 1)
                            (("2" (assert)
                              (("2"
                                (replace -4)
                                (("2"
                                  (assert)
                                  (("2"
                                    (lemma "expt_plus")
                                    (("2"
                                      (inst - "n" "-n" "10")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (replace -1 :dir rl)
                                          (("2"
                                            (hide-all-but 1)
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (replace -4)
              (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (div_cancel4 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
     real_defs nil)
    (abs_mult formula-decl nil real_props nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (expt def-decl "real" exponentiation nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (expt_plus formula-decl nil exponentiation nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (times_div2 formula-decl nil real_props nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (div_cancel3 formula-decl nil real_props nil)
    (both_sides_times_pos_ge1 formula-decl nil real_props nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil 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)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (sq const-decl "nonneg_real" sq nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}"
                 sqrt_approx nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)
  (sqrt_approx_TCC2-1 nil 3557745411
   ("" (skosimp*)
    (("" (assert)
      (("" (replaces -4)
        (("" (cross-mult 1)
          (("" (ground)
            (("1" (case "x!1*N!1>=0")
              (("1" (assert) nil nil)
               ("2" (assert)
                (("2" (lemma "nnreal_times_nnreal_is_nnreal")
                  (("2" (inst?) nil nil)) nil))
                nil))
              nil)
             ("2" (case "2*10^n!1>=1")
              (("1" (assert) nil nil)
               ("2" (case "FORALL (nn:nat): 2*10^nn >=1")
                (("1" (inst?) nil nil)
                 ("2" (hide-all-but 1)
                  (("2" (induct "nn")
                    (("1" (grind) nil nil)
                     ("2" (skeep)
                      (("2" (expand "^")
                        (("2" (expand "expt" +)
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
 (sqrt_approx_increasing 0
  (sqrt_approx_increasing-1 nil 3557827887
   ("" (skeep)
    (("" (name "qx" "sqrt_approx(x, n)")
      (("" (name "qy" "sqrt_approx(y, n)")
        (("" (replace -1)
          (("" (replace -2)
            (("" (expand "sqrt_approx")
              (("" (invoke (name "yy" "%1") (! -1 1 1))
                (("" (replace -1)
                  (("" (invoke (name "xx" "%1") (! -3 1 1))
                    (("" (replace -1)
                      (("" (case "xx<=yy")
                        (("1"
                          (name "qxx" "sqrt_newton(xx, 10 ^ (-n) / 2)")
                          (("1"
                            (name "qyy"
                                  "sqrt_newton(yy, 10 ^ (-n) / 2)")
                            (("1" (assert)
                              (("1"
                                (case "xx = yy")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (case "NOT xx<yy")
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (hide 1)
                                    (("2"
                                      (name "N" "2*10^n")
                                      (("2"
                                        (replace -1)
                                        (("2"
                                          (case "yy-xx>=1/N")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (typepred "qxx")
                                              (("1"
                                                (typepred "qyy")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (case
                                                     "1/N = 10^(-n)/2")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (replace -1)
                                                        (("1"
                                                          (name
                                                           "epsi"
                                                           "10^(-n)/2")
                                                          (("1"
                                                            (replace
                                                             -1)
                                                            (("1"
                                                              (case
                                                               "qxx<=qyy")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil)
                                                               ("2"
                                                                (hide-all-but
                                                                 (-5
                                                                  -6
                                                                  -9
                                                                  -10
                                                                  -11
                                                                  1))
                                                                (("2"
                                                                  (case
                                                                   "NOT sq(qxx)<=sq(qyy)")
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (lemma
                                                                     "sq_le")
                                                                    (("2"
                                                                      (inst?)
                                                                      (("2"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (assert)
                                                      (("2"
                                                        (expand "N" 1)
                                                        (("2"
                                                          (cross-mult
                                                           1)
                                                          (("2"
                                                            (lemma
                                                             "expt_plus")
                                                            (("2"
                                                              (inst
                                                               -
                                                               "n"
                                                               "-n"
                                                               "10")
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (replace
                                                                   -1
                                                                   :dir
                                                                   rl)
                                                                  (("2"
                                                                    (hide-all-but
                                                                     1)
                                                                    (("2"
                                                                      (grind)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (assert)
                                            (("2"
                                              (hide-all-but (-2 1))
                                              (("2"
                                                (expand "xx")
                                                (("2"
                                                  (expand "yy")
                                                  (("2"
                                                    (expand "N")
                                                    (("2"
                                                      (case
                                                       "floor(2 * (10 ^ n * x)) <=
       floor(2 * (10 ^ n * y))-1")
                                                      (("1"
                                                        (mult-by
                                                         -1
                                                         "1/(2*10^n)")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide 2)
                                                        (("2"
                                                          (case
                                                           "floor(2 * (10 ^ n * x)) < floor(2 * (10 ^ n * y))")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil)
                                                           ("2"
                                                            (mult-by
                                                             1
                                                             "1/(2*10^n)")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert)
                          (("2"
                            (case "floor(2 * (10 ^ n * x)) <= floor(2 * (10 ^ n * y))")
                            (("1" (mult-by -1 "1/(2*10^n)")
                              (("1" (assert) nil nil)) nil)
                             ("2" (mult-by -5 "2*10^n")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sqrt_approx const-decl "{z | abs(sq(z) - x) < 10 ^ (-n) / 2}"
     sqrt_approx nil)
    (^ const-decl "real" exponentiation nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (sq const-decl "nonneg_real" sq nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (posint_times_posint_is_posint application-judgement "posint"
     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)
    (minus_int_is_int application-judgement "int" integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}"
                 sqrt_approx nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (div_cancel3 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (times_div2 formula-decl nil real_props nil)
    (div_cancel4 formula-decl nil real_props nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (expt def-decl "real" exponentiation nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (expt_plus formula-decl nil exponentiation nil)
    (N skolem-const-decl "posint" sqrt_approx nil)
    (posrat nonempty-type-eq-decl nil rationals nil)
    (sq_le formula-decl nil sq nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (yy skolem-const-decl "nonneg_rat" sqrt_approx nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (xx skolem-const-decl "nonneg_rat" sqrt_approx nil)
    (integer nonempty-type-from-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonneg_rat nonempty-type-eq-decl nil rationals nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil))
   shostak))
 (sqrt_old_bounds 0
  (sqrt_old_bounds-1 nil 3576862732
   ("" (skeep)
    (("" (split)
      (("1" (expand "sqrt_lb_old")
        (("1" (name "q" "sqrt_approx(x,2*n)")
          (("1" (replaces -1)
            (("1" (typepred "q")
              (("1" (hide -1)
                (("1" (case "NOT x > sq(q)-10 ^ (-(2 * n)) / 2")
                  (("1" (hide 2) (("1" (grind :exclude "^") nil nil))
                    nil)
                   ("2" (lemma "sqrt_gt")
                    (("2" (expand "max")
                      (("2" (lift-if)
                        (("2" (ground)
                          (("2"
                            (inst - "x" "sq(q)-10 ^ (-(2 * n)) / 2")
                            (("1" (assert)
                              (("1"
                                (case
                                 "sqrt(sq(q)-10 ^ (-(2 * n)) / 2)>=q-10 ^ (-n)")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (lemma "sq_ge")
                                  (("2"
                                    (inst?)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (rewrite "sq_minus")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (case
                                             "2 * (10 ^ (-n) * q) >= 10 ^ (-(2 * n)) / 2 + sq(10 ^ (-n))")
                                            (("1" (assert) nil nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (case
                                                 "2 * 10 ^ (-n) >= 10 ^ (-n) / 2 + 10 ^ (-n)")
                                                (("1"
                                                  (case "q>=10^(-n)")
                                                  (("1"
                                                    (mult-ineq -1 -2)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (expand "sq")
                                                        (("1"
                                                          (lemma
                                                           "expt_plus")
                                                          (("1"
                                                            (inst
                                                             -
                                                             "-n"
                                                             "-n"
                                                             "10")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (lemma "sq_ge")
                              (("2"
                                (inst - "q" "10^(-n)")
                                (("2"
                                  (assert)
                                  (("2"
                                    (expand "sq")
                                    (("2"
                                      (rewrite "expt_plus" :dir rl)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "sqrt_ub_old")
        (("2" (name "q" "sqrt_approx(x,2*n)")
          (("2" (replaces -1)
            (("2" (typepred "q")
              (("2" (hide -1)
                (("2" (case "NOT x < sq(q)+10 ^ (-(2 * n)) / 2")
                  (("1" (hide 2) (("1" (grind :exclude "^") nil nil))
                    nil)
                   ("2" (lemma "sqrt_lt")
                    (("2" (inst - "x" "sq(q)+10 ^ (-(2 * n)) / 2")
                      (("2" (assert)
                        (("2"
                          (case "sqrt(sq(q)+10 ^ (-(2 * n)) / 2)<=q+10 ^ (-n)")
                          (("1" (assert) nil nil)
                           ("2" (hide 2)
                            (("2" (lemma "sq_le")
                              (("2"
                                (inst?)
                                (("2"
                                  (assert)
                                  (("2"
                                    (rewrite "sq_plus")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (case
                                         "10 ^ (-(2 * n)) = sq(10^(-n))")
                                        (("1" (assert) nil nil)
                                         ("2"
                                          (hide-all-but 1)
                                          (("2"
                                            (expand "sq")
                                            (("2"
                                              (rewrite
                                               "expt_plus"
                                               :dir
                                               rl)
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt_approx const-decl "{z | abs(sq(z) - x) < 10 ^ (-n) / 2}"
     sqrt_approx nil)
    (^ const-decl "real" exponentiation nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (sq const-decl "nonneg_real" sq nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (sq_ge formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (expt_plus formula-decl nil exponentiation nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (ge_times_ge_any1 formula-decl nil extra_real_props nil)
    (posrat_plus_nnrat_is_posrat application-judgement "posrat"
     rationals nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq_minus formula-decl nil sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (q skolem-const-decl "{z | abs(sq(z) - x) < 10 ^ (-(2 * n)) / 2}"
     sqrt_approx nil)
    (n skolem-const-decl "nat" sqrt_approx nil)
    (x skolem-const-decl "nnreal" sqrt_approx nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_gt formula-decl nil sqrt nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sqrt_lb_old const-decl "nnreal" sqrt_approx nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (nnrat_exp application-judgement "nnrat" exponentiation 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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (<= const-decl "bool" reals nil) (sq_le formula-decl nil sq nil)
    (sq_plus formula-decl nil sq nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sqrt_lt formula-decl nil sqrt nil)
    (sqrt_ub_old const-decl "posreal" sqrt_approx nil))
   nil))
 (sqrt_approx_fast_TCC1 0
  (sqrt_approx_fast_TCC1-2 nil 3577199357
   ("" (skosimp*)
    (("" (case "abs(sq(sa!1) - x!1) < 10 ^ (-n!1) / 2")
      (("1" (expand "min")
        (("1" (lift-if)
          (("1" (ground)
            (("1" (lemma "sq_gt")
              (("1" (inst - "sa!1" "8")
                (("1" (assert)
                  (("1" (hide -5) (("1" (grind :exclude "^") nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2) (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (^ const-decl "real" exponentiation nil)
    (OR const-decl "[bool, bool -> bool]" 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)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nnreal type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (sq const-decl "nonneg_real" sq nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (sq_gt formula-decl nil sq nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq nil))
   nil)
  (sqrt_approx_fast_TCC1-1 nil 3576859786 ("" (subtype-tcc) nil nil)
   nil nil))
 (sqrt_approx_fast_TCC2 0
  (sqrt_approx_fast_TCC2-1 nil 3576859786
   ("" (skosimp*) (("" (assert) nil nil)) 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))
   nil))
 (sqrt_approx_fast_TCC3 0
  (sqrt_approx_fast_TCC3-2 nil 3577192924
   ("" (skosimp*)
    (("" (case "abs(sq(sa!1) - x!1) < 10 ^ (-n!1) / 2")
      (("1" (hide-all-but (-1 +))
        (("1" (expand "max")
          (("1" (lift-if)
            (("1" (ground)
              (("1" (lemma "sq_lt")
                (("1" (inst - "sa!1" "8")
                  (("1" (assert) (("1" (grind :exclude "^") nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 3)
        (("2"
          (case "FORALL (pr1,ab1,ab2:nnreal): pr1*min(ab1,ab2) = min(pr1*ab1,pr1*ab2)")
          (("1" (rewrite -1)
            (("1" (hide -1)
              (("1"
                (name "sa4"
                      "(2 ^ twoexp!1) * sqrt_approx(newx!1, newn!1)")
                (("1" (replace -1)
                  (("1" (case "abs(sq(sa4) - x!1) < 10 ^ (-n!1) / 2")
                    (("1" (replaces -7)
                      (("1" (expand "min" 1)
                        (("1" (lift-if)
                          (("1" (split +)
                            (("1" (flatten)
                              (("1"
                                (case "sq(2 * (2 ^ twoexp!1)) >= x!1")
                                (("1"
                                  (lemma "sq_gt")
                                  (("1"
                                    (inst - "sa4" "2*(2^twoexp!1)")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (grind
                                         :exclude
                                         ("sqrt_approx"
                                          "^"
                                          "log_nat"
                                          "floor"
                                          "^"))
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (lemma "log_nat_bounds")
                                  (("2"
                                    (inst?)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (replace -6 :dir rl)
                                          (("2"
                                            (hide-all-but (-2 1))
                                            (("2"
                                              (case
                                               "4^(1+twoexp!1) = sq(2*(2^twoexp!1))")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (hide-all-but 1)
                                                (("2"
                                                  (rewrite "sq_times")
                                                  (("2"
                                                    (expand "sq" + 1)
                                                    (("2"
                                                      (lemma
                                                       "expt_plus")
                                                      (("2"
                                                        (inst?)
                                                        (("2"
                                                          (replaces -1)
                                                          (("2"
                                                            (expand
                                                             "^"
                                                             +
                                                             1)
                                                            (("2"
                                                              (expand
                                                               "expt")
                                                              (("2"
                                                                (expand
                                                                 "expt")
                                                                (("2"
                                                                  (case
                                                                   "FORALL (ijk:nat): 4^ijk = sq(2^ijk)")
                                                                  (("1"
                                                                    (inst?)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide
                                                                     2)
                                                                    (("2"
                                                                      (induct
                                                                       "ijk")
                                                                      (("1"
                                                                        (grind)
                                                                        nil
                                                                        nil)
                                                                       ("2"
                                                                        (skeep)
                                                                        (("2"
                                                                          (expand
                                                                           "^")
                                                                          (("2"
                                                                            (expand
                                                                             "expt"
                                                                             +)
                                                                            (("2"
                                                                              (grind
                                                                               :exclude
                                                                               "expt")
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (flatten) nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (replaces -1)
                        (("2" (replaces -1 :dir rl)
                          (("2" (rewrite "sq_times")
                            (("2" (case "x!1 = newx!1*sq(2^twoexp!1)")
                              (("1"
                                (replace -1 +)
                                (("1"
                                  (lemma "abs_mult")
                                  (("1"
                                    (inst
                                     -
                                     "sq(sqrt_approx(newx!1,newn!1))-newx!1"
                                     "sq(2^twoexp!1)")
                                    (("1"
                                      (replaces -1)
                                      (("1"
                                        (expand "abs" + 2)
                                        (("1"
                                          (case
                                           "sq(2^twoexp!1) < sq(10^exp2err!1)")
                                          (("1"
                                            (mult-by
                                             -1
                                             "abs(sq(sqrt_approx(newx!1, newn!1)) - newx!1)")
                                            (("1"
                                              (invoke
                                               (case "%1 < %2")
                                               (! -1 2)
                                               (! 1 2))
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (hide (-1 2))
                                                (("2"
                                                  (lemma "expt_plus")
                                                  (("2"
                                                    (inst
                                                     -
                                                     "exp2err!1"
                                                     "exp2err!1"
                                                     "10")
                                                    (("2"
                                                      (expand "sq" 1 1)
                                                      (("2"
                                                        (mult-by
                                                         -1
                                                         "abs(sq(sqrt_approx(newx!1, newn!1)) - newx!1)")
                                                        (("2"
                                                          (replace
                                                           -1
                                                           :dir
                                                           rl)
                                                          (("2"
                                                            (hide -1)
                                                            (("2"
                                                              (mult-by
                                                               1
                                                               "10^(-2*exp2err!1)")
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (lemma
                                                                   "expt_plus")
                                                                  (("2"
                                                                    (inst
                                                                     -
                                                                     "2*exp2err!1"
                                                                     "-2*exp2err!1"
                                                                     "10")
                                                                    (("2"
                                                                      (mult-by
                                                                       -1
                                                                       "abs(sq(sqrt_approx(newx!1, newn!1)) - newx!1)")
                                                                      (("2"
                                                                        (replaces
                                                                         -1
                                                                         :dir
                                                                         rl)
                                                                        (("2"
                                                                          (assert)
                                                                          (("2"
                                                                            (expand
                                                                             "^"
                                                                             +
                                                                             1)
                                                                            (("2"
                                                                              (expand
                                                                               "expt"
                                                                               1)
                                                                              (("2"
                                                                                (assert)
                                                                                (("2"
                                                                                  (lemma
                                                                                   "expt_plus")
                                                                                  (("2"
                                                                                    (inst
                                                                                     -
                                                                                     "-n!1"
                                                                                     "-2*exp2err!1"
                                                                                     "10")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide 2)
                                            (("2"
                                              (rewrite "sq_lt")
                                              (("2"
                                                (lemma
                                                 "both_sides_expt_pos_lt_aux")
                                                (("2"
                                                  (inst
                                                   -
                                                   "exp2err!1-1"
                                                   "8"
                                                   "10")
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (case
                                                       "2^(twoexp!1) <= (2^3)^exp2err!1")
                                                      (("1"
                                                        (case
                                                         "2^3 = 8")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (replaces
                                                             -1)
                                                            (("1"
                                                              (expand
                                                               "^")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (hide-all-but
                                                           1)
                                                          (("2"
                                                            (grind)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (lemma
                                                         "mult_expt")
                                                        (("2"
                                                          (case
                                                           "(2^3)^exp2err!1 = 2^(3*exp2err!1)")
                                                          (("1"
                                                            (replaces
                                                             -1)
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (lemma
                                                                 "both_sides_expt_gt1_le_aux")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "2"
                                                                   "twoexp!1-1"
                                                                   "3*exp2err!1-1")
                                                                  (("1"
                                                                    (expand
                                                                     "^"
                                                                     1)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (lemma
                                                                       "log_nat_bounds")
                                                                      (("2"
                                                                        (inst?)
                                                                        (("2"
                                                                          (assert)
                                                                          (("2"
                                                                            (flatten)
                                                                            (("2"
                                                                              (assert)
                                                                              (("2"
                                                                                (case
                                                                                 "4 ^ (1 + log_nat(x!1, 4)`1) >= 16")
                                                                                (("1"
                                                                                  (case
                                                                                   "16 = 4^2")
                                                                                  (("1"
                                                                                    (replaces
                                                                                     -1)
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "both_sides_expt_gt1_le_aux")
                                                                                      (("1"
                                                                                        (inst
                                                                                         -
                                                                                         "4"
                                                                                         "1"
                                                                                         "log_nat(x!1, 4)`1")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "^"
                                                                                           -2)
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (hide-all-but
                                                                                     1)
                                                                                    (("2"
                                                                                      (grind)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (replace
                                                                                   -5
                                                                                   :dir
                                                                                   rl)
                                                                                  (("2"
                                                                                    (lemma
                                                                                     "log_nat_incr")
                                                                                    (("2"
                                                                                      (inst
                                                                                       -
                                                                                       "4"
                                                                                       "16"
                                                                                       "x!1")
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide -1)
                                                            (("2"
                                                              (case
                                                               "NOT 2^3 = 2*2*2")
                                                              (("1"
                                                                (hide-all-but
                                                                 1)
                                                                (("1"
                                                                  (grind)
                                                                  nil
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (replaces
                                                                 -1)
                                                                (("2"
                                                                  (lemma
                                                                   "mult_expt")
                                                                  (("2"
                                                                    (inst
                                                                     -
                                                                     "exp2err!1"
                                                                     "2"
                                                                     "2*2")
                                                                    (("2"
                                                                      (replace
                                                                       -1)
                                                                      (("2"
                                                                        (lemma
                                                                         "mult_expt")
                                                                        (("2"
                                                                          (inst
                                                                           -
                                                                           "exp2err!1"
                                                                           "2"
                                                                           "2")
                                                                          (("2"
                                                                            (replace
                                                                             -1)
                                                                            (("2"
                                                                              (rewrite
                                                                               "expt_plus"
                                                                               1
                                                                               :dir
                                                                               rl)
                                                                              (("2"
                                                                                (rewrite
                                                                                 "expt_plus"
                                                                                 1
                                                                                 :dir
                                                                                 rl)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (replace -2 +)
                                (("2"
                                  (assert)
                                  (("2"
                                    (hide-all-but 1)
                                    (("2"
                                      (case
                                       "sq(2^twoexp!1) = 4^twoexp!1")
                                      (("1" (assert) nil nil)
                                       ("2"
                                        (hide 2)
                                        (("2"
                                          (lemma "mult_expt")
                                          (("2"
                                            (inst - "twoexp!1" "2" "2")
                                            (("2"
                                              (expand "sq")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide-all-but 1)
            (("2" (skeep)
              (("2" (expand "min")
                (("2" (lift-if)
                  (("2" (lift-if)
                    (("2" (lift-if)
                      (("2" (assert)
                        (("2" (ground)
                          (("1" (mult-by -1 "pr1")
                            (("1" (assert) nil nil)) nil)
                           ("2" (mult-by 1 "pr1")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (^ const-decl "real" exponentiation nil)
    (OR const-decl "[bool, bool -> bool]" 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)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nnreal type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (sq const-decl "nonneg_real" sq nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sq_lt formula-decl nil sq nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nonneg_real_min application-judgement
     "{z: nonneg_real | z <= x AND z <= y}" real_defs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (abs_mult formula-decl nil real_props nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (nzint_times_nzint_is_nzint application-judgement "nzint" integers
     nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (even_plus_even_is_even application-judgement "even_int" integers
     nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (both_sides_times1_imp formula-decl nil extra_real_props nil)
    (newx!1 skolem-const-decl "nnreal" sqrt_approx nil)
    (newn!1 skolem-const-decl "posint" sqrt_approx nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (twoexp!1 skolem-const-decl "nat" sqrt_approx nil)
    (log_nat_incr formula-decl nil log_nat nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat
     nil)
    (both_sides_expt_gt1_le_aux formula-decl nil exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (mult_expt formula-decl nil exponentiation nil)
    (both_sides_expt_pos_lt_aux formula-decl nil exponentiation nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (log_nat_bounds formula-decl nil log_nat nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq_times formula-decl nil sq nil)
    (expt_plus formula-decl nil exponentiation nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (expt def-decl "real" exponentiation nil)
    (pred type-eq-decl nil defined_types nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (sq_gt formula-decl nil sq nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_gt_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)
    (sqrt_approx const-decl "{z | abs(sq(z) - x) < 10 ^ (-n) / 2}"
     sqrt_approx nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (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)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil)
  (sqrt_approx_fast_TCC3-1 nil 3577192784 ("" (subtype-tcc) nil nil)
   nil nil))
 (sqrt_approx_fast_increasing 0
  (sqrt_approx_fast_increasing-1 nil 3577442137
   ("" (skeep)
    (("" (expand "sqrt_approx_fast" :assert? none)
      (("" (lift-if)
        (("" (split +)
          (("1" (flatten)
            (("1" (assert)
              (("1" (lift-if)
                (("1" (split +)
                  (("1" (flatten)
                    (("1" (lemma "sqrt_approx_increasing")
                      (("1" (inst - "n" "x" "y")
                        (("1" (assert)
                          (("1" (expand "min")
                            (("1" (lift-if)
                              (("1"
                                (lift-if)
                                (("1"
                                  (lift-if)
                                  (("1" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (flatten)
                    (("2"
                      (grind :exclude
                       ("sqrt_approx" "^" "log_nat" "floor" "^"))
                      nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (flatten)
            (("2" (case "y<=64")
              (("1" (hide 2) (("1" (assert) nil nil)) nil)
               ("2" (replace 1)
                (("2" (name "twoexpx" "log_nat(x, 4)`1")
                  (("2" (replace -1)
                    (("2" (name "twoexpy" "log_nat(y, 4)`1")
                      (("2" (replace -1)
                        (("2" (assert)
                          (("2"
                            (case "FORALL (eg1,eg2:real): eg1<=eg2 IMPLIES max(eg1,8)<=max(eg2,8)")
                            (("1" (rewrite -1)
                              (("1"
                                (hide 4)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (case "twoexpx = twoexpy")
                                    (("1"
                                      (replace -1)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (div-by -4 "4^twoexpy")
                                          (("1"
                                            (lemma
                                             "sqrt_approx_increasing")
                                            (("1"
                                              (inst
                                               -
                                               "2 + 2 * floor(twoexpy / 3) + n"
                                               "x / (4 ^ twoexpy)"
                                               "y / (4 ^ twoexpy)")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (mult-by
                                                   -1
                                                   "2^twoexpy")
                                                  (("1"
                                                    (case
                                                     "FORALL (pr1,ab1:nnreal): pr1*min(ab1,2) = min(pr1*ab1,pr1*2)")
                                                    (("1"
                                                      (rewrite -1)
                                                      (("1"
                                                        (rewrite -1)
                                                        (("1"
                                                          (hide -1)
                                                          (("1"
                                                            (expand
                                                             "min")
                                                            (("1"
                                                              (lift-if)
                                                              (("1"
                                                                (lift-if)
                                                                (("1"
                                                                  (lift-if)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide-all-but 1)
                                                      (("2"
                                                        (grind)
                                                        (("1"
                                                          (mult-by
                                                           -3
                                                           "pr1!1")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (mult-by
                                                           1
                                                           "pr1!1")
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (case "twoexpx<=twoexpy")
                                      (("1"
                                        (case
                                         "2^(twoexpx+1)<=2^twoexpy")
                                        (("1"
                                          (lemma "expt_plus")
                                          (("1"
                                            (inst?)
                                            (("1"
                                              (replaces -1)
                                              (("1"
                                                (rewrite "expt_x1")
                                                (("1"
                                                  (typepred
                                                   "min(sqrt_approx(x / (4 ^ twoexpx), 2 + 2 * floor(twoexpx / 3) + n),
           2)")
                                                  (("1"
                                                    (hide (-1 -2 -3))
                                                    (("1"
                                                      (mult-by
                                                       -1
                                                       "2^twoexpx")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (case
                                                           "min(sqrt_approx(y / (4 ^ twoexpy), 2 + 2 * floor(twoexpy / 3) + n),
            2)>=1")
                                                          (("1"
                                                            (mult-by
                                                             -1
                                                             "2^twoexpy")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide 3)
                                                            (("2"
                                                              (expand
                                                               "min"
                                                               1)
                                                              (("2"
                                                                (lift-if
                                                                 1)
                                                                (("2"
                                                                  (ground)
                                                                  (("2"
                                                                    (typepred
                                                                     "log_nat(y,4)`2")
                                                                    (("2"
                                                                      (hide
                                                                       1)
                                                                      (("2"
                                                                        (hide
                                                                         -4)
                                                                        (("2"
                                                                          (replace
                                                                           -6)
                                                                          (("2"
                                                                            (div-by
                                                                             -3
                                                                             "2^twoexpy")
                                                                            (("2"
                                                                              (assert)
                                                                              (("2"
                                                                                (case
                                                                                 "NOT y/4^twoexpy >=1")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide-all-but
                                                                                   (-1
                                                                                    1))
                                                                                  (("2"
                                                                                    (name
                                                                                     "h"
                                                                                     "y/4^twoexpy")
                                                                                    (("2"
                                                                                      (replaces
                                                                                       -1)
                                                                                      (("2"
                                                                                        (name
                                                                                         "d"
                                                                                         "2 + 2 * floor(twoexpy / 3) + n")
                                                                                        (("2"
                                                                                          (case
                                                                                           "NOT d>=2")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("2"
                                                                                            (replaces
                                                                                             -2)
                                                                                            (("2"
                                                                                              (lemma
                                                                                               "sqrt_approx_increasing")
                                                                                              (("2"
                                                                                                (inst
                                                                                                 -
                                                                                                 "d"
                                                                                                 "1"
                                                                                                 "h")
                                                                                                (("2"
                                                                                                  (assert)
                                                                                                  (("2"
                                                                                                    (case
                                                                                                     "sqrt_approx(1,d)>=1")
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      nil
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (hide-all-but
                                                                                                       (-2
                                                                                                        1))
                                                                                                      (("2"
                                                                                                        (expand
                                                                                                         "sqrt_approx")
                                                                                                        (("2"
                                                                                                          (assert)
                                                                                                          (("2"
                                                                                                            (case
                                                                                                             "NOT floor(2 * 10 ^ d) / (2 * 10 ^ d) = 1")
                                                                                                            (("1"
                                                                                                              (cross-mult
                                                                                                               1)
                                                                                                              (("1"
                                                                                                                (rewrite
                                                                                                                 "floor_int")
                                                                                                                nil
                                                                                                                nil))
                                                                                                              nil)
                                                                                                             ("2"
                                                                                                              (replaces
                                                                                                               -1)
                                                                                                              (("2"
                                                                                                                (lemma
                                                                                                                 "sqrt_newton_lt")
                                                                                                                (("2"
                                                                                                                  (inst?)
                                                                                                                  (("2"
                                                                                                                    (assert)
                                                                                                                    (("2"
                                                                                                                      (cross-mult
                                                                                                                       -1)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide 3)
                                          (("2"
                                            (name "k" "twoexpx+1")
                                            (("2"
                                              (case "NOT k<=twoexpy")
                                              (("1" (assert) nil nil)
                                               ("2"
                                                (replaces -2)
                                                (("2"
                                                  (hide-all-but (-1 1))
                                                  (("2"
                                                    (case
                                                     "FORALL (ijk:nat): 2^k<=2^(k+ijk)")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "twoexpy-k")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (induct "ijk")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil)
                                                       ("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (expand "^")
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (expand
                                                               "expt"
                                                               +
                                                               2)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (assert)
                                        (("2"
                                          (hide 3)
                                          (("2"
                                            (lemma "log_nat_incr")
                                            (("2"
                                              (inst - "4" "x" "y")
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (typepred
                                                   "log_nat(y,4)`2")
                                                  (("2"
                                                    (replace -4)
                                                    (("2"
                                                      (typepred
                                                       "log_nat(x,4)`2")
                                                      (("2"
                                                        (replace -8)
                                                        (("2"
                                                          (name
                                                           "dx"
                                                           "log_nat(x,4)`2")
                                                          (("2"
                                                            (replaces
                                                             -1)
                                                            (("2"
                                                              (name
                                                               "dy"
                                                               "log_nat(y,4)`2")
                                                              (("2"
                                                                (replaces
                                                                 -1)
                                                                (("2"
                                                                  (hide
                                                                   -7)
                                                                  (("2"
                                                                    (hide
                                                                     -7)
                                                                    (("2"
                                                                      (replaces
                                                                       -3)
                                                                      (("2"
                                                                        (replace
                                                                         -5)
                                                                        (("2"
                                                                          (case
                                                                           "NOT 4^twoexpx > 4^twoexpy")
                                                                          (("1"
                                                                            (expand
                                                                             "^"
                                                                             1)
                                                                            (("1"
                                                                              (lemma
                                                                               "both_sides_expt_gt1_lt_aux")
                                                                              (("1"
                                                                                (case
                                                                                 "twoexpy>0")
                                                                                (("1"
                                                                                  (inst
                                                                                   -
                                                                                   "4"
                                                                                   "twoexpy-1"
                                                                                   "twoexpx-1")
                                                                                  (("1"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil)
                                                                                   ("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (assert)
                                                                                  (("2"
                                                                                    (case
                                                                                     "NOT twoexpy=0")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil)
                                                                                     ("2"
                                                                                      (replaces
                                                                                       -1)
                                                                                      (("2"
                                                                                        (assert)
                                                                                        (("2"
                                                                                          (case
                                                                                           "NOT 4^0=1")
                                                                                          (("1"
                                                                                            (hide-all-but
                                                                                             1)
                                                                                            (("1"
                                                                                              (grind)
                                                                                              nil
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (replaces
                                                                                             -1)
                                                                                            (("2"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (mult-by
                                                                             -2
                                                                             "4^twoexpx")
                                                                            (("2"
                                                                              (assert)
                                                                              (("2"
                                                                                (case
                                                                                 "4^twoexpx>dy*4^twoexpy")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide
                                                                                   (-1
                                                                                    2))
                                                                                  (("2"
                                                                                    (case
                                                                                     "NOT 4^twoexpx>=4*4^twoexpy")
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "both_sides_expt_gt1_le_aux")
                                                                                      (("1"
                                                                                        (inst
                                                                                         -
                                                                                         "4"
                                                                                         "twoexpy"
                                                                                         "twoexpx-1")
                                                                                        (("1"
                                                                                          (assert)
                                                                                          (("1"
                                                                                            (lemma
                                                                                             "expt_plus")
                                                                                            (("1"
                                                                                              (inst
                                                                                               -
                                                                                               "1"
                                                                                               "twoexpy"
                                                                                               "4")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "^")
                                                                                                (("1"
                                                                                                  (replaces
                                                                                                   -1)
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "expt"
                                                                                                     -
                                                                                                     1)
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "expt"
                                                                                                       -
                                                                                                       1)
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (mult-by
                                                                                       -5
                                                                                       "4^twoexpy")
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but 1)
                              (("2" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_times_posint_is_posint application-judgement "posint"
     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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_plus_even_is_even application-judgement "even_int" integers
     nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqrt_approx_fast const-decl "{z | abs(sq(z) - x) < 10 ^ (-n) / 2}"
     sqrt_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_approx_increasing formula-decl nil sqrt_approx nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
    (nnreal type-eq-decl nil real_types nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (posreal_max application-judgement
     "{z: posreal | z >= x AND z >= y}" real_defs nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (<= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat
     nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (integer nonempty-type-from-decl nil integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt_approx const-decl "{z | abs(sq(z) - x) < 10 ^ (-n) / 2}"
     sqrt_approx nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (sq const-decl "nonneg_real" sq nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (pred type-eq-decl nil defined_types nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (expt def-decl "real" exponentiation nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (twoexpy skolem-const-decl "nat" sqrt_approx nil)
    (k skolem-const-decl "posint" sqrt_approx nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (expt_plus formula-decl nil exponentiation nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (sqrt_newton const-decl "{z | x < sq(z) AND sq(z) - x < eps}"
                 sqrt_approx nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_1 formula-decl nil sqrt nil)
    (sqrt_newton_lt formula-decl nil sqrt_approx nil)
    (div_cancel3 formula-decl nil real_props nil)
    (floor_int formula-decl nil floor_ceil nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (both_sides_div1 formula-decl nil real_props nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (both_sides_expt_gt1_lt_aux formula-decl nil exponentiation nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (both_sides_expt_gt1_le_aux formula-decl nil exponentiation nil)
    (log_nat_incr formula-decl nil log_nat nil)
    (both_sides_div_pos_le1 formula-decl nil real_props nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (nonneg_real_min application-judgement
     "{z: nonneg_real | z <= x AND z <= y}" real_defs nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil))
   shostak))
 (sqrt_bounds 0
  (sqrt_bounds-1 nil 3321015664
   ("" (skeep)
    (("" (split)
      (("1" (expand "sqrt_lb")
        (("1" (name "q" "sqrt_approx_fast(x,2*n)")
          (("1" (replaces -1)
            (("1" (typepred "q")
              (("1" (hide -1)
                (("1" (case "NOT x > sq(q)-10 ^ (-(2 * n)) / 2")
                  (("1" (hide 2) (("1" (grind :exclude "^") nil nil))
                    nil)
                   ("2" (lemma "sqrt_gt")
                    (("2" (expand "max")
                      (("2" (lift-if)
                        (("2" (ground)
                          (("2"
                            (inst - "x" "sq(q)-10 ^ (-(2 * n)) / 2")
                            (("1" (assert)
                              (("1"
                                (case
                                 "sqrt(sq(q)-10 ^ (-(2 * n)) / 2)>=q-10 ^ (-n)")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (lemma "sq_ge")
                                  (("2"
                                    (inst?)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (rewrite "sq_minus")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (case
                                             "2 * (10 ^ (-n) * q) >= 10 ^ (-(2 * n)) / 2 + sq(10 ^ (-n))")
                                            (("1" (assert) nil nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (case
                                                 "2 * 10 ^ (-n) >= 10 ^ (-n) / 2 + 10 ^ (-n)")
                                                (("1"
                                                  (case "q>=10^(-n)")
                                                  (("1"
                                                    (mult-ineq -1 -2)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (expand "sq")
                                                        (("1"
                                                          (lemma
                                                           "expt_plus")
                                                          (("1"
                                                            (inst
                                                             -
                                                             "-n"
                                                             "-n"
                                                             "10")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (lemma "sq_ge")
                              (("2"
                                (inst - "q" "10^(-n)")
                                (("2"
                                  (assert)
                                  (("2"
                                    (expand "sq")
                                    (("2"
                                      (rewrite "expt_plus" :dir rl)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "sqrt_ub")
        (("2" (name "q" "sqrt_approx_fast(x,2*n)")
          (("2" (replaces -1)
            (("2" (typepred "q")
              (("2" (hide -1)
                (("2" (case "NOT x < sq(q)+10 ^ (-(2 * n)) / 2")
                  (("1" (hide 2) (("1" (grind :exclude "^") nil nil))
                    nil)
                   ("2" (lemma "sqrt_lt")
                    (("2" (inst - "x" "sq(q)+10 ^ (-(2 * n)) / 2")
                      (("2" (assert)
                        (("2"
                          (case "sqrt(sq(q)+10 ^ (-(2 * n)) / 2)<=q+10 ^ (-n)")
                          (("1" (assert) nil nil)
                           ("2" (hide 2)
                            (("2" (lemma "sq_le")
                              (("2"
                                (inst?)
                                (("2"
                                  (assert)
                                  (("2"
                                    (rewrite "sq_plus")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (case
                                         "10 ^ (-(2 * n)) = sq(10^(-n))")
                                        (("1" (assert) nil nil)
                                         ("2"
                                          (hide-all-but 1)
                                          (("2"
                                            (expand "sq")
                                            (("2"
                                              (rewrite
                                               "expt_plus"
                                               :dir
                                               rl)
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt_approx_fast const-decl "{z | abs(sq(z) - x) < 10 ^ (-n) / 2}"
     sqrt_approx nil)
    (^ const-decl "real" exponentiation nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (sq const-decl "nonneg_real" sq nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (sq_ge formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (expt_plus formula-decl nil exponentiation nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (ge_times_ge_any1 formula-decl nil extra_real_props nil)
    (posrat_plus_nnrat_is_posrat application-judgement "posrat"
     rationals nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq_minus formula-decl nil sq nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
    (q skolem-const-decl "{z | abs(sq(z) - x) < 10 ^ (-(2 * n)) / 2}"
     sqrt_approx nil)
    (n skolem-const-decl "nat" sqrt_approx nil)
    (x skolem-const-decl "nnreal" sqrt_approx nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_gt formula-decl nil sqrt nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sqrt_lb const-decl "nnreal" sqrt_approx nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (nnrat_exp application-judgement "nnrat" exponentiation 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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (<= const-decl "bool" reals nil) (sq_le formula-decl nil sq nil)
    (sq_plus formula-decl nil sq nil)
    (sqrt_pos application-judgement "posreal" sqrt nil)
    (sqrt_lt formula-decl nil sqrt nil)
    (sqrt_ub const-decl "posreal" sqrt_approx nil))
   shostak)))