Impressum acos.prf

(acos (nnreal_le_pi_TCC1 0
       (nnreal_le_pi_TCC1-1 nil 3262275870 ("" (assert) nil nil)
        ((real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil))
        shostak))
      (acos_TCC1 0
       (acos_TCC1-1 nil 3262275879
        ("" (skolem 1 ("x"))
         (("" (typepred "asin(x)")
           (("" (expand "abs" -1)
             (("" (case "asin(x) < 0")
               (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
             nil))
           nil))
         nil)
        ((asin const-decl "real_abs_le_pi2" asin nil)
         (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
         (real_abs_le1 nonempty-type-eq-decl nil asin nil)
         (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}"
          trig_basic nil)
         (pi_ub const-decl "posreal" trig_basic nil)
         (< const-decl "bool" reals nil)
         (pi_lb const-decl "posreal" trig_basic 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)
         (>= const-decl "bool" reals nil)
         (- const-decl "[numfield -> numfield]" number_fields nil)
         (/ const-decl "[numfield, nznum -> numfield]" number_fields
            nil)
         (nznum nonempty-type-eq-decl nil number_fields nil)
         (/= const-decl "boolean" notequal nil)
         (numfield nonempty-type-eq-decl nil number_fields 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_minus_real_is_real application-judgement "real" reals
          nil)
         (real_ge_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_lt_is_strict_total_order name-judgement
          "(strict_total_order?[real])" real_props nil))
        shostak))
      (acos_neg_TCC1 0
       (acos_neg_TCC1-1 nil 3262871574 ("" (grind) nil nil) nil
        shostak))
      (acos_neg 0
       (acos_neg-1 nil 3262871521
        ("" (skolem 1 ("x"))
         (("" (expand "acos")
           (("" (rewrite "asin_neg") (("" (assert) nil nil)) nil))
           nil))
         nil)
        ((posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (acos const-decl "nnreal_le_pi" acos nil)
         (real_plus_real_is_real application-judgement "real" reals
          nil)
         (minus_real_is_real application-judgement "real" reals nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (real_abs_le1 nonempty-type-eq-decl nil asin nil)
         (- const-decl "[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)
         (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)
         (asin_neg formula-decl nil asin nil))
        shostak))
      (acos_0 0
       (acos_0-1 nil 3262276429
        ("" (expand "acos")
         (("" (rewrite "asin_0") (("" (assert) nil nil)) nil)) nil)
        ((asin_0 formula-decl nil asin nil)
         (int_times_even_is_even application-judgement "even_int"
          integers nil)
         (mult_divides1 application-judgement "(divides(n))" divides
          nil)
         (mult_divides2 application-judgement "(divides(m))" divides
          nil)
         (acos const-decl "nnreal_le_pi" acos nil))
        shostak))
      (acos_sqrt_half_TCC1 0
       (acos_sqrt_half_TCC1-1 nil 3263920337
        ("" (expand "abs")
         (("" (typepred "sqrt(1/2)")
           (("" (assert)
             (("" (lemma "sq_le" ("nna" "sqrt(1/2)" "nnb" "1"))
               (("" (rewrite "sq_sqrt")
                 (("" (expand "sq" -1) (("" (propax) nil nil)) nil))
                 nil))
               nil))
             nil))
           nil))
         nil)
        ((minus_odd_is_odd application-judgement "odd_int" integers
          nil)
         (real_le_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)
         (posreal_times_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (real_ge_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (sq_sqrt formula-decl nil sqrt "reals/")
         (sq const-decl "nonneg_real" sq "reals/")
         (sq_le formula-decl nil sq "reals/")
         (posrat_div_posrat_is_posrat application-judgement "posrat"
          rationals nil)
         (sqrt_pos application-judgement "posreal" sqrt "reals/")
         (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)
         (nonneg_real nonempty-type-eq-decl nil real_types nil)
         (nnreal type-eq-decl nil real_types 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
               "reals/")
         (/= const-decl "boolean" notequal nil)
         (nznum nonempty-type-eq-decl nil number_fields nil)
         (/ const-decl "[numfield, nznum -> numfield]" number_fields
            nil)
         (> const-decl "bool" reals nil))
        shostak))
      (acos_sqrt_half 0
       (acos_sqrt_half-1 nil 3263920536
        ("" (expand "acos")
         (("" (rewrite "asin_sqrt_half") (("" (assert) nil nil)) nil))
         nil)
        ((asin_sqrt_half formula-decl nil asin nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (acos const-decl "nnreal_le_pi" acos nil))
        shostak))
      (acos_1 0
       (acos_1-1 nil 3262276459
        ("" (expand "acos")
         (("" (rewrite "asin_1") (("" (assert) nil nil)) nil)) nil)
        ((asin_1 formula-decl nil asin nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (acos const-decl "nnreal_le_pi" acos nil))
        shostak))
      (acos_minus1 0
       (acos_minus1-1 nil 3262276496
        ("" (expand "acos")
         (("" (rewrite "asin_minus1") (("" (assert) nil nil)) nil))
         nil)
        ((asin_minus1 formula-decl nil asin nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (acos const-decl "nnreal_le_pi" acos nil))
        shostak))
      (acos_minus_sqrt_half_TCC1 0
       (acos_minus_sqrt_half_TCC1-1 nil 3263920463
        ("" (lemma "acos_sqrt_half_TCC1") (("" (grind) nil nil)) nil)
        ((real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (minus_odd_is_odd application-judgement "odd_int" integers
          nil)
         (sqrt_pos application-judgement "posreal" sqrt "reals/")
         (posrat_div_posrat_is_posrat application-judgement "posrat"
          rationals nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (acos_sqrt_half_TCC1 subtype-tcc nil acos nil))
        shostak))
      (acos_minus_sqrt_half 0
       (acos_minus_sqrt_half-1 nil 3263920585
        ("" (expand "acos")
         (("" (rewrite "asin_minus_sqrt_half") (("" (assert) nil nil))
           nil))
         nil)
        ((asin_minus_sqrt_half formula-decl nil asin nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (posreal_times_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (acos const-decl "nnreal_le_pi" acos nil)
         (sqrt_pos application-judgement "posreal" sqrt "reals/"))
        shostak))
      (acos_strict_decreasing 0
       (acos_strict_decreasing-1 nil 3262276758
        ("" (expand "strict_decreasing?")
         (("" (skolem 1 ("x" "y"))
           (("" (flatten)
             (("" (expand "acos")
               (("" (lemma "asin_strict_increasing")
                 (("" (expand "strict_increasing?")
                   (("" (inst - "x" "y") (("" (assert) nil nil)) nil))
                   nil))
                 nil))
               nil))
             nil))
           nil))
         nil)
        ((acos const-decl "nnreal_le_pi" acos nil)
         (strict_increasing? const-decl "bool" real_fun_preds "reals/")
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (real_lt_is_strict_total_order name-judgement
          "(strict_total_order?[real])" real_props nil)
         (real_abs_le1 nonempty-type-eq-decl nil asin nil)
         (- const-decl "[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)
         (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)
         (asin_strict_increasing formula-decl nil asin nil)
         (strict_decreasing? const-decl "bool" real_fun_preds
          "reals/"))
        shostak))
      (acos_bij 0
       (acos_bij-1 nil 3262277267
        ("" (lemma "asin_bij")
         (("" (expand "bijective?")
           (("" (expand "injective?")
             (("" (expand "surjective?")
               (("" (expand "acos")
                 (("" (flatten)
                   (("" (split 1)
                     (("1" (skolem 1 ("x" "y"))
                       (("1" (inst -1 "x" "y")
                         (("1" (flatten) (("1" (assert) nil nil)) nil))
                         nil))
                       nil)
                      ("2" (hide -1)
                       (("2" (skolem 1 ("y"))
                         (("2" (inst - "pi/2-y")
                           (("1" (skolem - ("x"))
                             (("1" (inst + "x")
                               (("1" (assert) nil nil)) nil))
                             nil)
                            ("2" (hide 2)
                             (("2" (typepred "y")
                               (("2"
                                 (expand "abs")
                                 (("2"
                                   (case "pi/2-y<0")
                                   (("1" (assert) nil nil)
                                    ("2" (assert) nil nil))
                                   nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil))
         nil)
        ((bijective? const-decl "bool" functions nil)
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (surjective? const-decl "bool" functions nil)
         (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (/= const-decl "boolean" notequal nil)
         (nznum nonempty-type-eq-decl nil number_fields nil)
         (/ const-decl "[numfield, nznum -> numfield]" number_fields
            nil)
         (>= const-decl "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)
         (pi_lb const-decl "posreal" trig_basic nil)
         (< const-decl "bool" reals nil)
         (pi_ub const-decl "posreal" trig_basic nil)
         (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}"
          trig_basic nil)
         (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
         (- const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (nnreal type-eq-decl nil real_types nil)
         (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
         (real_times_real_is_real application-judgement "real" reals
          nil)
         (real_abs_le1 nonempty-type-eq-decl nil asin nil)
         (- const-decl "[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)
         (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)
         (acos const-decl "nnreal_le_pi" acos nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (injective? const-decl "bool" functions nil)
         (asin_bij formula-decl nil asin nil))
        shostak))
      (acos_sum_TCC1 0
       (acos_sum_TCC1-1 nil 3263920917
        ("" (skosimp*)
         (("" (typepred "nnx!1") (("" (assert) nil nil)) nil)) nil)
        ((<= const-decl "bool" reals 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_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (minus_odd_is_odd application-judgement "odd_int" integers
          nil))
        shostak))
      (acos_sum_TCC2 0
       (acos_sum_TCC2-1 nil 3263920948
        ("" (skosimp*)
         (("" (typepred "nny!1")
           (("" (lemma "sq_le" ("nna" "nny!1" "nnb" "1"))
             (("" (expand "sq") (("" (assert) nil nil)) nil)) nil))
           nil))
         nil)
        ((<= const-decl "bool" reals 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)
         (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
          real_types nil)
         (sq const-decl "nonneg_real" sq "reals/")
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (real_ge_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (sq_le formula-decl nil sq "reals/")
         (nonneg_real nonempty-type-eq-decl nil real_types nil))
        shostak))
      (acos_sum_TCC3 0
       (acos_sum_TCC3-1 nil 3263921002
        ("" (skosimp*)
         (("" (typepred "nnx!1")
           (("" (typepred "nny!1")
             (("" (lemma "sq_le" ("nna" "0" "nnb" "nnx!1"))
               (("" (lemma "sq_le" ("nna" "0" "nnb" "nny!1"))
                 (("" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1"))
                   (("" (lemma "sq_le" ("nnb" "1" "nna" "nny!1"))
                     (("" (rewrite "sq_0")
                       (("" (rewrite "sq_1")
                         (("" (expand ">=")
                           (("" (flatten)
                             (("" (replace -9)
                               ((""
                                 (replace -9)
                                 ((""
                                   (replace -9)
                                   ((""
                                     (replace -9)
                                     ((""
                                       (case "0 <= 1 - sq(nny!1)")
                                       (("1"
                                         (case "0 <= 1 - sq(nnx!1)")
                                         (("1"
                                           (lemma
                                            "sqrt_le"
                                            ("nny"
                                             "1 - sq(nny!1)"
                                             "nnz"
                                             "1"))
                                           (("1"
                                             (lemma
                                              "sqrt_le"
                                              ("nny"
                                               "1 - sq(nnx!1)"
                                               "nnz"
                                               "1"))
                                             (("1"
                                               (assert)
                                               (("1"
                                                 (rewrite "sqrt_1")
                                                 (("1"
                                                   (typepred
                                                    "sqrt(1 - sq(nnx!1)) ")
                                                   (("1"
                                                     (typepred
                                                      "sqrt(1 - sq(nny!1)) ")
                                                     (("1"
                                                       (hide -2 -4)
                                                       (("1"
                                                         (lemma
                                                          "nnreal_times_nnreal_is_nnreal"
                                                          ("nnx"
                                                           "nnx!1"
                                                           "nny"
                                                           "nny!1"))
                                                         (("1"
                                                           (lemma
                                                            "nnreal_times_nnreal_is_nnreal"
                                                            ("nnx"
                                                             "sqrt(1 - sq(nnx!1))"
                                                             "nny"
                                                             "sqrt(1 - sq(nny!1))"))
                                                           (("1"
                                                             (lemma
                                                              "le_times_le_pos"
                                                              ("nnx"
                                                               "sqrt(1 - sq(nny!1))"
                                                               "y"
                                                               "1"
                                                               "nnz"
                                                               "sqrt(1 - sq(nnx!1))"
                                                               "w"
                                                               "1"))
                                                             (("1"
                                                               (assert)
                                                               (("1"
                                                                 (lemma
                                                                  "le_times_le_pos"
                                                                  ("nnx"
                                                                   "nnx!1"
                                                                   "y"
                                                                   "1"
                                                                   "nnz"
                                                                   "nny!1"
                                                                   "w"
                                                                   "1"))
                                                                 (("1"
                                                                   (assert)
                                                                   (("1"
                                                                     (lemma
                                                                      "le_minus_le"
                                                                      ("x"
                                                                       "nnx!1 * nny!1"
                                                                       "y"
                                                                       "1"
                                                                       "w"
                                                                       "0"
                                                                       "z"
                                                                       "(sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1)))"))
                                                                     (("1"
                                                                       (lemma
                                                                        "le_minus_le"
                                                                        ("y"
                                                                         "nnx!1 * nny!1"
                                                                         "x"
                                                                         "0"
                                                                         "z"
                                                                         "1"
                                                                         "w"
                                                                         "(sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1)))"))
                                                                       (("1"
                                                                         (expand
                                                                          ">=")
                                                                         (("1"
                                                                           (replace
                                                                            -3)
                                                                           (("1"
                                                                             (replace
                                                                              -4)
                                                                             (("1"
                                                                               (replace
                                                                                -5)
                                                                               (("1"
                                                                                 (replace
                                                                                  -6)
                                                                                 (("1"
                                                                                   (expand
                                                                                    "abs"
                                                                                    1)
                                                                                   (("1"
                                                                                     (case
                                                                                      "nnx!1 * nny!1 - (sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1))) < 0")
                                                                                     (("1"
                                                                                       (assert)
                                                                                       nil
                                                                                       nil)
                                                                                      ("2"
                                                                                       (assert)
                                                                                       nil
                                                                                       nil))
                                                                                     nil))
                                                                                   nil))
                                                                                 nil))
                                                                               nil))
                                                                             nil))
                                                                           nil))
                                                                         nil))
                                                                       nil))
                                                                     nil))
                                                                   nil))
                                                                 nil))
                                                               nil))
                                                             nil))
                                                           nil))
                                                         nil))
                                                       nil))
                                                     nil))
                                                   nil))
                                                 nil))
                                               nil)
                                              ("2" (assert) nil nil))
                                             nil)
                                            ("2" (assert) nil nil))
                                           nil)
                                          ("2" (assert) nil nil))
                                         nil)
                                        ("2" (assert) nil nil))
                                       nil))
                                     nil))
                                   nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil))
         nil)
        ((<= const-decl "bool" reals 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)
         (nonneg_real nonempty-type-eq-decl nil real_types nil)
         (sq_le formula-decl nil sq "reals/")
         (sq_0 formula-decl nil sq "reals/")
         (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
          real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (numfield nonempty-type-eq-decl nil number_fields nil)
         (- const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (sq const-decl "nonneg_real" sq "reals/")
         (sqrt_le formula-decl nil sqrt "reals/")
         (real_ge_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (minus_odd_is_odd application-judgement "odd_int" integers
          nil)
         (sqrt_pos application-judgement "posreal" sqrt "reals/")
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (sqrt_1 formula-decl nil sqrt "reals/")
         (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types
          nil)
         (le_times_le_pos formula-decl nil real_props nil)
         (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt
               "reals/")
         (* const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (= const-decl "[T, T -> boolean]" equalities nil)
         (sq_1 formula-decl nil sq "reals/"))
        shostak))
      (acos_sum 0
       (acos_sum-1 nil 3263922185
        ("" (skosimp*)
         (("" (typepred "nnx!1")
           (("" (typepred "nny!1")
             (("" (expand ">=")
               (("" (lemma "sq_le" ("nna" "0" "nnb" "nnx!1"))
                 (("" (lemma "sq_le" ("nna" "0" "nnb" "nny!1"))
                   (("" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1"))
                     (("" (lemma "sq_le" ("nnb" "1" "nna" "nny!1"))
                       (("" (rewrite "sq_0")
                         (("" (rewrite "sq_1")
                           (("" (simplify -1)
                             (("" (simplify -2)
                               ((""
                                 (flatten)
                                 ((""
                                   (replace -7)
                                   ((""
                                     (replace -8)
                                     ((""
                                       (expand "<=" -8)
                                       ((""
                                         (split -8)
                                         (("1"
                                           (expand "<=" -7)
                                           (("1"
                                             (split -7)
                                             (("1"
                                               (expand "<=" -8)
                                               (("1"
                                                 (split -8)
                                                 (("1"
                                                   (expand "<=" -8)
                                                   (("1"
                                                     (split -8)
                                                     (("1"
                                                       (expand
                                                        "acos"
                                                        1)
                                                       (("1"
                                                         (lemma
                                                          "div_cancel1"
                                                          ("x"
                                                           "pi"
                                                           "n0z"
                                                           "2"))
                                                         (("1"
                                                           (replace -1)
                                                           (("1"
                                                             (hide -1)
                                                             (("1"
                                                               (hide
                                                                -5
                                                                -6
                                                                -7
                                                                -8)
                                                               (("1"
                                                                 (lemma
                                                                  "sq_lt"
                                                                  ("nna"
                                                                   "0"
                                                                   "nnb"
                                                                   "nnx!1"))
                                                                 (("1"
                                                                   (lemma
                                                                    "sq_lt"
                                                                    ("nna"
                                                                     "0"
                                                                     "nnb"
                                                                     "nny!1"))
                                                                   (("1"
                                                                     (lemma
                                                                      "sq_lt"
                                                                      ("nnb"
                                                                       "1"
                                                                       "nna"
                                                                       "nnx!1"))
                                                                     (("1"
                                                                       (lemma
                                                                        "sq_lt"
                                                                        ("nnb"
                                                                         "1"
                                                                         "nna"
                                                                         "nny!1"))
                                                                       (("1"
                                                                         (rewrite
                                                                          "sq_0")
                                                                         (("1"
                                                                           (rewrite
                                                                            "sq_1")
                                                                           (("1"
                                                                             (replace
                                                                              -5)
                                                                             (("1"
                                                                               (replace
                                                                                -6)
                                                                               (("1"
                                                                                 (replace
                                                                                  -7)
                                                                                 (("1"
                                                                                   (replace
                                                                                    -8)
                                                                                   (("1"
                                                                                     (simplify)
                                                                                     (("1"
                                                                                       (case
                                                                                        "0 < 1-sq(nnx!1)")
                                                                                       (("1"
                                                                                         (case
                                                                                          "0 < 1-sq(nny!1)")
                                                                                         (("1"
                                                                                           (case
                                                                                            "1-sq(nnx!1)<1")
                                                                                           (("1"
                                                                                             (case
                                                                                              "1-sq(nny!1)<1")
                                                                                             (("1"
                                                                                               (lemma
                                                                                                "sqrt_lt"
                                                                                                ("nny"
                                                                                                 "0"
                                                                                                 "nnz"
                                                                                                 "1-sq(nnx!1)"))
                                                                                               (("1"
                                                                                                 (lemma
                                                                                                  "sqrt_lt"
                                                                                                  ("nny"
                                                                                                   "0"
                                                                                                   "nnz"
                                                                                                   "1-sq(nny!1)"))
                                                                                                 (("1"
                                                                                                   (lemma
                                                                                                    "sqrt_lt"
                                                                                                    ("nnz"
                                                                                                     "1"
                                                                                                     "nny"
                                                                                                     "1-sq(nnx!1)"))
                                                                                                   (("1"
                                                                                                     (lemma
                                                                                                      "sqrt_lt"
                                                                                                      ("nnz"
                                                                                                       "1"
                                                                                                       "nny"
                                                                                                       "1-sq(nny!1)"))
                                                                                                     (("1"
                                                                                                       (replace
                                                                                                        -5)
                                                                                                       (("1"
                                                                                                         (replace
                                                                                                          -6)
                                                                                                         (("1"
                                                                                                           (replace
                                                                                                            -7)
                                                                                                           (("1"
                                                                                                             (replace
                                                                                                              -8)
                                                                                                             (("1"
                                                                                                               (rewrite
                                                                                                                "sqrt_1")
                                                                                                               (("1"
                                                                                                                 (rewrite
                                                                                                                  "sqrt_0")
                                                                                                                 (("1"
                                                                                                                   (simplify)
                                                                                                                   (("1"
                                                                                                                     (lemma
                                                                                                                      "posreal_times_posreal_is_posreal"
                                                                                                                      ("px"
                                                                                                                       "nnx!1"
                                                                                                                       "py"
                                                                                                                       "nny!1"))
                                                                                                                     (("1"
                                                                                                                       (lemma
                                                                                                                        "posreal_times_posreal_is_posreal"
                                                                                                                        ("px"
                                                                                                                         "sqrt(1 - sq(nny!1))"
                                                                                                                         "py"
                                                                                                                         "sqrt(1 - sq(nnx!1))"))
                                                                                                                       (("1"
                                                                                                                         (lemma
                                                                                                                          "lt_times_lt_pos1"
                                                                                                                          ("px"
                                                                                                                           "nnx!1"
                                                                                                                           "y"
                                                                                                                           "1"
                                                                                                                           "nnz"
                                                                                                                           "nny!1"
                                                                                                                           "w"
                                                                                                                           "1"))
                                                                                                                         (("1"
                                                                                                                           (lemma
                                                                                                                            "lt_times_lt_pos1"
                                                                                                                            ("px"
                                                                                                                             "sqrt(1 - sq(nny!1))"
                                                                                                                             "y"
                                                                                                                             "1"
                                                                                                                             "nnz"
                                                                                                                             "sqrt(1 - sq(nnx!1))"
                                                                                                                             "w"
                                                                                                                             "1"))
                                                                                                                           (("1"
                                                                                                                             (assert)
                                                                                                                             (("1"
                                                                                                                               (lemma
                                                                                                                                "lt_minus_lt1"
                                                                                                                                ("x"
                                                                                                                                 "nnx!1 * nny!1"
                                                                                                                                 "y"
                                                                                                                                 "1"
                                                                                                                                 "w"
                                                                                                                                 "0"
                                                                                                                                 "z"
                                                                                                                                 "sqrt(1 - sq(nny!1)) * sqrt(1 - sq(nnx!1))"))
                                                                                                                               (("1"
                                                                                                                                 (lemma
                                                                                                                                  "lt_minus_lt1"
                                                                                                                                  ("x"
                                                                                                                                   "0"
                                                                                                                                   "y"
                                                                                                                                   "nnx!1 * nny!1"
                                                                                                                                   "w"
                                                                                                                                   "sqrt(1 - sq(nny!1)) * sqrt(1 - sq(nnx!1))"
                                                                                                                                   "z"
                                                                                                                                   "1"))
                                                                                                                                 (("1"
                                                                                                                                   (replace
                                                                                                                                    -3)
                                                                                                                                   (("1"
                                                                                                                                     (expand
                                                                                                                                      ">"
                                                                                                                                      -5)
                                                                                                                                     (("1"
                                                                                                                                       (replace
                                                                                                                                        -5)
                                                                                                                                       (("1"
                                                                                                                                         (split
                                                                                                                                          -1)
                                                                                                                                         (("1"
                                                                                                                                           (split
                                                                                                                                            -2)
                                                                                                                                           (("1"
                                                                                                                                             (simplify
                                                                                                                                              (-1
                                                                                                                                               -2))
                                                                                                                                             (("1"
                                                                                                                                               (expand
                                                                                                                                                "asin")
                                                                                                                                               (("1"
                                                                                                                                                 (rewrite
                                                                                                                                                  "sq_rew"
                                                                                                                                                  1)
                                                                                                                                                 (("1"
                                                                                                                                                   (rewrite
                                                                                                                                                    "sq_rew"
                                                                                                                                                    1)
                                                                                                                                                   (("1"
                                                                                                                                                     (lemma
                                                                                                                                                      "sq_sqrt"
                                                                                                                                                      ("x"
                                                                                                                                                       "1-sq(nnx!1)"))
                                                                                                                                                     (("1"
                                                                                                                                                       (lemma
                                                                                                                                                        "sq_sqrt"
                                                                                                                                                        ("x"
                                                                                                                                                         "1-sq(nny!1)"))
                                                                                                                                                       (("1"
                                                                                                                                                         (assert)
                                                                                                                                                         (("1"
                                                                                                                                                           (name-replace
                                                                                                                                                            "SX"
                                                                                                                                                            "sqrt(1 - sq(nnx!1))")
                                                                                                                                                           (("1"
                                                                                                                                                             (name-replace
                                                                                                                                                              "SY"
                                                                                                                                                              "sqrt(1 - sq(nny!1))")
                                                                                                                                                             (("1"
                                                                                                                                                               (rewrite
                                                                                                                                                                "sq_rew"
                                                                                                                                                                1)
                                                                                                                                                               (("1"
                                                                                                                                                                 (case
                                                                                                                                                                  "1 - sq(nnx!1) * nny!1 * nny!1 - sq(SX) * SY * SY = 1-sq(nnx!1)*sq(nny!1) - sq(SX)*sq(SY)")
                                                                                                                                                                 (("1"
                                                                                                                                                                   (replace
                                                                                                                                                                    -1
                                                                                                                                                                    1)
                                                                                                                                                                   (("1"
                                                                                                                                                                     (simplify
                                                                                                                                                                      1)
                                                                                                                                                                     (("1"
                                                                                                                                                                       (hide
                                                                                                                                                                        -1)
                                                                                                                                                                       (("1"
                                                                                                                                                                         (lemma
                                                                                                                                                                          "trich_lt"
                                                                                                                                                                          ("x"
                                                                                                                                                                           "(nnx!1 / SX)*(nny!1 / SY)"
                                                                                                                                                                           "y"
                                                                                                                                                                           "1"))
                                                                                                                                                                         (("1"
                                                                                                                                                                           (case-replace
                                                                                                                                                                            "(1 - sq(SX) * sq(SY) - sq(nnx!1) * sq(nny!1) +
                    2 * (SX * SY * nnx!1 * nny!1)) = sq(SY*nnx!1+SX*nny!1)")
                                                                                                                                                                           (("1"
                                                                                                                                                                             (rewrite
                                                                                                                                                                              "sqrt_sq"
                                                                                                                                                                              1)
                                                                                                                                                                             (("1"
                                                                                                                                                                               (hide
                                                                                                                                                                                -1)
                                                                                                                                                                               (("1"
                                                                                                                                                                                 (lemma
                                                                                                                                                                                  "atan_plus"
                                                                                                                                                                                  ("x"
                                                                                                                                                                                   "nnx!1/SX"
                                                                                                                                                                                   "y"
                                                                                                                                                                                   "nny!1/SY"))
                                                                                                                                                                                 (("1"
                                                                                                                                                                                   (split
                                                                                                                                                                                    -2)
                                                                                                                                                                                   (("1"
                                                                                                                                                                                     (assert)
                                                                                                                                                                                     (("1"
                                                                                                                                                                                       (rewrite
                                                                                                                                                                                        "div_times"
                                                                                                                                                                                        -1)
                                                                                                                                                                                       (("1"
                                                                                                                                                                                         (rewrite
                                                                                                                                                                                          "div_mult_pos_lt1"
                                                                                                                                                                                          -1)
                                                                                                                                                                                         (("1"
                                                                                                                                                                                           (rewrite
                                                                                                                                                                                            "add_div"
                                                                                                                                                                                            -2)
                                                                                                                                                                                           (("1"
                                                                                                                                                                                             (lemma
                                                                                                                                                                                              "minus_div1"
                                                                                                                                                                                              ("x"
                                                                                                                                                                                               "1"
                                                                                                                                                                                               "n0x"
                                                                                                                                                                                               "1"
                                                                                                                                                                                               "y"
                                                                                                                                                                                               "nnx!1 * nny!1"
                                                                                                                                                                                               "n0y"
                                                                                                                                                                                               "SX * SY"))
                                                                                                                                                                                             (("1"
                                                                                                                                                                                               (replace
                                                                                                                                                                                                -1
                                                                                                                                                                                                -3)
                                                                                                                                                                                               (("1"
                                                                                                                                                                                                 (name-replace
                                                                                                                                                                                                  "DRL5"
                                                                                                                                                                                                  "SX * SY")
                                                                                                                                                                                                 (("1"
                                                                                                                                                                                                   (rewrite
                                                                                                                                                                                                    "div_div1"
                                                                                                                                                                                                    -3)
                                                                                                                                                                                                   (("1"
                                                                                                                                                                                                     (rewrite
                                                                                                                                                                                                      " div_cancel2"
                                                                                                                                                                                                      -3)
                                                                                                                                                                                                     (("1"
                                                                                                                                                                                                       (lemma
                                                                                                                                                                                                        "posreal_div_posreal_is_posreal"
                                                                                                                                                                                                        ("px"
                                                                                                                                                                                                         "nnx!1 * SY + nny!1 * SX"
                                                                                                                                                                                                         "py"
                                                                                                                                                                                                         "DRL5 - nnx!1 * nny!1"))
                                                                                                                                                                                                       (("1"
                                                                                                                                                                                                         (lemma
                                                                                                                                                                                                          "atan_inv"
                                                                                                                                                                                                          ("px"
                                                                                                                                                                                                           "((nnx!1 * SY + nny!1 * SX) / (DRL5 - nnx!1 * nny!1))"))
                                                                                                                                                                                                         (("1"
                                                                                                                                                                                                           (rewrite
                                                                                                                                                                                                            "div_div1"
                                                                                                                                                                                                            -1)
                                                                                                                                                                                                           (("1"
                                                                                                                                                                                                             (name-replace
                                                                                                                                                                                                              "DRL6"
                                                                                                                                                                                                              "nnx!1 * SY + nny!1 * SX")
                                                                                                                                                                                                             (("1"
                                                                                                                                                                                                               (lemma
                                                                                                                                                                                                                "atan_neg"
                                                                                                                                                                                                                ("x"
                                                                                                                                                                                                                 "(DRL5 - nnx!1 * nny!1) / DRL6"))
                                                                                                                                                                                                               (("1"
                                                                                                                                                                                                                 (assert)
                                                                                                                                                                                                                 nil
                                                                                                                                                                                                                 nil)
                                                                                                                                                                                                                ("2"
                                                                                                                                                                                                                 (hide
                                                                                                                                                                                                                  2)
                                                                                                                                                                                                                 (("2"
                                                                                                                                                                                                                   (expand
                                                                                                                                                                                                                    "DRL6")
                                                                                                                                                                                                                   (("2"
                                                                                                                                                                                                                     (lemma
                                                                                                                                                                                                                      "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                                      ("px"
                                                                                                                                                                                                                       "nnx!1"
                                                                                                                                                                                                                       "py"
                                                                                                                                                                                                                       "SY"))
                                                                                                                                                                                                                     (("2"
                                                                                                                                                                                                                       (lemma
                                                                                                                                                                                                                        "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                                        ("px"
                                                                                                                                                                                                                         "nny!1"
                                                                                                                                                                                                                         "py"
                                                                                                                                                                                                                         "SX"))
                                                                                                                                                                                                                       (("2"
                                                                                                                                                                                                                         (assert)
                                                                                                                                                                                                                         nil
                                                                                                                                                                                                                         nil))
                                                                                                                                                                                                                       nil))
                                                                                                                                                                                                                     nil))
                                                                                                                                                                                                                   nil))
                                                                                                                                                                                                                 nil))
                                                                                                                                                                                                               nil))
                                                                                                                                                                                                             nil))
                                                                                                                                                                                                           nil)
                                                                                                                                                                                                          ("2"
                                                                                                                                                                                                           (assert)
                                                                                                                                                                                                           nil
                                                                                                                                                                                                           nil)
                                                                                                                                                                                                          ("3"
                                                                                                                                                                                                           (assert)
                                                                                                                                                                                                           nil
                                                                                                                                                                                                           nil))
                                                                                                                                                                                                         nil)
                                                                                                                                                                                                        ("2"
                                                                                                                                                                                                         (assert)
                                                                                                                                                                                                         nil
                                                                                                                                                                                                         nil)
                                                                                                                                                                                                        ("3"
                                                                                                                                                                                                         (assert)
                                                                                                                                                                                                         (("3"
                                                                                                                                                                                                           (lemma
                                                                                                                                                                                                            "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                            ("px"
                                                                                                                                                                                                             "nnx!1"
                                                                                                                                                                                                             "py"
                                                                                                                                                                                                             "SY"))
                                                                                                                                                                                                           (("3"
                                                                                                                                                                                                             (lemma
                                                                                                                                                                                                              "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                              ("px"
                                                                                                                                                                                                               "nny!1"
                                                                                                                                                                                                               "py"
                                                                                                                                                                                                               "SX"))
                                                                                                                                                                                                             (("3"
                                                                                                                                                                                                               (assert)
                                                                                                                                                                                                               nil
                                                                                                                                                                                                               nil))
                                                                                                                                                                                                             nil))
                                                                                                                                                                                                           nil))
                                                                                                                                                                                                         nil))
                                                                                                                                                                                                       nil))
                                                                                                                                                                                                     nil))
                                                                                                                                                                                                   nil))
                                                                                                                                                                                                 nil))
                                                                                                                                                                                               nil))
                                                                                                                                                                                             nil))
                                                                                                                                                                                           nil))
                                                                                                                                                                                         nil))
                                                                                                                                                                                       nil))
                                                                                                                                                                                     nil)
                                                                                                                                                                                    ("2"
                                                                                                                                                                                     (assert)
                                                                                                                                                                                     (("2"
                                                                                                                                                                                       (hide
                                                                                                                                                                                        -2)
                                                                                                                                                                                       (("2"
                                                                                                                                                                                         (rewrite
                                                                                                                                                                                          "div_times"
                                                                                                                                                                                          -1)
                                                                                                                                                                                         (("2"
                                                                                                                                                                                           (lemma
                                                                                                                                                                                            "div_cancel3"
                                                                                                                                                                                            ("x"
                                                                                                                                                                                             "nnx!1*nny!1"
                                                                                                                                                                                             "y"
                                                                                                                                                                                             "1"
                                                                                                                                                                                             "n0z"
                                                                                                                                                                                             "SX*SY"))
                                                                                                                                                                                           (("2"
                                                                                                                                                                                             (replace
                                                                                                                                                                                              -2
                                                                                                                                                                                              -1)
                                                                                                                                                                                             (("2"
                                                                                                                                                                                               (flatten)
                                                                                                                                                                                               (("2"
                                                                                                                                                                                                 (replace
                                                                                                                                                                                                  -1
                                                                                                                                                                                                  1)
                                                                                                                                                                                                 (("2"
                                                                                                                                                                                                   (assert)
                                                                                                                                                                                                   (("2"
                                                                                                                                                                                                     (assert)
                                                                                                                                                                                                     (("2"
                                                                                                                                                                                                       (case-replace
                                                                                                                                                                                                        "(SX * SY - SY * SX)=0")
                                                                                                                                                                                                       (("1"
                                                                                                                                                                                                         (rewrite
                                                                                                                                                                                                          "atan_0")
                                                                                                                                                                                                         (("1"
                                                                                                                                                                                                           (lemma
                                                                                                                                                                                                            "atan_inv"
                                                                                                                                                                                                            ("px"
                                                                                                                                                                                                             "nnx!1/SX"))
                                                                                                                                                                                                           (("1"
                                                                                                                                                                                                             (rewrite
                                                                                                                                                                                                              "div_div1"
                                                                                                                                                                                                              -1)
                                                                                                                                                                                                             (("1"
                                                                                                                                                                                                               (lemma
                                                                                                                                                                                                                "cross_mult"
                                                                                                                                                                                                                ("x"
                                                                                                                                                                                                                 "SX"
                                                                                                                                                                                                                 "n0x"
                                                                                                                                                                                                                 "nnx!1"
                                                                                                                                                                                                                 "y"
                                                                                                                                                                                                                 "nny!1"
                                                                                                                                                                                                                 "n0y"
                                                                                                                                                                                                                 "SY"))
                                                                                                                                                                                                               (("1"
                                                                                                                                                                                                                 (assert)
                                                                                                                                                                                                                 nil
                                                                                                                                                                                                                 nil))
                                                                                                                                                                                                               nil))
                                                                                                                                                                                                             nil)
                                                                                                                                                                                                            ("2"
                                                                                                                                                                                                             (lemma
                                                                                                                                                                                                              "posreal_div_posreal_is_posreal"
                                                                                                                                                                                                              ("px"
                                                                                                                                                                                                               "nnx!1"
                                                                                                                                                                                                               "py"
                                                                                                                                                                                                               "SX"))
                                                                                                                                                                                                             (("2"
                                                                                                                                                                                                               (assert)
                                                                                                                                                                                                               nil
                                                                                                                                                                                                               nil))
                                                                                                                                                                                                             nil))
                                                                                                                                                                                                           nil))
                                                                                                                                                                                                         nil)
                                                                                                                                                                                                        ("2"
                                                                                                                                                                                                         (assert)
                                                                                                                                                                                                         nil
                                                                                                                                                                                                         nil))
                                                                                                                                                                                                       nil))
                                                                                                                                                                                                     nil))
                                                                                                                                                                                                   nil))
                                                                                                                                                                                                 nil))
                                                                                                                                                                                               nil))
                                                                                                                                                                                             nil))
                                                                                                                                                                                           nil))
                                                                                                                                                                                         nil))
                                                                                                                                                                                       nil))
                                                                                                                                                                                     nil)
                                                                                                                                                                                    ("3"
                                                                                                                                                                                     (assert)
                                                                                                                                                                                     (("3"
                                                                                                                                                                                       (lemma
                                                                                                                                                                                        "posreal_div_posreal_is_posreal"
                                                                                                                                                                                        ("px"
                                                                                                                                                                                         "nny!1"
                                                                                                                                                                                         "py"
                                                                                                                                                                                         "SY"))
                                                                                                                                                                                       (("3"
                                                                                                                                                                                         (assert)
                                                                                                                                                                                         (("3"
                                                                                                                                                                                           (rewrite
                                                                                                                                                                                            "div_times"
                                                                                                                                                                                            -2)
                                                                                                                                                                                           (("3"
                                                                                                                                                                                             (rewrite
                                                                                                                                                                                              "add_div"
                                                                                                                                                                                              -3)
                                                                                                                                                                                             (("3"
                                                                                                                                                                                               (lemma
                                                                                                                                                                                                "minus_div1"
                                                                                                                                                                                                ("x"
                                                                                                                                                                                                 "1"
                                                                                                                                                                                                 "n0x"
                                                                                                                                                                                                 "1"
                                                                                                                                                                                                 "y"
                                                                                                                                                                                                 "nnx!1 * nny!1"
                                                                                                                                                                                                 "n0y"
                                                                                                                                                                                                 "SX * SY"))
                                                                                                                                                                                               (("3"
                                                                                                                                                                                                 (replace
                                                                                                                                                                                                  -1
                                                                                                                                                                                                  -4)
                                                                                                                                                                                                 (("3"
                                                                                                                                                                                                   (name-replace
                                                                                                                                                                                                    "DRL5"
                                                                                                                                                                                                    "SX * SY")
                                                                                                                                                                                                   (("3"
                                                                                                                                                                                                     (rewrite
                                                                                                                                                                                                      "div_div1"
                                                                                                                                                                                                      -4)
                                                                                                                                                                                                     (("3"
                                                                                                                                                                                                       (rewrite
                                                                                                                                                                                                        " div_cancel2"
                                                                                                                                                                                                        -4)
                                                                                                                                                                                                       (("3"
                                                                                                                                                                                                         (rewrite
                                                                                                                                                                                                          "div_mult_pos_lt2"
                                                                                                                                                                                                          -3)
                                                                                                                                                                                                         (("3"
                                                                                                                                                                                                           (lemma
                                                                                                                                                                                                            "both_sides_div_neg_lt1"
                                                                                                                                                                                                            ("nz"
                                                                                                                                                                                                             "DRL5 - nnx!1 * nny!1"
                                                                                                                                                                                                             "y"
                                                                                                                                                                                                             "0"
                                                                                                                                                                                                             "x"
                                                                                                                                                                                                             "nnx!1 * SY + nny!1 * SX"))
                                                                                                                                                                                                           (("1"
                                                                                                                                                                                                             (lemma
                                                                                                                                                                                                              "atan_inv_neg"
                                                                                                                                                                                                              ("nx"
                                                                                                                                                                                                               "(nnx!1 * SY + nny!1 * SX) / (DRL5 - nnx!1 * nny!1)"))
                                                                                                                                                                                                             (("1"
                                                                                                                                                                                                               (rewrite
                                                                                                                                                                                                                "div_div1"
                                                                                                                                                                                                                -1)
                                                                                                                                                                                                               (("1"
                                                                                                                                                                                                                 (lemma
                                                                                                                                                                                                                  "atan_neg"
                                                                                                                                                                                                                  ("x"
                                                                                                                                                                                                                   "(DRL5 - nnx!1 * nny!1) / (nnx!1 * SY + nny!1 * SX)"))
                                                                                                                                                                                                                 (("1"
                                                                                                                                                                                                                   (assert)
                                                                                                                                                                                                                   nil
                                                                                                                                                                                                                   nil)
                                                                                                                                                                                                                  ("2"
                                                                                                                                                                                                                   (lemma
                                                                                                                                                                                                                    "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                                    ("px"
                                                                                                                                                                                                                     "nny!1"
                                                                                                                                                                                                                     "py"
                                                                                                                                                                                                                     "SX"))
                                                                                                                                                                                                                   (("2"
                                                                                                                                                                                                                     (lemma
                                                                                                                                                                                                                      "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                                      ("px"
                                                                                                                                                                                                                       "nnx!1"
                                                                                                                                                                                                                       "py"
                                                                                                                                                                                                                       "SY"))
                                                                                                                                                                                                                     (("2"
                                                                                                                                                                                                                       (assert)
                                                                                                                                                                                                                       nil
                                                                                                                                                                                                                       nil))
                                                                                                                                                                                                                     nil))
                                                                                                                                                                                                                   nil))
                                                                                                                                                                                                                 nil)
                                                                                                                                                                                                                ("2"
                                                                                                                                                                                                                 (lemma
                                                                                                                                                                                                                  "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                                  ("px"
                                                                                                                                                                                                                   "nnx!1"
                                                                                                                                                                                                                   "py"
                                                                                                                                                                                                                   "SY"))
                                                                                                                                                                                                                 (("2"
                                                                                                                                                                                                                   (lemma
                                                                                                                                                                                                                    "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                                    ("px"
                                                                                                                                                                                                                     "nny!1"
                                                                                                                                                                                                                     "py"
                                                                                                                                                                                                                     "SX"))
                                                                                                                                                                                                                   (("2"
                                                                                                                                                                                                                     (assert)
                                                                                                                                                                                                                     nil
                                                                                                                                                                                                                     nil))
                                                                                                                                                                                                                   nil))
                                                                                                                                                                                                                 nil))
                                                                                                                                                                                                               nil)
                                                                                                                                                                                                              ("2"
                                                                                                                                                                                                               (assert)
                                                                                                                                                                                                               (("2"
                                                                                                                                                                                                                 (lemma
                                                                                                                                                                                                                  "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                                  ("px"
                                                                                                                                                                                                                   "nny!1"
                                                                                                                                                                                                                   "py"
                                                                                                                                                                                                                   "SX"))
                                                                                                                                                                                                                 (("2"
                                                                                                                                                                                                                   (lemma
                                                                                                                                                                                                                    "posreal_times_posreal_is_posreal"
                                                                                                                                                                                                                    ("px"
                                                                                                                                                                                                                     "nnx!1"
                                                                                                                                                                                                                     "py"
                                                                                                                                                                                                                     "SY"))
                                                                                                                                                                                                                   (("2"
                                                                                                                                                                                                                     (assert)
                                                                                                                                                                                                                     (("2"
                                                                                                                                                                                                                       (assert)
                                                                                                                                                                                                                       nil
                                                                                                                                                                                                                       nil))
                                                                                                                                                                                                                     nil))
                                                                                                                                                                                                                   nil))
                                                                                                                                                                                                                 nil))
                                                                                                                                                                                                               nil)
                                                                                                                                                                                                              ("3"
                                                                                                                                                                                                               (assert)
                                                                                                                                                                                                               nil
                                                                                                                                                                                                               nil))
                                                                                                                                                                                                             nil)
                                                                                                                                                                                                            ("2"
                                                                                                                                                                                                             (assert)
                                                                                                                                                                                                             nil
                                                                                                                                                                                                             nil))
                                                                                                                                                                                                           nil))
                                                                                                                                                                                                         nil))
                                                                                                                                                                                                       nil))
                                                                                                                                                                                                     nil))
                                                                                                                                                                                                   nil))
                                                                                                                                                                                                 nil))
                                                                                                                                                                                               nil))
                                                                                                                                                                                             nil))
                                                                                                                                                                                           nil))
                                                                                                                                                                                         nil))
                                                                                                                                                                                       nil))
                                                                                                                                                                                     nil))
                                                                                                                                                                                   nil))
                                                                                                                                                                                 nil))
                                                                                                                                                                               nil))
                                                                                                                                                                             nil)
                                                                                                                                                                            ("2"
                                                                                                                                                                             (hide-all-but
                                                                                                                                                                              1)
                                                                                                                                                                             (("2"
                                                                                                                                                                               (expand
                                                                                                                                                                                "SX")
                                                                                                                                                                               (("2"
                                                                                                                                                                                 (expand
                                                                                                                                                                                  "SY")
                                                                                                                                                                                 (("2"
                                                                                                                                                                                   (rewrite
                                                                                                                                                                                    "sq_sqrt")
                                                                                                                                                                                   (("2"
                                                                                                                                                                                     (rewrite
                                                                                                                                                                                      "sq_sqrt")
                                                                                                                                                                                     (("2"
                                                                                                                                                                                       (rewrite
                                                                                                                                                                                        "sq_plus")
                                                                                                                                                                                       (("2"
                                                                                                                                                                                         (assert)
                                                                                                                                                                                         (("2"
                                                                                                                                                                                           (rewrite
                                                                                                                                                                                            "sq_times")
                                                                                                                                                                                           (("2"
                                                                                                                                                                                             (rewrite
                                                                                                                                                                                              "sq_times")
                                                                                                                                                                                             (("2"
                                                                                                                                                                                               (assert)
                                                                                                                                                                                               nil
                                                                                                                                                                                               nil))
                                                                                                                                                                                             nil))
                                                                                                                                                                                           nil))
                                                                                                                                                                                         nil))
                                                                                                                                                                                       nil))
                                                                                                                                                                                     nil))
                                                                                                                                                                                   nil))
                                                                                                                                                                                 nil))
                                                                                                                                                                               nil))
                                                                                                                                                                             nil))
                                                                                                                                                                           nil))
                                                                                                                                                                         nil))
                                                                                                                                                                       nil))
                                                                                                                                                                     nil))
                                                                                                                                                                   nil)
                                                                                                                                                                  ("2"
                                                                                                                                                                   (hide
                                                                                                                                                                    2)
                                                                                                                                                                   (("2"
                                                                                                                                                                     (expand
                                                                                                                                                                      "sq"
                                                                                                                                                                      1)
                                                                                                                                                                     (("2"
                                                                                                                                                                       (propax)
                                                                                                                                                                       nil
                                                                                                                                                                       nil))
                                                                                                                                                                     nil))
                                                                                                                                                                   nil))
                                                                                                                                                                 nil))
                                                                                                                                                               nil))
                                                                                                                                                             nil))
                                                                                                                                                           nil))
                                                                                                                                                         nil))
                                                                                                                                                       nil))
                                                                                                                                                     nil))
                                                                                                                                                   nil))
                                                                                                                                                 nil))
                                                                                                                                               nil))
                                                                                                                                             nil)
                                                                                                                                            ("2"
                                                                                                                                             (assert)
                                                                                                                                             nil
                                                                                                                                             nil))
                                                                                                                                           nil)
                                                                                                                                          ("2"
                                                                                                                                           (assert)
                                                                                                                                           nil
                                                                                                                                           nil))
                                                                                                                                         nil))
                                                                                                                                       nil))
                                                                                                                                     nil))
                                                                                                                                   nil))
                                                                                                                                 nil))
                                                                                                                               nil))
                                                                                                                             nil))
                                                                                                                           nil))
                                                                                                                         nil)
                                                                                                                        ("2"
                                                                                                                         (assert)
                                                                                                                         nil
                                                                                                                         nil)
                                                                                                                        ("3"
                                                                                                                         (assert)
                                                                                                                         nil
                                                                                                                         nil))
                                                                                                                       nil)
                                                                                                                      ("2"
                                                                                                                       (assert)
                                                                                                                       nil
                                                                                                                       nil)
                                                                                                                      ("3"
                                                                                                                       (assert)
                                                                                                                       nil
                                                                                                                       nil))
                                                                                                                     nil))
                                                                                                                   nil))
                                                                                                                 nil))
                                                                                                               nil))
                                                                                                             nil))
                                                                                                           nil))
                                                                                                         nil))
                                                                                                       nil))
                                                                                                     nil))
                                                                                                   nil))
                                                                                                 nil))
                                                                                               nil)
                                                                                              ("2"
                                                                                               (assert)
                                                                                               nil
                                                                                               nil))
                                                                                             nil)
                                                                                            ("2"
                                                                                             (assert)
                                                                                             nil
                                                                                             nil))
                                                                                           nil)
                                                                                          ("2"
                                                                                           (assert)
                                                                                           nil
                                                                                           nil))
                                                                                         nil)
                                                                                        ("2"
                                                                                         (assert)
                                                                                         nil
                                                                                         nil))
                                                                                       nil))
                                                                                     nil))
                                                                                   nil))
                                                                                 nil))
                                                                               nil))
                                                                             nil))
                                                                           nil))
                                                                         nil))
                                                                       nil))
                                                                     nil))
                                                                   nil))
                                                                 nil))
                                                               nil))
                                                             nil))
                                                           nil))
                                                         nil))
                                                       nil)
                                                      ("2"
                                                       (replace
                                                        -1
                                                        *
                                                        rl)
                                                       (("2"
                                                         (rewrite
                                                          "acos_0")
                                                         (("2"
                                                           (rewrite
                                                            "sq_0")
                                                           (("2"
                                                             (rewrite
                                                              "sqrt_1")
                                                             (("2"
                                                               (simplify
                                                                1)
                                                               (("2"
                                                                 (hide
                                                                  -1)
                                                                 (("2"
                                                                   (lemma
                                                                    "acos_neg"
                                                                    ("x"
                                                                     "sqrt(1 - sq(nnx!1))"))
                                                                   (("1"
                                                                     (replace
                                                                      -1
                                                                      1)
                                                                     (("1"
                                                                       (hide
                                                                        -1)
                                                                       (("1"
                                                                         (expand
                                                                          "acos")
                                                                         (("1"
                                                                           (lemma
                                                                            "div_cancel1"
                                                                            ("x"
                                                                             "pi"
                                                                             "n0z"
                                                                             "2"))
                                                                           (("1"
                                                                             (replace
                                                                              -1)
                                                                             (("1"
                                                                               (lemma
                                                                                "asin_pos_restrict"
                                                                                ("px"
                                                                                 "nnx!1"))
                                                                               (("1"
                                                                                 (replace
                                                                                  -1
                                                                                  1)
                                                                                 (("1"
                                                                                   (hide
                                                                                    -1)
                                                                                   (("1"
                                                                                     (expand
                                                                                      "asin"
                                                                                      1)
                                                                                     (("1"
                                                                                       (lemma
                                                                                        "sq_lt"
                                                                                        ("nna"
                                                                                         "0"
                                                                                         "nnb"
                                                                                         "nnx!1"))
                                                                                       (("1"
                                                                                         (rewrite
                                                                                          "sq_0")
                                                                                         (("1"
                                                                                           (case
                                                                                            "1 - sq(nnx!1) < 1")
                                                                                           (("1"
                                                                                             (lemma
                                                                                              "sqrt_lt"
                                                                                              ("nny"
                                                                                               "1 - sq(nnx!1)"
                                                                                               "nnz"
                                                                                               "1"))
                                                                                             (("1"
                                                                                               (rewrite
                                                                                                "sq_rew"
                                                                                                1)
                                                                                               (("1"
                                                                                                 (rewrite
                                                                                                  "sq_rew"
                                                                                                  1)
                                                                                                 (("1"
                                                                                                   (simplify
                                                                                                    1)
                                                                                                   (("1"
                                                                                                     (rewrite
                                                                                                      "sqrt_sq"
                                                                                                      1)
                                                                                                     (("1"
                                                                                                       (rewrite
                                                                                                        "sqrt_1")
                                                                                                       (("1"
                                                                                                         (assert)
                                                                                                         nil
                                                                                                         nil))
                                                                                                       nil))
                                                                                                     nil))
                                                                                                   nil))
                                                                                                 nil))
                                                                                               nil))
                                                                                             nil)
                                                                                            ("2"
                                                                                             (hide
                                                                                              2)
                                                                                             (("2"
                                                                                               (assert)
                                                                                               nil
                                                                                               nil))
                                                                                             nil))
                                                                                           nil))
                                                                                         nil))
                                                                                       nil))
                                                                                     nil))
                                                                                   nil))
                                                                                 nil)
                                                                                ("2"
                                                                                 (expand
                                                                                  "abs"
                                                                                  1)
                                                                                 (("2"
                                                                                   (propax)
                                                                                   nil
                                                                                   nil))
                                                                                 nil))
                                                                               nil))
                                                                             nil))
                                                                           nil))
                                                                         nil))
                                                                       nil))
                                                                     nil)
                                                                    ("2"
                                                                     (expand
                                                                      "abs"
                                                                      1)
                                                                     (("2"
                                                                       (hide
                                                                        2)
                                                                       (("2"
                                                                         (case
                                                                          "1 - sq(nnx!1) <= 1")
                                                                         (("1"
                                                                           (lemma
                                                                            "sqrt_le"
                                                                            ("nny"
                                                                             "1 - sq(nnx!1)"
                                                                             "nnz"
                                                                             "1"))
                                                                           (("1"
                                                                             (rewrite
                                                                              "sqrt_1")
                                                                             (("1"
                                                                               (assert)
                                                                               nil
                                                                               nil))
                                                                             nil))
                                                                           nil)
                                                                          ("2"
                                                                           (assert)
                                                                           nil
                                                                           nil))
                                                                         nil))
                                                                       nil))
                                                                     nil))
                                                                   nil))
                                                                 nil))
                                                               nil))
                                                             nil))
                                                           nil))
                                                         nil))
                                                       nil))
                                                     nil))
                                                   nil)
                                                  ("2"
                                                   (replace -1 * rl)
                                                   (("2"
                                                     (rewrite "sq_0")
                                                     (("2"
                                                       (rewrite
                                                        "sqrt_1")
                                                       (("2"
                                                         (rewrite
                                                          "acos_0")
                                                         (("2"
                                                           (simplify 1)
                                                           (("2"
                                                             (lemma
                                                              "acos_neg"
                                                              ("x"
                                                               "sqrt(1 - sq(nny!1))"))
                                                             (("1"
                                                               (replace
                                                                -1)
                                                               (("1"
                                                                 (hide
                                                                  -1)
                                                                 (("1"
                                                                   (expand
                                                                    "acos")
                                                                   (("1"
                                                                     (lemma
                                                                      "div_cancel1"
                                                                      ("x"
                                                                       "pi"
                                                                       "n0z"
                                                                       "2"))
                                                                     (("1"
                                                                       (replace
                                                                        -1)
                                                                       (("1"
                                                                         (expand
                                                                          "<="
                                                                          -9)
                                                                         (("1"
                                                                           (split
                                                                            -9)
                                                                           (("1"
                                                                             (lemma
                                                                              "asin_pos_restrict"
                                                                              ("px"
                                                                               "nny!1"))
                                                                             (("1"
                                                                               (replace
                                                                                -1
                                                                                1)
                                                                               (("1"
                                                                                 (expand
                                                                                  "asin"
                                                                                  1)
                                                                                 (("1"
                                                                                   (rewrite
                                                                                    "sq_rew"
                                                                                    1)
                                                                                   (("1"
                                                                                     (rewrite
                                                                                      "sq_rew"
                                                                                      1)
                                                                                     (("1"
                                                                                       (simplify
                                                                                        1)
                                                                                       (("1"
                                                                                         (rewrite
                                                                                          "sqrt_sq")
                                                                                         (("1"
                                                                                           (lemma
                                                                                            "sq_lt"
                                                                                            ("nna"
                                                                                             "nny!1"
                                                                                             "nnb"
                                                                                             "1"))
                                                                                           (("1"
                                                                                             (rewrite
                                                                                              "sq_1")
                                                                                             (("1"
                                                                                               (case
                                                                                                "1 - sq(nny!1) < 1")
                                                                                               (("1"
                                                                                                 (lemma
                                                                                                  "sqrt_lt"
                                                                                                  ("nny"
                                                                                                   "1 - sq(nny!1)"
                                                                                                   "nnz"
                                                                                                   "1"))
                                                                                                 (("1"
                                                                                                   (rewrite
                                                                                                    "sqrt_1")
                                                                                                   (("1"
                                                                                                     (assert)
                                                                                                     nil
                                                                                                     nil))
                                                                                                   nil))
                                                                                                 nil)
                                                                                                ("2"
                                                                                                 (lemma
                                                                                                  "sq_lt"
                                                                                                  ("nna"
                                                                                                   "0"
                                                                                                   "nnb"
                                                                                                   "nny!1"))
                                                                                                 (("2"
                                                                                                   (rewrite
                                                                                                    "sq_0")
                                                                                                   (("2"
                                                                                                     (assert)
                                                                                                     nil
                                                                                                     nil))
                                                                                                   nil))
                                                                                                 nil))
                                                                                               nil))
                                                                                             nil))
                                                                                           nil))
                                                                                         nil))
                                                                                       nil))
                                                                                     nil))
                                                                                   nil))
                                                                                 nil))
                                                                               nil)
                                                                              ("2"
                                                                               (expand
                                                                                "abs"
                                                                                1)
                                                                               (("2"
                                                                                 (propax)
                                                                                 nil
                                                                                 nil))
                                                                               nil))
                                                                             nil)
                                                                            ("2"
                                                                             (replace
                                                                              -1
                                                                              *
                                                                              rl)
                                                                             (("2"
                                                                               (rewrite
                                                                                "asin_0")
                                                                               (("2"
                                                                                 (rewrite
                                                                                  "sq_0")
                                                                                 (("2"
                                                                                   (rewrite
                                                                                    "sqrt_1")
                                                                                   (("2"
                                                                                     (rewrite
                                                                                      "asin_1")
                                                                                     (("2"
                                                                                       (assert)
                                                                                       nil
                                                                                       nil))
                                                                                     nil))
                                                                                   nil))
                                                                                 nil))
                                                                               nil))
                                                                             nil))
                                                                           nil))
                                                                         nil))
                                                                       nil))
                                                                     nil))
                                                                   nil))
                                                                 nil))
                                                               nil)
                                                              ("2"
                                                               (expand
                                                                "abs"
                                                                1)
                                                               (("2"
                                                                 (hide
                                                                  2)
                                                                 (("2"
                                                                   (lemma
                                                                    "sq_le"
                                                                    ("nna"
                                                                     "0"
                                                                     "nnb"
                                                                     "nny!1"))
                                                                   (("2"
                                                                     (rewrite
                                                                      "sq_0")
                                                                     (("2"
                                                                       (lemma
                                                                        "sqrt_le"
                                                                        ("nny"
                                                                         "1-sq(nny!1)"
                                                                         "nnz"
                                                                         "1"))
                                                                       (("2"
                                                                         (rewrite
                                                                          "sqrt_1")
                                                                         (("2"
                                                                           (assert)
                                                                           nil
                                                                           nil))
                                                                         nil))
                                                                       nil))
                                                                     nil))
                                                                   nil))
                                                                 nil))
                                                               nil))
                                                             nil))
                                                           nil))
                                                         nil))
                                                       nil))
                                                     nil))
                                                   nil))
                                                 nil))
                                               nil)
                                              ("2"
                                               (replace -1)
                                               (("2"
                                                 (rewrite "acos_1")
                                                 (("2"
                                                   (rewrite "sq_1")
                                                   (("2"
                                                     (rewrite "sqrt_0")
                                                     (("2"
                                                       (assert)
                                                       nil
                                                       nil))
                                                     nil))
                                                   nil))
                                                 nil))
                                               nil))
                                             nil))
                                           nil)
                                          ("2"
                                           (replace -1)
                                           (("2"
                                             (rewrite "sq_1")
                                             (("2"
                                               (rewrite "sqrt_0")
                                               (("2"
                                                 (rewrite "acos_1")
                                                 (("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)
        ((<= const-decl "bool" reals 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)
         (sq_1 formula-decl nil sq "reals/")
         (sq_nz_pos application-judgement "posreal" sq "reals/")
         (acos_1 formula-decl nil acos nil)
         (posreal_plus_nnreal_is_posreal application-judgement
          "posreal" real_types nil)
         (asin_0 formula-decl nil asin nil)
         (asin_1 formula-decl nil asin nil)
         (nnreal_plus_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (acos_neg formula-decl nil acos nil)
         (- const-decl "[numfield -> numfield]" number_fields nil)
         (real_abs_le1 nonempty-type-eq-decl nil asin nil)
         (asin_pos_restrict formula-decl nil asin nil)
         (sqrt_le formula-decl nil sqrt "reals/")
         (acos_0 formula-decl nil acos nil)
         (posreal_div_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (acos const-decl "nnreal_le_pi" acos nil)
         (posreal_times_posreal_is_posreal application-judgement
          "posreal" real_types nil)
         (real_minus_real_is_real application-judgement "real" reals
          nil)
         (minus_odd_is_odd application-judgement "odd_int" integers
          nil)
         (real_times_real_is_real application-judgement "real" reals
          nil)
         (numfield nonempty-type-eq-decl nil number_fields nil)
         (- const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (sq const-decl "nonneg_real" sq "reals/")
         (sqrt_lt formula-decl nil sqrt "reals/")
         (real_ge_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (sqrt_1 formula-decl nil sqrt "reals/")
         (real_plus_real_is_real application-judgement "real" reals
          nil)
         (= const-decl "[T, T -> boolean]" equalities nil)
         (* const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt
               "reals/")
         (lt_minus_lt1 formula-decl nil real_props nil)
         (asin const-decl "real_abs_le_pi2" asin nil)
         (+ const-decl "[numfield, numfield -> numfield]" number_fields
            nil)
         (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
          real_types nil)
         (div_times formula-decl nil real_props nil)
         (add_div formula-decl nil real_props nil)
         (posrat_div_posrat_is_posrat application-judgement "posrat"
          rationals nil)
         (div_div1 formula-decl nil real_props nil)
         (posreal_div_posreal_is_posreal judgement-tcc nil real_types
          nil)
         (atan_neg formula-decl nil atan nil)
         (minus_real_is_real application-judgement "real" reals nil)
         (atan_inv formula-decl nil atan nil)
         (div_cancel2 formula-decl nil real_props nil)
         (minus_div1 formula-decl nil real_props nil)
         (div_mult_pos_lt1 formula-decl nil real_props nil)
         (div_cancel3 formula-decl nil real_props nil)
         (cross_mult formula-decl nil real_props nil)
         (atan_0 formula-decl nil atan nil)
         (both_sides_div_neg_lt1 formula-decl nil real_props nil)
         (nonpos_real nonempty-type-eq-decl nil real_types nil)
         (negreal nonempty-type-eq-decl nil real_types nil)
         (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (atan_inv_neg formula-decl nil atan nil)
         (div_mult_pos_lt2 formula-decl nil real_props nil)
         (atan_plus formula-decl nil atan nil)
         (sqrt_sq formula-decl nil sqrt "reals/")
         (SX skolem-const-decl
          "{nnz: nnreal | nnz * nnz = 1 - sq(nnx!1)}" acos nil)
         (sq_plus formula-decl nil sq "reals/")
         (sq_times formula-decl nil sq "reals/")
         (SY skolem-const-decl
          "{nnz: nnreal | nnz * nnz = 1 - sq(nny!1)}" acos nil)
         (/ const-decl "[numfield, nznum -> numfield]" number_fields
            nil)
         (nznum nonempty-type-eq-decl nil number_fields nil)
         (trich_lt formula-decl nil real_props nil)
         (real_div_nzreal_is_real application-judgement "real" reals
          nil)
         (sq_sqrt formula-decl nil sqrt "reals/")
         (sq_rew formula-decl nil sq "reals/")
         (even_minus_odd_is_odd application-judgement "odd_int"
          integers nil)
         (odd_minus_even_is_odd application-judgement "odd_int"
          integers nil)
         (lt_times_lt_pos1 formula-decl nil real_props nil)
         (real_gt_is_strict_total_order name-judgement
          "(strict_total_order?[real])" real_props nil)
         (posreal_times_posreal_is_posreal judgement-tcc nil real_types
          nil)
         (sqrt_0 formula-decl nil sqrt "reals/")
         (minus_nzreal_is_nzreal application-judgement "nzreal"
          real_types nil)
         (real_lt_is_strict_total_order name-judgement
          "(strict_total_order?[real])" real_props nil)
         (sq_lt formula-decl nil sq "reals/")
         (div_cancel1 formula-decl nil real_props nil)
         (/= const-decl "boolean" notequal nil)
         (nonzero_real nonempty-type-eq-decl nil reals nil)
         (> const-decl "bool" reals nil)
         (posreal nonempty-type-eq-decl nil real_types nil)
         (AND const-decl "[bool, bool -> bool]" booleans nil)
         (pi_lb const-decl "posreal" trig_basic nil)
         (< const-decl "bool" reals nil)
         (pi_ub const-decl "posreal" trig_basic nil)
         (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}"
          trig_basic nil)
         (real_le_is_total_order name-judgement "(total_order?[real])"
          real_props nil)
         (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
          real_types nil)
         (sq_0 formula-decl nil sq "reals/")
         (sq_le formula-decl nil sq "reals/")
         (nonneg_real nonempty-type-eq-decl nil real_types nil))
        shostak)))