Impressum law_cosines.prf

(law_cosines
 (distance_refl 0
  (distance_refl-1 nil 3269434431
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        (("" (assert)
          (("" (expand "sq") (("" (rewrite "sqrt_0") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nonneg_real" law_cosines nil)
    (sq_0 formula-decl nil sq "reals/")
    (sqrt_0 formula-decl nil sqrt "reals/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_dist const-decl "nonneg_real" law_cosines nil))
   nil))
 (distance_symm 0
  (distance_symm-1 nil 3269434431
   ("" (skolem 1 ("x0" "y0" "x1" "y1"))
    (("" (expand "dist")
      (("" (expand "sq_dist") (("" (grind) nil nil)) nil)) nil))
    nil)
   ((dist const-decl "nonneg_real" law_cosines nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_dist const-decl "nonneg_real" law_cosines nil))
   nil))
 (distance_trans 0
  (distance_trans-1 nil 3269668543
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((dist const-decl "nonneg_real" law_cosines nil)
    (sq_dist const-decl "nonneg_real" law_cosines nil))
   shostak))
 (distance_scale 0
  (distance_scale-1 nil 3269668008
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        (("" (lemma "sq_times")
          (("" (inst-cp - "pz!1" "x0!1-x1!1")
            (("" (inst - "pz!1" "y0!1-y1!1")
              (("" (lemma "sqrt_times")
                ((""
                  (inst - "sq(pz!1)"
                   "sq(x0!1 - x1!1) + sq(y0!1 - y1!1)")
                  (("" (rewrite "sqrt_sq") (("" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nonneg_real" law_cosines nil)
    (sq_times formula-decl nil sq "reals/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sqrt_sq formula-decl nil sqrt "reals/")
    (sqrt_times formula-decl nil sqrt "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_dist const-decl "nonneg_real" law_cosines nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (distance_rot 0
  (distance_rot-1 nil 3269668867
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        (("" (name "KX" "x0!1 - x1!1")
          (("" (name "KY" "y0!1 - y1!1")
            ((""
              (case "(cos(ac!1) * x0!1 + sin(ac!1) * y1!1 - cos(ac!1) * x1!1 -
                sin(ac!1) * y0!1) = cos(ac!1)*KX - sin(ac!1)*KY")
              (("1" (replace -1)
                (("1"
                  (case "(cos(ac!1) * y0!1 + sin(ac!1) * x0!1 - cos(ac!1) * y1!1 -
                 sin(ac!1) * x1!1) = sin(ac!1)*KX +cos(ac!1)*KY")
                  (("1" (replace -1)
                    (("1" (replace -3)
                      (("1" (replace -4)
                        (("1" (hide-all-but 1)
                          (("1" (lemma "sin2_cos2" ("a" "ac!1"))
                            (("1" (name-replace "SIN" "sin(ac!1)")
                              (("1"
                                (name-replace "COS" "cos(ac!1)")
                                (("1"
                                  (expand "sq")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2 -1)
                    (("2" (expand "KX")
                      (("2" (expand "KY") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "KY")
                (("2" (expand "KX") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sin_range application-judgement "trig_range" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (dist const-decl "nonneg_real" law_cosines 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (cos const-decl "real" sincos_def nil)
    (sin const-decl "real" sincos_def nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (trig_range type-eq-decl nil sincos_def nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sin2_cos2 formula-decl nil trig_basic nil)
    (KX skolem-const-decl "real" law_cosines nil)
    (KY skolem-const-decl "real" law_cosines nil)
    (sq_dist const-decl "nonneg_real" law_cosines nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (dot_product 0
  (dot_product-2 nil 3286013993
   ("" (stop-rewrite "sq_sqrt")
    (("" (skosimp*)
      (("" (lemma "distance_trans" ("x2" "-x1!1" "y2" "-y1!1"))
        (("" (inst-cp - "x1!1" "x0!1" "y1!1" "y0!1")
          (("" (replace -2)
            (("" (inst-cp - "x2!1" "x0!1" "y2!1" "y0!1")
              (("" (replace -2)
                (("" (inst - "x2!1" "x1!1" "y2!1" "y1!1")
                  (("" (replace -1)
                    (("" (hide-all-but 1)
                      (("" (name-replace "X0" "x0!1 - x1!1")
                        (("" (name-replace "Y0" "y0!1 - y1!1")
                          (("" (name-replace "X2" "x2!1 - x1!1")
                            (("" (name-replace "Y2" "y2!1 - y1!1")
                              ((""
                                (assert)
                                ((""
                                  (expand "dist")
                                  ((""
                                    (expand "sq_dist")
                                    ((""
                                      (lemma "sq_neg")
                                      ((""
                                        (inst-cp - "X0")
                                        ((""
                                          (inst-cp - "Y0")
                                          ((""
                                            (replace -2)
                                            ((""
                                              (replace -3)
                                              ((""
                                                (lemma "sqrt_times")
                                                ((""
                                                  (inst
                                                   -
                                                   "sq(X0) + sq(Y0)"
                                                   "sq(X2) + sq(Y2)")
                                                  ((""
                                                    (case
                                                     "-1 * -x1!1 - x1!1 = 0")
                                                    (("1"
                                                      (simplify -2)
                                                      (("1"
                                                        (case
                                                         "abs(X0 * X2 + Y0 * Y2) <= sqrt(sq(X0) + sq(Y0)) * sqrt(sq(X2) + sq(Y2))")
                                                        (("1"
                                                          (typepred
                                                           "sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) +
                  (sq(X2) * sq(Y0) + sq(Y0) * sq(Y2)))")
                                                          (("1"
                                                            (expand
                                                             ">="
                                                             -1)
                                                            (("1"
                                                              (expand
                                                               "<="
                                                               -1)
                                                              (("1"
                                                                (split
                                                                 -1)
                                                                (("1"
                                                                  (case
                                                                   "-1<= (X0 * X2 + Y0 * Y2)/sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) +
                          sq(Y0) * sq(Y2))")
                                                                  (("1"
                                                                    (case
                                                                     "(X0 * X2 + Y0 * Y2) /
                       sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) +
                             sq(Y0) * sq(Y2)) <= 1")
                                                                    (("1"
                                                                      (name-replace
                                                                       "DEN"
                                                                       "sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) +
                          sq(Y0) * sq(Y2))")
                                                                      (("1"
                                                                        (name-replace
                                                                         "NUM"
                                                                         "X0 * X2 + Y0 * Y2")
                                                                        (("1"
                                                                          (inst
                                                                           +
                                                                           "acos(NUM/DEN)")
                                                                          (("1"
                                                                            (lemma
                                                                             "div_cancel4"
                                                                             ("y"
                                                                              "cos(acos(NUM / DEN))"
                                                                              "n0z"
                                                                              "sqrt(sq(X0) + sq(Y0)) * sqrt(sq(X2) + sq(Y2))"
                                                                              "x"
                                                                              "NUM"))
                                                                            (("1"
                                                                              (hide-all-but
                                                                               (-2
                                                                                -3
                                                                                -4
                                                                                1))
                                                                              (("1"
                                                                                (name-replace
                                                                                 "K10"
                                                                                 "NUM / DEN")
                                                                                (("1"
                                                                                  (hide
                                                                                   -3)
                                                                                  (("1"
                                                                                    (typepred
                                                                                     "acos(K10)")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "cos")
                                                                                      (("1"
                                                                                        (case
                                                                                         "floor(acos(K10) / (2 * pi))=0")
                                                                                        (("1"
                                                                                          (replace
                                                                                           -1)
                                                                                          (("1"
                                                                                            (simplify
                                                                                             1)
                                                                                            (("1"
                                                                                              (expand
                                                                                               "<="
                                                                                               -3)
                                                                                              (("1"
                                                                                                (split
                                                                                                 -3)
                                                                                                (("1"
                                                                                                  (hide
                                                                                                   -2)
                                                                                                  (("1"
                                                                                                    (lemma
                                                                                                     "phase_cos_q1"
                                                                                                     ("x"
                                                                                                      "acos(K10)"))
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "cos_phase")
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         ">=")
                                                                                                        (("1"
                                                                                                          (replace
                                                                                                           -2)
                                                                                                          (("1"
                                                                                                            (replace
                                                                                                             -3)
                                                                                                            (("1"
                                                                                                              (flatten
                                                                                                               -1)
                                                                                                              (("1"
                                                                                                                (replace
                                                                                                                 -1)
                                                                                                                (("1"
                                                                                                                  (lemma
                                                                                                                   "cos_value_acos"
                                                                                                                   ("xa"
                                                                                                                    "K10"))
                                                                                                                  (("1"
                                                                                                                    (replaces
                                                                                                                     -1)
                                                                                                                    (("1"
                                                                                                                      (expand
                                                                                                                       "K10")
                                                                                                                      (("1"
                                                                                                                        (cross-mult
                                                                                                                         1)
                                                                                                                        (("1"
                                                                                                                          (cancel-by
                                                                                                                           1
                                                                                                                           "NUM")
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "DEN"
                                                                                                                             2)
                                                                                                                            (("1"
                                                                                                                              (both-sides-f
                                                                                                                               2
                                                                                                                               "sq")
                                                                                                                              (("1"
                                                                                                                                (grind)
                                                                                                                                nil
                                                                                                                                nil)
                                                                                                                               ("2"
                                                                                                                                (rewrite
                                                                                                                                 "sq_eq")
                                                                                                                                nil
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (replace
                                                                                                   -1)
                                                                                                  (("2"
                                                                                                    (rewrite
                                                                                                     "cos_phase_pi")
                                                                                                    (("2"
                                                                                                      (lemma
                                                                                                       "acos_bij")
                                                                                                      (("2"
                                                                                                        (lemma
                                                                                                         "acos_minus1")
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "bijective?")
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "injective?")
                                                                                                            (("2"
                                                                                                              (flatten
                                                                                                               -2)
                                                                                                              (("2"
                                                                                                                (inst
                                                                                                                 -
                                                                                                                 "K10"
                                                                                                                 "-1")
                                                                                                                (("2"
                                                                                                                  (assert)
                                                                                                                  (("2"
                                                                                                                    (expand
                                                                                                                     "K10")
                                                                                                                    (("2"
                                                                                                                      (cross-mult
                                                                                                                       -2)
                                                                                                                      (("2"
                                                                                                                        (replaces
                                                                                                                         -2)
                                                                                                                        (("2"
                                                                                                                          (neg-formula
                                                                                                                           1)
                                                                                                                          (("2"
                                                                                                                            (expand
                                                                                                                             "DEN"
                                                                                                                             1)
                                                                                                                            (("2"
                                                                                                                              (both-sides-f
                                                                                                                               1
                                                                                                                               "sq")
                                                                                                                              (("1"
                                                                                                                                (grind)
                                                                                                                                nil
                                                                                                                                nil)
                                                                                                                               ("2"
                                                                                                                                (rewrite
                                                                                                                                 "sq_eq")
                                                                                                                                nil
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (name-replace
                                                                                           "K11"
                                                                                           "acos(K10)")
                                                                                          (("2"
                                                                                            (hide
                                                                                             -3
                                                                                             -4
                                                                                             2)
                                                                                            (("2"
                                                                                              (lemma
                                                                                               "floor_def"
                                                                                               ("x"
                                                                                                "K11 / (2 * pi)"))
                                                                                              (("2"
                                                                                                (rewrite
                                                                                                 "div_mult_pos_lt1")
                                                                                                (("2"
                                                                                                  (rewrite
                                                                                                   "div_mult_pos_le2")
                                                                                                  (("2"
                                                                                                    (flatten
                                                                                                     -1)
                                                                                                    (("2"
                                                                                                      (name-replace
                                                                                                       "K12"
                                                                                                       "floor(K11 / (2 * pi))")
                                                                                                      (("2"
                                                                                                        (case
                                                                                                         "K12>=1")
                                                                                                        (("1"
                                                                                                          (lemma
                                                                                                           "both_sides_times_pos_ge1"
                                                                                                           ("x"
                                                                                                            "K12"
                                                                                                            "y"
                                                                                                            "1"
                                                                                                            "pz"
                                                                                                            "2*pi"))
                                                                                                          (("1"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (case
                                                                                                           "K12<=-1")
                                                                                                          (("1"
                                                                                                            (lemma
                                                                                                             "both_sides_times_pos_le1"
                                                                                                             ("x"
                                                                                                              "K12"
                                                                                                              "y"
                                                                                                              "-1"
                                                                                                              "pz"
                                                                                                              "2*pi"))
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil)
                                                                                                           ("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (case
                                                                               "NUM / DEN < 0")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (expand
                                                                             "abs")
                                                                            (("2"
                                                                              (case
                                                                               "NUM / DEN < 0")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       -1
                                                                       2)
                                                                      (("2"
                                                                        (rewrite
                                                                         "div_mult_pos_le1"
                                                                         1)
                                                                        (("2"
                                                                          (expand
                                                                           "abs"
                                                                           -3)
                                                                          (("2"
                                                                            (case
                                                                             "X0 * X2 + Y0 * Y2 < 0")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil)
                                                                             ("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide
                                                                     2)
                                                                    (("2"
                                                                      (replace
                                                                       -5
                                                                       -3
                                                                       rl)
                                                                      (("2"
                                                                        (rewrite
                                                                         "div_mult_pos_le2"
                                                                         1)
                                                                        (("2"
                                                                          (expand
                                                                           "abs"
                                                                           -3)
                                                                          (("2"
                                                                            (case
                                                                             "X0 * X2 + Y0 * Y2 < 0")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil)
                                                                             ("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("3"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (replace
                                                                   -1
                                                                   *
                                                                   rl)
                                                                  (("2"
                                                                    (inst
                                                                     +
                                                                     "0")
                                                                    (("2"
                                                                      (rewrite
                                                                       "cos_0")
                                                                      (("2"
                                                                        (replace
                                                                         -5
                                                                         1
                                                                         rl)
                                                                        (("2"
                                                                          (hide-all-but
                                                                           (-5
                                                                            1))
                                                                          (("2"
                                                                            (lemma
                                                                             "zero_times3"
                                                                             ("x"
                                                                              "sqrt(sq(X0) + sq(Y0))"
                                                                              "y"
                                                                              "sqrt(sq(X2) + sq(Y2))"))
                                                                            (("2"
                                                                              (replace
                                                                               -2
                                                                               -1
                                                                               rl)
                                                                              (("2"
                                                                                (flatten
                                                                                 -1)
                                                                                (("2"
                                                                                  (hide
                                                                                   -2)
                                                                                  (("2"
                                                                                    (split
                                                                                     -1)
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "sqrt_eq"
                                                                                       ("nny"
                                                                                        "sq(X0) + sq(Y0)"
                                                                                        "nnz"
                                                                                        "0"))
                                                                                      (("1"
                                                                                        (rewrite
                                                                                         "sqrt_0")
                                                                                        (("1"
                                                                                          (replace
                                                                                           -2)
                                                                                          (("1"
                                                                                            (flatten)
                                                                                            (("1"
                                                                                              (hide
                                                                                               -2)
                                                                                              (("1"
                                                                                                (lemma
                                                                                                 "sq_plus_eq_0"
                                                                                                 ("a"
                                                                                                  "X0"
                                                                                                  "b"
                                                                                                  "Y0"))
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  (("1"
                                                                                                    (flatten
                                                                                                     -1)
                                                                                                    (("1"
                                                                                                      (assert)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (lemma
                                                                                       "sq_plus_eq_0"
                                                                                       ("a"
                                                                                        "X2"
                                                                                        "b"
                                                                                        "Y2"))
                                                                                      (("2"
                                                                                        (lemma
                                                                                         "sqrt_eq"
                                                                                         ("nny"
                                                                                          "sq(X2) + sq(Y2)"
                                                                                          "nnz"
                                                                                          "0"))
                                                                                        (("2"
                                                                                          (rewrite
                                                                                           "sqrt_0")
                                                                                          (("2"
                                                                                            (replace
                                                                                             -3)
                                                                                            (("2"
                                                                                              (replace
                                                                                               -1
                                                                                               -2
                                                                                               rl)
                                                                                              (("2"
                                                                                                (flatten
                                                                                                 -2)
                                                                                                (("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"
                                                          (hide 2)
                                                          (("2"
                                                            (rewrite
                                                             "sq_le"
                                                             :dir
                                                             rl)
                                                            (("2"
                                                              (replace
                                                               -2
                                                               1
                                                               rl)
                                                              (("2"
                                                                (rewrite
                                                                 "sq_sqrt")
                                                                (("2"
                                                                  (case
                                                                   "FORALL (x:real): sq(abs(x)) = sq(x)")
                                                                  (("1"
                                                                    (inst
                                                                     -
                                                                     "X0 * X2 + Y0 * Y2")
                                                                    (("1"
                                                                      (rewrite
                                                                       "sq_plus")
                                                                      (("1"
                                                                        (rewrite
                                                                         "sq_times")
                                                                        (("1"
                                                                          (rewrite
                                                                           "sq_times")
                                                                          (("1"
                                                                            (simplify
                                                                             1)
                                                                            (("1"
                                                                              (case
                                                                               "2*(X0 * X2 * Y0 * Y2) <= sq(X2) * sq(Y0) + sq(X0) * sq(Y2)")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (hide
                                                                                 2)
                                                                                (("2"
                                                                                  (rewrite
                                                                                   "sq_times"
                                                                                   :dir
                                                                                   rl)
                                                                                  (("2"
                                                                                    (rewrite
                                                                                     "sq_times"
                                                                                     :dir
                                                                                     rl)
                                                                                    (("2"
                                                                                      (lemma
                                                                                       "sq_minus"
                                                                                       ("a"
                                                                                        "X2 * Y0"
                                                                                        "b"
                                                                                        "X0 * Y2"))
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide-all-but
                                                                     1)
                                                                    (("2"
                                                                      (expand
                                                                       "abs")
                                                                      (("2"
                                                                        (skosimp*)
                                                                        (("2"
                                                                          (rewrite
                                                                           "sq_neg")
                                                                          (("2"
                                                                            (case
                                                                             "x!1<0")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil)
                                                                             ("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nonneg_real" law_cosines nil)
    (sq_neg formula-decl nil sq "reals/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (sq_plus formula-decl nil sq "reals/")
    (sq_minus formula-decl nil sq "reals/")
    (sq_times formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq_abs formula-decl nil sq "reals/")
    (sq_le formula-decl nil sq "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (cos_0 formula-decl nil trig_basic nil)
    (sqrt_eq formula-decl nil sqrt "reals/")
    (sq_plus_eq_0 formula-decl nil sq "reals/")
    (sqrt_0 formula-decl nil sqrt "reals/")
    (zero_times3 formula-decl nil real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_div_nzreal_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)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NUM skolem-const-decl "real" law_cosines nil)
    (X0 skolem-const-decl "real" law_cosines nil)
    (X2 skolem-const-decl "real" law_cosines nil)
    (Y2 skolem-const-decl "real" law_cosines nil)
    (Y0 skolem-const-decl "real" law_cosines nil)
    (DEN skolem-const-decl "{nnz: nnreal |
         nnz * nnz =
          sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) +
           sq(Y0) * sq(Y2)}" law_cosines nil)
    (acos const-decl "nnreal_le_pi" acos nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (floor_def formula-decl nil floor_ceil nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (both_sides_times_pos_ge1 formula-decl nil real_props nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (acos_bij formula-decl nil acos 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)
    (mult_neg formula-decl nil extra_tegies nil)
    (injective? const-decl "bool" functions nil)
    (acos_minus1 formula-decl nil acos nil)
    (cos_phase_pi formula-decl nil sincos_phase nil)
    (cos_phase const-decl "real_abs_le1" sincos_phase nil)
    (cos_value_acos formula-decl nil sincos_quad nil)
    (K10 skolem-const-decl "real" law_cosines nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (CBD_12 skolem-const-decl "real" law_cosines nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (neg_neg formula-decl nil extra_tegies nil)
    (neg_one_times formula-decl nil extra_tegies nil)
    (sq_eq formula-decl nil sq "reals/")
    (div_cancel3 formula-decl nil real_props nil)
    (times_div1 formula-decl nil real_props nil)
    (trig_phase nonempty-type-eq-decl nil sincos_phase nil)
    (phase_cos_q1 formula-decl nil sincos_phase nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (< const-decl "bool" reals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (cos const-decl "real" sincos_def nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel4 formula-decl nil real_props nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (nnreal type-eq-decl nil real_types nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt_times formula-decl nil sqrt "reals/")
    (sq_dist const-decl "nonneg_real" law_cosines nil)
    (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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (distance_trans formula-decl nil law_cosines nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil))
   nil)
  (dot_product-1 nil 3269670013
   ("" (skosimp*)
    (("" (lemma "distance_trans" ("x2" "-x1!1" "y2" "-y1!1"))
      (("" (inst-cp - "x1!1" "x0!1" "y1!1" "y0!1")
        (("" (replace -2)
          (("" (inst-cp - "x2!1" "x0!1" "y2!1" "y0!1")
            (("" (replace -2)
              (("" (inst - "x2!1" "x1!1" "y2!1" "y1!1")
                (("" (replace -1)
                  (("" (hide-all-but 1)
                    (("" (name-replace "X0" "x0!1 - x1!1")
                      (("" (name-replace "Y0" "y0!1 - y1!1")
                        (("" (name-replace "X2" "x2!1 - x1!1")
                          (("" (name-replace "Y2" "y2!1 - y1!1")
                            (("" (assert)
                              ((""
                                (expand "dist")
                                ((""
                                  (expand "sq_dist")
                                  ((""
                                    (lemma "sq_neg")
                                    ((""
                                      (inst-cp - "X0")
                                      ((""
                                        (inst-cp - "Y0")
                                        ((""
                                          (replace -2)
                                          ((""
                                            (replace -3)
                                            ((""
                                              (lemma "sqrt_times")
                                              ((""
                                                (inst
                                                 -
                                                 "sq(X0) + sq(Y0)"
                                                 "sq(X2) + sq(Y2)")
                                                ((""
                                                  (case
                                                   "-1 * -x1!1 - x1!1 = 0")
                                                  (("1"
                                                    (replace -1)
                                                    (("1"
                                                      (simplify 1)
                                                      (("1"
                                                        (simplify -2)
                                                        (("1"
                                                          (case
                                                           "abs(X0 * X2 + Y0 * Y2) <= sqrt(sq(X0) + sq(Y0)) * sqrt(sq(X2) + sq(Y2))")
                                                          (("1"
                                                            (typepred
                                                             "sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) +
            (sq(X2) * sq(Y0) + sq(Y0) * sq(Y2)))")
                                                            (("1"
                                                              (expand
                                                               ">="
                                                               -1)
                                                              (("1"
                                                                (expand
                                                                 "<="
                                                                 -1)
                                                                (("1"
                                                                  (split
                                                                   -1)
                                                                  (("1"
                                                                    (case
                                                                     "-1<= (X0 * X2 + Y0 * Y2)/sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) +
             sq(Y0) * sq(Y2))")
                                                                    (("1"
                                                                      (case
                                                                       "(X0 * X2 + Y0 * Y2) /
        sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) +
              sq(Y0) * sq(Y2)) <= 1")
                                                                      (("1"
                                                                        (name-replace
                                                                         "DEN"
                                                                         "sqrt(sq(X0) * sq(X2) + sq(X0) * sq(Y2) + sq(X2) * sq(Y0) +
              sq(Y0) * sq(Y2))")
                                                                        (("1"
                                                                          (name-replace
                                                                           "NUM"
                                                                           "X0 * X2 + Y0 * Y2")
                                                                          (("1"
                                                                            (inst
                                                                             +
                                                                             "acos(NUM/DEN)")
                                                                            (("1"
                                                                              (lemma
                                                                               "div_cancel4"
                                                                               ("y"
                                                                                "cos(acos(NUM / DEN))"
                                                                                "n0z"
                                                                                "sqrt(sq(X0) + sq(Y0)) * sqrt(sq(X2) + sq(Y2))"
                                                                                "x"
                                                                                "NUM"))
                                                                              (("1"
                                                                                (hide-all-but
                                                                                 (-2
                                                                                  -3
                                                                                  -4
                                                                                  1))
                                                                                (("1"
                                                                                  (name-replace
                                                                                   "K10"
                                                                                   "NUM / DEN")
                                                                                  (("1"
                                                                                    (hide
                                                                                     -3)
                                                                                    (("1"
                                                                                      (typepred
                                                                                       "acos(K10)")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "cos")
                                                                                        (("1"
                                                                                          (case
                                                                                           "floor(acos(K10) / (2 * pi))=0")
                                                                                          (("1"
                                                                                            (replace
                                                                                             -1)
                                                                                            (("1"
                                                                                              (simplify
                                                                                               1)
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "<="
                                                                                                 -3)
                                                                                                (("1"
                                                                                                  (split
                                                                                                   -3)
                                                                                                  (("1"
                                                                                                    (hide
                                                                                                     -2)
                                                                                                    (("1"
                                                                                                      (lemma
                                                                                                       "phase_cos_q1"
                                                                                                       ("x"
                                                                                                        "acos(K10)"))
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "cos_phase")
                                                                                                        (("1"
                                                                                                          (expand
                                                                                                           ">=")
                                                                                                          (("1"
                                                                                                            (replace
                                                                                                             -2)
                                                                                                            (("1"
                                                                                                              (replace
                                                                                                               -3)
                                                                                                              (("1"
                                                                                                                (flatten
                                                                                                                 -1)
                                                                                                                (("1"
                                                                                                                  (replace
                                                                                                                   -1)
                                                                                                                  (("1"
                                                                                                                    (lemma
                                                                                                                     "cos_value_acos"
                                                                                                                     ("xa"
                                                                                                                      "K10"))
                                                                                                                    (("1"
                                                                                                                      (replaces
                                                                                                                       -1)
                                                                                                                      (("1"
                                                                                                                        (expand
                                                                                                                         "K10")
                                                                                                                        (("1"
                                                                                                                          (cross-mult
                                                                                                                           1)
                                                                                                                          (("1"
                                                                                                                            (cancel-by
                                                                                                                             1
                                                                                                                             "NUM")
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "DEN"
                                                                                                                               2)
                                                                                                                              (("1"
                                                                                                                                (wrap-formula
                                                                                                                                 2
                                                                                                                                 "sq")
                                                                                                                                (("1"
                                                                                                                                  (grind)
                                                                                                                                  nil
                                                                                                                                  nil)
                                                                                                                                 ("2"
                                                                                                                                  (rewrite
                                                                                                                                   "sq_eq")
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (replace
                                                                                                     -1)
                                                                                                    (("2"
                                                                                                      (rewrite
                                                                                                       "cos_phase_pi")
                                                                                                      (("2"
                                                                                                        (lemma
                                                                                                         "acos_bij")
                                                                                                        (("2"
                                                                                                          (lemma
                                                                                                           "acos_minus1")
                                                                                                          (("2"
                                                                                                            (expand
                                                                                                             "bijective?")
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "injective?")
                                                                                                              (("2"
                                                                                                                (flatten
                                                                                                                 -2)
                                                                                                                (("2"
                                                                                                                  (inst
                                                                                                                   -
                                                                                                                   "K10"
                                                                                                                   "-1")
                                                                                                                  (("1"
                                                                                                                    (assert)
                                                                                                                    (("1"
                                                                                                                      (replaces
                                                                                                                       -2
                                                                                                                       :dir
                                                                                                                       rl)
                                                                                                                      (("1"
                                                                                                                        (expand
                                                                                                                         "K10")
                                                                                                                        (("1"
                                                                                                                          (cross-mult
                                                                                                                           1)
                                                                                                                          (("1"
                                                                                                                            (cancel-by
                                                                                                                             1
                                                                                                                             "NUM")
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "DEN"
                                                                                                                               2)
                                                                                                                              (("1"
                                                                                                                                (wrap-formula
                                                                                                                                 2
                                                                                                                                 "sq")
                                                                                                                                (("1"
                                                                                                                                  (grind)
                                                                                                                                  nil
                                                                                                                                  nil)
                                                                                                                                 ("2"
                                                                                                                                  (rewrite
                                                                                                                                   "sq_eq")
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("2"
                                                                                                                    (expand
                                                                                                                     "abs")
                                                                                                                    (("2"
                                                                                                                      (assert)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("3"
                                                                                                                    (expand
                                                                                                                     "abs"
                                                                                                                     1)
                                                                                                                    (("3"
                                                                                                                      (case
                                                                                                                       "K10<0")
                                                                                                                      (("1"
                                                                                                                        (assert)
                                                                                                                        nil
                                                                                                                        nil)
                                                                                                                       ("2"
                                                                                                                        (assert)
                                                                                                                        nil
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (name-replace
                                                                                             "K11"
                                                                                             "acos(K10)")
                                                                                            (("2"
                                                                                              (hide
                                                                                               -3
                                                                                               -4
                                                                                               2)
                                                                                              (("2"
                                                                                                (lemma
                                                                                                 "floor_def"
                                                                                                 ("x"
                                                                                                  "K11 / (2 * pi)"))
                                                                                                (("2"
                                                                                                  (rewrite
                                                                                                   "div_mult_pos_lt1")
                                                                                                  (("2"
                                                                                                    (rewrite
                                                                                                     "div_mult_pos_le2")
                                                                                                    (("2"
                                                                                                      (flatten
                                                                                                       -1)
                                                                                                      (("2"
                                                                                                        (name-replace
                                                                                                         "K12"
                                                                                                         "floor(K11 / (2 * pi))")
                                                                                                        (("2"
                                                                                                          (case
                                                                                                           "K12>=1")
                                                                                                          (("1"
                                                                                                            (lemma
                                                                                                             "both_sides_times_pos_ge1"
                                                                                                             ("x"
                                                                                                              "K12"
                                                                                                              "y"
                                                                                                              "1"
                                                                                                              "pz"
                                                                                                              "2*pi"))
                                                                                                            (("1"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil)
                                                                                                           ("2"
                                                                                                            (case
                                                                                                             "K12<=-1")
                                                                                                            (("1"
                                                                                                              (lemma
                                                                                                               "both_sides_times_pos_le1"
                                                                                                               ("x"
                                                                                                                "K12"
                                                                                                                "y"
                                                                                                                "-1"
                                                                                                                "pz"
                                                                                                                "2*pi"))
                                                                                                              (("1"
                                                                                                                (assert)
                                                                                                                nil
                                                                                                                nil))
                                                                                                              nil)
                                                                                                             ("2"
                                                                                                              (assert)
                                                                                                              nil
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (expand
                                                                                         "abs")
                                                                                        (("2"
                                                                                          (case
                                                                                           "K10<0")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil)
                                                                                           ("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (expand
                                                                                 "abs"
                                                                                 1)
                                                                                (("2"
                                                                                  (case
                                                                                   "NUM / DEN < 0")
                                                                                  (("1"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil)
                                                                                   ("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil)
                                                                                   ("3"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("3"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("4"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (expand
                                                                               "abs")
                                                                              (("2"
                                                                                (case
                                                                                 "NUM / DEN < 0")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil)
                                                                                 ("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil)
                                                                                 ("3"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("3"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide
                                                                         -1
                                                                         2)
                                                                        (("2"
                                                                          (rewrite
                                                                           "div_mult_pos_le1"
                                                                           1)
                                                                          (("2"
                                                                            (expand
                                                                             "abs"
                                                                             -3)
                                                                            (("2"
                                                                              (case
                                                                               "X0 * X2 + Y0 * Y2 < 0")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2)
                                                                      (("2"
                                                                        (replace
                                                                         -5
                                                                         -3
                                                                         rl)
                                                                        (("2"
                                                                          (rewrite
                                                                           "div_mult_pos_le2"
                                                                           1)
                                                                          (("2"
                                                                            (expand
                                                                             "abs"
                                                                             -3)
                                                                            (("2"
                                                                              (case
                                                                               "X0 * X2 + Y0 * Y2 < 0")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("3"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (replace
                                                                     -1
                                                                     *
                                                                     rl)
                                                                    (("2"
                                                                      (inst
                                                                       +
                                                                       "0")
                                                                      (("2"
                                                                        (rewrite
                                                                         "cos_0")
                                                                        (("2"
                                                                          (replace
                                                                           -5
                                                                           1
                                                                           rl)
                                                                          (("2"
                                                                            (hide-all-but
                                                                             (-5
                                                                              1))
                                                                            (("2"
                                                                              (lemma
                                                                               "zero_times3"
                                                                               ("x"
                                                                                "sqrt(sq(X0) + sq(Y0))"
                                                                                "y"
                                                                                "sqrt(sq(X2) + sq(Y2))"))
                                                                              (("2"
                                                                                (replace
                                                                                 -2
                                                                                 -1
                                                                                 rl)
                                                                                (("2"
                                                                                  (flatten
                                                                                   -1)
                                                                                  (("2"
                                                                                    (hide
                                                                                     -2)
                                                                                    (("2"
                                                                                      (split
                                                                                       -1)
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "sqrt_eq"
                                                                                         ("nny"
                                                                                          "sq(X0) + sq(Y0)"
                                                                                          "nnz"
                                                                                          "0"))
                                                                                        (("1"
                                                                                          (rewrite
                                                                                           "sqrt_0")
                                                                                          (("1"
                                                                                            (replace
                                                                                             -2)
                                                                                            (("1"
                                                                                              (flatten)
                                                                                              (("1"
                                                                                                (hide
                                                                                                 -2)
                                                                                                (("1"
                                                                                                  (lemma
                                                                                                   "sq_plus_eq_0"
                                                                                                   ("a"
                                                                                                    "X0"
                                                                                                    "b"
                                                                                                    "Y0"))
                                                                                                  (("1"
                                                                                                    (assert)
                                                                                                    (("1"
                                                                                                      (flatten
                                                                                                       -1)
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (lemma
                                                                                         "sq_plus_eq_0"
                                                                                         ("a"
                                                                                          "X2"
                                                                                          "b"
                                                                                          "Y2"))
                                                                                        (("2"
                                                                                          (lemma
                                                                                           "sqrt_eq"
                                                                                           ("nny"
                                                                                            "sq(X2) + sq(Y2)"
                                                                                            "nnz"
                                                                                            "0"))
                                                                                          (("2"
                                                                                            (rewrite
                                                                                             "sqrt_0")
                                                                                            (("2"
                                                                                              (replace
                                                                                               -3)
                                                                                              (("2"
                                                                                                (replace
                                                                                                 -1
                                                                                                 -2
                                                                                                 rl)
                                                                                                (("2"
                                                                                                  (flatten
                                                                                                   -2)
                                                                                                  (("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"
                                                            (hide 2)
                                                            (("2"
                                                              (rewrite
                                                               "sq_le"
                                                               :dir
                                                               rl)
                                                              (("2"
                                                                (replace
                                                                 -2
                                                                 1
                                                                 rl)
                                                                (("2"
                                                                  (rewrite
                                                                   "sq_sqrt")
                                                                  (("2"
                                                                    (case
                                                                     "FORALL (x:real): sq(abs(x)) = sq(x)")
                                                                    (("1"
                                                                      (inst
                                                                       -
                                                                       "X0 * X2 + Y0 * Y2")
                                                                      (("1"
                                                                        (replace
                                                                         -1)
                                                                        (("1"
                                                                          (rewrite
                                                                           "sq_plus")
                                                                          (("1"
                                                                            (rewrite
                                                                             "sq_times")
                                                                            (("1"
                                                                              (rewrite
                                                                               "sq_times")
                                                                              (("1"
                                                                                (simplify
                                                                                 1)
                                                                                (("1"
                                                                                  (case
                                                                                   "2*(X0 * X2 * Y0 * Y2) <= sq(X2) * sq(Y0) + sq(X0) * sq(Y2)")
                                                                                  (("1"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil)
                                                                                   ("2"
                                                                                    (hide
                                                                                     2)
                                                                                    (("2"
                                                                                      (rewrite
                                                                                       "sq_times"
                                                                                       :dir
                                                                                       rl)
                                                                                      (("2"
                                                                                        (rewrite
                                                                                         "sq_times"
                                                                                         :dir
                                                                                         rl)
                                                                                        (("2"
                                                                                          (lemma
                                                                                           "sq_minus"
                                                                                           ("a"
                                                                                            "X2 * Y0"
                                                                                            "b"
                                                                                            "X0 * Y2"))
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide-all-but
                                                                       1)
                                                                      (("2"
                                                                        (expand
                                                                         "abs")
                                                                        (("2"
                                                                          (skosimp*)
                                                                          (("2"
                                                                            (rewrite
                                                                             "sq_neg")
                                                                            (("2"
                                                                              (case
                                                                               "x!1<0")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_neg formula-decl nil sq "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_times formula-decl nil sq "reals/")
    (sq_minus formula-decl nil sq "reals/")
    (sq_plus formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq_le formula-decl nil sq "reals/")
    (cos_0 formula-decl nil trig_basic nil)
    (sqrt_eq formula-decl nil sqrt "reals/")
    (sq_plus_eq_0 formula-decl nil sq "reals/")
    (sqrt_0 formula-decl nil sqrt "reals/")
    (acos const-decl "nnreal_le_pi" acos nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (pi const-decl "posreal" atan nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (acos_bij formula-decl nil acos nil)
    (acos_minus1 formula-decl nil acos nil)
    (cos_phase_pi formula-decl nil sincos_phase nil)
    (cos_phase const-decl "real_abs_le1" sincos_phase nil)
    (cos_value_acos formula-decl nil sincos_quad nil)
    (sq_eq formula-decl nil sq "reals/")
    (trig_phase nonempty-type-eq-decl nil sincos_phase nil)
    (phase_cos_q1 formula-decl nil sincos_phase nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sqrt_times formula-decl nil sqrt "reals/"))
   shostak))
 (Law_Cosines 0
  (Law_Cosines-1 nil 3269434431
   ("" (expand "dist")
    (("" (expand "sq_dist")
      (("" (ground)
        (("" (expand "sq")
          (("" (ground) (("" (skosimp*) (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_dist const-decl "nonneg_real" law_cosines nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (dist const-decl "nonneg_real" law_cosines nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (triangle 0
  (triangle-1 nil 3269434431
   (""
    (case "FORALL (x,y:real): dist(0,0,0,1) <= dist(x,y,0,1) + dist(x,y,0,0)")
    (("1"
      (case "FORALL (x,y:real,pz:posreal): dist(0, 0, 0, pz) <= dist(x, y, 0, pz) + dist(x, y, 0, 0)")
      (("1" (hide -2)
        (("1"
          (case "FORALL (x,y,a,b:real): dist(0, 0, a,b) <= dist(x, y, a,b) + dist(x, y, 0, 0)")
          (("1" (hide -2)
            (("1" (skosimp*)
              (("1"
                (lemma "distance_trans" ("x2" "-x0!1" "y2" "-y0!1"))
                (("1" (inst-cp - "x0!1" "x1!1" "y0!1" "y1!1")
                  (("1" (inst-cp - "x2!1" "x1!1" "y2!1" "y1!1")
                    (("1" (inst - "x2!1" "x0!1" "y2!1" "y0!1")
                      (("1"
                        (inst - "x2!1-x0!1" "y2!1-y0!1" "x1!1-x0!1"
                         "y1!1-y0!1")
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (skosimp*)
              (("2" (case "a!1=0")
                (("1" (replace -1)
                  (("1" (lemma "trichotomy" ("x" "b!1"))
                    (("1" (split -1)
                      (("1" (inst - "x!1" "y!1" "b!1")
                        (("1" (assert) nil nil)) nil)
                       ("2" (replace -1)
                        (("2" (expand "dist")
                          (("2" (expand "sq_dist")
                            (("2" (rewrite "sq_0")
                              (("2"
                                (rewrite "sqrt_0")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("3" (inst - "x!1" "-y!1" "-b!1")
                        (("1" (expand "dist")
                          (("1" (expand "sq_dist")
                            (("1" (sq-simp) nil nil)) nil))
                          nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (name "theta" "atan2(b!1,a!1)")
                  (("1" (lemma "distance_rot" ("ac" "theta"))
                    (("1" (lemma "sin_atan2" ("x" "b!1" "y" "a!1"))
                      (("1" (lemma "cos_atan2" ("x" "b!1" "y" "a!1"))
                        (("1" (assert)
                          (("1" (replace -4)
                            (("1" (inst-cp - "0" "a!1" "0" "b!1")
                              (("1"
                                (simplify -4)
                                (("1"
                                  (case
                                   "cos(theta) * a!1 - sin(theta) * b!1 = 0")
                                  (("1"
                                    (case
                                     "cos(theta) * b!1 + sin(theta) * a!1 = sqrt(sq(a!1)+sq(b!1))")
                                    (("1"
                                      (inst-cp - "x!1" "0" "y!1" "0")
                                      (("1"
                                        (inst
                                         -
                                         "x!1"
                                         "a!1"
                                         "y!1"
                                         "b!1")
                                        (("1"
                                          (replace -1)
                                          (("1"
                                            (replace -2)
                                            (("1"
                                              (replace -5)
                                              (("1"
                                                (replace -6)
                                                (("1"
                                                  (replace -7)
                                                  (("1"
                                                    (simplify 2)
                                                    (("1"
                                                      (inst
                                                       -
                                                       "cos(theta) * x!1 - sin(theta) * y!1"
                                                       "cos(theta) * y!1 + sin(theta) * x!1"
                                                       "sqrt(sq(a!1) + sq(b!1))")
                                                      (("1"
                                                        (hide
                                                         -3
                                                         -4
                                                         -5
                                                         -6
                                                         -7
                                                         -8
                                                         3)
                                                        (("1"
                                                          (lemma
                                                           "sqrt_pos"
                                                           ("px"
                                                            "sq(a!1) + sq(b!1)"))
                                                          (("1"
                                                            (propax)
                                                            nil
                                                            nil)
                                                           ("2"
                                                            (hide
                                                             -1
                                                             -2
                                                             2)
                                                            (("2"
                                                              (lemma
                                                               "sq_nz_pos"
                                                               ("nz"
                                                                "a!1"))
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide -1 -4 -5 -6 -7 3)
                                      (("2"
                                        (case "b!1=0")
                                        (("1"
                                          (replace -1)
                                          (("1"
                                            (rewrite "sq_0")
                                            (("1"
                                              (simplify 1)
                                              (("1"
                                                (case "a!1>0")
                                                (("1"
                                                  (rewrite "sqrt_sq")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (lemma
                                                   "sq_neg"
                                                   ("a" "a!1"))
                                                  (("2"
                                                    (replace -1 2 rl)
                                                    (("2"
                                                      (rewrite
                                                       "sqrt_sq")
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (assert)
                                          (("2"
                                            (case
                                             "1 + sq(a!1 / b!1) = (sq(a!1)+sq(b!1))/sq(b!1)")
                                            (("1"
                                              (replace -1)
                                              (("1"
                                                (rewrite "sqrt_div")
                                                (("1"
                                                  (case "b!1>0")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (rewrite
                                                       "div_div1")
                                                      (("1"
                                                        (rewrite
                                                         "div_div1")
                                                        (("1"
                                                          (lemma
                                                           "div_cancel2"
                                                           ("x"
                                                            "a!1"
                                                            "n0z"
                                                            "b!1"))
                                                          (("1"
                                                            (replace
                                                             -1
                                                             -5)
                                                            (("1"
                                                              (replace
                                                               -4)
                                                              (("1"
                                                                (replace
                                                                 -5)
                                                                (("1"
                                                                  (lemma
                                                                   "div_cancel3"
                                                                   ("x"
                                                                    "b!1*b!1+a!1*a!1"
                                                                    "n0z"
                                                                    "sqrt(sq(a!1) + sq(b!1))"
                                                                    "y"
                                                                    "sqrt(sq(a!1) + sq(b!1))"))
                                                                  (("1"
                                                                    (replace
                                                                     -1
                                                                     2)
                                                                    (("1"
                                                                      (rewrite
                                                                       "sq_rew"
                                                                       2)
                                                                      (("1"
                                                                        (rewrite
                                                                         "sq_rew"
                                                                         2)
                                                                        (("1"
                                                                          (rewrite
                                                                           "sq_rew"
                                                                           2)
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    (("2"
                                                      (rewrite
                                                       "div_div1")
                                                      (("2"
                                                        (rewrite
                                                         "div_div1")
                                                        (("2"
                                                          (lemma
                                                           "sq_neg"
                                                           ("a" "b!1"))
                                                          (("2"
                                                            (replace
                                                             -1
                                                             *
                                                             rl)
                                                            (("2"
                                                              (case
                                                               "-((a!1 / b!1 * -b!1) / sqrt((sq(a!1) + sq(-b!1)))) = a!1/ sqrt((sq(a!1) + sq(-b!1)))")
                                                              (("1"
                                                                (replace
                                                                 -1)
                                                                (("1"
                                                                  (case
                                                                   "-1*-b!1=b!1")
                                                                  (("1"
                                                                    (replace
                                                                     -1)
                                                                    (("1"
                                                                      (hide
                                                                       -1
                                                                       -2
                                                                       -4)
                                                                      (("1"
                                                                        (replace
                                                                         -2)
                                                                        (("1"
                                                                          (replace
                                                                           -3)
                                                                          (("1"
                                                                            (replace
                                                                             -1)
                                                                            (("1"
                                                                              (hide
                                                                               (-1
                                                                                -2
                                                                                -3))
                                                                              (("1"
                                                                                (lemma
                                                                                 "div_cancel3")
                                                                                (("1"
                                                                                  (inst
                                                                                   -
                                                                                   "sqrt(sq(a!1) + sq(b!1))"
                                                                                   "b!1*b!1+a!1*a!1"
                                                                                   "sqrt(sq(a!1) + sq(b!1))")
                                                                                  (("1"
                                                                                    (replace
                                                                                     -1
                                                                                     3)
                                                                                    (("1"
                                                                                      (rewrite
                                                                                       "sq_rew")
                                                                                      (("1"
                                                                                        (rewrite
                                                                                         "sq_rew")
                                                                                        (("1"
                                                                                          (rewrite
                                                                                           "sq_rew")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (hide
                                                                 4
                                                                 -3
                                                                 -4)
                                                                (("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (lemma
                                                   "sq_nz_pos"
                                                   ("nz" "b!1"))
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (rewrite "sq_div")
                                              (("2" (assert) nil nil))
                                              nil)
                                             ("3"
                                              (lemma
                                               "sq_nz_pos"
                                               ("nz" "b!1"))
                                              (("3" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide -3 -4 -5 -6 3)
                                    (("2"
                                      (case "b!1=0")
                                      (("1" (assert) nil nil)
                                       ("2"
                                        (case "b!1>0")
                                        (("1" (assert) nil nil)
                                         ("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (case "b!1=0")
                    (("1" (assert) nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skosimp*)
          (("2" (lemma "distance_scale" ("pz" "pz!1"))
            (("2" (inst-cp - "0" "0" "0" "1")
              (("2" (inst-cp - "x!1/pz!1" "0" "y!1/pz!1" "1")
                (("2" (inst - "x!1/pz!1" "0" "y!1/pz!1" "0")
                  (("2" (inst - "x!1/pz!1" "y!1/pz!1")
                    (("2"
                      (lemma "both_sides_times_pos_le1"
                       ("x" "dist(0, 0, 0, 1)" "y"
                        "dist(x!1/pz!1, y!1/pz!1, 0, 1) + dist(x!1/pz!1, y!1/pz!1, 0, 0)"
                        "pz" "pz!1"))
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp*)
        (("2" (expand "dist")
          (("2" (expand "sq_dist")
            (("2" (rewrite "sq_0")
              (("2" (name-replace "K1" "sq(x!1)")
                (("2" (rewrite "sq_le" :dir rl)
                  (("2" (rewrite "sq_plus")
                    (("2" (rewrite "sq_minus")
                      (("2" (lemma "trichotomy" ("x" "y!1"))
                        (("2" (split -1)
                          (("1"
                            (case "sq(y!1) - 2 * y!1 + K1 + (sq(y!1) + K1) >=0")
                            (("1" (assert) nil nil)
                             ("2"
                              (case "y!1-sq(y!1)-K1 <= (sqrt(1 + sq(y!1) - 2 * y!1 + K1) * sqrt(sq(y!1) + K1))")
                              (("1" (assert) nil nil)
                               ("2"
                                (hide 3)
                                (("2"
                                  (rewrite "sqrt_times" :dir rl)
                                  (("2"
                                    (rewrite "sq_le" :dir rl)
                                    (("2"
                                      (expand "sq" 1)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3" (assert) nil nil))
                              nil))
                            nil)
                           ("2" (replace -1)
                            (("2" (rewrite "sq_0")
                              (("2" (assert) nil nil)) nil))
                            nil)
                           ("3" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_le formula-decl nil sq "reals/")
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sq_1 formula-decl nil sq "reals/")
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (odd_minus_even_is_odd application-judgement "odd_int" integers
     nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (sq_plus formula-decl nil sq "reals/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (distance_trans formula-decl nil law_cosines nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 nil)
    (pi const-decl "posreal" atan nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (atan2 const-decl "real" atan2 nil)
    (/= const-decl "boolean" notequal nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nil application-judgement "nnreal_lt_2pi" atan2 nil)
    (sin_atan2 formula-decl nil atan2 nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (sin_range application-judgement "trig_range" sincos_def nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (cos const-decl "real" sincos_def nil)
    (sin const-decl "real" sincos_def nil)
    (sq_div formula-decl nil sq "reals/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (npreal_div_posreal_is_npreal application-judgement "npreal"
     real_types nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_div1 formula-decl nil real_props nil)
    (div_cancel2 formula-decl nil real_props nil)
    (div_cancel3 formula-decl nil real_props nil)
    (sq_rew formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sqrt_div formula-decl nil sqrt "reals/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_sq formula-decl nil sqrt "reals/")
    (a!1 skolem-const-decl "real" law_cosines nil)
    (sqrt_pos judgement-tcc nil sqrt "reals/")
    (sq_nz_pos judgement-tcc nil sq "reals/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (cos_atan2 formula-decl nil atan2 nil)
    (distance_rot formula-decl nil law_cosines nil)
    (b!1 skolem-const-decl "real" law_cosines nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_0 formula-decl nil sq "reals/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqrt_0 formula-decl nil sqrt "reals/")
    (sq_dist const-decl "nonneg_real" law_cosines nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqrt_times formula-decl nil sqrt "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sqrt_sq_neg formula-decl nil sqrt "reals/")
    (sq_minus formula-decl nil sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (sq_times formula-decl nil sq "reals/")
    (sq_neg formula-decl nil sq "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (trichotomy formula-decl nil real_axioms nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (distance_scale formula-decl nil law_cosines nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (dist const-decl "nonneg_real" law_cosines nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   nil)))